freescale porting, work in progress

[helm.git] / helm / software / matita / contribs / ng_assembly / freescale_tests / medium_tests.ma

diff --git a/helm/software/matita/contribs/ng_assembly/freescale_tests/medium_tests.ma b/helm/software/matita/contribs/ng_assembly/freescale_tests/medium_tests.ma
index 0123dd8854b03dec2da6e11aab325a0670893c43..68db649b5eb516ababefae13d97d204616ca1a22 100755 (executable)
--- a/helm/software/matita/contribs/ng_assembly/freescale_tests/medium_tests.ma
+++ b/helm/software/matita/contribs/ng_assembly/freescale_tests/medium_tests.ma
@@ -157,7 +157,7 @@ nlemma dTest_HCS08_sReverse_dump_aux ≝
   (* parametri IN: t,H:X,strlen(string),string *)
   (TickOK ? (dTest_HCS08_sReverse_status t 〈x0,x0〉 〈〈x0,xD〉:〈x4,xB〉〉 (byte8_strlen string) string))
   (* tempo di esecuzione 42+79*n+5*(n>>9) *)
-  (42+(79*(len_list ? string))+(5*((len_list ? string)/512))) with
+  (nat42 + (nat79 * (len_list ? string))+(nat5 * ((len_list ? string) / nat512))) with
    [ TickERR s _ ⇒ None ?
    (* azzeramento tutta RAM tranne dati *)
    | TickSUSP s _ ⇒ None ? 
@@ -189,7 +189,7 @@ nlemma dTest_HCS08_sReverse_aux ≝
   (* parametri IN: t,H:X,strlen(string),string *)
   (TickOK ? (dTest_HCS08_sReverse_status t 〈x0,x0〉 〈〈x0,xD〉:〈x4,xB〉〉 (byte8_strlen string) string))
   (* tempo di esecuzione 42+79*n+5*(n>>9) *)
-  (42+(79*(len_list ? string))+(5*((len_list ? string)/512))) with
+  (nat42 + (nat79 * (len_list ? string))+(nat5 * ((len_list ? string) / nat512))) with
    [ TickERR s _ ⇒ None ?
    (* azzeramento tutta RAM tranne dati *)
    | TickSUSP s _ ⇒ None ? 
@@ -231,7 +231,7 @@ 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))
-  (42+(79*(len_list ? string))+(5*((len_list ? string)/512))) with
+  (nat42 + (nat79 * (len_list ? string))+(nat5 * ((len_list ? string) / nat512))) with
    [ TickERR s _ ⇒ None ?
    | TickSUSP s _ ⇒ None ? 
    | TickOK s ⇒ Some ? (set_mem_desc HCS08 MEM_TREE s (load_from_source_at MEM_TREE (mem_desc HCS08 MEM_TREE s) dTest_zeros 〈〈x0,xD〉:〈x0,x0〉〉))
@@ -409,7 +409,7 @@ nlemma dTest_HCS08_cSort_aux ≝
   (* parametri IN: t,A,H:X,strlen(string),string *)
   (TickOK ? (dTest_HCS08_cSort_status t true 〈x0,x0〉 〈〈x0,xF〉:〈x4,xC〉〉 (byte8_strlen string) string))
   (* tempo di esecuzione 25700+150*n *)
-  ((257*100)+(150*(len_list ? string))) with
+  (((nat256 + nat1) * nat100)+((nat50 * nat3) * (len_list ? string))) with
    [ TickERR s _ ⇒ None ?
    (* azzeramento tutta RAM tranne dati *)
    | TickSUSP s _ ⇒ Some ? (set_mem_desc HCS08 t s (load_from_source_at t (mem_desc HCS08 t s) dTest_zeros 〈〈x0,xD〉:〈x0,x0〉〉))
@@ -434,7 +434,7 @@ 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))
-  ((257*100)+(150*(len_list ? string))) with
+  (((nat256 + nat1) * nat100)+((nat50 * nat3) * (len_list ? string))) with
    [ TickERR s _ ⇒ None ?
    | TickSUSP s _ ⇒ Some ? (set_mem_desc HCS08 MEM_TREE s (load_from_source_at MEM_TREE (mem_desc HCS08 MEM_TREE s) dTest_zeros 〈〈x0,xD〉:〈x0,x0〉〉))
    | TickOK s ⇒ None ?
@@ -803,7 +803,7 @@ nlet rec dTest_HCS08_gNum_execute1 (m:mcu_type) (t:memory_impl) (s:tick_result (
   | TickSUSP s' susp ⇒ TickSUSP ? s' susp
   | TickOK s' ⇒ match n with
    [ O ⇒ TickOK ? s'
-   | S n' ⇒ dTest_HCS08_gNum_execute1 m t (execute m t (TickOK ? s') (ntot+2)) n' ntot ]
+   | S n' ⇒ dTest_HCS08_gNum_execute1 m t (execute m t (TickOK ? s') (ntot + nat2)) n' ntot ]
   ].
 
 (* esecuzione execute k*(n+1)*(n+2) *)
@@ -813,7 +813,7 @@ nlet rec dTest_HCS08_gNum_execute2 (m:mcu_type) (t:memory_impl) (s:tick_result (
   | TickSUSP s' susp ⇒ TickSUSP ? s' susp
   | TickOK s' ⇒ match n with
    [ O ⇒ TickOK ? s'
-   | S n' ⇒ dTest_HCS08_gNum_execute2 m t (dTest_HCS08_gNum_execute1 m t (TickOK ? s') (ntot+1) ntot) n' ntot ]
+   | S n' ⇒ dTest_HCS08_gNum_execute2 m t (dTest_HCS08_gNum_execute1 m t (TickOK ? s') (ntot + nat1) ntot) n' ntot ]
   ].
 
 (* esecuzione execute k*n*(n+1)*(n+2) *)
@@ -832,7 +832,7 @@ ndefinition dTest_HCS08_gNum_execute4 ≝
  match s with
   [ TickERR s' error ⇒ TickERR ? s' error
   | TickSUSP s' susp ⇒ TickSUSP ? s' susp
-  | TickOK s' ⇒ execute m t (dTest_HCS08_gNum_execute3 m t (TickOK ? s') 11 ntot) 80
+  | TickOK s' ⇒ execute m t (dTest_HCS08_gNum_execute3 m t (TickOK ? s') nat11 ntot) nat80
   ].
 
 (* parametrizzazione dell'enunciato del teorema parziale *)