1 | include "ASM/ASM.ma". |
---|
2 | include "ASM/Fetch.ma". |
---|
3 | include "ASM/Arithmetic.ma". |
---|
4 | |
---|
5 | let rec member_p |
---|
6 | (a: Type[0]) (eq: a → a → bool) (element: a) (the_list: list a) |
---|
7 | on the_list: Prop ≝ |
---|
8 | match the_list with |
---|
9 | [ nil ⇒ False |
---|
10 | | cons hd tl ⇒ |
---|
11 | match eq hd element with |
---|
12 | [ true ⇒ True |
---|
13 | | false ⇒ member_p … eq element tl |
---|
14 | ] |
---|
15 | ]. |
---|
16 | |
---|
17 | definition well_labelled_p ≝ |
---|
18 | ∀pc: Word. |
---|
19 | ∀acc_a: Byte. |
---|
20 | ∀function_locations: list Word. |
---|
21 | ∀program: BitVectorTrie Byte 16. |
---|
22 | ∀cost_labels. |
---|
23 | let 〈instruction, newpc, cost〉 ≝ fetch program pc in |
---|
24 | match instruction with |
---|
25 | [ LCALL lcall ⇒ |
---|
26 | match lcall return λx. bool_to_Prop (is_in … [[ addr16 ]] x) → ? with |
---|
27 | [ ADDR16 addr16 ⇒ λ_. member_p … (eq_bv …) addr16 function_locations |
---|
28 | | _ ⇒ λabsurd. ⊥ |
---|
29 | ] (subaddressing_modein … lcall) |
---|
30 | | ACALL acall ⇒ |
---|
31 | match acall return λx. bool_to_Prop (is_in … [[ addr11 ]] x) → ? with |
---|
32 | [ ADDR11 addr11 ⇒ λ_. |
---|
33 | let 〈pc_bu, pc_bl〉 ≝ vsplit … 8 8 pc in |
---|
34 | let 〈thr, eig〉 ≝ vsplit … 3 8 addr11 in |
---|
35 | let 〈fiv, thr'〉 ≝ vsplit … 5 3 pc_bu in |
---|
36 | let new_pc ≝ (fiv @@ thr) @@ pc_bl in |
---|
37 | match lookup_opt … new_pc cost_labels with |
---|
38 | [ None ⇒ False |
---|
39 | | _ ⇒ True |
---|
40 | ] |
---|
41 | | _ ⇒ λabsurd. ⊥ |
---|
42 | ] (subaddressing_modein … acall) |
---|
43 | | AJMP ajmp ⇒ |
---|
44 | match ajmp return λx. bool_to_Prop (is_in … [[ addr11 ]] x) → ? with |
---|
45 | [ ADDR11 addr11 ⇒ λ_. |
---|
46 | let 〈pc_bu, pc_bl〉 ≝ vsplit … 8 8 pc in |
---|
47 | let 〈nu, nl〉 ≝ vsplit … 4 4 pc_bu in |
---|
48 | let bit ≝ get_index' … O ? nl in |
---|
49 | let 〈relevant1, relevant2〉 ≝ vsplit … 3 8 addr11 in |
---|
50 | let new_addr ≝ (nu @@ (bit ::: relevant1)) @@ relevant2 in |
---|
51 | let 〈carry, new_pc〉 ≝ half_add … pc new_addr in |
---|
52 | match lookup_opt … new_pc cost_labels with |
---|
53 | [ None ⇒ False |
---|
54 | | _ ⇒ True |
---|
55 | ] |
---|
56 | | _ ⇒ λabsurd. ⊥ |
---|
57 | ] (subaddressing_modein … ajmp) |
---|
58 | | LJMP ljmp ⇒ |
---|
59 | match ljmp return λx. bool_to_Prop (is_in … [[ addr16 ]] x) → ? with |
---|
60 | [ ADDR16 addr16 ⇒ λ_. |
---|
61 | match lookup_opt … addr16 cost_labels with |
---|
62 | [ None ⇒ False |
---|
63 | | _ ⇒ True |
---|
64 | ] |
---|
65 | | _ ⇒ λabsurd. ⊥ |
---|
66 | ] (subaddressing_modein … ljmp) |
---|
67 | | SJMP sjmp ⇒ |
---|
68 | match sjmp return λx. bool_to_Prop (is_in … [[ relative ]] x) → ? with |
---|
69 | [ RELATIVE rel ⇒ λ_. |
---|
70 | let 〈carry, new_pc〉 ≝ half_add … pc (sign_extend 8 8 rel) in |
---|
71 | match lookup_opt … new_pc cost_labels with |
---|
72 | [ None ⇒ False |
---|
73 | | _ ⇒ True |
---|
74 | ] |
---|
75 | | _ ⇒ λabsurd. ⊥ |
---|
76 | ] (subaddressing_modein … sjmp) |
---|
77 | | JMP jmp ⇒ True (* XXX: check is dynamic, as we can only jump to functions *) |
---|
78 | | MOVC _ _ ⇒ True |
---|
79 | | RealInstruction instruction ⇒ |
---|
80 | match instruction with |
---|
81 | [ JZ jz ⇒ |
---|
82 | match jz return λx. bool_to_Prop (is_in … [[ relative ]] x) → ? with |
---|
83 | [ RELATIVE rel ⇒ λ_. |
---|
84 | let 〈carry, new_pc〉 ≝ half_add … pc (sign_extend 8 8 rel) in |
---|
85 | match lookup_opt … new_pc cost_labels with |
---|
86 | [ None ⇒ False |
---|
87 | | _ ⇒ True |
---|
88 | ] |
---|
89 | | _ ⇒ λabsurd. ⊥ |
---|
90 | ] (subaddressing_modein … jz) |
---|
91 | | JNZ jnz ⇒ |
---|
92 | match jnz return λx. bool_to_Prop (is_in … [[ relative ]] x) → ? with |
---|
93 | [ RELATIVE rel ⇒ λ_. |
---|
94 | let 〈carry, new_pc〉 ≝ half_add … pc (sign_extend 8 8 rel) in |
---|
95 | match lookup_opt … new_pc cost_labels with |
---|
96 | [ None ⇒ False |
---|
97 | | _ ⇒ True |
---|
98 | ] |
---|
99 | | _ ⇒ λabsurd. ⊥ |
---|
100 | ] (subaddressing_modein … jnz) |
---|
101 | | JC jc ⇒ |
---|
102 | match jc return λx. bool_to_Prop (is_in … [[ relative ]] x) → ? with |
---|
103 | [ RELATIVE rel ⇒ λ_. |
---|
104 | let 〈carry, new_pc〉 ≝ half_add … pc (sign_extend 8 8 rel) in |
---|
105 | match lookup_opt … new_pc cost_labels with |
---|
106 | [ None ⇒ False |
---|
107 | | _ ⇒ True |
---|
108 | ] |
---|
109 | | _ ⇒ λabsurd. ⊥ |
---|
110 | ] (subaddressing_modein … jc) |
---|
111 | | JNC jnc ⇒ |
---|
112 | match jnc return λx. bool_to_Prop (is_in … [[ relative ]] x) → ? with |
---|
113 | [ RELATIVE rel ⇒ λ_. |
---|
114 | let 〈carry, new_pc〉 ≝ half_add … pc (sign_extend 8 8 rel) in |
---|
115 | match lookup_opt … new_pc cost_labels with |
---|
116 | [ None ⇒ False |
---|
117 | | _ ⇒ True |
---|
118 | ] |
---|
119 | | _ ⇒ λabsurd. ⊥ |
---|
120 | ] (subaddressing_modein … jnc) |
---|
121 | | JB baddr jb ⇒ |
---|
122 | match jb return λx. bool_to_Prop (is_in … [[ relative ]] x) → ? with |
---|
123 | [ RELATIVE rel ⇒ λ_. |
---|
124 | let 〈carry, new_pc〉 ≝ half_add … pc (sign_extend 8 8 rel) in |
---|
125 | match lookup_opt … new_pc cost_labels with |
---|
126 | [ None ⇒ False |
---|
127 | | _ ⇒ True |
---|
128 | ] |
---|
129 | | _ ⇒ λabsurd. ⊥ |
---|
130 | ] (subaddressing_modein … jb) |
---|
131 | | JNB baddr jnb ⇒ |
---|
132 | match jnb return λx. bool_to_Prop (is_in … [[ relative ]] x) → ? with |
---|
133 | [ RELATIVE rel ⇒ λ_. |
---|
134 | let 〈carry, new_pc〉 ≝ half_add … pc (sign_extend 8 8 rel) in |
---|
135 | match lookup_opt … new_pc cost_labels with |
---|
136 | [ None ⇒ False |
---|
137 | | _ ⇒ True |
---|
138 | ] |
---|
139 | | _ ⇒ λabsurd. ⊥ |
---|
140 | ] (subaddressing_modein … jnb) |
---|
141 | | JBC baddr jbc ⇒ |
---|
142 | match jbc return λx. bool_to_Prop (is_in … [[ relative ]] x) → ? with |
---|
143 | [ RELATIVE rel ⇒ λ_. |
---|
144 | let 〈carry, new_pc〉 ≝ half_add … pc (sign_extend 8 8 rel) in |
---|
145 | match lookup_opt … new_pc cost_labels with |
---|
146 | [ None ⇒ False |
---|
147 | | _ ⇒ True |
---|
148 | ] |
---|
149 | | _ ⇒ λabsurd. ⊥ |
---|
150 | ] (subaddressing_modein … jbc) |
---|
151 | | CJNE args cjne ⇒ |
---|
152 | match cjne return λx. bool_to_Prop (is_in … [[ relative ]] x) → ? with |
---|
153 | [ RELATIVE rel ⇒ λ_. |
---|
154 | let 〈carry, new_pc〉 ≝ half_add … pc (sign_extend 8 8 rel) in |
---|
155 | match lookup_opt … new_pc cost_labels with |
---|
156 | [ None ⇒ False |
---|
157 | | _ ⇒ True |
---|
158 | ] |
---|
159 | | _ ⇒ λabsurd. ⊥ |
---|
160 | ] (subaddressing_modein … cjne) |
---|
161 | | DJNZ args djnz ⇒ |
---|
162 | match djnz return λx. bool_to_Prop (is_in … [[ relative ]] x) → ? with |
---|
163 | [ RELATIVE rel ⇒ λ_. |
---|
164 | let 〈carry, new_pc〉 ≝ half_add … pc (sign_extend 8 8 rel) in |
---|
165 | match lookup_opt … new_pc cost_labels with |
---|
166 | [ None ⇒ False |
---|
167 | | _ ⇒ True |
---|
168 | ] |
---|
169 | | _ ⇒ λabsurd. ⊥ |
---|
170 | ] (subaddressing_modein … djnz) |
---|
171 | | _ ⇒ True |
---|
172 | ] |
---|
173 | ]. |
---|
174 | [*: normalize in absurd; // ] |
---|
175 | qed. |
---|