source: src/ASM/Fetch.ma @ 1602

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

giving up on fetch proofs for time being

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