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