source: src/ASM/Fetch.ma @ 1598

Last change on this file since 1598 was 1598, checked in by mulligan, 8 years ago

changes over the last couple of days

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