source: src/ASM/Fetch.ma @ 1646

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

finished big proof in all but two cases

File size: 23.5 KB
RevLine 
[698]1include "ASM/BitVectorTrie.ma".
2include "ASM/Arithmetic.ma".
3include "ASM/ASM.ma".
[1600]4include "basics/russell.ma".
[475]5
[1591]6definition bitvector_max_nat ≝
7  λlength: nat.
8    2^length.
[475]9
[1591]10definition code_memory_size ≝ bitvector_max_nat 16.
11
[1604]12definition next: BitVectorTrie Byte 16 → ∀program_counter: Word. Word × Byte ≝
[1591]13  λpmem: BitVectorTrie Byte 16.
14  λpc: Word.
15    〈\snd (half_add … pc (bitvector_of_nat 16 (S O))), lookup ? ? pc pmem (zero 8)〉.
16
[1598]17lemma Prod_inv_rect_Type0:
18 ∀A,B. ∀P: A × B → Type[0].∀ab.
19  (∀a,b. ab = 〈a,b〉 → P 〈a,b〉) → P ab.
20 #A #B #P * /2/
21qed.
22
23notation > "hvbox('let' 〈ident x,ident y〉 {ident H} ≝ t 'in' s)"
24 with precedence 10
25for @{ Prod_inv_rect_Type0 ??? $t (λ${ident x}.λ${ident y}.λ${ident H}.$s) }.
26
27notation < "hvbox('let' 〈ident x,ident y〉 {ident H} ≝ t 'in' s)"
28 with precedence 10
29for @{ Prod_inv_rect_Type0 $z $w $r $t (λ${ident x}:$X.λ${ident y}:$Y.λ${ident H}:$h.$s) }.
30
31lemma breakup_pair' : ∀A,B,C:Type[0].∀x. ∀R:C → Prop. ∀P:∀a:A.∀b:B. x=〈a,b〉 → C.
32  R (P (\fst x) (\snd x) ?) → R (let 〈a,b〉 {H} ≝ x in P a b H).
33[2: // ]
34#A #B #C *; normalize /2/
35qed.
36
[475]37(* timings taken from SIEMENS *)
38
[1604]39definition fetch0: ∀code_memory: BitVectorTrie Byte 16.
40    ∀program_counter: Word. Byte → instruction × Word × nat ≝
[1591]41  λpmem.
42  λpc.
43  λv.
[475]44   let 〈b,v〉 ≝ head … v in if b then
45    let 〈b,v〉 ≝ head … v in if b then
46     let 〈b,v〉 ≝ head … v in if b then
47      let 〈b,v〉 ≝ head … v in if b then
48       let 〈b,v〉 ≝ head … v in if b then
[820]49        〈〈RealInstruction (MOV … (inl … (inl … (inl … (inl … (inr … 〈REGISTER v,ACC_A〉)))))), pc〉, 1〉
[475]50       else
51        let 〈b,v〉≝  head … v in if b then
52         let 〈b,v〉≝  head … v in if b then
[820]53          〈〈RealInstruction (MOV … (inl … (inl … (inl … (inl … (inr … 〈INDIRECT (from_singl … v),ACC_A〉)))))), pc〉, 1〉
[475]54         else
55          let 〈b,v〉≝  head … v in if b then
[1604]56           let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈RealInstruction (MOV … (inl … (inl … (inl … (inr … 〈DIRECT b1,ACC_A〉))))), pc〉, 1〉
[475]57          else
[856]58           〈〈RealInstruction (CPL … ACC_A), pc〉, 1〉
[475]59        else
60         let 〈b,v〉≝  head … v in if b then
[820]61          〈〈RealInstruction (MOVX … (inr … 〈EXT_INDIRECT (from_singl … v),ACC_A〉)), pc〉, 2〉
[475]62         else
63          let 〈b,v〉≝  head … v in if b then
[1604]64           let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈ACALL … (ADDR11 (([[true;true;true]]) @@ b1)), pc〉, 2〉
[475]65          else
[820]66           〈〈RealInstruction (MOVX … (inr … 〈EXT_INDIRECT_DPTR,ACC_A〉)), pc〉, 2〉
[475]67      else
68       let 〈b,v〉≝  head … v in if b then
[820]69        〈〈RealInstruction (MOV … (inl … (inl … (inl … (inl … (inl … 〈ACC_A,REGISTER v〉)))))), pc〉, 1〉
[475]70       else
71        let 〈b,v〉≝  head … v in if b then
72         let 〈b,v〉≝  head … v in if b then
[820]73          〈〈RealInstruction (MOV … (inl … (inl … (inl … (inl … (inl … 〈ACC_A,INDIRECT (from_singl … v)〉)))))), pc〉, 1〉
[475]74         else
75          let 〈b,v〉≝  head … v in if b then
[1604]76           let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈RealInstruction (MOV … (inl … (inl … (inl … (inl … (inl … 〈ACC_A,DIRECT b1〉)))))), pc〉, 1〉
[475]77          else
[820]78           〈〈RealInstruction (CLR … ACC_A), pc〉, 1〉
[475]79        else
80         let 〈b,v〉≝  head … v in if b then
[820]81          〈〈RealInstruction (MOVX … (inl … 〈ACC_A,EXT_INDIRECT (from_singl … v)〉)), pc〉, 2〉
[475]82         else
83          let 〈b,v〉≝  head … v in if b then
[1604]84           let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈AJMP … (ADDR11 (([[true;true;true]]) @@ b1)), pc〉, 2〉
[475]85          else
[820]86           〈〈RealInstruction (MOVX … (inl … 〈ACC_A,EXT_INDIRECT_DPTR〉)), pc〉, 2〉
[475]87     else
88      let 〈b,v〉≝  head … v in if b then
89       let 〈b,v〉≝  head … v in if b then
[1604]90        let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈RealInstruction (DJNZ … (REGISTER v) (RELATIVE b1)), pc〉, 2〉
[475]91       else
92        let 〈b,v〉≝  head … v in if b then
93         let 〈b,v〉≝  head … v in if b then
[820]94          〈〈RealInstruction (XCHD … ACC_A (INDIRECT (from_singl … v))), pc〉, 1〉
[475]95         else
96          let 〈b,v〉≝  head … v in if b then
[1604]97           let 〈pc,b1〉 {EQ} ≝ next pmem pc in let 〈pc,b2〉 {EQ'} ≝ next pmem pc in 〈〈RealInstruction (DJNZ … (DIRECT b1) (RELATIVE b2)), pc〉, 2〉
[475]98          else
[820]99           〈〈RealInstruction (DA … ACC_A), pc〉, 1〉
[475]100        else
101         let 〈b,v〉≝  head … v in if b then
102          let 〈b,v〉≝  head … v in if b then
[820]103           〈〈RealInstruction (SETB … CARRY), pc〉, 1〉
[475]104          else
[1604]105           let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈RealInstruction (SETB … (BIT_ADDR b1)), pc〉, 1〉
[475]106         else
107          let 〈b,v〉≝  head … v in if b then
[1604]108           let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈ACALL … (ADDR11 (([[true;true;false]]) @@ b1)), pc〉, 2〉
[475]109          else
[1604]110           let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈RealInstruction (POP … (DIRECT b1)), pc〉, 2〉
[475]111      else
112       let 〈b,v〉≝  head … v in if b then
[820]113        〈〈RealInstruction (XCH … ACC_A (REGISTER v)), pc〉, 1〉
[475]114       else
115        let 〈b,v〉≝  head … v in if b then
116         let 〈b,v〉≝  head … v in if b then
[820]117          〈〈RealInstruction (XCH … ACC_A (INDIRECT (from_singl … v))), pc〉, 1〉
[475]118         else
119          let 〈b,v〉≝  head … v in if b then
[1604]120           let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈RealInstruction (XCH … ACC_A (DIRECT b1)), pc〉, 1〉
[475]121          else
[820]122           〈〈RealInstruction (SWAP … ACC_A), pc〉, 1〉
[475]123        else
124         let 〈b,v〉≝  head … v in if b then
125          let 〈b,v〉≝  head … v in if b then
[820]126           〈〈RealInstruction (CLR … CARRY), pc〉, 1〉
[475]127          else
[1604]128           let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈RealInstruction (CLR … (BIT_ADDR b1)), pc〉, 1〉
[475]129         else
130          let 〈b,v〉≝  head … v in if b then
[1604]131           let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈AJMP … (ADDR11 (([[true;true;false]]) @@ b1)), pc〉, 2〉
[475]132          else
[1604]133           let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈RealInstruction (PUSH … (DIRECT b1)), pc〉, 2〉
[475]134    else
135     let 〈b,v〉≝  head … v in if b then
136      let 〈b,v〉≝  head … v in if b then
137       let 〈b,v〉≝  head … v in if b then
[1604]138        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〉
[475]139       else
140        let 〈b,v〉≝  head … v in if b then
141         let 〈b,v〉≝  head … v in if b then
[1604]142          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〉
[475]143         else
144          let 〈b,v〉≝  head … v in if b then
[1604]145           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〉
[475]146          else
[1604]147           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〉
[475]148        else
149         let 〈b,v〉≝  head … v in if b then
150          let 〈b,v〉≝  head … v in if b then
[820]151           〈〈RealInstruction (CPL … CARRY), pc〉, 1〉
[475]152          else
[1604]153           let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈RealInstruction (CPL … (BIT_ADDR b1)), pc〉, 1〉
[475]154         else
155          let 〈b,v〉≝  head … v in if b then
[1604]156           let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈ACALL … (ADDR11 (([[true;false;true]]) @@ b1)), pc〉, 2〉
[475]157          else
[1604]158           let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈RealInstruction (ANL … (inr … 〈CARRY,N_BIT_ADDR b1〉)), pc〉, 2〉
[475]159      else
160       let 〈b,v〉≝  head … v in if b then
[1604]161        let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈RealInstruction (MOV … (inl … (inl … (inl … (inl … (inr … 〈REGISTER v,DIRECT b1〉)))))), pc〉, 2〉
[475]162       else
163        let 〈b,v〉≝  head … v in if b then
164         let 〈b,v〉≝  head … v in if b then
[1604]165          let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈RealInstruction (MOV … (inl … (inl … (inl … (inl … (inr … 〈INDIRECT (from_singl … v),DIRECT b1〉)))))), pc〉, 2〉
[475]166         else
[820]167          〈〈RealInstruction (MUL … ACC_A ACC_B), pc〉, 4〉
[475]168        else
169         let 〈b,v〉≝  head … v in if b then
170          let 〈b,v〉≝  head … v in if b then
[820]171           〈〈RealInstruction (INC … DPTR), pc〉, 2〉
[475]172          else
[1604]173           let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈RealInstruction (MOV … (inl … (inr … 〈CARRY,BIT_ADDR b1〉))), pc〉, 1〉
[475]174         else
175          let 〈b,v〉≝  head … v in if b then
[1604]176           let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈AJMP … (ADDR11 (([[true;false;true]]) @@ b1)), pc〉, 2〉
[475]177          else
[1604]178           let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈RealInstruction (ORL … (inr … 〈CARRY,N_BIT_ADDR b1〉)), pc〉, 2〉
[475]179     else
180      let 〈b,v〉≝  head … v in if b then
181       let 〈b,v〉≝  head … v in if b then
[820]182        〈〈RealInstruction (SUBB … ACC_A (REGISTER v)), pc〉, 1〉
[475]183       else
184        let 〈b,v〉≝  head … v in if b then
185         let 〈b,v〉≝  head … v in if b then
[820]186          〈〈RealInstruction (SUBB … ACC_A (INDIRECT (from_singl … v))), pc〉, 1〉
[475]187         else
188          let 〈b,v〉≝  head … v in if b then
[1604]189           let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈RealInstruction (SUBB … ACC_A (DIRECT b1)), pc〉, 1〉
[475]190          else
[1604]191           let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈RealInstruction (SUBB … ACC_A (DATA b1)), pc〉, 1〉
[475]192        else
193         let 〈b,v〉≝  head … v in if b then
194          let 〈b,v〉≝  head … v in if b then
195           〈〈MOVC … ACC_A (ACC_DPTR), pc〉, 2〉
196          else
[1604]197           let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈RealInstruction (MOV … (inr … 〈BIT_ADDR b1,CARRY〉)), pc〉, 2〉
[475]198         else
199          let 〈b,v〉≝  head … v in if b then
[1604]200           let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈ACALL … (ADDR11 (([[true;false;false]]) @@ b1)), pc〉, 2〉
[475]201          else
[1604]202           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〉
[475]203      else
204       let 〈b,v〉≝  head … v in if b then
[1604]205        let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈RealInstruction (MOV … (inl … (inl … (inl … (inr … 〈DIRECT b1,REGISTER v〉))))), pc〉, 2〉
[475]206       else
207        let 〈b,v〉≝  head … v in if b then
208         let 〈b,v〉≝  head … v in if b then
[1604]209          let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈RealInstruction (MOV … (inl … (inl … (inl … (inr … 〈DIRECT b1,INDIRECT (from_singl … v)〉))))), pc〉, 2〉
[475]210         else
211          let 〈b,v〉≝  head … v in if b then
[1604]212           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〉
[475]213          else
[820]214           〈〈RealInstruction (DIV … ACC_A ACC_B), pc〉, 4〉
[475]215        else
216         let 〈b,v〉≝  head … v in if b then
217          let 〈b,v〉≝  head … v in if b then
218           〈〈MOVC … ACC_A (ACC_PC), pc〉, 2〉
219          else
[1604]220           let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈RealInstruction (ANL … (inr … 〈CARRY,BIT_ADDR b1〉)), pc〉, 2〉
[475]221         else
222          let 〈b,v〉≝  head … v in if b then
[1604]223           let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈AJMP … (ADDR11 (([[true;false;false]]) @@ b1)), pc〉, 2〉
[475]224          else
[1604]225           let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈SJMP … (RELATIVE b1), pc〉, 2〉
[475]226   else
227    let 〈b,v〉≝  head … v in if b then
228     let 〈b,v〉≝  head … v in if b then
229      let 〈b,v〉≝  head … v in if b then
230       let 〈b,v〉≝  head … v in if b then
[1604]231        let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈RealInstruction (MOV … (inl … (inl … (inl … (inl … (inr … 〈REGISTER v,DATA b1〉)))))), pc〉, 1〉
[475]232       else
233        let 〈b,v〉≝  head … v in if b then
234         let 〈b,v〉≝  head … v in if b then
[1604]235          let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈RealInstruction (MOV … (inl … (inl … (inl … (inl … (inr … 〈INDIRECT (from_singl … v),DATA b1〉)))))), pc〉, 1〉
[475]236         else
237          let 〈b,v〉≝  head … v in if b then
[1604]238           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〉
[475]239          else
[1604]240           let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈RealInstruction (MOV … (inl … (inl … (inl … (inl … (inl … 〈ACC_A,DATA b1〉)))))), pc〉, 1〉
[475]241        else
242         let 〈b,v〉≝  head … v in if b then
243          let 〈b,v〉≝  head … v in if b then
244           〈〈JMP … INDIRECT_DPTR, pc〉, 2〉
245          else
[1604]246           let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈RealInstruction (ORL … (inr … 〈CARRY,BIT_ADDR b1〉)), pc〉, 2〉
[475]247         else
248          let 〈b,v〉≝  head … v in if b then
[1604]249           let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈ACALL … (ADDR11 (([[false;true;true]]) @@ b1)), pc〉, 2〉
[475]250          else
[1604]251           let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈RealInstruction (JNZ … (RELATIVE b1)), pc〉, 2〉
[475]252      else
253       let 〈b,v〉≝  head … v in if b then
[820]254        〈〈RealInstruction (XRL … (inl … 〈ACC_A,REGISTER v〉)), pc〉, 1〉
[475]255       else
256        let 〈b,v〉≝  head … v in if b then
257         let 〈b,v〉≝  head … v in if b then
[820]258          〈〈RealInstruction (XRL … (inl … 〈ACC_A,INDIRECT (from_singl … v)〉)), pc〉, 1〉
[475]259         else
260          let 〈b,v〉≝  head … v in if b then
[1604]261           let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈RealInstruction (XRL … (inl … 〈ACC_A,DIRECT b1〉)), pc〉, 1〉
[475]262          else
[1604]263           let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈RealInstruction (XRL … (inl … 〈ACC_A,DATA b1〉)), pc〉, 1〉
[475]264        else
265         let 〈b,v〉≝  head … v in if b then
266          let 〈b,v〉≝  head … v in if b then
[1604]267           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〉
[475]268          else
[1604]269           let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈RealInstruction (XRL … (inr … 〈DIRECT b1,ACC_A〉)), pc〉, 1〉
[475]270         else
271          let 〈b,v〉≝  head … v in if b then
[1604]272           let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈AJMP … (ADDR11 (([[false;true;true]]) @@ b1)), pc〉, 2〉
[475]273          else
[1604]274           let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈RealInstruction (JZ … (RELATIVE b1)), pc〉, 2〉
[475]275     else
276      let 〈b,v〉≝  head … v in if b then
277       let 〈b,v〉≝  head … v in if b then
[820]278        〈〈RealInstruction (ANL … (inl … (inl … 〈ACC_A,REGISTER v〉))), pc〉, 1〉
[475]279       else
280        let 〈b,v〉≝  head … v in if b then
281         let 〈b,v〉≝  head … v in if b then
[820]282          〈〈RealInstruction (ANL … (inl … (inl … 〈ACC_A,INDIRECT (from_singl … v)〉))), pc〉, 1〉
[475]283         else
284          let 〈b,v〉≝  head … v in if b then
[1604]285           let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈RealInstruction (ANL … (inl … (inl … 〈ACC_A,DIRECT b1〉))), pc〉, 1〉
[475]286          else
[1604]287           let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈RealInstruction (ANL … (inl … (inl … 〈ACC_A,DATA b1〉))), pc〉, 1〉
[475]288        else
289         let 〈b,v〉≝  head … v in if b then
290          let 〈b,v〉≝  head … v in if b then
[1604]291           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〉
[475]292          else
[1604]293           let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈RealInstruction (ANL … (inl … (inr … 〈DIRECT b1,ACC_A〉))), pc〉, 1〉
[475]294         else
295          let 〈b,v〉≝  head … v in if b then
[1604]296           let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈ACALL … (ADDR11 (([[false;true;false]]) @@ b1)), pc〉, 2〉
[475]297          else
[1604]298           let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈RealInstruction (JNC … (RELATIVE b1)), pc〉, 2〉
[475]299      else
300       let 〈b,v〉≝  head … v in if b then
[820]301        〈〈RealInstruction (ORL … (inl … (inl … 〈ACC_A,REGISTER v〉))), pc〉, 1〉
[475]302       else
303        let 〈b,v〉≝  head … v in if b then
304         let 〈b,v〉≝  head … v in if b then
[820]305          〈〈RealInstruction (ORL … (inl … (inl … 〈ACC_A,INDIRECT (from_singl … v)〉))), pc〉, 1〉
[475]306         else
307          let 〈b,v〉≝  head … v in if b then
[1604]308           let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈RealInstruction (ORL … (inl … (inl … 〈ACC_A,DIRECT b1〉))), pc〉, 1〉
[475]309          else
[1604]310           let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈RealInstruction (ORL … (inl … (inl … 〈ACC_A,DATA b1〉))), pc〉, 1〉
[475]311        else
312         let 〈b,v〉≝  head … v in if b then
313          let 〈b,v〉≝  head … v in if b then
[1604]314           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〉
[475]315          else
[1604]316           let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈RealInstruction (ORL … (inl … (inr … 〈DIRECT b1,ACC_A〉))), pc〉, 1〉
[475]317         else
318          let 〈b,v〉≝  head … v in if b then
[1604]319           let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈AJMP … (ADDR11 (([[false;true;false]]) @@ b1)), pc〉, 2〉
[475]320          else
[1604]321           let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈RealInstruction (JC … (RELATIVE b1)), pc〉, 2〉
[475]322    else
323     let 〈b,v〉≝  head … v in if b then
324      let 〈b,v〉≝  head … v in if b then
325       let 〈b,v〉≝  head … v in if b then
[820]326        〈〈RealInstruction (ADDC … ACC_A (REGISTER v)), pc〉, 1〉
[475]327       else
328        let 〈b,v〉≝  head … v in if b then
329         let 〈b,v〉≝  head … v in if b then
[820]330          〈〈RealInstruction (ADDC … ACC_A (INDIRECT (from_singl … v))), pc〉, 1〉
[475]331         else
332          let 〈b,v〉≝  head … v in if b then
[1604]333           let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈RealInstruction (ADDC … ACC_A (DIRECT b1)), pc〉, 1〉
[475]334          else
[1604]335           let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈RealInstruction (ADDC … ACC_A (DATA b1)), pc〉, 1〉
[475]336        else
337         let 〈b,v〉≝  head … v in if b then
338          let 〈b,v〉≝  head … v in if b then
[820]339           〈〈RealInstruction (RLC … ACC_A), pc〉, 1〉
[475]340          else
[820]341           〈〈RealInstruction (RETI …), pc〉, 2〉
[475]342         else
343          let 〈b,v〉≝  head … v in if b then
[1604]344           let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈ACALL … (ADDR11 (([[false;false;true]]) @@ b1)), pc〉, 2〉
[475]345          else
[1604]346           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〉
[475]347      else
348       let 〈b,v〉≝  head … v in if b then
[820]349        〈〈RealInstruction (ADD … ACC_A (REGISTER v)), pc〉, 1〉
[475]350       else
351        let 〈b,v〉≝  head … v in if b then
352         let 〈b,v〉≝  head … v in if b then
[820]353          〈〈RealInstruction (ADD … ACC_A (INDIRECT (from_singl … v))), pc〉, 1〉
[475]354         else
355          let 〈b,v〉≝  head … v in if b then
[1604]356           let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈RealInstruction (ADD … ACC_A (DIRECT b1)), pc〉, 1〉
[475]357          else
[1604]358           let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈RealInstruction (ADD … ACC_A (DATA b1)), pc〉, 1〉
[475]359        else
360         let 〈b,v〉≝  head … v in if b then
361          let 〈b,v〉≝  head … v in if b then
[820]362           〈〈RealInstruction (RL … ACC_A), pc〉, 1〉
[475]363          else
[820]364           〈〈RealInstruction (RET …), pc〉, 2〉
[475]365         else
366          let 〈b,v〉≝  head … v in if b then
[1604]367           let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈AJMP … (ADDR11 (([[false;false;true]]) @@ b1)), pc〉, 2〉
[475]368          else
[1604]369           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〉
[475]370     else
371      let 〈b,v〉≝  head … v in if b then
372       let 〈b,v〉≝  head … v in if b then
[820]373        〈〈RealInstruction (DEC … (REGISTER v)), pc〉, 1〉
[475]374       else
375        let 〈b,v〉≝  head … v in if b then
376         let 〈b,v〉≝  head … v in if b then
[820]377          〈〈RealInstruction (DEC … (INDIRECT (from_singl … v))), pc〉, 1〉
[475]378         else
379          let 〈b,v〉≝  head … v in if b then
[1604]380           let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈RealInstruction (DEC … (DIRECT b1)), pc〉, 1〉
[475]381          else
[820]382           〈〈RealInstruction (DEC … ACC_A), pc〉, 1〉
[475]383        else
384         let 〈b,v〉≝  head … v in if b then
385          let 〈b,v〉≝  head … v in if b then
[820]386           〈〈RealInstruction (RRC … ACC_A), pc〉, 1〉
[475]387          else
[1604]388           let 〈pc,b1〉 {EQ} ≝ next pmem pc in let 〈pc,b2〉 {EQ'} ≝ next pmem pc in 〈〈LCALL … (ADDR16 (b1 @@ b2)), pc〉, 2〉
[475]389         else
390          let 〈b,v〉≝  head … v in if b then
[1604]391           let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈ACALL … (ADDR11 (([[false;false;false]]) @@ b1)), pc〉, 2〉
[475]392          else
[1604]393           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〉
[475]394      else
395       let 〈b,v〉≝  head … v in if b then
[820]396        〈〈RealInstruction (INC … (REGISTER v)), pc〉, 1〉
[475]397       else
398        let 〈b,v〉≝  head … v in if b then
399         let 〈b,v〉≝  head … v in if b then
[820]400          〈〈RealInstruction (INC … (INDIRECT (from_singl … v))), pc〉, 1〉
[475]401         else
402          let 〈b,v〉≝  head … v in if b then
[1604]403           let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈RealInstruction (INC … (DIRECT b1)), pc〉, 1〉
[475]404          else
[820]405           〈〈RealInstruction (INC … ACC_A), pc〉, 1〉
[475]406        else
407         let 〈b,v〉≝  head … v in if b then
408          let 〈b,v〉≝  head … v in if b then
[820]409           〈〈RealInstruction (RR … ACC_A), pc〉, 1〉
[475]410          else
[1604]411           let 〈pc,b1〉 {EQ} ≝ next pmem pc in let 〈pc,b2〉 {EQ'} ≝ next pmem pc in 〈〈LJMP … (ADDR16 (b1 @@ b2)), pc〉, 2〉
[475]412         else
413          let 〈b,v〉≝  head … v in if b then
[1604]414           let 〈pc,b1〉 {EQ} ≝ next pmem pc in 〈〈AJMP … (ADDR11 (([[false;false;false]]) @@ b1)), pc〉, 2〉
[475]415          else
[820]416           〈〈RealInstruction (NOP …), pc〉, 1〉.
[1604]417  %
[475]418qed.
[876]419
[1604]420definition fetch: ∀code_memory: BitVectorTrie Byte 16.
421    ∀program_counter: Word. instruction × Word × nat ≝
[1591]422  λpmem: BitVectorTrie Byte 16.
423  λpc: Word.
[1604]424  let 〈word, byte〉 ≝ next pmem pc in
[1642]425    fetch0 pmem word byte.
Note: See TracBrowser for help on using the repository browser.