From: Cosimo Oliboni Date: Fri, 17 Jul 2009 12:41:15 +0000 (+0000) Subject: freescale porting, work in progress X-Git-Tag: make_still_working~3673 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=2d88fad67eb842ed5fc70cd435f9920c7a2583f8;p=helm.git freescale porting, work in progress --- diff --git a/helm/software/matita/contribs/ng_assembly/compiler/ast_type.ma b/helm/software/matita/contribs/ng_assembly/compiler/ast_type.ma new file mode 100755 index 000000000..8f6de6f47 --- /dev/null +++ b/helm/software/matita/contribs/ng_assembly/compiler/ast_type.ma @@ -0,0 +1,194 @@ +(**************************************************************************) +(* ___ *) +(* ||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: Cosimo Oliboni, oliboni@cs.unibo.it *) +(* Cosimo Oliboni, oliboni@cs.unibo.it *) +(* *) +(* ********************************************************************** *) + +include "utility/utility.ma". +include "freescale/nat_lemmas.ma". + +(* ************************* *) +(* dimensioni degli elementi *) +(* ************************* *) + +(* usato per definire nell'ast *) +ninductive ast_base_type : Type ≝ + AST_BASE_TYPE_BYTE8: ast_base_type +| AST_BASE_TYPE_WORD16: ast_base_type +| AST_BASE_TYPE_WORD32: ast_base_type. + +ndefinition ast_base_type_ind + : ΠP:ast_base_type → Prop.P AST_BASE_TYPE_BYTE8 → P AST_BASE_TYPE_WORD16 → P AST_BASE_TYPE_WORD32 → + Πa:ast_base_type.P a ≝ +λP:ast_base_type → Prop.λp:P AST_BASE_TYPE_BYTE8.λp1:P AST_BASE_TYPE_WORD16.λp2:P AST_BASE_TYPE_WORD32. +λa:ast_base_type. + match a with [ AST_BASE_TYPE_BYTE8 ⇒ p | AST_BASE_TYPE_WORD16 ⇒ p1 | AST_BASE_TYPE_WORD32 ⇒ p2 ]. + +ndefinition ast_base_type_rec + : ΠP:ast_base_type → Set.P AST_BASE_TYPE_BYTE8 → P AST_BASE_TYPE_WORD16 → P AST_BASE_TYPE_WORD32 → + Πa:ast_base_type.P a ≝ +λP:ast_base_type → Set.λp:P AST_BASE_TYPE_BYTE8.λp1:P AST_BASE_TYPE_WORD16.λp2:P AST_BASE_TYPE_WORD32. +λa:ast_base_type. + match a with [ AST_BASE_TYPE_BYTE8 ⇒ p | AST_BASE_TYPE_WORD16 ⇒ p1 | AST_BASE_TYPE_WORD32 ⇒ p2 ]. + +ndefinition ast_base_type_rect + : ΠP:ast_base_type → Type.P AST_BASE_TYPE_BYTE8 → P AST_BASE_TYPE_WORD16 → P AST_BASE_TYPE_WORD32 → + Πa:ast_base_type.P a ≝ +λP:ast_base_type → Type.λp:P AST_BASE_TYPE_BYTE8.λp1:P AST_BASE_TYPE_WORD16.λp2:P AST_BASE_TYPE_WORD32. +λa:ast_base_type. + match a with [ AST_BASE_TYPE_BYTE8 ⇒ p | AST_BASE_TYPE_WORD16 ⇒ p1 | AST_BASE_TYPE_WORD32 ⇒ p2 ]. + +ninductive ast_type : Type ≝ + AST_TYPE_BASE: ast_base_type → ast_type +| AST_TYPE_ARRAY: ast_type → nat → ast_type +| AST_TYPE_STRUCT: ne_list ast_type → ast_type. + +nlet rec ast_type_ind_aux (P:ast_type → Prop) + (f:Πt.P t → P (AST_TYPE_STRUCT (ne_nil ? t))) + (f1:Πh,t.P h → P (AST_TYPE_STRUCT t) → P (AST_TYPE_STRUCT (ne_cons ? h t))) + (f2:Πt.P t) + (t:ne_list ast_type) on t ≝ + match t return λt.P (AST_TYPE_STRUCT t) with + [ ne_nil h ⇒ f h (f2 h) + | ne_cons h t ⇒ f1 h t (f2 h) (ast_type_ind_aux P f f1 f2 t) + ]. + +nlet rec ast_type_ind (P:ast_type → Prop) + (f:Πb.P (AST_TYPE_BASE b)) + (f1:Πt,n.P t → P (AST_TYPE_ARRAY t n)) + (f2:Πt.P t → P (AST_TYPE_STRUCT (ne_nil ? t))) + (f3:Πh,t.P h → P (AST_TYPE_STRUCT t) → P (AST_TYPE_STRUCT (ne_cons ? h t))) + (t:ast_type) on t : P t ≝ + match t return λt.P t with + [ AST_TYPE_BASE b ⇒ f b + | AST_TYPE_ARRAY t' n ⇒ f1 t' n (ast_type_ind P f f1 f2 f3 t') + | AST_TYPE_STRUCT nl ⇒ match nl with + [ ne_nil h ⇒ f2 h (ast_type_ind P f f1 f2 f3 h) + | ne_cons h t ⇒ f3 h t (ast_type_ind P f f1 f2 f3 h) (ast_type_ind_aux P f2 f3 (ast_type_ind P f f1 f2 f3) t) + ] + ]. + +nlet rec ast_type_rec_aux (P:ast_type → Set) + (f:Πt.P t → P (AST_TYPE_STRUCT (ne_nil ? t))) + (f1:Πh,t.P h → P (AST_TYPE_STRUCT t) → P (AST_TYPE_STRUCT (ne_cons ? h t))) + (f2:Πt.P t) + (t:ne_list ast_type) on t ≝ + match t return λt.P (AST_TYPE_STRUCT t) with + [ ne_nil h ⇒ f h (f2 h) + | ne_cons h t ⇒ f1 h t (f2 h) (ast_type_rec_aux P f f1 f2 t) + ]. + +nlet rec ast_type_rec (P:ast_type → Set) + (f:Πb.P (AST_TYPE_BASE b)) + (f1:Πt,n.P t → P (AST_TYPE_ARRAY t n)) + (f2:Πt.P t → P (AST_TYPE_STRUCT (ne_nil ? t))) + (f3:Πh,t.P h → P (AST_TYPE_STRUCT t) → P (AST_TYPE_STRUCT (ne_cons ? h t))) + (t:ast_type) on t : P t ≝ + match t return λt.P t with + [ AST_TYPE_BASE b ⇒ f b + | AST_TYPE_ARRAY t' n ⇒ f1 t' n (ast_type_rec P f f1 f2 f3 t') + | AST_TYPE_STRUCT nl ⇒ match nl with + [ ne_nil h ⇒ f2 h (ast_type_rec P f f1 f2 f3 h) + | ne_cons h t ⇒ f3 h t (ast_type_rec P f f1 f2 f3 h) (ast_type_rec_aux P f2 f3 (ast_type_rec P f f1 f2 f3) t) + ] + ]. + +nlet rec ast_type_rect_aux (P:ast_type → Type) + (f:Πt.P t → P (AST_TYPE_STRUCT (ne_nil ? t))) + (f1:Πh,t.P h → P (AST_TYPE_STRUCT t) → P (AST_TYPE_STRUCT (ne_cons ? h t))) + (f2:Πt.P t) + (t:ne_list ast_type) on t ≝ + match t return λt.P (AST_TYPE_STRUCT t) with + [ ne_nil h ⇒ f h (f2 h) + | ne_cons h t ⇒ f1 h t (f2 h) (ast_type_rect_aux P f f1 f2 t) + ]. + +nlet rec ast_type_rect (P:ast_type → Type) + (f:Πb.P (AST_TYPE_BASE b)) + (f1:Πt,n.P t → P (AST_TYPE_ARRAY t n)) + (f2:Πt.P t → P (AST_TYPE_STRUCT (ne_nil ? t))) + (f3:Πh,t.P h → P (AST_TYPE_STRUCT t) → P (AST_TYPE_STRUCT (ne_cons ? h t))) + (t:ast_type) on t : P t ≝ + match t return λt.P t with + [ AST_TYPE_BASE b ⇒ f b + | AST_TYPE_ARRAY t' n ⇒ f1 t' n (ast_type_rect P f f1 f2 f3 t') + | AST_TYPE_STRUCT nl ⇒ match nl with + [ ne_nil h ⇒ f2 h (ast_type_rect P f f1 f2 f3 h) + | ne_cons h t ⇒ f3 h t (ast_type_rect P f f1 f2 f3 h) (ast_type_rect_aux P f2 f3 (ast_type_rect P f f1 f2 f3) t) + ] + ]. + +ndefinition eq_ast_base_type ≝ +λt1,t2:ast_base_type.match t1 with + [ AST_BASE_TYPE_BYTE8 ⇒ match t2 with + [ AST_BASE_TYPE_BYTE8 ⇒ true | _ ⇒ false ] + | AST_BASE_TYPE_WORD16 ⇒ match t2 with + [ AST_BASE_TYPE_WORD16 ⇒ true | _ ⇒ false ] + | AST_BASE_TYPE_WORD32 ⇒ match t2 with + [ AST_BASE_TYPE_WORD32 ⇒ true | _ ⇒ false ] + ]. + +nlet rec eq_ast_type (t1,t2:ast_type) on t1 ≝ + match t1 with + [ AST_TYPE_BASE bType1 ⇒ match t2 with + [ AST_TYPE_BASE bType2 ⇒ eq_ast_base_type bType1 bType2 + | _ ⇒ false ] + | AST_TYPE_ARRAY subType1 dim1 ⇒ match t2 with + [ AST_TYPE_ARRAY subType2 dim2 ⇒ (eq_ast_type subType1 subType2) ⊗ (eq_nat dim1 dim2) + | _ ⇒ false ] + | AST_TYPE_STRUCT nelSubType1 ⇒ match t2 with + [ AST_TYPE_STRUCT nelSubType2 ⇒ + match eq_nat (len_neList ? nelSubType1) (len_neList ? nelSubType2) + return λx.eq_nat (len_neList ? nelSubType1) (len_neList ? nelSubType2) = x → bool + with + [ true ⇒ λp:(eq_nat (len_neList ? nelSubType1) (len_neList ? nelSubType2) = true). + fold_right_neList2 ?? (λx1,x2,acc.(eq_ast_type x1 x2)⊗acc) + true nelSubType1 nelSubType2 + (eqnat_to_eq (len_neList ? nelSubType1) (len_neList ? nelSubType2) p) + | false ⇒ λp:(eq_nat (len_neList ? nelSubType1) (len_neList ? nelSubType2) = false).false + ] (refl_eq ? (eq_nat (len_neList ? nelSubType1) (len_neList ? nelSubType2))) + | _ ⇒ false + ] + ]. + +ndefinition is_ast_base_type ≝ +λast:ast_type.match ast with [ AST_TYPE_BASE _ ⇒ True | _ ⇒ False ]. + +ndefinition isb_ast_base_type ≝ +λast:ast_type.match ast with [ AST_TYPE_BASE _ ⇒ true | _ ⇒ false ]. + +ndefinition isnt_ast_base_type ≝ +λast:ast_type.match ast with [ AST_TYPE_BASE _ ⇒ False | _ ⇒ True ]. + +ndefinition isntb_ast_base_type ≝ +λast:ast_type.match ast with [ AST_TYPE_BASE _ ⇒ false | _ ⇒ true ]. + +ndefinition eval_size_base_type ≝ +λast:ast_base_type.match ast with + [ AST_BASE_TYPE_BYTE8 ⇒ 1 + | AST_BASE_TYPE_WORD16 ⇒ 2 + | AST_BASE_TYPE_WORD32 ⇒ 4 + ]. + +nlet rec eval_size_type (ast:ast_type) on ast ≝ + match ast with + [ AST_TYPE_BASE b ⇒ eval_size_base_type b + | AST_TYPE_ARRAY sub_ast dim ⇒ (dim+1)*(eval_size_type sub_ast) + | AST_TYPE_STRUCT nel_ast ⇒ fold_right_neList ?? (λt,x.(eval_size_type t)+x) O nel_ast + ]. diff --git a/helm/software/matita/contribs/ng_assembly/compiler/ast_type_lemmas.ma b/helm/software/matita/contribs/ng_assembly/compiler/ast_type_lemmas.ma new file mode 100755 index 000000000..99f0f1b12 --- /dev/null +++ b/helm/software/matita/contribs/ng_assembly/compiler/ast_type_lemmas.ma @@ -0,0 +1,177 @@ +(**************************************************************************) +(* ___ *) +(* ||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: Cosimo Oliboni, oliboni@cs.unibo.it *) +(* Cosimo Oliboni, oliboni@cs.unibo.it *) +(* *) +(* ********************************************************************** *) + +include "compiler/ast_type.ma". + +(* ************************* *) +(* dimensioni degli elementi *) +(* ************************* *) + +ndefinition astbasetype_destruct_aux ≝ +Πb1,b2:ast_base_type.ΠP:Prop.b1 = b2 → + match b1 with + [ AST_BASE_TYPE_BYTE8 ⇒ match b2 with [ AST_BASE_TYPE_BYTE8 ⇒ P → P | _ ⇒ P ] + | AST_BASE_TYPE_WORD16 ⇒ match b2 with [ AST_BASE_TYPE_WORD16 ⇒ P → P | _ ⇒ P ] + | AST_BASE_TYPE_WORD32 ⇒ match b2 with [ AST_BASE_TYPE_WORD32 ⇒ P → P | _ ⇒ P ] + ]. + +ndefinition astbasetype_destruct : astbasetype_destruct_aux. + #b1; #b2; #P; + nelim b1; + nelim b2; + nnormalize; + #H; + ##[ ##1,5,9: napply (λx:P.x) + ##| ##2,3: napply (False_ind ??); + nchange with (match AST_BASE_TYPE_BYTE8 with [ AST_BASE_TYPE_BYTE8 ⇒ False | _ ⇒ True]); + nrewrite > H; + nnormalize; + napply I + ##| ##4,6: napply (False_ind ??); + nchange with (match AST_BASE_TYPE_WORD16 with [ AST_BASE_TYPE_WORD16 ⇒ False | _ ⇒ True]); + nrewrite > H; + nnormalize; + napply I + ##| ##7,8: napply (False_ind ??); + nchange with (match AST_BASE_TYPE_WORD32 with [ AST_BASE_TYPE_WORD32 ⇒ False | _ ⇒ True]); + nrewrite > H; + nnormalize; + napply I + ##] +nqed. + +nlemma symmetric_eqastbasetype : symmetricT ast_base_type bool eq_ast_base_type. + #b1; #b2; ncases b1; ncases b2; nnormalize; napply (refl_eq ??). nqed. + +nlemma eqastbasetype_to_eq : ∀b1,b2.eq_ast_base_type b1 b2 = true → b1 = b2. + #b1; #b2; ncases b1; ncases b2; nnormalize; + ##[ ##1,5,9: #H; napply (refl_eq ??) + ##| ##*: #H; napply (bool_destruct ??? H) + ##] +nqed. + +nlemma eq_to_eqastbasetype : ∀b1,b2.b1 = b2 → eq_ast_base_type b1 b2 = true. + #b1; #b2; ncases b1; ncases b2; nnormalize; + ##[ ##1,5,9: #H; napply (refl_eq ??) + ##| ##*: #H; napply (astbasetype_destruct ??? H) + ##] +nqed. + +nlemma asttype_destruct_base_base : ∀b1,b2.AST_TYPE_BASE b1 = AST_TYPE_BASE b2 → b1 = b2. + #b1; #b2; #H; + nchange with (match AST_TYPE_BASE b2 with [ AST_TYPE_BASE a ⇒ b1 = a | _ ⇒ False ]); + nrewrite < H; + nnormalize; + napply (refl_eq ??). +nqed. + +nlemma asttype_destruct_array_array_1 : ∀x1,x2,y1,y2.AST_TYPE_ARRAY x1 y1 = AST_TYPE_ARRAY x2 y2 → x1 = x2. + #x1; #x2; #y1; #y2; #H; + nchange with (match AST_TYPE_ARRAY x2 y2 with [ AST_TYPE_ARRAY a _ ⇒ x1 = a | _ ⇒ False ]); + nrewrite < H; + nnormalize; + napply (refl_eq ??). +nqed. + +nlemma asttype_destruct_array_array_2 : ∀x1,x2,y1,y2.AST_TYPE_ARRAY x1 y1 = AST_TYPE_ARRAY x2 y2 → y1 = y2. + #x1; #x2; #y1; #y2; #H; + nchange with (match AST_TYPE_ARRAY x2 y2 with [ AST_TYPE_ARRAY _ b ⇒ y1 = b | _ ⇒ False ]); + nrewrite < H; + nnormalize; + napply (refl_eq ??). +nqed. + +nlemma asttype_destruct_struc_struct : ∀b1,b2.AST_TYPE_STRUCT b1 = AST_TYPE_STRUCT b2 → b1 = b2. + #b1; #b2; #H; + nchange with (match AST_TYPE_STRUCT b2 with [ AST_TYPE_STRUCT a ⇒ b1 = a | _ ⇒ False ]); + nrewrite < H; + nnormalize; + napply (refl_eq ??). +nqed. + +ndefinition asttype_destruct_aux ≝ +Πb1,b2:ast_type.ΠP:Prop.b1 = b2 → + match b1 with + [ AST_TYPE_BASE s1 ⇒ match b2 with + [ AST_TYPE_BASE s2 ⇒ match s1 with + [ AST_BASE_TYPE_BYTE8 ⇒ match s2 with [ AST_BASE_TYPE_BYTE8 ⇒ P → P | _ ⇒ P ] + | AST_BASE_TYPE_WORD16 ⇒ match s2 with [ AST_BASE_TYPE_WORD16 ⇒ P → P | _ ⇒ P ] + | AST_BASE_TYPE_WORD32 ⇒ match s2 with [ AST_BASE_TYPE_WORD32 ⇒ P → P | _ ⇒ P ] + ] | _ ⇒ P ] + | AST_TYPE_ARRAY _ _ ⇒ match b2 with [ AST_TYPE_ARRAY _ _ ⇒ P → P | _ ⇒ P ] + | AST_TYPE_STRUCT _ ⇒ match b2 with [ AST_TYPE_STRUCT _ ⇒ P → P | _ ⇒ P ] + ]. + +ndefinition asttype_destruct : asttype_destruct_aux. + #b1; #b2; #P; + ncases b1; + ##[ ##1: ncases b2; + ##[ ##1: nnormalize; #s1; #s2; ncases s1; ncases s2; nnormalize; + ##[ ##1,5,9: #H; napply (λx:P.x) + ##| ##*: #H; napply (astbasetype_destruct ??? (asttype_destruct_base_base ?? H)) + ##] + ##| ##2: #t; #n; #b; nnormalize; #H + ##| ##3: #l; #b; nnormalize; #H + ##] + napply (False_ind ??); + nchange with (match AST_TYPE_BASE b with [ AST_TYPE_BASE _ ⇒ False | _ ⇒ True ]); + nrewrite > H; nnormalize; napply I + ##| ##2: ncases b2; + ##[ ##2: #t1; #n1; #t2; #n2; nnormalize; #H; napply (λx:P.x) + ##| ##1: #b; #t; #n; nnormalize; #H + ##| ##3: #l; #t; #n; nnormalize; #H + ##] + napply (False_ind ??); + nchange with (match AST_TYPE_ARRAY t n with [ AST_TYPE_ARRAY _ _ ⇒ False | _ ⇒ True ]); + nrewrite > H; nnormalize; napply I + ##| ##3: ncases b2; + ##[ ##3: #l1; #l2; nnormalize; #H; napply (λx:P.x) + ##| ##1: #b; #l; nnormalize; #H + ##| ##2: #t; #n; #l; nnormalize; #H + ##] + napply (False_ind ??); + nchange with (match AST_TYPE_STRUCT l with [ AST_TYPE_STRUCT _ ⇒ False | _ ⇒ True ]); + nrewrite > H; nnormalize; napply I + ##] +nqed. + +(* eq_ast lemmas missing *) + +nlemma isbastbasetype_to_isastbasetype : ∀ast.isb_ast_base_type ast = true → is_ast_base_type ast. + #ast; + ncases ast; + nnormalize; + ##[ ##1: #t; #H; napply I + ##| ##2: #t; #n; #H; napply (bool_destruct ??? H) + ##| ##3: #t; #H; napply (bool_destruct ??? H) + ##] +nqed. + +nlemma isntbastbasetype_to_isntastbasetype : ∀ast.isntb_ast_base_type ast = true → isnt_ast_base_type ast. + #ast; + ncases ast; + nnormalize; + ##[ ##1: #t; #H; napply (bool_destruct ??? H) + ##| ##2: #t; #n; #H; napply I + ##| ##3: #l; #H; napply I + ##] +nqed. diff --git a/helm/software/matita/contribs/ng_assembly/depends b/helm/software/matita/contribs/ng_assembly/depends index 3a517048b..4c1f165d2 100644 --- a/helm/software/matita/contribs/ng_assembly/depends +++ b/helm/software/matita/contribs/ng_assembly/depends @@ -3,10 +3,11 @@ freescale/status.ma freescale/memory_abs.ma freescale/opcode_base.ma freescale/p freescale/memory_bits.ma freescale/memory_trees.ma utility/ascii_lemmas1.ma freescale/theory.ma utility/ascii.ma freescale/byte8_lemmas.ma freescale/byte8.ma freescale/exadecim_lemmas.ma -utility/string_lemmas.ma utility/ascii_lemmas2.ma utility/string.ma +utility/string_lemmas.ma freescale/nat_lemmas.ma utility/ascii_lemmas2.ma utility/string.ma freescale/table_HCS08_tests.ma freescale/table_HCS08.ma freescale/multivm.ma freescale/load_write.ma freescale/nat_lemmas.ma freescale/opcode_base_lemmas.ma freescale/bool_lemmas.ma freescale/opcode_base.ma +compiler/ast_type_lemmas.ma compiler/ast_type.ma freescale/table_HC05_tests.ma freescale/table_HC05.ma freescale/option.ma freescale/bool.ma freescale/bool.ma freescale/pts.ma @@ -23,12 +24,13 @@ freescale/nat.ma freescale/bool.ma freescale/pts.ma freescale/medium_tests_tools.ma freescale/multivm.ma utility/utility_lemmas.ma utility/utility.ma freescale/memory_abs.ma freescale/memory_bits.ma freescale/memory_func.ma freescale/memory_trees.ma -test_errori.ma freescale/byte8_lemmas.ma utility/utility.ma +test_errori.ma compiler/ast_type_lemmas.ma freescale/byte8_lemmas.ma utility/utility.ma freescale/memory_struct.ma freescale/aux_bases.ma freescale/byte8.ma freescale/model.ma freescale/status.ma freescale/aux_bases.ma freescale/byte8.ma freescale/nat.ma freescale/table_HC05.ma freescale/opcode.ma freescale/exadecim_lemmas.ma freescale/bool_lemmas.ma freescale/exadecim.ma +compiler/ast_type.ma freescale/nat_lemmas.ma utility/utility.ma freescale/word16.ma freescale/byte8.ma utility/ascii.ma freescale/bool.ma freescale/memory_trees.ma freescale/memory_struct.ma freescale/option.ma freescale/theory.ma freescale/word16.ma @@ -38,7 +40,7 @@ freescale/aux_bases_lemmas.ma freescale/aux_bases.ma freescale/bool_lemmas.ma freescale/opcode_base_lemmas1.ma freescale/opcode_base_lemmas_instrmode2.ma freescale/opcode_base_lemmas_opcode2.ma freescale/word16_lemmas.ma freescale/table_HC08.ma freescale/opcode.ma freescale/prod.ma freescale/bool.ma -utility/string.ma utility/ascii.ma utility/utility.ma +utility/string.ma freescale/nat.ma freescale/theory.ma utility/ascii.ma freescale/table_HCS08.ma freescale/opcode.ma freescale/word32.ma freescale/word16.ma freescale/prod_lemmas.ma freescale/bool_lemmas.ma freescale/prod.ma @@ -46,6 +48,7 @@ freescale/opcode_base.ma freescale/aux_bases.ma freescale/theory.ma freescale/wo freescale/word32_lemmas.ma freescale/word16_lemmas.ma freescale/word32.ma freescale/status_lemmas.ma freescale/opcode_base_lemmas1.ma freescale/option_lemmas.ma freescale/prod_lemmas.ma freescale/status.ma freescale/word16_lemmas.ma utility/ascii_lemmas2.ma freescale/bool_lemmas.ma utility/ascii_lemmas1.ma +freescale/micro_tests.ma freescale/multivm.ma freescale/status_lemmas.ma freescale/table_HC08_tests.ma freescale/table_HC08.ma utility/utility.ma freescale/nat_lemmas.ma freescale/option.ma freescale/theory.ma freescale/opcode_base_lemmas_instrmode1.ma freescale/aux_bases_lemmas.ma freescale/exadecim_lemmas.ma freescale/opcode_base.ma diff --git a/helm/software/matita/contribs/ng_assembly/freescale/medium_tests.ma b/helm/software/matita/contribs/ng_assembly/freescale/medium_tests.ma index e50fe56a7..54004c444 100755 --- a/helm/software/matita/contribs/ng_assembly/freescale/medium_tests.ma +++ b/helm/software/matita/contribs/ng_assembly/freescale/medium_tests.ma @@ -175,10 +175,9 @@ lemma dTest_HCS08_sReverse_dump : qed. *) -(* (* parametrizzazione dell'enunciato del teorema *) (* dimostrazione senza svolgimento degli stati *) -lemma dTest_HCS08_sReverse_aux ≝ +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〉〉) ∧ @@ -227,7 +226,7 @@ lemma dTest_HCS08_sReverse : qed. *) -definition sReverseCalc ≝ +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)) @@ -237,7 +236,7 @@ definition sReverseCalc ≝ | TickOK s ⇒ Some ? (set_mem_desc HCS08 MEM_TREE s (load_from_source_at MEM_TREE (get_mem_desc HCS08 MEM_TREE s) dTest_zeros 〈〈x0,xD〉:〈x0,x0〉〉)) ]. -definition sReverseNoCalc ≝ +ndefinition sReverseNoCalc ≝ λstring:list byte8. Some ? (set_pc_reg HCS08 MEM_TREE (dTest_HCS08_sReverse_status MEM_TREE (fst ?? (shr_b8 (w16h (byte8_strlen string)))) @@ -245,30 +244,30 @@ definition sReverseNoCalc ≝ (byte8_strlen string) (reverse_list ? string)) (mk_word16 (mk_byte8 x1 x9) (mk_byte8 x2 xB))). -definition sReverseCalc32 ≝ sReverseCalc dTest_random_32. -definition sReverseCalc64 ≝ sReverseCalc dTest_random_64. -definition sReverseCalc128 ≝ sReverseCalc dTest_random_128. -definition sReverseCalc256 ≝ sReverseCalc dTest_random_256. -definition sReverseCalc512 ≝ sReverseCalc dTest_random_512. -definition sReverseCalc1024 ≝ sReverseCalc dTest_random_1024. -definition sReverseCalc2048 ≝ sReverseCalc dTest_random_2048. -definition sReverseCalc3072 ≝ sReverseCalc dTest_random_3072. - -definition sReverseNoCalc32 ≝ sReverseNoCalc dTest_random_32. -definition sReverseNoCalc64 ≝ sReverseNoCalc dTest_random_64. -definition sReverseNoCalc128 ≝ sReverseNoCalc dTest_random_128. -definition sReverseNoCalc256 ≝ sReverseNoCalc dTest_random_256. -definition sReverseNoCalc512 ≝ sReverseNoCalc dTest_random_512. -definition sReverseNoCalc1024 ≝ sReverseNoCalc dTest_random_1024. -definition sReverseNoCalc2048 ≝ sReverseNoCalc dTest_random_2048. -definition sReverseNoCalc3072 ≝ sReverseNoCalc dTest_random_3072. +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 *) -definition dTest_HCS08_cSort_source : word16 → (list byte8) ≝ +ndefinition dTest_HCS08_cSort_source : word16 → (list byte8) ≝ λelems:word16. let m ≝ HCS08 in source_to_byte8 m ( (* BEFORE: A=0x00 H:X=0x0F4C SP=0x0F4B PC=0x18C8 Z=true *) @@ -370,7 +369,7 @@ let m ≝ HCS08 in source_to_byte8 m ( ). (* creazione del processore+caricamento+impostazione registri *) -definition dTest_HCS08_cSort_status ≝ +ndefinition dTest_HCS08_cSort_status ≝ λt:memory_impl. λI_op:bool. λA_op:byte8. @@ -400,7 +399,7 @@ definition dTest_HCS08_cSort_status ≝ I_op. (* parametrizzazione dell'enunciato del teorema parziale *) -lemma dTest_HCS08_cSort_aux ≝ +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〉〉) ∧ @@ -430,7 +429,7 @@ lemma dTest_HCS08_cSort : qed. *) -definition cSortCalc ≝ +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)) @@ -440,36 +439,36 @@ definition cSortCalc ≝ | TickOK s ⇒ None ? ]. -definition cSortNoCalc ≝ +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))). -definition cSortCalc32 ≝ cSortCalc dTest_random_32. -definition cSortCalc64 ≝ cSortCalc dTest_random_64. -definition cSortCalc128 ≝ cSortCalc dTest_random_128. -definition cSortCalc256 ≝ cSortCalc dTest_random_256. -definition cSortCalc512 ≝ cSortCalc dTest_random_512. -definition cSortCalc1024 ≝ cSortCalc dTest_random_1024. -definition cSortCalc2048 ≝ cSortCalc dTest_random_2048. -definition cSortCalc3072 ≝ cSortCalc dTest_random_3072. - -definition cSortNoCalc32 ≝ cSortNoCalc dTest_random_32. -definition cSortNoCalc64 ≝ cSortNoCalc dTest_random_64. -definition cSortNoCalc128 ≝ cSortNoCalc dTest_random_128. -definition cSortNoCalc256 ≝ cSortNoCalc dTest_random_256. -definition cSortNoCalc512 ≝ cSortNoCalc dTest_random_512. -definition cSortNoCalc1024 ≝ cSortNoCalc dTest_random_1024. -definition cSortNoCalc2048 ≝ cSortNoCalc dTest_random_2048. -definition cSortNoCalc3072 ≝ cSortNoCalc dTest_random_3072. +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 *) -definition dTest_HCS08_gNum_source : word16 → (list byte8) ≝ +ndefinition dTest_HCS08_gNum_source : word16 → (list byte8) ≝ λelems:word16. let m ≝ HCS08 in source_to_byte8 m ( (* BEFORE: A=0x00 HX=0x1A00 PC=0x18BE SP=0x016F Z=1 (I=1) *) @@ -747,7 +746,7 @@ void _POP32(void) { ... } ). (* creazione del processore+caricamento+impostazione registri *) -definition dTest_HCS08_gNum_status ≝ +ndefinition dTest_HCS08_gNum_status ≝ λt:memory_impl. λI_op:bool. λA_op:byte8. @@ -779,7 +778,7 @@ definition dTest_HCS08_gNum_status ≝ I_op. (* NUMERI AUREI: Somma divisori(x)=x, fino a 0xFFFF sono 6/28/496/8128 *) -definition dTest_HCS08_gNum_aurei ≝ +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 @@ -797,7 +796,7 @@ definition dTest_HCS08_gNum_aurei ≝ ; 〈x0,x0〉 ; 〈x0,x0〉 ; 〈x0,x0〉 ; 〈x0,x0〉 ; 〈x0,x0〉 ; 〈x0,x0〉 ; 〈x0,x0〉 ; 〈x0,x0〉 ]. (* esecuzione execute k*(n+2) *) -let rec dTest_HCS08_gNum_execute1 (m:mcu_type) (t:memory_impl) (s:tick_result (any_status m t)) (n,ntot:nat) on n ≝ +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 @@ -807,7 +806,7 @@ let rec dTest_HCS08_gNum_execute1 (m:mcu_type) (t:memory_impl) (s:tick_result (a ]. (* esecuzione execute k*(n+1)*(n+2) *) -let rec dTest_HCS08_gNum_execute2 (m:mcu_type) (t:memory_impl) (s:tick_result (any_status m t)) (n,ntot:nat) on n ≝ +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 @@ -817,7 +816,7 @@ let rec dTest_HCS08_gNum_execute2 (m:mcu_type) (t:memory_impl) (s:tick_result (a ]. (* esecuzione execute k*n*(n+1)*(n+2) *) -let rec dTest_HCS08_gNum_execute3 (m:mcu_type) (t:memory_impl) (s:tick_result (any_status m t)) (n,ntot:nat) on n ≝ +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 @@ -827,7 +826,7 @@ let rec dTest_HCS08_gNum_execute3 (m:mcu_type) (t:memory_impl) (s:tick_result (a ]. (* esecuzione execute 80+11*n*(n+1)*(n+2) *) -definition dTest_HCS08_gNum_execute4 ≝ +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 @@ -836,7 +835,7 @@ definition dTest_HCS08_gNum_execute4 ≝ ]. (* parametrizzazione dell'enunciato del teorema parziale *) -lemma dTest_HCS08_gNum_aux ≝ +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 @@ -850,7 +849,7 @@ lemma dTest_HCS08_gNum_aux ≝ ] = Some ? (dTest_HCS08_gNum_status t false 〈x0,x0〉 num 〈〈x1,x9〉:〈x5,x1〉〉 〈〈x1,x8〉:〈xB,xE〉〉 num (dTest_HCS08_gNum_aurei num)). -definition gNumCalc ≝ +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)) @@ -860,30 +859,28 @@ definition gNumCalc ≝ | TickOK s ⇒ None ? ]. -definition gNumNoCalc ≝ +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)). -definition gNumCalc1 ≝ gNumCalc 〈〈x0,x0〉:〈x0,x1〉〉. -definition gNumCalc2 ≝ gNumCalc 〈〈x0,x0〉:〈x0,x2〉〉. -definition gNumCalc5 ≝ gNumCalc 〈〈x0,x0〉:〈x0,x5〉〉. -definition gNumCalc10 ≝ gNumCalc 〈〈x0,x0〉:〈x0,xA〉〉. -definition gNumCalc20 ≝ gNumCalc 〈〈x0,x0〉:〈x1,x4〉〉. -definition gNumCalc50 ≝ gNumCalc 〈〈x0,x0〉:〈x3,x2〉〉. -definition gNumCalc100 ≝ gNumCalc 〈〈x0,x0〉:〈x6,x4〉〉. -definition gNumCalc250 ≝ gNumCalc 〈〈x0,x0〉:〈xF,xA〉〉. -definition gNumCalc500 ≝ gNumCalc 〈〈x0,x1〉:〈xF,x4〉〉. -definition gNumCalc1000 ≝ gNumCalc 〈〈x0,x3〉:〈xE,x8〉〉. - -definition gNumNoCalc1 ≝ gNumNoCalc 〈〈x0,x0〉:〈x0,x1〉〉. -definition gNumNoCalc2 ≝ gNumNoCalc 〈〈x0,x0〉:〈x0,x2〉〉. -definition gNumNoCalc5 ≝ gNumNoCalc 〈〈x0,x0〉:〈x0,x5〉〉. -definition gNumNoCalc10 ≝ gNumNoCalc 〈〈x0,x0〉:〈x0,xA〉〉. -definition gNumNoCalc20 ≝ gNumNoCalc 〈〈x0,x0〉:〈x1,x4〉〉. -definition gNumNoCalc50 ≝ gNumNoCalc 〈〈x0,x0〉:〈x3,x2〉〉. -definition gNumNoCalc100 ≝ gNumNoCalc 〈〈x0,x0〉:〈x6,x4〉〉. -definition gNumNoCalc250 ≝ gNumNoCalc 〈〈x0,x0〉:〈xF,xA〉〉. -definition gNumNoCalc500 ≝ gNumNoCalc 〈〈x0,x1〉:〈xF,x4〉〉. -definition gNumNoCalc1000 ≝ gNumNoCalc 〈〈x0,x3〉:〈xE,x8〉〉. -*) - +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/freescale/micro_tests.ma b/helm/software/matita/contribs/ng_assembly/freescale/micro_tests.ma new file mode 100755 index 000000000..a135d153a --- /dev/null +++ b/helm/software/matita/contribs/ng_assembly/freescale/micro_tests.ma @@ -0,0 +1,787 @@ +(**************************************************************************) +(* ___ *) +(* ||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: Cosimo Oliboni, oliboni@cs.unibo.it *) +(* Cosimo Oliboni, oliboni@cs.unibo.it *) +(* *) +(* ********************************************************************** *) + +include "freescale/multivm.ma". +include "freescale/status_lemmas.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〉〉. + +ndefinition mTest_HCS08_ADC_source ≝ let m ≝ HCS08 in source_to_byte8 m ( +(* 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 m ? ADC (maIMM1 〈xA,xA〉) I) @ (* AFTER1: imm1=0xAA quindi 0x00+imm1+true=A:0xAB C:false *) +(* [0x1862] 3clk *) (compile m ? ADC (maDIR1 〈xF,xF〉) I) @ (* AFTER2: dir1=[0x00FF]=0x8F quindi 0xAB+dir1+false=A:0x3A C:true *) +(* [0x1864] 4clk *) (compile m ? ADC (maDIR2 〈〈xF,xF〉:〈x1,x1〉〉) I) @ (* AFTER3: dir2=[0xFF11]=0x11 quindi 0x3A+dir2+true=A:0x4C C:false *) +(* [0x1867] 4clk *) (compile m ? ADC (maIX2 〈〈xF,xF〉:〈xF,x0〉〉) I) @ (* AFTER4: ix2=[X+0xFFF0]=[0xFF40]=0x40 quindi 0x4C+ix2+false=A:0x8C C:false *) +(* [0x186A] 3clk *) (compile m ? ADC (maIX1 〈x2,x4〉) I) @ (* AFTER5: ix1=[X+0x0024]=[0xFF74]=0x74 quindi 0x8C+ix1+false=A:0x00 C:true *) +(* [0x186C] 3clk *) (compile m ? ADC maIX0 I) @ (* AFTER6: ix0=[X]=[0xFF50]=0x50 quindi 0x00+ix0+true=A:0x51 C:false *) +(* [0x186D] 5clk *) (compile m ? ADC (maSP2 〈〈xF,xF〉:〈x6,x1〉〉) I) @ (* AFTER7: sp2=[SP+0xFF61]=[0x0071]=0x01 quindi 0x51+sp2+false=A:0x52 C:false *) +(* [0x1871] 4clk *) (compile m ? ADC (maSP1 〈x2,x4〉) I) (* 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 *) +). + +(* 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_mcu_version_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 mTest_HCS08_prog) + mTest_bytes mTest_HCS08_RAM) + mTest_bytes mTest_HCS08_data) + (build_memory_type_of_mcu_version (FamilyHCS08 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 : + ∀t:memory_impl. + execute HCS08 t (TickOK ? (mTest_HCS08_ADC_status t)) 28 = + (* 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〉)). + #t; nelim t; + (* esempio per svoglimento degli stati manualmente + [ 1: + letin BEFORE ≝ (get_alu HCS08 MEM_FUNC (mTest_HCS08_ADC_status MEM_FUNC)); + normalize in BEFORE:(%); + + letin AFTER_ALU1 ≝ (match execute HCS08 MEM_FUNC (TickOK ? (mTest_HCS08_ADC_status MEM_FUNC)) 2 with + [ TickERR _ _ ⇒ BEFORE + | TickSUSP _ _ ⇒ BEFORE + | TickOK s ⇒ get_alu HCS08 MEM_FUNC s ]); + normalize in AFTER_ALU1:(%); + + letin AFTER_ALU2 ≝ (match execute HCS08 MEM_FUNC (TickOK ? + (set_alu HCS08 MEM_FUNC (mTest_HCS08_ADC_status MEM_FUNC) AFTER_ALU1)) 3 with + [ TickERR _ _ ⇒ BEFORE + | TickSUSP _ _ ⇒ BEFORE + | TickOK s ⇒ get_alu HCS08 MEM_FUNC s ]); + normalize in AFTER_ALU2:(%); + + letin AFTER_ALU3 ≝ (match execute HCS08 MEM_FUNC (TickOK ? + (set_alu HCS08 MEM_FUNC (mTest_HCS08_ADC_status MEM_FUNC) AFTER_ALU2)) 4 with + [ TickERR _ _ ⇒ BEFORE + | TickSUSP _ _ ⇒ BEFORE + | TickOK s ⇒ get_alu HCS08 MEM_FUNC s ]); + normalize in AFTER_ALU3:(%); + + letin AFTER_ALU4 ≝ (match execute HCS08 MEM_FUNC (TickOK ? + (set_alu HCS08 MEM_FUNC (mTest_HCS08_ADC_status MEM_FUNC) AFTER_ALU3)) 4 with + [ TickERR _ _ ⇒ BEFORE + | TickSUSP _ _ ⇒ BEFORE + | TickOK s ⇒ get_alu HCS08 MEM_FUNC s ]); + normalize in AFTER_ALU4:(%); + + letin AFTER_ALU5 ≝ (match execute HCS08 MEM_FUNC (TickOK ? + (set_alu HCS08 MEM_FUNC (mTest_HCS08_ADC_status MEM_FUNC) AFTER_ALU4)) 3 with + [ TickERR _ _ ⇒ BEFORE + | TickSUSP _ _ ⇒ BEFORE + | TickOK s ⇒ get_alu HCS08 MEM_FUNC s ]); + normalize in AFTER_ALU5:(%); + + letin AFTER_ALU6 ≝ (match execute HCS08 MEM_FUNC (TickOK ? + (set_alu HCS08 MEM_FUNC (mTest_HCS08_ADC_status MEM_FUNC) AFTER_ALU5)) 3 with + [ TickERR _ _ ⇒ BEFORE + | TickSUSP _ _ ⇒ BEFORE + | TickOK s ⇒ get_alu HCS08 MEM_FUNC s ]); + normalize in AFTER_ALU6:(%); + + letin AFTER_ALU7 ≝ (match execute HCS08 MEM_FUNC (TickOK ? + (set_alu HCS08 MEM_FUNC (mTest_HCS08_ADC_status MEM_FUNC) AFTER_ALU6)) 5 with + [ TickERR _ _ ⇒ BEFORE + | TickSUSP _ _ ⇒ BEFORE + | TickOK s ⇒ get_alu HCS08 MEM_FUNC s ]); + normalize in AFTER_ALU7:(%); + + letin AFTER_ALU8 ≝ (match execute HCS08 MEM_FUNC (TickOK ? + (set_alu HCS08 MEM_FUNC (mTest_HCS08_ADC_status MEM_FUNC) AFTER_ALU7)) 4 with + [ TickERR _ _ ⇒ BEFORE + | TickSUSP _ _ ⇒ BEFORE + | TickOK s ⇒ get_alu HCS08 MEM_FUNC s ]); + normalize in AFTER_ALU8:(%); *) + + napply (refl_eq ??). +nqed. + +(* ********* *) +(* HCS08 MOV *) +(* ********* *) + +(* +definition mTest_HCS08_MOV_source ≝ let m ≝ HCS08 in source_to_byte8 m ( +(* testa la logica di MOV e le modalita' xxx_to_xxx *) +(* BEFORE: H:X=0x0071 PC=0x1860 *) +(* [0x1860] 4clk *) (compile m ? MOV (maIMM1_to_DIR1 〈x3,xA〉 〈x7,x0〉) I) @ (* 0x3A in [0x0070] *) +(* [0x1863] 5clk *) (compile m ? MOV (maDIR1_to_DIR1 〈x7,x0〉 〈x7,x1〉) I) @ (* [0x0070] in [0x0071] *) +(* [0x1866] 5clk *) (compile m ? MOV (maIX0p_to_DIR1 〈x7,x2〉) I) @ (* [X++=0x0071] in [0x0072] *) +(* [0x1868] 5clk *) (compile m ? MOV (maDIR1_to_IX0p 〈x7,x2〉) I) (* [0x0072] in [X++=0x0072] *) +(* [0x186A] si puo' quindi enunciare che dopo 4+5+5+5=19 clk *) +(* PC<-0x186A X<-0x0073 *) +). + +(* creazione del processore+caricamento+impostazione registri *) +definition mTest_HCS08_MOV_status ≝ +λt:memory_impl. +λb1,b2,b3:byte8. + setweak_indX_16_reg HCS08 t (* H:X<-0x0071 *) + (set_pc_reg HCS08 t (* PC<-mTest_HCS08_prog *) + (start_of_mcu_version_HCS08 + MC9S08AW60 t + (load_from_source_at t (* carica b1-3 in RAM:mTest_HCS08_RAM *) + (load_from_source_at t (zero_memory t) (* carica source in ROM:mTest_HCS08_prog *) + mTest_HCS08_MOV_source mTest_HCS08_prog) + [ b1 ; b2 ; b3 ] mTest_HCS08_RAM) + (build_memory_type_of_mcu_version (FamilyHCS08 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 〈x0,x0〉 〈x7,x1〉). + +(* dimostrazione senza svolgimento degli stati, immediata *) +(* NB: la memoria e' cambiata e bisogna applicare eq_status *) +lemma ok_mTest_HCS08_MOV_full : +∀t:memory_impl. + eq_status HCS08 t + (match execute HCS08 t (TickOK ? (mTest_HCS08_MOV_status t 〈x0,x0〉 〈x0,x0〉 〈x0,x0〉)) 19 + with [ TickERR s _ ⇒ s | TickSUSP s _ ⇒ s | TickOK s ⇒ s ]) + (setweak_indX_16_reg HCS08 t (* H:X *) + (set_pc_reg HCS08 t (mTest_HCS08_MOV_status t 〈x3,xA〉 〈x3,xA〉 〈x3,xA〉) (* PC *) + (mk_word16 〈x1,x8〉 〈x6,xA〉)) + (mk_word16 〈x0,x0〉 〈x7,x3〉)) + [ 〈〈x0,x0〉:〈x7,x0〉〉 ; 〈〈x0,x0〉:〈x7,x1〉〉 ; 〈〈x0,x0〉:〈x7,x2〉〉 ] = true. + intro; + apply (eq_to_eqstatus_weak [ 〈〈x0,x0〉:〈x7,x0〉〉 ; 〈〈x0,x0〉:〈x7,x1〉〉 ; 〈〈x0,x0〉:〈x7,x2〉〉 ] HCS08 t + (match execute HCS08 t (TickOK ? (mTest_HCS08_MOV_status t 〈x0,x0〉 〈x0,x0〉 〈x0,x0〉)) 19 + with [ TickERR s _ ⇒ s | TickSUSP s _ ⇒ s | TickOK s ⇒ s ]) + (setweak_indX_16_reg HCS08 t (* H:X *) + (set_pc_reg HCS08 t (mTest_HCS08_MOV_status t 〈x3,xA〉 〈x3,xA〉 〈x3,xA〉) (* PC *) + (mk_word16 〈x1,x8〉 〈x6,xA〉)) + (mk_word16 〈x0,x0〉 〈x7,x3〉))); + elim t; + [ 1,2,3: normalize in ⊢ (? ? ? %); reflexivity + | 4,5,6: normalize in ⊢ (? ? ? %); reflexivity + | 7,8,9: normalize; reflexivity + ]. +qed. + +(* ************* *) +(* HCS08 ROL/ROR *) +(* ************* *) + +definition mTest_HCS08_ROL_ROR_source ≝ let m ≝ HCS08 in source_to_byte8 m ( +(* testa la logica di ROL/ROR e le modalita' IMM2,INHx *) +(* BEFORE: A=0x00 H:X=0x0000 PC=0x1860 Z=true *) +(* [0x1860] 3clk *) (compile m ? LDHX (maIMM2 〈〈x1,x2〉:〈x3,x4〉〉) I) @ +(* [0x1863] 2clk *) (compile m ? LDA (maIMM1 〈x5,x6〉) I) @ +(* [0x1865] 1clk *) (compile m ? ROL maINHA I) @ +(* [0x1866] 1clk *) (compile m ? ROL maINHX I) @ +(* [0x1867] 1clk *) (compile m ? ROR maINHA I) @ +(* [0x1868] 1clk *) (compile m ? ROR maINHX I) @ +(* [0x1869] 1clk *) (compile m ? CLR maINHA I) @ +(* [0x186A] 1clk *) (compile m ? CLR maINHX I) @ +(* [0x186B] 1clk *) (compile m ? CLR maINHH I) +(* [0x186C] si puo' quindi enunciare che dopo 3+2+1+1+1+1+1+1+1=12 clk *) +(* PC<-0x186C *) +). + +(* creazione del processore+caricamento+impostazione registri *) +definition mTest_HCS08_ROL_ROR_status ≝ +λt:memory_impl. + set_z_flag HCS08 t (* Z<-true *) + (setweak_indX_16_reg HCS08 t (* H:X<-0x0000 *) + (set_pc_reg HCS08 t (* PC<-mTest_HCS08_prog *) + (start_of_mcu_version_HCS08 + MC9S08AW60 t + (load_from_source_at t (zero_memory t) (* carica source in ROM:mTest_HCS08_prog *) + mTest_HCS08_ROL_ROR_source mTest_HCS08_prog) + (build_memory_type_of_mcu_version (FamilyHCS08 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 (mk_byte8 x0 x0) (mk_byte8 x0 x0))) + true. + +(* dimostrazione senza svolgimento degli stati, immediata *) +lemma ok_mTest_HCS08_ROL_ROR_full : + ∀t:memory_impl. + execute HCS08 t (TickOK ? (mTest_HCS08_ROL_ROR_status t)) 12 = + TickOK ? (set_pc_reg HCS08 t (* nuovo PC *) + (mTest_HCS08_ROL_ROR_status t) (mk_word16 〈x1,x8〉 〈x6,xC〉)). + intro; + elim t; + reflexivity. +qed. + +(* **************** *) +(* HCS08 CBEQx/DBNZ *) +(* **************** *) + +definition mTest_HCS08_CBEQ_DBNZ_source ≝ let m ≝ HCS08 in source_to_byte8 m ( +(* testa la logica di CBEQx/DBNZ e le modalita' xxx_and_IMM1 *) +(* BEFORE: H:X=0x006F SP=0x006F PC=0x1860 *) +(* [0x1860] 5clk *) (compile m ? CBEQA (maDIR1_and_IMM1 〈x7,x1〉 〈x0,x1〉) I) @ +(* [0x1863] 1clk *) (compile m ? NOP maINH I) @ (* eseguito: A≠[0x0071]=0x01 *) +(* [0x1864] 4clk *) (compile m ? CBEQA (maIMM1_and_IMM1 〈x0,x0〉 〈x0,x1〉) I) @ +(* [0x1867] 1clk *) (compile m ? NOP maINH I) @ (* non eseguito: A=0x00 *) +(* [0x1868] 4clk *) (compile m ? CBEQX (maIMM1_and_IMM1 〈x6,xF〉 〈x0,x1〉) I) @ +(* [0x186B] 1clk *) (compile m ? NOP maINH I) @ (* non eseguito: X=0x6F *) +(* [0x186C] 5clk *) (compile m ? CBEQA (maIX1p_and_IMM1 〈x0,x1〉 〈x0,x1〉) I) @ (* H:X++ *) +(* [0x186F] 1clk *) (compile m ? NOP maINH I) @ (* non eseguito: A=[X+0x01]=[0x0070]=0x00 *) +(* [0x1870] 5clk *) (compile m ? CBEQA (maIX0p_and_IMM1 〈x0,x1〉) I) @ (* H:X++ *) +(* [0x1872] 1clk *) (compile m ? NOP maINH I) @ (* non eseguito: A=[X]=[0x0070]=0x00 *) +(* [0x1873] 6clk *) (compile m ? CBEQA (maSP1_and_IMM1 〈x0,x2〉 〈x0,x1〉) I) @ +(* [0x1877] 1clk *) (compile m ? NOP maINH I) @ (* eseguito: A≠[SP+0x02]=[0x0071]=0x01 *) + +(* [0x1878] 7clk *) (compile m ? DBNZ (maDIR1_and_IMM1 〈x7,x2〉 〈x0,x1〉) I) @ +(* [0x187B] 1clk *) (compile m ? NOP maINH I) @ (* non eseguito: --[0x0072]=0x01≠0 *) +(* [0x187C] 4clk *) (compile m ? DBNZ (maINHA_and_IMM1 〈x0,x1〉) I) @ +(* [0x187E] 1clk *) (compile m ? NOP maINH I) @ (* non eseguito: --A=0xFF≠0 *) +(* [0x187F] 4clk *) (compile m ? DBNZ (maINHX_and_IMM1 〈x0,x1〉) I) @ +(* [0x1881] 1clk *) (compile m ? NOP maINH I) @ (* non eseguito: --X=0x70≠0 *) +(* [0x1882] 7clk *) (compile m ? DBNZ (maIX1_and_IMM1 〈x0,x2〉 〈x0,x1〉) I) @ +(* [0x1885] 1clk *) (compile m ? NOP maINH I) @ (* eseguito: --[X+0x02]=[0x0072]=0x00=0 *) +(* [0x1886] 6clk *) (compile m ? DBNZ (maIX0_and_IMM1 〈x0,x1〉) I) @ +(* [0x1888] 1clk *) (compile m ? NOP maINH I) @ (* non eseguito: --[X]=[0x0070]=0xFF≠0 *) +(* [0x1889] 8clk *) (compile m ? DBNZ (maSP1_and_IMM1 〈x0,x1〉 〈x0,x1〉) I) @ +(* [0x188D] 1clk *) (compile m ? NOP maINH I) (* non eseguito: --[SP+0x01]=[0x0070]=0xFE≠0 *) +(* [0x188E] si puo' quindi enunciare che dopo 5+1+4+4+5+5+6+1 (31) + 7+4+4+7+1+6+8 (37) =68 clk *) +(* A<-0xFF PC<-0x188E H:X<-0070 *) +). + +(* creazione del processore+caricamento+impostazione registri *) +definition mTest_HCS08_CBEQ_DBNZ_status ≝ +λt:memory_impl. +λb1,b2,b3:byte8. + setweak_sp_reg HCS08 t (* SP<-0x006F *) + (setweak_indX_16_reg HCS08 t (* H:X<-0x006F *) + (set_pc_reg HCS08 t (* PC<-mTest_HCS08_prog *) + (start_of_mcu_version_HCS08 + MC9S08AW60 t + (load_from_source_at t (* carica b1-3 in RAM:mTest_HCS08_RAM *) + (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_CBEQ_DBNZ_source mTest_HCS08_prog) + mTest_bytes mTest_HCS08_RAM) + [ b1 ; b2 ; b3 ] mTest_HCS08_RAM) + (build_memory_type_of_mcu_version (FamilyHCS08 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 (mk_byte8 x0 x0) (mk_byte8 x6 xF))) + (mk_word16 (mk_byte8 x0 x0) (mk_byte8 x6 xF)). + +(* dimostrazione senza svolgimento degli stati, immediata *) +(* NB: la memoria e' cambiata e bisogna applicare eq_status *) +lemma ok_mTest_HCS08_CBEQ_DBNZ_full : +∀t:memory_impl. + eq_status HCS08 t + (match execute HCS08 t (TickOK ? (mTest_HCS08_CBEQ_DBNZ_status t 〈x0,x0〉 〈x0,x1〉 〈x0,x2〉)) 68 + with [ TickERR s _ ⇒ s | TickSUSP s _ ⇒ s | TickOK s ⇒ s ]) + (set_acc_8_low_reg HCS08 t (* nuovo A *) + (set_pc_reg HCS08 t (* nuovo PC *) + (setweak_indX_16_reg HCS08 t (mTest_HCS08_CBEQ_DBNZ_status t 〈xF,xE〉 〈x0,x1〉 〈x0,x0〉) (* nuovo H:X *) + (mk_word16 〈x0,x0〉 〈x7,x0〉)) + (mk_word16 〈x1,x8〉 〈x8,xE〉)) + (mk_byte8 xF xF)) + [ 〈〈x0,x0〉:〈x7,x0〉〉 ; 〈〈x0,x0〉:〈x7,x1〉〉 ; 〈〈x0,x0〉:〈x7,x2〉〉 ] = true. + intro; + apply (eq_to_eqstatus_weak [ 〈〈x0,x0〉:〈x7,x0〉〉 ; 〈〈x0,x0〉:〈x7,x1〉〉 ; 〈〈x0,x0〉:〈x7,x2〉〉 ] HCS08 t + (match execute HCS08 t (TickOK ? (mTest_HCS08_CBEQ_DBNZ_status t 〈x0,x0〉 〈x0,x1〉 〈x0,x2〉)) 68 + with [ TickERR s _ ⇒ s | TickSUSP s _ ⇒ s | TickOK s ⇒ s ]) + (set_acc_8_low_reg HCS08 t (* nuovo A *) + (set_pc_reg HCS08 t (* nuovo PC *) + (setweak_indX_16_reg HCS08 t (mTest_HCS08_CBEQ_DBNZ_status t 〈xF,xE〉 〈x0,x1〉 〈x0,x0〉) (* nuovo H:X *) + (mk_word16 〈x0,x0〉 〈x7,x0〉)) + (mk_word16 〈x1,x8〉 〈x8,xE〉)) + (mk_byte8 xF xF))); + elim t; + [ 1,2,3: normalize in ⊢ (? ? ? %); reflexivity + | 4,5,6: normalize in ⊢ (? ? ? %); reflexivity + | 7,8,9: normalize; reflexivity + ]. +qed. + +(* ***************** *) +(* HCS08 BSETn/BCLRn *) +(* ***************** *) + +definition mTest_HCS08_BSETn_BCLRn_source ≝ let m ≝ HCS08 in source_to_byte8 m ( +(* testa la logica di BSETn/BCLRn e le modalita' DIRn *) +(* BEFORE: PC=0x1860 *) +(* [0x1860] 5clk *) (compile m ? BSETn (maDIRn o0 〈x7,x0〉) I) @ (* [0x0070]=0x01 *) +(* [0x1862] 5clk *) (compile m ? BSETn (maDIRn o1 〈x7,x0〉) I) @ (* [0x0070]=0x03 *) +(* [0x1864] 5clk *) (compile m ? BSETn (maDIRn o2 〈x7,x0〉) I) @ (* [0x0070]=0x07 *) +(* [0x1866] 5clk *) (compile m ? BSETn (maDIRn o3 〈x7,x0〉) I) @ (* [0x0070]=0x0F *) +(* [0x1868] 5clk *) (compile m ? BSETn (maDIRn o4 〈x7,x0〉) I) @ (* [0x0070]=0x1F *) +(* [0x186A] 5clk *) (compile m ? BSETn (maDIRn o5 〈x7,x0〉) I) @ (* [0x0070]=0x3F *) +(* [0x186C] 5clk *) (compile m ? BSETn (maDIRn o6 〈x7,x0〉) I) @ (* [0x0070]=0x7F *) +(* [0x186E] 5clk *) (compile m ? BSETn (maDIRn o7 〈x7,x0〉) I) @ (* [0x0070]=0xFF *) + +(* [0x1870] 5clk *) (compile m ? BCLRn (maDIRn o0 〈x7,x0〉) I) @ (* [0x0070]=0xFE *) +(* [0x1872] 5clk *) (compile m ? BCLRn (maDIRn o1 〈x7,x0〉) I) @ (* [0x0070]=0xFC *) +(* [0x1874] 5clk *) (compile m ? BCLRn (maDIRn o2 〈x7,x0〉) I) @ (* [0x0070]=0xF8 *) +(* [0x1876] 5clk *) (compile m ? BCLRn (maDIRn o3 〈x7,x0〉) I) @ (* [0x0070]=0xF0 *) +(* [0x1878] 5clk *) (compile m ? BCLRn (maDIRn o4 〈x7,x0〉) I) @ (* [0x0070]=0xE0 *) +(* [0x187A] 5clk *) (compile m ? BCLRn (maDIRn o5 〈x7,x0〉) I) @ (* [0x0070]=0xC0 *) +(* [0x187C] 5clk *) (compile m ? BCLRn (maDIRn o6 〈x7,x0〉) I) @ (* [0x0070]=0x80 *) +(* [0x187E] 5clk *) (compile m ? BCLRn (maDIRn o7 〈x7,x0〉) I) (* [0x0070]=0x00 *) +(* [0x1880] si puo' quindi enunciare che dopo 5+5+5+5+5+5+5+5 + 5+5+5+5+5+5+5+5 =80 clk *) +(* PC<-0x1880 *) +). + +(* creazione del processore+caricamento+impostazione registri *) +definition mTest_HCS08_BSETn_BCLRn_status ≝ +λt:memory_impl. +λb1:byte8. + set_pc_reg HCS08 t (* PC<-mTest_HCS08_prog *) + (start_of_mcu_version_HCS08 + MC9S08AW60 t + (load_from_source_at t (* carica b1 in RAM:mTest_HCS08_RAM *) + (load_from_source_at t (zero_memory t) (* carica source in ROM:mTest_HCS08_prog *) + mTest_HCS08_BSETn_BCLRn_source mTest_HCS08_prog) + [ b1 ] mTest_HCS08_RAM) + (build_memory_type_of_mcu_version (FamilyHCS08 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. + +(* dimostrazione senza svolgimento degli stati, immediata *) +(* NB: la memoria e' cambiata e bisogna applicare eq_status *) +lemma ok_mTest_HCS08_BSETn_BCLRn_full : +∀t:memory_impl. + eq_status HCS08 t + (match execute HCS08 t (TickOK ? (mTest_HCS08_BSETn_BCLRn_status t 〈x0,x0〉)) 80 + with [ TickERR s _ ⇒ s | TickSUSP s _ ⇒ s | TickOK s ⇒ s ]) + (set_pc_reg HCS08 t (mTest_HCS08_BSETn_BCLRn_status t 〈x0,x0〉) 〈〈x1,x8〉:〈x8,x0〉〉 (* nuovo PC *)) + [ 〈〈x0,x0〉:〈x7,x0〉〉 ; 〈〈x0,x0〉:〈x7,x1〉〉 ; 〈〈x0,x0〉:〈x7,x2〉〉 ] = true. + intro; + apply (eq_to_eqstatus_weak [ 〈〈x0,x0〉:〈x7,x0〉〉 ; 〈〈x0,x0〉:〈x7,x1〉〉 ; 〈〈x0,x0〉:〈x7,x2〉〉 ] HCS08 t + (match execute HCS08 t (TickOK ? (mTest_HCS08_BSETn_BCLRn_status t 〈x0,x0〉)) 80 + with [ TickERR s _ ⇒ s | TickSUSP s _ ⇒ s | TickOK s ⇒ s ]) + (set_pc_reg HCS08 t (mTest_HCS08_BSETn_BCLRn_status t 〈x0,x0〉) 〈〈x1,x8〉:〈x8,x0〉〉 (* nuovo PC *))); + elim t; + [ 1,2,3: normalize in ⊢ (? ? ? %); reflexivity + | 4,5,6: normalize in ⊢ (? ? ? %); reflexivity + | 7,8,9: normalize; reflexivity + ]. +qed. + +(* ******************* *) +(* HCS08 BRSETn/BRCLRn *) +(* ******************* *) + +definition mTest_HCS08_BRSETn_BRCLRn_source ≝ let m ≝ HCS08 in source_to_byte8 m ( +(* testa la logica di BRSETn/BRCLRn e le modalita' DIRn_and_IMM1 *) +(* BEFORE: va a testare [0x00C5]=0x55 PC=0x1860 *) +(* [0x1860] 5clk *) (compile m ? BRSETn (maDIRn_and_IMM1 o0 〈xC,x5〉 〈x0,x1〉) I) @ +(* [0x1863] 1clk *) (compile m ? NOP maINH I) @ +(* [0x1864] 5clk *) (compile m ? BRSETn (maDIRn_and_IMM1 o1 〈xC,x5〉 〈x0,x1〉) I) @ +(* [0x1867] 1clk *) (compile m ? NOP maINH I) @ +(* [0x1868] 5clk *) (compile m ? BRSETn (maDIRn_and_IMM1 o2 〈xC,x5〉 〈x0,x1〉) I) @ +(* [0x186B] 1clk *) (compile m ? NOP maINH I) @ +(* [0x186C] 5clk *) (compile m ? BRSETn (maDIRn_and_IMM1 o3 〈xC,x5〉 〈x0,x1〉) I) @ +(* [0x186F] 1clk *) (compile m ? NOP maINH I) @ +(* [0x1870] 5clk *) (compile m ? BRSETn (maDIRn_and_IMM1 o4 〈xC,x5〉 〈x0,x1〉) I) @ +(* [0x1873] 1clk *) (compile m ? NOP maINH I) @ +(* [0x1874] 5clk *) (compile m ? BRSETn (maDIRn_and_IMM1 o5 〈xC,x5〉 〈x0,x1〉) I) @ +(* [0x1877] 1clk *) (compile m ? NOP maINH I) @ +(* [0x1878] 5clk *) (compile m ? BRSETn (maDIRn_and_IMM1 o6 〈xC,x5〉 〈x0,x1〉) I) @ +(* [0x187B] 1clk *) (compile m ? NOP maINH I) @ +(* [0x187C] 5clk *) (compile m ? BRSETn (maDIRn_and_IMM1 o7 〈xC,x5〉 〈x0,x1〉) I) @ +(* [0x187F] 1clk *) (compile m ? NOP maINH I) @ + +(* [0x1880] 5clk *) (compile m ? BRCLRn (maDIRn_and_IMM1 o0 〈xC,x5〉 〈x0,x1〉) I) @ +(* [0x1883] 1clk *) (compile m ? NOP maINH I) @ +(* [0x1884] 5clk *) (compile m ? BRCLRn (maDIRn_and_IMM1 o1 〈xC,x5〉 〈x0,x1〉) I) @ +(* [0x1887] 1clk *) (compile m ? NOP maINH I) @ +(* [0x1888] 5clk *) (compile m ? BRCLRn (maDIRn_and_IMM1 o2 〈xC,x5〉 〈x0,x1〉) I) @ +(* [0x188B] 1clk *) (compile m ? NOP maINH I) @ +(* [0x188C] 5clk *) (compile m ? BRCLRn (maDIRn_and_IMM1 o3 〈xC,x5〉 〈x0,x1〉) I) @ +(* [0x188F] 1clk *) (compile m ? NOP maINH I) @ +(* [0x1890] 5clk *) (compile m ? BRCLRn (maDIRn_and_IMM1 o4 〈xC,x5〉 〈x0,x1〉) I) @ +(* [0x1893] 1clk *) (compile m ? NOP maINH I) @ +(* [0x1894] 5clk *) (compile m ? BRCLRn (maDIRn_and_IMM1 o5 〈xC,x5〉 〈x0,x1〉) I) @ +(* [0x1897] 1clk *) (compile m ? NOP maINH I) @ +(* [0x1898] 5clk *) (compile m ? BRCLRn (maDIRn_and_IMM1 o6 〈xC,x5〉 〈x0,x1〉) I) @ +(* [0x189B] 1clk *) (compile m ? NOP maINH I) @ +(* [0x189C] 5clk *) (compile m ? BRCLRn (maDIRn_and_IMM1 o7 〈xC,x5〉 〈x0,x1〉) I) @ +(* [0x189F] 1clk *) (compile m ? NOP maINH I) + +(* [0x18A0] si puo' quindi enunciare che dopo 80+8=88 clk + (vengono eseguiti 16*5 test, meta' BRSETn/BRCLRn saltano *) +(* PC<-0x18A0 *) +). + +(* creazione del processore+caricamento+impostazione registri *) +definition mTest_HCS08_BRSETn_BRCLRn_status ≝ +λt:memory_impl. + set_pc_reg HCS08 t (* PC<-mTest_HCS08_prog *) + (start_of_mcu_version_HCS08 + MC9S08AW60 t + (load_from_source_at t + (load_from_source_at t (zero_memory t) (* carica mTest_bytes in RAM:mTest_HCS08_RAM *) + mTest_HCS08_BRSETn_BRCLRn_source mTest_HCS08_prog) (* carica source in ROM:mTest_HCS08_prog *) + mTest_bytes mTest_HCS08_RAM) + (build_memory_type_of_mcu_version (FamilyHCS08 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. + +(* dimostrazione senza svolgimento degli stati, immediata *) +lemma ok_mTest_HCS08_BRSETn_BRCLRn_full : + ∀t:memory_impl. + execute HCS08 t (TickOK ? (mTest_HCS08_BRSETn_BRCLRn_status t)) 88 = + TickOK ? (set_pc_reg HCS08 t (mTest_HCS08_BRSETn_BRCLRn_status t) (* nuovo PC *) + (mk_word16 〈x1,x8〉 〈xA,x0〉)). + intro; + elim t; + reflexivity. +qed. + +(* *************** *) +(* RS08 X,D[X],TNY *) +(* *************** *) + +definition mTest_RS08_TNY_source ≝ let m ≝ RS08 in source_to_byte8 m ( +(* testa la logica RS08 X,D[X] le modalita' TNY *) +(* NB: il meccanismo utilizzato e' quello complesso dell'RS08 + fare riferimento alle spiegazioni in STATUS/LOAD_WRITE *) +(* X=20 PS=0 *) +(* [0x3800] 3clk *) (compile m ? ADD (maTNY xD) I) @ (* ... +[0x000D]=0x0C *) +(* [0x3801] 3clk *) (compile m ? ADD (maTNY xE) I) @ (* ... +D[X]=[0x0020]=0x1F *) +(* [0x3802] 3clk *) (compile m ? ADD (maTNY xF) I) @ (* ... +X=0x20 *) +(* [0x3803] 3clk *) (compile m ? ADD (maDIR1 〈xC,xF〉) I) @ (* ... +X=0x20 *) +(* [0x3805] 3clk *) (compile m ? ADD (maDIR1 〈xC,xE〉) I) (* ... +[0x000E]=0x0D *) +(* [0x3807] si puo' quindi enunciare che dopo 15 clk + A<-0x78 PC<-0x3807 *) +). + +(* creazione del processore+caricamento+impostazione registri *) +definition mTest_RS08_TNY_status ≝ +λt:memory_impl. + setweak_x_map RS08 t (* X<-0x20 *) + (setweak_ps_map RS08 t (* PS<-0x00 *) + (set_pc_reg RS08 t (* PC<-mTest_RS08_prog *) + (start_of_mcu_version_RS08 + MC9RS08KA2 t + (load_from_source_at t (* carica mTest_bytes in RAM:mTest_RS08_RAM *) + (load_from_source_at t (zero_memory t) (* carica source in ROM:mTest_RS08_prog *) + mTest_RS08_TNY_source mTest_RS08_prog) + mTest_bytes 〈〈x0,x0〉:〈x0,x1〉〉) + (build_memory_type_of_mcu_version (FamilyRS08 MC9RS08KA2) 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_RS08_prog) + (mk_byte8 x0 x0)) + (mk_byte8 x2 x0). + +(* dimostrazione senza svolgimento degli stati, immediata *) +lemma ok_mTest_RS08_TNY_full : + ∀t:memory_impl. + execute RS08 t (TickOK ? (mTest_RS08_TNY_status t)) 15 = + TickOK ? (set_acc_8_low_reg RS08 t (* nuovo A *) + (set_pc_reg RS08 t (mTest_RS08_TNY_status t) (* nuovo PC *) + (mk_word16 〈x3,x8〉 〈x0,x7〉)) + (mk_byte8 x7 x8)). + intro; + elim t; + reflexivity. +qed. + +(* *********** *) +(* RS08 PS,SRT *) +(* *********** *) + +definition mTest_RS08_SRT_source ≝ let m ≝ RS08 in source_to_byte8 m ( +(* testa la logica RS08 PS le modalita' SRT *) +(* NB: il meccanismo utilizzato e' quello complesso dell'RS08 + fare riferimento alle spiegazioni in STATUS/LOAD_WRITE *) +(* X=0x1F PS=0xFE Z=1 *) +(* [0x3800] 3clk *) (compile m ? LDA (maSRT t1F) I) @ (* A<-PS *) +(* [0x3801] 2clk *) (compile m ? SUB (maIMM1 〈xF,xE〉) I) @ (* risulta 0 *) +(* [0x3803] 3clk *) (compile m ? BEQ (maIMM1 〈x0,x1〉) I) @ (* salta *) +(* [0x3805] 1clk *) (compile m ? NOP maINH I) @ + +(* [0x3806] 3clk *) (compile m ? LDA (maSRT t0E) I) @ (* A<-PS *) +(* [0x3807] 2clk *) (compile m ? SUB (maIMM1 〈xF,xE〉) I) @ (* risulta 0 *) +(* [0x3809] 3clk *) (compile m ? BEQ (maIMM1 〈x0,x1〉) I) @ (* salta *) +(* [0x380B] 1clk *) (compile m ? NOP maINH I) @ + +(* [0x380C] 3clk *) (compile m ? LDA (maDIR1 〈xC,x3〉) I) @ (* A<-[0x00C3]=[0x3F83]=0x83 *) +(* [0x380E] 2clk *) (compile m ? SUB (maIMM1 〈x8,x3〉) I) @ (* risulta 0 *) +(* [0x3810] 3clk *) (compile m ? BEQ (maIMM1 〈x0,x1〉) I) @ (* salta *) +(* [0x3812] 1clk *) (compile m ? NOP maINH I) +(* [0x3813] si puo' quindi enunciare che dopo 24 clk + PC<-0x3813 *) +). + +(* creazione del processore+caricamento+impostazione registri *) +definition mTest_RS08_SRT_status ≝ +λt:memory_impl. + setweak_x_map RS08 t (* X<-0x1F *) + (setweak_ps_map RS08 t (* PS<-0xFE *) + (set_z_flag RS08 t (* Z<-true *) + (set_pc_reg RS08 t (* PC<-mTest_RS08_prog *) + (start_of_mcu_version_RS08 + MC9RS08KA2 t + (load_from_source_at t (* carica mTest_bytes in ROM:mTest_RS08_data *) + (load_from_source_at t (zero_memory t) (* carica source in ROM:mTest_RS08_prog *) + mTest_RS08_SRT_source mTest_RS08_prog) + mTest_bytes mTest_RS08_data) + (build_memory_type_of_mcu_version (FamilyRS08 MC9RS08KA2) 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_RS08_prog) + true) + (mk_byte8 xF xE)) + (mk_byte8 x1 xF). + +(* dimostrazione senza svolgimento degli stati, immediata *) +lemma ok_mTest_RS08_SRT_full : + ∀t:memory_impl. + execute RS08 t (TickOK ? (mTest_RS08_SRT_status t)) 24 = + TickOK ? (set_pc_reg RS08 t (mTest_RS08_SRT_status t) (* nuovo PC *) + (mk_word16 〈x3,x8〉 〈x1,x3〉)). + intro; + elim t; + reflexivity. +qed. + +(* ********************* *) +(* TEOREMA MULT PER RS08 *) +(* ********************* *) + +definition mTest_RS08_mult_source ≝ let m ≝ RS08 in source_to_byte8 m ( +(* + ZH:ZL=X*Y con [0x0020-0x004F] X ≝ [0x0020] Y ≝ [0x0021] ZH ≝ [0x0022] ZL ≝ [0x0023] +*) +(* [0x3800] ZH <- 0 3clk *) (compile m ? CLR (maDIR1 〈x2,x2〉) I) @ +(* [0x3802] ZL <- 0 3clk *) (compile m ? CLR (maDIR1 〈x2,x3〉) I) @ +(* [0x3804] (l1) A <- Y 3clk *) (compile m ? LDA (maDIR1 〈x2,x1〉) I) @ +(* [0x3806] A=0 goto l2 3clk *) (compile m ? BEQ (maIMM1 〈x0,xE〉) I) @ +(* [0x3808] A <- ZL 3clk *) (compile m ? LDA (maDIR1 〈x2,x3〉) I) @ +(* [0x380A] Y -- 5clk *) (compile m ? DEC (maDIR1 〈x2,x1〉) I) @ +(* [0x380C] A += X 3clk *) (compile m ? ADD (maDIR1 〈x2,x0〉) I) @ +(* [0x380E] C=0 goto l3 3clk *) (compile m ? BCC (maIMM1 〈x0,x2〉) I) @ +(* [0x3810] ZH ++ 5clk *) (compile m ? INC (maDIR1 〈x2,x2〉) I) @ +(* [0x3812] (l3) ZL <- A 3clk *) (compile m ? STA (maDIR1 〈x2,x3〉) I) @ +(* [0x3814] goto l1 3clk *) (compile m ? BRA (maIMM1 〈xE,xE〉) I) +(* [0x3816] (l2) si puo' quindi enunciare che + - il caso base X * 0 richiede 12 cicli + - bisogna aggiungere Y * 26 cicli, Y>0 + - bisogna aggiungere ZH * 5 cicli, X * Y > 0xFF *) +). + +(* creazione del processore+caricamento+impostazione registri *) +definition mTest_RS08_mult_status ≝ +λt:memory_impl. +λb1,b2,b3,b4:byte8. + set_z_flag RS08 t (* Z<-true *) + (set_pc_reg RS08 t (* PC<-mTest_RS08_prog *) + (start_of_mcu_version_RS08 + MC9RS08KA2 t + (load_from_source_at t (* carica X,Y,ZH,ZL:mTest_RS08_RAM *) + (load_from_source_at t (zero_memory t) (* carica source in ROM:mTest_RS08_prog *) + mTest_RS08_mult_source mTest_RS08_prog) + [ b1 ; b2 ; b3 ; b4 ] mTest_RS08_RAM) + (build_memory_type_of_mcu_version (FamilyRS08 MC9RS08KA2) 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_RS08_prog) + true. + +(* parametrizzazione dell'enunciato del teorema mult *) +(* NB: la memoria e' cambiata e bisogna applicare eq_status *) +definition ok_mTest_RS08_mult_full_aux ≝ +λt:memory_impl.λX,Y:byte8. + eq_status RS08 t + (match execute RS08 t (TickOK ? (mTest_RS08_mult_status t X Y 〈x0,x0〉 〈x0,x0〉)) + (12 + (26 * (nat_of_byte8 Y)) + (5 * (nat_of_byte8 (w16h (mul_b8 X Y))))) + (* FIXME: alla ALU azzero C perche' la funzione che ne descrive il valore finale e' MOLTO complessa *) + with [ TickERR s _ ⇒ s | TickSUSP s _ ⇒ s | TickOK s ⇒ set_c_flag RS08 t s false ]) + (set_pc_reg RS08 t (mTest_RS08_mult_status t X 〈x0,x0〉 (w16h (mul_b8 X Y)) (w16l (mul_b8 X Y))) 〈〈x3,x8〉:〈x1,x6〉〉) + (* controllo che coincidano X,Y,ZH,ZL *) + [ 〈〈x0,x0〉:〈x2,x0〉〉 ; 〈〈x0,x0〉:〈x2,x1〉〉 ; 〈〈x0,x0〉:〈x2,x2〉〉 ; 〈〈x0,x0〉:〈x2,x3〉〉 ] = true. + +lemma ok_mTest_RS08_mult_full : +let X ≝ 〈xF,xF〉 in +let Y ≝ 〈x1,xE〉 in + ∀t:memory_impl. + ok_mTest_RS08_mult_full_aux t X Y. + unfold ok_mTest_RS08_mult_full_aux; + intros 3; + apply (eq_to_eqstatus_weak [ 〈〈x0,x0〉:〈x2,x0〉〉 ; 〈〈x0,x0〉:〈x2,x1〉〉 ; 〈〈x0,x0〉:〈x2,x2〉〉 ; 〈〈x0,x0〉:〈x2,x3〉〉 ] RS08 t + (match execute RS08 t (TickOK ? (mTest_RS08_mult_status t X Y 〈x0,x0〉 〈x0,x0〉)) + (12 + (26 * (nat_of_byte8 Y)) + (5 * (nat_of_byte8 (w16h (mul_b8 X Y))))) + with [ TickERR s _ ⇒ s | TickSUSP s _ ⇒ s | TickOK s ⇒ set_c_flag RS08 t s false ]) + (set_pc_reg RS08 t (mTest_RS08_mult_status t X 〈x0,x0〉 (w16h (mul_b8 X Y)) (w16l (mul_b8 X Y))) 〈〈x3,x8〉:〈x1,x6〉〉)); + elim t; + [ 1,2,3: normalize in ⊢ (? ? ? %); reflexivity + | 4,5,6: normalize in ⊢ (? ? ? %); reflexivity + | 7,8,9: normalize; reflexivity + ]. +qed. + +(* ************************ *) +(* TEST SU GRANULARITA' BIT *) +(* ************************ *) + +definition mTest_bits_source ≝ let m ≝ HCS08 in source_to_byte8 m ( +(* BEFORE: va a testare [0x0070]=0x00 *) +(* [0x1860] 4clk *) (compile m ? MOV (maIMM1_to_DIR1 〈xF,xF〉 〈x7,x0〉) I) +(* [0x1863] *) +). + +(* creazione del processore+caricamento+impostazione registri *) +definition mTest_bits_status ≝ +λt:memory_impl. +λsub:oct. +λb:byte8. + setweak_n_flag HCS08 t (* N<-1 *) + (set_pc_reg HCS08 t (* PC<-mTest_HCS08_prog *) + (start_of_mcu_version_HCS08 + MC9S08AW60 t + (load_from_source_at t + (load_from_source_at t (zero_memory t) (* carica b in RAM:mTest_HCS08_RAM *) + mTest_bits_source mTest_HCS08_prog) (* carica source in ROM:mTest_HCS08_prog *) + [ b ] mTest_HCS08_RAM) + (check_update_bit t (* setta mTest_HCS08_RAM,o come ROM *) + (build_memory_type_of_mcu_version (FamilyHCS08 MC9S08AW60) t) + mTest_HCS08_RAM sub MEM_READ_ONLY) + (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) + true. + +(* dimostrazione senza svolgimento degli stati, immediata *) +lemma ok_mTest_bits_MEM_BITS_full : + ∀sub:oct. + execute HCS08 MEM_BITS (TickOK ? (mTest_bits_status MEM_BITS sub 〈x0,x0〉)) 4 = + TickOK ? (set_pc_reg HCS08 MEM_BITS (mTest_bits_status MEM_BITS sub (byte8_of_bits (setn_array8T sub ? (bits_of_byte8 〈xF,xF〉) false))) (* nuovo PC *) + (mk_word16 〈x1,x8〉 〈x6,x3〉)). + intro; + elim sub; + reflexivity. +qed. + +(* NB: la memoria e' cambiata e bisogna applicare eq_status *) +lemma ok_mTest_bits_MEM_FUNC_full : +∀sub:oct. + eq_status HCS08 MEM_FUNC + (match execute HCS08 MEM_FUNC (TickOK ? (mTest_bits_status MEM_FUNC sub 〈x0,x0〉)) 4 + with [ TickERR s _ ⇒ s | TickSUSP s _ ⇒ s | TickOK s ⇒ s ]) + (set_pc_reg HCS08 MEM_FUNC (mTest_bits_status MEM_FUNC sub 〈xF,xF〉) (* nuovo PC *) 〈〈x1,x8〉:〈x6,x3〉〉) + [ 〈〈x0,x0〉:〈x7,x0〉〉 ] = true. + intro; + apply (eq_to_eqstatus_weak [ 〈〈x0,x0〉:〈x7,x0〉〉 ] HCS08 MEM_FUNC + (match execute HCS08 MEM_FUNC (TickOK ? (mTest_bits_status MEM_FUNC sub 〈x0,x0〉)) 4 + with [ TickERR s _ ⇒ s | TickSUSP s _ ⇒ s | TickOK s ⇒ s ]) + (set_pc_reg HCS08 MEM_FUNC (mTest_bits_status MEM_FUNC sub 〈xF,xF〉) (* nuovo PC *) 〈〈x1,x8〉:〈x6,x3〉〉)); + normalize in ⊢ (? ? ? %); + reflexivity. +qed. + +lemma ok_mTest_bits_MEM_TREE_full : +∀sub:oct. + eq_status HCS08 MEM_TREE + (match execute HCS08 MEM_TREE (TickOK ? (mTest_bits_status MEM_TREE sub 〈x0,x0〉)) 4 + with [ TickERR s _ ⇒ s | TickSUSP s _ ⇒ s | TickOK s ⇒ s ]) + (set_pc_reg HCS08 MEM_TREE (mTest_bits_status MEM_TREE sub 〈xF,xF〉) (* nuovo PC *) 〈〈x1,x8〉:〈x6,x3〉〉) + [ 〈〈x0,x0〉:〈x7,x0〉〉 ] = true. + intro; + apply (eq_to_eqstatus_weak [ 〈〈x0,x0〉:〈x7,x0〉〉 ] HCS08 MEM_TREE + (match execute HCS08 MEM_TREE (TickOK ? (mTest_bits_status MEM_TREE sub 〈x0,x0〉)) 4 + with [ TickERR s _ ⇒ s | TickSUSP s _ ⇒ s | TickOK s ⇒ s ]) + (set_pc_reg HCS08 MEM_TREE (mTest_bits_status MEM_TREE sub 〈xF,xF〉) (* nuovo PC *) 〈〈x1,x8〉:〈x6,x3〉〉)); + normalize in ⊢ (? ? ? %); + reflexivity. +qed. +*) diff --git a/helm/software/matita/contribs/ng_assembly/freescale/model.ma b/helm/software/matita/contribs/ng_assembly/freescale/model.ma index 4f6d713d1..5dad70809 100755 --- a/helm/software/matita/contribs/ng_assembly/freescale/model.ma +++ b/helm/software/matita/contribs/ng_assembly/freescale/model.ma @@ -62,20 +62,21 @@ ndefinition HC08_mcu_model_rect : ΠP:HC08_mcu_model → Type.P MC68HC08AB16A (* modelli di HCS08 *) ninductive HCS08_mcu_model : Type ≝ - MC9S08GB60 : HCS08_mcu_model + MC9S08AW60 : HCS08_mcu_model +| MC9S08GB60 : HCS08_mcu_model (*..*). -ndefinition HCS08_mcu_model_ind : ΠP:HCS08_mcu_model → Prop.P MC9S08GB60 → Πh:HCS08_mcu_model.P h ≝ -λP:HCS08_mcu_model → Prop.λp:P MC9S08GB60.λh:HCS08_mcu_model. - match h with [ MC9S08GB60 ⇒ p ]. +ndefinition HCS08_mcu_model_ind : ΠP:HCS08_mcu_model → Prop.P MC9S08GB60 → P MC9S08AW60 → Πh:HCS08_mcu_model.P h ≝ +λP:HCS08_mcu_model → Prop.λp:P MC9S08GB60.λp1:P MC9S08AW60.λh:HCS08_mcu_model. + match h with [ MC9S08GB60 ⇒ p | MC9S08AW60 ⇒ p1 ]. -ndefinition HCS08_mcu_model_rec : ΠP:HCS08_mcu_model → Set.P MC9S08GB60 → Πh:HCS08_mcu_model.P h ≝ -λP:HCS08_mcu_model → Set.λp:P MC9S08GB60.λh:HCS08_mcu_model. - match h with [ MC9S08GB60 ⇒ p ]. +ndefinition HCS08_mcu_model_rec : ΠP:HCS08_mcu_model → Set.P MC9S08GB60 → P MC9S08AW60 → Πh:HCS08_mcu_model.P h ≝ +λP:HCS08_mcu_model → Set.λp:P MC9S08GB60.λp1:P MC9S08AW60.λh:HCS08_mcu_model. + match h with [ MC9S08GB60 ⇒ p | MC9S08AW60 ⇒ p1 ]. -ndefinition HCS08_mcu_model_rect : ΠP:HCS08_mcu_model → Type.P MC9S08GB60 → Πh:HCS08_mcu_model.P h ≝ -λP:HCS08_mcu_model → Type.λp:P MC9S08GB60.λh:HCS08_mcu_model. - match h with [ MC9S08GB60 ⇒ p ]. +ndefinition HCS08_mcu_model_rect : ΠP:HCS08_mcu_model → Type.P MC9S08GB60 → P MC9S08AW60 → Πh:HCS08_mcu_model.P h ≝ +λP:HCS08_mcu_model → Type.λp:P MC9S08GB60.λp1:P MC9S08AW60.λh:HCS08_mcu_model. + match h with [ MC9S08GB60 ⇒ p | MC9S08AW60 ⇒ p1 ]. (* modelli di RS08 *) ninductive RS08_mcu_model : Type ≝ @@ -187,7 +188,15 @@ ndefinition memory_type_of_FamilyHC08 ≝ (* memoria degli HCS08 *) ndefinition memory_type_of_FamilyHCS08 ≝ λm:HCS08_mcu_model.match m with - [ MC9S08GB60 ⇒ + [ MC9S08AW60 ⇒ + [ + (* astraggo molto *) + (* 0x0000-0x006F,0x1800-0x185F: sarebbe memory mapped IO *) + + triple ??? 〈〈x0,x0〉:〈x7,x0〉〉 〈〈x0,x8〉:〈x6,xF〉〉 MEM_READ_WRITE (* 2048B RAM *) + ; triple ??? 〈〈x0,x8〉:〈x7,x0〉〉 〈〈x1,x7〉:〈xF,xF〉〉 MEM_READ_ONLY (* 3984B FLASH *) + ; triple ??? 〈〈x1,x8〉:〈x6,x0〉〉 〈〈xF,xF〉:〈xF,xF〉〉 MEM_READ_ONLY (* 59296B FLASH *) ] + | MC9S08GB60 ⇒ [ (* astraggo molto *) (* 0x0000-0x006F,0x1800-0x185F: sarebbe memory mapped IO *) diff --git a/helm/software/matita/contribs/ng_assembly/test_errori.ma b/helm/software/matita/contribs/ng_assembly/test_errori.ma index 430df6e17..155b6073f 100644 --- a/helm/software/matita/contribs/ng_assembly/test_errori.ma +++ b/helm/software/matita/contribs/ng_assembly/test_errori.ma @@ -69,3 +69,98 @@ nlemma associative_plusb8 (*...*) *) + +include "compiler/ast_type_lemmas.ma". + +(* +nlemma symmetric_eqasttype_aux1 + : ∀x1,x2,y2.eq_nat (len_neList ast_type («£x1»)) (len_neList ast_type (x2§§y2)) = false. + #x1; #x2; #y2; ncases y2; nnormalize; + ##[ ##1: #t; napply (refl_eq ??) + ##| ##2: #t; #l; napply (refl_eq ??) + ##] +nqed. + +nlemma symmetric_eqasttype_aux2 + : ∀x1,y1,x2.eq_nat (len_neList ast_type (x1§§y1)) (len_neList ast_type («£x2»)) = false. + #x1; #y1; #x2; ncases y1; nnormalize; + ##[ ##1: #t; napply (refl_eq ??) + ##| ##2: #t; #l; napply (refl_eq ??) + ##] +nqed. + +ndefinition symmetric_eqasttype_aux3 ≝ +λnelSubType1,nelSubType2:ne_list ast_type. + match eq_nat (len_neList ast_type nelSubType1) (len_neList ast_type nelSubType2) + return λx.eq_nat (len_neList ast_type nelSubType1) (len_neList ast_type nelSubType2) = x → bool + with + [ true ⇒ λp:(eq_nat (len_neList ast_type nelSubType1) (len_neList ast_type nelSubType2) = true). + fold_right_neList2 ?? (λx1,x2,acc.(eq_ast_type x1 x2)⊗acc) + true nelSubType1 nelSubType2 + (eqnat_to_eq (len_neList ? nelSubType1) (len_neList ? nelSubType2) p) + | false ⇒ λp:(eq_nat (len_neList ast_type nelSubType1) (len_neList ast_type nelSubType2) = false).false + ] (refl_eq ? (eq_nat (len_neList ast_type nelSubType1) (len_neList ast_type nelSubType2))). + +nlemma symmetric_eqasttype : symmetricT ast_type bool eq_ast_type. + #t1; + napply (ast_type_ind ????? t1); + ##[ ##1: #b1; #t2; ncases t2; + ##[ ##1: #b2; nchange with ((eq_ast_base_type b1 b2) = (eq_ast_base_type b2 b1)); + nrewrite > (symmetric_eqastbasetype b1 b2); + napply (refl_eq ??) + ##| ##2: #tt; #n; nnormalize; napply (refl_eq ??) + ##| ##3: #l; nnormalize; napply (refl_eq ??) + ##] + ##| ##2: #tt1; #n1; #H; #t2; ncases t2; + ##[ ##2: #tt2; #n2; nchange with (((eq_ast_type tt1 tt2)⊗(eq_nat n1 n2)) = ((eq_ast_type tt2 tt1)⊗(eq_nat n2 n1))); + nrewrite > (H tt2); + nrewrite > (symmetric_eqnat n1 n2); + napply (refl_eq ??) + ##| ##1: #b2; nnormalize; napply (refl_eq ??) + ##| ##3: #l; nnormalize; napply (refl_eq ??) + ##] + ##| ##3: #tt1; #H; #t2; ncases t2; + ##[ ##3: #l; ncases l; + ##[ ##1: #tt2; nnormalize; nrewrite > (H tt2); napply (refl_eq ??) + ##| ##2: #tt2; #l1; + nchange with ( + (match eq_nat (len_neList ast_type «£tt1») (len_neList ast_type (tt2§§l1)) + return λx.eq_nat (len_neList ast_type «£tt1») (len_neList ast_type (tt2§§l1)) = x → bool + with + [ true ⇒ λp:(eq_nat (len_neList ast_type «£tt1») (len_neList ast_type (tt2§§l1)) = true). + fold_right_neList2 ?? (λx1,x2,acc.(eq_ast_type x1 x2)⊗acc) + true «£tt1» (tt2§§l1) + (eqnat_to_eq (len_neList ? «£tt1») (len_neList ? (tt2§§l1)) p) + | false ⇒ λp:(eq_nat (len_neList ast_type «£tt1») (len_neList ast_type (tt2§§l1)) = false).false + ] (refl_eq ? (eq_nat (len_neList ast_type «£tt1») (len_neList ast_type (tt2§§l1))))) = ?); + + (* eseguendo questa sequenza e' ok *) + nrewrite > (symmetric_eqasttype_aux1 tt1 tt2 l1); + nchange with ( + false = (match eq_nat (len_neList ast_type (tt2§§l1)) (len_neList ast_type «£tt1») + return λx.eq_nat (len_neList ast_type (tt2§§l1)) (len_neList ast_type «£tt1») = x → bool + with + [ true ⇒ λp:(eq_nat (len_neList ast_type (tt2§§l1)) (len_neList ast_type «£tt1») = true). + fold_right_neList2 ?? (λx1,x2,acc.(eq_ast_type x1 x2)⊗acc) + true (tt2§§l1) «£tt1» + (eqnat_to_eq (len_neList ? (tt2§§l1)) (len_neList ? «£tt1») p) + | false ⇒ λp:(eq_nat (len_neList ast_type (tt2§§l1)) (len_neList ast_type «£tt1») = false).false + ] (refl_eq ? (eq_nat (len_neList ast_type (tt2§§l1)) (len_neList ast_type «£tt1»))))); + nrewrite > (symmetric_eqasttype_aux2 tt2 l1 tt1); + nnormalize; + + (* se commentiamo invece la prima sequenza ed eseguiamo questa *) + (* come e' possibile che rigetti la seconda rewrite? *) + nchange with ( + ? = (match eq_nat (len_neList ast_type (tt2§§l1)) (len_neList ast_type «£tt1») + return λx.eq_nat (len_neList ast_type (tt2§§l1)) (len_neList ast_type «£tt1») = x → bool + with + [ true ⇒ λp:(eq_nat (len_neList ast_type (tt2§§l1)) (len_neList ast_type «£tt1») = true). + fold_right_neList2 ?? (λx1,x2,acc.(eq_ast_type x1 x2)⊗acc) + true (tt2§§l1) «£tt1» + (eqnat_to_eq (len_neList ? (tt2§§l1)) (len_neList ? «£tt1») p) + | false ⇒ λp:(eq_nat (len_neList ast_type (tt2§§l1)) (len_neList ast_type «£tt1») = false).false + ] (refl_eq ? (eq_nat (len_neList ast_type (tt2§§l1)) (len_neList ast_type «£tt1»))))); + nrewrite > (symmetric_eqasttype_aux1 tt1 tt2 l1); + nrewrite > (symmetric_eqasttype_aux2 tt2 l1 tt1); +*) diff --git a/helm/software/matita/contribs/ng_assembly/utility/string.ma b/helm/software/matita/contribs/ng_assembly/utility/string.ma index 227f9f478..d2a552901 100644 --- a/helm/software/matita/contribs/ng_assembly/utility/string.ma +++ b/helm/software/matita/contribs/ng_assembly/utility/string.ma @@ -21,7 +21,8 @@ (* ********************************************************************** *) include "utility/ascii.ma". -include "utility/utility.ma". +include "freescale/theory.ma". +include "freescale/nat.ma". (* ************************ *) (* MANIPOLAZIONE DI STRINGA *) @@ -30,14 +31,6 @@ include "utility/utility.ma". (* tipo pubblico *) ndefinition aux_str_type ≝ list ascii. -(* empty string *) -ndefinition empty_str ≝ nil ascii. - -(* is empty ? *) -ndefinition isNull_str ≝ -λstr:aux_str_type.match str with - [ nil ⇒ true | cons _ _ ⇒ false ]. - (* strcmp *) nlet rec eq_str (str,str':aux_str_type) ≝ match str with @@ -50,13 +43,6 @@ nlet rec eq_str (str,str':aux_str_type) ≝ ] ]. -(* strcat *) -ndefinition strCat_str ≝ -λstr,str':aux_str_type.str@str'. - -(* strlen *) -ndefinition strLen_str ≝ len_list ascii. - (* ************ *) (* STRINGA + ID *) (* ************ *) diff --git a/helm/software/matita/contribs/ng_assembly/utility/string_lemmas.ma b/helm/software/matita/contribs/ng_assembly/utility/string_lemmas.ma index 52b3b9f7a..3944d87ad 100755 --- a/helm/software/matita/contribs/ng_assembly/utility/string_lemmas.ma +++ b/helm/software/matita/contribs/ng_assembly/utility/string_lemmas.ma @@ -22,6 +22,7 @@ include "utility/string.ma". include "utility/ascii_lemmas2.ma". +include "freescale/nat_lemmas.ma". (* ************************ *) (* MANIPOLAZIONE DI STRINGA *) diff --git a/helm/software/matita/contribs/ng_assembly/utility/utility_lemmas.ma b/helm/software/matita/contribs/ng_assembly/utility/utility_lemmas.ma index 6ed8dea6c..557cdfbb1 100755 --- a/helm/software/matita/contribs/ng_assembly/utility/utility_lemmas.ma +++ b/helm/software/matita/contribs/ng_assembly/utility/utility_lemmas.ma @@ -58,7 +58,7 @@ nlemma nelist_destruct_cons_nil : ∀T.∀x1,x2:T.∀y1:ne_list T.ne_cons T x1 y napply I. nqed. -nlemma list_destruct_nil_cons : ∀T.∀x1,x2:T.∀y2:ne_list T.ne_nil T x1 = ne_cons T x2 y2 → False. +nlemma nelist_destruct_nil_cons : ∀T.∀x1,x2:T.∀y2:ne_list T.ne_nil T x1 = ne_cons T x2 y2 → False. #T; #x1; #x2; #y2; #H; nchange with (match ne_cons T x2 y2 with [ ne_nil _ ⇒ True | ne_cons a b ⇒ False ]); nrewrite < H; @@ -66,6 +66,119 @@ nlemma list_destruct_nil_cons : ∀T.∀x1,x2:T.∀y2:ne_list T.ne_nil T x1 = ne napply I. nqed. +nlemma symmetric_eqlenlist : ∀T.∀l1,l2:list T.len_list T l1 = len_list T l2 → len_list T l2 = len_list T l1. + #T; #l1; + napply (list_ind ???? l1); + ##[ ##1: #l2; ncases l2; nnormalize; + ##[ ##1: #H; napply (refl_eq ??) + ##| ##2: #h; #t; #H; nelim (nat_destruct_0_S ? H) + ##] + ##| ##2: #h; #l2; ncases l2; nnormalize; + ##[ ##1: #H; #l; #H1; nrewrite < H1; napply (refl_eq ??) + ##| ##2: #h; #l; #H; #l3; #H1; nrewrite < H1; napply (refl_eq ??) + ##] + ##] +nqed. + +nlemma symmetric_foldrightlist2_aux + : ∀T1,T2:Type.∀f:T1 → T1 → T2 → T2.∀acc:T2.∀l1,l2:list T1. + ∀H1:len_list T1 l1 = len_list T1 l2.∀H2:len_list T1 l2 = len_list T1 l1. + (∀x,y,z.f x y z = f y x z) → + fold_right_list2 T1 T2 f acc l1 l2 H1 = fold_right_list2 T1 T2 f acc l2 l1 H2. + #T1; #T2; #f; #acc; #l1; + napply (list_ind ???? l1); + ##[ ##1: #l2; ncases l2; + ##[ ##1: nnormalize; #H1; #H2; #H3; napply (refl_eq ??) + ##| ##2: #h; #l; #H1; #H2; #H3; + nchange in H1:(%) with (O = (S (len_list ? l))); + nelim (nat_destruct_0_S ? H1) + ##] + ##| ##2: #h3; #l3; #H; #l2; ncases l2; + ##[ ##1: #H1; #H2; #H3; nchange in H1:(%) with ((S (len_list ? l3)) = O); + nelim (nat_destruct_S_0 ? H1) + ##| ##2: #h4; #l4; #H1; #H2; #H3; + nchange in H1:(%) with ((S (len_list ? l3)) = (S (len_list ? l4))); + nchange in H2:(%) with ((S (len_list ? l4)) = (S (len_list ? l3))); + nchange with ((f h3 h4 (fold_right_list2 T1 T2 f acc l3 l4 (fold_right_list2_aux3 T1 h3 h4 l3 l4 ?))) = + (f h4 h3 (fold_right_list2 T1 T2 f acc l4 l3 (fold_right_list2_aux3 T1 h4 h3 l4 l3 ?)))); + nrewrite < (H l4 (fold_right_list2_aux3 T1 h3 h4 l3 l4 H1) (fold_right_list2_aux3 T1 h4 h3 l4 l3 H2) H3); + nrewrite > (H3 h3 h4 (fold_right_list2 T1 T2 f acc l3 l4 ?)); + napply (refl_eq ??) + ##] + ##] +nqed. + +nlemma symmetric_foldrightlist2 + : ∀T1,T2:Type.∀f:T1 → T1 → T2 → T2.∀acc:T2.∀l1,l2:list T1.∀H:len_list T1 l1 = len_list T1 l2. + (∀x,y,z.f x y z = f y x z) → + fold_right_list2 T1 T2 f acc l1 l2 H = fold_right_list2 T1 T2 f acc l2 l1 (symmetric_eqlenlist T1 l1 l2 H). + #T1; #T2; #f; #acc; #l1; #l2; #H; #H1; + nrewrite > (symmetric_foldrightlist2_aux T1 T2 f acc l1 l2 H (symmetric_eqlenlist T1 l1 l2 H) H1); + napply (refl_eq ??). +nqed. + +nlemma symmetric_eqlennelist : ∀T.∀l1,l2:ne_list T.len_neList T l1 = len_neList T l2 → len_neList T l2 = len_neList T l1. + #T; #l1; + napply (ne_list_ind ???? l1); + ##[ ##1: #h; #l2; ncases l2; nnormalize; + ##[ ##1: #H; #H1; napply (refl_eq ??) + ##| ##2: #h; #t; #H; nrewrite > H; napply (refl_eq ??) + ##] + ##| ##2: #h; #l2; ncases l2; nnormalize; + ##[ ##1: #h1; #H; #l; #H1; nrewrite < H1; napply (refl_eq ??) + ##| ##2: #h; #l; #H; #l3; #H1; nrewrite < H1; napply (refl_eq ??) + ##] + ##] +nqed. + +nlemma symmetric_foldrightnelist2_aux + : ∀T1,T2:Type.∀f:T1 → T1 → T2 → T2.∀acc:T2.∀l1,l2:ne_list T1. + ∀H1:len_neList T1 l1 = len_neList T1 l2.∀H2:len_neList T1 l2 = len_neList T1 l1. + (∀x,y,z.f x y z = f y x z) → + fold_right_neList2 T1 T2 f acc l1 l2 H1 = fold_right_neList2 T1 T2 f acc l2 l1 H2. + #T1; #T2; #f; #acc; #l1; + napply (ne_list_ind ???? l1); + ##[ ##1: #h; #l2; ncases l2; + ##[ ##1: #h1; nnormalize; #H1; #H2; #H3; nrewrite > (H3 h h1 acc); napply (refl_eq ??) + ##| ##2: #h1; #l; ncases l; + ##[ ##1: #h3; #H1; #H2; #H3; + nchange in H1:(%) with ((S O) = (S (S O))); + nelim (nat_destruct_0_S ? (nat_destruct_S_S ?? H1)) + ##| ##2: #h3; #l3; #H1; #H2; #H3; + nchange in H1:(%) with ((S O) = (S (S (len_neList ? l3)))); + nelim (nat_destruct_0_S ? (nat_destruct_S_S ?? H1)) + ##] + ##] + ##| ##2: #h3; #l3; #H; #l2; ncases l2; + ##[ ##1: #h4; ncases l3; + ##[ ##1: #h5; #H1; #H2; #H3; + nchange in H1:(%) with ((S (S O)) = (S O)); + nelim (nat_destruct_S_0 ? (nat_destruct_S_S ?? H1)) + ##| ##2: #h5; #l5; #H1; #H2; #H3; + nchange in H1:(%) with ((S (S (len_neList ? l5))) = (S O)); + nelim (nat_destruct_S_0 ? (nat_destruct_S_S ?? H1)) + ##] + ##| ##2: #h4; #l4; #H1; #H2; #H3; + nchange in H1:(%) with ((S (len_neList ? l3)) = (S (len_neList ? l4))); + nchange in H2:(%) with ((S (len_neList ? l4)) = (S (len_neList ? l3))); + nchange with ((f h3 h4 (fold_right_neList2 T1 T2 f acc l3 l4 (fold_right_neList2_aux3 T1 h3 h4 l3 l4 ?))) = + (f h4 h3 (fold_right_neList2 T1 T2 f acc l4 l3 (fold_right_neList2_aux3 T1 h4 h3 l4 l3 ?)))); + nrewrite < (H l4 (fold_right_neList2_aux3 T1 h3 h4 l3 l4 H1) (fold_right_neList2_aux3 T1 h4 h3 l4 l3 H2) H3); + nrewrite > (H3 h3 h4 (fold_right_neList2 T1 T2 f acc l3 l4 ?)); + napply (refl_eq ??) + ##] + ##] +nqed. + +nlemma symmetric_foldrightnelist2 + : ∀T1,T2:Type.∀f:T1 → T1 → T2 → T2.∀acc:T2.∀l1,l2:ne_list T1.∀H:len_neList T1 l1 = len_neList T1 l2. + (∀x,y,z.f x y z = f y x z) → + fold_right_neList2 T1 T2 f acc l1 l2 H = fold_right_neList2 T1 T2 f acc l2 l1 (symmetric_eqlennelist T1 l1 l2 H). + #T1; #T2; #f; #acc; #l1; #l2; #H; #H1; + nrewrite > (symmetric_foldrightnelist2_aux T1 T2 f acc l1 l2 H (symmetric_eqlennelist T1 l1 l2 H) H1); + napply (refl_eq ??). +nqed. + nlemma isbemptylist_to_isemptylist : ∀T,l.isb_empty_list T l = true → is_empty_list T l. #T; #l; ncases l;