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 set "baseuri" "cic:/matita/freescale/medium_tests/".
  28
  29 (*include "/media/VIRTUOSO/freescale/medium_tests_tools.ma".*)
  30 include "freescale/medium_tests_tools.ma".
  31
  32 (* ************************ *)
  33 (* HCS08GB60 String Reverse *)
  34 (* ************************ *)
  35
  36 (* versione ridotta, in cui non si riazzerano gli elementi di counters *)
  37 definition dTest_HCS08_sReverse_source : word16 → (list byte8) ≝
  38 λelems:word16.
  39 let m ≝ HCS08 in source_to_byte8 m (
  40 (* BEFORE: A=0x00 H:X=0x0D4B SP=0x0D4A PC=0x18E0 Z=true *)
  41
  42 (* static unsigned char dati[3072]={...};
  43
  44    void swap(unsigned char *a, unsigned char *b)
  45     { unsigned char tmp=*a; *a=*b; *b=tmp; return; } *)
  46
  47 (* [0x18C8]    allineamento *) (compile m ? NOP maINH I) @
  48
  49 (* [0x18C9]       PSHX      *) (compile m ? PSHX maINH I) @
  50 (* [0x18CA]       PSHH      *) (compile m ? PSHH maINH I) @
  51 (* [0x18CB]       LDHX 5,SP *) (compile m ? LDHX (maSP1 〈x0,x5〉) I) @
  52 (* [0x18CE]       LDA ,X    *) (compile m ? LDA maIX0 I) @
  53 (* [0x18CF]       LDHX 1,SP *) (compile m ? LDHX (maSP1 〈x0,x1〉) I) @
  54 (* [0x18D2]       PSHA      *) (compile m ? PSHA maINH I) @
  55 (* [0x18D3]       LDA ,X    *) (compile m ? LDA maIX0 I) @
  56 (* [0x18D4]       LDHX 6,SP *) (compile m ? LDHX (maSP1 〈x0,x6〉) I) @
  57 (* [0x18D7]       STA ,X    *) (compile m ? STA maIX0 I) @
  58 (* [0x18D8]       LDHX 2,SP *) (compile m ? LDHX (maSP1 〈x0,x2〉) I) @
  59 (* [0x18DB]       PULA      *) (compile m ? PULA maINH I) @
  60 (* [0x18DC]       STA ,X    *) (compile m ? STA maIX0 I) @
  61 (* [0x18DD]       AIS #2    *) (compile m ? AIS (maIMM1 〈x0,x2〉) I) @
  62 (* [0x18DF]       RTS       *) (compile m ? RTS maINH I) @
  63
  64 (* void main(void)
  65    {
  66    unsigned int pos=0,limit=0;
  67
  68    for(limit=3072;pos<(limit/2);pos++)
  69     { swap(&dati[pos],&dati[limit-pos-1]); } *)
  70
  71 (* [0x18E0]       LDHX #LUNG      *) (compile m ? LDHX (maIMM2 elems) I) @
  72 (* [0x18E3]       STHX 4,SP       *) (compile m ? STHX (maSP1 〈x0,x4〉) I) @
  73 (* [0x18E6] 20 32 BRA *+52 ; 191A *) (compile m ? BRA (maIMM1 〈x3,x2〉) I) @
  74 (* [0x18E8]       TSX             *) (compile m ? TSX maINH I) @
  75 (* [0x18E9]       LDA 2,X         *) (compile m ? LDA (maIX1 〈x0,x2〉) I) @
  76 (* [0x18EB]       ADD #0x00       *) (compile m ? ADD (maIMM1 〈x0,x0〉) I) @
  77 (* [0x18ED]       PSHA            *) (compile m ? PSHA maINH I) @
  78 (* [0x18EE]       LDA 1,X         *) (compile m ? LDA (maIX1 〈x0,x1〉) I) @
  79 (* [0x18F0]       ADC #0x01       *) (compile m ? ADC (maIMM1 〈x0,x1〉) I) @
  80 (* [0x18F2]       PSHA            *) (compile m ? PSHA maINH I) @
  81 (* [0x18F3]       LDA 4,X         *) (compile m ? LDA (maIX1 〈x0,x4〉) I) @
  82 (* [0x18F5]       SUB 2,X         *) (compile m ? SUB (maIX1 〈x0,x2〉) I) @
  83 (* [0x18F7]       STA ,X          *) (compile m ? STA maIX0 I) @
  84 (* [0x18F8]       LDA 3,X         *) (compile m ? LDA (maIX1 〈x0,x3〉) I) @
  85 (* [0x18FA]       SBC 1,X         *) (compile m ? SBC (maIX1 〈x0,x1〉) I) @
  86 (* [0x18FC]       PSHA            *) (compile m ? PSHA maINH I) @
  87 (* [0x18FD]       LDX ,X          *) (compile m ? LDX maIX0 I) @
  88 (* [0x18FE]       PULH            *) (compile m ? PULH maINH I) @
  89 (* [0x18FF]       AIX #-1         *) (compile m ? AIX (maIMM1 〈xF,xF〉) I) @
  90 (* [0x1901]       TXA             *) (compile m ? TXA maINH I) @
  91 (* [0x1902]       ADD #0x00       *) (compile m ? ADD (maIMM1 〈x0,x0〉) I) @
  92 (* [0x1904]       PSHH            *) (compile m ? PSHH maINH I) @
  93 (* [0x1905]       TSX             *) (compile m ? TSX maINH I) @
  94 (* [0x1906]       STA 3,X         *) (compile m ? STA (maIX1 〈x0,x3〉) I) @
  95 (* [0x1908]       PULA            *) (compile m ? PULA maINH I) @
  96 (* [0x1909]       ADC #0x01       *) (compile m ? ADC (maIMM1 〈x0,x1〉) I) @
  97 (* [0x190B]       LDX 3,X         *) (compile m ? LDX (maIX1 〈x0,x3〉) I) @
  98 (* [0x190D]       PSHA            *) (compile m ? PSHA maINH I) @
  99 (* [0x190E]       PULH            *) (compile m ? PULH maINH I) @
 100 (* [0x190F] AD B8 BSR *-70 ; 18C9 *) (compile m ? BSR (maIMM1 〈xB,x8〉) I) @
 101 (* [0x1911]       AIS #2          *) (compile m ? AIS (maIMM1 〈x0,x2〉) I) @
 102 (* [0x1913]       TSX             *) (compile m ? TSX maINH I) @
 103 (* [0x1914]       INC 2,X         *) (compile m ? INC (maIX1 〈x0,x2〉) I) @
 104 (* [0x1916] 26 02 BNE *+4 ; 191A  *) (compile m ? BNE (maIMM1 〈x0,x2〉) I) @
 105 (* [0x1918]       INC 1,X         *) (compile m ? INC (maIX1 〈x0,x1〉) I) @
 106 (* [0x191A]       TSX             *) (compile m ? TSX maINH I) @
 107 (* [0x191B]       LDA 3,X         *) (compile m ? LDA (maIX1 〈x0,x3〉) I) @
 108 (* [0x191D]       PSHA            *) (compile m ? PSHA maINH I) @
 109 (* [0x191E]       PULH            *) (compile m ? PULH maINH I) @
 110 (* [0x191F]       LSRA            *) (compile m ? LSR maINHA I) @
 111 (* [0x1920]       TSX             *) (compile m ? TSX maINH I) @
 112 (* [0x1921]       LDX 4,X         *) (compile m ? LDX (maIX1 〈x0,x4〉) I) @
 113 (* [0x1923]       RORX            *) (compile m ? ROR maINHX I) @
 114 (* [0x1924]       PSHA            *) (compile m ? PSHA maINH I) @
 115 (* [0x1925]       PULH            *) (compile m ? PULH maINH I) @
 116 (* [0x1926]       CPHX 2,SP       *) (compile m ? CPHX (maSP1 〈x0,x2〉) I) @
 117 (* [0x1929] 22 BD BHI *-65 ; 18E8 *) (compile m ? BHI (maIMM1 〈xB,xD〉) I)
 118
 119 (* [0x192B] attraverso simulazione in CodeWarrior si puo' enunciare che dopo
 120             42+79*n+(n>>9) ci sara' il reverse di n byte (PARI) e
 121             H:X=n/2 *)
 122  ).
 123
 124 (* creazione del processore+caricamento+impostazione registri *)
 125 definition dTest_HCS08_sReverse_status ≝
 126 λt:memory_impl.
 127 λHX_op:word16.
 128 λelems:word16.
 129 λdata:list byte8.
 130  set_z_flag HCS08 t (* Z<-true *)
 131   (setweak_sp_reg HCS08 t (* SP<-0x0D4A *)
 132    (setweak_indX_16_reg HCS08 t (* H:X<-HX_op *)
 133     (set_pc_reg HCS08 t (* PC<-0x18E0 *)
 134      (start_of_mcu_version
 135       MC9S08GB60 t
 136       (load_from_source_at t (* carica data in RAM:dTest_HCS08_RAM *)
 137        (load_from_source_at t (zero_memory t) (* carica source in ROM:dTest_HCS08_prog *)
 138          (dTest_HCS08_sReverse_source elems) dTest_HCS08_prog)
 139         data dTest_HCS08_RAM)
 140       (build_memory_type_of_mcu_version MC9S08GB60 t)
 141       (mk_byte8 x0 x0) (mk_byte8 x0 x0) (* non deterministici tutti a 0 *)
 142       false false false false false false) (* non deterministici tutti a 0 *)
 143      (mk_word16 (mk_byte8 x1 x8) (mk_byte8 xE x0)))
 144     HX_op)
 145    (mk_word16 (mk_byte8 x0 xD) (mk_byte8 x4 xA)))
 146   true.
 147
 148 (* parametrizzazione dell'enunciato del teorema *)
 149 (* primo sbozzo: confronto esecuzione con hexdump... *)
 150 lemma dTest_HCS08_sReverse_dump_aux ≝
 151 λt:memory_impl.λstring:list byte8.
 152  (* 1) la stringa deve avere una lunghezza ∈ [0,3072] *)
 153  (byte8_bounded_strlen string 〈〈x0,xC〉:〈x0,x0〉〉) ∧
 154  (* 2) la stringa deve avere lunghezza pari *)
 155  ((and_b8 (w16l (byte8_strlen string)) 〈x0,x1〉) = 〈x0,x0〉) ∧
 156  (* 3) match di esecuzione su tempo in forma di tempo esatto *)
 157  (match execute HCS08 t
 158   (* parametri IN: t,H:X,strlen(string),string *)
 159   (TickOK ? (dTest_HCS08_sReverse_status t 〈〈x0,xD〉:〈x4,xB〉〉 (byte8_strlen string) string))
 160   (* tempo di esecuzione 25700+150*n *)
 161   (42+79*(byte8_strlen string)+((byte8_strlen string)/512)) with
 162    [ TickERR s _ ⇒ None ?
 163    (* azzeramento tutta RAM tranne dati *)
 164    | TickSUSP s _ ⇒ None ?
 165    | TickOK s ⇒ Some ? (byte8_hexdump t (get_mem_desc HCS08 t s) dTest_HCS08_RAM (byte8_strlen string))
 166    ] =
 167   Some ? (byte8_reverse string)).
 168
 169 (* primo sbozzo: confronto esecuzione con hexdump... *)
 170 lemma dTest_HCS08_sReverse_dump :
 171  dTest_HCS08_sReverse_dump_aux MEM_TREE dTest_random_32.
 172  unfold dTest_HCS08_sReverse_dump_aux;
 173  split;
 174  [ split; [ normalize in ⊢ (%); autobatch ] reflexivity ]
 175  reflexivity.
 176 qed.
 177
 178 (* parametrizzazione dell'enunciato del teorema *)
 179 (* dimostrazione senza svolgimento degli stati *)
 180 lemma dTest_HCS08_sReverse_aux ≝
 181 λt:memory_impl.λstring:list byte8.
 182  (* 1) la stringa deve avere una lunghezza ∈ [0,3072] *)
 183  (byte8_bounded_strlen string 〈〈x0,xC〉:〈x0,x0〉〉) ∧
 184  (* 2) la stringa deve avere lunghezza pari *)
 185  ((and_b8 (w16l (byte8_strlen string)) 〈x0,x1〉) = 〈x0,x0〉) ∧
 186  (* 3) match di esecuzione su tempo in forma di tempo esatto *)
 187  (match execute HCS08 t
 188   (* parametri IN: t,H:X,strlen(string),string *)
 189   (TickOK ? (dTest_HCS08_sReverse_status t 〈〈x0,xD〉:〈x4,xB〉〉 (byte8_strlen string) string))
 190   (* tempo di esecuzione 25700+150*n *)
 191   (42+79*(byte8_strlen string)+((byte8_strlen string)/512)) with
 192    [ TickERR s _ ⇒ None ?
 193    (* azzeramento tutta RAM tranne dati *)
 194    | TickSUSP s _ ⇒ None ?
 195    | 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〉〉))
 196    ] =
 197   Some ? (set_pc_reg HCS08 t
 198    (dTest_HCS08_sReverse_status t (fst ?? (shr_w16 (byte8_strlen string))) (byte8_strlen string) (byte8_reverse string))
 199    (mk_word16 (mk_byte8 x1 x9) (mk_byte8 x2 xB)))).
 200
 201 (* dimostrazione senza svolgimento degli stati *)
 202 (* sembra corretta, ma non basta la memoria per arrivare in fondo con quelli grandi! *)
 203 (* NB: sono gia' pronti dei pattern piu' impegnativi in medium_tests_tool: *)
 204 (*     dTest_random_32/64/128/256/512/1024/2048/3072 generati con Mathematica *)
 205 (*     ex: dTest_HCS08_sReverse_aux MEM_TREE dTest_random_3072 sarebbe gia' un bell'obbiettivo! *)
 206 lemma dTest_HCS08_sReverse :
 207  dTest_HCS08_sReverse_aux MEM_TREE dTest_random_32.
 208  unfold dTest_HCS08_sReverse_aux;
 209  split;
 210  [ split; [ normalize in ⊢ (%); autobatch ] reflexivity ]
 211  reflexivity.
 212 qed.
 213
 214 (* *********************** *)
 215 (* HCS08GB60 Counting Sort *)
 216 (* *********************** *)
 217
 218 (* versione ridotta, in cui non si riazzerano gli elementi di counters *)
 219 definition dTest_HCS08_cSort_source : word16 → (list byte8) ≝
 220 λelems:word16.
 221 let m ≝ HCS08 in source_to_byte8 m (
 222 (* BEFORE: A=0x00 H:X=0x0F4C SP=0x0F4B PC=0x18C8 Z=true *)
 223
 224 (* /* IPOTESI: INIT VARIABILI+ARRAY GIA' ESEGUITO */
 225    static unsigned int counters[256]={ campitura di 0 };
 226    static unsigned char dati[3072]={ dati random };
 227
 228    void CountingSort(void)
 229     {
 230     unsigned int index=0,position=0; *)
 231
 232 (* /* TESI: CODICE DA ESEGUIRE
 233
 234     /* calcolo del # ripetizioni degli elementi byte */
 235     for(;index<3072;index++)
 236      { counters[dati[index]]++; } *)
 237
 238 (* [0x18C8] 20 1D       BRA *+31;18E7 [3] *) (compile m ? BRA (maIMM1 〈x1,xD〉) I) @
 239 (* [0x18CA] 9E FE 01    LDHX 1,SP     [5] *) (compile m ? LDHX (maSP1 〈x0,x1〉) I) @
 240 (* [0x18CD] D6 01 00    LDA 256,X     [4] *) (compile m ? LDA (maIX2 〈〈x0,x1〉:〈x0,x0〉〉) I) @
 241 (* [0x18D0] 48          LSLA          [1] *) (compile m ? ASL maINHA I) @
 242 (* [0x18D1] 5F          CLRX          [1] *) (compile m ? CLR maINHX I) @
 243 (* [0x18D2] 59          ROLX          [1] *) (compile m ? ROL maINHX I) @
 244 (* [0x18D3] AB 00       ADD #0x00     [2] *) (compile m ? ADD (maIMM1 〈x0,x0〉) I) @
 245 (* [0x18D5] 87          PSHA          [2] *) (compile m ? PSHA maINH I) @
 246 (* [0x18D6] 9F          TXA           [1] *) (compile m ? TXA maINH I) @
 247 (* [0x18D7] A9 0D       ADC #0x0D     [2] *) (compile m ? ADC (maIMM1 〈x0,xD〉) I) @
 248 (* [0x18D9] 87          PSHA          [2] *) (compile m ? PSHA maINH I) @
 249 (* [0x18DA] 8A          PULH          [3] *) (compile m ? PULH maINH I) @
 250 (* [0x18DB] 88          PULX          [3] *) (compile m ? PULX maINH I) @
 251 (* [0x18DC] 6C 01       INC 1,X       [5] *) (compile m ? INC (maIX1 〈x0,x1〉) I) @
 252 (* [0x18DE] 26 01       BNE *+3       [3] *) (compile m ? BNE (maIMM1 〈x0,x1〉) I) @
 253 (* [0x18E0] 7C          INC ,X        [4] *) (compile m ? INC maIX0 I) @
 254 (* [0x18E1] 95          TSX           [2] *) (compile m ? TSX maINH I) @
 255 (* [0x18E2] 6C 01       INC 1,X       [5] *) (compile m ? INC (maIX1 〈x0,x1〉) I) @
 256 (* [0x18E4] 26 01       BNE *+3       [3] *) (compile m ? BNE (maIMM1 〈x0,x1〉) I) @
 257 (* [0x18E6] 7C          INC ,X        [4] *) (compile m ? INC maIX0 I) @
 258 (* [0x18E7] 9E FE 01    LDHX 1,SP     [5] *) (compile m ? LDHX (maSP1 〈x0,x1〉) I) @
 259 (* [0x18EA] 65 0C 00    CPHX #0x0C00  [3] *) (compile m ? CPHX (maIMM2 elems) I) @ (* dimensione dei dati al massimo 0x0C00 *)
 260 (* [0x18ED] 25 DB       BCS *-35;18CA [3] *) (compile m ? BCS (maIMM1 〈xD,xB〉) I) @
 261
 262 (* /* sovrascrittura di dati per produrre la versione ordinata */
 263    for(index=0;index<256;index++)
 264     {
 265     while(counters[index]--)
 266      { dati[position++]=index; }
 267     } *)
 268
 269 (* [0x18EF] 95          TSX          *) (compile m ? TSX maINH I) @
 270 (* [0x18F0] 6F 01       CLR 1,X      *) (compile m ? CLR (maIX1 〈x0,x1〉) I) @
 271 (* [0x18F2] 7F          CLR ,X       *) (compile m ? CLR maIX0 I) @
 272 (* [0x18F3] 20 0E       BRA *+16     *) (compile m ? BRA (maIMM1 〈x0,xE〉) I) @
 273 (* [0x18F5] 95          TSX          *) (compile m ? TSX maINH I) @
 274 (* [0x18F6] E6 01       LDA 1,X      *) (compile m ? LDA (maIX1 〈x0,x1〉) I) @
 275 (* [0x18F8] 9E FE 03    LDHX 3,SP    *) (compile m ? LDHX (maSP1 〈x0,x3〉) I) @
 276 (* [0x18FB] D7 01 00    STA 256,X    *) (compile m ? STA (maIX2 〈〈x0,x1〉:〈x0,x0〉〉) I) @
 277 (* [0x18FE] AF 01       AIX #1       *) (compile m ? AIX (maIMM1 〈x0,x1〉) I) @
 278 (* [0x1900] 9E FF 03    STHX 3,SP    *) (compile m ? STHX (maSP1 〈x0,x3〉) I) @
 279 (* [0x1903] 95          TSX          *) (compile m ? TSX maINH I) @
 280 (* [0x1904] EE 01       LDX 1,X      *) (compile m ? LDX (maIX1 〈x0,x1〉) I) @
 281 (* [0x1906] 58          LSLX         *) (compile m ? ASL maINHX I) @
 282 (* [0x1907] 9E E6 01    LDA 1,SP     *) (compile m ? LDA (maSP1 〈x0,x1〉) I) @
 283 (* [0x190A] 49          ROLA         *) (compile m ? ROL maINHA I) @
 284 (* [0x190B] 87          PSHA         *) (compile m ? PSHA maINH I) @
 285 (* [0x190C] 8A          PULH         *) (compile m ? PULH maINH I) @
 286 (* [0x190D] 89          PSHX         *) (compile m ? PSHX maINH I) @
 287 (* [0x190E] 9E BE 0D 00 LDHX 3328,X  *) (compile m ? LDHX (maIX2 〈〈x0,xD〉:〈x0,x0〉〉) I) @
 288 (* [0x1912] 89          PSHX         *) (compile m ? PSHX maINH I) @
 289 (* [0x1913] 8B          PSHH         *) (compile m ? PSHH maINH I) @
 290 (* [0x1914] AF FF       AIX #-1      *) (compile m ? AIX (maIMM1 〈xF,xF〉) I) @
 291 (* [0x1916] 8B          PSHH         *) (compile m ? PSHH maINH I) @
 292 (* [0x1917] 87          PSHA         *) (compile m ? PSHA maINH I) @
 293 (* [0x1918] 8A          PULH         *) (compile m ? PULH maINH I) @
 294 (* [0x1919] 89          PSHX         *) (compile m ? PSHX maINH I) @
 295 (* [0x191A] 9E EE 05    LDX 5,SP     *) (compile m ? LDX (maSP1 〈x0,x5〉) I) @
 296 (* [0x191D] 86          PULA         *) (compile m ? PULA maINH I) @
 297 (* [0x191E] D7 0D 01    STA 3329,X   *) (compile m ? STA (maIX2 〈〈x0,xD〉:〈x0,x1〉〉) I) @
 298 (* [0x1921] 86          PULA         *) (compile m ? PULA maINH I) @
 299 (* [0x1922] D7 0D 00    STA 3328,X   *) (compile m ? STA (maIX2 〈〈x0,xD〉:〈x0,x0〉〉) I) @
 300 (* [0x1925] 8A          PULH         *) (compile m ? PULH maINH I) @
 301 (* [0x1926] 88          PULX         *) (compile m ? PULX maINH I) @
 302 (* [0x1927] 65 00 00    CPHX #0x0000 *) (compile m ? CPHX (maIMM2 〈〈x0,x0〉:〈x0,x0〉〉) I) @
 303 (* [0x192A] 8A          PULH         *) (compile m ? PULH maINH I) @
 304 (* [0x192B] 26 C8       BNE *-54     *) (compile m ? BNE (maIMM1 〈xC,x8〉) I) @
 305 (* [0x192D] 95          TSX          *) (compile m ? TSX maINH I) @
 306 (* [0x192E] 6C 01       INC 1,X      *) (compile m ? INC (maIX1 〈x0,x1〉) I) @
 307 (* [0x1930] 26 01       BNE *+3      *) (compile m ? BNE (maIMM1 〈x0,x1〉) I) @
 308 (* [0x1932] 7C          INC ,X       *) (compile m ? INC maIX0 I) @
 309 (* [0x1933] 9E FE 01    LDHX 1,SP    *) (compile m ? LDHX (maSP1 〈x0,x1〉) I) @
 310 (* [0x1936] 65 01 00    CPHX #0x0100 *) (compile m ? CPHX (maIMM2 〈〈x0,x1〉:〈x0,x0〉〉) I) @
 311 (* [0x1939] 25 C8       BNE *-54     *) (compile m ? BNE (maIMM1 〈xC,x8〉) I) @
 312 (* [0x193B] 8E                       *) (compile m ? STOP maINH I)
 313
 314 (* [0x193C] attraverso simulazione in CodeWarrior si puo' enunciare che dopo
 315             25700+150n si sara' entrati in stato STOP corrispondente con ordinamento
 316             di n byte, A=0xFF H:X=0x0100 *)
 317  ).
 318
 319 (* creazione del processore+caricamento+impostazione registri *)
 320 definition dTest_HCS08_cSort_status ≝
 321 λt:memory_impl.
 322 λA_op:byte8.
 323 λHX_op:word16.
 324 λelems:word16.
 325 λdata:list byte8.
 326  set_acc_8_low_reg HCS08 t (* A<-A_op *)
 327   (set_z_flag HCS08 t (* Z<-true *)
 328    (setweak_sp_reg HCS08 t (* SP<-0x0F4B *)
 329     (setweak_indX_16_reg HCS08 t (* H:X<-HX_op *)
 330      (set_pc_reg HCS08 t (* PC<-dTest_HCS08_prog *)
 331       (start_of_mcu_version
 332        MC9S08GB60 t
 333        (load_from_source_at t (* carica data in RAM:dTest_HCS08_RAM *)
 334         (load_from_source_at t (zero_memory t) (* carica source in ROM:dTest_HCS08_prog *)
 335           (dTest_HCS08_cSort_source elems) dTest_HCS08_prog)
 336          data dTest_HCS08_RAM)
 337        (build_memory_type_of_mcu_version MC9S08GB60 t)
 338        (mk_byte8 x0 x0) (mk_byte8 x0 x0) (* non deterministici tutti a 0 *)
 339        false false false false false false) (* non deterministici tutti a 0 *)
 340       dTest_HCS08_prog)
 341      HX_op)
 342     (mk_word16 (mk_byte8 x0 xF) (mk_byte8 x4 xB)))
 343    true)
 344   A_op.
 345
 346 (* parametrizzazione dell'enunciato del teorema parziale *)
 347 lemma dTest_HCS08_cSort_aux ≝
 348 λt:memory_impl.λstring:list byte8.
 349  (* 1) la stringa deve avere una lunghezza ∈ [0,3072] *)
 350  (byte8_bounded_strlen string 〈〈x0,xC〉:〈x0,x0〉〉) ∧
 351  (* 2) match di esecuzione su tempo in forma di upperbound *)
 352  (match execute HCS08 t
 353   (* parametri IN: t,A,H:X,strlen(string),string *)
 354   (TickOK ? (dTest_HCS08_cSort_status t 〈x0,x0〉 〈〈x0,xF〉:〈x4,xC〉〉 (byte8_strlen string) string))
 355   (* tempo di esecuzione 25700+150*n *)
 356   ((nat_of_word16 〈〈x6,x4〉:〈x6,x4〉〉)+(nat_of_byte8 〈x9,x6〉)*(nat_of_word16 (byte8_strlen string))) with
 357    [ TickERR s _ ⇒ None ?
 358    (* azzeramento tutta RAM tranne dati *)
 359    | 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〉〉))
 360    | TickOK s ⇒ None ?
 361    ] =
 362   Some ? (set_pc_reg HCS08 t
 363    (dTest_HCS08_cSort_status t 〈xF,xF〉 〈〈x0,x1〉:〈x0,x0〉〉 (byte8_strlen string) (byte8_list_ordering string))
 364    (mk_word16 (mk_byte8 x1 x9) (mk_byte8 x3 xC)))).
 365
 366 (* dimostrazione senza svolgimento degli stati *)
 367 (* sembra corretta, ma non basta la memoria per arrivare in fondo nemmeno col piccolo! *)
 368 (* NB: sono gia' pronti dei pattern piu' impegnativi in medium_tests_tool: *)
 369 (*     dTest_random_32/64/128/256/512/1024/2048/3072 generati con Mathematica *)
 370 (*     ex: dTest_HCS08_cSort_aux MEM_TREE dTest_random_3072 sarebbe gia' un bell'obbiettivo! *)
 371
 372 (*
 373 lemma dTest_HCS08_cSort :
 374  dTest_HCS08_cSort_aux MEM_TREE dTest_random_32.
 375  unfold dTest_HCS08_cSort_aux;
 376  split;
 377  [ normalize in ⊢ (%); autobatch ]
 378  reflexivity.
 379 qed.
 380 *)