source: src/ASM/Fetch.ma @ 1600

Last change on this file since 1600 was 1600, checked in by sacerdot, 8 years ago

utilities and ASM ported to the new standard library
File size: 26.3 KB
Line 
1include "ASM/BitVectorTrie.ma".
2include "ASM/Arithmetic.ma".
3include "ASM/ASM.ma".
4include "basics/russell.ma".
5
6definition bitvector_max_nat ≝
7  λlength: nat.
8    2^length.
9
10definition code_memory_size ≝ bitvector_max_nat 16.
11
12axiom bitvector_lt_bitvector_max_nat:
13  ∀length: nat.
14  ∀v: BitVector length.
15    nat_of_bitvector length v < bitvector_max_nat length.
16
17lemma word_lt_bitvector_max_nat:
18  ∀w: Word.
19    nat_of_bitvector … w < code_memory_size.
20  #w //
21qed.
22   
23axiom w_lt_half_add_increment:
24  ∀length: nat.
25  ∀v: BitVector length.
26  ∀proof: nat_of_bitvector … v < bitvector_max_nat length - 1.
27    nat_of_bitvector … v < nat_of_bitvector … (\snd (half_add … v (bitvector_of_nat … (S O)))).
28
29definition next: BitVectorTrie Byte 16 → ∀program_counter: Word.
30    nat_of_bitvector … program_counter < (code_memory_size - 1) →
31      Σret: Word × Byte. nat_of_bitvector … program_counter < nat_of_bitvector … (\fst ret) ≝
32  λpmem: BitVectorTrie Byte 16.
33  λpc: Word.
34  λproof.
35    〈\snd (half_add … pc (bitvector_of_nat 16 (S O))), lookup ? ? pc pmem (zero 8)〉.
36  @w_lt_half_add_increment @proof
37qed.
38
39axiom o_lt_p_to_m_lt_n_minus_o_to_m_lt_n_minus_p:
40  ∀m, n, o, p: nat.
41    p < o → m < n - o → m < n - p.
42
43lemma pair_eq_1_jmeq:
44  ∀a, b: Type[0].
45  ∀a1, a2: a.
46  ∀b1, b2: b.
47    〈a1, b1〉 ≃ 〈a2, b2〉 → a1 = a2.
48  #a #b #a1 #a2 #b1 #b2 #assm
49  cases daemon (* XXX: no jm discrimination for pairs *)
50qed.
51   
52lemma prod_fst_jmeq:
53  ∀a, b: Type[0].
54  ∀p: a × b.
55  ∀l: a.
56  ∀r: b.
57    p ≃ 〈l, r〉 → l = fst … p.
58  #a #b #p #l #r
59  cases p #aa #bb #assm @sym_eq
60  lapply (pair_eq_1_jmeq a b aa l bb r assm)
61  #assm assumption
62qed.
63
64lemma lt_to_le:
65  ∀m, n: nat.
66    m < n → m ≤ n.
67  #m #n #assm /2 by le_S_to_le/
68qed.
69
70lemma Prod_inv_rect_Type0:
71 ∀A,B. ∀P: A × B → Type[0].∀ab.
72  (∀a,b. ab = 〈a,b〉 → P 〈a,b〉) → P ab.
73 #A #B #P * /2/
74qed.
75
76notation > "hvbox('let' 〈ident x,ident y〉 {ident H} ≝ t 'in' s)"
77 with precedence 10
78for @{ Prod_inv_rect_Type0 ??? $t (λ${ident x}.λ${ident y}.λ${ident H}.$s) }.
79
80notation < "hvbox('let' 〈ident x,ident y〉 {ident H} ≝ t 'in' s)"
81 with precedence 10
82for @{ Prod_inv_rect_Type0 $z $w $r $t (λ${ident x}:$X.λ${ident y}:$Y.λ${ident H}:$h.$s) }.
83
84lemma breakup_pair' : ∀A,B,C:Type[0].∀x. ∀R:C → Prop. ∀P:∀a:A.∀b:B. x=〈a,b〉 → C.
85  R (P (\fst x) (\snd x) ?) → R (let 〈a,b〉 {H} ≝ x in P a b H).
86[2: // ]
87#A #B #C *; normalize /2/
88qed.
89
90(* timings taken from SIEMENS *)
91
92definition fetch0: BitVectorTrie Byte 16 → ∀program_counter: Word. Byte →
93  nat_of_bitvector … program_counter < code_memory_size - 24 (* 3 bytes *) →
94  Σret: instruction × Word × nat. nat_of_bitvector … program_counter ≤ nat_of_bitvector … (\snd (\fst ret)) ≝
95  λpmem.
96  λpc.
97  λv.
98  λproof.
99   let 〈b,v〉 ≝ head … v in if b then
100    let 〈b,v〉 ≝ head … v in if b then
101     let 〈b,v〉 ≝ head … v in if b then
102      let 〈b,v〉 ≝ head … v in if b then
103       let 〈b,v〉 ≝ head … v in if b then
104        〈〈RealInstruction (MOV … (inl … (inl … (inl … (inl … (inr … 〈REGISTER v,ACC_A〉)))))), pc〉, 1〉
105       else
106        let 〈b,v〉≝  head … v in if b then
107         let 〈b,v〉≝  head … v in if b then
108          〈〈RealInstruction (MOV … (inl … (inl … (inl … (inl … (inr … 〈INDIRECT (from_singl … v),ACC_A〉)))))), pc〉, 1〉
109         else
110          let 〈b,v〉≝  head … v in if b then
111           let 〈pc,b1〉 {EQ} ≝ next pmem pc ? in 〈〈RealInstruction (MOV … (inl … (inl … (inl … (inr … 〈DIRECT b1,ACC_A〉))))), pc〉, 1〉
112          else
113           〈〈RealInstruction (CPL … ACC_A), pc〉, 1〉
114        else
115         let 〈b,v〉≝  head … v in if b then
116          〈〈RealInstruction (MOVX … (inr … 〈EXT_INDIRECT (from_singl … v),ACC_A〉)), pc〉, 2〉
117         else
118          let 〈b,v〉≝  head … v in if b then
119           let 〈pc,b1〉 {EQ} ≝ next pmem pc ? in 〈〈ACALL … (ADDR11 (([[true;true;true]]) @@ b1)), pc〉, 2〉
120          else
121           〈〈RealInstruction (MOVX … (inr … 〈EXT_INDIRECT_DPTR,ACC_A〉)), pc〉, 2〉
122      else
123       let 〈b,v〉≝  head … v in if b then
124        〈〈RealInstruction (MOV … (inl … (inl … (inl … (inl … (inl … 〈ACC_A,REGISTER v〉)))))), pc〉, 1〉
125       else
126        let 〈b,v〉≝  head … v in if b then
127         let 〈b,v〉≝  head … v in if b then
128          〈〈RealInstruction (MOV … (inl … (inl … (inl … (inl … (inl … 〈ACC_A,INDIRECT (from_singl … v)〉)))))), pc〉, 1〉
129         else
130          let 〈b,v〉≝  head … v in if b then
131           let 〈pc,b1〉 {EQ} ≝ next pmem pc ? in 〈〈RealInstruction (MOV … (inl … (inl … (inl … (inl … (inl … 〈ACC_A,DIRECT b1〉)))))), pc〉, 1〉
132          else
133           〈〈RealInstruction (CLR … ACC_A), pc〉, 1〉
134        else
135         let 〈b,v〉≝  head … v in if b then
136          〈〈RealInstruction (MOVX … (inl … 〈ACC_A,EXT_INDIRECT (from_singl … v)〉)), pc〉, 2〉
137         else
138          let 〈b,v〉≝  head … v in if b then
139           let 〈pc,b1〉 {EQ} ≝ next pmem pc ? in 〈〈AJMP … (ADDR11 (([[true;true;true]]) @@ b1)), pc〉, 2〉
140          else
141           〈〈RealInstruction (MOVX … (inl … 〈ACC_A,EXT_INDIRECT_DPTR〉)), pc〉, 2〉
142     else
143      let 〈b,v〉≝  head … v in if b then
144       let 〈b,v〉≝  head … v in if b then
145        let 〈pc,b1〉 {EQ} ≝ next pmem pc ? in 〈〈RealInstruction (DJNZ … (REGISTER v) (RELATIVE b1)), pc〉, 2〉
146       else
147        let 〈b,v〉≝  head … v in if b then
148         let 〈b,v〉≝  head … v in if b then
149          〈〈RealInstruction (XCHD … ACC_A (INDIRECT (from_singl … v))), pc〉, 1〉
150         else
151          let 〈b,v〉≝  head … v in if b then
152           let 〈pc,b1〉 {EQ} ≝ next pmem pc ? in let 〈pc,b2〉≝ next pmem pc ? in 〈〈RealInstruction (DJNZ … (DIRECT b1) (RELATIVE b2)), pc〉, 2〉
153          else
154           〈〈RealInstruction (DA … ACC_A), pc〉, 1〉
155        else
156         let 〈b,v〉≝  head … v in if b then
157          let 〈b,v〉≝  head … v in if b then
158           〈〈RealInstruction (SETB … CARRY), pc〉, 1〉
159          else
160           let 〈pc,b1〉 {EQ} ≝ next pmem pc ? in 〈〈RealInstruction (SETB … (BIT_ADDR b1)), pc〉, 1〉
161         else
162          let 〈b,v〉≝  head … v in if b then
163           let 〈pc,b1〉 {EQ} ≝ next pmem pc ? in 〈〈ACALL … (ADDR11 (([[true;true;false]]) @@ b1)), pc〉, 2〉
164          else
165           let 〈pc,b1〉 {EQ} ≝ next pmem pc ? in 〈〈RealInstruction (POP … (DIRECT b1)), pc〉, 2〉
166      else
167       let 〈b,v〉≝  head … v in if b then
168        〈〈RealInstruction (XCH … ACC_A (REGISTER v)), pc〉, 1〉
169       else
170        let 〈b,v〉≝  head … v in if b then
171         let 〈b,v〉≝  head … v in if b then
172          〈〈RealInstruction (XCH … ACC_A (INDIRECT (from_singl … v))), pc〉, 1〉
173         else
174          let 〈b,v〉≝  head … v in if b then
175           let 〈pc,b1〉 {EQ} ≝ next pmem pc ? in 〈〈RealInstruction (XCH … ACC_A (DIRECT b1)), pc〉, 1〉
176          else
177           〈〈RealInstruction (SWAP … ACC_A), pc〉, 1〉
178        else
179         let 〈b,v〉≝  head … v in if b then
180          let 〈b,v〉≝  head … v in if b then
181           〈〈RealInstruction (CLR … CARRY), pc〉, 1〉
182          else
183           let 〈pc,b1〉 {EQ} ≝ next pmem pc ? in 〈〈RealInstruction (CLR … (BIT_ADDR b1)), pc〉, 1〉
184         else
185          let 〈b,v〉≝  head … v in if b then
186           let 〈pc,b1〉 {EQ} ≝ next pmem pc ? in 〈〈AJMP … (ADDR11 (([[true;true;false]]) @@ b1)), pc〉, 2〉
187          else
188           let 〈pc,b1〉 {EQ} ≝ next pmem pc ? in 〈〈RealInstruction (PUSH … (DIRECT b1)), pc〉, 2〉
189    else
190     let 〈b,v〉≝  head … v in if b then
191      let 〈b,v〉≝  head … v in if b then
192       let 〈b,v〉≝  head … v in if b then
193        let 〈pc,b1〉 {EQ} ≝ next pmem pc ? in let 〈pc,b2〉≝ next pmem pc ? in 〈〈RealInstruction (CJNE …  (inr … 〈REGISTER v,DATA b1〉) (RELATIVE b2)), pc〉, 2〉
194       else
195        let 〈b,v〉≝  head … v in if b then
196         let 〈b,v〉≝  head … v in if b then
197          let 〈pc,b1〉 {EQ} ≝ next pmem pc ? in let 〈pc,b2〉≝ next pmem pc ? in 〈〈RealInstruction (CJNE … (inr … 〈INDIRECT (from_singl … v),DATA b1〉) (RELATIVE b2)), pc〉, 2〉
198         else
199          let 〈b,v〉≝  head … v in if b then
200           let 〈pc,b1〉 {EQ} ≝ next pmem pc ? in let 〈pc,b2〉≝ next pmem pc ? in 〈〈RealInstruction (CJNE …  (inl … 〈ACC_A,DIRECT b1〉) (RELATIVE b2)), pc〉, 2〉
201          else
202           let 〈pc,b1〉 {EQ} ≝ next pmem pc ? in let 〈pc,b2〉≝ next pmem pc ? in 〈〈RealInstruction (CJNE … (inl … 〈ACC_A,DATA b1〉) (RELATIVE b2)), pc〉, 2〉
203        else
204         let 〈b,v〉≝  head … v in if b then
205          let 〈b,v〉≝  head … v in if b then
206           〈〈RealInstruction (CPL … CARRY), pc〉, 1〉
207          else
208           let 〈pc,b1〉 {EQ} ≝ next pmem pc ? in 〈〈RealInstruction (CPL … (BIT_ADDR b1)), pc〉, 1〉
209         else
210          let 〈b,v〉≝  head … v in if b then
211           let 〈pc,b1〉 {EQ} ≝ next pmem pc ? in 〈〈ACALL … (ADDR11 (([[true;false;true]]) @@ b1)), pc〉, 2〉
212          else
213           let 〈pc,b1〉 {EQ} ≝ next pmem pc ? in 〈〈RealInstruction (ANL … (inr … 〈CARRY,N_BIT_ADDR b1〉)), pc〉, 2〉
214      else
215       let 〈b,v〉≝  head … v in if b then
216        let 〈pc,b1〉 {EQ} ≝ next pmem pc ? in 〈〈RealInstruction (MOV … (inl … (inl … (inl … (inl … (inr … 〈REGISTER v,DIRECT b1〉)))))), pc〉, 2〉
217       else
218        let 〈b,v〉≝  head … v in if b then
219         let 〈b,v〉≝  head … v in if b then
220          let 〈pc,b1〉 {EQ} ≝ next pmem pc ? in 〈〈RealInstruction (MOV … (inl … (inl … (inl … (inl … (inr … 〈INDIRECT (from_singl … v),DIRECT b1〉)))))), pc〉, 2〉
221         else
222          〈〈RealInstruction (MUL … ACC_A ACC_B), pc〉, 4〉
223        else
224         let 〈b,v〉≝  head … v in if b then
225          let 〈b,v〉≝  head … v in if b then
226           〈〈RealInstruction (INC … DPTR), pc〉, 2〉
227          else
228           let 〈pc,b1〉 {EQ} ≝ next pmem pc ? in 〈〈RealInstruction (MOV … (inl … (inr … 〈CARRY,BIT_ADDR b1〉))), pc〉, 1〉
229         else
230          let 〈b,v〉≝  head … v in if b then
231           let 〈pc,b1〉 {EQ} ≝ next pmem pc ? in 〈〈AJMP … (ADDR11 (([[true;false;true]]) @@ b1)), pc〉, 2〉
232          else
233           let 〈pc,b1〉 {EQ} ≝ next pmem pc ? in 〈〈RealInstruction (ORL … (inr … 〈CARRY,N_BIT_ADDR b1〉)), pc〉, 2〉
234     else
235      let 〈b,v〉≝  head … v in if b then
236       let 〈b,v〉≝  head … v in if b then
237        〈〈RealInstruction (SUBB … ACC_A (REGISTER v)), pc〉, 1〉
238       else
239        let 〈b,v〉≝  head … v in if b then
240         let 〈b,v〉≝  head … v in if b then
241          〈〈RealInstruction (SUBB … ACC_A (INDIRECT (from_singl … v))), pc〉, 1〉
242         else
243          let 〈b,v〉≝  head … v in if b then
244           let 〈pc,b1〉 {EQ} ≝ next pmem pc ? in 〈〈RealInstruction (SUBB … ACC_A (DIRECT b1)), pc〉, 1〉
245          else
246           let 〈pc,b1〉 {EQ} ≝ next pmem pc ? in 〈〈RealInstruction (SUBB … ACC_A (DATA b1)), pc〉, 1〉
247        else
248         let 〈b,v〉≝  head … v in if b then
249          let 〈b,v〉≝  head … v in if b then
250           〈〈MOVC … ACC_A (ACC_DPTR), pc〉, 2〉
251          else
252           let 〈pc,b1〉 {EQ} ≝ next pmem pc ? in 〈〈RealInstruction (MOV … (inr … 〈BIT_ADDR b1,CARRY〉)), pc〉, 2〉
253         else
254          let 〈b,v〉≝  head … v in if b then
255           let 〈pc,b1〉 {EQ} ≝ next pmem pc ? in 〈〈ACALL … (ADDR11 (([[true;false;false]]) @@ b1)), pc〉, 2〉
256          else
257           let 〈pc,b1〉 {EQ} ≝ next pmem pc ? in let 〈pc,b2〉≝ next pmem pc ? in 〈〈RealInstruction (MOV … (inl … (inl … (inr … 〈DPTR,DATA16 (b1 @@ b2)〉)))), pc〉, 2〉
258      else
259       let 〈b,v〉≝  head … v in if b then
260        let 〈pc,b1〉 {EQ} ≝ next pmem pc ? in 〈〈RealInstruction (MOV … (inl … (inl … (inl … (inr … 〈DIRECT b1,REGISTER v〉))))), pc〉, 2〉
261       else
262        let 〈b,v〉≝  head … v in if b then
263         let 〈b,v〉≝  head … v in if b then
264          let 〈pc,b1〉 {EQ} ≝ next pmem pc ? in 〈〈RealInstruction (MOV … (inl … (inl … (inl … (inr … 〈DIRECT b1,INDIRECT (from_singl … v)〉))))), pc〉, 2〉
265         else
266          let 〈b,v〉≝  head … v in if b then
267           let 〈pc,b1〉 {EQ} ≝ next pmem pc ? in let 〈pc,b2〉≝ next pmem pc ? in 〈〈RealInstruction (MOV … (inl … (inl … (inl … (inr … 〈DIRECT b1,DIRECT b2〉))))), pc〉, 2〉
268          else
269           〈〈RealInstruction (DIV … ACC_A ACC_B), pc〉, 4〉
270        else
271         let 〈b,v〉≝  head … v in if b then
272          let 〈b,v〉≝  head … v in if b then
273           〈〈MOVC … ACC_A (ACC_PC), pc〉, 2〉
274          else
275           let 〈pc,b1〉 {EQ} ≝ next pmem pc ? in 〈〈RealInstruction (ANL … (inr … 〈CARRY,BIT_ADDR b1〉)), pc〉, 2〉
276         else
277          let 〈b,v〉≝  head … v in if b then
278           let 〈pc,b1〉 {EQ} ≝ next pmem pc ? in 〈〈AJMP … (ADDR11 (([[true;false;false]]) @@ b1)), pc〉, 2〉
279          else
280           let 〈pc,b1〉 {EQ} ≝ next pmem pc ? in 〈〈SJMP … (RELATIVE b1), pc〉, 2〉
281   else
282    let 〈b,v〉≝  head … v in if b then
283     let 〈b,v〉≝  head … v in if b then
284      let 〈b,v〉≝  head … v in if b then
285       let 〈b,v〉≝  head … v in if b then
286        let 〈pc,b1〉 {EQ} ≝ next pmem pc ? in 〈〈RealInstruction (MOV … (inl … (inl … (inl … (inl … (inr … 〈REGISTER v,DATA b1〉)))))), pc〉, 1〉
287       else
288        let 〈b,v〉≝  head … v in if b then
289         let 〈b,v〉≝  head … v in if b then
290          let 〈pc,b1〉 {EQ} ≝ next pmem pc ? in 〈〈RealInstruction (MOV … (inl … (inl … (inl … (inl … (inr … 〈INDIRECT (from_singl … v),DATA b1〉)))))), pc〉, 1〉
291         else
292          let 〈b,v〉≝  head … v in if b then
293           let 〈pc,b1〉 {EQ} ≝ next pmem pc ? in let 〈pc,b2〉≝ next pmem pc ? in 〈〈RealInstruction (MOV … (inl … (inl … (inl … (inr … 〈DIRECT b1,DATA b2〉))))), pc〉, 3〉
294          else
295           let 〈pc,b1〉 {EQ} ≝ next pmem pc ? in 〈〈RealInstruction (MOV … (inl … (inl … (inl … (inl … (inl … 〈ACC_A,DATA b1〉)))))), pc〉, 1〉
296        else
297         let 〈b,v〉≝  head … v in if b then
298          let 〈b,v〉≝  head … v in if b then
299           〈〈JMP … INDIRECT_DPTR, pc〉, 2〉
300          else
301           let 〈pc,b1〉 {EQ} ≝ next pmem pc ? in 〈〈RealInstruction (ORL … (inr … 〈CARRY,BIT_ADDR b1〉)), pc〉, 2〉
302         else
303          let 〈b,v〉≝  head … v in if b then
304           let 〈pc,b1〉 {EQ} ≝ next pmem pc ? in 〈〈ACALL … (ADDR11 (([[false;true;true]]) @@ b1)), pc〉, 2〉
305          else
306           let 〈pc,b1〉 {EQ} ≝ next pmem pc ? in 〈〈RealInstruction (JNZ … (RELATIVE b1)), pc〉, 2〉
307      else
308       let 〈b,v〉≝  head … v in if b then
309        〈〈RealInstruction (XRL … (inl … 〈ACC_A,REGISTER v〉)), pc〉, 1〉
310       else
311        let 〈b,v〉≝  head … v in if b then
312         let 〈b,v〉≝  head … v in if b then
313          〈〈RealInstruction (XRL … (inl … 〈ACC_A,INDIRECT (from_singl … v)〉)), pc〉, 1〉
314         else
315          let 〈b,v〉≝  head … v in if b then
316           let 〈pc,b1〉 {EQ} ≝ next pmem pc ? in 〈〈RealInstruction (XRL … (inl … 〈ACC_A,DIRECT b1〉)), pc〉, 1〉
317          else
318           let 〈pc,b1〉 {EQ} ≝ next pmem pc ? in 〈〈RealInstruction (XRL … (inl … 〈ACC_A,DATA b1〉)), pc〉, 1〉
319        else
320         let 〈b,v〉≝  head … v in if b then
321          let 〈b,v〉≝  head … v in if b then
322           let 〈pc,b1〉 {EQ} ≝ next pmem pc ? in let 〈pc,b2〉≝ next pmem pc ? in 〈〈RealInstruction (XRL … (inr … 〈DIRECT b1,DATA b2〉)), pc〉, 2〉
323          else
324           let 〈pc,b1〉 {EQ} ≝ next pmem pc ? in 〈〈RealInstruction (XRL … (inr … 〈DIRECT b1,ACC_A〉)), pc〉, 1〉
325         else
326          let 〈b,v〉≝  head … v in if b then
327           let 〈pc,b1〉 {EQ} ≝ next pmem pc ? in 〈〈AJMP … (ADDR11 (([[false;true;true]]) @@ b1)), pc〉, 2〉
328          else
329           let 〈pc,b1〉 {EQ} ≝ next pmem pc ? in 〈〈RealInstruction (JZ … (RELATIVE b1)), pc〉, 2〉
330     else
331      let 〈b,v〉≝  head … v in if b then
332       let 〈b,v〉≝  head … v in if b then
333        〈〈RealInstruction (ANL … (inl … (inl … 〈ACC_A,REGISTER v〉))), pc〉, 1〉
334       else
335        let 〈b,v〉≝  head … v in if b then
336         let 〈b,v〉≝  head … v in if b then
337          〈〈RealInstruction (ANL … (inl … (inl … 〈ACC_A,INDIRECT (from_singl … v)〉))), pc〉, 1〉
338         else
339          let 〈b,v〉≝  head … v in if b then
340           let 〈pc,b1〉 {EQ} ≝ next pmem pc ? in 〈〈RealInstruction (ANL … (inl … (inl … 〈ACC_A,DIRECT b1〉))), pc〉, 1〉
341          else
342           let 〈pc,b1〉 {EQ} ≝ next pmem pc ? in 〈〈RealInstruction (ANL … (inl … (inl … 〈ACC_A,DATA b1〉))), pc〉, 1〉
343        else
344         let 〈b,v〉≝  head … v in if b then
345          let 〈b,v〉≝  head … v in if b then
346           let 〈pc,b1〉 {EQ} ≝ next pmem pc ? in let 〈pc,b2〉≝ next pmem pc ? in 〈〈RealInstruction (ANL … (inl … (inr … 〈DIRECT b1,DATA b2〉))), pc〉, 2〉
347          else
348           let 〈pc,b1〉 {EQ} ≝ next pmem pc ? in 〈〈RealInstruction (ANL … (inl … (inr … 〈DIRECT b1,ACC_A〉))), pc〉, 1〉
349         else
350          let 〈b,v〉≝  head … v in if b then
351           let 〈pc,b1〉 {EQ} ≝ next pmem pc ? in 〈〈ACALL … (ADDR11 (([[false;true;false]]) @@ b1)), pc〉, 2〉
352          else
353           let 〈pc,b1〉 {EQ} ≝ next pmem pc ? in 〈〈RealInstruction (JNC … (RELATIVE b1)), pc〉, 2〉
354      else
355       let 〈b,v〉≝  head … v in if b then
356        〈〈RealInstruction (ORL … (inl … (inl … 〈ACC_A,REGISTER v〉))), pc〉, 1〉
357       else
358        let 〈b,v〉≝  head … v in if b then
359         let 〈b,v〉≝  head … v in if b then
360          〈〈RealInstruction (ORL … (inl … (inl … 〈ACC_A,INDIRECT (from_singl … v)〉))), pc〉, 1〉
361         else
362          let 〈b,v〉≝  head … v in if b then
363           let 〈pc,b1〉 {EQ} ≝ next pmem pc ? in 〈〈RealInstruction (ORL … (inl … (inl … 〈ACC_A,DIRECT b1〉))), pc〉, 1〉
364          else
365           let 〈pc,b1〉 {EQ} ≝ next pmem pc ? in 〈〈RealInstruction (ORL … (inl … (inl … 〈ACC_A,DATA b1〉))), pc〉, 1〉
366        else
367         let 〈b,v〉≝  head … v in if b then
368          let 〈b,v〉≝  head … v in if b then
369           let 〈pc,b1〉 {EQ} ≝ next pmem pc ? in let 〈pc,b2〉≝ next pmem pc ? in 〈〈RealInstruction (ORL … (inl … (inr … 〈DIRECT b1,DATA b2〉))), pc〉, 2〉
370          else
371           let 〈pc,b1〉 {EQ} ≝ next pmem pc ? in 〈〈RealInstruction (ORL … (inl … (inr … 〈DIRECT b1,ACC_A〉))), pc〉, 1〉
372         else
373          let 〈b,v〉≝  head … v in if b then
374           let 〈pc,b1〉 {EQ} ≝ next pmem pc ? in 〈〈AJMP … (ADDR11 (([[false;true;false]]) @@ b1)), pc〉, 2〉
375          else
376           let 〈pc,b1〉 {EQ} ≝ next pmem pc ? in 〈〈RealInstruction (JC … (RELATIVE b1)), pc〉, 2〉
377    else
378     let 〈b,v〉≝  head … v in if b then
379      let 〈b,v〉≝  head … v in if b then
380       let 〈b,v〉≝  head … v in if b then
381        〈〈RealInstruction (ADDC … ACC_A (REGISTER v)), pc〉, 1〉
382       else
383        let 〈b,v〉≝  head … v in if b then
384         let 〈b,v〉≝  head … v in if b then
385          〈〈RealInstruction (ADDC … ACC_A (INDIRECT (from_singl … v))), pc〉, 1〉
386         else
387          let 〈b,v〉≝  head … v in if b then
388           let 〈pc,b1〉 {EQ} ≝ next pmem pc ? in 〈〈RealInstruction (ADDC … ACC_A (DIRECT b1)), pc〉, 1〉
389          else
390           let 〈pc,b1〉 {EQ} ≝ next pmem pc ? in 〈〈RealInstruction (ADDC … ACC_A (DATA b1)), pc〉, 1〉
391        else
392         let 〈b,v〉≝  head … v in if b then
393          let 〈b,v〉≝  head … v in if b then
394           〈〈RealInstruction (RLC … ACC_A), pc〉, 1〉
395          else
396           〈〈RealInstruction (RETI …), pc〉, 2〉
397         else
398          let 〈b,v〉≝  head … v in if b then
399           let 〈pc,b1〉 {EQ} ≝ next pmem pc ? in 〈〈ACALL … (ADDR11 (([[false;false;true]]) @@ b1)), pc〉, 2〉
400          else
401           let 〈pc,b1〉 {EQ} ≝ next pmem pc ? in let 〈pc,b2〉≝ next pmem pc ? in 〈〈RealInstruction (JNB … (BIT_ADDR b1) (RELATIVE b2)), pc〉, 2〉
402      else
403       let 〈b,v〉≝  head … v in if b then
404        〈〈RealInstruction (ADD … ACC_A (REGISTER v)), pc〉, 1〉
405       else
406        let 〈b,v〉≝  head … v in if b then
407         let 〈b,v〉≝  head … v in if b then
408          〈〈RealInstruction (ADD … ACC_A (INDIRECT (from_singl … v))), pc〉, 1〉
409         else
410          let 〈b,v〉≝  head … v in if b then
411           let 〈pc,b1〉 {EQ} ≝ next pmem pc ? in 〈〈RealInstruction (ADD … ACC_A (DIRECT b1)), pc〉, 1〉
412          else
413           let 〈pc,b1〉 {EQ} ≝ next pmem pc ? in 〈〈RealInstruction (ADD … ACC_A (DATA b1)), pc〉, 1〉
414        else
415         let 〈b,v〉≝  head … v in if b then
416          let 〈b,v〉≝  head … v in if b then
417           〈〈RealInstruction (RL … ACC_A), pc〉, 1〉
418          else
419           〈〈RealInstruction (RET …), pc〉, 2〉
420         else
421          let 〈b,v〉≝  head … v in if b then
422           let 〈pc,b1〉 {EQ} ≝ next pmem pc ? in 〈〈AJMP … (ADDR11 (([[false;false;true]]) @@ b1)), pc〉, 2〉
423          else
424           let 〈pc,b1〉 {EQ} ≝ next pmem pc ? in let 〈pc,b2〉≝ next pmem pc ? in 〈〈RealInstruction (JB … (BIT_ADDR b1) (RELATIVE b2)), pc〉, 2〉
425     else
426      let 〈b,v〉≝  head … v in if b then
427       let 〈b,v〉≝  head … v in if b then
428        〈〈RealInstruction (DEC … (REGISTER v)), pc〉, 1〉
429       else
430        let 〈b,v〉≝  head … v in if b then
431         let 〈b,v〉≝  head … v in if b then
432          〈〈RealInstruction (DEC … (INDIRECT (from_singl … v))), pc〉, 1〉
433         else
434          let 〈b,v〉≝  head … v in if b then
435           let 〈pc,b1〉 {EQ} ≝ next pmem pc ? in 〈〈RealInstruction (DEC … (DIRECT b1)), pc〉, 1〉
436          else
437           〈〈RealInstruction (DEC … ACC_A), pc〉, 1〉
438        else
439         let 〈b,v〉≝  head … v in if b then
440          let 〈b,v〉≝  head … v in if b then
441           〈〈RealInstruction (RRC … ACC_A), pc〉, 1〉
442          else
443           let 〈pc,b1〉 {EQ} ≝ next pmem pc ? in let 〈pc,b2〉≝ next pmem pc ? in 〈〈LCALL … (ADDR16 (b1 @@ b2)), pc〉, 2〉
444         else
445          let 〈b,v〉≝  head … v in if b then
446           let 〈pc,b1〉 {EQ} ≝ next pmem pc ? in 〈〈ACALL … (ADDR11 (([[false;false;false]]) @@ b1)), pc〉, 2〉
447          else
448           let 〈pc,b1〉 {EQ} ≝ next pmem pc ? in let 〈pc,b2〉≝ next pmem pc ? in 〈〈RealInstruction (JBC … (BIT_ADDR b1) (RELATIVE b2)), pc〉, 2〉
449      else
450       let 〈b,v〉≝  head … v in if b then
451        〈〈RealInstruction (INC … (REGISTER v)), pc〉, 1〉
452       else
453        let 〈b,v〉≝  head … v in if b then
454         let 〈b,v〉≝  head … v in if b then
455          〈〈RealInstruction (INC … (INDIRECT (from_singl … v))), pc〉, 1〉
456         else
457          let 〈b,v〉≝  head … v in if b then
458           let 〈pc,b1〉 {EQ} ≝ next pmem pc ? in 〈〈RealInstruction (INC … (DIRECT b1)), pc〉, 1〉
459          else
460           〈〈RealInstruction (INC … ACC_A), pc〉, 1〉
461        else
462         let 〈b,v〉≝  head … v in if b then
463          let 〈b,v〉≝  head … v in if b then
464           〈〈RealInstruction (RR … ACC_A), pc〉, 1〉
465          else
466           let 〈pc,b1〉 {EQ} ≝ next pmem pc ? in let 〈pc,b2〉≝ next pmem pc ? in 〈〈LJMP … (ADDR16 (b1 @@ b2)), pc〉, 2〉
467         else
468          let 〈b,v〉≝  head … v in if b then
469           let 〈pc,b1〉 {EQ} ≝ next pmem pc ? in 〈〈AJMP … (ADDR11 (([[false;false;false]]) @@ b1)), pc〉, 2〉
470          else
471           〈〈RealInstruction (NOP …), pc〉, 1〉.
472  try %
473  try (
474    @(o_lt_p_to_m_lt_n_minus_o_to_m_lt_n_minus_p
475      (nat_of_bitvector 16 pc) code_memory_size 24 1
476      (le_S_S 1 23 (le_S_S O 22 (le_O_n 22))) proof)
477  )
478  [1,2,3,4,5,6,7,8:
479    @breakup_pair' cases (next pmem pc ?)
480    normalize * normalize #pc' #byte @lt_to_le
481  |3:
482    @breakup_pair' cases (next pmem pc ?)
483    normalize * normalize #pc' #byte @lt_to_le
484  |2:
485    @breakup_pair' cases(next pmem pc ?)
486    normalize * normalize #pc' #byte @lt_to_le
487  [
488  | 92:
489    cases (next ???) in EQ; * #pc' #content #H #EQ whd in EQ:(??%?); destruct
490   
491   
492    lapply(eq_pair_fst_snd ? ? (next pmem pc ?))
493    #assm >assm
494    cut(nat_of_bitvector … pc < nat_of_bitvector …
495      (\fst  (next pmem pc
496                (o_lt_p_to_m_lt_n_minus_o_to_m_lt_n_minus_p (nat_of_bitvector 16 pc)
497                 code_memory_size 24 1 (le_S_S 1 23 (le_S_S O 22 (le_O_n 22))) proof))))
498    [ @sig2
499    | #assm @lt_to_le assumption
500    ]
501  |92:
502    check next.
503    lapply pc -pc
504    @sig2
505  cases daemon (* XXX: requires rewrite of the above to make it more russell friendly *)
506qed.
507
508definition fetch: BitVectorTrie Byte 16 → ∀program_counter: Word.
509    Σret: instruction × Word × nat. nat_of_bitvector … program_counter < nat_of_bitvector … (\snd (\fst ret)) ≝
510  λpmem: BitVectorTrie Byte 16.
511  λpc: Word.
512  let 〈word, byte〉 ≝ next pmem pc ? in
513    fetch0 pmem word byte ?.
514  cases daemon (* XXX: todo, proofs about size of pc *)
515qed.
Note: See TracBrowser for help on using the repository browser.