helm/software/matita/library/freescale/medium_tests.ma

   1 (**************************************************************************)
   2 (*       ___                                                              *)
   3 (*      ||M||                                                             *)
   4 (*      ||A||       A project by Andrea Asperti                           *)
   5 (*      ||T||                                                             *)
   6 (*      ||I||       Developers:                                           *)
   7 (*      ||T||         The HELM team.                                      *)
   8 (*      ||A||         http://helm.cs.unibo.it                             *)
   9 (*      \   /                                                             *)
  10 (*       \ /        This file is distributed under the terms of the       *)
  11 (*        v         GNU General Public License Version 2                  *)
  12 (*                                                                        *)
  13 (**************************************************************************)
  14
  15 (* ********************************************************************** *)
  16 (*                           Progetto FreeScale                           *)
  17 (*                                                                        *)
  18 (* Sviluppato da:                                                         *)
  19 (*   Cosimo Oliboni, oliboni@cs.unibo.it                                  *)
  20 (*                                                                        *)
  21 (* Questo materiale fa parte della tesi:                                  *)
  22 (*   "Formalizzazione Interattiva dei Microcontroller a 8bit FreeScale"   *)
  23 (*                                                                        *)
  24 (*                    data ultima modifica 15/11/2007                     *)
  25 (* ********************************************************************** *)
  26
  27 include "freescale/medium_tests_lemmas.ma".
  28
  29 (* ************************ *)
  30 (* HCS08GB60 String Reverse *)
  31 (* ************************ *)
  32
  33 (* versione ridotta, in cui non si riazzerano gli elementi di counters *)
  34 definition dTest_HCS08_sReverse_source : word16 → (list byte8) ≝
  35 λelems:word16.
  36 let m ≝ HCS08 in source_to_byte8 m (
  37 (* BEFORE: A=0x00 H:X=0x0D4B SP=0x0D4A PC=0x18E0 Z=true *)
  38
  39 (* static unsigned char dati[3072]={...};
  40
  41    void swap(unsigned char *a, unsigned char *b)
  42     { unsigned char tmp=*a; *a=*b; *b=tmp; return; } *)
  43
  44 (* [0x18C8]    allineamento *) (compile m ? NOP maINH I) @
  45
  46 (* [0x18C9]       PSHX      *) (compile m ? PSHX maINH I) @
  47 (* [0x18CA]       PSHH      *) (compile m ? PSHH maINH I) @
  48 (* [0x18CB]       LDHX 5,SP *) (compile m ? LDHX (maSP1 〈x0,x5〉) I) @
  49 (* [0x18CE]       LDA ,X    *) (compile m ? LDA maIX0 I) @
  50 (* [0x18CF]       LDHX 1,SP *) (compile m ? LDHX (maSP1 〈x0,x1〉) I) @
  51 (* [0x18D2]       PSHA      *) (compile m ? PSHA maINH I) @
  52 (* [0x18D3]       LDA ,X    *) (compile m ? LDA maIX0 I) @
  53 (* [0x18D4]       LDHX 6,SP *) (compile m ? LDHX (maSP1 〈x0,x6〉) I) @
  54 (* [0x18D7]       STA ,X    *) (compile m ? STA maIX0 I) @
  55 (* [0x18D8]       LDHX 2,SP *) (compile m ? LDHX (maSP1 〈x0,x2〉) I) @
  56 (* [0x18DB]       PULA      *) (compile m ? PULA maINH I) @
  57 (* [0x18DC]       STA ,X    *) (compile m ? STA maIX0 I) @
  58 (* [0x18DD]       AIS #2    *) (compile m ? AIS (maIMM1 〈x0,x2〉) I) @
  59 (* [0x18DF]       RTS       *) (compile m ? RTS maINH I) @
  60
  61 (* void main(void)
  62    {
  63    unsigned int pos=0,limit=0;
  64
  65    for(limit=3072;pos<(limit/2);pos++)
  66     { swap(&dati[pos],&dati[limit-pos-1]); } *)
  67
  68 (* [0x18E0]       LDHX #LUNG      *) (compile m ? LDHX (maIMM2 elems) I) @
  69 (* [0x18E3]       STHX 4,SP       *) (compile m ? STHX (maSP1 〈x0,x4〉) I) @
  70 (* [0x18E6] 20 32 BRA *+52 ; 191A *) (compile m ? BRA (maIMM1 〈x3,x2〉) I) @
  71 (* [0x18E8]       TSX             *) (compile m ? TSX maINH I) @
  72 (* [0x18E9]       LDA 2,X         *) (compile m ? LDA (maIX1 〈x0,x2〉) I) @
  73 (* [0x18EB]       ADD #0x00       *) (compile m ? ADD (maIMM1 〈x0,x0〉) I) @
  74 (* [0x18ED]       PSHA            *) (compile m ? PSHA maINH I) @
  75 (* [0x18EE]       LDA 1,X         *) (compile m ? LDA (maIX1 〈x0,x1〉) I) @
  76 (* [0x18F0]       ADC #0x01       *) (compile m ? ADC (maIMM1 〈x0,x1〉) I) @
  77 (* [0x18F2]       PSHA            *) (compile m ? PSHA maINH I) @
  78 (* [0x18F3]       LDA 4,X         *) (compile m ? LDA (maIX1 〈x0,x4〉) I) @
  79 (* [0x18F5]       SUB 2,X         *) (compile m ? SUB (maIX1 〈x0,x2〉) I) @
  80 (* [0x18F7]       STA ,X          *) (compile m ? STA maIX0 I) @
  81 (* [0x18F8]       LDA 3,X         *) (compile m ? LDA (maIX1 〈x0,x3〉) I) @
  82 (* [0x18FA]       SBC 1,X         *) (compile m ? SBC (maIX1 〈x0,x1〉) I) @
  83 (* [0x18FC]       PSHA            *) (compile m ? PSHA maINH I) @
  84 (* [0x18FD]       LDX ,X          *) (compile m ? LDX maIX0 I) @
  85 (* [0x18FE]       PULH            *) (compile m ? PULH maINH I) @
  86 (* [0x18FF]       AIX #-1         *) (compile m ? AIX (maIMM1 〈xF,xF〉) I) @
  87 (* [0x1901]       TXA             *) (compile m ? TXA maINH I) @
  88 (* [0x1902]       ADD #0x00       *) (compile m ? ADD (maIMM1 〈x0,x0〉) I) @
  89 (* [0x1904]       PSHH            *) (compile m ? PSHH maINH I) @
  90 (* [0x1905]       TSX             *) (compile m ? TSX maINH I) @
  91 (* [0x1906]       STA 3,X         *) (compile m ? STA (maIX1 〈x0,x3〉) I) @
  92 (* [0x1908]       PULA            *) (compile m ? PULA maINH I) @
  93 (* [0x1909]       ADC #0x01       *) (compile m ? ADC (maIMM1 〈x0,x1〉) I) @
  94 (* [0x190B]       LDX 3,X         *) (compile m ? LDX (maIX1 〈x0,x3〉) I) @
  95 (* [0x190D]       PSHA            *) (compile m ? PSHA maINH I) @
  96 (* [0x190E]       PULH            *) (compile m ? PULH maINH I) @
  97 (* [0x190F] AD B8 BSR *-70 ; 18C9 *) (compile m ? BSR (maIMM1 〈xB,x8〉) I) @
  98 (* [0x1911]       AIS #2          *) (compile m ? AIS (maIMM1 〈x0,x2〉) I) @
  99 (* [0x1913]       TSX             *) (compile m ? TSX maINH I) @
 100 (* [0x1914]       INC 2,X         *) (compile m ? INC (maIX1 〈x0,x2〉) I) @
 101 (* [0x1916] 26 02 BNE *+4 ; 191A  *) (compile m ? BNE (maIMM1 〈x0,x2〉) I) @
 102 (* [0x1918]       INC 1,X         *) (compile m ? INC (maIX1 〈x0,x1〉) I) @
 103 (* [0x191A]       TSX             *) (compile m ? TSX maINH I) @
 104 (* [0x191B]       LDA 3,X         *) (compile m ? LDA (maIX1 〈x0,x3〉) I) @
 105 (* [0x191D]       PSHA            *) (compile m ? PSHA maINH I) @
 106 (* [0x191E]       PULH            *) (compile m ? PULH maINH I) @
 107 (* [0x191F]       LSRA            *) (compile m ? LSR maINHA I) @
 108 (* [0x1920]       TSX             *) (compile m ? TSX maINH I) @
 109 (* [0x1921]       LDX 4,X         *) (compile m ? LDX (maIX1 〈x0,x4〉) I) @
 110 (* [0x1923]       RORX            *) (compile m ? ROR maINHX I) @
 111 (* [0x1924]       PSHA            *) (compile m ? PSHA maINH I) @
 112 (* [0x1925]       PULH            *) (compile m ? PULH maINH I) @
 113 (* [0x1926]       CPHX 2,SP       *) (compile m ? CPHX (maSP1 〈x0,x2〉) I) @
 114 (* [0x1929] 22 BD BHI *-65 ; 18E8 *) (compile m ? BHI (maIMM1 〈xB,xD〉) I)
 115
 116 (* [0x192B] attraverso simulazione in CodeWarrior si puo' enunciare che dopo
 117             42+79*n+5*(n>>9) ci sara' il reverse di n byte (PARI) e
 118             H:X=n/2 *)
 119  ).
 120
 121 (* creazione del processore+caricamento+impostazione registri *)
 122 definition dTest_HCS08_sReverse_status ≝
 123 λt:memory_impl.
 124 λHX_op:word16.
 125 λelems:word16.
 126 λdata:list byte8.
 127  set_z_flag HCS08 t (* Z<-true *)
 128   (setweak_sp_reg HCS08 t (* SP<-0x0D4A *)
 129    (setweak_indX_16_reg HCS08 t (* H:X<-HX_op *)
 130     (set_pc_reg HCS08 t (* PC<-0x18E0 *)
 131      (start_of_mcu_version
 132       MC9S08GB60 t
 133       (load_from_source_at t (* carica data in RAM:dTest_HCS08_RAM *)
 134        (load_from_source_at t (zero_memory t) (* carica source in ROM:dTest_HCS08_prog *)
 135          (dTest_HCS08_sReverse_source elems) dTest_HCS08_prog)
 136         data dTest_HCS08_RAM)
 137       (build_memory_type_of_mcu_version MC9S08GB60 t)
 138       (mk_byte8 x0 x0) (mk_byte8 x0 x0) (* non deterministici tutti a 0 *)
 139       false false false false false false) (* non deterministici tutti a 0 *)
 140      (mk_word16 (mk_byte8 x1 x8) (mk_byte8 xE x0)))
 141     HX_op)
 142    (mk_word16 (mk_byte8 x0 xD) (mk_byte8 x4 xA)))
 143   true.
 144
 145 (* parametrizzazione dell'enunciato del teorema *)
 146 (* primo sbozzo: confronto esecuzione con hexdump... *)
 147 lemma dTest_HCS08_sReverse_dump_aux ≝
 148 λt:memory_impl.λstring:list byte8.
 149  (* 1) la stringa deve avere una lunghezza ∈ [0,3072] *)
 150  (byte8_bounded_strlen string 〈〈x0,xC〉:〈x0,x0〉〉) ∧
 151  (* 2) la stringa deve avere lunghezza pari *)
 152  ((and_b8 (w16l (byte8_strlen string)) 〈x0,x1〉) = 〈x0,x0〉) ∧
 153  (* 3) match di esecuzione su tempo in forma di tempo esatto *)
 154  (match execute HCS08 t
 155   (* parametri IN: t,H:X,strlen(string),string *)
 156   (TickOK ? (dTest_HCS08_sReverse_status t 〈〈x0,xD〉:〈x4,xB〉〉 (byte8_strlen string) string))
 157   (* tempo di esecuzione 42+79*n+5*(n>>9) *)
 158   (42+79*(byte8_strlen string)+5*((byte8_strlen string)/512)) with
 159    [ TickERR s _ ⇒ None ?
 160    (* azzeramento tutta RAM tranne dati *)
 161    | TickSUSP s _ ⇒ None ?
 162    | TickOK s ⇒ Some ? (byte8_hexdump t (get_mem_desc HCS08 t s) dTest_HCS08_RAM (byte8_strlen string))
 163    ] =
 164   Some ? (byte8_reverse string)).
 165
 166 (* confronto esecuzione con hexdump... *)
 167 (*
 168 lemma dTest_HCS08_sReverse_dump :
 169  dTest_HCS08_sReverse_dump_aux MEM_TREE dTest_random_32.
 170  unfold dTest_HCS08_sReverse_dump_aux;
 171  split;
 172  [ split; [ normalize in ⊢ (%); autobatch ] reflexivity ]
 173  reflexivity.
 174 qed.
 175 *)
 176
 177 (* parametrizzazione dell'enunciato del teorema *)
 178 (* dimostrazione senza svolgimento degli stati *)
 179 lemma dTest_HCS08_sReverse_aux ≝
 180 λt:memory_impl.λstring:list byte8.
 181  (* 1) la stringa deve avere una lunghezza ∈ [0,3072] *)
 182  (byte8_bounded_strlen string 〈〈x0,xC〉:〈x0,x0〉〉) ∧
 183  (* 2) la stringa deve avere lunghezza pari *)
 184  ((and_b8 (w16l (byte8_strlen string)) 〈x0,x1〉) = 〈x0,x0〉) ∧
 185  (* 3) match di esecuzione su tempo in forma di tempo esatto *)
 186  (match execute HCS08 t
 187   (* parametri IN: t,H:X,strlen(string),string *)
 188   (TickOK ? (dTest_HCS08_sReverse_status t 〈〈x0,xD〉:〈x4,xB〉〉 (byte8_strlen string) string))
 189   (* tempo di esecuzione 42+79*n+5*(n>>9) *)
 190   (42+79*(byte8_strlen string)+5*((byte8_strlen string)/512)) with
 191    [ TickERR s _ ⇒ None ?
 192    (* azzeramento tutta RAM tranne dati *)
 193    | TickSUSP s _ ⇒ None ?
 194    | 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〉〉))
 195    ] =
 196   Some ? (set_pc_reg HCS08 t
 197    (dTest_HCS08_sReverse_status t (fst ?? (shr_w16 (byte8_strlen string))) (byte8_strlen string) (byte8_reverse string))
 198    (mk_word16 (mk_byte8 x1 x9) (mk_byte8 x2 xB)))).
 199
 200 (*
 201 lemma dTest_HCS08_sReverse :
 202  dTest_HCS08_sReverse_aux MEM_TREE dTest_random_32.
 203  unfold dTest_HCS08_sReverse_aux;
 204  split;
 205  [ split; [ normalize in ⊢ (%); autobatch ] reflexivity ]
 206
 207  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⇒?] ?);
 208  letin status0 ≝ (dTest_HCS08_sReverse_status MEM_TREE 〈〈x0,xD〉:〈x4,xB〉〉 (byte8_strlen dTest_random_32) dTest_random_32);
 209  change in ⊢ (? ? match ? ? ? (? ? ? % ?) ? in tick_result return ? with [TickERR⇒?|TickSUSP⇒?|TickOK⇒?] ?) with
 210   (TickOK ? status0);
 211  rewrite > (execute_HCS08_LDHX_maIMM2 MEM_TREE status0 〈x0,x0〉 〈x2,x0〉) in ⊢ (? ? match ? ? ? % ? in tick_result return ? with [TickERR⇒?|TickSUSP⇒?|TickOK⇒?] ?);
 212  [ 2,3,4,5: reflexivity; ]
 213
 214  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));
 215  change in ⊢ (? ? match ? ? ? % ? in tick_result return ? with [TickERR⇒?|TickSUSP⇒?|TickOK⇒?] ?) with (TickOK ? status1);
 216
 217  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⇒?] ?);
 218  change in ⊢ (? ? match ? ? ? (? ? ? % ?) ? in tick_result return ? with [TickERR⇒?|TickSUSP⇒?|TickOK⇒?] ?) with (TickOK ? status1);
 219  rewrite > (execute_HCS08_STHX_maSP1 status1 〈x0,x4〉)
 220   in ⊢ (? ? match ? ? ? % ? in tick_result return ? with [TickERR⇒?|TickSUSP⇒?|TickOK⇒?] ?);
 221  [ 2,3,4,5,6,7: reflexivity; ]
 222
 223  elim daemon.
 224
 225 qed.
 226 *)
 227
 228 definition sReverseCalc ≝
 229 λstring:list byte8.
 230  match execute HCS08 MEM_TREE
 231   (TickOK ? (dTest_HCS08_sReverse_status MEM_TREE 〈〈x0,xD〉:〈x4,xB〉〉 (byte8_strlen string) string))
 232   (42+79*(byte8_strlen string)+5*((byte8_strlen string)/512)) with
 233    [ TickERR s _ ⇒ None ?
 234    | TickSUSP s _ ⇒ None ?
 235    | 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〉〉))
 236    ].
 237
 238 definition sReverseNoCalc ≝
 239 λstring:list byte8.
 240  Some ? (set_pc_reg HCS08 MEM_TREE
 241    (dTest_HCS08_sReverse_status MEM_TREE (fst ?? (shr_w16 (byte8_strlen string))) (byte8_strlen string) (byte8_reverse string))
 242    (mk_word16 (mk_byte8 x1 x9) (mk_byte8 x2 xB))).
 243
 244 definition sReverseCalc32   ≝ sReverseCalc dTest_random_32.
 245 definition sReverseCalc64   ≝ sReverseCalc dTest_random_64.
 246 definition sReverseCalc128  ≝ sReverseCalc dTest_random_128.
 247 definition sReverseCalc256  ≝ sReverseCalc dTest_random_256.
 248 definition sReverseCalc512  ≝ sReverseCalc dTest_random_512.
 249 definition sReverseCalc1024 ≝ sReverseCalc dTest_random_1024.
 250 definition sReverseCalc2048 ≝ sReverseCalc dTest_random_2048.
 251 definition sReverseCalc3072 ≝ sReverseCalc dTest_random_3072.
 252
 253 definition sReverseNoCalc32   ≝ sReverseNoCalc dTest_random_32.
 254 definition sReverseNoCalc64   ≝ sReverseNoCalc dTest_random_64.
 255 definition sReverseNoCalc128  ≝ sReverseNoCalc dTest_random_128.
 256 definition sReverseNoCalc256  ≝ sReverseNoCalc dTest_random_256.
 257 definition sReverseNoCalc512  ≝ sReverseNoCalc dTest_random_512.
 258 definition sReverseNoCalc1024 ≝ sReverseNoCalc dTest_random_1024.
 259 definition sReverseNoCalc2048 ≝ sReverseNoCalc dTest_random_2048.
 260 definition sReverseNoCalc3072 ≝ sReverseNoCalc dTest_random_3072.
 261
 262 (*
 263 lemma ver : sReverseCalc128 = sReverseNoCalc128.
 264  reflexivity.
 265 qed.
 266 *)
 267
 268 (* *********************** *)
 269 (* HCS08GB60 Counting Sort *)
 270 (* *********************** *)
 271
 272 (* versione ridotta, in cui non si riazzerano gli elementi di counters *)
 273 definition dTest_HCS08_cSort_source : word16 → (list byte8) ≝
 274 λelems:word16.
 275 let m ≝ HCS08 in source_to_byte8 m (
 276 (* BEFORE: A=0x00 H:X=0x0F4C SP=0x0F4B PC=0x18C8 Z=true *)
 277
 278 (* /* IPOTESI: INIT VARIABILI+ARRAY GIA' ESEGUITO */
 279    static unsigned int counters[256]={ campitura di 0 };
 280    static unsigned char dati[3072]={ dati random };
 281
 282    void CountingSort(void)
 283     {
 284     unsigned int index=0,position=0; *)
 285
 286 (* /* TESI: CODICE DA ESEGUIRE
 287
 288     /* calcolo del # ripetizioni degli elementi byte */
 289     for(;index<3072;index++)
 290      { counters[dati[index]]++; } *)
 291
 292 (* [0x18C8] 20 1D       BRA *+31;18E7 [3] *) (compile m ? BRA (maIMM1 〈x1,xD〉) I) @
 293 (* [0x18CA] 9E FE 01    LDHX 1,SP     [5] *) (compile m ? LDHX (maSP1 〈x0,x1〉) I) @
 294 (* [0x18CD] D6 01 00    LDA 256,X     [4] *) (compile m ? LDA (maIX2 〈〈x0,x1〉:〈x0,x0〉〉) I) @
 295 (* [0x18D0] 48          LSLA          [1] *) (compile m ? ASL maINHA I) @
 296 (* [0x18D1] 5F          CLRX          [1] *) (compile m ? CLR maINHX I) @
 297 (* [0x18D2] 59          ROLX          [1] *) (compile m ? ROL maINHX I) @
 298 (* [0x18D3] AB 00       ADD #0x00     [2] *) (compile m ? ADD (maIMM1 〈x0,x0〉) I) @
 299 (* [0x18D5] 87          PSHA          [2] *) (compile m ? PSHA maINH I) @
 300 (* [0x18D6] 9F          TXA           [1] *) (compile m ? TXA maINH I) @
 301 (* [0x18D7] A9 0D       ADC #0x0D     [2] *) (compile m ? ADC (maIMM1 〈x0,xD〉) I) @
 302 (* [0x18D9] 87          PSHA          [2] *) (compile m ? PSHA maINH I) @
 303 (* [0x18DA] 8A          PULH          [3] *) (compile m ? PULH maINH I) @
 304 (* [0x18DB] 88          PULX          [3] *) (compile m ? PULX maINH I) @
 305 (* [0x18DC] 6C 01       INC 1,X       [5] *) (compile m ? INC (maIX1 〈x0,x1〉) I) @
 306 (* [0x18DE] 26 01       BNE *+3       [3] *) (compile m ? BNE (maIMM1 〈x0,x1〉) I) @
 307 (* [0x18E0] 7C          INC ,X        [4] *) (compile m ? INC maIX0 I) @
 308 (* [0x18E1] 95          TSX           [2] *) (compile m ? TSX maINH I) @
 309 (* [0x18E2] 6C 01       INC 1,X       [5] *) (compile m ? INC (maIX1 〈x0,x1〉) I) @
 310 (* [0x18E4] 26 01       BNE *+3       [3] *) (compile m ? BNE (maIMM1 〈x0,x1〉) I) @
 311 (* [0x18E6] 7C          INC ,X        [4] *) (compile m ? INC maIX0 I) @
 312 (* [0x18E7] 9E FE 01    LDHX 1,SP     [5] *) (compile m ? LDHX (maSP1 〈x0,x1〉) I) @
 313 (* [0x18EA] 65 0C 00    CPHX #0x0C00  [3] *) (compile m ? CPHX (maIMM2 elems) I) @ (* dimensione dei dati al massimo 0x0C00 *)
 314 (* [0x18ED] 25 DB       BCS *-35;18CA [3] *) (compile m ? BCS (maIMM1 〈xD,xB〉) I) @
 315
 316 (* /* sovrascrittura di dati per produrre la versione ordinata */
 317    for(index=0;index<256;index++)
 318     {
 319     while(counters[index]--)
 320      { dati[position++]=index; }
 321     } *)
 322
 323 (* [0x18EF] 95          TSX          *) (compile m ? TSX maINH I) @
 324 (* [0x18F0] 6F 01       CLR 1,X      *) (compile m ? CLR (maIX1 〈x0,x1〉) I) @
 325 (* [0x18F2] 7F          CLR ,X       *) (compile m ? CLR maIX0 I) @
 326 (* [0x18F3] 20 0E       BRA *+16     *) (compile m ? BRA (maIMM1 〈x0,xE〉) I) @
 327 (* [0x18F5] 95          TSX          *) (compile m ? TSX maINH I) @
 328 (* [0x18F6] E6 01       LDA 1,X      *) (compile m ? LDA (maIX1 〈x0,x1〉) I) @
 329 (* [0x18F8] 9E FE 03    LDHX 3,SP    *) (compile m ? LDHX (maSP1 〈x0,x3〉) I) @
 330 (* [0x18FB] D7 01 00    STA 256,X    *) (compile m ? STA (maIX2 〈〈x0,x1〉:〈x0,x0〉〉) I) @
 331 (* [0x18FE] AF 01       AIX #1       *) (compile m ? AIX (maIMM1 〈x0,x1〉) I) @
 332 (* [0x1900] 9E FF 03    STHX 3,SP    *) (compile m ? STHX (maSP1 〈x0,x3〉) I) @
 333 (* [0x1903] 95          TSX          *) (compile m ? TSX maINH I) @
 334 (* [0x1904] EE 01       LDX 1,X      *) (compile m ? LDX (maIX1 〈x0,x1〉) I) @
 335 (* [0x1906] 58          LSLX         *) (compile m ? ASL maINHX I) @
 336 (* [0x1907] 9E E6 01    LDA 1,SP     *) (compile m ? LDA (maSP1 〈x0,x1〉) I) @
 337 (* [0x190A] 49          ROLA         *) (compile m ? ROL maINHA I) @
 338 (* [0x190B] 87          PSHA         *) (compile m ? PSHA maINH I) @
 339 (* [0x190C] 8A          PULH         *) (compile m ? PULH maINH I) @
 340 (* [0x190D] 89          PSHX         *) (compile m ? PSHX maINH I) @
 341 (* [0x190E] 9E BE 0D 00 LDHX 3328,X  *) (compile m ? LDHX (maIX2 〈〈x0,xD〉:〈x0,x0〉〉) I) @
 342 (* [0x1912] 89          PSHX         *) (compile m ? PSHX maINH I) @
 343 (* [0x1913] 8B          PSHH         *) (compile m ? PSHH maINH I) @
 344 (* [0x1914] AF FF       AIX #-1      *) (compile m ? AIX (maIMM1 〈xF,xF〉) I) @
 345 (* [0x1916] 8B          PSHH         *) (compile m ? PSHH maINH I) @
 346 (* [0x1917] 87          PSHA         *) (compile m ? PSHA maINH I) @
 347 (* [0x1918] 8A          PULH         *) (compile m ? PULH maINH I) @
 348 (* [0x1919] 89          PSHX         *) (compile m ? PSHX maINH I) @
 349 (* [0x191A] 9E EE 05    LDX 5,SP     *) (compile m ? LDX (maSP1 〈x0,x5〉) I) @
 350 (* [0x191D] 86          PULA         *) (compile m ? PULA maINH I) @
 351 (* [0x191E] D7 0D 01    STA 3329,X   *) (compile m ? STA (maIX2 〈〈x0,xD〉:〈x0,x1〉〉) I) @
 352 (* [0x1921] 86          PULA         *) (compile m ? PULA maINH I) @
 353 (* [0x1922] D7 0D 00    STA 3328,X   *) (compile m ? STA (maIX2 〈〈x0,xD〉:〈x0,x0〉〉) I) @
 354 (* [0x1925] 8A          PULH         *) (compile m ? PULH maINH I) @
 355 (* [0x1926] 88          PULX         *) (compile m ? PULX maINH I) @
 356 (* [0x1927] 65 00 00    CPHX #0x0000 *) (compile m ? CPHX (maIMM2 〈〈x0,x0〉:〈x0,x0〉〉) I) @
 357 (* [0x192A] 8A          PULH         *) (compile m ? PULH maINH I) @
 358 (* [0x192B] 26 C8       BNE *-54     *) (compile m ? BNE (maIMM1 〈xC,x8〉) I) @
 359 (* [0x192D] 95          TSX          *) (compile m ? TSX maINH I) @
 360 (* [0x192E] 6C 01       INC 1,X      *) (compile m ? INC (maIX1 〈x0,x1〉) I) @
 361 (* [0x1930] 26 01       BNE *+3      *) (compile m ? BNE (maIMM1 〈x0,x1〉) I) @
 362 (* [0x1932] 7C          INC ,X       *) (compile m ? INC maIX0 I) @
 363 (* [0x1933] 9E FE 01    LDHX 1,SP    *) (compile m ? LDHX (maSP1 〈x0,x1〉) I) @
 364 (* [0x1936] 65 01 00    CPHX #0x0100 *) (compile m ? CPHX (maIMM2 〈〈x0,x1〉:〈x0,x0〉〉) I) @
 365 (* [0x1939] 25 C8       BNE *-54     *) (compile m ? BNE (maIMM1 〈xC,x8〉) I) @
 366 (* [0x193B] 8E                       *) (compile m ? STOP maINH I)
 367
 368 (* [0x193C] attraverso simulazione in CodeWarrior si puo' enunciare che dopo
 369             25700+150n si sara' entrati in stato STOP corrispondente con ordinamento
 370             di n byte, A=0xFF H:X=0x0100 *)
 371  ).
 372
 373 (* creazione del processore+caricamento+impostazione registri *)
 374 definition dTest_HCS08_cSort_status ≝
 375 λt:memory_impl.
 376 λA_op:byte8.
 377 λHX_op:word16.
 378 λelems:word16.
 379 λdata:list byte8.
 380  set_acc_8_low_reg HCS08 t (* A<-A_op *)
 381   (set_z_flag HCS08 t (* Z<-true *)
 382    (setweak_sp_reg HCS08 t (* SP<-0x0F4B *)
 383     (setweak_indX_16_reg HCS08 t (* H:X<-HX_op *)
 384      (set_pc_reg HCS08 t (* PC<-dTest_HCS08_prog *)
 385       (start_of_mcu_version
 386        MC9S08GB60 t
 387        (load_from_source_at t (* carica data in RAM:dTest_HCS08_RAM *)
 388         (load_from_source_at t (zero_memory t) (* carica source in ROM:dTest_HCS08_prog *)
 389           (dTest_HCS08_cSort_source elems) dTest_HCS08_prog)
 390          data dTest_HCS08_RAM)
 391        (build_memory_type_of_mcu_version MC9S08GB60 t)
 392        (mk_byte8 x0 x0) (mk_byte8 x0 x0) (* non deterministici tutti a 0 *)
 393        false false false false false false) (* non deterministici tutti a 0 *)
 394       dTest_HCS08_prog)
 395      HX_op)
 396     (mk_word16 (mk_byte8 x0 xF) (mk_byte8 x4 xB)))
 397    true)
 398   A_op.
 399
 400 (* parametrizzazione dell'enunciato del teorema parziale *)
 401 lemma dTest_HCS08_cSort_aux ≝
 402 λt:memory_impl.λstring:list byte8.
 403  (* 1) la stringa deve avere una lunghezza ∈ [0,3072] *)
 404  (byte8_bounded_strlen string 〈〈x0,xC〉:〈x0,x0〉〉) ∧
 405  (* 2) match di esecuzione su tempo in forma di upperbound *)
 406  (match execute HCS08 t
 407   (* parametri IN: t,A,H:X,strlen(string),string *)
 408   (TickOK ? (dTest_HCS08_cSort_status t 〈x0,x0〉 〈〈x0,xF〉:〈x4,xC〉〉 (byte8_strlen string) string))
 409   (* tempo di esecuzione 25700+150*n *)
 410   ((nat_of_word16 〈〈x6,x4〉:〈x6,x4〉〉)+(nat_of_byte8 〈x9,x6〉)*(nat_of_word16 (byte8_strlen string))) with
 411    [ TickERR s _ ⇒ None ?
 412    (* azzeramento tutta RAM tranne dati *)
 413    | 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〉〉))
 414    | TickOK s ⇒ None ?
 415    ] =
 416   Some ? (set_pc_reg HCS08 t
 417    (dTest_HCS08_cSort_status t 〈xF,xF〉 〈〈x0,x1〉:〈x0,x0〉〉 (byte8_strlen string) (byte8_list_ordering string))
 418    (mk_word16 (mk_byte8 x1 x9) (mk_byte8 x3 xC)))).
 419
 420 (* dimostrazione senza svolgimento degli stati *)
 421 (*
 422 lemma dTest_HCS08_cSort :
 423  dTest_HCS08_cSort_aux MEM_TREE dTest_random_32.
 424  unfold dTest_HCS08_cSort_aux;
 425  split;
 426  [ normalize in ⊢ (%); autobatch ]
 427  reflexivity.
 428 qed.
 429 *)
 430
 431 definition cSortCalc ≝
 432 λstring:list byte8.
 433  match execute HCS08 MEM_TREE
 434   (TickOK ? (dTest_HCS08_cSort_status MEM_TREE 〈x0,x0〉 〈〈x0,xF〉:〈x4,xC〉〉 (byte8_strlen string) string))
 435   ((nat_of_word16 〈〈x6,x4〉:〈x6,x4〉〉)+(nat_of_byte8 〈x9,x6〉)*(nat_of_word16 (byte8_strlen string))) with
 436    [ TickERR s _ ⇒ None ?
 437    | 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〉〉))
 438    | TickOK s ⇒ None ?
 439    ].
 440
 441 definition cSortNoCalc ≝
 442 λstring:list byte8.
 443  Some ? (set_pc_reg HCS08 MEM_TREE
 444    (dTest_HCS08_cSort_status MEM_TREE 〈xF,xF〉 〈〈x0,x1〉:〈x0,x0〉〉 (byte8_strlen string) (byte8_list_ordering string))
 445    (mk_word16 (mk_byte8 x1 x9) (mk_byte8 x3 xC))).
 446
 447 definition cSortCalc32   ≝ cSortCalc dTest_random_32.
 448 definition cSortCalc64   ≝ cSortCalc dTest_random_64.
 449 definition cSortCalc128  ≝ cSortCalc dTest_random_128.
 450 definition cSortCalc256  ≝ cSortCalc dTest_random_256.
 451 definition cSortCalc512  ≝ cSortCalc dTest_random_512.
 452 definition cSortCalc1024 ≝ cSortCalc dTest_random_1024.
 453 definition cSortCalc2048 ≝ cSortCalc dTest_random_2048.
 454 definition cSortCalc3072 ≝ cSortCalc dTest_random_3072.
 455
 456 definition cSortNoCalc32   ≝ cSortNoCalc dTest_random_32.
 457 definition cSortNoCalc64   ≝ cSortNoCalc dTest_random_64.
 458 definition cSortNoCalc128  ≝ cSortNoCalc dTest_random_128.
 459 definition cSortNoCalc256  ≝ cSortNoCalc dTest_random_256.
 460 definition cSortNoCalc512  ≝ cSortNoCalc dTest_random_512.
 461 definition cSortNoCalc1024 ≝ cSortNoCalc dTest_random_1024.
 462 definition cSortNoCalc2048 ≝ cSortNoCalc dTest_random_2048.
 463 definition cSortNoCalc3072 ≝ cSortNoCalc dTest_random_3072.
 464
 465 (*
 466 lemma ver : cSortCalc32 = cSortNoCalc32.
 467  reflexivity.
 468 qed.
 469 *)