From b002318881bb5dfacb7fde54e3cb41b24d135ddb Mon Sep 17 00:00:00 2001 From: Cosimo Oliboni Date: Tue, 2 Feb 2010 08:38:57 +0000 Subject: [PATCH] freescale porting --- .../matita/contribs/ng_assembly/depends | 177 ++-- .../emulator/tests/medium_tests.ma | 883 ++++++++++++++++++ .../emulator/tests/medium_tests_tools.ma | 592 ++++++++++++ .../emulator/tests/micro_tests1.ma | 141 +++ .../emulator/tests/micro_tests_tools.ma | 80 ++ 5 files changed, 1788 insertions(+), 85 deletions(-) create mode 100755 helm/software/matita/contribs/ng_assembly/emulator/tests/medium_tests.ma create mode 100755 helm/software/matita/contribs/ng_assembly/emulator/tests/medium_tests_tools.ma create mode 100755 helm/software/matita/contribs/ng_assembly/emulator/tests/micro_tests1.ma create mode 100755 helm/software/matita/contribs/ng_assembly/emulator/tests/micro_tests_tools.ma diff --git a/helm/software/matita/contribs/ng_assembly/depends b/helm/software/matita/contribs/ng_assembly/depends index a6e34a5ba..0e0eb8a5f 100644 --- a/helm/software/matita/contribs/ng_assembly/depends +++ b/helm/software/matita/contribs/ng_assembly/depends @@ -1,104 +1,111 @@ -num/word24_lemmas.ma num/byte8_lemmas.ma num/word24.ma -emulator/model/HCS08_model.ma emulator/status/status.ma -common/prod_lemmas.ma common/prod.ma num/bool_lemmas.ma -emulator/opcodes/HC05_table_tests.ma emulator/opcodes/HC05_table.ma emulator/opcodes/pseudo.ma -num/bool.ma common/theory.ma +common/sigma.ma common/theory.ma compiler/preast_tree.ma common/string.ma compiler/ast_type.ma num/word32.ma -emulator/status/RS08_status_lemmas.ma emulator/status/RS08_status.ma num/word16_lemmas.ma -emulator/status/HC08_status.ma num/word16.ma -common/nat.ma num/bool.ma -common/nat_to_num.ma common/nat.ma num/word32.ma -common/string_lemmas.ma common/ascii_lemmas.ma common/list_utility_lemmas.ma common/string.ma emulator/opcodes/IP2022_pseudo.ma num/bool.ma -compiler/ast_type_lemmas.ma common/list_utility_lemmas.ma compiler/ast_type.ma -emulator/memory/memory_struct_lemmas.ma emulator/memory/memory_struct.ma num/bool_lemmas.ma -emulator/read_write/load_write.ma emulator/read_write/Freescale_load_write.ma emulator/read_write/IP2022_load_write.ma -num/quatern.ma num/bool.ma +emulator/status/HC08_status_lemmas.ma emulator/status/HC08_status.ma num/word16_lemmas.ma +emulator/status/HC05_status_lemmas.ma emulator/status/HC05_status.ma num/word16_lemmas.ma +emulator/multivm/multivm.ma emulator/multivm/Freescale_multivm.ma emulator/multivm/IP2022_multivm.ma emulator/read_write/fetch.ma +emulator/translation/translation.ma emulator/translation/Freescale_translation.ma emulator/translation/IP2022_translation.ma +num/word24.ma num/byte8.ma +num/bool_lemmas.ma num/bool.ma +emulator/multivm/multivm_lemmas.ma common/nat_lemmas.ma emulator/multivm/multivm.ma +emulator/opcodes/IP2022_instr_mode.ma num/word16.ma +common/string.ma common/ascii.ma common/list_utility.ma +compiler/environment.ma common/string.ma compiler/ast_type.ma +emulator/opcodes/HC08_table.ma common/list.ma emulator/opcodes/Freescale_instr_mode.ma emulator/opcodes/Freescale_pseudo.ma emulator/opcodes/byte_or_word.ma num/exadecim.ma common/prod.ma num/bool.ma num/oct.ma num/quatern.ma -emulator/status/IP2022_status_lemmas.ma emulator/memory/memory_struct_lemmas.ma emulator/status/IP2022_status.ma num/oct_lemmas.ma num/word16_lemmas.ma num/word24_lemmas.ma -num/bitrigesim_lemmas.ma num/bitrigesim.ma num/bool_lemmas.ma -emulator/status/status_lemmas.ma common/option_lemmas.ma common/prod_lemmas.ma emulator/opcodes/pseudo_lemmas.ma emulator/status/HC05_status_lemmas.ma emulator/status/HC08_status_lemmas.ma emulator/status/IP2022_status_lemmas.ma emulator/status/RS08_status_lemmas.ma emulator/status/status.ma -emulator/status/status.ma emulator/memory/memory_abs.ma emulator/opcodes/pseudo.ma emulator/status/HC05_status.ma emulator/status/HC08_status.ma emulator/status/IP2022_status.ma emulator/status/RS08_status.ma +emulator/opcodes/IP2022_pseudo_lemmas.ma emulator/opcodes/IP2022_pseudo.ma num/bool_lemmas.ma +common/list_utility.ma common/list.ma common/nat_lemmas.ma common/option.ma +emulator/read_write/RS08_read_write.ma emulator/status/status_setter.ma num/byte8.ma common/nat.ma num/bitrigesim.ma num/comp_num.ma num/exadecim.ma -emulator/model/model.ma emulator/model/HC05_model.ma emulator/model/HC08_model.ma emulator/model/HCS08_model.ma emulator/model/IP2022_model.ma emulator/model/RS08_model.ma -emulator/opcodes/HC08_table.ma common/list.ma emulator/opcodes/Freescale_instr_mode.ma emulator/opcodes/Freescale_pseudo.ma emulator/opcodes/byte_or_word.ma -common/nat_lemmas.ma common/nat.ma num/bool_lemmas.ma -emulator/multivm/multivm.ma emulator/multivm/Freescale_multivm.ma -emulator/opcodes/HC05_table.ma common/list.ma emulator/opcodes/Freescale_instr_mode.ma emulator/opcodes/Freescale_pseudo.ma emulator/opcodes/byte_or_word.ma -common/list_utility_lemmas.ma common/list_lemmas.ma common/list_utility.ma -emulator/memory/memory_trees.ma common/list.ma common/option.ma emulator/memory/memory_struct.ma num/word32.ma -emulator/opcodes/Freescale_pseudo.ma num/bool.ma -num/word32_lemmas.ma num/word16_lemmas.ma num/word32.ma -emulator/opcodes/RS08_table_tests.ma emulator/opcodes/RS08_table.ma emulator/opcodes/pseudo.ma -emulator/opcodes/Freescale_instr_mode_lemmas.ma emulator/opcodes/Freescale_instr_mode.ma num/bitrigesim_lemmas.ma num/bool_lemmas.ma num/exadecim_lemmas.ma num/oct_lemmas.ma -test_errori.ma -emulator/multivm/multivm_base.ma common/theory.ma emulator/status/status_setter.ma -compiler/environment.ma common/string.ma compiler/ast_type.ma -common/ascii_lemmas.ma common/ascii.ma num/bool_lemmas.ma emulator/read_write/IP2022_read_write.ma emulator/read_write/read_write_base.ma emulator/status/status_setter.ma -emulator/translation/translation_base.ma common/option.ma emulator/opcodes/HC05_table.ma emulator/opcodes/HC08_table.ma emulator/opcodes/HCS08_table.ma emulator/opcodes/IP2022_table.ma emulator/opcodes/RS08_table.ma emulator/opcodes/pseudo.ma -emulator/opcodes/IP2022_table.ma common/list.ma emulator/opcodes/IP2022_instr_mode.ma emulator/opcodes/IP2022_pseudo.ma emulator/opcodes/byte_or_word.ma +emulator/model/RS08_model.ma emulator/status/status.ma +emulator/status/RS08_status_lemmas.ma emulator/status/RS08_status.ma num/word16_lemmas.ma +num/byte8_lemmas.ma num/byte8.ma num/comp_num_lemmas.ma num/exadecim_lemmas.ma +num/oct_lemmas.ma num/bool_lemmas.ma num/oct.ma emulator/status/HC05_status.ma num/word16.ma -emulator/opcodes/Freescale_pseudo_lemmas.ma emulator/opcodes/Freescale_pseudo.ma num/bool_lemmas.ma +num/bool.ma common/theory.ma +emulator/model/HC05_model.ma emulator/status/status.ma +emulator/tests/micro_tests_tools.ma common/list.ma num/word16.ma +emulator/translation/Freescale_translation.ma emulator/translation/translation_base.ma +emulator/opcodes/HC08_table_tests.ma emulator/opcodes/HC08_table.ma emulator/opcodes/pseudo.ma +emulator/status/IP2022_status.ma emulator/memory/memory_struct.ma num/word16.ma num/word24.ma +num/bitrigesim_lemmas.ma num/bitrigesim.ma num/bool_lemmas.ma +emulator/status/status.ma emulator/memory/memory_abs.ma emulator/opcodes/pseudo.ma emulator/status/HC05_status.ma emulator/status/HC08_status.ma emulator/status/IP2022_status.ma emulator/status/RS08_status.ma emulator/memory/memory_bits.ma emulator/memory/memory_trees.ma -common/theory.ma -common/string.ma common/ascii.ma common/list_utility.ma -emulator/read_write/RS08_read_write.ma emulator/status/status_setter.ma -emulator/opcodes/byte_or_word.ma num/word16.ma -compiler/ast_type.ma common/list_utility.ma -num/word16.ma num/byte8.ma -common/prod.ma num/bool.ma -emulator/opcodes/IP2022_instr_mode.ma num/word16.ma -num/exadecim_lemmas.ma num/bool_lemmas.ma num/exadecim.ma -num/word16_lemmas.ma num/byte8_lemmas.ma num/word16.ma -emulator/status/HC05_status_lemmas.ma emulator/status/HC05_status.ma num/word16_lemmas.ma -emulator/status/status_getter.ma emulator/status/status_setter.ma -num/word24.ma num/byte8.ma -num/bool_lemmas.ma num/bool.ma -emulator/model/HC08_model.ma emulator/status/status.ma -emulator/memory/memory_abs.ma emulator/memory/memory_bits.ma emulator/memory/memory_func.ma emulator/memory/memory_trees.ma -num/oct_lemmas.ma num/bool_lemmas.ma num/oct.ma +emulator/opcodes/RS08_table_tests.ma emulator/opcodes/RS08_table.ma emulator/opcodes/pseudo.ma +emulator/model/HCS08_model.ma emulator/status/status.ma emulator/read_write/Freescale_load_write.ma emulator/read_write/load_write_base.ma emulator/status/status_getter.ma -emulator/memory/memory_struct.ma num/byte8.ma num/oct.ma -emulator/model/HC05_model.ma emulator/status/status.ma +num/quatern.ma num/bool.ma +emulator/opcodes/Freescale_instr_mode.ma num/word16.ma +common/nat_lemmas.ma common/nat.ma num/bool_lemmas.ma +universe/universe.ma common/list.ma common/nat_lemmas.ma common/prod.ma +emulator/translation/translation_base.ma common/option.ma emulator/opcodes/HC05_table.ma emulator/opcodes/HC08_table.ma emulator/opcodes/HCS08_table.ma emulator/opcodes/IP2022_table.ma emulator/opcodes/RS08_table.ma emulator/opcodes/pseudo.ma +num/word16_lemmas.ma num/byte8_lemmas.ma num/word16.ma +emulator/read_write/IP2022_load_write.ma emulator/read_write/load_write_base.ma emulator/status/status_getter.ma +emulator/tests/micro_tests2.ma emulator/multivm/multivm.ma emulator/status/status_lemmas.ma emulator/tests/micro_tests_tools.ma +emulator/memory/memory_trees.ma common/list.ma common/option.ma emulator/memory/memory_struct.ma num/word32.ma +common/nat.ma num/bool.ma +emulator/status/RS08_status.ma num/word16.ma +compiler/ast_type_lemmas.ma common/list_utility_lemmas.ma compiler/ast_type.ma +common/string_lemmas.ma common/ascii_lemmas.ma common/list_utility_lemmas.ma common/string.ma +emulator/status/IP2022_status_lemmas.ma emulator/memory/memory_struct_lemmas.ma emulator/status/IP2022_status.ma num/oct_lemmas.ma num/word16_lemmas.ma num/word24_lemmas.ma +num/comp_num.ma num/exadecim.ma emulator/status/status_setter.ma emulator/status/status.ma -num/word32.ma num/word16.ma +emulator/multivm/IP2022_multivm.ma emulator/multivm/multivm_base.ma emulator/read_write/load_write.ma +num/quatern_lemmas.ma num/bool_lemmas.ma num/quatern.ma +common/list.ma common/theory.ma +emulator/opcodes/HCS08_table.ma common/list.ma emulator/opcodes/Freescale_instr_mode.ma emulator/opcodes/Freescale_pseudo.ma emulator/opcodes/byte_or_word.ma +emulator/opcodes/HC05_table_tests.ma emulator/opcodes/HC05_table.ma emulator/opcodes/pseudo.ma common/ascii.ma num/bool.ma -emulator/read_write/load_write_base.ma emulator/read_write/read_write.ma +num/exadecim_lemmas.ma num/bool_lemmas.ma num/exadecim.ma +emulator/memory/memory_struct_lemmas.ma emulator/memory/memory_struct.ma num/bool_lemmas.ma +emulator/opcodes/IP2022_table.ma common/list.ma emulator/opcodes/IP2022_instr_mode.ma emulator/opcodes/IP2022_pseudo.ma emulator/opcodes/byte_or_word.ma +num/oct.ma num/bool.ma +num/word32.ma num/word16.ma emulator/model/IP2022_model.ma emulator/status/status.ma -emulator/opcodes/HCS08_table_tests.ma emulator/opcodes/HCS08_table.ma emulator/opcodes/pseudo.ma +emulator/tests/micro_tests1.ma emulator/multivm/multivm.ma emulator/status/status_lemmas.ma emulator/tests/micro_tests_tools.ma +emulator/read_write/read_write_base.ma common/theory.ma +num/word16.ma num/byte8.ma +emulator/opcodes/Freescale_pseudo_lemmas.ma emulator/opcodes/Freescale_pseudo.ma num/bool_lemmas.ma +emulator/model/model.ma emulator/model/HC05_model.ma emulator/model/HC08_model.ma emulator/model/HCS08_model.ma emulator/model/IP2022_model.ma emulator/model/RS08_model.ma +num/word24_lemmas.ma num/byte8_lemmas.ma num/word24.ma emulator/opcodes/IP2022_table_tests.ma emulator/opcodes/IP2022_table.ma emulator/opcodes/pseudo.ma -emulator/status/IP2022_status.ma emulator/memory/memory_struct.ma num/word16.ma num/word24.ma -emulator/translation/Freescale_translation.ma emulator/translation/translation_base.ma -num/quatern_lemmas.ma num/bool_lemmas.ma num/quatern.ma +common/prod.ma num/bool.ma +common/option.ma num/bool.ma +emulator/tests/medium_tests.ma common/list_utility.ma common/nat_to_num.ma emulator/tests/medium_tests_tools.ma +emulator/translation/IP2022_translation.ma emulator/translation/translation_base.ma +emulator/multivm/multivm_base.ma common/theory.ma emulator/status/status_setter.ma +num/comp_num_lemmas.ma num/bool_lemmas.ma num/comp_num.ma emulator/memory/memory_func.ma common/list.ma common/option.ma emulator/memory/memory_struct.ma num/word32.ma +emulator/model/HC08_model.ma emulator/status/status.ma +emulator/status/status_getter.ma emulator/status/status_setter.ma +common/ascii_lemmas.ma common/ascii.ma num/bool_lemmas.ma +emulator/multivm/Freescale_multivm.ma emulator/multivm/multivm_base.ma emulator/read_write/load_write.ma emulator/read_write/read_write.ma emulator/read_write/IP2022_read_write.ma emulator/read_write/RS08_read_write.ma -emulator/opcodes/Freescale_instr_mode.ma num/word16.ma -num/comp_num_lemmas.ma num/bool_lemmas.ma num/comp_num.ma -emulator/read_write/read_write_base.ma common/theory.ma -emulator/status/RS08_status.ma num/word16.ma +emulator/memory/memory_struct.ma num/byte8.ma num/oct.ma +common/list_utility_lemmas.ma common/list_lemmas.ma common/list_utility.ma +common/nat_to_num.ma common/nat.ma num/word32.ma +emulator/read_write/fetch.ma emulator/memory/memory_abs.ma emulator/status/status_getter.ma emulator/translation/translation.ma +compiler/ast_type.ma common/list_utility.ma +emulator/opcodes/HC05_table.ma common/list.ma emulator/opcodes/Freescale_instr_mode.ma emulator/opcodes/Freescale_pseudo.ma emulator/opcodes/byte_or_word.ma +emulator/status/HC08_status.ma num/word16.ma +common/prod_lemmas.ma common/prod.ma num/bool_lemmas.ma +test_errori.ma +emulator/memory/memory_abs.ma emulator/memory/memory_bits.ma emulator/memory/memory_func.ma emulator/memory/memory_trees.ma +emulator/tests/medium_tests_tools.ma emulator/multivm/multivm.ma +emulator/opcodes/Freescale_pseudo.ma num/bool.ma +emulator/read_write/load_write_base.ma emulator/read_write/read_write.ma +num/word32_lemmas.ma num/word16_lemmas.ma num/word32.ma +emulator/read_write/load_write.ma emulator/read_write/Freescale_load_write.ma emulator/read_write/IP2022_load_write.ma +emulator/opcodes/byte_or_word.ma num/word16.ma common/option_lemmas.ma common/option.ma num/bool_lemmas.ma -common/option.ma num/bool.ma -emulator/opcodes/pseudo_lemmas.ma emulator/opcodes/Freescale_instr_mode_lemmas.ma emulator/opcodes/Freescale_pseudo_lemmas.ma emulator/opcodes/IP2022_instr_mode_lemmas.ma emulator/opcodes/IP2022_pseudo_lemmas.ma emulator/opcodes/pseudo.ma -emulator/multivm/Freescale_multivm.ma emulator/multivm/multivm_base.ma emulator/read_write/fetch.ma emulator/read_write/load_write.ma -num/byte8_lemmas.ma num/byte8.ma num/comp_num_lemmas.ma num/exadecim_lemmas.ma emulator/opcodes/RS08_table.ma common/list.ma emulator/opcodes/Freescale_instr_mode.ma emulator/opcodes/Freescale_pseudo.ma emulator/opcodes/byte_or_word.ma -emulator/model/RS08_model.ma emulator/status/status.ma -num/comp_num.ma num/exadecim.ma -common/sigma.ma common/theory.ma -common/list_lemmas.ma common/list.ma -emulator/status/HC08_status_lemmas.ma emulator/status/HC08_status.ma num/word16_lemmas.ma -emulator/opcodes/HCS08_table.ma common/list.ma emulator/opcodes/Freescale_instr_mode.ma emulator/opcodes/Freescale_pseudo.ma emulator/opcodes/byte_or_word.ma -emulator/read_write/IP2022_load_write.ma emulator/read_write/load_write_base.ma emulator/status/status_getter.ma -emulator/translation/IP2022_translation.ma emulator/translation/translation_base.ma -universe/universe.ma common/list.ma common/nat_lemmas.ma common/prod.ma num/bitrigesim.ma num/bool.ma +common/theory.ma emulator/opcodes/pseudo.ma common/list.ma emulator/opcodes/Freescale_instr_mode.ma emulator/opcodes/Freescale_pseudo.ma emulator/opcodes/IP2022_instr_mode.ma emulator/opcodes/IP2022_pseudo.ma emulator/opcodes/byte_or_word.ma -common/list_utility.ma common/list.ma common/nat_lemmas.ma common/option.ma -emulator/translation/translation.ma emulator/translation/Freescale_translation.ma emulator/translation/IP2022_translation.ma -emulator/read_write/fetch.ma emulator/memory/memory_abs.ma emulator/status/status_getter.ma emulator/translation/translation.ma +emulator/opcodes/Freescale_instr_mode_lemmas.ma emulator/opcodes/Freescale_instr_mode.ma num/bitrigesim_lemmas.ma num/bool_lemmas.ma num/exadecim_lemmas.ma num/oct_lemmas.ma +emulator/status/status_lemmas.ma common/option_lemmas.ma common/prod_lemmas.ma emulator/opcodes/pseudo_lemmas.ma emulator/status/HC05_status_lemmas.ma emulator/status/HC08_status_lemmas.ma emulator/status/IP2022_status_lemmas.ma emulator/status/RS08_status_lemmas.ma emulator/status/status.ma +common/list_lemmas.ma common/list.ma +emulator/opcodes/pseudo_lemmas.ma emulator/opcodes/Freescale_instr_mode_lemmas.ma emulator/opcodes/Freescale_pseudo_lemmas.ma emulator/opcodes/IP2022_instr_mode_lemmas.ma emulator/opcodes/IP2022_pseudo_lemmas.ma emulator/opcodes/pseudo.ma +emulator/opcodes/HCS08_table_tests.ma emulator/opcodes/HCS08_table.ma emulator/opcodes/pseudo.ma emulator/opcodes/IP2022_instr_mode_lemmas.ma emulator/opcodes/IP2022_instr_mode.ma num/bitrigesim_lemmas.ma num/bool_lemmas.ma num/oct_lemmas.ma -num/oct.ma num/bool.ma -common/list.ma common/theory.ma -emulator/opcodes/HC08_table_tests.ma emulator/opcodes/HC08_table.ma emulator/opcodes/pseudo.ma -emulator/opcodes/IP2022_pseudo_lemmas.ma emulator/opcodes/IP2022_pseudo.ma num/bool_lemmas.ma diff --git a/helm/software/matita/contribs/ng_assembly/emulator/tests/medium_tests.ma b/helm/software/matita/contribs/ng_assembly/emulator/tests/medium_tests.ma new file mode 100755 index 000000000..2b85f09dc --- /dev/null +++ b/helm/software/matita/contribs/ng_assembly/emulator/tests/medium_tests.ma @@ -0,0 +1,883 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +(* ********************************************************************** *) +(* Progetto FreeScale *) +(* *) +(* Sviluppato da: Ing. Cosimo Oliboni, oliboni@cs.unibo.it *) +(* Sviluppo: 2008-2010 *) +(* *) +(* ********************************************************************** *) + +include "emulator/tests/medium_tests_tools.ma". +include "common/list_utility.ma". +include "common/nat_to_num.ma". +include "emulator/model/model.ma". + +(* ************************ *) +(* HCS08GB60 String Reverse *) +(* ************************ *) + +(* versione ridotta, in cui non si riazzerano gli elementi di counters *) +ndefinition dTest_HCS08_sReverse_source : word16 → (list byte8) ≝ +λelems:word16.source_to_byte8 HCS08 ( +(* BEFORE: A=0x00 H:X=0x0D4B SP=0x0D4A PC=0x18E0 Z=true *) + +(* static unsigned char dati[3072]={...}; + + void swap(unsigned char *a, unsigned char *b) + { unsigned char tmp=*a; *a=*b; *b=tmp; return; } *) + +(* [0x18C8] allineamento *) (compile HCS08 ? NOP maINH ?) @ + +(* argomenti: HX e [0x0D49-A], passaggio ibrido reg, stack *) +(* [0x18C9] PSHX *) (compile HCS08 ? PSHX maINH ?) @ +(* [0x18CA] PSHH *) (compile HCS08 ? PSHH maINH ?) @ +(* [0x18CB] LDHX 5,SP *) (compile HCS08 ? LDHX (maSP1 〈x0,x5〉) ?) @ +(* [0x18CE] LDA ,X *) (compile HCS08 ? LDA maIX0 ?) @ +(* [0x18CF] LDHX 1,SP *) (compile HCS08 ? LDHX (maSP1 〈x0,x1〉) ?) @ +(* [0x18D2] PSHA *) (compile HCS08 ? PSHA maINH ?) @ +(* [0x18D3] LDA ,X *) (compile HCS08 ? LDA maIX0 ?) @ +(* [0x18D4] LDHX 6,SP *) (compile HCS08 ? LDHX (maSP1 〈x0,x6〉) ?) @ +(* [0x18D7] STA ,X *) (compile HCS08 ? STA maIX0 ?) @ +(* [0x18D8] LDHX 2,SP *) (compile HCS08 ? LDHX (maSP1 〈x0,x2〉) ?) @ +(* [0x18DB] PULA *) (compile HCS08 ? PULA maINH ?) @ +(* [0x18DC] STA ,X *) (compile HCS08 ? STA maIX0 ?) @ +(* [0x18DD] AIS #2 *) (compile HCS08 ? AIS (maIMM1 〈x0,x2〉) ?) @ +(* [0x18DF] RTS *) (compile HCS08 ? RTS maINH ?) @ + +(* void main(void) + { + unsigned int pos=0,limit=0; + + for(limit=3072;pos<(limit/2);pos++) + { swap(&dati[pos],&dati[limit-pos-1]); } *) + +(* [0x18E0] LDHX #elems *) (compile HCS08 ? LDHX (maIMM2 elems) ?) @ +(* [0x18E3] STHX 4,SP *) (compile HCS08 ? STHX (maSP1 〈x0,x4〉) ?) @ +(* [0x18E6] BRA *+52 ; 191A *) (compile HCS08 ? BRA (maIMM1 〈x3,x2〉) ?) @ +(* [0x18E8] TSX *) (compile HCS08 ? TSX maINH ?) @ +(* [0x18E9] LDA 2,X *) (compile HCS08 ? LDA (maIX1 〈x0,x2〉) ?) @ +(* [0x18EB] ADD #0x00 *) (compile HCS08 ? ADD (maIMM1 〈x0,x0〉) ?) @ +(* [0x18ED] PSHA *) (compile HCS08 ? PSHA maINH ?) @ +(* [0x18EE] LDA 1,X *) (compile HCS08 ? LDA (maIX1 〈x0,x1〉) ?) @ +(* [0x18F0] ADC #0x01 *) (compile HCS08 ? ADC (maIMM1 〈x0,x1〉) ?) @ +(* [0x18F2] PSHA *) (compile HCS08 ? PSHA maINH ?) @ +(* [0x18F3] LDA 4,X *) (compile HCS08 ? LDA (maIX1 〈x0,x4〉) ?) @ +(* [0x18F5] SUB 2,X *) (compile HCS08 ? SUB (maIX1 〈x0,x2〉) ?) @ +(* [0x18F7] STA ,X *) (compile HCS08 ? STA maIX0 ?) @ +(* [0x18F8] LDA 3,X *) (compile HCS08 ? LDA (maIX1 〈x0,x3〉) ?) @ +(* [0x18FA] SBC 1,X *) (compile HCS08 ? SBC (maIX1 〈x0,x1〉) ?) @ +(* [0x18FC] PSHA *) (compile HCS08 ? PSHA maINH ?) @ +(* [0x18FD] LDX ,X *) (compile HCS08 ? LDX maIX0 ?) @ +(* [0x18FE] PULH *) (compile HCS08 ? PULH maINH ?) @ +(* [0x18FF] AIX #-1 *) (compile HCS08 ? AIX (maIMM1 〈xF,xF〉) ?) @ +(* [0x1901] TXA *) (compile HCS08 ? TXA maINH ?) @ +(* [0x1902] ADD #0x00 *) (compile HCS08 ? ADD (maIMM1 〈x0,x0〉) ?) @ +(* [0x1904] PSHH *) (compile HCS08 ? PSHH maINH ?) @ +(* [0x1905] TSX *) (compile HCS08 ? TSX maINH ?) @ +(* [0x1906] STA 3,X *) (compile HCS08 ? STA (maIX1 〈x0,x3〉) ?) @ +(* [0x1908] PULA *) (compile HCS08 ? PULA maINH ?) @ +(* [0x1909] ADC #0x01 *) (compile HCS08 ? ADC (maIMM1 〈x0,x1〉) ?) @ +(* [0x190B] LDX 3,X *) (compile HCS08 ? LDX (maIX1 〈x0,x3〉) ?) @ +(* [0x190D] PSHA *) (compile HCS08 ? PSHA maINH ?) @ +(* [0x190E] PULH *) (compile HCS08 ? PULH maINH ?) @ +(* [0x190F] BSR *-70 ; 18C9 *) (compile HCS08 ? BSR (maIMM1 〈xB,x8〉) ?) @ +(* [0x1911] AIS #2 *) (compile HCS08 ? AIS (maIMM1 〈x0,x2〉) ?) @ +(* [0x1913] TSX *) (compile HCS08 ? TSX maINH ?) @ +(* [0x1914] INC 2,X *) (compile HCS08 ? INC (maIX1 〈x0,x2〉) ?) @ +(* [0x1916] BNE *+4 ; 191A *) (compile HCS08 ? BNE (maIMM1 〈x0,x2〉) ?) @ +(* [0x1918] INC 1,X *) (compile HCS08 ? INC (maIX1 〈x0,x1〉) ?) @ +(* [0x191A] TSX *) (compile HCS08 ? TSX maINH ?) @ +(* [0x191B] LDA 3,X *) (compile HCS08 ? LDA (maIX1 〈x0,x3〉) ?) @ +(* [0x191D] PSHA *) (compile HCS08 ? PSHA maINH ?) @ +(* [0x191E] PULH *) (compile HCS08 ? PULH maINH ?) @ +(* [0x191F] LSRA *) (compile HCS08 ? LSR maINHA ?) @ +(* [0x1920] TSX *) (compile HCS08 ? TSX maINH ?) @ +(* [0x1921] LDX 4,X *) (compile HCS08 ? LDX (maIX1 〈x0,x4〉) ?) @ +(* [0x1923] RORX *) (compile HCS08 ? ROR maINHX ?) @ +(* [0x1924] PSHA *) (compile HCS08 ? PSHA maINH ?) @ +(* [0x1925] PULH *) (compile HCS08 ? PULH maINH ?) @ +(* [0x1926] CPHX 2,SP *) (compile HCS08 ? CPHX (maSP1 〈x0,x2〉) ?) @ +(* [0x1929] BHI *-65 ; 18E8 *) (compile HCS08 ? BHI (maIMM1 〈xB,xD〉) ?) + +(* [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 *) + ). napply I. nqed. + +(* creazione del processore+caricamento+impostazione registri *) +ndefinition dTest_HCS08_sReverse_status ≝ +λt:memory_impl. +λ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<-0x0D4A *) + (setweak_indX_16_reg HCS08 t (* H:X<-HX_op *) + (set_pc_reg HCS08 t (* PC<-0x18E0 *) + (start_of_model HCS08 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_sReverse_source elems) (extu_w32 dTest_HCS08_prog)) + data (extu_w32 dTest_HCS08_RAM)) + (build_memory_type_of_model HCS08 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 *) + (mk_word16 (mk_byte8 x1 x8) (mk_byte8 xE x0))) + HX_op) + (mk_word16 (mk_byte8 x0 xD) (mk_byte8 x4 xA))) + true) + A_op. + +(* parametrizzazione dell'enunciato del teorema *) +(* primo sbozzo: confronto esecuzione con hexdump... *) +nlemma dTest_HCS08_sReverse_dump_aux ≝ +λt:memory_impl.λstring:list byte8. + (* 1) la stringa deve avere una lunghezza ∈ [0,3072] *) + (byte8_bounded_strlen string 〈〈x0,xC〉:〈x0,x0〉〉) ∧ + (* 2) la stringa deve avere lunghezza pari *) + ((and_b8 (cnL ? (byte8_strlen string)) 〈x0,x1〉) = 〈x0,x0〉) ∧ + (* 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,x0〉 〈〈x0,xD〉:〈x4,xB〉〉 (byte8_strlen string) string)) + (* tempo di esecuzione 42+79*n+5*(n>>9) *) + (nat42 + (nat79 * (len_list ? string))+(nat5 * ((len_list ? string) / nat512))) with + [ TickERR s _ ⇒ None ? + (* azzeramento tutta RAM tranne dati *) + | TickSUSP s _ ⇒ None ? + | TickOK s ⇒ Some ? (byte8_hexdump t (mem_desc HCS08 t s) (extu_w32 dTest_HCS08_RAM) (len_list ? string)) + ] = + Some ? (reverse_list ? string)). + +(* confronto esecuzione con hexdump... *) +(* +lemma dTest_HCS08_sReverse_dump : + dTest_HCS08_sReverse_dump_aux MEM_TREE dTest_random_32. + unfold dTest_HCS08_sReverse_dump_aux; + split; + [ split; [ normalize in ⊢ (%); autobatch ] reflexivity ] + reflexivity. +qed. +*) + +(* parametrizzazione dell'enunciato del teorema *) +(* dimostrazione senza svolgimento degli stati *) +nlemma dTest_HCS08_sReverse_aux ≝ +λt:memory_impl.λstring:list byte8. + (* 1) la stringa deve avere una lunghezza ∈ [0,3072] *) + (byte8_bounded_strlen string 〈〈x0,xC〉:〈x0,x0〉〉) ∧ + (* 2) la stringa deve avere lunghezza pari *) + ((and_b8 (cnL ? (byte8_strlen string)) 〈x0,x1〉) = 〈x0,x0〉) ∧ + (* 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,x0〉 〈〈x0,xD〉:〈x4,xB〉〉 (byte8_strlen string) string)) + (* tempo di esecuzione 42+79*n+5*(n>>9) *) + (nat42 + (nat79 * (len_list ? string))+(nat5 * ((len_list ? string) / nat512))) with + [ TickERR s _ ⇒ None ? + (* azzeramento tutta RAM tranne dati *) + | TickSUSP s _ ⇒ None ? + | TickOK s ⇒ Some ? (set_mem_desc HCS08 t s (load_from_source_at t (mem_desc HCS08 t s) dTest_zeros (extu_w32 〈〈x0,xD〉:〈x0,x0〉〉))) + ] = + Some ? (set_pc_reg HCS08 t + (dTest_HCS08_sReverse_status t (snd … (shr_b8 (cnH ? (byte8_strlen string)))) (snd … (shr_w16 (byte8_strlen string))) (byte8_strlen string) (reverse_list ? string)) + (mk_word16 (mk_byte8 x1 x9) (mk_byte8 x2 xB)))). + +(* +lemma dTest_HCS08_sReverse : + dTest_HCS08_sReverse_aux MEM_TREE dTest_random_32. + unfold dTest_HCS08_sReverse_aux; + split; + [ split; [ normalize in ⊢ (%); autobatch ] reflexivity ] + + rewrite > (breakpoint HCS08 MEM_TREE (TickOK ? (dTest_HCS08_sReverse_status MEM_TREE 〈〈x0,xD〉:〈x4,xB〉〉 (byte8_strlen dTest_random_32) dTest_random_32)) 3 (39+79*byte8_strlen dTest_random_32+5*(byte8_strlen dTest_random_32/512))) in ⊢ (? ? match % in tick_result return ? with [TickERR⇒?|TickSUSP⇒?|TickOK⇒?] ?); + letin status0 ≝ (dTest_HCS08_sReverse_status MEM_TREE 〈〈x0,xD〉:〈x4,xB〉〉 (byte8_strlen dTest_random_32) dTest_random_32); + change in ⊢ (? ? match ? ? ? (? ? ? % ?) ? in tick_result return ? with [TickERR⇒?|TickSUSP⇒?|TickOK⇒?] ?) with + (TickOK ? status0); + rewrite > (execute_HCS08_LDHX_maIMM2 MEM_TREE status0 〈x0,x0〉 〈x2,x0〉) in ⊢ (? ? match ? ? ? % ? in tick_result return ? with [TickERR⇒?|TickSUSP⇒?|TickOK⇒?] ?); + [ 2,3,4,5: reflexivity; ] + + letin status1 ≝ (set_pc_reg HCS08 MEM_TREE (setweak_v_flag HCS08 MEM_TREE (setweak_n_flag HCS08 MEM_TREE (set_z_flag HCS08 MEM_TREE (set_alu HCS08 MEM_TREE (dTest_HCS08_sReverse_status MEM_TREE 〈〈x0,xD〉:〈x4,xB〉〉 (byte8_strlen dTest_random_32) dTest_random_32) (set_indX_16_reg_HC08 (alu HCS08 MEM_TREE (dTest_HCS08_sReverse_status MEM_TREE 〈〈x0,xD〉:〈x4,xB〉〉 (byte8_strlen dTest_random_32) dTest_random_32)) 〈〈x0,x0〉:〈x2,x0〉〉)) (eq_w16 〈〈x0,x0〉:〈x2,x0〉〉 〈〈x0,x0〉:〈x0,x0〉〉)) (MSB_w16 〈〈x0,x0〉:〈x2,x0〉〉)) false) (filtered_plus_w16 HCS08 MEM_TREE (dTest_HCS08_sReverse_status MEM_TREE 〈〈x0,xD〉:〈x4,xB〉〉 (byte8_strlen dTest_random_32) dTest_random_32) (get_pc_reg HCS08 MEM_TREE (dTest_HCS08_sReverse_status MEM_TREE 〈〈x0,xD〉:〈x4,xB〉〉 (byte8_strlen dTest_random_32) dTest_random_32)) 3)); + change in ⊢ (? ? match ? ? ? % ? in tick_result return ? with [TickERR⇒?|TickSUSP⇒?|TickOK⇒?] ?) with (TickOK ? status1); + + rewrite > (breakpoint HCS08 MEM_TREE (TickOK ? status1) 5 (34+79*byte8_strlen dTest_random_32+5*(byte8_strlen dTest_random_32/512))) in ⊢ (? ? match % in tick_result return ? with [TickERR⇒?|TickSUSP⇒?|TickOK⇒?] ?); + change in ⊢ (? ? match ? ? ? (? ? ? % ?) ? in tick_result return ? with [TickERR⇒?|TickSUSP⇒?|TickOK⇒?] ?) with (TickOK ? status1); + rewrite > (execute_HCS08_STHX_maSP1 status1 〈x0,x4〉) + in ⊢ (? ? match ? ? ? % ? in tick_result return ? with [TickERR⇒?|TickSUSP⇒?|TickOK⇒?] ?); + [ 2,3,4,5,6,7: reflexivity; ] + + elim daemon. + +qed. +*) + +ndefinition sReverseCalc ≝ +λstring:list byte8. + match execute HCS08 MEM_TREE + (TickOK ? (dTest_HCS08_sReverse_status MEM_TREE 〈x0,x0〉 〈〈x0,xD〉:〈x4,xB〉〉 (byte8_strlen string) string)) + (nat42 + (nat79 * (len_list ? string))+(nat5 * ((len_list ? string) / nat512))) with + [ TickERR s _ ⇒ None ? + | TickSUSP s _ ⇒ None ? + | TickOK s ⇒ Some ? (set_mem_desc HCS08 MEM_TREE s (load_from_source_at MEM_TREE (mem_desc HCS08 MEM_TREE s) dTest_zeros (extu_w32 〈〈x0,xD〉:〈x0,x0〉〉))) + ]. + +ndefinition sReverseNoCalc ≝ +λstring:list byte8. + Some ? (set_pc_reg HCS08 MEM_TREE + (dTest_HCS08_sReverse_status MEM_TREE (snd … (shr_b8 (cnH ? (byte8_strlen string)))) + (snd … (shr_w16 (byte8_strlen string))) + (byte8_strlen string) (reverse_list ? string)) + (mk_word16 (mk_byte8 x1 x9) (mk_byte8 x2 xB))). + +ndefinition sReverseCalc32 ≝ sReverseCalc dTest_random_32. +ndefinition sReverseCalc64 ≝ sReverseCalc dTest_random_64. +ndefinition sReverseCalc128 ≝ sReverseCalc dTest_random_128. +ndefinition sReverseCalc256 ≝ sReverseCalc dTest_random_256. +ndefinition sReverseCalc512 ≝ sReverseCalc dTest_random_512. +ndefinition sReverseCalc1024 ≝ sReverseCalc dTest_random_1024. +ndefinition sReverseCalc2048 ≝ sReverseCalc dTest_random_2048. +ndefinition sReverseCalc3072 ≝ sReverseCalc dTest_random_3072. + +ndefinition sReverseNoCalc32 ≝ sReverseNoCalc dTest_random_32. +ndefinition sReverseNoCalc64 ≝ sReverseNoCalc dTest_random_64. +ndefinition sReverseNoCalc128 ≝ sReverseNoCalc dTest_random_128. +ndefinition sReverseNoCalc256 ≝ sReverseNoCalc dTest_random_256. +ndefinition sReverseNoCalc512 ≝ sReverseNoCalc dTest_random_512. +ndefinition sReverseNoCalc1024 ≝ sReverseNoCalc dTest_random_1024. +ndefinition sReverseNoCalc2048 ≝ sReverseNoCalc dTest_random_2048. +ndefinition sReverseNoCalc3072 ≝ sReverseNoCalc dTest_random_3072. + +(* *********************** *) +(* HCS08GB60 Counting Sort *) +(* *********************** *) + +(* versione ridotta, in cui non si riazzerano gli elementi di counters *) +ndefinition dTest_HCS08_cSort_source : word16 → (list byte8) ≝ +λelems:word16.source_to_byte8 HCS08 ( +(* BEFORE: A=0x00 H:X=0x0F4C SP=0x0F4B PC=0x18C8 Z=true *) + +(* /* IPOTESI: INIT VARIABILI+ARRAY GIA' ESEGUITO */ + static unsigned int counters[256]={ campitura di 0 }; + static unsigned char dati[3072]={ dati random }; + + void CountingSort(void) + { + unsigned int index=0,position=0; *) + +(* /* TESI: CODICE DA ESEGUIRE + + /* calcolo del # ripetizioni degli elementi byte */ + for(;index<3072;index++) + { counters[dati[index]]++; } *) + +(* [0x18C8] BRA *+31;18E7 *) (compile HCS08 ? BRA (maIMM1 〈x1,xD〉) ?) @ +(* [0x18CA] LDHX 1,SP *) (compile HCS08 ? LDHX (maSP1 〈x0,x1〉) ?) @ +(* [0x18CD] LDA 256,X *) (compile HCS08 ? LDA (maIX2 〈〈x0,x1〉:〈x0,x0〉〉) ?) @ +(* [0x18D0] LSLA *) (compile HCS08 ? ASL maINHA ?) @ +(* [0x18D1] CLRX *) (compile HCS08 ? CLR maINHX ?) @ +(* [0x18D2] ROLX *) (compile HCS08 ? ROL maINHX ?) @ +(* [0x18D3] ADD #0x00 *) (compile HCS08 ? ADD (maIMM1 〈x0,x0〉) ?) @ +(* [0x18D5] PSHA *) (compile HCS08 ? PSHA maINH ?) @ +(* [0x18D6] TXA *) (compile HCS08 ? TXA maINH ?) @ +(* [0x18D7] ADC #0x0D *) (compile HCS08 ? ADC (maIMM1 〈x0,xD〉) ?) @ +(* [0x18D9] PSHA *) (compile HCS08 ? PSHA maINH ?) @ +(* [0x18DA] PULH *) (compile HCS08 ? PULH maINH ?) @ +(* [0x18DB] PULX *) (compile HCS08 ? PULX maINH ?) @ +(* [0x18DC] INC 1,X *) (compile HCS08 ? INC (maIX1 〈x0,x1〉) ?) @ +(* [0x18DE] BNE *+3 *) (compile HCS08 ? BNE (maIMM1 〈x0,x1〉) ?) @ +(* [0x18E0] INC ,X *) (compile HCS08 ? INC maIX0 ?) @ +(* [0x18E1] TSX *) (compile HCS08 ? TSX maINH ?) @ +(* [0x18E2] INC 1,X *) (compile HCS08 ? INC (maIX1 〈x0,x1〉) ?) @ +(* [0x18E4] BNE *+3 *) (compile HCS08 ? BNE (maIMM1 〈x0,x1〉) ?) @ +(* [0x18E6] INC ,X *) (compile HCS08 ? INC maIX0 ?) @ +(* [0x18E7] LDHX 1,SP *) (compile HCS08 ? LDHX (maSP1 〈x0,x1〉) ?) @ +(* [0x18EA] CPHX #elems *) (compile HCS08 ? CPHX (maIMM2 elems) ?) @ (* dimensione dei dati al massimo 0x0C00 *) +(* [0x18ED] BCS *-35;18CA *) (compile HCS08 ? BCS (maIMM1 〈xD,xB〉) ?) @ + +(* /* sovrascrittura di dati per produrre la versione ordinata */ + for(index=0;index<256;index++) + { + while(counters[index]--) + { dati[position++]=index; } + } *) + +(* [0x18EF] TSX *) (compile HCS08 ? TSX maINH ?) @ +(* [0x18F0] CLR 1,X *) (compile HCS08 ? CLR (maIX1 〈x0,x1〉) ?) @ +(* [0x18F2] CLR ,X *) (compile HCS08 ? CLR maIX0 ?) @ +(* [0x18F3] BRA *+16 *) (compile HCS08 ? BRA (maIMM1 〈x0,xE〉) ?) @ +(* [0x18F5] TSX *) (compile HCS08 ? TSX maINH ?) @ +(* [0x18F6] LDA 1,X *) (compile HCS08 ? LDA (maIX1 〈x0,x1〉) ?) @ +(* [0x18F8] LDHX 3,SP *) (compile HCS08 ? LDHX (maSP1 〈x0,x3〉) ?) @ +(* [0x18FB] STA 256,X *) (compile HCS08 ? STA (maIX2 〈〈x0,x1〉:〈x0,x0〉〉) ?) @ +(* [0x18FE] AIX #1 *) (compile HCS08 ? AIX (maIMM1 〈x0,x1〉) ?) @ +(* [0x1900] STHX 3,SP *) (compile HCS08 ? STHX (maSP1 〈x0,x3〉) ?) @ +(* [0x1903] TSX *) (compile HCS08 ? TSX maINH ?) @ +(* [0x1904] LDX 1,X *) (compile HCS08 ? LDX (maIX1 〈x0,x1〉) ?) @ +(* [0x1906] LSLX *) (compile HCS08 ? ASL maINHX ?) @ +(* [0x1907] LDA 1,SP *) (compile HCS08 ? LDA (maSP1 〈x0,x1〉) ?) @ +(* [0x190A] ROLA *) (compile HCS08 ? ROL maINHA ?) @ +(* [0x190B] PSHA *) (compile HCS08 ? PSHA maINH ?) @ +(* [0x190C] PULH *) (compile HCS08 ? PULH maINH ?) @ +(* [0x190D] PSHX *) (compile HCS08 ? PSHX maINH ?) @ +(* [0x190E] LDHX 3328,X *) (compile HCS08 ? LDHX (maIX2 〈〈x0,xD〉:〈x0,x0〉〉) ?) @ +(* [0x1912] PSHX *) (compile HCS08 ? PSHX maINH ?) @ +(* [0x1913] PSHH *) (compile HCS08 ? PSHH maINH ?) @ +(* [0x1914] AIX #-1 *) (compile HCS08 ? AIX (maIMM1 〈xF,xF〉) ?) @ +(* [0x1916] PSHH *) (compile HCS08 ? PSHH maINH ?) @ +(* [0x1917] PSHA *) (compile HCS08 ? PSHA maINH ?) @ +(* [0x1918] PULH *) (compile HCS08 ? PULH maINH ?) @ +(* [0x1919] PSHX *) (compile HCS08 ? PSHX maINH ?) @ +(* [0x191A] LDX 5,SP *) (compile HCS08 ? LDX (maSP1 〈x0,x5〉) ?) @ +(* [0x191D] PULA *) (compile HCS08 ? PULA maINH ?) @ +(* [0x191E] STA 3329,X *) (compile HCS08 ? STA (maIX2 〈〈x0,xD〉:〈x0,x1〉〉) ?) @ +(* [0x1921] PULA *) (compile HCS08 ? PULA maINH ?) @ +(* [0x1922] STA 3328,X *) (compile HCS08 ? STA (maIX2 〈〈x0,xD〉:〈x0,x0〉〉) ?) @ +(* [0x1925] PULH *) (compile HCS08 ? PULH maINH ?) @ +(* [0x1926] PULX *) (compile HCS08 ? PULX maINH ?) @ +(* [0x1927] CPHX #0x0000 *) (compile HCS08 ? CPHX (maIMM2 〈〈x0,x0〉:〈x0,x0〉〉) ?) @ +(* [0x192A] PULH *) (compile HCS08 ? PULH maINH ?) @ +(* [0x192B] BNE *-54 *) (compile HCS08 ? BNE (maIMM1 〈xC,x8〉) ?) @ +(* [0x192D] TSX *) (compile HCS08 ? TSX maINH ?) @ +(* [0x192E] INC 1,X *) (compile HCS08 ? INC (maIX1 〈x0,x1〉) ?) @ +(* [0x1930] BNE *+3 *) (compile HCS08 ? BNE (maIMM1 〈x0,x1〉) ?) @ +(* [0x1932] INC ,X *) (compile HCS08 ? INC maIX0 ?) @ +(* [0x1933] LDHX 1,SP *) (compile HCS08 ? LDHX (maSP1 〈x0,x1〉) ?) @ +(* [0x1936] CPHX #0x0100 *) (compile HCS08 ? CPHX (maIMM2 〈〈x0,x1〉:〈x0,x0〉〉) ?) @ +(* [0x1939] BNE *-54 *) (compile HCS08 ? BNE (maIMM1 〈xC,x8〉) ?) @ +(* [0x193B] STOP *) (compile HCS08 ? STOP maINH ?) + +(* [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 *) + ). napply I. nqed. + +(* creazione del processore+caricamento+impostazione registri *) +ndefinition dTest_HCS08_cSort_status ≝ +λt:memory_impl. +λI_op:bool. +λA_op:byte8. +λHX_op: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<-0x0F4B *) + (setweak_indX_16_reg HCS08 t (* H:X<-HX_op *) + (set_pc_reg HCS08 t (* PC<-dTest_HCS08_prog *) + (start_of_model HCS08 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) (extu_w32 dTest_HCS08_prog)) + data (extu_w32 dTest_HCS08_RAM)) + (build_memory_type_of_model HCS08 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 *) +nlemma dTest_HCS08_cSort_aux ≝ +λt:memory_impl.λstring:list byte8. + (* 1) la stringa deve avere una lunghezza ∈ [0,3072] *) + (byte8_bounded_strlen string 〈〈x0,xC〉:〈x0,x0〉〉) ∧ + (* 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 true 〈x0,x0〉 〈〈x0,xF〉:〈x4,xC〉〉 (byte8_strlen string) string)) + (* tempo di esecuzione 25700+150*n *) + (((nat256 + nat1) * nat100)+((nat50 * nat3) * (len_list ? string))) with + [ TickERR s _ ⇒ None ? + (* azzeramento tutta RAM tranne dati *) + | TickSUSP s _ ⇒ Some ? (set_mem_desc HCS08 t s (load_from_source_at t (mem_desc HCS08 t s) dTest_zeros (extu_w32 〈〈x0,xD〉:〈x0,x0〉〉))) + | TickOK s ⇒ None ? + ] = + Some ? (set_pc_reg HCS08 t + (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 *) +(* +lemma dTest_HCS08_cSort : + dTest_HCS08_cSort_aux MEM_TREE dTest_random_32. + unfold dTest_HCS08_cSort_aux; + split; + [ normalize in ⊢ (%); autobatch ] + reflexivity. +qed. +*) + +ndefinition cSortCalc ≝ +λstring:list byte8. + match execute HCS08 MEM_TREE + (TickOK ? (dTest_HCS08_cSort_status MEM_TREE true 〈x0,x0〉 〈〈x0,xF〉:〈x4,xC〉〉 (byte8_strlen string) string)) + (((nat256 + nat1) * nat100)+((nat50 * nat3) * (len_list ? string))) with + [ TickERR s _ ⇒ None ? + | TickSUSP s _ ⇒ Some ? (set_mem_desc HCS08 MEM_TREE s (load_from_source_at MEM_TREE (mem_desc HCS08 MEM_TREE s) dTest_zeros (extu_w32 〈〈x0,xD〉:〈x0,x0〉〉))) + | TickOK s ⇒ None ? + ]. + +ndefinition cSortNoCalc ≝ +λstring:list byte8. + Some ? (set_pc_reg HCS08 MEM_TREE + (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))). + +ndefinition cSortCalc32 ≝ cSortCalc dTest_random_32. +ndefinition cSortCalc64 ≝ cSortCalc dTest_random_64. +ndefinition cSortCalc128 ≝ cSortCalc dTest_random_128. +ndefinition cSortCalc256 ≝ cSortCalc dTest_random_256. +ndefinition cSortCalc512 ≝ cSortCalc dTest_random_512. +ndefinition cSortCalc1024 ≝ cSortCalc dTest_random_1024. +ndefinition cSortCalc2048 ≝ cSortCalc dTest_random_2048. +ndefinition cSortCalc3072 ≝ cSortCalc dTest_random_3072. + +ndefinition cSortNoCalc32 ≝ cSortNoCalc dTest_random_32. +ndefinition cSortNoCalc64 ≝ cSortNoCalc dTest_random_64. +ndefinition cSortNoCalc128 ≝ cSortNoCalc dTest_random_128. +ndefinition cSortNoCalc256 ≝ cSortNoCalc dTest_random_256. +ndefinition cSortNoCalc512 ≝ cSortNoCalc dTest_random_512. +ndefinition cSortNoCalc1024 ≝ cSortNoCalc dTest_random_1024. +ndefinition cSortNoCalc2048 ≝ cSortNoCalc dTest_random_2048. +ndefinition cSortNoCalc3072 ≝ cSortNoCalc dTest_random_3072. + +(* ********************** *) +(* HCS08GB60 numeri aurei *) +(* ********************** *) + +(* versione ridotta, in cui non si riazzerano gli elementi di counters *) +ndefinition dTest_HCS08_gNum_source : word16 → (list byte8) ≝ +λelems:word16.source_to_byte8 HCS08 ( +(* BEFORE: A=0x00 HX=0x1A00 PC=0x18BE SP=0x016F Z=1 (I=1) *) + +(* +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 HCS08 ? AIS (maIMM1 〈xF,x6〉) ?) @ +(* [0x18C0] TSX *) (compile HCS08 ? TSX maINH ?) @ +(* [0x18C1] CLR 9,x *) (compile HCS08 ? CLR (maIX1 〈x0,x9〉) ?) @ +(* [0x18C3] CLR 8,X *) (compile HCS08 ? CLR (maIX1 〈x0,x8〉) ?) @ +(* [0x18C5] CLR 1,X *) (compile HCS08 ? CLR (maIX1 〈x0,x1〉) ?) @ +(* [0x18C7] CLR ,X *) (compile HCS08 ? CLR maIX0 ?) @ +(* [0x18C8] CLR 3,X *) (compile HCS08 ? CLR (maIX1 〈x0,x3〉) ?) @ +(* [0x18CA] CLR 2,X *) (compile HCS08 ? CLR (maIX1 〈x0,x2〉) ?) @ +(* [0x18CC] JSR 0x1951 *) (compile HCS08 ? JSR (maIMM2 〈〈x1,x9〉:〈x5,x1〉〉) ?) @ + +(* +for(tested_num=1;tested_num<2;tested_num++) + { +*) + +(* [0x18CF] STHX 1,SP *) (compile HCS08 ? STHX (maSP1 〈x0,x1〉) ?) @ +(* [0x18D2] BRA *+116 ; 0x1946 *) (compile HCS08 ? BRA (maIMM1 〈x7,x2〉) ?) @ +(* [0x18D4] BSR *+125 ; 0x1951 *) (compile HCS08 ? BSR (maIMM1 〈x7,xB〉) ?) @ +(* [0x18D6] STHX 3,SP *) (compile HCS08 ? STHX (maSP1 〈x0,x3〉) ?) @ + +(* + for(acc=0,divisor=1;divisor1951 !FINE! *) (compile HCS08 ? STOP maINH ?) @ +(* [0x1951] CLRX *) (compile HCS08 ? CLR maINHX ?) @ +(* [0x1952] CLRH *) (compile HCS08 ? CLR maINHH ?) @ +(* [0x1953] STHX 9,SP *) (compile HCS08 ? STHX (maSP1 〈x0,x9〉) ?) @ +(* [0x1956] CLRH *) (compile HCS08 ? CLR maINHH ?) @ +(* [0x1957] STHX 7,SP *) (compile HCS08 ? STHX (maSP1 〈x0,x7〉) ?) @ +(* [0x195A] INCX *) (compile HCS08 ? INC maINHX ?) @ +(* [0x195B] RTS *) (compile HCS08 ? RTS maINH ?) @ + +(* +static void _PUSH_ARGS_L(void) { ... } +*) + +(* [0x195C] LDA 3,X *) (compile HCS08 ? LDA (maIX1 〈x0,x3〉) ?) @ +(* [0x195E] PSHA *) (compile HCS08 ? PSHA maINH ?) @ +(* [0x195F] LDA 2,X *) (compile HCS08 ? LDA (maIX1 〈x0,x2〉) ?) @ +(* [0x1961] PSHA *) (compile HCS08 ? PSHA maINH ?) @ +(* [0x1962] LDHX ,X *) (compile HCS08 ? LDHX maIX0 ?) @ +(* [0x1964] PSHX *) (compile HCS08 ? PSHX maINH ?) @ +(* [0x1965] PSHH *) (compile HCS08 ? PSHH maINH ?) @ +(* [0x1966] LDHX 7,SP *) (compile HCS08 ? LDHX (maSP1 〈x0,x7〉) ?) @ +(* [0x1969] LDA 3,X *) (compile HCS08 ? LDA (maIX1 〈x0,x3〉) ?) @ +(* [0x196B] STA 17,SP *) (compile HCS08 ? STA (maSP1 〈x1,x1〉) ?) @ +(* [0x196E] LDA 2,X *) (compile HCS08 ? LDA (maIX1 〈x0,x2〉) ?) @ +(* [0x1970] STA 16,SP *) (compile HCS08 ? STA (maSP1 〈x1,x0〉) ?) @ +(* [0x1973] LDHX ,X *) (compile HCS08 ? LDHX maIX0 ?) @ +(* [0x1975] STHX 14,SP *) (compile HCS08 ? STHX (maSP1 〈x0,xE〉) ?) @ +(* [0x1978] LDHX 5,SP *) (compile HCS08 ? LDHX (maSP1 〈x0,x5〉) ?) @ +(* [0x197B] JMP ,X *) (compile HCS08 ? JMP maINHX0ADD ?) @ + +(* +static void _ENTER_BINARY_L(void) { ... } +*) + +(* [0x197C] PSHA *) (compile HCS08 ? PSHA maINH ?) @ +(* [0x197D] PSHX *) (compile HCS08 ? PSHX maINH ?) @ +(* [0x197E] PSHH *) (compile HCS08 ? PSHH maINH ?) @ +(* [0x197F] PSHX *) (compile HCS08 ? PSHX maINH ?) @ +(* [0x1980] PSHH *) (compile HCS08 ? PSHH maINH ?) @ +(* [0x1981] LDHX 6,SP *) (compile HCS08 ? LDHX (maSP1 〈x0,x6〉) ?) @ +(* [0x1984] PSHX *) (compile HCS08 ? PSHX maINH ?) @ +(* [0x1985] PSHH *) (compile HCS08 ? PSHH maINH ?) @ +(* [0x1986] LDHX 10,SP *) (compile HCS08 ? LDHX (maSP1 〈x0,xA〉) ?) @ +(* [0x1989] STHX 8,SP *) (compile HCS08 ? STHX (maSP1 〈x0,x8〉) ?) @ +(* [0x198C] LDHX 12,SP *) (compile HCS08 ? LDHX (maSP1 〈x0,xC〉) ?) @ +(* [0x198F] JMP 0x195C *) (compile HCS08 ? JMP (maIMM2 〈〈x1,x9〉:〈x5,xC〉〉) ?) @ + +(* +static void _IDIVMOD (char dummy_sgn, int j, int dummy, int i, ...) { ... } +*) + +(* [0x1992] TST 4,SP *) (compile HCS08 ? TST (maSP1 〈x0,x4〉) ?) @ +(* [0x1995] BNE *+28 ; 0x19B1 *) (compile HCS08 ? BNE (maIMM1 〈x1,xA〉) ?) @ +(* [0x1997] TSX *) (compile HCS08 ? TSX maINH ?) @ +(* [0x1998] LDA 7,X *) (compile HCS08 ? LDA (maIX1 〈x0,x7〉) ?) @ +(* [0x199A] LDX 4,X *) (compile HCS08 ? LDX (maIX1 〈x0,x4〉) ?) @ +(* [0x199C] CLRH *) (compile HCS08 ? CLR maINHH ?) @ +(* [0x199D] DIV *) (compile HCS08 ? DIV maINH ?) @ +(* [0x199E] STA 4,SP *) (compile HCS08 ? STA (maSP1 〈x0,x4〉) ?) @ +(* [0x19A1] LDA 9,SP *) (compile HCS08 ? LDA (maSP1 〈x0,x9〉) ?) @ +(* [0x19A4] DIV *) (compile HCS08 ? DIV maINH ?) @ +(* [0x19A5] STA 5,SP *) (compile HCS08 ? STA (maSP1 〈x0,x5〉) ?) @ +(* [0x19A8] CLR 8,SP *) (compile HCS08 ? CLR (maSP1 〈x0,x8〉) ?) @ +(* [0x19AB] PSHH *) (compile HCS08 ? PSHH maINH ?) @ +(* [0x19AC] PULA *) (compile HCS08 ? PULA maINH ?) @ +(* [0x19AD] STA 9,SP *) (compile HCS08 ? STA (maSP1 〈x0,x9〉) ?) @ +(* [0x19B0] RTS *) (compile HCS08 ? RTS maINH ?) @ +(* [0x19B1] CLRA *) (compile HCS08 ? CLR maINHA ?) @ +(* [0x19B2] PSHA *) (compile HCS08 ? PSHA maINH ?) @ +(* [0x19B3] LDX #0x08 *) (compile HCS08 ? LDX (maIMM1 〈x0,x8〉) ?) @ +(* [0x19B5] CLC *) (compile HCS08 ? CLC maINH ?) @ +(* [0x19B6] ROL 10,SP *) (compile HCS08 ? ROL (maSP1 〈x0,xA〉) ?) @ +(* [0x19B9] ROL 9,SP *) (compile HCS08 ? ROL (maSP1 〈x0,x9〉) ?) @ +(* [0x19BC] ROL 1,SP *) (compile HCS08 ? ROL (maSP1 〈x0,x1〉) ?) @ +(* [0x19BF] LDA 5,SP *) (compile HCS08 ? LDA (maSP1 〈x0,x5〉) ?) @ +(* [0x19C2] CMP 1,SP *) (compile HCS08 ? CMP (maSP1 〈x0,x1〉) ?) @ +(* [0x19C5] BHI *+31 ; 0x19E4 *) (compile HCS08 ? BHI (maIMM1 〈x1,xD〉) ?) @ +(* [0x19C7] BNE *+10 ; 0x19D1 *) (compile HCS08 ? BNE (maIMM1 〈x0,x8〉) ?) @ +(* [0x19C9] LDA 6,SP *) (compile HCS08 ? LDA (maSP1 〈x0,x6〉) ?) @ +(* [0x19CC] CMP 9,SP *) (compile HCS08 ? CMP (maSP1 〈x0,x9〉) ?) @ +(* [0x19CF] BHI *+21 ; 0x19E4 *) (compile HCS08 ? BHI (maIMM1 〈x1,x3〉) ?) @ +(* [0x19D1] LDA 9,SP *) (compile HCS08 ? LDA (maSP1 〈x0,x9〉) ?) @ +(* [0x19D4] SUB 6,SP *) (compile HCS08 ? SUB (maSP1 〈x0,x6〉) ?) @ +(* [0x19D7] STA 9,SP *) (compile HCS08 ? STA (maSP1 〈x0,x9〉) ?) @ +(* [0x19DA] LDA 1,SP *) (compile HCS08 ? LDA (maSP1 〈x0,x1〉) ?) @ +(* [0x19DD] SBC 5,SP *) (compile HCS08 ? SBC (maSP1 〈x0,x5〉) ?) @ +(* [0x19E0] STA 1,SP *) (compile HCS08 ? STA (maSP1 〈x0,x1〉) ?) @ +(* [0x19E3] SEC *) (compile HCS08 ? SEC maINH ?) @ +(* [0x19E4] DBNZX *-46 ; 0x19B6 *) (compile HCS08 ? DBNZ (maINHX_and_IMM1 〈xD,x0〉) ?) @ +(* [0x19E6] LDA 10,SP *) (compile HCS08 ? LDA (maSP1 〈x0,xA〉) ?) @ +(* [0x19E9] ROLA *) (compile HCS08 ? ROL maINHA ?) @ +(* [0x19EA] STA 6,SP *) (compile HCS08 ? STA (maSP1 〈x0,x6〉) ?) @ +(* [0x19ED] LDA 9,SP *) (compile HCS08 ? LDA (maSP1 〈x0,x9〉) ?) @ +(* [0x19F0] STA 10,SP *) (compile HCS08 ? STA (maSP1 〈x0,xA〉) ?) @ +(* [0x19F3] PULA *) (compile HCS08 ? PULA maINH ?) @ +(* [0x19F4] STA 8,SP *) (compile HCS08 ? STA (maSP1 〈x0,x8〉) ?) @ +(* [0x19F7] CLR 4,SP *) (compile HCS08 ? CLR (maSP1 〈x0,x4〉) ?) @ +(* [0x19FA] RTS *) (compile HCS08 ? RTS maINH ?) @ + +(* +static void _LADD_k_is_k_plus_j(_PARAM_BINARY_L) { ... } +*) + +(* [0x19FB] TSX *) (compile HCS08 ? TSX maINH ?) @ +(* [0x19FC] LDA 18,X *) (compile HCS08 ? LDA (maIX1 〈x1,x2〉) ?) @ +(* [0x19FE] ADD 5,X *) (compile HCS08 ? ADD (maIX1 〈x0,x5〉) ?) @ +(* [0x1A00] STA 18,X *) (compile HCS08 ? STA (maIX1 〈x1,x2〉) ?) @ +(* [0x1A02] LDA 17,X *) (compile HCS08 ? LDA (maIX1 〈x1,x1〉) ?) @ +(* [0x1A04] ADC 4,X *) (compile HCS08 ? ADC (maIX1 〈x0,x4〉) ?) @ +(* [0x1A06] STA 17,X *) (compile HCS08 ? STA (maIX1 〈x1,x1〉) ?) @ +(* [0x1A08] LDA 16,X *) (compile HCS08 ? LDA (maIX1 〈x1,x0〉) ?) @ +(* [0x1A0A] ADC 3,X *) (compile HCS08 ? ADC (maIX1 〈x0,x3〉) ?) @ +(* [0x1A0C] STA 16,X *) (compile HCS08 ? STA (maIX1 〈x1,x0〉) ?) @ +(* [0x1A0E] LDA 15,X *) (compile HCS08 ? LDA (maIX1 〈x0,xF〉) ?) @ +(* [0x1A10] ADC 2,X *) (compile HCS08 ? ADC (maIX1 〈x0,x2〉) ?) @ +(* [0x1A12] STA 15,X *) (compile HCS08 ? STA (maIX1 〈x0,xF〉) ?) @ +(* [0x1A14] AIS #10 *) (compile HCS08 ? AIS (maIMM1 〈x0,xA〉) ?) @ +(* [0x1A16] PULH *) (compile HCS08 ? PULH maINH ?) @ +(* [0x1A17] PULX *) (compile HCS08 ? PULX maINH ?) @ +(* [0x1A18] PULA *) (compile HCS08 ? PULA maINH ?) @ +(* [0x1A19] RTS *) (compile HCS08 ? RTS maINH ?) @ + +(* +void _IMODU_STAR08(int i, ...) { ... } +*) + +(* [0x1A1A] AIS #-2 *) (compile HCS08 ? AIS (maIMM1 〈xF,xE〉) ?) @ +(* [0x1A1C] STHX 1,SP *) (compile HCS08 ? STHX (maSP1 〈x0,x1〉) ?) @ +(* [0x1A1F] PSHA *) (compile HCS08 ? PSHA maINH ?) @ +(* [0x1A20] JSR 0x1992 *) (compile HCS08 ? JSR (maIMM2 〈〈x1,x9〉:〈x9,x2〉〉) ?) @ +(* [0x1A23] PULA *) (compile HCS08 ? PULA maINH ?) @ +(* [0x1A24] AIS #2 *) (compile HCS08 ? AIS (maIMM1 〈x0,x2〉) ?) @ +(* [0x1A26] LDHX 3,SP *) (compile HCS08 ? LDHX (maSP1 〈x0,x3〉) ?) @ +(* [0x1A29] RTS *) (compile HCS08 ? RTS maINH ?) @ + +(* +void _LADD(void) { ... } +*) + +(* [0x1A2A] JSR 0x197C *) (compile HCS08 ? JSR (maIMM2 〈〈x1,x9〉:〈x7,xC〉〉) ?) @ +(* [0x1A2D] JSR 0x19FB *) (compile HCS08 ? JSR (maIMM2 〈〈x1,x9〉:〈xF,xB〉〉) ?) @ + +(* +void _POP32(void) { ... } +*) + +(* [0x1A30] PSHA *) (compile HCS08 ? PSHA maINH ?) @ +(* [0x1A31] LDA 4,SP *) (compile HCS08 ? LDA (maSP1 〈x0,x4〉) ?) @ +(* [0x1A34] STA ,X *) (compile HCS08 ? STA maIX0 ?) @ +(* [0x1A35] LDA 5,SP *) (compile HCS08 ? LDA (maSP1 〈x0,x5〉) ?) @ +(* [0x1A38] STA 1,X *) (compile HCS08 ? STA (maIX1 〈x0,x1〉) ?) @ +(* [0x1A3A] LDA 6,SP *) (compile HCS08 ? LDA (maSP1 〈x0,x6〉) ?) @ +(* [0x1A3D] STA 2,X *) (compile HCS08 ? STA (maIX1 〈x0,x2〉) ?) @ +(* [0x1A3F] LDA 7,SP *) (compile HCS08 ? LDA (maSP1 〈x0,x7〉) ?) @ +(* [0x1A42] STA 3,X *) (compile HCS08 ? STA (maIX1 〈x0,x3〉) ?) @ +(* [0x1A44] PULA *) (compile HCS08 ? PULA maINH ?) @ +(* [0x1A45] PULH *) (compile HCS08 ? PULH maINH ?) @ +(* [0x1A46] PULX *) (compile HCS08 ? PULX maINH ?) @ +(* [0x1A47] AIS #4 *) (compile HCS08 ? AIS (maIMM1 〈x0,x4〉) ?) @ +(* [0x1A49] JMP ,X *) (compile HCS08 ? JMP maINHX0ADD ?) + +(* 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 *) + ). napply I. nqed. + +(* creazione del processore+caricamento+impostazione registri *) +ndefinition 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_model HCS08 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) (extu_w32 addr)) + data (extu_w32 dTest_HCS08_RAM)) + (build_memory_type_of_model HCS08 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 *) +ndefinition 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) *) +nlet 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 + nat2)) n' ntot ] + ]. + +(* esecuzione execute k*(n+1)*(n+2) *) +nlet 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 + nat1) ntot) n' ntot ] + ]. + +(* esecuzione execute k*n*(n+1)*(n+2) *) +nlet 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) *) +ndefinition 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') nat11 ntot) nat80 + ]. + +(* parametrizzazione dell'enunciato del teorema parziale *) +nlemma 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) *) + (nat_of_w16 num) with + [ TickERR s _ ⇒ None ? + (* azzeramento tutta RAM tranne dati *) + | TickSUSP s _ ⇒ Some ? (set_mem_desc HCS08 t s (load_from_source_at t (mem_desc HCS08 t s) dTest_zeros3K (extu_w32 〈〈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)). + +ndefinition 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)) + (nat_of_w16 num) with + [ TickERR s _ ⇒ None ? + | TickSUSP s _ ⇒ Some ? (set_mem_desc HCS08 MEM_TREE s (load_from_source_at MEM_TREE (mem_desc HCS08 MEM_TREE s) dTest_zeros3K (extu_w32 〈〈x0,x1〉:〈x2,x0〉〉))) + | TickOK s ⇒ None ? + ]. + +ndefinition 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)). + +ndefinition gNumCalc1 ≝ gNumCalc 〈〈x0,x0〉:〈x0,x1〉〉. +ndefinition gNumCalc2 ≝ gNumCalc 〈〈x0,x0〉:〈x0,x2〉〉. +ndefinition gNumCalc5 ≝ gNumCalc 〈〈x0,x0〉:〈x0,x5〉〉. +ndefinition gNumCalc10 ≝ gNumCalc 〈〈x0,x0〉:〈x0,xA〉〉. +ndefinition gNumCalc20 ≝ gNumCalc 〈〈x0,x0〉:〈x1,x4〉〉. +ndefinition gNumCalc50 ≝ gNumCalc 〈〈x0,x0〉:〈x3,x2〉〉. +ndefinition gNumCalc100 ≝ gNumCalc 〈〈x0,x0〉:〈x6,x4〉〉. +ndefinition gNumCalc250 ≝ gNumCalc 〈〈x0,x0〉:〈xF,xA〉〉. +ndefinition gNumCalc500 ≝ gNumCalc 〈〈x0,x1〉:〈xF,x4〉〉. +ndefinition gNumCalc1000 ≝ gNumCalc 〈〈x0,x3〉:〈xE,x8〉〉. + +ndefinition gNumNoCalc1 ≝ gNumNoCalc 〈〈x0,x0〉:〈x0,x1〉〉. +ndefinition gNumNoCalc2 ≝ gNumNoCalc 〈〈x0,x0〉:〈x0,x2〉〉. +ndefinition gNumNoCalc5 ≝ gNumNoCalc 〈〈x0,x0〉:〈x0,x5〉〉. +ndefinition gNumNoCalc10 ≝ gNumNoCalc 〈〈x0,x0〉:〈x0,xA〉〉. +ndefinition gNumNoCalc20 ≝ gNumNoCalc 〈〈x0,x0〉:〈x1,x4〉〉. +ndefinition gNumNoCalc50 ≝ gNumNoCalc 〈〈x0,x0〉:〈x3,x2〉〉. +ndefinition gNumNoCalc100 ≝ gNumNoCalc 〈〈x0,x0〉:〈x6,x4〉〉. +ndefinition gNumNoCalc250 ≝ gNumNoCalc 〈〈x0,x0〉:〈xF,xA〉〉. +ndefinition gNumNoCalc500 ≝ gNumNoCalc 〈〈x0,x1〉:〈xF,x4〉〉. +ndefinition gNumNoCalc1000 ≝ gNumNoCalc 〈〈x0,x3〉:〈xE,x8〉〉. diff --git a/helm/software/matita/contribs/ng_assembly/emulator/tests/medium_tests_tools.ma b/helm/software/matita/contribs/ng_assembly/emulator/tests/medium_tests_tools.ma new file mode 100755 index 000000000..3bee9c998 --- /dev/null +++ b/helm/software/matita/contribs/ng_assembly/emulator/tests/medium_tests_tools.ma @@ -0,0 +1,592 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +(* ********************************************************************** *) +(* Progetto FreeScale *) +(* *) +(* Sviluppato da: Ing. Cosimo Oliboni, oliboni@cs.unibo.it *) +(* Sviluppo: 2008-2010 *) +(* *) +(* ********************************************************************** *) + +include "emulator/multivm/multivm.ma". + +(* ********* *) +(* INDIRIZZI *) +(* ********* *) + +(* specifico per MC9S08GB60 in modo da caricare codice compilato da CodeWarrior *) +(* l'obbiettivo e' dimostrare una routine scritta in C *) +(* passo 1 e' formalizzare l'uso di 3Kb dei 4Kb di RAM [0x0100-0x0CFF] *) +ndefinition dTest_HCS08_RAM ≝ 〈〈x0,x1〉:〈x0,x0〉〉. +ndefinition dTest_HCS08_prog ≝ 〈〈x1,x8〉:〈xC,x8〉〉. + +(* ***** *) +(* TOOLS *) +(* ***** *) + +(* visita di un albero da 256B di elementi: ln16(256)=2 passaggi *) +ndefinition dTest_visit ≝ +λdata:Array16T (Array16T (list byte8)).λaddr:byte8. + getn_array16T (cnL ? addr) ? + (getn_array16T (cnH ? addr) ? data). + +(* scrittura di un elemento in un albero da 256B *) +ndefinition dTest_update ≝ +λdata:Array16T (Array16T (list byte8)).λaddr:byte8.λv:list byte8. + let lev2 ≝ getn_array16T (cnH ? addr) ? data in + setn_array16T (cnH ? addr) ? data + (setn_array16T (cnL ? addr) ? lev2 v) . + +(* array a 0 *) +ndefinition dTest_zero_array ≝ +let elem ≝ nil byte8 in +let lev2 ≝ mk_Array16T ? + elem elem elem elem elem elem elem elem + elem elem elem elem elem elem elem elem + in +let lev1 ≝ mk_Array16T ? + lev2 lev2 lev2 lev2 lev2 lev2 lev2 lev2 + lev2 lev2 lev2 lev2 lev2 lev2 lev2 lev2 + in +lev1. + +(* incrementa n-simo elemento *) +ndefinition dTest_inc ≝ +λdata:Array16T (Array16T (list byte8)).λaddr:byte8. + dTest_update data addr ((dTest_visit data addr)@[ addr ]). + +(* costruisce una lista a partire dai conteggi per elemento *) +ndefinition dTest_build_list_from_count ≝ +λdata:Array16T (Array16T (list byte8)). + let aux1 ≝ λparam1:Array16T (list byte8). + match param1 with + [ mk_Array16T e00 e01 e02 e03 e04 e05 e06 e07 e08 e09 e10 e11 e12 e13 e14 e15 ⇒ + e00@e01@e02@e03@e04@e05@e06@e07@e08@e09@e10@e11@e12@e13@e14@e15 ] in + let aux2 ≝ λparam2:Array16T (Array16T (list byte8)). + match param2 with + [ mk_Array16T e00 e01 e02 e03 e04 e05 e06 e07 e08 e09 e10 e11 e12 e13 e14 e15 ⇒ + (aux1 e00)@(aux1 e01)@(aux1 e02)@(aux1 e03)@(aux1 e04)@(aux1 e05)@(aux1 e06)@(aux1 e07)@ + (aux1 e08)@(aux1 e09)@(aux1 e10)@(aux1 e11)@(aux1 e12)@(aux1 e13)@(aux1 e14)@(aux1 e15) ] in + aux2 data. + +(* ci sono ora tutti gli elementi per definire l'ordinamento *) +(* di una lista di byte8 secondo il counting sort *) +nlet rec byte8_list_ordering_aux (source:list byte8) (count:Array16T (Array16T (list byte8))) on source ≝ + match source with + [ nil ⇒ dTest_build_list_from_count count + | cons hd tl ⇒ byte8_list_ordering_aux tl (dTest_inc count hd) + ]. + +ndefinition byte8_list_ordering ≝ +λsource:list byte8.byte8_list_ordering_aux source dTest_zero_array. + +(* strlen esadecimale limitato, considerando overflow! *) +nlet rec byte8_bounded_strlen_aux (source:list byte8) (count,limit:word16) on source ≝ + match source with + [ nil ⇒ True + | cons _ tl ⇒ match eq_w16 count 〈〈xF,xF〉:〈xF,xF〉〉 with + [ true ⇒ False + | false ⇒ match le_w16 (succ_w16 count) limit with + [ true ⇒ byte8_bounded_strlen_aux tl (succ_w16 count) limit + | false ⇒ False + ] + ] + ]. + +ndefinition byte8_bounded_strlen ≝ +λsource:list byte8.λlimit:word16. + byte8_bounded_strlen_aux source 〈〈x0,x0〉:〈x0,x0〉〉 limit. + +(* strlen esadecimale normale *) +nlet rec byte8_strlen_aux (source:list byte8) (count:word16) on source ≝ + match source with + [ nil ⇒ count + | cons _ tl ⇒ byte8_strlen_aux tl (succ_w16 count) + ]. + +ndefinition byte8_strlen ≝ +λsource:list byte8. + byte8_strlen_aux source 〈〈x0,x0〉:〈x0,x0〉〉. + +(* hex dump: memory -> list byte8 *) +nlet rec byte8_hexdump_aux (t:memory_impl) (mem:aux_mem_type t) (inf:word32) (count:nat) (out:list byte8) on count ≝ + match count with + [ O ⇒ out + | S n ⇒ byte8_hexdump_aux t mem (succ_w32 inf) n (out@[ mem_read_abs t mem inf ]) + ]. + +ndefinition byte8_hexdump ≝ +λt:memory_impl.λmem:aux_mem_type t.λinf:word32.λcount:nat. + byte8_hexdump_aux t mem inf count []. + +(* ************* *) +(* TEST PATTERNS *) +(* ************* *) + +(* lista di 3072 numeri random generati da Mathematica, in blocchi da 32 *) +ndefinition dTest_random_ex00 ≝ +[〈x8,x1〉;〈x5,xE〉;〈x7,x6〉;〈xD,x1〉;〈x7,x5〉;〈x1,x0〉;〈x8,x5〉;〈x9,x0〉;〈x1,xF〉;〈x1,x2〉;〈xE,x2〉;〈x3,xC〉;〈x1,xD〉;〈x0,x6〉;〈x3,xC〉;〈xD,x1〉 +;〈x8,x3〉;〈xE,xB〉;〈x7,x2〉;〈x1,xF〉;〈x9,x0〉;〈xF,x0〉;〈x4,x7〉;〈xA,x3〉;〈xD,x0〉;〈x4,x6〉;〈xC,x5〉;〈x3,x2〉;〈xC,x9〉;〈x0,xB〉;〈x1,xB〉;〈x7,x3〉 ]. + +ndefinition dTest_random_ex01 ≝ +[〈x1,x1〉;〈xA,xF〉;〈xD,x2〉;〈xB,xF〉;〈x0,xB〉;〈xB,xC〉;〈x0,x8〉;〈xE,x5〉;〈xF,xE〉;〈xA,xC〉;〈xF,xC〉;〈x9,x4〉;〈x3,x4〉;〈x8,x8〉;〈x2,x8〉;〈xD,xB〉 +;〈xD,x3〉;〈x3,xD〉;〈x3,x8〉;〈x6,xA〉;〈x4,xD〉;〈x7,x4〉;〈x4,x9〉;〈x7,xE〉;〈x6,xF〉;〈x4,xD〉;〈x3,xD〉;〈x3,xA〉;〈xC,x2〉;〈xD,x3〉;〈x3,x6〉;〈x7,x0〉 ]. + +ndefinition dTest_random_ex02 ≝ +[〈x8,x0〉;〈xC,x9〉;〈x3,xB〉;〈x5,x2〉;〈x8,xF〉;〈x1,xE〉;〈x8,x4〉;〈x5,x2〉;〈x2,xD〉;〈xA,xF〉;〈x1,xB〉;〈x0,x1〉;〈x3,x5〉;〈x7,x2〉;〈x1,x0〉;〈x0,x7〉 +;〈x5,xD〉;〈xA,xB〉;〈xE,x0〉;〈x7,x6〉;〈xB,xD〉;〈x3,xC〉;〈x0,xD〉;〈xC,xE〉;〈xB,x7〉;〈x9,xD〉;〈xA,x9〉;〈xF,x3〉;〈xC,x1〉;〈x9,x3〉;〈x8,xC〉;〈x4,xE〉 ]. + +ndefinition dTest_random_ex03 ≝ +[〈xF,x8〉;〈xC,x3〉;〈x1,x3〉;〈x3,xA〉;〈xA,x2〉;〈xB,xD〉;〈x1,x0〉;〈x9,xB〉;〈x5,xC〉;〈xC,x8〉;〈xE,x5〉;〈xC,x8〉;〈xA,x6〉;〈xF,xB〉;〈x1,x3〉;〈xC,x8〉 +;〈x6,x4〉;〈x0,x9〉;〈xD,x6〉;〈xD,x7〉;〈x3,x9〉;〈xF,x9〉;〈xE,x4〉;〈x0,x3〉;〈x4,x9〉;〈xC,xE〉;〈x7,x1〉;〈x5,x7〉;〈x3,x4〉;〈x2,xE〉;〈xA,x3〉;〈x5,x3〉 ]. + +ndefinition dTest_random_ex04 ≝ +[〈xF,x9〉;〈x2,xA〉;〈xF,x0〉;〈xE,x1〉;〈x6,x6〉;〈x8,x9〉;〈x2,xE〉;〈x8,x6〉;〈xC,x7〉;〈x2,xD〉;〈x1,x2〉;〈xD,x5〉;〈x4,xA〉;〈x7,x9〉;〈x6,xD〉;〈x1,xB〉 +;〈x4,x1〉;〈x9,x4〉;〈x6,xC〉;〈x6,xD〉;〈xF,x4〉;〈x5,xD〉;〈x8,xB〉;〈xB,xE〉;〈xC,x8〉;〈xE,x5〉;〈xA,x4〉;〈xB,xA〉;〈xB,x1〉;〈x2,x1〉;〈x5,x0〉;〈x6,xB〉 ]. + +ndefinition dTest_random_ex05 ≝ +[〈x9,x5〉;〈x0,x6〉;〈x4,x5〉;〈xE,x0〉;〈x0,xF〉;〈x5,xA〉;〈xC,xE〉;〈xC,x8〉;〈x8,x2〉;〈x4,xF〉;〈xC,x2〉;〈xF,x5〉;〈xF,x8〉;〈x1,x3〉;〈xD,xA〉;〈x2,xB〉 +;〈x7,x9〉;〈xB,xF〉;〈xA,x4〉;〈x5,xA〉;〈xD,x2〉;〈x7,x6〉;〈x8,xD〉;〈x1,xF〉;〈x1,x5〉;〈x5,xA〉;〈xD,xE〉;〈x2,x3〉;〈x9,xD〉;〈x7,xE〉;〈x6,x7〉;〈x6,x3〉 ]. + +ndefinition dTest_random_ex06 ≝ +[〈x1,x1〉;〈xF,x5〉;〈x2,x4〉;〈xD,x6〉;〈x6,xA〉;〈x0,xC〉;〈x7,xF〉;〈x1,x2〉;〈xD,x6〉;〈xE,xE〉;〈xB,xA〉;〈x4,x4〉;〈x3,x9〉;〈x9,x2〉;〈x6,x6〉;〈xE,xA〉 +;〈x2,x3〉;〈x4,x4〉;〈xC,xF〉;〈x7,x4〉;〈x6,xB〉;〈x8,x3〉;〈x7,x7〉;〈x0,x4〉;〈x6,x4〉;〈xB,x3〉;〈x3,xC〉;〈x2,x6〉;〈xF,xC〉;〈xD,x5〉;〈x4,x1〉;〈xB,x7〉 ]. + +ndefinition dTest_random_ex07 ≝ +[〈x2,x4〉;〈xE,x0〉;〈xB,x4〉;〈x1,x3〉;〈x3,x2〉;〈x4,x5〉;〈x1,x8〉;〈xD,xB〉;〈x0,x0〉;〈xB,x6〉;〈x5,xF〉;〈x3,xA〉;〈xB,x7〉;〈x4,xF〉;〈xB,x4〉;〈xD,xF〉 +;〈xF,x4〉;〈x1,xA〉;〈x1,x0〉;〈xE,x9〉;〈xC,x5〉;〈x2,xC〉;〈xB,xC〉;〈x5,xB〉;〈x0,x5〉;〈x4,xA〉;〈x5,x2〉;〈xC,x0〉;〈x1,xF〉;〈x5,x9〉;〈xF,x2〉;〈xE,x5〉 ]. + +ndefinition dTest_random_ex08 ≝ +[〈x9,x7〉;〈x5,x1〉;〈xF,x7〉;〈x3,xC〉;〈x7,x7〉;〈x8,x1〉;〈x7,xC〉;〈xB,x0〉;〈x1,xD〉;〈x1,xA〉;〈x7,xB〉;〈x4,x7〉;〈x7,x9〉;〈xC,x2〉;〈x3,xF〉;〈xD,x3〉 +;〈xB,x6〉;〈xD,x7〉;〈xC,x9〉;〈x9,x2〉;〈x0,xD〉;〈x7,xF〉;〈x0,xB〉;〈x7,x5〉;〈x0,xE〉;〈x5,x1〉;〈x9,xF〉;〈x4,xC〉;〈xE,x5〉;〈xD,x0〉;〈xC,x1〉;〈x3,x9〉 ]. + +ndefinition dTest_random_ex09 ≝ +[〈x7,xF〉;〈xE,xA〉;〈x4,x1〉;〈x0,x5〉;〈x0,x8〉;〈x7,xE〉;〈x7,x6〉;〈x2,xF〉;〈x6,x2〉;〈x7,x1〉;〈xF,x8〉;〈x3,x8〉;〈xB,x6〉;〈x7,x0〉;〈xD,xD〉;〈xD,x0〉 +;〈xA,xD〉;〈x7,x8〉;〈x3,xD〉;〈x7,xB〉;〈xC,xC〉;〈x6,xD〉;〈x3,xF〉;〈xA,xC〉;〈xC,x7〉;〈x6,xE〉;〈xF,xF〉;〈x4,x5〉;〈xC,x1〉;〈x7,x4〉;〈xB,xF〉;〈x2,x9〉 ]. + +ndefinition dTest_random_ex0A ≝ +[〈x4,x9〉;〈xC,x5〉;〈x7,xC〉;〈x2,xD〉;〈xF,x2〉;〈xC,xC〉;〈xF,xA〉;〈x5,x8〉;〈xA,xC〉;〈x5,x8〉;〈x5,x1〉;〈x0,xE〉;〈x4,x8〉;〈x7,x0〉;〈x4,x1〉;〈xE,xD〉 +;〈x9,x5〉;〈xB,x4〉;〈x4,x7〉;〈xF,x1〉;〈x8,x1〉;〈xE,x4〉;〈x4,x0〉;〈x5,x4〉;〈x7,xB〉;〈xA,x1〉;〈xD,x2〉;〈x0,x2〉;〈xC,x5〉;〈x7,xD〉;〈x7,xA〉;〈xF,x1〉 ]. + +ndefinition dTest_random_ex0B ≝ +[〈x0,x0〉;〈x8,xD〉;〈x6,x6〉;〈xB,x0〉;〈xA,x9〉;〈x7,xA〉;〈x2,xB〉;〈x2,xC〉;〈x6,xF〉;〈x5,xF〉;〈x6,xF〉;〈x4,xE〉;〈x2,xB〉;〈x1,x1〉;〈xF,xF〉;〈x4,x7〉 +;〈x7,xF〉;〈xC,xF〉;〈xD,x3〉;〈x8,x5〉;〈xB,x8〉;〈x4,xD〉;〈x9,x9〉;〈x8,x3〉;〈x7,x6〉;〈xE,x8〉;〈x3,x0〉;〈xF,x8〉;〈xD,x0〉;〈x5,x9〉;〈xB,x8〉;〈x7,x1〉 ]. + +ndefinition dTest_random_ex0C ≝ +[〈x5,x7〉;〈xA,xF〉;〈xB,x5〉;〈xD,x5〉;〈xF,xC〉;〈x8,x2〉;〈x1,x6〉;〈x1,x0〉;〈xB,x3〉;〈xC,x1〉;〈x1,xA〉;〈x0,x1〉;〈x1,x1〉;〈xF,xF〉;〈x5,x9〉;〈x2,x4〉 +;〈xC,x5〉;〈x7,x2〉;〈xD,x8〉;〈xD,x0〉;〈xA,xD〉;〈xF,xE〉;〈xD,x7〉;〈x1,x1〉;〈xC,xE〉;〈xF,x9〉;〈xB,x8〉;〈x7,x7〉;〈x3,xA〉;〈x1,xF〉;〈x6,x1〉;〈x1,xB〉 ]. + +ndefinition dTest_random_ex0D ≝ +[〈xB,xB〉;〈x5,x5〉;〈x8,x0〉;〈x7,xC〉;〈x2,x5〉;〈x3,x4〉;〈x8,x9〉;〈xF,x2〉;〈xC,x9〉;〈xD,xF〉;〈x3,x5〉;〈xC,x5〉;〈x1,x2〉;〈xF,x0〉;〈x0,x5〉;〈xD,xE〉 +;〈x2,x6〉;〈x4,x9〉;〈xB,x7〉;〈x3,x9〉;〈x0,x5〉;〈xC,x2〉;〈xD,xB〉;〈xF,xC〉;〈x9,xF〉;〈xA,x9〉;〈x6,x6〉;〈xA,xD〉;〈x4,xA〉;〈x3,xF〉;〈xB,xF〉;〈x6,xD〉 ]. + +ndefinition dTest_random_ex0E ≝ +[〈x8,x7〉;〈x6,xA〉;〈xB,x1〉;〈x3,xE〉;〈xB,x6〉;〈x0,xE〉;〈x7,xA〉;〈x3,xB〉;〈x4,x5〉;〈xE,x9〉;〈xC,xE〉;〈x6,xA〉;〈x6,xA〉;〈x7,x0〉;〈x6,x0〉;〈x6,xA〉 +;〈x2,xC〉;〈xD,x2〉;〈xB,x8〉;〈x3,x6〉;〈x2,x1〉;〈x0,x0〉;〈x5,x4〉;〈x3,x1〉;〈x6,x0〉;〈x1,xB〉;〈x4,xC〉;〈xC,xA〉;〈xB,xE〉;〈x5,xF〉;〈x8,x1〉;〈xB,x7〉 ]. + +ndefinition dTest_random_ex0F ≝ +[〈x9,xB〉;〈x2,x6〉;〈x9,x4〉;〈x2,xB〉;〈x4,x1〉;〈x2,xB〉;〈x9,x8〉;〈x6,x3〉;〈x6,x6〉;〈x6,x5〉;〈x4,x6〉;〈x2,x3〉;〈xE,x5〉;〈x0,x7〉;〈x9,xE〉;〈x1,xC〉 +;〈x3,x8〉;〈x5,xC〉;〈x9,x7〉;〈x6,x3〉;〈x5,x3〉;〈x6,x6〉;〈x0,x8〉;〈x5,xD〉;〈x0,x8〉;〈xD,xB〉;〈x6,xE〉;〈x5,x6〉;〈x7,x0〉;〈x3,x2〉;〈x4,x5〉;〈x0,x2〉 ]. + +ndefinition dTest_random_ex10 ≝ +[〈x6,x3〉;〈x7,x2〉;〈x9,xC〉;〈xD,x9〉;〈x5,x0〉;〈x0,x6〉;〈x5,x9〉;〈x1,x7〉;〈x6,x8〉;〈xD,x2〉;〈xD,x7〉;〈x8,xE〉;〈x6,x9〉;〈x5,xF〉;〈x8,x1〉;〈x8,x4〉 +;〈x8,x7〉;〈xD,xC〉;〈x9,x8〉;〈xE,x5〉;〈xB,x5〉;〈xC,x3〉;〈x2,x5〉;〈x6,xC〉;〈x9,x2〉;〈xD,xD〉;〈x2,xA〉;〈xD,x1〉;〈x1,x4〉;〈x7,xE〉;〈x1,x7〉;〈xB,x2〉 ]. + +ndefinition dTest_random_ex11 ≝ +[〈x9,x8〉;〈x5,x5〉;〈xF,xC〉;〈x3,xD〉;〈x8,xD〉;〈xE,xF〉;〈x8,x1〉;〈xB,x8〉;〈xB,xB〉;〈x5,x1〉;〈x0,x0〉;〈xB,x4〉;〈x2,xE〉;〈x3,x0〉;〈x6,x0〉;〈x7,xE〉 +;〈x9,x0〉;〈xE,x3〉;〈xF,x4〉;〈x7,x2〉;〈x1,xC〉;〈xB,x3〉;〈x7,x8〉;〈x1,xB〉;〈x9,xF〉;〈x1,xB〉;〈x0,x3〉;〈xA,x3〉;〈x0,x5〉;〈xD,xE〉;〈x3,x8〉;〈xB,xA〉 ]. + +ndefinition dTest_random_ex12 ≝ +[〈x0,xE〉;〈xE,xD〉;〈xE,xC〉;〈x1,xF〉;〈x3,x8〉;〈xE,x3〉;〈xF,x7〉;〈xA,xA〉;〈xE,x9〉;〈x3,xD〉;〈xF,xF〉;〈xF,x3〉;〈x1,x4〉;〈x2,xC〉;〈x8,x8〉;〈x6,x1〉 +;〈x3,x0〉;〈xA,xB〉;〈x1,x8〉;〈xD,xC〉;〈xF,xE〉;〈x6,xA〉;〈x2,x9〉;〈xF,x1〉;〈xC,xB〉;〈x9,x0〉;〈x7,x8〉;〈x9,x9〉;〈x1,xF〉;〈x2,x8〉;〈xF,x9〉;〈xC,xB〉 ]. + +ndefinition dTest_random_ex13 ≝ +[〈x1,x4〉;〈x8,x4〉;〈xF,x3〉;〈xD,x6〉;〈x7,xE〉;〈xE,xC〉;〈x5,x6〉;〈xC,xE〉;〈xD,xA〉;〈x5,xE〉;〈x6,x1〉;〈xF,x1〉;〈x6,x6〉;〈x6,x9〉;〈x9,x3〉;〈x5,x9〉 +;〈x3,xC〉;〈x1,xD〉;〈x6,xB〉;〈xF,x4〉;〈x5,x9〉;〈x4,xD〉;〈x3,x8〉;〈xA,x9〉;〈x3,xB〉;〈x7,xF〉;〈xB,x2〉;〈xE,xC〉;〈xA,xE〉;〈xF,x6〉;〈xB,x2〉;〈x2,x2〉 ]. + +ndefinition dTest_random_ex14 ≝ +[〈x6,x4〉;〈x2,x7〉;〈x6,xC〉;〈x2,x0〉;〈xE,xE〉;〈x5,x1〉;〈x3,xE〉;〈x8,x8〉;〈xD,xD〉;〈xC,x1〉;〈xD,xC〉;〈xC,x1〉;〈x6,x6〉;〈x6,x1〉;〈x4,x2〉;〈x7,x7〉 +;〈x3,x6〉;〈x0,x8〉;〈x2,x9〉;〈x6,x0〉;〈xA,x9〉;〈xF,xC〉;〈x7,xC〉;〈xA,x7〉;〈xB,x4〉;〈xF,xC〉;〈x8,x7〉;〈x1,xD〉;〈x6,xC〉;〈xA,x2〉;〈x3,xF〉;〈x1,xD〉 ]. + +ndefinition dTest_random_ex15 ≝ +[〈x1,x7〉;〈x0,xF〉;〈x0,x2〉;〈x2,x6〉;〈xA,x2〉;〈x6,xA〉;〈x5,xC〉;〈xE,xD〉;〈x2,x7〉;〈xC,x5〉;〈x7,xB〉;〈xF,x5〉;〈x9,xC〉;〈x8,x5〉;〈x6,x3〉;〈x5,x6〉 +;〈xC,x3〉;〈x4,xB〉;〈x1,xB〉;〈xA,x0〉;〈x1,xB〉;〈x8,x9〉;〈x3,x5〉;〈xD,x6〉;〈xD,x9〉;〈xD,xD〉;〈x2,xE〉;〈x6,x2〉;〈x7,x5〉;〈xE,x7〉;〈x1,x8〉;〈x4,xD〉 ]. + +ndefinition dTest_random_ex16 ≝ +[〈xD,x7〉;〈x5,x8〉;〈xA,x7〉;〈x5,xF〉;〈x9,x4〉;〈x8,x7〉;〈xA,x8〉;〈xE,x7〉;〈x2,xB〉;〈xF,x2〉;〈xE,x7〉;〈xB,x9〉;〈x0,x6〉;〈xA,xF〉;〈xD,xA〉;〈xD,xC〉 +;〈xC,x6〉;〈x3,xF〉;〈x8,xD〉;〈x7,x9〉;〈x9,x5〉;〈xD,xA〉;〈x5,xB〉;〈x9,x2〉;〈xE,xE〉;〈x3,xC〉;〈xF,xE〉;〈x4,x9〉;〈x5,xA〉;〈x1,x0〉;〈x4,xD〉;〈x8,x9〉 ]. + +ndefinition dTest_random_ex17 ≝ +[〈x8,x3〉;〈x2,x6〉;〈xE,xC〉;〈x8,xD〉;〈xC,x9〉;〈x7,x7〉;〈xE,xE〉;〈xF,x1〉;〈x4,x0〉;〈x6,xD〉;〈x4,x9〉;〈x5,x7〉;〈x9,xB〉;〈xC,x4〉;〈x1,xF〉;〈x8,x0〉 +;〈x9,x5〉;〈xB,xC〉;〈xE,x8〉;〈xF,x9〉;〈xD,x7〉;〈x1,x4〉;〈x3,xE〉;〈xC,x3〉;〈x6,xF〉;〈x8,xF〉;〈x7,x2〉;〈xD,x5〉;〈xB,xE〉;〈x8,xA〉;〈xA,x3〉;〈xF,x7〉 ]. + +ndefinition dTest_random_ex18 ≝ +[〈x6,x0〉;〈x3,xA〉;〈x7,x4〉;〈xF,xB〉;〈xB,xD〉;〈x7,x4〉;〈x8,x3〉;〈xE,x3〉;〈x9,xD〉;〈xD,x9〉;〈xB,x8〉;〈x1,x3〉;〈x5,x0〉;〈x4,x0〉;〈x8,xA〉;〈x9,x6〉 +;〈x3,xA〉;〈xA,x6〉;〈xE,xC〉;〈x7,xC〉;〈x1,x5〉;〈x8,x7〉;〈x4,xD〉;〈x6,xA〉;〈xA,xA〉;〈xE,x0〉;〈xB,xA〉;〈xF,xF〉;〈x3,xB〉;〈xE,x2〉;〈x5,x1〉;〈x2,x2〉 ]. + +ndefinition dTest_random_ex19 ≝ +[〈x2,x2〉;〈x1,xF〉;〈xA,x1〉;〈x2,x1〉;〈xA,xF〉;〈x3,x7〉;〈x8,xA〉;〈xD,xF〉;〈xE,x3〉;〈x6,x9〉;〈xE,xE〉;〈xC,x4〉;〈xE,x7〉;〈x7,x1〉;〈x9,x6〉;〈x1,x1〉 +;〈xE,x4〉;〈x3,x9〉;〈xE,x5〉;〈xA,xF〉;〈xF,x5〉;〈x5,x7〉;〈xE,xB〉;〈x5,x5〉;〈x6,x5〉;〈x8,xB〉;〈x3,xE〉;〈x8,xD〉;〈x4,x6〉;〈x5,x3〉;〈xB,x2〉;〈x1,x9〉 ]. + +ndefinition dTest_random_ex1A ≝ +[〈x3,x4〉;〈xE,x9〉;〈x4,xA〉;〈x4,xB〉;〈x5,x2〉;〈x3,x0〉;〈x3,xF〉;〈xA,x7〉;〈x4,xF〉;〈x1,xA〉;〈xB,x8〉;〈x6,x4〉;〈x5,xB〉;〈xD,x9〉;〈x6,xD〉;〈x6,x1〉 +;〈xA,x5〉;〈xC,xF〉;〈x8,xC〉;〈xD,xD〉;〈xE,x6〉;〈xD,x5〉;〈x3,x6〉;〈x0,xC〉;〈x8,xD〉;〈xF,x7〉;〈x4,xE〉;〈x9,xC〉;〈xB,xF〉;〈x2,xB〉;〈x4,x4〉;〈xD,x1〉 ]. + +ndefinition dTest_random_ex1B ≝ +[〈xC,x0〉;〈x8,x0〉;〈x0,x8〉;〈xA,xD〉;〈xC,xE〉;〈xB,xD〉;〈x4,xC〉;〈x5,x3〉;〈x6,x5〉;〈xB,x6〉;〈x4,x8〉;〈xF,x6〉;〈x6,x4〉;〈x7,xC〉;〈x9,x8〉;〈x1,x0〉 +;〈x9,xD〉;〈xF,xD〉;〈x4,x9〉;〈xC,x4〉;〈xD,xD〉;〈x1,x4〉;〈xB,x6〉;〈x6,xF〉;〈x3,xB〉;〈x4,x6〉;〈xD,x7〉;〈x1,xA〉;〈x4,x4〉;〈xA,x4〉;〈x8,x1〉;〈x3,x1〉 ]. + +ndefinition dTest_random_ex1C ≝ +[〈xA,x2〉;〈x4,x0〉;〈x7,x0〉;〈x3,x9〉;〈x9,xA〉;〈x4,xC〉;〈x4,xF〉;〈x9,x3〉;〈x9,xD〉;〈xD,x4〉;〈x9,x7〉;〈x3,x9〉;〈xA,x8〉;〈xA,x8〉;〈xF,x9〉;〈xB,x3〉 +;〈xE,x7〉;〈xD,x8〉;〈x4,xD〉;〈x6,xD〉;〈x8,x8〉;〈x6,xB〉;〈x5,x4〉;〈x5,x5〉;〈x9,x2〉;〈x1,x9〉;〈xE,x4〉;〈xB,x1〉;〈xE,x3〉;〈x4,x6〉;〈xD,x5〉;〈x6,xC〉 ]. + +ndefinition dTest_random_ex1D ≝ +[〈xF,x9〉;〈x3,x3〉;〈xE,x5〉;〈xD,x2〉;〈x7,x7〉;〈x1,x8〉;〈x8,x6〉;〈x1,x4〉;〈x7,xE〉;〈x1,xE〉;〈xC,x8〉;〈xB,x4〉;〈xC,xE〉;〈xC,x7〉;〈x5,x7〉;〈x2,xD〉 +;〈x5,x2〉;〈xE,x7〉;〈x5,x7〉;〈x9,xB〉;〈x1,xA〉;〈x4,x9〉;〈x0,x9〉;〈x4,xB〉;〈xF,x6〉;〈xB,x5〉;〈x0,xA〉;〈x2,xC〉;〈xB,xA〉;〈x1,xF〉;〈x2,x6〉;〈x3,x8〉 ]. + +ndefinition dTest_random_ex1E ≝ +[〈x6,x0〉;〈x3,x4〉;〈xC,x4〉;〈x8,x9〉;〈xB,xF〉;〈x0,x4〉;〈x5,xF〉;〈xF,x4〉;〈x1,x1〉;〈xF,x3〉;〈x4,xA〉;〈xE,x2〉;〈xD,x8〉;〈x3,x6〉;〈xF,xA〉;〈x4,x3〉 +;〈x0,xC〉;〈x6,x0〉;〈x5,x1〉;〈x2,xD〉;〈x0,x3〉;〈xF,xC〉;〈x9,x2〉;〈x2,x1〉;〈xC,xA〉;〈x7,x5〉;〈x6,x6〉;〈xD,xC〉;〈x8,x4〉;〈xC,x4〉;〈x6,xF〉;〈xF,x0〉 ]. + +ndefinition dTest_random_ex1F ≝ +[〈x0,x4〉;〈x5,x2〉;〈xA,xB〉;〈x9,xA〉;〈xC,xE〉;〈xA,xA〉;〈x2,xF〉;〈x3,x6〉;〈xF,x3〉;〈xA,x7〉;〈x4,x2〉;〈x0,x7〉;〈x5,xE〉;〈xB,x6〉;〈x5,xB〉;〈x9,x8〉 +;〈x7,x9〉;〈x4,x3〉;〈x8,x8〉;〈x9,xA〉;〈x0,xA〉;〈x5,x5〉;〈xE,x3〉;〈x9,x8〉;〈x7,x5〉;〈xA,x2〉;〈xE,xA〉;〈xB,x9〉;〈x3,x2〉;〈x4,x1〉;〈x0,x7〉;〈x3,x8〉 ]. + +ndefinition dTest_random_ex20 ≝ +[〈xB,x1〉;〈x0,x3〉;〈x4,xE〉;〈x6,xF〉;〈x9,x7〉;〈x3,xC〉;〈x5,x4〉;〈xB,xB〉;〈xB,xC〉;〈x0,xB〉;〈x0,xC〉;〈xA,xB〉;〈x3,xB〉;〈x2,x8〉;〈xA,xA〉;〈x0,x4〉 +;〈x5,x0〉;〈xA,x3〉;〈x6,xB〉;〈xF,xA〉;〈xF,x0〉;〈xE,x6〉;〈x1,x8〉;〈xD,x8〉;〈x7,xA〉;〈x5,xF〉;〈x0,x3〉;〈x8,x2〉;〈x9,x6〉;〈x9,xA〉;〈xB,xF〉;〈x1,x5〉 ]. + +ndefinition dTest_random_ex21 ≝ +[〈x8,x5〉;〈xE,xF〉;〈xB,x3〉;〈x7,xB〉;〈xE,xE〉;〈xE,xF〉;〈x1,x0〉;〈x6,x9〉;〈xC,x2〉;〈xF,x9〉;〈x2,xD〉;〈x8,x1〉;〈xF,x3〉;〈x0,xE〉;〈xC,x3〉;〈x7,xF〉 +;〈xD,xD〉;〈x2,xE〉;〈x2,xA〉;〈xB,xD〉;〈xE,xA〉;〈x9,x2〉;〈xF,xF〉;〈xF,xA〉;〈x7,xB〉;〈xD,x3〉;〈x3,x0〉;〈x7,x5〉;〈x6,x7〉;〈xA,x8〉;〈x0,xF〉;〈x2,x1〉 ]. + +ndefinition dTest_random_ex22 ≝ +[〈xD,xC〉;〈xE,x5〉;〈xE,x2〉;〈x8,x9〉;〈x2,x9〉;〈xC,x5〉;〈xA,x3〉;〈xA,x2〉;〈x4,x2〉;〈x3,xF〉;〈xA,x3〉;〈x5,x8〉;〈xE,x0〉;〈x7,xC〉;〈x0,x3〉;〈xF,xF〉 +;〈x2,x8〉;〈x8,xB〉;〈x8,xB〉;〈x1,x2〉;〈xD,x8〉;〈xA,x8〉;〈x7,x6〉;〈xB,x9〉;〈xE,x2〉;〈xF,xE〉;〈x2,x1〉;〈x3,xF〉;〈xA,xC〉;〈x4,x6〉;〈xB,xC〉;〈xF,x8〉 ]. + +ndefinition dTest_random_ex23 ≝ +[〈xD,x3〉;〈xE,xB〉;〈xF,xC〉;〈x9,xF〉;〈xE,x7〉;〈x6,x1〉;〈xC,xB〉;〈xB,xF〉;〈x4,xE〉;〈xC,x4〉;〈x9,x7〉;〈x1,xE〉;〈x0,xD〉;〈x7,x9〉;〈x8,x3〉;〈xA,xB〉 +;〈x4,xC〉;〈x2,x6〉;〈x6,x3〉;〈x6,xF〉;〈xE,xE〉;〈x5,x9〉;〈x8,x1〉;〈x0,x2〉;〈x2,xC〉;〈xE,xD〉;〈x6,xF〉;〈x0,x4〉;〈x1,x0〉;〈xE,x0〉;〈xD,xA〉;〈xB,xE〉 ]. + +ndefinition dTest_random_ex24 ≝ +[〈xE,xE〉;〈x5,x7〉;〈xB,x0〉;〈x3,x1〉;〈x4,x1〉;〈xD,xC〉;〈x3,xC〉;〈xC,xC〉;〈x5,x8〉;〈x2,x8〉;〈x2,xC〉;〈x1,xB〉;〈x8,x6〉;〈xD,x6〉;〈xF,x9〉;〈xD,x5〉 +;〈x4,xA〉;〈xE,xA〉;〈x0,xB〉;〈x2,x0〉;〈x2,xC〉;〈x4,x2〉;〈xC,xE〉;〈x4,x5〉;〈x2,xB〉;〈x0,x1〉;〈xA,xA〉;〈xB,x1〉;〈x6,xE〉;〈xB,x7〉;〈xB,x7〉;〈x2,x8〉 ]. + +ndefinition dTest_random_ex25 ≝ +[〈x9,x5〉;〈x1,x9〉;〈xA,x7〉;〈x5,xC〉;〈x4,xE〉;〈x7,xB〉;〈x3,xE〉;〈xD,x3〉;〈x9,x0〉;〈x8,x6〉;〈x7,x1〉;〈x1,x4〉;〈xD,x2〉;〈xD,x4〉;〈xB,x4〉;〈xF,x2〉 +;〈x3,x1〉;〈x2,x8〉;〈x4,x5〉;〈xF,xD〉;〈x7,x8〉;〈x5,xD〉;〈xF,xA〉;〈xF,x3〉;〈x9,x5〉;〈x4,xD〉;〈x3,x1〉;〈xB,x8〉;〈xC,xC〉;〈x2,x1〉;〈x1,x9〉;〈x4,x2〉 ]. + +ndefinition dTest_random_ex26 ≝ +[〈x2,xA〉;〈xF,x2〉;〈xB,xA〉;〈x0,x4〉;〈x9,xF〉;〈x4,x3〉;〈x4,x5〉;〈x1,xC〉;〈x7,x4〉;〈xB,xB〉;〈x7,x0〉;〈x5,xE〉;〈x0,x1〉;〈xA,xC〉;〈x6,xD〉;〈xD,x7〉 +;〈x9,xC〉;〈x9,xD〉;〈x1,xA〉;〈x9,x8〉;〈xB,x1〉;〈xF,xC〉;〈x6,x1〉;〈xA,x3〉;〈x4,x1〉;〈x4,x1〉;〈xA,xF〉;〈x1,xD〉;〈xE,x1〉;〈x3,x2〉;〈x1,x9〉;〈x6,x0〉 ]. + +ndefinition dTest_random_ex27 ≝ +[〈x2,x9〉;〈x9,x7〉;〈x8,x5〉;〈x5,x3〉;〈x5,x3〉;〈x9,x1〉;〈xB,x3〉;〈x9,x4〉;〈xD,x5〉;〈x9,xD〉;〈x4,xC〉;〈x3,x6〉;〈x0,xE〉;〈x8,x4〉;〈xA,x1〉;〈x4,x6〉 +;〈x6,xA〉;〈x1,xF〉;〈xF,x3〉;〈x6,xB〉;〈xB,xE〉;〈x4,xA〉;〈x1,x9〉;〈x7,x5〉;〈xF,xC〉;〈xC,x6〉;〈xE,xA〉;〈x7,xE〉;〈xD,x1〉;〈x3,x3〉;〈x6,x7〉;〈xB,x7〉 ]. + +ndefinition dTest_random_ex28 ≝ +[〈xE,xE〉;〈x5,x9〉;〈xE,x2〉;〈xD,xD〉;〈x2,x2〉;〈x8,xC〉;〈x9,xB〉;〈x3,xE〉;〈x9,x8〉;〈xF,xC〉;〈x1,x3〉;〈xE,x2〉;〈x0,xC〉;〈x4,xE〉;〈x3,x1〉;〈x8,x7〉 +;〈x6,x7〉;〈x6,xA〉;〈x4,xC〉;〈x4,xC〉;〈x7,x2〉;〈x0,x0〉;〈x0,x5〉;〈x1,xF〉;〈xF,x6〉;〈x3,x0〉;〈xE,xE〉;〈xD,xE〉;〈xB,x1〉;〈x4,xC〉;〈xF,x7〉;〈xE,xC〉 ]. + +ndefinition dTest_random_ex29 ≝ +[〈x2,xC〉;〈x4,x0〉;〈x6,xB〉;〈x6,x8〉;〈x9,x0〉;〈x8,x8〉;〈x6,xF〉;〈xB,x3〉;〈x4,x7〉;〈x6,x2〉;〈x9,x2〉;〈x9,xB〉;〈x2,xB〉;〈x3,x2〉;〈x4,x0〉;〈xA,x7〉 +;〈x8,x9〉;〈x4,x0〉;〈x2,x3〉;〈x5,xC〉;〈xF,x9〉;〈x2,x9〉;〈x6,x2〉;〈xA,xE〉;〈x5,xB〉;〈xC,x9〉;〈x2,xC〉;〈x9,x2〉;〈x6,xF〉;〈xF,x5〉;〈xA,x0〉;〈x0,xE〉 ]. + +ndefinition dTest_random_ex2A ≝ +[〈xD,xE〉;〈xF,x9〉;〈x0,x9〉;〈x1,x0〉;〈x3,x9〉;〈x4,x6〉;〈xC,x5〉;〈xE,x2〉;〈x8,x3〉;〈xD,x5〉;〈x8,xE〉;〈x4,x6〉;〈x4,xC〉;〈xA,xC〉;〈x7,xF〉;〈x4,xF〉 +;〈xC,x1〉;〈x4,xF〉;〈x1,xA〉;〈x6,x1〉;〈x9,x6〉;〈x0,xB〉;〈x0,x0〉;〈x6,xF〉;〈x2,x6〉;〈x8,xC〉;〈xE,xE〉;〈x9,x3〉;〈x1,xB〉;〈x9,xE〉;〈xA,x5〉;〈x9,x6〉 ]. + +ndefinition dTest_random_ex2B ≝ +[〈x2,xA〉;〈xE,xB〉;〈x4,x6〉;〈x5,xF〉;〈x3,xC〉;〈xD,x6〉;〈x2,xD〉;〈x9,x4〉;〈x6,xB〉;〈xF,x4〉;〈xD,xA〉;〈x6,x9〉;〈x5,x9〉;〈xA,xC〉;〈xB,xD〉;〈x9,xE〉 +;〈x4,x8〉;〈x0,x2〉;〈xD,xC〉;〈x5,xC〉;〈x6,x0〉;〈x2,xA〉;〈x6,xE〉;〈xC,xA〉;〈x6,xE〉;〈x1,xF〉;〈xD,x4〉;〈x3,xA〉;〈xB,x0〉;〈x9,xE〉;〈x8,xF〉;〈xA,xB〉 ]. + +ndefinition dTest_random_ex2C ≝ +[〈xB,x2〉;〈x0,x2〉;〈x4,x7〉;〈x7,xD〉;〈xA,xB〉;〈xD,xB〉;〈xB,x5〉;〈x6,xD〉;〈xE,x2〉;〈x8,x9〉;〈x4,xD〉;〈x0,x4〉;〈xB,xE〉;〈xF,xA〉;〈x2,x2〉;〈x1,x4〉 +;〈x7,x1〉;〈x1,x2〉;〈x1,xB〉;〈x0,xD〉;〈xB,xA〉;〈x5,xA〉;〈x6,xC〉;〈x1,xE〉;〈x3,xA〉;〈x0,xF〉;〈x6,xE〉;〈x4,x4〉;〈xC,x8〉;〈xB,x5〉;〈x8,xC〉;〈x0,x3〉 ]. + +ndefinition dTest_random_ex2D ≝ +[〈x0,x6〉;〈x6,x4〉;〈x8,x5〉;〈x2,x8〉;〈x6,x4〉;〈x2,x2〉;〈x8,x1〉;〈x7,x6〉;〈xF,xE〉;〈xF,xA〉;〈x6,x2〉;〈x9,x1〉;〈xB,xE〉;〈xB,xC〉;〈x6,x1〉;〈x4,xB〉 +;〈x7,xE〉;〈x5,x0〉;〈xB,xC〉;〈xE,xE〉;〈x6,x3〉;〈xC,xF〉;〈x1,xD〉;〈xF,xD〉;〈x6,x2〉;〈x5,xC〉;〈x8,x5〉;〈x9,xE〉;〈xA,x5〉;〈x2,x6〉;〈xE,x7〉;〈x4,x6〉 ]. + +ndefinition dTest_random_ex2E ≝ +[〈x3,xB〉;〈xE,xA〉;〈xB,xE〉;〈x0,x4〉;〈x8,x8〉;〈xF,x2〉;〈x9,x2〉;〈x0,xB〉;〈xD,x9〉;〈xE,x9〉;〈x2,x9〉;〈x3,x8〉;〈x8,x8〉;〈x8,xA〉;〈x6,x9〉;〈x1,x7〉 +;〈x4,xB〉;〈xB,xF〉;〈x0,xC〉;〈xF,x2〉;〈xF,xD〉;〈x7,x3〉;〈x5,x9〉;〈xB,xE〉;〈x5,x4〉;〈x1,xC〉;〈xD,x3〉;〈x3,x1〉;〈x6,x2〉;〈x1,xB〉;〈xB,x7〉;〈x3,x2〉 ]. + +ndefinition dTest_random_ex2F ≝ +[〈xA,x4〉;〈xF,x1〉;〈x7,x0〉;〈x9,xA〉;〈x4,x6〉;〈xA,x1〉;〈x1,xC〉;〈x0,x4〉;〈x6,xC〉;〈xF,x2〉;〈xE,x6〉;〈xC,x1〉;〈xA,x4〉;〈xF,x2〉;〈x2,xA〉;〈x4,xB〉 +;〈x3,x5〉;〈x9,xB〉;〈x9,x9〉;〈xF,xF〉;〈x0,x1〉;〈x1,x3〉;〈xF,x9〉;〈x5,xC〉;〈x3,xC〉;〈x5,x1〉;〈x8,xA〉;〈xA,x5〉;〈x5,xF〉;〈x9,xE〉;〈x5,xE〉;〈xC,x6〉 ]. + +ndefinition dTest_random_ex30 ≝ +[〈x2,x1〉;〈x3,x7〉;〈xD,x2〉;〈xB,x9〉;〈x9,x8〉;〈xA,x1〉;〈x6,x0〉;〈xE,x9〉;〈x4,x5〉;〈xC,xA〉;〈xD,x7〉;〈xB,xD〉;〈xC,xF〉;〈x0,xF〉;〈x2,x4〉;〈xE,x5〉 +;〈x7,x9〉;〈x4,xB〉;〈x1,xC〉;〈x5,x7〉;〈x3,xA〉;〈x2,x4〉;〈x2,x2〉;〈x0,x8〉;〈x3,x3〉;〈xE,x2〉;〈xA,x2〉;〈x5,x8〉;〈x2,x5〉;〈x5,x4〉;〈x7,x1〉;〈x2,xB〉 ]. + +ndefinition dTest_random_ex31 ≝ +[〈xF,xF〉;〈xE,xD〉;〈x4,x8〉;〈xF,x6〉;〈x2,x3〉;〈x3,x1〉;〈xB,xA〉;〈x5,x1〉;〈x9,xF〉;〈xA,xA〉;〈xC,xC〉;〈x0,x3〉;〈x1,x5〉;〈xC,x7〉;〈x2,xD〉;〈xD,x3〉 +;〈xE,xB〉;〈x8,xF〉;〈x8,x4〉;〈x4,x0〉;〈x5,x3〉;〈xA,xD〉;〈x6,x7〉;〈xE,xC〉;〈xA,xF〉;〈xD,xC〉;〈x1,xC〉;〈x7,x4〉;〈x6,xB〉;〈xA,xD〉;〈xC,xD〉;〈xA,x7〉 ]. + +ndefinition dTest_random_ex32 ≝ +[〈x1,x1〉;〈x1,x0〉;〈xC,xF〉;〈xB,xE〉;〈xA,x1〉;〈x0,x1〉;〈x3,xF〉;〈xC,x0〉;〈x8,x5〉;〈x2,x8〉;〈x6,xB〉;〈xC,x3〉;〈x6,xD〉;〈xD,x8〉;〈x7,x5〉;〈x5,xA〉 +;〈xF,x0〉;〈x2,x2〉;〈x4,xB〉;〈x9,xC〉;〈x3,x1〉;〈xE,x4〉;〈xE,x7〉;〈xC,x6〉;〈xF,xC〉;〈x3,x0〉;〈xD,x5〉;〈xF,x9〉;〈x1,xA〉;〈x4,x0〉;〈x1,xF〉;〈x6,xD〉 ]. + +ndefinition dTest_random_ex33 ≝ +[〈xD,x5〉;〈x7,x8〉;〈xB,x5〉;〈x7,x6〉;〈xC,x9〉;〈xE,x1〉;〈xD,xF〉;〈x1,x2〉;〈x6,x1〉;〈xD,xF〉;〈x9,xF〉;〈x5,x7〉;〈x7,xD〉;〈x0,xB〉;〈xA,xD〉;〈x5,xA〉 +;〈xA,x1〉;〈x8,x4〉;〈xE,x5〉;〈xF,x7〉;〈xB,xC〉;〈xD,x3〉;〈xA,x5〉;〈xB,x4〉;〈x8,x5〉;〈x6,x7〉;〈x3,x6〉;〈xF,xC〉;〈xB,x1〉;〈xB,x3〉;〈xC,xB〉;〈x1,xE〉 ]. + +ndefinition dTest_random_ex34 ≝ +[〈xE,xC〉;〈x6,xE〉;〈xE,x1〉;〈x1,xC〉;〈xA,x5〉;〈x5,x3〉;〈x9,x8〉;〈xF,x6〉;〈xD,xF〉;〈x4,x1〉;〈x1,x3〉;〈x2,xE〉;〈x7,xF〉;〈x0,xE〉;〈x3,x8〉;〈x3,xC〉 +;〈xD,x4〉;〈x8,xC〉;〈x2,xA〉;〈x2,x8〉;〈x4,xE〉;〈x7,xE〉;〈x0,xE〉;〈xF,x7〉;〈xC,xA〉;〈x3,xE〉;〈xE,x4〉;〈xB,x4〉;〈x0,x5〉;〈x5,x8〉;〈xD,xC〉;〈x7,x8〉 ]. + +ndefinition dTest_random_ex35 ≝ +[〈xD,x9〉;〈xF,x9〉;〈x7,x9〉;〈x8,x4〉;〈x0,x2〉;〈x3,xF〉;〈xC,xF〉;〈x3,x8〉;〈xD,x7〉;〈x2,x6〉;〈x1,xD〉;〈x1,x8〉;〈x4,xD〉;〈xE,xA〉;〈x7,xA〉;〈xD,x4〉 +;〈x2,x4〉;〈x0,xD〉;〈x4,xD〉;〈x9,x0〉;〈x1,x7〉;〈x1,xE〉;〈x6,xE〉;〈xB,x6〉;〈xC,xC〉;〈xC,x0〉;〈xB,x0〉;〈x5,xE〉;〈x9,x9〉;〈x6,xD〉;〈xC,xF〉;〈xE,xE〉 ]. + +ndefinition dTest_random_ex36 ≝ +[〈x2,x9〉;〈xC,xF〉;〈xA,x2〉;〈x0,xC〉;〈xA,xB〉;〈x7,x4〉;〈x2,x9〉;〈x4,xE〉;〈x8,x2〉;〈x9,x3〉;〈x6,x9〉;〈x7,xB〉;〈xE,xC〉;〈xC,x7〉;〈x8,x9〉;〈xC,xA〉 +;〈xD,xD〉;〈xA,xC〉;〈x6,x5〉;〈x8,x0〉;〈x1,x4〉;〈x0,x9〉;〈x5,x5〉;〈x0,xE〉;〈x8,x4〉;〈x5,xE〉;〈x6,xF〉;〈x3,x4〉;〈x1,x8〉;〈xC,x9〉;〈x8,xB〉;〈xE,x4〉 ]. + +ndefinition dTest_random_ex37 ≝ +[〈x3,xE〉;〈xC,x4〉;〈x1,x6〉;〈xA,x4〉;〈x1,x9〉;〈x3,x4〉;〈x0,xE〉;〈x5,xE〉;〈xF,x9〉;〈x0,x3〉;〈x1,x3〉;〈x7,x2〉;〈x2,x7〉;〈x2,x8〉;〈xA,x7〉;〈x6,xD〉 +;〈xC,x1〉;〈x1,xD〉;〈xF,x0〉;〈x2,x8〉;〈xF,xB〉;〈xF,x6〉;〈x3,x8〉;〈x0,x1〉;〈xF,x9〉;〈xB,xC〉;〈x6,x6〉;〈xF,x8〉;〈x6,xE〉;〈xD,x1〉;〈xB,x5〉;〈x3,x8〉 ]. + +ndefinition dTest_random_ex38 ≝ +[〈x4,x3〉;〈xB,x6〉;〈x6,x8〉;〈xA,xC〉;〈x0,x9〉;〈xF,xD〉;〈x0,x9〉;〈x6,x8〉;〈xE,x0〉;〈x2,x2〉;〈xA,xF〉;〈x4,x0〉;〈x2,x6〉;〈x0,xC〉;〈x5,x2〉;〈xA,x7〉 +;〈xA,xD〉;〈xC,x3〉;〈x8,x2〉;〈xD,xC〉;〈x3,xC〉;〈x6,x5〉;〈xF,x2〉;〈xE,x8〉;〈xC,x0〉;〈x0,x6〉;〈x6,x4〉;〈xB,x1〉;〈x2,x0〉;〈x9,x5〉;〈x2,x2〉;〈xD,xD〉 ]. + +ndefinition dTest_random_ex39 ≝ +[〈xA,xD〉;〈xF,xF〉;〈x1,xB〉;〈x8,xB〉;〈xB,x6〉;〈x4,xA〉;〈xB,xB〉;〈x9,x8〉;〈x1,xA〉;〈xE,xC〉;〈x7,xB〉;〈xA,x6〉;〈x2,xC〉;〈xE,x1〉;〈xC,x7〉;〈xD,xC〉 +;〈x1,x9〉;〈x0,x6〉;〈x0,xA〉;〈x9,xF〉;〈x5,x2〉;〈x2,xB〉;〈xC,xA〉;〈x2,xF〉;〈x4,x0〉;〈xF,x8〉;〈xE,xA〉;〈x8,x7〉;〈x8,x9〉;〈xF,xD〉;〈x5,xD〉;〈x0,x0〉 ]. + +ndefinition dTest_random_ex3A ≝ +[〈x6,xE〉;〈x0,x0〉;〈x0,xD〉;〈x3,x0〉;〈x4,x3〉;〈x5,xA〉;〈x8,xF〉;〈x8,xA〉;〈xA,x4〉;〈x5,x0〉;〈x8,xF〉;〈x0,xC〉;〈x7,x7〉;〈xF,x2〉;〈x6,x5〉;〈xE,x4〉 +;〈x2,xD〉;〈xE,x5〉;〈xA,x8〉;〈x7,xF〉;〈x7,x8〉;〈xE,x3〉;〈x9,x5〉;〈xD,xA〉;〈x0,x7〉;〈x2,x9〉;〈x5,x1〉;〈x9,x4〉;〈xE,x4〉;〈x0,x1〉;〈xB,xF〉;〈x6,xE〉 ]. + +ndefinition dTest_random_ex3B ≝ +[〈x9,x8〉;〈x9,xC〉;〈x9,x0〉;〈xA,x8〉;〈x0,xA〉;〈x3,xD〉;〈x3,xC〉;〈x5,x0〉;〈xE,xB〉;〈x1,x2〉;〈xC,x4〉;〈x5,xF〉;〈x4,x7〉;〈x7,xB〉;〈x2,xC〉;〈xD,xF〉 +;〈x7,x8〉;〈x1,x3〉;〈x7,x4〉;〈xE,x0〉;〈x7,xB〉;〈x7,x1〉;〈x4,x7〉;〈x4,x8〉;〈x1,xB〉;〈xE,x3〉;〈x6,xB〉;〈x0,xB〉;〈x4,xB〉;〈x5,x9〉;〈x9,x3〉;〈xD,xF〉 ]. + +ndefinition dTest_random_ex3C ≝ +[〈xE,x1〉;〈x1,xB〉;〈xD,x0〉;〈xE,xD〉;〈x4,x7〉;〈x4,xD〉;〈xC,x2〉;〈xD,xE〉;〈x5,xC〉;〈xD,xA〉;〈x9,x5〉;〈xC,x8〉;〈x1,x0〉;〈x7,x7〉;〈x7,xF〉;〈xC,x0〉 +;〈xA,x7〉;〈xD,x3〉;〈xD,x3〉;〈xD,x8〉;〈x3,x4〉;〈xA,x1〉;〈x1,x5〉;〈xE,x0〉;〈x0,x4〉;〈x1,xE〉;〈x8,x2〉;〈xC,xA〉;〈xD,x9〉;〈x1,x1〉;〈xB,x1〉;〈xC,x9〉 ]. + +ndefinition dTest_random_ex3D ≝ +[〈x4,xC〉;〈x4,xB〉;〈x0,x9〉;〈x4,x8〉;〈xF,xC〉;〈xD,xD〉;〈x6,xE〉;〈xC,xA〉;〈x7,x6〉;〈xA,xE〉;〈x8,xE〉;〈x3,xB〉;〈xF,xB〉;〈x6,x5〉;〈x8,x3〉;〈x1,xD〉 +;〈xD,xB〉;〈xA,xE〉;〈x4,xF〉;〈xC,x6〉;〈x1,xE〉;〈xC,x5〉;〈xC,xC〉;〈x7,xC〉;〈x2,x8〉;〈xF,x9〉;〈xD,x2〉;〈x8,x6〉;〈x1,x5〉;〈xF,xA〉;〈x4,x1〉;〈x4,x5〉 ]. + +ndefinition dTest_random_ex3E ≝ +[〈x2,xE〉;〈x9,x5〉;〈xB,xF〉;〈x0,xD〉;〈x8,xB〉;〈x8,xD〉;〈x1,x1〉;〈x9,xC〉;〈xB,x8〉;〈xF,xB〉;〈x2,x6〉;〈xD,x6〉;〈x9,x1〉;〈x0,xD〉;〈xC,xD〉;〈x0,x7〉 +;〈x5,x0〉;〈xF,xA〉;〈x2,x9〉;〈x3,xF〉;〈x0,xC〉;〈x2,xB〉;〈xF,xE〉;〈x9,x7〉;〈x5,x5〉;〈x5,xA〉;〈x6,xD〉;〈x9,x6〉;〈x0,x5〉;〈x0,x9〉;〈x4,x5〉;〈xE,xF〉 ]. + +ndefinition dTest_random_ex3F ≝ +[〈x0,xF〉;〈x7,x4〉;〈x9,x3〉;〈x6,xC〉;〈x8,x2〉;〈x3,x7〉;〈xE,xB〉;〈x5,x0〉;〈xF,x5〉;〈xC,x4〉;〈x0,xB〉;〈x3,x8〉;〈x2,xD〉;〈x8,xA〉;〈x9,x3〉;〈x6,xD〉 +;〈x1,xD〉;〈xE,x5〉;〈xF,x7〉;〈xE,x7〉;〈xD,x7〉;〈x5,xC〉;〈xB,x4〉;〈x5,x0〉;〈x7,x5〉;〈x0,xD〉;〈xF,x3〉;〈xC,xE〉;〈x3,x1〉;〈xF,x1〉;〈x8,xE〉;〈x8,xF〉 ]. + +ndefinition dTest_random_ex40 ≝ +[〈xD,xB〉;〈x1,x4〉;〈xF,x6〉;〈x0,x3〉;〈xA,xB〉;〈xA,xE〉;〈xB,xC〉;〈xE,xB〉;〈xC,x8〉;〈x6,x7〉;〈xC,xC〉;〈xF,xF〉;〈x4,xF〉;〈xC,x6〉;〈x2,x9〉;〈x9,x5〉 +;〈xB,xC〉;〈x6,x5〉;〈x5,x2〉;〈xF,x2〉;〈x3,x5〉;〈xC,x4〉;〈xF,x4〉;〈x9,xB〉;〈x4,x5〉;〈x1,xC〉;〈xD,xB〉;〈x6,x1〉;〈xF,xE〉;〈x3,xF〉;〈xB,x9〉;〈xD,x8〉 ]. + +ndefinition dTest_random_ex41 ≝ +[〈xF,x1〉;〈xA,xC〉;〈x0,x7〉;〈xA,x4〉;〈xB,x8〉;〈x8,x8〉;〈x9,x5〉;〈xB,x8〉;〈x5,x6〉;〈x3,x2〉;〈x5,xA〉;〈x3,xE〉;〈x2,x2〉;〈x0,xB〉;〈x9,x6〉;〈xE,xE〉 +;〈x6,xF〉;〈x1,xE〉;〈x3,x2〉;〈x4,x9〉;〈x4,xF〉;〈xC,xC〉;〈xD,xB〉;〈x5,x1〉;〈x4,xD〉;〈xD,x1〉;〈x4,xF〉;〈x0,x9〉;〈x5,xA〉;〈xA,xC〉;〈xE,x7〉;〈x8,x6〉 ]. + +ndefinition dTest_random_ex42 ≝ +[〈x5,x8〉;〈xA,x5〉;〈xA,x7〉;〈x5,xE〉;〈x3,x6〉;〈x1,x1〉;〈x3,xA〉;〈x8,x9〉;〈x8,x2〉;〈xD,xC〉;〈x6,x2〉;〈x0,xE〉;〈xA,xB〉;〈x2,xB〉;〈x2,x5〉;〈xF,x9〉 +;〈x7,x7〉;〈x8,x6〉;〈x1,xD〉;〈x7,x9〉;〈x5,x1〉;〈xB,xD〉;〈x9,x8〉;〈xB,x7〉;〈xB,xB〉;〈xF,x6〉;〈xD,x9〉;〈x6,x6〉;〈x0,x1〉;〈x1,x2〉;〈xE,xB〉;〈x0,xA〉 ]. + +ndefinition dTest_random_ex43 ≝ +[〈xC,xD〉;〈x1,xA〉;〈xA,xA〉;〈xC,xC〉;〈x6,x5〉;〈x4,x2〉;〈x8,xF〉;〈x2,xA〉;〈x4,x8〉;〈xC,x6〉;〈xB,xA〉;〈xD,x8〉;〈x2,xD〉;〈x2,x9〉;〈xE,x8〉;〈x5,x7〉 +;〈x7,x7〉;〈x7,xA〉;〈xB,x4〉;〈x4,x9〉;〈x6,x5〉;〈x4,x3〉;〈x5,x7〉;〈xF,xE〉;〈xC,x6〉;〈xC,x7〉;〈x6,x2〉;〈x6,x7〉;〈x5,x8〉;〈xD,x6〉;〈x9,xA〉;〈xC,x8〉 ]. + +ndefinition dTest_random_ex44 ≝ +[〈xE,x8〉;〈x3,x0〉;〈x6,x0〉;〈x7,x3〉;〈x8,x9〉;〈x2,x3〉;〈x0,x8〉;〈x7,xA〉;〈xA,xC〉;〈x5,xD〉;〈x6,xD〉;〈xC,xE〉;〈x0,xC〉;〈x1,xB〉;〈x1,x7〉;〈xC,x1〉 +;〈x4,x2〉;〈x5,x3〉;〈x1,x5〉;〈x7,xC〉;〈x7,x4〉;〈x2,xB〉;〈x2,x5〉;〈x5,x6〉;〈x6,x1〉;〈xE,xC〉;〈x0,xB〉;〈x4,x2〉;〈x0,x4〉;〈xC,xA〉;〈x0,x9〉;〈xA,xB〉 ]. + +ndefinition dTest_random_ex45 ≝ +[〈x1,xB〉;〈xD,x0〉;〈x9,xF〉;〈x6,xA〉;〈x7,xF〉;〈x4,x1〉;〈xF,x8〉;〈xE,xA〉;〈x8,x2〉;〈x8,x1〉;〈x4,x1〉;〈xC,xE〉;〈xC,xE〉;〈x0,xD〉;〈x2,xB〉;〈x3,x3〉 +;〈xA,x3〉;〈x6,x4〉;〈xF,xA〉;〈xA,x6〉;〈x3,x9〉;〈x7,xF〉;〈xF,x6〉;〈xB,x2〉;〈x5,x5〉;〈x6,xB〉;〈xA,xC〉;〈x3,x3〉;〈x9,x3〉;〈xE,x7〉;〈xB,xE〉;〈x3,x4〉 ]. + +ndefinition dTest_random_ex46 ≝ +[〈xC,xF〉;〈xE,xF〉;〈xA,x2〉;〈xE,xE〉;〈xE,xD〉;〈xC,xB〉;〈xB,x0〉;〈x8,x9〉;〈xD,xA〉;〈x3,xB〉;〈xB,xE〉;〈x3,xE〉;〈x3,x3〉;〈x5,x1〉;〈xA,x5〉;〈x3,xC〉 +;〈xC,xC〉;〈xA,x0〉;〈xF,xD〉;〈x3,x9〉;〈xC,xB〉;〈xF,xC〉;〈x1,xF〉;〈x8,xD〉;〈x6,x8〉;〈xD,x4〉;〈x8,xC〉;〈xA,xA〉;〈x8,xE〉;〈x3,xA〉;〈x9,x7〉;〈x2,x6〉 ]. + +ndefinition dTest_random_ex47 ≝ +[〈x6,xB〉;〈xA,xC〉;〈x8,xA〉;〈x4,xB〉;〈x7,x4〉;〈x3,xF〉;〈xB,x7〉;〈xB,xF〉;〈x0,xC〉;〈xE,x6〉;〈xC,xD〉;〈x4,x2〉;〈xF,xA〉;〈xE,xE〉;〈xF,x9〉;〈x0,xC〉 +;〈x2,xC〉;〈x7,x9〉;〈x7,xE〉;〈xD,x8〉;〈x4,x0〉;〈x7,xC〉;〈x3,x8〉;〈x4,x9〉;〈x7,x1〉;〈x7,x5〉;〈xB,x7〉;〈x3,x6〉;〈x0,x7〉;〈x1,xA〉;〈x2,xC〉;〈x1,xE〉 ]. + +ndefinition dTest_random_ex48 ≝ +[〈x3,xC〉;〈x7,xA〉;〈x3,x8〉;〈x4,xA〉;〈x3,x4〉;〈x2,x0〉;〈x9,x5〉;〈x6,x0〉;〈xF,x7〉;〈xC,x3〉;〈xB,x1〉;〈x6,xE〉;〈xB,x1〉;〈x7,x0〉;〈x7,x4〉;〈x3,xB〉 +;〈x0,xD〉;〈x6,xD〉;〈xF,xB〉;〈xE,x5〉;〈xE,x2〉;〈x6,x6〉;〈x6,x8〉;〈x0,x8〉;〈xF,xB〉;〈x3,xC〉;〈x8,xC〉;〈xD,xD〉;〈x0,x2〉;〈x2,xE〉;〈x6,xE〉;〈xF,x1〉 ]. + +ndefinition dTest_random_ex49 ≝ +[〈xA,xF〉;〈x7,x9〉;〈x6,x7〉;〈xE,x2〉;〈x4,xC〉;〈xA,x5〉;〈x7,x9〉;〈xC,x6〉;〈xB,x5〉;〈xA,xF〉;〈x1,x5〉;〈xF,xE〉;〈xE,x2〉;〈x2,xB〉;〈xC,xA〉;〈xE,x6〉 +;〈x3,xE〉;〈x2,xC〉;〈x5,x8〉;〈x7,x2〉;〈xC,xE〉;〈x7,x1〉;〈x8,xC〉;〈xB,xE〉;〈x2,x0〉;〈x6,x6〉;〈x0,x7〉;〈x6,xF〉;〈xD,x1〉;〈x8,x2〉;〈x3,x1〉;〈xF,x3〉 ]. + +ndefinition dTest_random_ex4A ≝ +[〈x9,x5〉;〈x9,x1〉;〈x1,x2〉;〈xF,x3〉;〈x4,xF〉;〈x6,xC〉;〈xA,x6〉;〈x8,xE〉;〈xB,x2〉;〈x7,x8〉;〈xD,xE〉;〈x7,x9〉;〈xC,x5〉;〈x2,x2〉;〈xF,x3〉;〈x0,x7〉 +;〈xE,x7〉;〈x9,xE〉;〈x9,x2〉;〈x7,x3〉;〈x3,xC〉;〈xA,x1〉;〈xD,xA〉;〈x2,x1〉;〈x2,x3〉;〈x4,x5〉;〈xE,x5〉;〈x7,x4〉;〈x8,x4〉;〈xC,x2〉;〈x6,x8〉;〈x3,x5〉 ]. + +ndefinition dTest_random_ex4B ≝ +[〈x9,xA〉;〈xC,x8〉;〈x2,xE〉;〈x1,xD〉;〈xD,x1〉;〈xA,x6〉;〈xD,xF〉;〈x0,x6〉;〈x7,xF〉;〈x8,xC〉;〈x2,x8〉;〈xF,x6〉;〈xC,x3〉;〈xF,x8〉;〈x6,x2〉;〈xF,x9〉 +;〈x5,x7〉;〈x2,x7〉;〈xD,x1〉;〈xD,x3〉;〈x0,xB〉;〈xA,x3〉;〈x8,x7〉;〈x8,x3〉;〈xC,x9〉;〈x1,x4〉;〈xB,x4〉;〈xC,x5〉;〈xE,xD〉;〈x5,x4〉;〈xE,x1〉;〈xB,x9〉 ]. + +ndefinition dTest_random_ex4C ≝ +[〈x2,x9〉;〈x6,xF〉;〈xE,x3〉;〈x0,xD〉;〈xC,xC〉;〈xF,x6〉;〈x0,xD〉;〈x2,x4〉;〈x4,x5〉;〈x6,xE〉;〈xE,x4〉;〈xD,xB〉;〈xF,x9〉;〈xC,x1〉;〈xD,x4〉;〈xB,x4〉 +;〈xB,x5〉;〈x6,x6〉;〈x1,xC〉;〈x6,xE〉;〈xA,xF〉;〈x4,x0〉;〈xE,x6〉;〈x4,x9〉;〈x7,xE〉;〈x4,x1〉;〈x1,x8〉;〈x8,x7〉;〈xD,xF〉;〈xB,xB〉;〈x6,x0〉;〈x0,x5〉 ]. + +ndefinition dTest_random_ex4D ≝ +[〈xF,x4〉;〈x5,xD〉;〈xA,x1〉;〈xD,x6〉;〈x6,x7〉;〈x2,xA〉;〈xC,x8〉;〈x7,x7〉;〈xF,x9〉;〈x8,xA〉;〈xF,x9〉;〈x2,x6〉;〈xE,xF〉;〈x7,x4〉;〈x5,x8〉;〈x6,xA〉 +;〈xC,x8〉;〈x3,x5〉;〈x1,x0〉;〈xC,x5〉;〈x1,xE〉;〈x0,xB〉;〈x8,x3〉;〈x6,xA〉;〈x4,x4〉;〈x8,xD〉;〈x5,xC〉;〈xF,xB〉;〈xF,xE〉;〈x9,x2〉;〈x0,x3〉;〈x4,x3〉 ]. + +ndefinition dTest_random_ex4E ≝ +[〈x0,x5〉;〈xA,xF〉;〈xC,x0〉;〈xF,x3〉;〈x0,x4〉;〈x2,x8〉;〈x9,xD〉;〈x0,x9〉;〈x3,x5〉;〈xE,x3〉;〈x5,xF〉;〈x4,x5〉;〈xA,xB〉;〈xC,xD〉;〈x8,xC〉;〈xF,xD〉 +;〈x2,xC〉;〈x9,xD〉;〈xA,xF〉;〈x6,x4〉;〈x4,x3〉;〈x8,x0〉;〈x8,x2〉;〈xE,x5〉;〈x8,xE〉;〈x3,xD〉;〈x2,xD〉;〈xD,xB〉;〈xD,xF〉;〈xA,xB〉;〈x0,x8〉;〈x1,x6〉 ]. + +ndefinition dTest_random_ex4F ≝ +[〈xE,xC〉;〈x7,xE〉;〈xA,x7〉;〈xC,xB〉;〈xD,x8〉;〈x5,xC〉;〈x2,xC〉;〈x8,x8〉;〈x9,x8〉;〈xC,x2〉;〈xA,xD〉;〈x1,xD〉;〈xB,x0〉;〈xB,x1〉;〈xC,xE〉;〈x9,x3〉 +;〈xE,x2〉;〈xF,x4〉;〈xD,xB〉;〈xA,x5〉;〈xB,x6〉;〈x4,x9〉;〈x8,x7〉;〈x1,xD〉;〈xA,x2〉;〈x7,x9〉;〈x3,x5〉;〈xB,xE〉;〈x5,x5〉;〈xC,xD〉;〈x6,x3〉;〈x2,xC〉 ]. + +ndefinition dTest_random_ex50 ≝ +[〈x1,x0〉;〈x1,xF〉;〈xE,xC〉;〈x3,xB〉;〈x8,xA〉;〈x3,xF〉;〈x3,x8〉;〈x8,x0〉;〈x1,xC〉;〈x2,xD〉;〈x9,x2〉;〈x5,xF〉;〈xE,x1〉;〈xB,x5〉;〈xB,xC〉;〈x8,x3〉 +;〈xB,x6〉;〈x1,xB〉;〈xE,xD〉;〈x4,xF〉;〈x3,xA〉;〈xC,x4〉;〈xF,xE〉;〈xF,xF〉;〈xC,xB〉;〈x8,x1〉;〈x6,x7〉;〈xC,x2〉;〈x5,x9〉;〈xD,xA〉;〈x0,xA〉;〈x9,xC〉 ]. + +ndefinition dTest_random_ex51 ≝ +[〈x2,x2〉;〈xE,xB〉;〈x9,x3〉;〈xE,x2〉;〈x7,xF〉;〈xA,xC〉;〈x4,xA〉;〈x8,x2〉;〈x8,x1〉;〈x3,xF〉;〈xE,xB〉;〈x8,xB〉;〈x0,xF〉;〈x9,xC〉;〈x4,x1〉;〈x8,x2〉 +;〈x9,xB〉;〈x7,xC〉;〈x5,x1〉;〈xA,x7〉;〈xA,xB〉;〈xA,xD〉;〈x9,x2〉;〈x1,x9〉;〈xF,x0〉;〈xF,xD〉;〈x9,x3〉;〈xF,x6〉;〈xA,xD〉;〈x2,x4〉;〈xC,xB〉;〈xD,xE〉 ]. + +ndefinition dTest_random_ex52 ≝ +[〈xB,x5〉;〈xA,xB〉;〈x8,x1〉;〈x5,x4〉;〈xA,xE〉;〈x2,x4〉;〈x6,x4〉;〈xD,x2〉;〈xD,x0〉;〈xF,xE〉;〈x3,x3〉;〈x2,xA〉;〈x7,x5〉;〈x0,x7〉;〈x8,xF〉;〈x3,xA〉 +;〈x1,x2〉;〈x9,xF〉;〈xB,xE〉;〈x1,xB〉;〈x1,xB〉;〈x1,xF〉;〈xC,x7〉;〈xF,x1〉;〈x7,xC〉;〈x9,x1〉;〈x5,xD〉;〈x3,x2〉;〈xD,x9〉;〈xD,x6〉;〈xE,xA〉;〈x0,x6〉 ]. + +ndefinition dTest_random_ex53 ≝ +[〈x5,xB〉;〈x6,x9〉;〈x6,xB〉;〈xA,xC〉;〈x0,x9〉;〈x1,x6〉;〈xA,x3〉;〈xC,xA〉;〈x8,xE〉;〈x8,x3〉;〈x3,x4〉;〈xB,x7〉;〈x4,x1〉;〈x2,x7〉;〈xB,x3〉;〈x0,x1〉 +;〈xE,x6〉;〈x0,x6〉;〈x8,xC〉;〈x0,x4〉;〈x3,xD〉;〈xB,xE〉;〈x2,xC〉;〈x6,x6〉;〈xB,x5〉;〈x8,x6〉;〈x1,x1〉;〈x1,x3〉;〈x6,xD〉;〈xD,x0〉;〈xB,xE〉;〈x8,xD〉 ]. + +ndefinition dTest_random_ex54 ≝ +[〈xC,x7〉;〈x5,x5〉;〈x0,x2〉;〈xC,x1〉;〈x7,x6〉;〈x5,xF〉;〈x2,x0〉;〈x5,xE〉;〈xE,x4〉;〈x3,xE〉;〈x7,x7〉;〈xE,x1〉;〈x3,xF〉;〈xE,x8〉;〈x6,xC〉;〈x4,xA〉 +;〈xA,x0〉;〈xF,xE〉;〈xC,xE〉;〈x3,xF〉;〈x6,x7〉;〈x9,x4〉;〈x3,xF〉;〈xE,xF〉;〈xE,xF〉;〈x8,x6〉;〈xD,x9〉;〈x4,xA〉;〈x0,x8〉;〈x8,xB〉;〈xC,x8〉;〈x1,xC〉 ]. + +ndefinition dTest_random_ex55 ≝ +[〈xA,xD〉;〈x2,x0〉;〈xA,x7〉;〈x8,xC〉;〈x0,x6〉;〈x6,x7〉;〈xA,xF〉;〈x7,x3〉;〈xC,xD〉;〈x1,x6〉;〈x8,x4〉;〈x3,x2〉;〈xD,x0〉;〈xF,x3〉;〈xD,xC〉;〈xD,xB〉 +;〈xB,x7〉;〈x2,x4〉;〈x6,xA〉;〈x6,x3〉;〈x1,xC〉;〈xA,x1〉;〈xD,xE〉;〈xB,xC〉;〈x9,x2〉;〈xF,x1〉;〈x5,xC〉;〈xE,x7〉;〈xE,x0〉;〈xD,x5〉;〈xA,x4〉;〈x4,xA〉 ]. + +ndefinition dTest_random_ex56 ≝ +[〈x0,x0〉;〈xD,x6〉;〈x2,x2〉;〈x9,xC〉;〈x5,x2〉;〈x8,xF〉;〈xE,x8〉;〈x2,x2〉;〈xA,x2〉;〈xF,x0〉;〈x9,x8〉;〈x3,x8〉;〈x0,xD〉;〈xF,x6〉;〈x4,x3〉;〈x7,x9〉 +;〈x8,x2〉;〈xA,xF〉;〈xD,x5〉;〈xC,x1〉;〈x8,x2〉;〈x5,x2〉;〈xD,xB〉;〈x8,xF〉;〈x7,xE〉;〈xD,x1〉;〈x9,xD〉;〈xA,x6〉;〈x8,xE〉;〈x9,xE〉;〈xA,x9〉;〈x8,xE〉 ]. + +ndefinition dTest_random_ex57 ≝ +[〈xD,x1〉;〈xF,x6〉;〈xB,x0〉;〈xE,xA〉;〈x8,x3〉;〈xE,x9〉;〈xF,x7〉;〈x3,xB〉;〈x4,xA〉;〈x0,x9〉;〈x1,xE〉;〈x3,x2〉;〈xD,x2〉;〈x5,xD〉;〈xD,x7〉;〈xA,xB〉 +;〈x4,xD〉;〈x6,xF〉;〈x5,x9〉;〈xF,xC〉;〈x4,x3〉;〈x4,x1〉;〈x0,x0〉;〈x3,xC〉;〈x9,x4〉;〈x5,x2〉;〈x5,x9〉;〈x6,xC〉;〈x6,xE〉;〈xE,x8〉;〈x6,x6〉;〈xF,x5〉 ]. + +ndefinition dTest_random_ex58 ≝ +[〈x9,xC〉;〈x5,x7〉;〈x6,xC〉;〈xE,x2〉;〈x3,xB〉;〈xA,x2〉;〈x2,x1〉;〈xE,xE〉;〈xF,x6〉;〈x4,xF〉;〈xF,x3〉;〈x6,x2〉;〈xD,xB〉;〈x8,xF〉;〈x6,x4〉;〈xD,x3〉 +;〈x8,x0〉;〈x6,x9〉;〈x9,x7〉;〈x4,x7〉;〈x8,xB〉;〈xB,x6〉;〈x3,x8〉;〈x4,x5〉;〈xB,xE〉;〈x0,xD〉;〈x6,x1〉;〈xC,xF〉;〈x7,x8〉;〈xC,xF〉;〈x4,x1〉;〈x7,xF〉 ]. + +ndefinition dTest_random_ex59 ≝ +[〈xF,x4〉;〈x5,xA〉;〈x8,xB〉;〈x7,x2〉;〈xE,x6〉;〈x7,xD〉;〈x4,xC〉;〈x1,x8〉;〈xE,xE〉;〈x3,xA〉;〈x1,x2〉;〈x9,x4〉;〈x3,x4〉;〈x3,x0〉;〈x3,x9〉;〈x0,x0〉 +;〈x9,x5〉;〈x6,x0〉;〈xF,xA〉;〈x7,xF〉;〈xA,x6〉;〈xC,x7〉;〈xB,x1〉;〈x7,xE〉;〈x0,xD〉;〈x2,x4〉;〈xF,xF〉;〈x4,x3〉;〈x7,x8〉;〈x8,x8〉;〈x6,xC〉;〈x0,x7〉 ]. + +ndefinition dTest_random_ex5A ≝ +[〈x7,x3〉;〈x9,x2〉;〈xC,x8〉;〈x0,xB〉;〈x5,x0〉;〈x9,x7〉;〈xF,x4〉;〈x1,xB〉;〈xD,xB〉;〈x4,x5〉;〈x6,x2〉;〈x9,x1〉;〈x8,x7〉;〈x5,xD〉;〈xF,x5〉;〈x6,x1〉 +;〈x3,x8〉;〈xF,x3〉;〈x8,xA〉;〈x4,xF〉;〈xD,xB〉;〈x3,xD〉;〈x4,x3〉;〈x2,xF〉;〈xB,xA〉;〈xA,x9〉;〈xB,x4〉;〈xA,x9〉;〈x2,x6〉;〈x7,xE〉;〈x8,xC〉;〈x1,x6〉 ]. + +ndefinition dTest_random_ex5B ≝ +[〈xF,xC〉;〈x1,xC〉;〈xA,x7〉;〈x9,xD〉;〈x7,xC〉;〈x8,x5〉;〈xA,x7〉;〈x3,x5〉;〈x8,x6〉;〈x4,xF〉;〈xC,x8〉;〈x9,xA〉;〈x0,xD〉;〈x2,x4〉;〈x0,x4〉;〈x5,x8〉 +;〈x4,x2〉;〈x3,x0〉;〈x7,x5〉;〈x8,xD〉;〈xB,xC〉;〈x7,x2〉;〈x3,x4〉;〈xF,x9〉;〈x4,x6〉;〈x5,xE〉;〈xF,x4〉;〈x5,xC〉;〈x6,x7〉;〈x0,x4〉;〈x8,x8〉;〈x2,x8〉 ]. + +ndefinition dTest_random_ex5C ≝ +[〈xA,x9〉;〈xE,xC〉;〈xE,xC〉;〈x7,xC〉;〈x4,x6〉;〈x6,xE〉;〈x1,xC〉;〈xD,x9〉;〈xC,x0〉;〈x6,x1〉;〈x5,x8〉;〈x5,xE〉;〈x3,x7〉;〈xB,x0〉;〈x9,x9〉;〈x9,x7〉 +;〈xA,x0〉;〈x9,xB〉;〈x7,x7〉;〈x4,xA〉;〈xD,x0〉;〈xB,x5〉;〈x1,xD〉;〈xA,x6〉;〈x4,xA〉;〈xC,x5〉;〈x3,xA〉;〈x9,x4〉;〈xB,x4〉;〈x5,x0〉;〈x0,x6〉;〈xC,x0〉 ]. + +ndefinition dTest_random_ex5D ≝ +[〈xA,x8〉;〈x0,x2〉;〈x5,xF〉;〈x0,xE〉;〈x2,x1〉;〈x0,x3〉;〈xB,x1〉;〈x9,x6〉;〈x0,x2〉;〈x9,x7〉;〈x8,x0〉;〈x1,xA〉;〈x0,xB〉;〈x3,xD〉;〈x2,x1〉;〈x7,xF〉 +;〈x0,x3〉;〈x2,x9〉;〈x3,x2〉;〈x6,x6〉;〈xB,xF〉;〈x3,xB〉;〈x5,x7〉;〈x5,x3〉;〈xE,x7〉;〈xD,x5〉;〈xE,x5〉;〈x4,x5〉;〈xA,x3〉;〈x1,xA〉;〈x1,xB〉;〈xF,x8〉 ]. + +ndefinition dTest_random_ex5E ≝ +[〈xC,xF〉;〈xB,x3〉;〈x9,x5〉;〈x5,x9〉;〈x4,xE〉;〈x6,x4〉;〈x4,x3〉;〈xF,x4〉;〈x2,x5〉;〈xC,xC〉;〈x6,x1〉;〈x3,x5〉;〈xD,xF〉;〈x3,x6〉;〈x5,x5〉;〈xC,xF〉 +;〈x9,xA〉;〈x1,x1〉;〈xF,x6〉;〈xD,x4〉;〈x4,xF〉;〈x9,xB〉;〈xA,xF〉;〈xF,x2〉;〈x0,x3〉;〈x1,x9〉;〈x9,xB〉;〈xA,xB〉;〈xC,x4〉;〈x1,x9〉;〈xA,x1〉;〈xE,xA〉 ]. + +ndefinition dTest_random_ex5F ≝ +[〈x1,xB〉;〈x2,x5〉;〈xA,xD〉;〈xA,xA〉;〈x0,x0〉;〈x5,xB〉;〈x9,xD〉;〈x6,xF〉;〈x8,x8〉;〈x6,xF〉;〈x3,x0〉;〈x8,x5〉;〈xC,x6〉;〈x1,x7〉;〈x5,x7〉;〈x1,x1〉 +;〈xA,xB〉;〈x0,x2〉;〈xD,xD〉;〈x9,x2〉;〈x4,xD〉;〈x8,x2〉;〈x0,x2〉;〈x3,x5〉;〈xC,xB〉;〈x4,x4〉;〈xA,x4〉;〈x4,x1〉;〈xD,x5〉;〈x1,x2〉;〈xE,x7〉;〈x4,xD〉 ]. + +ndefinition dTest_random_32 ≝ + dTest_random_ex00. + +ndefinition dTest_random_64 ≝ + dTest_random_32@dTest_random_ex01. + +ndefinition dTest_random_128 ≝ + dTest_random_64@dTest_random_ex02@dTest_random_ex03. + +ndefinition dTest_random_256 ≝ + dTest_random_128@ + dTest_random_ex04@dTest_random_ex05@dTest_random_ex06@dTest_random_ex07. + +ndefinition dTest_random_512 ≝ + dTest_random_256@ + dTest_random_ex08@dTest_random_ex09@dTest_random_ex0A@dTest_random_ex0B@ + dTest_random_ex0C@dTest_random_ex0D@dTest_random_ex0E@dTest_random_ex0F. + +ndefinition dTest_random_1024 ≝ + dTest_random_512@ + dTest_random_ex10@dTest_random_ex11@dTest_random_ex12@dTest_random_ex13@ + dTest_random_ex14@dTest_random_ex15@dTest_random_ex16@dTest_random_ex17@ + dTest_random_ex18@dTest_random_ex19@dTest_random_ex1A@dTest_random_ex1B@ + dTest_random_ex1C@dTest_random_ex1D@dTest_random_ex1E@dTest_random_ex1F. + +ndefinition dTest_random_2048 ≝ + dTest_random_1024@ + dTest_random_ex20@dTest_random_ex21@dTest_random_ex22@dTest_random_ex23@ + dTest_random_ex24@dTest_random_ex25@dTest_random_ex26@dTest_random_ex27@ + dTest_random_ex28@dTest_random_ex29@dTest_random_ex2A@dTest_random_ex2B@ + dTest_random_ex2C@dTest_random_ex2D@dTest_random_ex2E@dTest_random_ex2F@ + dTest_random_ex30@dTest_random_ex31@dTest_random_ex32@dTest_random_ex33@ + dTest_random_ex34@dTest_random_ex35@dTest_random_ex36@dTest_random_ex37@ + dTest_random_ex38@dTest_random_ex39@dTest_random_ex3A@dTest_random_ex3B@ + dTest_random_ex3C@dTest_random_ex3D@dTest_random_ex3E@dTest_random_ex3F. + +ndefinition dTest_random_3072 ≝ + dTest_random_2048@ + dTest_random_ex40@dTest_random_ex41@dTest_random_ex42@dTest_random_ex43@ + dTest_random_ex44@dTest_random_ex45@dTest_random_ex46@dTest_random_ex47@ + dTest_random_ex48@dTest_random_ex49@dTest_random_ex4A@dTest_random_ex4B@ + dTest_random_ex4C@dTest_random_ex4D@dTest_random_ex4E@dTest_random_ex4F@ + dTest_random_ex50@dTest_random_ex51@dTest_random_ex52@dTest_random_ex53@ + dTest_random_ex54@dTest_random_ex55@dTest_random_ex56@dTest_random_ex57@ + dTest_random_ex58@dTest_random_ex59@dTest_random_ex5A@dTest_random_ex5B@ + dTest_random_ex5C@dTest_random_ex5D@dTest_random_ex5E@dTest_random_ex5F. + +(* campitura di 128 0x00 *) +ndefinition dTest_bytes_aux : list byte8 ≝ +[ +〈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〉; +〈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〉; +〈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〉; +〈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〉 +]. + +(* blocco di 0x00 lungo 0x0380 da caricare dopo dati per azzerare + counters, index, position, e stack di esecuzione *) +ndefinition 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. + +ndefinition 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/contribs/ng_assembly/emulator/tests/micro_tests1.ma b/helm/software/matita/contribs/ng_assembly/emulator/tests/micro_tests1.ma new file mode 100755 index 000000000..96a546aa5 --- /dev/null +++ b/helm/software/matita/contribs/ng_assembly/emulator/tests/micro_tests1.ma @@ -0,0 +1,141 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +(* ********************************************************************** *) +(* Progetto FreeScale *) +(* *) +(* Sviluppato da: Ing. Cosimo Oliboni, oliboni@cs.unibo.it *) +(* Sviluppo: 2008-2010 *) +(* *) +(* ********************************************************************** *) + +include "emulator/tests/micro_tests_tools.ma". +include "emulator/multivm/multivm.ma". +include "emulator/status/status_lemmas.ma". +include "emulator/model/model.ma". + +(* ****************************************** *) +(* MICRO TEST DI CORRETTEZZA DELLE ISTRUZIONI *) +(* ****************************************** *) + +(* ********* *) +(* HCS08 ADC *) +(* ********* *) + +ndefinition mTest_HCS08_ADC_source ≝ source_to_byte8 HCS08 ( +(* testa la logica di ADC e le modalita' IMM1,DIR1/2,IX0/1/2,SP1/2 *) +(* BEFORE: A=0x00 H:X=0xFF50 PC=0x1860 SP=0x0110 C=true *) +(* [0x1860] 2clk *) (compile HCS08 ? ADC (maIMM1 〈xA,xA〉) ?) @ (* AFTER1: imm1=0xAA quindi 0x00+imm1+true=A:0xAB C:false *) +(* [0x1862] 3clk *) (compile HCS08 ? ADC (maDIR1 〈xF,xF〉) ?) @ (* AFTER2: dir1=[0x00FF]=0x8F quindi 0xAB+dir1+false=A:0x3A C:true *) +(* [0x1864] 4clk *) (compile HCS08 ? ADC (maDIR2 〈〈xF,xF〉:〈x1,x1〉〉) ?) @ (* AFTER3: dir2=[0xFF11]=0x11 quindi 0x3A+dir2+true=A:0x4C C:false *) +(* [0x1867] 4clk *) (compile HCS08 ? ADC (maIX2 〈〈xF,xF〉:〈xF,x0〉〉) ?) @ (* AFTER4: ix2=[X+0xFFF0]=[0xFF40]=0x40 quindi 0x4C+ix2+false=A:0x8C C:false *) +(* [0x186A] 3clk *) (compile HCS08 ? ADC (maIX1 〈x2,x4〉) ?) @ (* AFTER5: ix1=[X+0x0024]=[0xFF74]=0x74 quindi 0x8C+ix1+false=A:0x00 C:true *) +(* [0x186C] 3clk *) (compile HCS08 ? ADC maIX0 ?) @ (* AFTER6: ix0=[X]=[0xFF50]=0x50 quindi 0x00+ix0+true=A:0x51 C:false *) +(* [0x186D] 5clk *) (compile HCS08 ? ADC (maSP2 〈〈xF,xF〉:〈x6,x1〉〉) ?) @ (* AFTER7: sp2=[SP+0xFF61]=[0x0071]=0x01 quindi 0x51+sp2+false=A:0x52 C:false *) +(* [0x1871] 4clk *) (compile HCS08 ? ADC (maSP1 〈x2,x4〉) ?) (* AFTER8: sp1=[SP+0x0024]=[0x0134]=0xC4 quindi 0x52+sp1+false=A:0x16 C:true *) +(* [0x1874] si puo' quindi enunciare che dopo 2+3+4+4+3+3+5+4=28 clk *) +(* A<-0x16 PC<-0x1874 *) +). napply I. nqed. + +(* creazione del processore+caricamento+impostazione registri *) +ndefinition mTest_HCS08_ADC_status ≝ +λt:memory_impl. + set_c_flag HCS08 t (* C<-true *) + (setweak_sp_reg HCS08 t (* SP<-0x0110 *) + (setweak_indX_16_reg HCS08 t (* H:X<-0xFF50 *) + (set_pc_reg HCS08 t (* PC<-mTest_HCS08_prog *) + (start_of_model HCS08 MC9S08AW60 t + (load_from_source_at t (* carica mTest_bytes in ROM:mTest_HCS08_data *) + (load_from_source_at t (* carica mTest_bytes in RAM:mTest_HCS08_RAM *) + (load_from_source_at t (zero_memory t) (* carica source in ROM:mTest_HCS08_prog *) + mTest_HCS08_ADC_source (extu_w32 mTest_HCS08_prog)) + mTest_bytes (extu_w32 mTest_HCS08_RAM)) + mTest_bytes (extu_w32 mTest_HCS08_data)) + (build_memory_type_of_model HCS08 MC9S08AW60 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 *) + mTest_HCS08_prog) + (mk_word16 〈xF,xF〉 〈x5,x0〉)) + (mk_word16 〈x0,x1〉 〈x1,x0〉)) + true. + +(* dimostrazione senza svolgimento degli stati, immediata *) +nlemma ok_mTest_HCS08_ADC_full : + let t ≝ MEM_TREE in + execute HCS08 t (TickOK ? (mTest_HCS08_ADC_status t)) nat28 = + (* NB: V,N,Z sono tornati false C e' tornato true *) + TickOK ? (set_pc_reg HCS08 t (* nuovo PC *) + (set_acc_8_low_reg HCS08 t (mTest_HCS08_ADC_status t) 〈x1,x6〉) (* nuovo A *) + (mk_word16 〈x1,x8〉 〈x7,x4〉)). + (* esempio per svoglimento degli stati manualmente*) + nletin BEFORE ≝ (alu HCS08 t (mTest_HCS08_ADC_status t)); + nnormalize in BEFORE:(%); + + nletin AFTER_ALU1 ≝ (match execute HCS08 t (TickOK ? (mTest_HCS08_ADC_status t)) nat2 with + [ TickERR _ _ ⇒ BEFORE + | TickSUSP _ _ ⇒ BEFORE + | TickOK s ⇒ alu HCS08 t s ]); + nnormalize in AFTER_ALU1:(%); + + nletin AFTER_ALU2 ≝ (match execute HCS08 t (TickOK ? + (set_alu HCS08 t (mTest_HCS08_ADC_status t) AFTER_ALU1)) nat3 with + [ TickERR _ _ ⇒ BEFORE + | TickSUSP _ _ ⇒ BEFORE + | TickOK s ⇒ alu HCS08 t s ]); + nnormalize in AFTER_ALU2:(%); + + nletin AFTER_ALU3 ≝ (match execute HCS08 t (TickOK ? + (set_alu HCS08 t (mTest_HCS08_ADC_status t) AFTER_ALU2)) nat4 with + [ TickERR _ _ ⇒ BEFORE + | TickSUSP _ _ ⇒ BEFORE + | TickOK s ⇒ alu HCS08 t s ]); + nnormalize in AFTER_ALU3:(%); + + nletin AFTER_ALU4 ≝ (match execute HCS08 t (TickOK ? + (set_alu HCS08 t (mTest_HCS08_ADC_status t) AFTER_ALU3)) nat4 with + [ TickERR _ _ ⇒ BEFORE + | TickSUSP _ _ ⇒ BEFORE + | TickOK s ⇒ alu HCS08 t s ]); + nnormalize in AFTER_ALU4:(%); + + nletin AFTER_ALU5 ≝ (match execute HCS08 t (TickOK ? + (set_alu HCS08 t (mTest_HCS08_ADC_status t) AFTER_ALU4)) nat3 with + [ TickERR _ _ ⇒ BEFORE + | TickSUSP _ _ ⇒ BEFORE + | TickOK s ⇒ alu HCS08 t s ]); + nnormalize in AFTER_ALU5:(%); + + nletin AFTER_ALU6 ≝ (match execute HCS08 t (TickOK ? + (set_alu HCS08 t (mTest_HCS08_ADC_status t) AFTER_ALU5)) nat3 with + [ TickERR _ _ ⇒ BEFORE + | TickSUSP _ _ ⇒ BEFORE + | TickOK s ⇒ alu HCS08 t s ]); + nnormalize in AFTER_ALU6:(%); + + nletin AFTER_ALU7 ≝ (match execute HCS08 t (TickOK ? + (set_alu HCS08 t (mTest_HCS08_ADC_status t) AFTER_ALU6)) nat5 with + [ TickERR _ _ ⇒ BEFORE + | TickSUSP _ _ ⇒ BEFORE + | TickOK s ⇒ alu HCS08 t s ]); + nnormalize in AFTER_ALU7:(%); + + nletin AFTER_ALU8 ≝ (match execute HCS08 t (TickOK ? + (set_alu HCS08 t (mTest_HCS08_ADC_status t) AFTER_ALU7)) nat4 with + [ TickERR _ _ ⇒ BEFORE + | TickSUSP _ _ ⇒ BEFORE + | TickOK s ⇒ alu HCS08 t s ]); + nnormalize in AFTER_ALU8:(%); *) + + napply refl_eq. +nqed. diff --git a/helm/software/matita/contribs/ng_assembly/emulator/tests/micro_tests_tools.ma b/helm/software/matita/contribs/ng_assembly/emulator/tests/micro_tests_tools.ma new file mode 100755 index 000000000..47417a2c4 --- /dev/null +++ b/helm/software/matita/contribs/ng_assembly/emulator/tests/micro_tests_tools.ma @@ -0,0 +1,80 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +(* ********************************************************************** *) +(* Progetto FreeScale *) +(* *) +(* Sviluppato da: Ing. Cosimo Oliboni, oliboni@cs.unibo.it *) +(* Sviluppo: 2008-2010 *) +(* *) +(* ********************************************************************** *) + +include "num/word16.ma". +include "common/list.ma". + +(* ****************************************** *) +(* MICRO TEST DI CORRETTEZZA DELLE ISTRUZIONI *) +(* ****************************************** *) + +(* tabella 0x00 - 0xFF utile da caricare in RAM/ROM *) +ndefinition mTest_bytes : list byte8 ≝ + [ 〈x0,x0〉 ; 〈x0,x1〉 ; 〈x0,x2〉 ; 〈x0,x3〉 ; 〈x0,x4〉 ; 〈x0,x5〉 ; 〈x0,x6〉 ; 〈x0,x7〉 + ; 〈x0,x8〉 ; 〈x0,x9〉 ; 〈x0,xA〉 ; 〈x0,xB〉 ; 〈x0,xC〉 ; 〈x0,xD〉 ; 〈x0,xE〉 ; 〈x0,xF〉 ] +@[ 〈x1,x0〉 ; 〈x1,x1〉 ; 〈x1,x2〉 ; 〈x1,x3〉 ; 〈x1,x4〉 ; 〈x1,x5〉 ; 〈x1,x6〉 ; 〈x1,x7〉 + ; 〈x1,x8〉 ; 〈x1,x9〉 ; 〈x1,xA〉 ; 〈x1,xB〉 ; 〈x1,xC〉 ; 〈x1,xD〉 ; 〈x1,xE〉 ; 〈x1,xF〉 ] +@[ 〈x2,x0〉 ; 〈x2,x1〉 ; 〈x2,x2〉 ; 〈x2,x3〉 ; 〈x2,x4〉 ; 〈x2,x5〉 ; 〈x2,x6〉 ; 〈x2,x7〉 + ; 〈x2,x8〉 ; 〈x2,x9〉 ; 〈x2,xA〉 ; 〈x2,xB〉 ; 〈x2,xC〉 ; 〈x2,xD〉 ; 〈x2,xE〉 ; 〈x2,xF〉 ] +@[ 〈x3,x0〉 ; 〈x3,x1〉 ; 〈x3,x2〉 ; 〈x3,x3〉 ; 〈x3,x4〉 ; 〈x3,x5〉 ; 〈x3,x6〉 ; 〈x3,x7〉 + ; 〈x3,x8〉 ; 〈x3,x9〉 ; 〈x3,xA〉 ; 〈x3,xB〉 ; 〈x3,xC〉 ; 〈x3,xD〉 ; 〈x3,xE〉 ; 〈x3,xF〉 ] +@[ 〈x4,x0〉 ; 〈x4,x1〉 ; 〈x4,x2〉 ; 〈x4,x3〉 ; 〈x4,x4〉 ; 〈x4,x5〉 ; 〈x4,x6〉 ; 〈x4,x7〉 + ; 〈x4,x8〉 ; 〈x4,x9〉 ; 〈x4,xA〉 ; 〈x4,xB〉 ; 〈x4,xC〉 ; 〈x4,xD〉 ; 〈x4,xE〉 ; 〈x4,xF〉 ] +@[ 〈x5,x0〉 ; 〈x5,x1〉 ; 〈x5,x2〉 ; 〈x5,x3〉 ; 〈x5,x4〉 ; 〈x5,x5〉 ; 〈x5,x6〉 ; 〈x5,x7〉 + ; 〈x5,x8〉 ; 〈x5,x9〉 ; 〈x5,xA〉 ; 〈x5,xB〉 ; 〈x5,xC〉 ; 〈x5,xD〉 ; 〈x5,xE〉 ; 〈x5,xF〉 ] +@[ 〈x6,x0〉 ; 〈x6,x1〉 ; 〈x6,x2〉 ; 〈x6,x3〉 ; 〈x6,x4〉 ; 〈x6,x5〉 ; 〈x6,x6〉 ; 〈x6,x7〉 + ; 〈x6,x8〉 ; 〈x6,x9〉 ; 〈x6,xA〉 ; 〈x6,xB〉 ; 〈x6,xC〉 ; 〈x6,xD〉 ; 〈x6,xE〉 ; 〈x6,xF〉 ] +@[ 〈x7,x0〉 ; 〈x7,x1〉 ; 〈x7,x2〉 ; 〈x7,x3〉 ; 〈x7,x4〉 ; 〈x7,x5〉 ; 〈x7,x6〉 ; 〈x7,x7〉 + ; 〈x7,x8〉 ; 〈x7,x9〉 ; 〈x7,xA〉 ; 〈x7,xB〉 ; 〈x7,xC〉 ; 〈x7,xD〉 ; 〈x7,xE〉 ; 〈x7,xF〉 ] +@[ 〈x8,x0〉 ; 〈x8,x1〉 ; 〈x8,x2〉 ; 〈x8,x3〉 ; 〈x8,x4〉 ; 〈x8,x5〉 ; 〈x8,x6〉 ; 〈x8,x7〉 + ; 〈x8,x8〉 ; 〈x8,x9〉 ; 〈x8,xA〉 ; 〈x8,xB〉 ; 〈x8,xC〉 ; 〈x8,xD〉 ; 〈x8,xE〉 ; 〈x8,xF〉 ] +@[ 〈x9,x0〉 ; 〈x9,x1〉 ; 〈x9,x2〉 ; 〈x9,x3〉 ; 〈x9,x4〉 ; 〈x9,x5〉 ; 〈x9,x6〉 ; 〈x9,x7〉 + ; 〈x9,x8〉 ; 〈x9,x9〉 ; 〈x9,xA〉 ; 〈x9,xB〉 ; 〈x9,xC〉 ; 〈x9,xD〉 ; 〈x9,xE〉 ; 〈x9,xF〉 ] +@[ 〈xA,x0〉 ; 〈xA,x1〉 ; 〈xA,x2〉 ; 〈xA,x3〉 ; 〈xA,x4〉 ; 〈xA,x5〉 ; 〈xA,x6〉 ; 〈xA,x7〉 + ; 〈xA,x8〉 ; 〈xA,x9〉 ; 〈xA,xA〉 ; 〈xA,xB〉 ; 〈xA,xC〉 ; 〈xA,xD〉 ; 〈xA,xE〉 ; 〈xA,xF〉 ] +@[ 〈xB,x0〉 ; 〈xB,x1〉 ; 〈xB,x2〉 ; 〈xB,x3〉 ; 〈xB,x4〉 ; 〈xB,x5〉 ; 〈xB,x6〉 ; 〈xB,x7〉 + ; 〈xB,x8〉 ; 〈xB,x9〉 ; 〈xB,xA〉 ; 〈xB,xB〉 ; 〈xB,xC〉 ; 〈xB,xD〉 ; 〈xB,xE〉 ; 〈xB,xF〉 ] +@[ 〈xC,x0〉 ; 〈xC,x1〉 ; 〈xC,x2〉 ; 〈xC,x3〉 ; 〈xC,x4〉 ; 〈xC,x5〉 ; 〈xC,x6〉 ; 〈xC,x7〉 + ; 〈xC,x8〉 ; 〈xC,x9〉 ; 〈xC,xA〉 ; 〈xC,xB〉 ; 〈xC,xC〉 ; 〈xC,xD〉 ; 〈xC,xE〉 ; 〈xC,xF〉 ] +@[ 〈xD,x0〉 ; 〈xD,x1〉 ; 〈xD,x2〉 ; 〈xD,x3〉 ; 〈xD,x4〉 ; 〈xD,x5〉 ; 〈xD,x6〉 ; 〈xD,x7〉 + ; 〈xD,x8〉 ; 〈xD,x9〉 ; 〈xD,xA〉 ; 〈xD,xB〉 ; 〈xD,xC〉 ; 〈xD,xD〉 ; 〈xD,xE〉 ; 〈xD,xF〉 ] +@[ 〈xE,x0〉 ; 〈xE,x1〉 ; 〈xE,x2〉 ; 〈xE,x3〉 ; 〈xE,x4〉 ; 〈xE,x5〉 ; 〈xE,x6〉 ; 〈xE,x7〉 + ; 〈xE,x8〉 ; 〈xE,x9〉 ; 〈xE,xA〉 ; 〈xE,xB〉 ; 〈xE,xC〉 ; 〈xE,xD〉 ; 〈xE,xE〉 ; 〈xE,xF〉 ] +@[ 〈xF,x0〉 ; 〈xF,x1〉 ; 〈xF,x2〉 ; 〈xF,x3〉 ; 〈xF,x4〉 ; 〈xF,x5〉 ; 〈xF,x6〉 ; 〈xF,x7〉 + ; 〈xF,x8〉 ; 〈xF,x9〉 ; 〈xF,xA〉 ; 〈xF,xB〉 ; 〈xF,xC〉 ; 〈xF,xD〉 ; 〈xF,xE〉 ; 〈xF,xF〉 + ]. + +(* + 1) mTest_x_RAM : inizio della RAM + (start point per caricamento mTest_bytes in RAM) + 2) mTest_x_prog: inizio della ROM + (start point per caricamento programma in ROM) + 3) mTest_x_data: ultimi 256b della ROM + (start point per caricamento mTest_bytes in ROM) +*) +ndefinition mTest_HCS08_RAM ≝ 〈〈x0,x0〉:〈x7,x0〉〉. +ndefinition mTest_HCS08_prog ≝ 〈〈x1,x8〉:〈x6,x0〉〉. +ndefinition mTest_HCS08_data ≝ 〈〈xF,xF〉:〈x0,x0〉〉. + +ndefinition mTest_RS08_RAM ≝ 〈〈x0,x0〉:〈x2,x0〉〉. +ndefinition mTest_RS08_prog ≝ 〈〈x3,x8〉:〈x0,x0〉〉. +ndefinition mTest_RS08_data ≝ 〈〈x3,xF〉:〈x0,x0〉〉. -- 2.39.2