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