(* data ultima modifica 15/11/2007 *)
(* ********************************************************************** *)
-set "baseuri" "cic:/matita/freescale/medium_tests/".
-
-(*include "/media/VIRTUOSO/freescale/medium_tests_tools.ma".*)
-include "freescale/medium_tests_tools.ma".
-
+include "freescale/medium_tests_lemmas.ma".
+
(* ************************ *)
(* HCS08GB60 String Reverse *)
(* ************************ *)
(* [0x1929] 22 BD BHI *-65 ; 18E8 *) (compile m ? BHI (maIMM1 〈xB,xD〉) I)
(* [0x192B] attraverso simulazione in CodeWarrior si puo' enunciare che dopo
- 42+79*n+(n>>9) ci sara' il reverse di n byte (PARI) e
+ 42+79*n+5*(n>>9) ci sara' il reverse di n byte (PARI) e
H:X=n/2 *)
).
(match execute HCS08 t
(* parametri IN: t,H:X,strlen(string),string *)
(TickOK ? (dTest_HCS08_sReverse_status t 〈〈x0,xD〉:〈x4,xB〉〉 (byte8_strlen string) string))
- (* tempo di esecuzione 25700+150*n *)
- (42+79*(byte8_strlen string)+((byte8_strlen string)/512)) with
+ (* tempo di esecuzione 42+79*n+5*(n>>9) *)
+ (42+79*(byte8_strlen string)+5*((byte8_strlen string)/512)) with
[ TickERR s _ ⇒ None ?
(* azzeramento tutta RAM tranne dati *)
| TickSUSP s _ ⇒ None ?
] =
Some ? (byte8_reverse string)).
-(* primo sbozzo: confronto esecuzione con hexdump... *)
+(* 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; [ normalize in ⊢ (%); autobatch ] reflexivity ]
reflexivity.
qed.
+*)
(* parametrizzazione dell'enunciato del teorema *)
(* dimostrazione senza svolgimento degli stati *)
(match execute HCS08 t
(* parametri IN: t,H:X,strlen(string),string *)
(TickOK ? (dTest_HCS08_sReverse_status t 〈〈x0,xD〉:〈x4,xB〉〉 (byte8_strlen string) string))
- (* tempo di esecuzione 25700+150*n *)
- (42+79*(byte8_strlen string)+((byte8_strlen string)/512)) with
+ (* tempo di esecuzione 42+79*n+5*(n>>9) *)
+ (42+79*(byte8_strlen string)+5*((byte8_strlen string)/512)) 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 (get_mem_desc HCS08 t s) dTest_bytes 〈〈x0,xD〉:〈x0,x0〉〉))
+ | TickOK s ⇒ Some ? (set_mem_desc HCS08 t s (load_from_source_at t (get_mem_desc HCS08 t s) dTest_zeros 〈〈x0,xD〉:〈x0,x0〉〉))
] =
Some ? (set_pc_reg HCS08 t
- (dTest_HCS08_sReverse_status t (fstT ?? (shr_w16 (byte8_strlen string))) (byte8_strlen string) (byte8_reverse string))
+ (dTest_HCS08_sReverse_status t (fst ?? (shr_w16 (byte8_strlen string))) (byte8_strlen string) (byte8_reverse string))
(mk_word16 (mk_byte8 x1 x9) (mk_byte8 x2 xB)))).
-(* dimostrazione senza svolgimento degli stati *)
-(* sembra corretta, ma non basta la memoria per arrivare in fondo con quelli grandi! *)
-(* NB: sono gia' pronti dei pattern piu' impegnativi in medium_tests_tool: *)
-(* dTest_random_32/64/128/256/512/1024/2048/3072 generati con Mathematica *)
-(* ex: dTest_HCS08_sReverse_aux MEM_TREE dTest_random_3072 sarebbe gia' un bell'obbiettivo! *)
+(*
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.
+*)
+
+definition sReverseCalc ≝
+λstring:list byte8.
+ match execute HCS08 MEM_TREE
+ (TickOK ? (dTest_HCS08_sReverse_status MEM_TREE 〈〈x0,xD〉:〈x4,xB〉〉 (byte8_strlen string) string))
+ (42+79*(byte8_strlen string)+5*((byte8_strlen string)/512)) with
+ [ TickERR s _ ⇒ None ?
+ | TickSUSP s _ ⇒ None ?
+ | 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 ≝
+λstring:list byte8.
+ Some ? (set_pc_reg HCS08 MEM_TREE
+ (dTest_HCS08_sReverse_status MEM_TREE (fst ?? (shr_w16 (byte8_strlen string))) (byte8_strlen string) (byte8_reverse string))
+ (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.
+
+(*
+lemma ver : sReverseCalc128 = sReverseNoCalc128.
reflexivity.
qed.
+*)
(* *********************** *)
(* HCS08GB60 Counting Sort *)
((nat_of_word16 〈〈x6,x4〉:〈x6,x4〉〉)+(nat_of_byte8 〈x9,x6〉)*(nat_of_word16 (byte8_strlen string))) with
[ TickERR s _ ⇒ None ?
(* azzeramento tutta RAM tranne dati *)
- | TickSUSP s _ ⇒ Some ? (set_mem_desc HCS08 t s (load_from_source_at t (get_mem_desc HCS08 t s) dTest_bytes 〈〈x0,xD〉:〈x0,x0〉〉))
+ | TickSUSP s _ ⇒ Some ? (set_mem_desc HCS08 t s (load_from_source_at t (get_mem_desc HCS08 t s) dTest_zeros 〈〈x0,xD〉:〈x0,x0〉〉))
| TickOK s ⇒ None ?
] =
Some ? (set_pc_reg HCS08 t
(mk_word16 (mk_byte8 x1 x9) (mk_byte8 x3 xC)))).
(* dimostrazione senza svolgimento degli stati *)
-(* sembra corretta, ma non basta la memoria per arrivare in fondo nemmeno col piccolo! *)
-(* NB: sono gia' pronti dei pattern piu' impegnativi in medium_tests_tool: *)
-(* dTest_random_32/64/128/256/512/1024/2048/3072 generati con Mathematica *)
-(* ex: dTest_HCS08_cSort_aux MEM_TREE dTest_random_3072 sarebbe gia' un bell'obbiettivo! *)
-
(*
lemma dTest_HCS08_cSort :
dTest_HCS08_cSort_aux MEM_TREE dTest_random_32.
reflexivity.
qed.
*)
+
+definition cSortCalc ≝
+λstring:list byte8.
+ match execute HCS08 MEM_TREE
+ (TickOK ? (dTest_HCS08_cSort_status MEM_TREE 〈x0,x0〉 〈〈x0,xF〉:〈x4,xC〉〉 (byte8_strlen string) string))
+ ((nat_of_word16 〈〈x6,x4〉:〈x6,x4〉〉)+(nat_of_byte8 〈x9,x6〉)*(nat_of_word16 (byte8_strlen string))) with
+ [ TickERR s _ ⇒ None ?
+ | TickSUSP s _ ⇒ Some ? (set_mem_desc HCS08 MEM_TREE s (load_from_source_at MEM_TREE (get_mem_desc HCS08 MEM_TREE s) dTest_zeros 〈〈x0,xD〉:〈x0,x0〉〉))
+ | TickOK s ⇒ None ?
+ ].
+
+definition cSortNoCalc ≝
+λstring:list byte8.
+ Some ? (set_pc_reg HCS08 MEM_TREE
+ (dTest_HCS08_cSort_status MEM_TREE 〈xF,xF〉 〈〈x0,x1〉:〈x0,x0〉〉 (byte8_strlen string) (byte8_list_ordering string))
+ (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.
+
+(*
+lemma ver : cSortCalc32 = cSortNoCalc32.
+ reflexivity.
+qed.
+*)
projects / helm.git / blobdiff