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