helm/software/matita/contribs/ng_assembly/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: Cosimo Oliboni, oliboni@cs.unibo.it                   *)
  19 (*     Cosimo Oliboni, oliboni@cs.unibo.it                                *)
  20 (*                                                                        *)
  21 (* ********************************************************************** *)
  22
  23 include "freescale/medium_tests_tools.ma".
  24 include "utility/utility.ma".
  25
  26 (* ************************ *)
  27 (* HCS08GB60 String Reverse *)
  28 (* ************************ *)
  29
  30 (* versione ridotta, in cui non si riazzerano gli elementi di counters *)
  31 ndefinition dTest_HCS08_sReverse_source : word16 → (list byte8) ≝
  32 λelems:word16.
  33 let m ≝ HCS08 in source_to_byte8 m (
  34 (* BEFORE: A=0x00 H:X=0x0D4B SP=0x0D4A PC=0x18E0 Z=true *)
  35
  36 (* static unsigned char dati[3072]={...};
  37
  38    void swap(unsigned char *a, unsigned char *b)
  39     { unsigned char tmp=*a; *a=*b; *b=tmp; return; } *)
  40
  41 (* [0x18C8]    allineamento *) (compile m ? NOP maINH I) @
  42
  43 (* argomenti: HX e [0x0D49-A], passaggio ibrido reg, stack *)
  44 (* [0x18C9] PSHX      *) (compile m ? PSHX maINH I) @
  45 (* [0x18CA] PSHH      *) (compile m ? PSHH maINH I) @
  46 (* [0x18CB] LDHX 5,SP *) (compile m ? LDHX (maSP1 〈x0,x5〉) I) @
  47 (* [0x18CE] LDA ,X    *) (compile m ? LDA maIX0 I) @
  48 (* [0x18CF] LDHX 1,SP *) (compile m ? LDHX (maSP1 〈x0,x1〉) I) @
  49 (* [0x18D2] PSHA      *) (compile m ? PSHA maINH I) @
  50 (* [0x18D3] LDA ,X    *) (compile m ? LDA maIX0 I) @
  51 (* [0x18D4] LDHX 6,SP *) (compile m ? LDHX (maSP1 〈x0,x6〉) I) @
  52 (* [0x18D7] STA ,X    *) (compile m ? STA maIX0 I) @
  53 (* [0x18D8] LDHX 2,SP *) (compile m ? LDHX (maSP1 〈x0,x2〉) I) @
  54 (* [0x18DB] PULA      *) (compile m ? PULA maINH I) @
  55 (* [0x18DC] STA ,X    *) (compile m ? STA maIX0 I) @
  56 (* [0x18DD] AIS #2    *) (compile m ? AIS (maIMM1 〈x0,x2〉) I) @
  57 (* [0x18DF] RTS       *) (compile m ? RTS maINH I) @
  58
  59 (* void main(void)
  60    {
  61    unsigned int pos=0,limit=0;
  62
  63    for(limit=3072;pos<(limit/2);pos++)
  64     { swap(&dati[pos],&dati[limit-pos-1]); } *)
  65
  66 (* [0x18E0] LDHX #elems     *) (compile m ? LDHX (maIMM2 elems) I) @
  67 (* [0x18E3] STHX 4,SP       *) (compile m ? STHX (maSP1 〈x0,x4〉) I) @
  68 (* [0x18E6] BRA *+52 ; 191A *) (compile m ? BRA (maIMM1 〈x3,x2〉) I) @
  69 (* [0x18E8] TSX             *) (compile m ? TSX maINH I) @
  70 (* [0x18E9] LDA 2,X         *) (compile m ? LDA (maIX1 〈x0,x2〉) I) @
  71 (* [0x18EB] ADD #0x00       *) (compile m ? ADD (maIMM1 〈x0,x0〉) I) @
  72 (* [0x18ED] PSHA            *) (compile m ? PSHA maINH I) @
  73 (* [0x18EE] LDA 1,X         *) (compile m ? LDA (maIX1 〈x0,x1〉) I) @
  74 (* [0x18F0] ADC #0x01       *) (compile m ? ADC (maIMM1 〈x0,x1〉) I) @
  75 (* [0x18F2] PSHA            *) (compile m ? PSHA maINH I) @
  76 (* [0x18F3] LDA 4,X         *) (compile m ? LDA (maIX1 〈x0,x4〉) I) @
  77 (* [0x18F5] SUB 2,X         *) (compile m ? SUB (maIX1 〈x0,x2〉) I) @
  78 (* [0x18F7] STA ,X          *) (compile m ? STA maIX0 I) @
  79 (* [0x18F8] LDA 3,X         *) (compile m ? LDA (maIX1 〈x0,x3〉) I) @
  80 (* [0x18FA] SBC 1,X         *) (compile m ? SBC (maIX1 〈x0,x1〉) I) @
  81 (* [0x18FC] PSHA            *) (compile m ? PSHA maINH I) @
  82 (* [0x18FD] LDX ,X          *) (compile m ? LDX maIX0 I) @
  83 (* [0x18FE] PULH            *) (compile m ? PULH maINH I) @
  84 (* [0x18FF] AIX #-1         *) (compile m ? AIX (maIMM1 〈xF,xF〉) I) @
  85 (* [0x1901] TXA             *) (compile m ? TXA maINH I) @
  86 (* [0x1902] ADD #0x00       *) (compile m ? ADD (maIMM1 〈x0,x0〉) I) @
  87 (* [0x1904] PSHH            *) (compile m ? PSHH maINH I) @
  88 (* [0x1905] TSX             *) (compile m ? TSX maINH I) @
  89 (* [0x1906] STA 3,X         *) (compile m ? STA (maIX1 〈x0,x3〉) I) @
  90 (* [0x1908] PULA            *) (compile m ? PULA maINH I) @
  91 (* [0x1909] ADC #0x01       *) (compile m ? ADC (maIMM1 〈x0,x1〉) I) @
  92 (* [0x190B] LDX 3,X         *) (compile m ? LDX (maIX1 〈x0,x3〉) I) @
  93 (* [0x190D] PSHA            *) (compile m ? PSHA maINH I) @
  94 (* [0x190E] PULH            *) (compile m ? PULH maINH I) @
  95 (* [0x190F] BSR *-70 ; 18C9 *) (compile m ? BSR (maIMM1 〈xB,x8〉) I) @
  96 (* [0x1911] AIS #2          *) (compile m ? AIS (maIMM1 〈x0,x2〉) I) @
  97 (* [0x1913] TSX             *) (compile m ? TSX maINH I) @
  98 (* [0x1914] INC 2,X         *) (compile m ? INC (maIX1 〈x0,x2〉) I) @
  99 (* [0x1916] BNE *+4 ; 191A  *) (compile m ? BNE (maIMM1 〈x0,x2〉) I) @
 100 (* [0x1918] INC 1,X         *) (compile m ? INC (maIX1 〈x0,x1〉) I) @
 101 (* [0x191A] TSX             *) (compile m ? TSX maINH I) @
 102 (* [0x191B] LDA 3,X         *) (compile m ? LDA (maIX1 〈x0,x3〉) I) @
 103 (* [0x191D] PSHA            *) (compile m ? PSHA maINH I) @
 104 (* [0x191E] PULH            *) (compile m ? PULH maINH I) @
 105 (* [0x191F] LSRA            *) (compile m ? LSR maINHA I) @
 106 (* [0x1920] TSX             *) (compile m ? TSX maINH I) @
 107 (* [0x1921] LDX 4,X         *) (compile m ? LDX (maIX1 〈x0,x4〉) I) @
 108 (* [0x1923] RORX            *) (compile m ? ROR maINHX I) @
 109 (* [0x1924] PSHA            *) (compile m ? PSHA maINH I) @
 110 (* [0x1925] PULH            *) (compile m ? PULH maINH I) @
 111 (* [0x1926] CPHX 2,SP       *) (compile m ? CPHX (maSP1 〈x0,x2〉) I) @
 112 (* [0x1929] BHI *-65 ; 18E8 *) (compile m ? BHI (maIMM1 〈xB,xD〉) I)
 113
 114 (* [0x192B] !FINE!
 115             attraverso simulazione in CodeWarrior si puo' enunciare che dopo
 116             42+79*n+5*(n>>9) ci sara' il reverse di n byte (PARI) e
 117             H:X=n/2 *)
 118  ).
 119
 120 (* creazione del processore+caricamento+impostazione registri *)
 121 ndefinition dTest_HCS08_sReverse_status ≝
 122 λt:memory_impl.
 123 λA_op:byte8.
 124 λHX_op:word16.
 125 λelems:word16.
 126 λdata:list byte8.
 127  set_acc_8_low_reg HCS08 t (* A<-A_op *)
 128  (set_z_flag HCS08 t (* Z<-true *)
 129   (setweak_sp_reg HCS08 t (* SP<-0x0D4A *)
 130    (setweak_indX_16_reg HCS08 t (* H:X<-HX_op *)
 131     (set_pc_reg HCS08 t (* PC<-0x18E0 *)
 132      (start_of_mcu_version_HCS08 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 (FamilyHCS08 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  A_op.
 145
 146 (* parametrizzazione dell'enunciato del teorema *)
 147 (* primo sbozzo: confronto esecuzione con hexdump... *)
 148 nlemma dTest_HCS08_sReverse_dump_aux ≝
 149 λt:memory_impl.λstring:list byte8.
 150  (* 1) la stringa deve avere una lunghezza ∈ [0,3072] *)
 151  (byte8_bounded_strlen string 〈〈x0,xC〉:〈x0,x0〉〉) ∧
 152  (* 2) la stringa deve avere lunghezza pari *)
 153  ((and_b8 (w16l (byte8_strlen string)) 〈x0,x1〉) = 〈x0,x0〉) ∧
 154  (* 3) match di esecuzione su tempo in forma di tempo esatto *)
 155  (match execute HCS08 t
 156   (* parametri IN: t,H:X,strlen(string),string *)
 157   (TickOK ? (dTest_HCS08_sReverse_status t 〈x0,x0〉 〈〈x0,xD〉:〈x4,xB〉〉 (byte8_strlen string) string))
 158   (* tempo di esecuzione 42+79*n+5*(n>>9) *)
 159   (42+79*(nat_of_word16 (byte8_strlen string))+5*((nat_of_word16 (byte8_strlen string))/512)) with
 160    [ TickERR s _ ⇒ None ?
 161    (* azzeramento tutta RAM tranne dati *)
 162    | TickSUSP s _ ⇒ None ?
 163    | TickOK s ⇒ Some ? (byte8_hexdump t (mem_desc HCS08 t s) dTest_HCS08_RAM (nat_of_word16 (byte8_strlen string)))
 164    ] =
 165   Some ? (reverse_list ? string)).
 166
 167 (* confronto esecuzione con hexdump... *)
 168 (*
 169 lemma dTest_HCS08_sReverse_dump :
 170  dTest_HCS08_sReverse_dump_aux MEM_TREE dTest_random_32.
 171  unfold dTest_HCS08_sReverse_dump_aux;
 172  split;
 173  [ split; [ normalize in ⊢ (%); autobatch ] reflexivity ]
 174  reflexivity.
 175 qed.
 176 *)
 177
 178 (* parametrizzazione dell'enunciato del teorema *)
 179 (* dimostrazione senza svolgimento degli stati *)
 180 nlemma 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,x0〉 〈〈x0,xD〉:〈x4,xB〉〉 (byte8_strlen string) string))
 190   (* tempo di esecuzione 42+79*n+5*(n>>9) *)
 191   (42+79*(nat_of_word16 (byte8_strlen string))+5*((nat_of_word16 (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 (mem_desc HCS08 t s) dTest_zeros 〈〈x0,xD〉:〈x0,x0〉〉))
 196    ] =
 197   Some ? (set_pc_reg HCS08 t
 198    (dTest_HCS08_sReverse_status t (fst … (shr_b8 (w16h (byte8_strlen string)))) (fst … (shr_w16 (byte8_strlen string))) (byte8_strlen string) (reverse_list ? string))
 199    (mk_word16 (mk_byte8 x1 x9) (mk_byte8 x2 xB)))).
 200
 201 (*
 202 lemma dTest_HCS08_sReverse :
 203  dTest_HCS08_sReverse_aux MEM_TREE dTest_random_32.
 204  unfold dTest_HCS08_sReverse_aux;
 205  split;
 206  [ split; [ normalize in ⊢ (%); autobatch ] reflexivity ]
 207
 208  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⇒?] ?);
 209  letin status0 ≝ (dTest_HCS08_sReverse_status MEM_TREE 〈〈x0,xD〉:〈x4,xB〉〉 (byte8_strlen dTest_random_32) dTest_random_32);
 210  change in ⊢ (? ? match ? ? ? (? ? ? % ?) ? in tick_result return ? with [TickERR⇒?|TickSUSP⇒?|TickOK⇒?] ?) with
 211   (TickOK ? status0);
 212  rewrite > (execute_HCS08_LDHX_maIMM2 MEM_TREE status0 〈x0,x0〉 〈x2,x0〉) in ⊢ (? ? match ? ? ? % ? in tick_result return ? with [TickERR⇒?|TickSUSP⇒?|TickOK⇒?] ?);
 213  [ 2,3,4,5: reflexivity; ]
 214
 215  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));
 216  change in ⊢ (? ? match ? ? ? % ? in tick_result return ? with [TickERR⇒?|TickSUSP⇒?|TickOK⇒?] ?) with (TickOK ? status1);
 217
 218  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⇒?] ?);
 219  change in ⊢ (? ? match ? ? ? (? ? ? % ?) ? in tick_result return ? with [TickERR⇒?|TickSUSP⇒?|TickOK⇒?] ?) with (TickOK ? status1);
 220  rewrite > (execute_HCS08_STHX_maSP1 status1 〈x0,x4〉)
 221   in ⊢ (? ? match ? ? ? % ? in tick_result return ? with [TickERR⇒?|TickSUSP⇒?|TickOK⇒?] ?);
 222  [ 2,3,4,5,6,7: reflexivity; ]
 223
 224  elim daemon.
 225
 226 qed.
 227 *)
 228
 229 ndefinition sReverseCalc ≝
 230 λstring:list byte8.
 231  match execute HCS08 MEM_TREE
 232   (TickOK ? (dTest_HCS08_sReverse_status MEM_TREE 〈x0,x0〉 〈〈x0,xD〉:〈x4,xB〉〉 (byte8_strlen string) string))
 233   (42+79*(nat_of_word16 (byte8_strlen string))+5*((nat_of_word16 (byte8_strlen string))/512)) with
 234    [ TickERR s _ ⇒ None ?
 235    | TickSUSP s _ ⇒ None ?
 236    | 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〉〉))
 237    ].
 238
 239 ndefinition sReverseNoCalc ≝
 240 λstring:list byte8.
 241  Some ? (set_pc_reg HCS08 MEM_TREE
 242    (dTest_HCS08_sReverse_status MEM_TREE (fst … (shr_b8 (w16h (byte8_strlen string))))
 243                                          (fst … (shr_w16 (byte8_strlen string)))
 244                                          (byte8_strlen string) (reverse_list ? string))
 245    (mk_word16 (mk_byte8 x1 x9) (mk_byte8 x2 xB))).
 246
 247 ndefinition sReverseCalc32   ≝ sReverseCalc dTest_random_32.
 248 ndefinition sReverseCalc64   ≝ sReverseCalc dTest_random_64.
 249 ndefinition sReverseCalc128  ≝ sReverseCalc dTest_random_128.
 250 ndefinition sReverseCalc256  ≝ sReverseCalc dTest_random_256.
 251 ndefinition sReverseCalc512  ≝ sReverseCalc dTest_random_512.
 252 ndefinition sReverseCalc1024 ≝ sReverseCalc dTest_random_1024.
 253 ndefinition sReverseCalc2048 ≝ sReverseCalc dTest_random_2048.
 254 ndefinition sReverseCalc3072 ≝ sReverseCalc dTest_random_3072.
 255
 256 ndefinition sReverseNoCalc32   ≝ sReverseNoCalc dTest_random_32.
 257 ndefinition sReverseNoCalc64   ≝ sReverseNoCalc dTest_random_64.
 258 ndefinition sReverseNoCalc128  ≝ sReverseNoCalc dTest_random_128.
 259 ndefinition sReverseNoCalc256  ≝ sReverseNoCalc dTest_random_256.
 260 ndefinition sReverseNoCalc512  ≝ sReverseNoCalc dTest_random_512.
 261 ndefinition sReverseNoCalc1024 ≝ sReverseNoCalc dTest_random_1024.
 262 ndefinition sReverseNoCalc2048 ≝ sReverseNoCalc dTest_random_2048.
 263 ndefinition sReverseNoCalc3072 ≝ sReverseNoCalc dTest_random_3072.
 264
 265 (* *********************** *)
 266 (* HCS08GB60 Counting Sort *)
 267 (* *********************** *)
 268
 269 (* versione ridotta, in cui non si riazzerano gli elementi di counters *)
 270 ndefinition dTest_HCS08_cSort_source : word16 → (list byte8) ≝
 271 λelems:word16.
 272 let m ≝ HCS08 in source_to_byte8 m (
 273 (* BEFORE: A=0x00 H:X=0x0F4C SP=0x0F4B PC=0x18C8 Z=true *)
 274
 275 (* /* IPOTESI: INIT VARIABILI+ARRAY GIA' ESEGUITO */
 276    static unsigned int counters[256]={ campitura di 0 };
 277    static unsigned char dati[3072]={ dati random };
 278
 279    void CountingSort(void)
 280     {
 281     unsigned int index=0,position=0; *)
 282
 283 (* /* TESI: CODICE DA ESEGUIRE
 284
 285     /* calcolo del # ripetizioni degli elementi byte */
 286     for(;index<3072;index++)
 287      { counters[dati[index]]++; } *)
 288
 289 (* [0x18C8] BRA *+31;18E7 *) (compile m ? BRA (maIMM1 〈x1,xD〉) I) @
 290 (* [0x18CA] LDHX 1,SP     *) (compile m ? LDHX (maSP1 〈x0,x1〉) I) @
 291 (* [0x18CD] LDA 256,X     *) (compile m ? LDA (maIX2 〈〈x0,x1〉:〈x0,x0〉〉) I) @
 292 (* [0x18D0] LSLA          *) (compile m ? ASL maINHA I) @
 293 (* [0x18D1] CLRX          *) (compile m ? CLR maINHX I) @
 294 (* [0x18D2] ROLX          *) (compile m ? ROL maINHX I) @
 295 (* [0x18D3] ADD #0x00     *) (compile m ? ADD (maIMM1 〈x0,x0〉) I) @
 296 (* [0x18D5] PSHA          *) (compile m ? PSHA maINH I) @
 297 (* [0x18D6] TXA           *) (compile m ? TXA maINH I) @
 298 (* [0x18D7] ADC #0x0D     *) (compile m ? ADC (maIMM1 〈x0,xD〉) I) @
 299 (* [0x18D9] PSHA          *) (compile m ? PSHA maINH I) @
 300 (* [0x18DA] PULH          *) (compile m ? PULH maINH I) @
 301 (* [0x18DB] PULX          *) (compile m ? PULX maINH I) @
 302 (* [0x18DC] INC 1,X       *) (compile m ? INC (maIX1 〈x0,x1〉) I) @
 303 (* [0x18DE] BNE *+3       *) (compile m ? BNE (maIMM1 〈x0,x1〉) I) @
 304 (* [0x18E0] INC ,X        *) (compile m ? INC maIX0 I) @
 305 (* [0x18E1] TSX           *) (compile m ? TSX maINH I) @
 306 (* [0x18E2] INC 1,X       *) (compile m ? INC (maIX1 〈x0,x1〉) I) @
 307 (* [0x18E4] BNE *+3       *) (compile m ? BNE (maIMM1 〈x0,x1〉) I) @
 308 (* [0x18E6] INC ,X        *) (compile m ? INC maIX0 I) @
 309 (* [0x18E7] LDHX 1,SP     *) (compile m ? LDHX (maSP1 〈x0,x1〉) I) @
 310 (* [0x18EA] CPHX #elems   *) (compile m ? CPHX (maIMM2 elems) I) @ (* dimensione dei dati al massimo 0x0C00 *)
 311 (* [0x18ED] BCS *-35;18CA *) (compile m ? BCS (maIMM1 〈xD,xB〉) I) @
 312
 313 (* /* sovrascrittura di dati per produrre la versione ordinata */
 314    for(index=0;index<256;index++)
 315     {
 316     while(counters[index]--)
 317      { dati[position++]=index; }
 318     } *)
 319
 320 (* [0x18EF] TSX          *) (compile m ? TSX maINH I) @
 321 (* [0x18F0] CLR 1,X      *) (compile m ? CLR (maIX1 〈x0,x1〉) I) @
 322 (* [0x18F2] CLR ,X       *) (compile m ? CLR maIX0 I) @
 323 (* [0x18F3] BRA *+16     *) (compile m ? BRA (maIMM1 〈x0,xE〉) I) @
 324 (* [0x18F5] TSX          *) (compile m ? TSX maINH I) @
 325 (* [0x18F6] LDA 1,X      *) (compile m ? LDA (maIX1 〈x0,x1〉) I) @
 326 (* [0x18F8] LDHX 3,SP    *) (compile m ? LDHX (maSP1 〈x0,x3〉) I) @
 327 (* [0x18FB] STA 256,X    *) (compile m ? STA (maIX2 〈〈x0,x1〉:〈x0,x0〉〉) I) @
 328 (* [0x18FE] AIX #1       *) (compile m ? AIX (maIMM1 〈x0,x1〉) I) @
 329 (* [0x1900] STHX 3,SP    *) (compile m ? STHX (maSP1 〈x0,x3〉) I) @
 330 (* [0x1903] TSX          *) (compile m ? TSX maINH I) @
 331 (* [0x1904] LDX 1,X      *) (compile m ? LDX (maIX1 〈x0,x1〉) I) @
 332 (* [0x1906] LSLX         *) (compile m ? ASL maINHX I) @
 333 (* [0x1907] LDA 1,SP     *) (compile m ? LDA (maSP1 〈x0,x1〉) I) @
 334 (* [0x190A] ROLA         *) (compile m ? ROL maINHA I) @
 335 (* [0x190B] PSHA         *) (compile m ? PSHA maINH I) @
 336 (* [0x190C] PULH         *) (compile m ? PULH maINH I) @
 337 (* [0x190D] PSHX         *) (compile m ? PSHX maINH I) @
 338 (* [0x190E] LDHX 3328,X  *) (compile m ? LDHX (maIX2 〈〈x0,xD〉:〈x0,x0〉〉) I) @
 339 (* [0x1912] PSHX         *) (compile m ? PSHX maINH I) @
 340 (* [0x1913] PSHH         *) (compile m ? PSHH maINH I) @
 341 (* [0x1914] AIX #-1      *) (compile m ? AIX (maIMM1 〈xF,xF〉) I) @
 342 (* [0x1916] PSHH         *) (compile m ? PSHH maINH I) @
 343 (* [0x1917] PSHA         *) (compile m ? PSHA maINH I) @
 344 (* [0x1918] PULH         *) (compile m ? PULH maINH I) @
 345 (* [0x1919] PSHX         *) (compile m ? PSHX maINH I) @
 346 (* [0x191A] LDX 5,SP     *) (compile m ? LDX (maSP1 〈x0,x5〉) I) @
 347 (* [0x191D] PULA         *) (compile m ? PULA maINH I) @
 348 (* [0x191E] STA 3329,X   *) (compile m ? STA (maIX2 〈〈x0,xD〉:〈x0,x1〉〉) I) @
 349 (* [0x1921] PULA         *) (compile m ? PULA maINH I) @
 350 (* [0x1922] STA 3328,X   *) (compile m ? STA (maIX2 〈〈x0,xD〉:〈x0,x0〉〉) I) @
 351 (* [0x1925] PULH         *) (compile m ? PULH maINH I) @
 352 (* [0x1926] PULX         *) (compile m ? PULX maINH I) @
 353 (* [0x1927] CPHX #0x0000 *) (compile m ? CPHX (maIMM2 〈〈x0,x0〉:〈x0,x0〉〉) I) @
 354 (* [0x192A] PULH         *) (compile m ? PULH maINH I) @
 355 (* [0x192B] BNE *-54     *) (compile m ? BNE (maIMM1 〈xC,x8〉) I) @
 356 (* [0x192D] TSX          *) (compile m ? TSX maINH I) @
 357 (* [0x192E] INC 1,X      *) (compile m ? INC (maIX1 〈x0,x1〉) I) @
 358 (* [0x1930] BNE *+3      *) (compile m ? BNE (maIMM1 〈x0,x1〉) I) @
 359 (* [0x1932] INC ,X       *) (compile m ? INC maIX0 I) @
 360 (* [0x1933] LDHX 1,SP    *) (compile m ? LDHX (maSP1 〈x0,x1〉) I) @
 361 (* [0x1936] CPHX #0x0100 *) (compile m ? CPHX (maIMM2 〈〈x0,x1〉:〈x0,x0〉〉) I) @
 362 (* [0x1939] BNE *-54     *) (compile m ? BNE (maIMM1 〈xC,x8〉) I) @
 363 (* [0x193B] STOP         *) (compile m ? STOP maINH I)
 364
 365 (* [0x193C] !FINE!
 366             attraverso simulazione in CodeWarrior si puo' enunciare che dopo
 367             25700+150n si sara' entrati in stato STOP corrispondente con ordinamento
 368             di n byte, A=0xFF H:X=0x0100 *)
 369  ).
 370
 371 (* creazione del processore+caricamento+impostazione registri *)
 372 ndefinition dTest_HCS08_cSort_status ≝
 373 λt:memory_impl.
 374 λI_op:bool.
 375 λA_op:byte8.
 376 λHX_op:word16.
 377 λelems:word16.
 378 λdata:list byte8.
 379  setweak_i_flag HCS08 t (* I<-I_op *)
 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_HCS08
 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 (FamilyHCS08 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   I_op.
 400
 401 (* parametrizzazione dell'enunciato del teorema parziale *)
 402 nlemma dTest_HCS08_cSort_aux ≝
 403 λt:memory_impl.λstring:list byte8.
 404  (* 1) la stringa deve avere una lunghezza ∈ [0,3072] *)
 405  (byte8_bounded_strlen string 〈〈x0,xC〉:〈x0,x0〉〉) ∧
 406  (* 2) match di esecuzione su tempo in forma di upperbound *)
 407  (match execute HCS08 t
 408   (* parametri IN: t,A,H:X,strlen(string),string *)
 409   (TickOK ? (dTest_HCS08_cSort_status t true 〈x0,x0〉 〈〈x0,xF〉:〈x4,xC〉〉 (byte8_strlen string) string))
 410   (* tempo di esecuzione 25700+150*n *)
 411   ((nat_of_word16 〈〈x6,x4〉:〈x6,x4〉〉)+(nat_of_byte8 〈x9,x6〉)*(nat_of_word16 (byte8_strlen string))) with
 412    [ TickERR s _ ⇒ None ?
 413    (* azzeramento tutta RAM tranne dati *)
 414    | 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〉〉))
 415    | TickOK s ⇒ None ?
 416    ] =
 417   Some ? (set_pc_reg HCS08 t
 418    (dTest_HCS08_cSort_status t false 〈xF,xF〉 〈〈x0,x1〉:〈x0,x0〉〉 (byte8_strlen string) (byte8_list_ordering string))
 419    (mk_word16 (mk_byte8 x1 x9) (mk_byte8 x3 xC)))).
 420
 421 (* dimostrazione senza svolgimento degli stati *)
 422 (*
 423 lemma dTest_HCS08_cSort :
 424  dTest_HCS08_cSort_aux MEM_TREE dTest_random_32.
 425  unfold dTest_HCS08_cSort_aux;
 426  split;
 427  [ normalize in ⊢ (%); autobatch ]
 428  reflexivity.
 429 qed.
 430 *)
 431
 432 ndefinition cSortCalc ≝
 433 λstring:list byte8.
 434  match execute HCS08 MEM_TREE
 435   (TickOK ? (dTest_HCS08_cSort_status MEM_TREE true 〈x0,x0〉 〈〈x0,xF〉:〈x4,xC〉〉 (byte8_strlen string) string))
 436   ((nat_of_word16 〈〈x6,x4〉:〈x6,x4〉〉)+(nat_of_byte8 〈x9,x6〉)*(nat_of_word16 (byte8_strlen string))) with
 437    [ TickERR s _ ⇒ None ?
 438    | 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〉〉))
 439    | TickOK s ⇒ None ?
 440    ].
 441
 442 ndefinition cSortNoCalc ≝
 443 λstring:list byte8.
 444  Some ? (set_pc_reg HCS08 MEM_TREE
 445    (dTest_HCS08_cSort_status MEM_TREE false 〈xF,xF〉 〈〈x0,x1〉:〈x0,x0〉〉 (byte8_strlen string) (byte8_list_ordering string))
 446    (mk_word16 (mk_byte8 x1 x9) (mk_byte8 x3 xC))).
 447
 448 ndefinition cSortCalc32   ≝ cSortCalc dTest_random_32.
 449 ndefinition cSortCalc64   ≝ cSortCalc dTest_random_64.
 450 ndefinition cSortCalc128  ≝ cSortCalc dTest_random_128.
 451 ndefinition cSortCalc256  ≝ cSortCalc dTest_random_256.
 452 ndefinition cSortCalc512  ≝ cSortCalc dTest_random_512.
 453 ndefinition cSortCalc1024 ≝ cSortCalc dTest_random_1024.
 454 ndefinition cSortCalc2048 ≝ cSortCalc dTest_random_2048.
 455 ndefinition cSortCalc3072 ≝ cSortCalc dTest_random_3072.
 456
 457 ndefinition cSortNoCalc32   ≝ cSortNoCalc dTest_random_32.
 458 ndefinition cSortNoCalc64   ≝ cSortNoCalc dTest_random_64.
 459 ndefinition cSortNoCalc128  ≝ cSortNoCalc dTest_random_128.
 460 ndefinition cSortNoCalc256  ≝ cSortNoCalc dTest_random_256.
 461 ndefinition cSortNoCalc512  ≝ cSortNoCalc dTest_random_512.
 462 ndefinition cSortNoCalc1024 ≝ cSortNoCalc dTest_random_1024.
 463 ndefinition cSortNoCalc2048 ≝ cSortNoCalc dTest_random_2048.
 464 ndefinition cSortNoCalc3072 ≝ cSortNoCalc dTest_random_3072.
 465
 466 (* ********************** *)
 467 (* HCS08GB60 numeri aurei *)
 468 (* ********************** *)
 469
 470 (* versione ridotta, in cui non si riazzerano gli elementi di counters *)
 471 ndefinition dTest_HCS08_gNum_source : word16 → (list byte8) ≝
 472 λelems:word16.
 473 let m ≝ HCS08 in source_to_byte8 m (
 474 (* BEFORE: A=0x00 HX=0x1A00 PC=0x18BE SP=0x016F Z=1 (I=1) *)
 475
 476 (*
 477 static unsigned int result[16]={ 0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0 };
 478 word result[16] = 0x0100
 479
 480 void goldenNumbers(void)
 481 {
 482 unsigned int res_pos=0,tested_num=0,divisor=0;
 483 unsigned long int acc=0;
 484 *)
 485
 486 (* [0x18BE] AIS #-10   *) (compile m ? AIS (maIMM1 〈xF,x6〉) I) @
 487 (* [0x18C0] TSX        *) (compile m ? TSX maINH I) @
 488 (* [0x18C1] CLR 9,x    *) (compile m ? CLR (maIX1 〈x0,x9〉) I) @
 489 (* [0x18C3] CLR 8,X    *) (compile m ? CLR (maIX1 〈x0,x8〉) I) @
 490 (* [0x18C5] CLR 1,X    *) (compile m ? CLR (maIX1 〈x0,x1〉) I) @
 491 (* [0x18C7] CLR ,X     *) (compile m ? CLR maIX0 I) @
 492 (* [0x18C8] CLR 3,X    *) (compile m ? CLR (maIX1 〈x0,x3〉) I) @
 493 (* [0x18CA] CLR 2,X    *) (compile m ? CLR (maIX1 〈x0,x2〉) I) @
 494 (* [0x18CC] JSR 0x1951 *) (compile m ? JSR (maIMM2 〈〈x1,x9〉:〈x5,x1〉〉) I) @
 495
 496 (*
 497 for(tested_num=1;tested_num<2;tested_num++)
 498  {
 499 *)
 500
 501 (* [0x18CF] STHX 1,SP          *) (compile m ? STHX (maSP1 〈x0,x1〉) I) @
 502 (* [0x18D2] BRA *+116 ; 0x1946 *) (compile m ? BRA (maIMM1 〈x7,x2〉) I) @
 503 (* [0x18D4] BSR *+125 ; 0x1951 *) (compile m ? BSR (maIMM1 〈x7,xB〉) I) @
 504 (* [0x18D6] STHX 3,SP          *) (compile m ? STHX (maSP1 〈x0,x3〉) I) @
 505
 506 (*
 507  for(acc=0,divisor=1;divisor<tested_num;divisor++)
 508   {
 509   if(!(tested_num%divisor))
 510    { acc+=divisor; }
 511   }
 512 *)
 513
 514 (* [0x18D9] BRA *+61 ; 0x1916 *) (compile m ? BRA (maIMM1 〈x3,xB〉) I) @
 515 (* [0x18DB] LDHX 1,SP         *) (compile m ? LDHX (maSP1 〈x0,x1〉) I) @
 516 (* [0x18DE] PSHX              *) (compile m ? PSHX maINH I) @
 517 (* [0x18DF] PSHH              *) (compile m ? PSHH maINH I) @
 518 (* [0x18E0] LDHX 5,SP         *) (compile m ? LDHX (maSP1 〈x0,x5〉) I) @
 519 (* [0x18E3] JSR 0x1A1A        *) (compile m ? JSR (maIMM2 〈〈x1,xA〉:〈x1,xA〉〉) I) @
 520 (* [0x18E6] AIS #2            *) (compile m ? AIS (maIMM1 〈x0,x2〉) I) @
 521 (* [0x18E8] CPHX #0x0000      *) (compile m ? CPHX (maIMM2 〈〈x0,x0〉:〈x0,x0〉〉) I) @
 522 (* [0x18EB] BNE *+33 ; 0x190C *) (compile m ? BNE (maIMM1 〈x1,xF〉) I) @
 523 (* [0x18ED] TSX               *) (compile m ? TSX maINH I) @
 524 (* [0x18EE] LDA 3,X           *) (compile m ? LDA (maIX1 〈x0,x3〉) I) @
 525 (* [0x18F0] LDX 2,X           *) (compile m ? LDX (maIX1 〈x0,x2〉) I) @
 526 (* [0x18F2] PSHA              *) (compile m ? PSHA maINH I) @
 527 (* [0x18F3] PSHX              *) (compile m ? PSHX maINH I) @
 528 (* [0x18F4] CLRA              *) (compile m ? CLR maINHA I) @
 529 (* [0x18F5] PSHA              *) (compile m ? PSHA maINH I) @
 530 (* [0x18F6] PSHA              *) (compile m ? PSHA maINH I) @
 531 (* [0x18F7] TSX               *) (compile m ? TSX maINH I) @
 532 (* [0x18F8] PSHX              *) (compile m ? PSHX maINH I) @
 533 (* [0x19F9] PSHH              *) (compile m ? PSHH maINH I) @
 534 (* [0x18FA] AIX #8            *) (compile m ? AIX (maIMM1 〈x0,x8〉) I) @
 535 (* [0x18FC] PSHX              *) (compile m ? PSHX maINH I) @
 536 (* [0x18FD] PSHH              *) (compile m ? PSHH maINH I) @
 537 (* [0x18FE] LDHX 3,SP         *) (compile m ? LDHX (maSP1 〈x0,x3〉) I) @
 538 (* [0x1901] JSR 0x1A2A        *) (compile m ? JSR (maIMM2 〈〈x1,xA〉:〈x2,xA〉〉) I) @
 539 (* [0x1904] TSX               *) (compile m ? TSX maINH I) @
 540 (* [0x1905] AIX #14           *) (compile m ? AIX (maIMM1 〈x0,xE〉) I) @
 541 (* [0x1907] JSR 0x1A30        *) (compile m ? JSR (maIMM2 〈〈x1,xA〉:〈x3,x0〉〉) I) @
 542 (* [0x190A] AIS #6            *) (compile m ? AIS (maIMM1 〈x0,x6〉) I) @
 543 (* [0x190C] STA 0x1800  !COP! *) (compile m ? STA (maDIR2 〈〈x0,xC〉:〈x0,x0〉〉) I) @
 544 (* [0x190F] TSX               *) (compile m ? TSX maINH I) @
 545 (* [0x1910] INC 3,X           *) (compile m ? INC (maIX1 〈x0,x3〉) I) @
 546 (* [0x1912] BNE *+4 ; 0x1916  *) (compile m ? BNE (maIMM1 〈x0,x2〉) I) @
 547 (* [0x1914] INC 2,X           *) (compile m ? INC (maIX1 〈x0,x2〉) I) @
 548 (* [0x1916] LDHX 1,SP         *) (compile m ? LDHX (maSP1 〈x0,x1〉) I) @
 549 (* [0x1919] CPHX 3,SP         *) (compile m ? CPHX (maSP1 〈x0,x3〉) I) @
 550 (* [0x191C] BHI *-65 ; 0x18DB *) (compile m ? BHI (maIMM1 〈xB,xD〉) I) @
 551
 552 (*
 553  if(acc==tested_num)
 554   { result[res_pos++]=tested_num; }
 555  }
 556 }
 557 *)
 558
 559 (* [0x191E] CPHX 7,SP          *) (compile m ? CPHX (maSP1 〈x0,x7〉) I) @
 560 (* [0x1921] BNE *+31 ; 0x1940  *) (compile m ? BNE (maIMM1 〈x1,xD〉) I) @
 561 (* [0x1923] LDHX 5,SP          *) (compile m ? LDHX (maSP1 〈x0,x5〉) I) @
 562 (* [0x1926] BNE *+26 ; 0x1940  *) (compile m ? BNE (maIMM1 〈x1,x8〉) I) @
 563 (* [0x1928] LDHX 9,SP          *) (compile m ? LDHX (maSP1 〈x0,x9〉) I) @
 564 (* [0x192B] PSHX               *) (compile m ? PSHX maINH I) @
 565 (* [0x192C] AIX #1             *) (compile m ? AIX (maIMM1 〈x0,x1〉) I) @
 566 (* [0x192E] STHX 10,SP         *) (compile m ? STHX (maSP1 〈x0,xA〉) I) @
 567 (* [0x1931] PULX               *) (compile m ? PULX maINH I) @
 568 (* [0x1932] LSLX               *) (compile m ? ASL maINHX I) @
 569 (* [0x1933] LDA 2,SP           *) (compile m ? LDA (maSP1 〈x0,x2〉) I) @
 570 (* [0x1936] CLRH               *) (compile m ? CLR maINHH I) @
 571 (* [0x1937] STA 257,X          *) (compile m ? STA (maIX2 〈〈x0,x1〉:〈x0,x1〉〉) I) @
 572 (* [0x193A] LDA 1,SP           *) (compile m ? LDA (maSP1 〈x0,x1〉) I) @
 573 (* [0x193D] STA 256,X          *) (compile m ? STA (maIX2 〈〈x0,x1〉:〈x0,x0〉〉) I) @
 574 (* [0x1940] TSX                *) (compile m ? TSX maINH I) @
 575 (* [0x1941] INC 1,X            *) (compile m ? INC (maIX1 〈x0,x1〉) I) @
 576 (* [0x1943] BNE *+3 ; 0x1946   *) (compile m ? BNE (maIMM1 〈x0,x1〉) I) @
 577 (* [0x1945] INC ,X             *) (compile m ? INC maIX0 I) @
 578 (* [0x1946] LDHX 1,SP          *) (compile m ? LDHX (maSP1 〈x0,x1〉) I) @
 579 (* [0x1949] CPHX #elems        *) (compile m ? CPHX (maIMM2 elems) I) @
 580 (* [0x194C] BCS *-120 ; 0x18D4 *) (compile m ? BCS (maIMM1 〈x8,x6〉) I) @
 581 (* [0x194E] AIS #10            *) (compile m ? AIS (maIMM1 〈x0,xA〉) I) @
 582 (* [0x1950] STOP ->1951 !FINE! *) (compile m ? STOP maINH I) @
 583 (* [0x1951] CLRX               *) (compile m ? CLR maINHX I) @
 584 (* [0x1952] CLRH               *) (compile m ? CLR maINHH I) @
 585 (* [0x1953] STHX 9,SP          *) (compile m ? STHX (maSP1 〈x0,x9〉) I) @
 586 (* [0x1956] CLRH               *) (compile m ? CLR maINHH I) @
 587 (* [0x1957] STHX 7,SP          *) (compile m ? STHX (maSP1 〈x0,x7〉) I) @
 588 (* [0x195A] INCX               *) (compile m ? INC maINHX I) @
 589 (* [0x195B] RTS                *) (compile m ? RTS maINH I) @
 590
 591 (*
 592 static void _PUSH_ARGS_L(void) { ... }
 593 *)
 594
 595 (* [0x195C] LDA 3,X    *) (compile m ? LDA (maIX1 〈x0,x3〉) I) @
 596 (* [0x195E] PSHA       *) (compile m ? PSHA maINH I) @
 597 (* [0x195F] LDA 2,X    *) (compile m ? LDA (maIX1 〈x0,x2〉) I) @
 598 (* [0x1961] PSHA       *) (compile m ? PSHA maINH I) @
 599 (* [0x1962] LDHX ,X    *) (compile m ? LDHX maIX0 I) @
 600 (* [0x1964] PSHX       *) (compile m ? PSHX maINH I) @
 601 (* [0x1965] PSHH       *) (compile m ? PSHH maINH I) @
 602 (* [0x1966] LDHX 7,SP  *) (compile m ? LDHX (maSP1 〈x0,x7〉) I) @
 603 (* [0x1969] LDA 3,X    *) (compile m ? LDA (maIX1 〈x0,x3〉) I) @
 604 (* [0x196B] STA 17,SP  *) (compile m ? STA (maSP1 〈x1,x1〉) I) @
 605 (* [0x196E] LDA 2,X    *) (compile m ? LDA (maIX1 〈x0,x2〉) I) @
 606 (* [0x1970] STA 16,SP  *) (compile m ? STA (maSP1 〈x1,x0〉) I) @
 607 (* [0x1973] LDHX ,X    *) (compile m ? LDHX maIX0 I) @
 608 (* [0x1975] STHX 14,SP *) (compile m ? STHX (maSP1 〈x0,xE〉) I) @
 609 (* [0x1978] LDHX 5,SP  *) (compile m ? LDHX (maSP1 〈x0,x5〉) I) @
 610 (* [0x197B] JMP ,X     *) (compile m ? JMP maINHX0ADD I) @
 611
 612 (*
 613 static void _ENTER_BINARY_L(void) { ... }
 614 *)
 615
 616 (* [0x197C] PSHA       *) (compile m ? PSHA maINH I) @
 617 (* [0x197D] PSHX       *) (compile m ? PSHX maINH I) @
 618 (* [0x197E] PSHH       *) (compile m ? PSHH maINH I) @
 619 (* [0x197F] PSHX       *) (compile m ? PSHX maINH I) @
 620 (* [0x1980] PSHH       *) (compile m ? PSHH maINH I) @
 621 (* [0x1981] LDHX 6,SP  *) (compile m ? LDHX (maSP1 〈x0,x6〉) I) @
 622 (* [0x1984] PSHX       *) (compile m ? PSHX maINH I) @
 623 (* [0x1985] PSHH       *) (compile m ? PSHH maINH I) @
 624 (* [0x1986] LDHX 10,SP *) (compile m ? LDHX (maSP1 〈x0,xA〉) I) @
 625 (* [0x1989] STHX 8,SP  *) (compile m ? STHX (maSP1 〈x0,x8〉) I) @
 626 (* [0x198C] LDHX 12,SP *) (compile m ? LDHX (maSP1 〈x0,xC〉) I) @
 627 (* [0x198F] JMP 0x195C *) (compile m ? JMP (maIMM2 〈〈x1,x9〉:〈x5,xC〉〉) I) @
 628
 629 (*
 630 static void _IDIVMOD (char dummy_sgn, int j, int dummy, int i, ...) { ... }
 631 *)
 632
 633 (* [0x1992] TST 4,SP            *) (compile m ? TST (maSP1 〈x0,x4〉) I) @
 634 (* [0x1995] BNE *+28 ; 0x19B1   *) (compile m ? BNE (maIMM1 〈x1,xA〉) I) @
 635 (* [0x1997] TSX                 *) (compile m ? TSX maINH I) @
 636 (* [0x1998] LDA 7,X             *) (compile m ? LDA (maIX1 〈x0,x7〉) I) @
 637 (* [0x199A] LDX 4,X             *) (compile m ? LDX (maIX1 〈x0,x4〉) I) @
 638 (* [0x199C] CLRH                *) (compile m ? CLR maINHH I) @
 639 (* [0x199D] DIV                 *) (compile m ? DIV maINH I) @
 640 (* [0x199E] STA 4,SP            *) (compile m ? STA (maSP1 〈x0,x4〉) I) @
 641 (* [0x19A1] LDA 9,SP            *) (compile m ? LDA (maSP1 〈x0,x9〉) I) @
 642 (* [0x19A4] DIV                 *) (compile m ? DIV maINH I) @
 643 (* [0x19A5] STA 5,SP            *) (compile m ? STA (maSP1 〈x0,x5〉) I) @
 644 (* [0x19A8] CLR 8,SP            *) (compile m ? CLR (maSP1 〈x0,x8〉) I) @
 645 (* [0x19AB] PSHH                *) (compile m ? PSHH maINH I) @
 646 (* [0x19AC] PULA                *) (compile m ? PULA maINH I) @
 647 (* [0x19AD] STA 9,SP            *) (compile m ? STA (maSP1 〈x0,x9〉) I) @
 648 (* [0x19B0] RTS                 *) (compile m ? RTS maINH I) @
 649 (* [0x19B1] CLRA                *) (compile m ? CLR maINHA I) @
 650 (* [0x19B2] PSHA                *) (compile m ? PSHA maINH I) @
 651 (* [0x19B3] LDX #0x08           *) (compile m ? LDX (maIMM1 〈x0,x8〉) I) @
 652 (* [0x19B5] CLC                 *) (compile m ? CLC maINH I) @
 653 (* [0x19B6] ROL 10,SP           *) (compile m ? ROL (maSP1 〈x0,xA〉) I) @
 654 (* [0x19B9] ROL 9,SP            *) (compile m ? ROL (maSP1 〈x0,x9〉) I) @
 655 (* [0x19BC] ROL 1,SP            *) (compile m ? ROL (maSP1 〈x0,x1〉) I) @
 656 (* [0x19BF] LDA 5,SP            *) (compile m ? LDA (maSP1 〈x0,x5〉) I) @
 657 (* [0x19C2] CMP 1,SP            *) (compile m ? CMP (maSP1 〈x0,x1〉) I) @
 658 (* [0x19C5] BHI *+31 ; 0x19E4   *) (compile m ? BHI (maIMM1 〈x1,xD〉) I) @
 659 (* [0x19C7] BNE *+10 ; 0x19D1   *) (compile m ? BNE (maIMM1 〈x0,x8〉) I) @
 660 (* [0x19C9] LDA 6,SP            *) (compile m ? LDA (maSP1 〈x0,x6〉) I) @
 661 (* [0x19CC] CMP 9,SP            *) (compile m ? CMP (maSP1 〈x0,x9〉) I) @
 662 (* [0x19CF] BHI *+21 ; 0x19E4   *) (compile m ? BHI (maIMM1 〈x1,x3〉) I) @
 663 (* [0x19D1] LDA 9,SP            *) (compile m ? LDA (maSP1 〈x0,x9〉) I) @
 664 (* [0x19D4] SUB 6,SP            *) (compile m ? SUB (maSP1 〈x0,x6〉) I) @
 665 (* [0x19D7] STA 9,SP            *) (compile m ? STA (maSP1 〈x0,x9〉) I) @
 666 (* [0x19DA] LDA 1,SP            *) (compile m ? LDA (maSP1 〈x0,x1〉) I) @
 667 (* [0x19DD] SBC 5,SP            *) (compile m ? SBC (maSP1 〈x0,x5〉) I) @
 668 (* [0x19E0] STA 1,SP            *) (compile m ? STA (maSP1 〈x0,x1〉) I) @
 669 (* [0x19E3] SEC                 *) (compile m ? SEC maINH I) @
 670 (* [0x19E4] DBNZX *-46 ; 0x19B6 *) (compile m ? DBNZ (maINHX_and_IMM1 〈xD,x0〉) I) @
 671 (* [0x19E6] LDA 10,SP           *) (compile m ? LDA (maSP1 〈x0,xA〉) I) @
 672 (* [0x19E9] ROLA                *) (compile m ? ROL maINHA I) @
 673 (* [0x19EA] STA 6,SP            *) (compile m ? STA (maSP1 〈x0,x6〉) I) @
 674 (* [0x19ED] LDA 9,SP            *) (compile m ? LDA (maSP1 〈x0,x9〉) I) @
 675 (* [0x19F0] STA 10,SP           *) (compile m ? STA (maSP1 〈x0,xA〉) I) @
 676 (* [0x19F3] PULA                *) (compile m ? PULA maINH I) @
 677 (* [0x19F4] STA 8,SP            *) (compile m ? STA (maSP1 〈x0,x8〉) I) @
 678 (* [0x19F7] CLR 4,SP            *) (compile m ? CLR (maSP1 〈x0,x4〉) I) @
 679 (* [0x19FA] RTS                 *) (compile m ? RTS maINH I) @
 680
 681 (*
 682 static void _LADD_k_is_k_plus_j(_PARAM_BINARY_L) { ... }
 683 *)
 684
 685 (* [0x19FB] TSX      *) (compile m ? TSX maINH I) @
 686 (* [0x19FC] LDA 18,X *) (compile m ? LDA (maIX1 〈x1,x2〉) I) @
 687 (* [0x19FE] ADD 5,X  *) (compile m ? ADD (maIX1 〈x0,x5〉) I) @
 688 (* [0x1A00] STA 18,X *) (compile m ? STA (maIX1 〈x1,x2〉) I) @
 689 (* [0x1A02] LDA 17,X *) (compile m ? LDA (maIX1 〈x1,x1〉) I) @
 690 (* [0x1A04] ADC 4,X  *) (compile m ? ADC (maIX1 〈x0,x4〉) I) @
 691 (* [0x1A06] STA 17,X *) (compile m ? STA (maIX1 〈x1,x1〉) I) @
 692 (* [0x1A08] LDA 16,X *) (compile m ? LDA (maIX1 〈x1,x0〉) I) @
 693 (* [0x1A0A] ADC 3,X  *) (compile m ? ADC (maIX1 〈x0,x3〉) I) @
 694 (* [0x1A0C] STA 16,X *) (compile m ? STA (maIX1 〈x1,x0〉) I) @
 695 (* [0x1A0E] LDA 15,X *) (compile m ? LDA (maIX1 〈x0,xF〉) I) @
 696 (* [0x1A10] ADC 2,X  *) (compile m ? ADC (maIX1 〈x0,x2〉) I) @
 697 (* [0x1A12] STA 15,X *) (compile m ? STA (maIX1 〈x0,xF〉) I) @
 698 (* [0x1A14] AIS #10  *) (compile m ? AIS (maIMM1 〈x0,xA〉) I) @
 699 (* [0x1A16] PULH     *) (compile m ? PULH maINH I) @
 700 (* [0x1A17] PULX     *) (compile m ? PULX maINH I) @
 701 (* [0x1A18] PULA     *) (compile m ? PULA maINH I) @
 702 (* [0x1A19] RTS      *) (compile m ? RTS maINH I) @
 703
 704 (*
 705 void _IMODU_STAR08(int i, ...) { ... }
 706 *)
 707
 708 (* [0x1A1A] AIS #-2    *) (compile m ? AIS (maIMM1 〈xF,xE〉) I) @
 709 (* [0x1A1C] STHX 1,SP  *) (compile m ? STHX (maSP1 〈x0,x1〉) I) @
 710 (* [0x1A1F] PSHA       *) (compile m ? PSHA maINH I) @
 711 (* [0x1A20] JSR 0x1992 *) (compile m ? JSR (maIMM2 〈〈x1,x9〉:〈x9,x2〉〉) I) @
 712 (* [0x1A23] PULA       *) (compile m ? PULA maINH I) @
 713 (* [0x1A24] AIS #2     *) (compile m ? AIS (maIMM1 〈x0,x2〉) I) @
 714 (* [0x1A26] LDHX 3,SP  *) (compile m ? LDHX (maSP1 〈x0,x3〉) I) @
 715 (* [0x1A29] RTS        *) (compile m ? RTS maINH I) @
 716
 717 (*
 718 void _LADD(void) { ... }
 719 *)
 720
 721 (* [0x1A2A] JSR 0x197C *) (compile m ? JSR (maIMM2 〈〈x1,x9〉:〈x7,xC〉〉) I) @
 722 (* [0x1A2D] JSR 0x19FB *) (compile m ? JSR (maIMM2 〈〈x1,x9〉:〈xF,xB〉〉) I) @
 723
 724 (*
 725 void _POP32(void) { ... }
 726 *)
 727
 728 (* [0x1A30] PSHA     *) (compile m ? PSHA maINH I) @
 729 (* [0x1A31] LDA 4,SP *) (compile m ? LDA (maSP1 〈x0,x4〉) I) @
 730 (* [0x1A34] STA ,X   *) (compile m ? STA maIX0 I) @
 731 (* [0x1A35] LDA 5,SP *) (compile m ? LDA (maSP1 〈x0,x5〉) I) @
 732 (* [0x1A38] STA 1,X  *) (compile m ? STA (maIX1 〈x0,x1〉) I) @
 733 (* [0x1A3A] LDA 6,SP *) (compile m ? LDA (maSP1 〈x0,x6〉) I) @
 734 (* [0x1A3D] STA 2,X  *) (compile m ? STA (maIX1 〈x0,x2〉) I) @
 735 (* [0x1A3F] LDA 7,SP *) (compile m ? LDA (maSP1 〈x0,x7〉) I) @
 736 (* [0x1A42] STA 3,X  *) (compile m ? STA (maIX1 〈x0,x3〉) I) @
 737 (* [0x1A44] PULA     *) (compile m ? PULA maINH I) @
 738 (* [0x1A45] PULH     *) (compile m ? PULH maINH I) @
 739 (* [0x1A46] PULX     *) (compile m ? PULX maINH I) @
 740 (* [0x1A47] AIS #4   *) (compile m ? AIS (maIMM1 〈x0,x4〉) I) @
 741 (* [0x1A49] JMP ,X   *) (compile m ? JMP maINHX0ADD I)
 742
 743 (* attraverso simulazione in CodeWarrior si puo' enunciare che dopo
 744    80+(65*n*(n+1)*(n+2))/6 si sara' entrati in stato STOP corrispondente
 745    AFTER: HX=num PC=0x1951 I=0 *)
 746  ).
 747
 748 (* creazione del processore+caricamento+impostazione registri *)
 749 ndefinition dTest_HCS08_gNum_status ≝
 750 λt:memory_impl.
 751 λI_op:bool.
 752 λA_op:byte8.
 753 λHX_op:word16.
 754 λPC_op:word16.
 755 λaddr:word16.
 756 λelems:word16.
 757 λdata:list byte8.
 758  setweak_i_flag HCS08 t (* I<-I_op *)
 759   (set_acc_8_low_reg HCS08 t (* A<-A_op *)
 760    (set_z_flag HCS08 t (* Z<-true *)
 761     (setweak_sp_reg HCS08 t (* SP<-0x016F *)
 762      (setweak_indX_16_reg HCS08 t (* H:X<-HX_op *)
 763       (set_pc_reg HCS08 t (* PC<-PC_op *)
 764        (start_of_mcu_version_HCS08
 765         MC9S08GB60 t
 766         (load_from_source_at t (* carica data in RAM:dTest_HCS08_RAM *)
 767          (load_from_source_at t (zero_memory t) (* carica source in ROM:addr *)
 768            (dTest_HCS08_cSort_source elems) addr)
 769           data dTest_HCS08_RAM)
 770         (build_memory_type_of_mcu_version (FamilyHCS08 MC9S08GB60) t)
 771         (mk_byte8 x0 x0) (mk_byte8 x0 x0) (* non deterministici tutti a 0 *)
 772         false false false false false false) (* non deterministici tutti a 0 *)
 773        PC_op)
 774       HX_op)
 775      (mk_word16 (mk_byte8 x0 x1) (mk_byte8 x6 xF)))
 776     true)
 777    A_op)
 778   I_op.
 779
 780 (* NUMERI AUREI: Somma divisori(x)=x, fino a 0xFFFF sono 6/28/496/8128 *)
 781 ndefinition dTest_HCS08_gNum_aurei ≝
 782 λnum:word16.match gt_w16 num 〈〈x1,xF〉:〈xC,x0〉〉 with
 783  [ true ⇒ [ 〈x0,x0〉 ; 〈x0,x6〉 ; 〈x0,x0〉 ; 〈x1,xC〉 ; 〈x0,x1〉 ; 〈xF,x0〉 ; 〈x1,xF〉 ; 〈xC,x0〉 ]
 784  | false ⇒ match gt_w16 num 〈〈x0,x1〉:〈xF,x0〉〉 with
 785   [ true ⇒ [ 〈x0,x0〉 ; 〈x0,x6〉 ; 〈x0,x0〉 ; 〈x1,xC〉 ; 〈x0,x1〉 ; 〈xF,x0〉 ; 〈x0,x0〉 ; 〈x0,x0〉 ]
 786   | false ⇒ match gt_w16 num 〈〈x0,x0〉:〈x1,xC〉〉 with
 787    [ true ⇒ [ 〈x0,x0〉 ; 〈x0,x6〉 ; 〈x0,x0〉 ; 〈x1,xC〉 ; 〈x0,x0〉 ; 〈x0,x0〉 ; 〈x0,x0〉 ; 〈x0,x0〉 ]
 788    | false ⇒ match gt_w16 num 〈〈x0,x0〉:〈x0,x6〉〉 with
 789     [ true ⇒ [ 〈x0,x0〉 ; 〈x0,x6〉 ; 〈x0,x0〉 ; 〈x0,x0〉 ; 〈x0,x0〉 ; 〈x0,x0〉 ; 〈x0,x0〉 ; 〈x0,x0〉 ]
 790     | false ⇒ [ 〈x0,x0〉 ; 〈x0,x0〉 ; 〈x0,x0〉 ; 〈x0,x0〉 ; 〈x0,x0〉 ; 〈x0,x0〉 ; 〈x0,x0〉 ; 〈x0,x0〉 ]
 791     ]
 792    ]
 793   ]
 794  ] @ [ 〈x0,x0〉 ; 〈x0,x0〉 ; 〈x0,x0〉 ; 〈x0,x0〉 ; 〈x0,x0〉 ; 〈x0,x0〉 ; 〈x0,x0〉 ; 〈x0,x0〉
 795      ; 〈x0,x0〉 ; 〈x0,x0〉 ; 〈x0,x0〉 ; 〈x0,x0〉 ; 〈x0,x0〉 ; 〈x0,x0〉 ; 〈x0,x0〉 ; 〈x0,x0〉
 796      ; 〈x0,x0〉 ; 〈x0,x0〉 ; 〈x0,x0〉 ; 〈x0,x0〉 ; 〈x0,x0〉 ; 〈x0,x0〉 ; 〈x0,x0〉 ; 〈x0,x0〉 ].
 797
 798 (* esecuzione execute k*(n+2) *)
 799 nlet rec dTest_HCS08_gNum_execute1 (m:mcu_type) (t:memory_impl) (s:tick_result (any_status m t)) (n,ntot:nat) on n ≝
 800  match s with
 801   [ TickERR s' error ⇒ TickERR ? s' error
 802   | TickSUSP s' susp ⇒ TickSUSP ? s' susp
 803   | TickOK s' ⇒ match n with
 804    [ O ⇒ TickOK ? s'
 805    | S n' ⇒ dTest_HCS08_gNum_execute1 m t (execute m t (TickOK ? s') (ntot+2)) n' ntot ]
 806   ].
 807
 808 (* esecuzione execute k*(n+1)*(n+2) *)
 809 nlet rec dTest_HCS08_gNum_execute2 (m:mcu_type) (t:memory_impl) (s:tick_result (any_status m t)) (n,ntot:nat) on n ≝
 810  match s with
 811   [ TickERR s' error ⇒ TickERR ? s' error
 812   | TickSUSP s' susp ⇒ TickSUSP ? s' susp
 813   | TickOK s' ⇒ match n with
 814    [ O ⇒ TickOK ? s'
 815    | S n' ⇒ dTest_HCS08_gNum_execute2 m t (dTest_HCS08_gNum_execute1 m t (TickOK ? s') (ntot+1) ntot) n' ntot ]
 816   ].
 817
 818 (* esecuzione execute k*n*(n+1)*(n+2) *)
 819 nlet rec dTest_HCS08_gNum_execute3 (m:mcu_type) (t:memory_impl) (s:tick_result (any_status m t)) (n,ntot:nat) on n ≝
 820  match s with
 821   [ TickERR s' error ⇒ TickERR ? s' error
 822   | TickSUSP s' susp ⇒ TickSUSP ? s' susp
 823   | TickOK s' ⇒ match n with
 824    [ O ⇒ TickOK ? s'
 825    | S n' ⇒ dTest_HCS08_gNum_execute3 m t (dTest_HCS08_gNum_execute2 m t (TickOK ? s') ntot ntot) n' ntot ]
 826   ].
 827
 828 (* esecuzione execute 80+11*n*(n+1)*(n+2) *)
 829 ndefinition dTest_HCS08_gNum_execute4 ≝
 830 λm:mcu_type.λt:memory_impl.λs:tick_result (any_status m t).λntot:nat.
 831  match s with
 832   [ TickERR s' error ⇒ TickERR ? s' error
 833   | TickSUSP s' susp ⇒ TickSUSP ? s' susp
 834   | TickOK s' ⇒ execute m t (dTest_HCS08_gNum_execute3 m t (TickOK ? s') 11 ntot) 80
 835   ].
 836
 837 (* parametrizzazione dell'enunciato del teorema parziale *)
 838 nlemma dTest_HCS08_gNum_aux ≝
 839 λt:memory_impl.λnum:word16.
 840  (* 2) match di esecuzione su tempo in forma di upperbound *)
 841  match dTest_HCS08_gNum_execute4 HCS08 t
 842   (TickOK ? (dTest_HCS08_gNum_status t true 〈x0,x0〉 〈〈x1,xA〉:〈x0,x0〉〉 〈〈x1,x8〉:〈xB,xE〉〉 〈〈x1,x8〉:〈xB,xE〉〉 num dTest_zeros))
 843   (* tempo di esecuzione 80+11*n*(n+1)*(n+2) *)
 844   (nat_of_word16 num) with
 845    [ TickERR s _ ⇒ None ?
 846    (* azzeramento tutta RAM tranne dati *)
 847    | TickSUSP s _ ⇒ Some ? (set_mem_desc HCS08 t s (load_from_source_at t (mem_desc HCS08 t s) dTest_zeros3K 〈〈x0,x1〉:〈x2,x0〉〉))
 848    | TickOK s ⇒ None ?
 849    ] =
 850   Some ? (dTest_HCS08_gNum_status t false 〈x0,x0〉 num 〈〈x1,x9〉:〈x5,x1〉〉 〈〈x1,x8〉:〈xB,xE〉〉 num (dTest_HCS08_gNum_aurei num)).
 851
 852 ndefinition gNumCalc ≝
 853 λnum:word16.
 854  match dTest_HCS08_gNum_execute4 HCS08 MEM_TREE
 855   (TickOK ? (dTest_HCS08_gNum_status MEM_TREE true 〈x0,x0〉 〈〈x1,xA〉:〈x0,x0〉〉 〈〈x1,x8〉:〈xB,xE〉〉 〈〈x1,x8〉:〈xB,xE〉〉 num dTest_zeros))
 856   (nat_of_word16 num) with
 857    [ TickERR s _ ⇒ None ?
 858    | TickSUSP s _ ⇒ Some ? (set_mem_desc HCS08 MEM_TREE s (load_from_source_at MEM_TREE (mem_desc HCS08 MEM_TREE s) dTest_zeros3K 〈〈x0,x1〉:〈x2,x0〉〉))
 859    | TickOK s ⇒ None ?
 860    ].
 861
 862 ndefinition gNumNoCalc ≝
 863 λnum:word16.
 864  Some ? (dTest_HCS08_gNum_status MEM_TREE false 〈x0,x0〉 num 〈〈x1,x9〉:〈x5,x1〉〉 〈〈x1,x8〉:〈xB,xE〉〉 num (dTest_HCS08_gNum_aurei num)).
 865
 866 ndefinition gNumCalc1    ≝ gNumCalc 〈〈x0,x0〉:〈x0,x1〉〉.
 867 ndefinition gNumCalc2    ≝ gNumCalc 〈〈x0,x0〉:〈x0,x2〉〉.
 868 ndefinition gNumCalc5    ≝ gNumCalc 〈〈x0,x0〉:〈x0,x5〉〉.
 869 ndefinition gNumCalc10   ≝ gNumCalc 〈〈x0,x0〉:〈x0,xA〉〉.
 870 ndefinition gNumCalc20   ≝ gNumCalc 〈〈x0,x0〉:〈x1,x4〉〉.
 871 ndefinition gNumCalc50   ≝ gNumCalc 〈〈x0,x0〉:〈x3,x2〉〉.
 872 ndefinition gNumCalc100  ≝ gNumCalc 〈〈x0,x0〉:〈x6,x4〉〉.
 873 ndefinition gNumCalc250  ≝ gNumCalc 〈〈x0,x0〉:〈xF,xA〉〉.
 874 ndefinition gNumCalc500  ≝ gNumCalc 〈〈x0,x1〉:〈xF,x4〉〉.
 875 ndefinition gNumCalc1000 ≝ gNumCalc 〈〈x0,x3〉:〈xE,x8〉〉.
 876
 877 ndefinition gNumNoCalc1    ≝ gNumNoCalc 〈〈x0,x0〉:〈x0,x1〉〉.
 878 ndefinition gNumNoCalc2    ≝ gNumNoCalc 〈〈x0,x0〉:〈x0,x2〉〉.
 879 ndefinition gNumNoCalc5    ≝ gNumNoCalc 〈〈x0,x0〉:〈x0,x5〉〉.
 880 ndefinition gNumNoCalc10   ≝ gNumNoCalc 〈〈x0,x0〉:〈x0,xA〉〉.
 881 ndefinition gNumNoCalc20   ≝ gNumNoCalc 〈〈x0,x0〉:〈x1,x4〉〉.
 882 ndefinition gNumNoCalc50   ≝ gNumNoCalc 〈〈x0,x0〉:〈x3,x2〉〉.
 883 ndefinition gNumNoCalc100  ≝ gNumNoCalc 〈〈x0,x0〉:〈x6,x4〉〉.
 884 ndefinition gNumNoCalc250  ≝ gNumNoCalc 〈〈x0,x0〉:〈xF,xA〉〉.
 885 ndefinition gNumNoCalc500  ≝ gNumNoCalc 〈〈x0,x1〉:〈xF,x4〉〉.
 886 ndefinition gNumNoCalc1000 ≝ gNumNoCalc 〈〈x0,x3〉:〈xE,x8〉〉.