X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Flibrary%2Ffreescale%2Fmedium_tests.ma;h=20a0da441095905c70ae6a5942766170fc130a7f;hb=09e3a050664b07c961a92bf16245a7345346f964;hp=41cc96ae9ccfcfe255853171d788a09758f3e990;hpb=5806e0aa438ae85f09c93c93ba9f53d9663d7420;p=helm.git

diff --git a/helm/software/matita/library/freescale/medium_tests.ma b/helm/software/matita/library/freescale/medium_tests.ma
index 41cc96ae9..20a0da441 100644
--- a/helm/software/matita/library/freescale/medium_tests.ma
+++ b/helm/software/matita/library/freescale/medium_tests.ma
@@ -24,11 +24,8 @@
 (*                    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 *)
 (* ************************ *)
@@ -117,7 +114,7 @@ let m ≝ HCS08 in source_to_byte8 m (
 (* [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 *)
  ).
 
@@ -157,8 +154,8 @@ lemma dTest_HCS08_sReverse_dump_aux ≝
  (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 ? 
@@ -166,7 +163,8 @@ lemma dTest_HCS08_sReverse_dump_aux ≝
    ] =
   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;
@@ -174,6 +172,7 @@ lemma dTest_HCS08_sReverse_dump :
  [ split; [ normalize in ⊢ (%); autobatch ] reflexivity ]
  reflexivity.
 qed.
+*)
 
 (* parametrizzazione dell'enunciato del teorema *)
 (* dimostrazione senza svolgimento degli stati *)
@@ -187,29 +186,84 @@ lemma dTest_HCS08_sReverse_aux ≝
  (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 *)
@@ -356,7 +410,7 @@ lemma dTest_HCS08_cSort_aux ≝
   ((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
@@ -364,11 +418,6 @@ lemma dTest_HCS08_cSort_aux ≝
    (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.
@@ -378,3 +427,43 @@ lemma dTest_HCS08_cSort :
  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.
+*)