[2160] | 1 | include "ASM/Assembly.ma". |
---|
| 2 | include "ASM/Interpret.ma". |
---|
| 3 | include "ASM/StatusProofs.ma". |
---|
| 4 | include alias "arithmetics/nat.ma". |
---|
| 5 | include "ASM/AssemblyProof.ma". |
---|
| 6 | |
---|
| 7 | lemma set_program_counter_status_of_pseudo_status: |
---|
| 8 | ∀M. |
---|
| 9 | ∀cm. |
---|
| 10 | ∀sigma. |
---|
| 11 | ∀policy. |
---|
[2173] | 12 | ∀s, s'. |
---|
[2160] | 13 | ∀new_ppc. |
---|
[2173] | 14 | status_of_pseudo_status M cm s sigma policy = s' → |
---|
[2160] | 15 | set_program_counter (BitVectorTrie Byte 16) |
---|
| 16 | (code_memory_of_pseudo_assembly_program cm sigma policy) |
---|
[2173] | 17 | s' |
---|
[2160] | 18 | (sigma new_ppc) = |
---|
[2173] | 19 | status_of_pseudo_status M cm (set_program_counter … cm s new_ppc) sigma policy. |
---|
| 20 | #M #cm #sigma #policy #s #s' #new_ppc #s_refl <s_refl // |
---|
[2160] | 21 | qed. |
---|
| 22 | |
---|
| 23 | lemma set_p1_latch_status_of_pseudo_status: |
---|
| 24 | ∀M. |
---|
| 25 | ∀code_memory. |
---|
| 26 | ∀sigma. |
---|
| 27 | ∀policy. |
---|
[2173] | 28 | ∀s,s'. |
---|
[2160] | 29 | ∀v. |
---|
[2173] | 30 | status_of_pseudo_status M code_memory s sigma policy = s' → |
---|
[2160] | 31 | set_p1_latch (BitVectorTrie Byte 16) |
---|
| 32 | (code_memory_of_pseudo_assembly_program code_memory sigma policy) |
---|
[2173] | 33 | s' v = |
---|
[2160] | 34 | status_of_pseudo_status M code_memory |
---|
| 35 | (set_p1_latch pseudo_assembly_program code_memory s v) sigma policy. |
---|
[2173] | 36 | #M #cm #sigma #policy #s #s' #new_ppc #s_refl <s_refl // |
---|
[2160] | 37 | qed. |
---|
| 38 | |
---|
| 39 | lemma set_p3_latch_status_of_pseudo_status: |
---|
| 40 | ∀M. |
---|
| 41 | ∀code_memory. |
---|
| 42 | ∀sigma. |
---|
| 43 | ∀policy. |
---|
[2173] | 44 | ∀s, s'. |
---|
[2160] | 45 | ∀v. |
---|
[2173] | 46 | status_of_pseudo_status M code_memory s sigma policy = s' → |
---|
[2160] | 47 | set_p3_latch (BitVectorTrie Byte 16) |
---|
| 48 | (code_memory_of_pseudo_assembly_program code_memory sigma policy) |
---|
[2173] | 49 | s' v = |
---|
[2160] | 50 | status_of_pseudo_status M code_memory |
---|
| 51 | (set_p3_latch pseudo_assembly_program code_memory s v) sigma policy. |
---|
[2173] | 52 | #M #code_memory #sigma #policy #s #s' #v #s_refl <s_refl // |
---|
[2160] | 53 | qed. |
---|
| 54 | |
---|
| 55 | definition map_acc_a_using_internal_pseudo_address_map: |
---|
| 56 | ∀M: internal_pseudo_address_map. (Word → Word) → Byte → Byte ≝ |
---|
| 57 | λM, sigma, v. |
---|
| 58 | match \snd M with |
---|
| 59 | [ data ⇒ v |
---|
| 60 | | address upper_lower word ⇒ |
---|
| 61 | let mapped ≝ sigma word in |
---|
| 62 | let 〈high, low〉 ≝ vsplit bool 8 8 mapped in |
---|
| 63 | if eq_upper_lower upper_lower upper then |
---|
| 64 | high |
---|
| 65 | else |
---|
| 66 | low |
---|
| 67 | ]. |
---|
| 68 | |
---|
[2164] | 69 | (*CSC: Taken from AssemblyProofSplit.ma; there named map_lower_internal... *) |
---|
| 70 | definition map_internal_ram_address_using_pseudo_address_map: |
---|
| 71 | ∀M: internal_pseudo_address_map. (Word → Word) → Byte → Byte → Byte ≝ |
---|
| 72 | λM: internal_pseudo_address_map. |
---|
| 73 | λsigma: Word → Word. |
---|
| 74 | λaddress: Byte. |
---|
| 75 | λvalue: Byte. |
---|
| 76 | match assoc_list_lookup ?? address (eq_bv …) (\fst M) with |
---|
| 77 | [ None ⇒ value |
---|
| 78 | | Some upper_lower_word ⇒ |
---|
| 79 | let 〈upper_lower, word〉 ≝ upper_lower_word in |
---|
| 80 | let 〈high, low〉 ≝ vsplit bool 8 8 (sigma word) in |
---|
| 81 | if eq_upper_lower upper_lower upper then |
---|
| 82 | high |
---|
| 83 | else |
---|
| 84 | low |
---|
| 85 | ]. |
---|
| 86 | |
---|
[2160] | 87 | definition map_address_using_internal_pseudo_address_map: |
---|
| 88 | ∀M: internal_pseudo_address_map. (Word → Word) → SFR8051 → Byte → Byte ≝ |
---|
| 89 | λM, sigma, sfr, v. |
---|
| 90 | match sfr with |
---|
| 91 | [ SFR_ACC_A ⇒ map_acc_a_using_internal_pseudo_address_map M sigma v |
---|
| 92 | | _ ⇒ v |
---|
| 93 | ]. |
---|
| 94 | |
---|
| 95 | lemma set_index_set_index_overwrite: |
---|
| 96 | ∀A: Type[0]. |
---|
| 97 | ∀n: nat. |
---|
| 98 | ∀v: Vector A n. |
---|
| 99 | ∀index: nat. |
---|
| 100 | ∀e, e': A. |
---|
| 101 | ∀proof. |
---|
| 102 | ∀proof'. |
---|
| 103 | set_index A n v index e proof = |
---|
| 104 | set_index A n (set_index A n v index e' proof') index e proof. |
---|
| 105 | #A #n #v elim v normalize |
---|
| 106 | [1: |
---|
| 107 | #index #e #e' #absurd cases (lt_to_not_zero … absurd) |
---|
| 108 | |2: |
---|
| 109 | #n' #hd #tl #inductive_hypothesis #index #e #e' cases index #proof #proof' |
---|
| 110 | normalize // |
---|
| 111 | ] |
---|
| 112 | qed. |
---|
| 113 | |
---|
| 114 | lemma set_index_set_index_commutation: |
---|
| 115 | ∀A: Type[0]. |
---|
| 116 | ∀n: nat. |
---|
| 117 | ∀v: Vector A n. |
---|
| 118 | ∀m, o: nat. |
---|
| 119 | ∀m_lt_proof: m < n. |
---|
| 120 | ∀o_lt_proof: o < n. |
---|
| 121 | ∀e, f: A. |
---|
| 122 | m ≠ o → |
---|
| 123 | set_index A n (set_index A n v o f o_lt_proof) m e m_lt_proof = |
---|
| 124 | set_index A n (set_index A n v m e m_lt_proof) o f o_lt_proof. |
---|
| 125 | #A #n #v elim v |
---|
| 126 | [1: |
---|
| 127 | #m #o #m_lt_proof |
---|
| 128 | normalize in m_lt_proof; cases (lt_to_not_zero … m_lt_proof) |
---|
| 129 | |2: |
---|
| 130 | #n' #hd #tl #inductive_hypothesis |
---|
| 131 | #m #o |
---|
| 132 | cases m cases o |
---|
| 133 | [1: |
---|
| 134 | #m_lt_proof #o_lt_proof #e #f #absurd @⊥ cases absurd #relevant |
---|
| 135 | @relevant % |
---|
| 136 | |2,3: |
---|
| 137 | #o' normalize // |
---|
| 138 | |4: |
---|
| 139 | #m' #o' #m_lt_proof #o_lt_proof #e #f #o_neq_m_assm |
---|
| 140 | normalize @eq_f @inductive_hypothesis @nmk #relevant |
---|
| 141 | >relevant in o_neq_m_assm; #relevant @(absurd ?? relevant) % |
---|
| 142 | ] |
---|
| 143 | ] |
---|
| 144 | qed. |
---|
| 145 | |
---|
[2171] | 146 | (* XXX: move elsewhere *) |
---|
| 147 | lemma get_index_v_set_index_miss: |
---|
| 148 | ∀a: Type[0]. |
---|
| 149 | ∀n: nat. |
---|
| 150 | ∀v: Vector a n. |
---|
| 151 | ∀i, j: nat. |
---|
| 152 | ∀e: a. |
---|
| 153 | ∀i_proof: i < n. |
---|
| 154 | ∀j_proof: j < n. |
---|
| 155 | i ≠ j → |
---|
| 156 | get_index_v a n (set_index a n v i e i_proof) j j_proof = |
---|
| 157 | get_index_v a n v j j_proof. |
---|
| 158 | #a #n #v elim v |
---|
| 159 | [1: |
---|
| 160 | #i #j #e #i_proof |
---|
| 161 | cases (lt_to_not_zero … i_proof) |
---|
| 162 | |2: |
---|
| 163 | #n' #hd #tl #inductive_hypothesis #i #j |
---|
| 164 | cases i cases j |
---|
| 165 | [1: |
---|
| 166 | #e #i_proof #j_proof #neq_assm |
---|
| 167 | cases (absurd ? (refl … 0) neq_assm) |
---|
| 168 | |2,3: |
---|
| 169 | #i' #e #i_proof #j_proof #_ % |
---|
| 170 | |4: |
---|
| 171 | #i' #j' #e #i_proof #j_proof #neq_assm |
---|
| 172 | @inductive_hypothesis @nmk #eq_assm |
---|
| 173 | >eq_assm in neq_assm; #neq_assm |
---|
| 174 | cases (absurd ? (refl ??) neq_assm) |
---|
| 175 | ] |
---|
| 176 | ] |
---|
| 177 | qed. |
---|
| 178 | |
---|
[2160] | 179 | lemma set_index_status_of_pseudo_status: |
---|
| 180 | ∀M, code_memory, sigma, policy, s, sfr, v, v'. |
---|
| 181 | map_address_using_internal_pseudo_address_map M sigma sfr v = v' → |
---|
| 182 | (set_index Byte 19 |
---|
| 183 | (special_function_registers_8051 (BitVectorTrie Byte 16) |
---|
| 184 | (code_memory_of_pseudo_assembly_program code_memory sigma policy) |
---|
| 185 | (status_of_pseudo_status M code_memory s sigma policy)) |
---|
| 186 | (sfr_8051_index sfr) v' (sfr8051_index_19 sfr) |
---|
| 187 | =sfr_8051_of_pseudo_sfr_8051 M |
---|
| 188 | (special_function_registers_8051 pseudo_assembly_program code_memory |
---|
| 189 | (set_8051_sfr pseudo_assembly_program code_memory s sfr v)) sigma). |
---|
| 190 | #M #code_memory #sigma #policy #s #sfr #v #v' #sfr_neq_acc_a_assm |
---|
| 191 | whd in match status_of_pseudo_status; normalize nodelta |
---|
| 192 | whd in match sfr_8051_of_pseudo_sfr_8051; normalize nodelta |
---|
| 193 | inversion (\snd M) try (#upper_lower #address) #sndM_refl normalize nodelta |
---|
| 194 | [1: |
---|
| 195 | <sfr_neq_acc_a_assm cases sfr |
---|
| 196 | [18: |
---|
| 197 | whd in match map_address_using_internal_pseudo_address_map; normalize nodelta |
---|
| 198 | whd in match map_acc_a_using_internal_pseudo_address_map; normalize nodelta |
---|
| 199 | >sndM_refl % |
---|
| 200 | ] |
---|
| 201 | % |
---|
| 202 | |2: |
---|
| 203 | @pair_elim #high #low #high_low_refl normalize nodelta |
---|
| 204 | inversion (eq_upper_lower upper_lower upper) #eq_upper_lower_refl normalize nodelta |
---|
| 205 | <sfr_neq_acc_a_assm cases sfr |
---|
| 206 | [18,37: |
---|
| 207 | whd in match map_address_using_internal_pseudo_address_map; normalize nodelta |
---|
| 208 | whd in match map_acc_a_using_internal_pseudo_address_map; normalize nodelta |
---|
| 209 | >sndM_refl normalize nodelta >high_low_refl normalize nodelta |
---|
| 210 | >eq_upper_lower_refl normalize nodelta |
---|
| 211 | whd in match (set_8051_sfr ?????); |
---|
| 212 | [1: |
---|
| 213 | <set_index_set_index_overwrite in ⊢ (??%?); |
---|
| 214 | <set_index_set_index_overwrite in ⊢ (???%); % |
---|
| 215 | |2: |
---|
| 216 | <set_index_set_index_overwrite in ⊢ (??%?); |
---|
| 217 | <set_index_set_index_overwrite in ⊢ (???%); % |
---|
| 218 | ] |
---|
| 219 | ] |
---|
| 220 | whd in match map_address_using_internal_pseudo_address_map; normalize nodelta |
---|
| 221 | whd in match (set_8051_sfr ?????); @set_index_set_index_commutation normalize |
---|
| 222 | @nmk #absurd destruct(absurd) |
---|
| 223 | ] |
---|
| 224 | qed. |
---|
| 225 | |
---|
[2171] | 226 | lemma get_index_v_status_of_pseudo_status: |
---|
| 227 | ∀M, code_memory, sigma, policy, s, sfr. |
---|
| 228 | (get_index_v Byte 19 |
---|
| 229 | (special_function_registers_8051 (BitVectorTrie Byte 16) |
---|
| 230 | (code_memory_of_pseudo_assembly_program code_memory sigma policy) |
---|
| 231 | (status_of_pseudo_status M code_memory s sigma policy)) |
---|
| 232 | (sfr_8051_index sfr) (sfr8051_index_19 sfr) = |
---|
| 233 | map_address_using_internal_pseudo_address_map M sigma sfr |
---|
| 234 | (get_index_v Byte 19 |
---|
| 235 | (special_function_registers_8051 pseudo_assembly_program code_memory s) |
---|
| 236 | (sfr_8051_index sfr) (sfr8051_index_19 sfr))). |
---|
| 237 | #M #code_memory #sigma #policy #s #sfr |
---|
| 238 | whd in match status_of_pseudo_status; normalize nodelta |
---|
| 239 | whd in match sfr_8051_of_pseudo_sfr_8051; normalize nodelta |
---|
| 240 | inversion (\snd M) try (#upper_lower #address) #sndM_refl normalize nodelta |
---|
| 241 | [1: |
---|
| 242 | cases sfr |
---|
| 243 | [18: |
---|
| 244 | whd in match map_address_using_internal_pseudo_address_map; normalize nodelta |
---|
| 245 | whd in match map_acc_a_using_internal_pseudo_address_map; normalize nodelta |
---|
| 246 | >sndM_refl % |
---|
| 247 | ] |
---|
| 248 | % |
---|
| 249 | |2: |
---|
| 250 | @pair_elim #high #low #high_low_refl normalize nodelta |
---|
| 251 | inversion (eq_upper_lower upper_lower upper) #eq_upper_lower_refl normalize nodelta |
---|
| 252 | cases sfr |
---|
| 253 | [18,37: |
---|
| 254 | whd in match map_address_using_internal_pseudo_address_map; normalize nodelta |
---|
| 255 | whd in match map_acc_a_using_internal_pseudo_address_map; normalize nodelta |
---|
| 256 | >sndM_refl normalize nodelta >high_low_refl normalize nodelta |
---|
| 257 | >eq_upper_lower_refl normalize nodelta |
---|
| 258 | whd in match (set_8051_sfr ?????); // |
---|
| 259 | ] |
---|
| 260 | @get_index_v_set_index_miss whd in ⊢ (?(??%%)); |
---|
| 261 | @nmk #absurd destruct(absurd) |
---|
| 262 | ] |
---|
| 263 | qed. |
---|
| 264 | |
---|
[2160] | 265 | lemma set_8051_sfr_status_of_pseudo_status: |
---|
[2173] | 266 | ∀M, code_memory, sigma, policy, s, s', sfr, v,v'. |
---|
| 267 | status_of_pseudo_status M code_memory s sigma policy = s' → |
---|
| 268 | map_address_using_internal_pseudo_address_map M sigma sfr v = v' → |
---|
| 269 | set_8051_sfr ? (code_memory_of_pseudo_assembly_program code_memory sigma policy) s' sfr v' = |
---|
| 270 | status_of_pseudo_status M code_memory |
---|
| 271 | (set_8051_sfr pseudo_assembly_program code_memory s sfr v) sigma policy. |
---|
| 272 | #M #code_memory #sigma #policy #s #s' #sfr #v #v' #s_ok #v_ok |
---|
| 273 | <s_ok whd in ⊢ (??%%); @split_eq_status try % /2/ |
---|
[2163] | 274 | qed. |
---|
[2160] | 275 | |
---|
[2171] | 276 | lemma get_8051_sfr_status_of_pseudo_status: |
---|
[2173] | 277 | ∀M, code_memory, sigma, policy, s, s', sfr. |
---|
| 278 | status_of_pseudo_status M code_memory s sigma policy = s' → |
---|
[2171] | 279 | (get_8051_sfr (BitVectorTrie Byte 16) |
---|
| 280 | (code_memory_of_pseudo_assembly_program code_memory sigma policy) |
---|
[2173] | 281 | s' sfr = |
---|
[2171] | 282 | map_address_using_internal_pseudo_address_map M sigma sfr |
---|
| 283 | (get_8051_sfr pseudo_assembly_program code_memory s sfr)). |
---|
[2173] | 284 | #M #code_memory #sigma #policy #s #s' #sfr #s_refl <s_refl |
---|
[2171] | 285 | whd in match get_8051_sfr; normalize nodelta |
---|
| 286 | @get_index_v_status_of_pseudo_status |
---|
| 287 | qed. |
---|
| 288 | |
---|
| 289 | lemma get_8052_sfr_status_of_pseudo_status: |
---|
[2173] | 290 | ∀M, code_memory, sigma, policy, s, s', sfr. |
---|
| 291 | status_of_pseudo_status M code_memory s sigma policy = s' → |
---|
[2171] | 292 | (get_8052_sfr (BitVectorTrie Byte 16) |
---|
| 293 | (code_memory_of_pseudo_assembly_program code_memory sigma policy) |
---|
[2173] | 294 | s' sfr = |
---|
[2171] | 295 | (get_8052_sfr pseudo_assembly_program code_memory s sfr)). |
---|
[2173] | 296 | #M #code_memory #sigma #policy #s #s' #sfr #s_refl <s_refl // |
---|
[2171] | 297 | qed. |
---|
| 298 | |
---|
[2163] | 299 | lemma set_8052_sfr_status_of_pseudo_status: |
---|
[2173] | 300 | ∀M, code_memory, sigma, policy, s, s', sfr, v. |
---|
| 301 | status_of_pseudo_status M code_memory s sigma policy = s' → |
---|
| 302 | (set_8052_sfr (BitVectorTrie Byte 16) |
---|
| 303 | (code_memory_of_pseudo_assembly_program code_memory sigma policy) s' sfr v = |
---|
| 304 | status_of_pseudo_status M code_memory |
---|
| 305 | (set_8052_sfr pseudo_assembly_program code_memory s sfr v) sigma policy). |
---|
| 306 | #M #code_memory #sigma #policy #s #s' #sfr #v #s_refl <s_refl // |
---|
[2163] | 307 | qed. |
---|
[2172] | 308 | |
---|
[2163] | 309 | definition map_address_Byte_using_internal_pseudo_address_map ≝ |
---|
| 310 | λM,sigma,d,v. |
---|
| 311 | match sfr_of_Byte d with |
---|
| 312 | [ None ⇒ v |
---|
| 313 | | Some sfr8051_8052 ⇒ |
---|
[2172] | 314 | match sfr8051_8052 with |
---|
| 315 | [ inl sfr ⇒ |
---|
| 316 | map_address_using_internal_pseudo_address_map M sigma sfr v |
---|
| 317 | | inr _ ⇒ v |
---|
| 318 | ] |
---|
| 319 | ]. |
---|
[2163] | 320 | |
---|
| 321 | lemma set_bit_addressable_sfr_status_of_pseudo_status': |
---|
[2173] | 322 | let M ≝ pseudo_assembly_program in |
---|
| 323 | ∀code_memory: M. |
---|
| 324 | ∀s: PreStatus M code_memory. |
---|
| 325 | ∀d: Byte. |
---|
| 326 | ∀v: Byte. |
---|
| 327 | Σp: PreStatus M code_memory. |
---|
| 328 | ∀M. |
---|
| 329 | ∀sigma. |
---|
| 330 | ∀policy. |
---|
| 331 | ∀s'. |
---|
| 332 | ∀v'. |
---|
| 333 | status_of_pseudo_status M code_memory s sigma policy = s' → |
---|
| 334 | map_address_Byte_using_internal_pseudo_address_map M sigma d v = v' → |
---|
| 335 | (set_bit_addressable_sfr (BitVectorTrie Byte 16) |
---|
| 336 | (code_memory_of_pseudo_assembly_program code_memory sigma policy) s' d v' = |
---|
| 337 | status_of_pseudo_status M code_memory |
---|
| 338 | (set_bit_addressable_sfr pseudo_assembly_program code_memory s d v) sigma policy). |
---|
[2172] | 339 | whd in match map_address_Byte_using_internal_pseudo_address_map; |
---|
[2163] | 340 | whd in match set_bit_addressable_sfr; |
---|
| 341 | normalize nodelta |
---|
[2160] | 342 | @(let M ≝ pseudo_assembly_program in |
---|
| 343 | λcode_memory:M. |
---|
| 344 | λs: PreStatus M code_memory. |
---|
| 345 | λb: Byte. |
---|
| 346 | λv: Byte. |
---|
[2163] | 347 | match sfr_of_Byte b with |
---|
| 348 | [ None ⇒ match not_implemented in False with [ ] |
---|
| 349 | | Some sfr8051_8052 ⇒ |
---|
| 350 | match sfr8051_8052 with |
---|
| 351 | [ inl sfr ⇒ |
---|
| 352 | match sfr with |
---|
| 353 | [ SFR_P1 ⇒ |
---|
| 354 | let status_1 ≝ set_8051_sfr ?? s SFR_P1 v in |
---|
| 355 | set_p1_latch ?? s v |
---|
| 356 | | SFR_P3 ⇒ |
---|
| 357 | let status_1 ≝ set_8051_sfr ?? s SFR_P3 v in |
---|
| 358 | set_p3_latch ?? s v |
---|
| 359 | | _ ⇒ set_8051_sfr ?? s sfr v ] |
---|
| 360 | | inr sfr ⇒ set_8052_sfr ?? s sfr v ]]) |
---|
[2173] | 361 | normalize nodelta #M #sigma #policy #s' #v' #s_refl <s_refl |
---|
[2172] | 362 | /2 by refl, set_8051_sfr_status_of_pseudo_status, set_8052_sfr_status_of_pseudo_status/ |
---|
[2173] | 363 | whd in match map_address_using_internal_pseudo_address_map; normalize nodelta |
---|
| 364 | #v_refl >v_refl // |
---|
[2163] | 365 | qed. |
---|
[2160] | 366 | |
---|
[2163] | 367 | lemma set_bit_addressable_sfr_status_of_pseudo_status: |
---|
| 368 | ∀code_memory: pseudo_assembly_program. ∀s: PreStatus … code_memory. ∀d: Byte. ∀v: Byte. |
---|
[2173] | 369 | ∀M. ∀sigma. ∀policy. ∀s': Status ?. ∀v'. |
---|
| 370 | status_of_pseudo_status M code_memory s sigma policy = s' → |
---|
[2163] | 371 | map_address_Byte_using_internal_pseudo_address_map M sigma d v = v' → |
---|
| 372 | (set_bit_addressable_sfr (BitVectorTrie Byte 16) |
---|
| 373 | (code_memory_of_pseudo_assembly_program code_memory sigma policy) |
---|
[2173] | 374 | s' d v' |
---|
[2163] | 375 | =status_of_pseudo_status M code_memory |
---|
| 376 | (set_bit_addressable_sfr pseudo_assembly_program code_memory s d v) sigma policy). |
---|
| 377 | #code #s #d #v cases (set_bit_addressable_sfr_status_of_pseudo_status' code s d v) #_ |
---|
| 378 | #H @H |
---|
| 379 | qed. |
---|
| 380 | |
---|
[2164] | 381 | lemma set_low_internal_ram_status_of_pseudo_status: |
---|
[2173] | 382 | ∀cm,sigma,policy,M,s,s',ram. |
---|
| 383 | status_of_pseudo_status M cm s sigma policy = s' → |
---|
[2163] | 384 | set_low_internal_ram (BitVectorTrie Byte 16) |
---|
| 385 | (code_memory_of_pseudo_assembly_program cm sigma policy) |
---|
[2173] | 386 | s' |
---|
[2163] | 387 | (low_internal_ram_of_pseudo_low_internal_ram M ram) |
---|
| 388 | = status_of_pseudo_status M cm |
---|
| 389 | (set_low_internal_ram pseudo_assembly_program cm s ram) sigma policy. |
---|
[2173] | 390 | #cm #sigma #policy #M #s #s' #ram #s_refl <s_refl // |
---|
[2163] | 391 | qed. |
---|
[2164] | 392 | |
---|
| 393 | (* Real axiom ATM *) |
---|
| 394 | axiom insert_low_internal_ram_of_pseudo_low_internal_ram: |
---|
| 395 | ∀M,sigma,cm,s,addr,v,v'. |
---|
| 396 | map_internal_ram_address_using_pseudo_address_map M sigma (false:::addr) v = v' → |
---|
| 397 | insert Byte 7 addr v' |
---|
| 398 | (low_internal_ram_of_pseudo_low_internal_ram M |
---|
| 399 | (low_internal_ram pseudo_assembly_program cm s)) |
---|
| 400 | =low_internal_ram_of_pseudo_low_internal_ram M |
---|
| 401 | (insert Byte 7 addr v (low_internal_ram pseudo_assembly_program cm s)). |
---|
[2163] | 402 | |
---|
[2164] | 403 | lemma insert_low_internal_ram_status_of_pseudo_status: |
---|
| 404 | ∀M,cm,sigma,policy,s,addr,v,v'. |
---|
| 405 | map_internal_ram_address_using_pseudo_address_map M sigma (false:::addr) v = v' → |
---|
| 406 | insert Byte 7 addr v' |
---|
[2163] | 407 | (low_internal_ram (BitVectorTrie Byte 16) |
---|
| 408 | (code_memory_of_pseudo_assembly_program cm sigma policy) |
---|
| 409 | (status_of_pseudo_status M cm s sigma policy)) |
---|
| 410 | = low_internal_ram_of_pseudo_low_internal_ram M |
---|
| 411 | (insert Byte 7 addr v |
---|
| 412 | (low_internal_ram pseudo_assembly_program cm s)). |
---|
[2164] | 413 | /2 by insert_low_internal_ram_of_pseudo_low_internal_ram/ |
---|
| 414 | qed. |
---|
[2163] | 415 | |
---|
[2168] | 416 | (* Real axiom ATM *) |
---|
| 417 | axiom insert_high_internal_ram_of_pseudo_high_internal_ram: |
---|
| 418 | ∀M,sigma,cm,s,addr,v,v'. |
---|
| 419 | map_internal_ram_address_using_pseudo_address_map M sigma (true:::addr) v = v' → |
---|
| 420 | insert Byte 7 addr v' |
---|
| 421 | (high_internal_ram_of_pseudo_high_internal_ram M |
---|
| 422 | (high_internal_ram pseudo_assembly_program cm s)) |
---|
| 423 | =high_internal_ram_of_pseudo_high_internal_ram M |
---|
| 424 | (insert Byte 7 addr v (high_internal_ram pseudo_assembly_program cm s)). |
---|
| 425 | |
---|
| 426 | lemma insert_high_internal_ram_status_of_pseudo_status: |
---|
| 427 | ∀M,cm,sigma,policy,s,addr,v,v'. |
---|
| 428 | map_internal_ram_address_using_pseudo_address_map M sigma (true:::addr) v = v' → |
---|
| 429 | insert Byte 7 addr v' |
---|
| 430 | (high_internal_ram (BitVectorTrie Byte 16) |
---|
| 431 | (code_memory_of_pseudo_assembly_program cm sigma policy) |
---|
| 432 | (status_of_pseudo_status M cm s sigma policy)) |
---|
| 433 | = high_internal_ram_of_pseudo_high_internal_ram M |
---|
| 434 | (insert Byte 7 addr v |
---|
| 435 | (high_internal_ram pseudo_assembly_program cm s)). |
---|
| 436 | /2 by insert_high_internal_ram_of_pseudo_high_internal_ram/ |
---|
| 437 | qed. |
---|
| 438 | |
---|
[2164] | 439 | lemma bit_address_of_register_status_of_pseudo_status: |
---|
| 440 | ∀M,cm,s,sigma,policy,r. |
---|
| 441 | bit_address_of_register … |
---|
| 442 | (code_memory_of_pseudo_assembly_program cm sigma policy) |
---|
| 443 | (status_of_pseudo_status M cm s sigma policy) r = |
---|
| 444 | bit_address_of_register … cm s r. |
---|
| 445 | #M #cm #s #sigma #policy #r whd in ⊢ (??%%); |
---|
[2173] | 446 | >(get_8051_sfr_status_of_pseudo_status … (refl …)) |
---|
[2164] | 447 | @pair_elim #un #ln #_ |
---|
| 448 | @pair_elim #r1 #r0 #_ % |
---|
| 449 | qed. |
---|
| 450 | |
---|
| 451 | (*CSC: provable using the axiom in AssemblyProof, but this one seems more |
---|
| 452 | primitive *) |
---|
| 453 | axiom lookup_low_internal_ram_of_pseudo_low_internal_ram: |
---|
| 454 | ∀M,sigma,cm,s,addr. |
---|
| 455 | lookup Byte 7 addr |
---|
| 456 | (low_internal_ram_of_pseudo_low_internal_ram M |
---|
| 457 | (low_internal_ram pseudo_assembly_program cm s)) (zero 8) |
---|
| 458 | = |
---|
| 459 | map_internal_ram_address_using_pseudo_address_map M sigma (false:::addr) |
---|
| 460 | (lookup Byte 7 addr |
---|
| 461 | (low_internal_ram pseudo_assembly_program cm s) (zero 8)). |
---|
| 462 | |
---|
[2171] | 463 | (*CSC: provable using the axiom in AssemblyProof, but this one seems more |
---|
| 464 | primitive *) |
---|
| 465 | axiom lookup_high_internal_ram_of_pseudo_high_internal_ram: |
---|
| 466 | ∀M,sigma,cm,s,addr. |
---|
| 467 | lookup Byte 7 addr |
---|
| 468 | (high_internal_ram_of_pseudo_high_internal_ram M |
---|
| 469 | (high_internal_ram pseudo_assembly_program cm s)) (zero 8) |
---|
| 470 | = |
---|
| 471 | map_internal_ram_address_using_pseudo_address_map M sigma (true:::addr) |
---|
| 472 | (lookup Byte 7 addr |
---|
| 473 | (high_internal_ram pseudo_assembly_program cm s) (zero 8)). |
---|
| 474 | |
---|
[2164] | 475 | lemma get_register_status_of_pseudo_status: |
---|
[2173] | 476 | ∀M,cm,sigma,policy,s,s',r. |
---|
| 477 | status_of_pseudo_status M cm s sigma policy = s' → |
---|
[2164] | 478 | get_register … |
---|
| 479 | (code_memory_of_pseudo_assembly_program cm sigma policy) |
---|
[2173] | 480 | s' r = |
---|
[2164] | 481 | map_internal_ram_address_using_pseudo_address_map M sigma (false:::bit_address_of_register pseudo_assembly_program cm s r) |
---|
| 482 | (get_register … cm s r). |
---|
[2173] | 483 | #M #cm #sigma #policy #s #s' #r #s_refl <s_refl whd in match get_register; normalize nodelta |
---|
[2164] | 484 | whd in match status_of_pseudo_status; normalize nodelta |
---|
| 485 | >bit_address_of_register_status_of_pseudo_status |
---|
| 486 | @lookup_low_internal_ram_of_pseudo_low_internal_ram |
---|
| 487 | qed. |
---|
| 488 | |
---|
[2165] | 489 | lemma external_ram_status_of_pseudo_status: |
---|
| 490 | ∀M,cm,s,sigma,policy. |
---|
| 491 | external_ram … |
---|
| 492 | (code_memory_of_pseudo_assembly_program cm sigma policy) |
---|
| 493 | (status_of_pseudo_status M cm s sigma policy) = |
---|
| 494 | external_ram … cm s. |
---|
| 495 | // |
---|
| 496 | qed. |
---|
| 497 | |
---|
| 498 | lemma set_external_ram_status_of_pseudo_status: |
---|
| 499 | ∀M,cm,ps,sigma,policy,ram. |
---|
| 500 | set_external_ram … |
---|
| 501 | (code_memory_of_pseudo_assembly_program cm sigma policy) |
---|
| 502 | (status_of_pseudo_status M cm ps sigma policy) |
---|
| 503 | ram = |
---|
| 504 | status_of_pseudo_status M cm (set_external_ram … cm ps ram) sigma policy. |
---|
| 505 | // |
---|
| 506 | qed. |
---|
| 507 | |
---|
[2167] | 508 | lemma set_register_status_of_pseudo_status: |
---|
[2173] | 509 | ∀M,sigma,policy,cm,s,s',r,v,v'. |
---|
| 510 | status_of_pseudo_status M cm s sigma policy = s' → |
---|
[2167] | 511 | map_internal_ram_address_using_pseudo_address_map M sigma |
---|
| 512 | (false:::bit_address_of_register pseudo_assembly_program cm s r) v =v' → |
---|
| 513 | set_register (BitVectorTrie Byte 16) |
---|
| 514 | (code_memory_of_pseudo_assembly_program cm sigma policy) |
---|
[2173] | 515 | s' r v' |
---|
[2167] | 516 | = status_of_pseudo_status M cm (set_register pseudo_assembly_program cm s r v) |
---|
| 517 | sigma policy. |
---|
[2173] | 518 | #M #sigma #policy #cm #s #s' #r #v #v' #s_refl <s_refl #v_ok |
---|
[2167] | 519 | whd in match set_register; normalize nodelta |
---|
| 520 | >bit_address_of_register_status_of_pseudo_status |
---|
| 521 | >(insert_low_internal_ram_status_of_pseudo_status … v_ok) |
---|
[2173] | 522 | @set_low_internal_ram_status_of_pseudo_status % |
---|
[2167] | 523 | qed. |
---|
| 524 | |
---|
[2166] | 525 | definition map_address_mode_using_internal_pseudo_address_map_ok1 ≝ |
---|
[2171] | 526 | λM:internal_pseudo_address_map.λcm.λs:PreStatus ? cm.λsigma. λaddr. |
---|
[2163] | 527 | match addr with |
---|
[2166] | 528 | [ INDIRECT i ⇒ |
---|
| 529 | assoc_list_lookup ?? |
---|
| 530 | (false:::bit_address_of_register pseudo_assembly_program cm s [[false; false; i]]) (eq_bv …) (\fst M) = None … |
---|
| 531 | | EXT_INDIRECT e ⇒ |
---|
| 532 | assoc_list_lookup ?? |
---|
| 533 | (false:::bit_address_of_register pseudo_assembly_program cm s [[false; false; e]]) (eq_bv …) (\fst M) = None … |
---|
[2171] | 534 | | ACC_DPTR ⇒ |
---|
| 535 | (* XXX: \snd M = None plus in the very rare case when we are trying to dereference a null (O) pointer |
---|
| 536 | in the ACC_A *) |
---|
| 537 | map_acc_a_using_internal_pseudo_address_map M sigma (get_8051_sfr pseudo_assembly_program cm s SFR_ACC_A) = |
---|
| 538 | get_8051_sfr … cm s SFR_ACC_A |
---|
| 539 | | ACC_PC ⇒ |
---|
| 540 | (* XXX: as above *) |
---|
| 541 | map_acc_a_using_internal_pseudo_address_map M sigma (get_8051_sfr pseudo_assembly_program cm s SFR_ACC_A) = |
---|
| 542 | get_8051_sfr … cm s SFR_ACC_A ∧ sigma (program_counter … s) = program_counter … s |
---|
[2166] | 543 | | _ ⇒ True ]. |
---|
| 544 | |
---|
| 545 | definition map_address_mode_using_internal_pseudo_address_map_ok2 ≝ |
---|
| 546 | λT,M,sigma,cm.λs:PreStatus T cm.λaddr,v. |
---|
| 547 | match addr with |
---|
[2163] | 548 | [ DIRECT d ⇒ |
---|
[2164] | 549 | let 〈 bit_one, seven_bits 〉 as vsplit_refl ≝ vsplit … 1 7 d in |
---|
| 550 | match head' … bit_one with |
---|
[2163] | 551 | [ true ⇒ |
---|
[2164] | 552 | map_address_Byte_using_internal_pseudo_address_map M sigma (true:::seven_bits) v |
---|
| 553 | | false ⇒ |
---|
[2166] | 554 | map_internal_ram_address_using_pseudo_address_map M sigma (false:::seven_bits) v ] |
---|
[2164] | 555 | | INDIRECT i ⇒ |
---|
| 556 | let register ≝ get_register ?? s [[ false; false; i ]] in |
---|
[2166] | 557 | map_internal_ram_address_using_pseudo_address_map M sigma register v |
---|
[2167] | 558 | | REGISTER r ⇒ |
---|
| 559 | map_internal_ram_address_using_pseudo_address_map M sigma |
---|
| 560 | (false:::bit_address_of_register … s r) v |
---|
[2166] | 561 | | ACC_A ⇒ |
---|
| 562 | map_address_using_internal_pseudo_address_map M sigma SFR_ACC_A v |
---|
| 563 | | _ ⇒ v ]. |
---|
[2163] | 564 | |
---|
[2164] | 565 | (*CSC: move elsewhere*) |
---|
| 566 | lemma eq_head': ∀A,n,v. v = head' A n v ::: tail … v. |
---|
| 567 | #A #n #v inversion v in ⊢ ?; |
---|
| 568 | [ #abs @⊥ lapply (jmeq_to_eq ??? abs) /2/ |
---|
| 569 | | #m #hd #tl #_ #EQ <(injective_S … EQ) in tl; #tl #EQ' >EQ' % ] |
---|
[2160] | 570 | qed. |
---|
| 571 | |
---|
[2164] | 572 | (*CSC: move elsewhere*) |
---|
| 573 | lemma tail_singleton: ∀A,v. tail A 0 v = [[]]. |
---|
| 574 | #A #v inversion v in ⊢ ?; |
---|
| 575 | [ #abs @⊥ lapply (jmeq_to_eq ??? abs) #H destruct(H) |
---|
| 576 | | #n #hd #tl #_ #EQ <(injective_S … EQ) in tl; #tl #EQ1 >EQ1 normalize |
---|
| 577 | /2 by jmeq_to_eq/ |
---|
| 578 | ] |
---|
| 579 | qed. |
---|
| 580 | |
---|
| 581 | (*CSC: move elsewhere*) |
---|
| 582 | lemma eq_cons_head_append: |
---|
| 583 | ∀A,n.∀hd: Vector A 1. ∀tl: Vector A n. |
---|
| 584 | head' A 0 hd:::tl = hd@@tl. |
---|
| 585 | #A #n #hd #tl >(eq_head' … hd) >tail_singleton % |
---|
| 586 | qed. |
---|
| 587 | |
---|
[2160] | 588 | lemma set_arg_8_status_of_pseudo_status: |
---|
| 589 | ∀cm. |
---|
| 590 | ∀ps. |
---|
[2163] | 591 | ∀addr:[[ direct ; indirect ; registr ; acc_a ; acc_b ; ext_indirect ; ext_indirect_dptr ]]. |
---|
[2173] | 592 | ∀value. Σp: PreStatus ? cm. ∀M. ∀sigma. ∀policy. ∀s'. ∀value'. |
---|
| 593 | status_of_pseudo_status M cm ps sigma policy = s' → |
---|
[2171] | 594 | map_address_mode_using_internal_pseudo_address_map_ok1 M cm ps sigma addr → |
---|
[2166] | 595 | map_address_mode_using_internal_pseudo_address_map_ok2 … M sigma cm ps addr value = value' → |
---|
[2160] | 596 | set_arg_8 (BitVectorTrie Byte 16) |
---|
| 597 | (code_memory_of_pseudo_assembly_program cm sigma policy) |
---|
[2173] | 598 | s' addr value' = |
---|
[2160] | 599 | status_of_pseudo_status M cm (set_arg_8 … cm ps addr value) sigma policy. |
---|
[2163] | 600 | whd in match set_arg_8; normalize nodelta |
---|
[2160] | 601 | @(let m ≝ pseudo_assembly_program in λcm, s. λa: [[ direct ; indirect ; registr ; |
---|
| 602 | acc_a ; acc_b ; ext_indirect ; |
---|
| 603 | ext_indirect_dptr ]]. λv. |
---|
| 604 | match a return λaddr. bool_to_Prop (is_in ? [[ direct ; indirect ; registr ; |
---|
| 605 | acc_a ; acc_b ; ext_indirect ; |
---|
| 606 | ext_indirect_dptr ]] addr) → |
---|
[2163] | 607 | Σp.? |
---|
[2160] | 608 | with |
---|
| 609 | [ DIRECT d ⇒ |
---|
| 610 | λdirect: True. |
---|
[2164] | 611 | deplet 〈 bit_one, seven_bits 〉 as vsplit_refl ≝ vsplit ? 1 7 d in |
---|
| 612 | match head' … bit_one with |
---|
| 613 | [ true ⇒ set_bit_addressable_sfr ?? s (true:::seven_bits) v |
---|
[2160] | 614 | | false ⇒ |
---|
[2164] | 615 | let memory ≝ insert ? 7 seven_bits v (low_internal_ram ?? s) in |
---|
[2160] | 616 | set_low_internal_ram ?? s memory |
---|
| 617 | ] |
---|
| 618 | | INDIRECT i ⇒ |
---|
| 619 | λindirect: True. |
---|
| 620 | let register ≝ get_register ?? s [[ false; false; i ]] in |
---|
[2164] | 621 | let 〈bit_one, seven_bits〉 ≝ vsplit ? 1 7 register in |
---|
| 622 | match head' … bit_one with |
---|
[2160] | 623 | [ false ⇒ |
---|
[2164] | 624 | let memory ≝ insert … seven_bits v (low_internal_ram ?? s) in |
---|
[2160] | 625 | set_low_internal_ram ?? s memory |
---|
| 626 | | true ⇒ |
---|
[2164] | 627 | let memory ≝ insert … seven_bits v (high_internal_ram ?? s) in |
---|
[2160] | 628 | set_high_internal_ram ?? s memory |
---|
| 629 | ] |
---|
| 630 | | REGISTER r ⇒ λregister: True. set_register ?? s r v |
---|
| 631 | | ACC_A ⇒ λacc_a: True. set_8051_sfr ?? s SFR_ACC_A v |
---|
| 632 | | ACC_B ⇒ λacc_b: True. set_8051_sfr ?? s SFR_ACC_B v |
---|
| 633 | | EXT_INDIRECT e ⇒ |
---|
| 634 | λext_indirect: True. |
---|
| 635 | let address ≝ get_register ?? s [[ false; false; e ]] in |
---|
| 636 | let padded_address ≝ pad 8 8 address in |
---|
| 637 | let memory ≝ insert ? 16 padded_address v (external_ram ?? s) in |
---|
| 638 | set_external_ram ?? s memory |
---|
| 639 | | EXT_INDIRECT_DPTR ⇒ |
---|
| 640 | λext_indirect_dptr: True. |
---|
| 641 | let address ≝ (get_8051_sfr ?? s SFR_DPH) @@ (get_8051_sfr ?? s SFR_DPL) in |
---|
| 642 | let memory ≝ insert ? 16 address v (external_ram ?? s) in |
---|
| 643 | set_external_ram ?? s memory |
---|
| 644 | | _ ⇒ |
---|
| 645 | λother: False. |
---|
| 646 | match other in False with [ ] |
---|
[2163] | 647 | ] (subaddressing_modein … a)) normalize nodelta |
---|
[2173] | 648 | #M #sigma #policy #s' #v' #s_refl <s_refl |
---|
[2166] | 649 | whd in match map_address_mode_using_internal_pseudo_address_map_ok1; normalize nodelta |
---|
| 650 | whd in match map_address_mode_using_internal_pseudo_address_map_ok2; normalize nodelta |
---|
[2163] | 651 | [1,2: |
---|
| 652 | <vsplit_refl normalize nodelta >p normalize nodelta |
---|
[2166] | 653 | [ >(vsplit_ok … vsplit_refl) #_ @set_bit_addressable_sfr_status_of_pseudo_status |
---|
| 654 | | #_ #v_ok >(insert_low_internal_ram_status_of_pseudo_status … v) // ] |
---|
| 655 | |3,4: #EQ1 #EQ2 change with (get_register ????) in match register in p; |
---|
[2173] | 656 | >(get_register_status_of_pseudo_status … (refl …)) |
---|
[2164] | 657 | whd in match map_internal_ram_address_using_pseudo_address_map; normalize nodelta |
---|
| 658 | >EQ1 normalize nodelta >p normalize nodelta >p1 normalize nodelta |
---|
[2168] | 659 | [ >(insert_high_internal_ram_status_of_pseudo_status … v) |
---|
| 660 | | >(insert_low_internal_ram_status_of_pseudo_status … v) ] |
---|
| 661 | // <EQ2 @eq_f2 try % <(vsplit_ok … (sym_eq … p)) <eq_cons_head_append >p1 % |
---|
[2173] | 662 | |5: #EQ1 #EQ2 <EQ2 >(get_register_status_of_pseudo_status … (refl …)) |
---|
[2165] | 663 | whd in match map_internal_ram_address_using_pseudo_address_map; normalize nodelta |
---|
| 664 | >EQ1 normalize nodelta |
---|
| 665 | >external_ram_status_of_pseudo_status @set_external_ram_status_of_pseudo_status |
---|
[2167] | 666 | |6: #EQ1 #EQ2 <EQ2 /2 by set_register_status_of_pseudo_status/ |
---|
[2166] | 667 | |7: #EQ1 #EQ2 <EQ2 /2 by set_8051_sfr_status_of_pseudo_status/ |
---|
| 668 | |8: #_ #EQ <EQ @set_8051_sfr_status_of_pseudo_status % |
---|
[2173] | 669 | |9: #_ #EQ <EQ >(get_8051_sfr_status_of_pseudo_status … (refl …)) |
---|
| 670 | >(get_8051_sfr_status_of_pseudo_status … (refl …)) |
---|
| 671 | >external_ram_status_of_pseudo_status @set_external_ram_status_of_pseudo_status ] % |
---|
[2171] | 672 | qed. |
---|
| 673 | |
---|
| 674 | lemma p1_latch_status_of_pseudo_status: |
---|
| 675 | ∀M. |
---|
[2173] | 676 | ∀sigma. |
---|
| 677 | ∀policy. |
---|
[2171] | 678 | ∀code_memory: pseudo_assembly_program. |
---|
| 679 | ∀s: PreStatus … code_memory. |
---|
[2173] | 680 | ∀s'. |
---|
| 681 | (status_of_pseudo_status M code_memory s sigma policy) = s' → |
---|
[2171] | 682 | (p1_latch (BitVectorTrie Byte 16) |
---|
| 683 | (code_memory_of_pseudo_assembly_program code_memory sigma policy) |
---|
[2173] | 684 | s' = |
---|
[2171] | 685 | (p1_latch pseudo_assembly_program code_memory s)). |
---|
[2173] | 686 | #M #sigma #policy #code_memory #s #s' #s_refl <s_refl // |
---|
[2171] | 687 | qed. |
---|
| 688 | |
---|
| 689 | lemma p3_latch_status_of_pseudo_status: |
---|
| 690 | ∀M. |
---|
[2173] | 691 | ∀sigma. |
---|
| 692 | ∀policy. |
---|
[2171] | 693 | ∀code_memory: pseudo_assembly_program. |
---|
| 694 | ∀s: PreStatus … code_memory. |
---|
[2173] | 695 | ∀s'. |
---|
| 696 | (status_of_pseudo_status M code_memory s sigma policy) = s' → |
---|
[2171] | 697 | (p3_latch (BitVectorTrie Byte 16) |
---|
| 698 | (code_memory_of_pseudo_assembly_program code_memory sigma policy) |
---|
| 699 | (status_of_pseudo_status M code_memory s sigma policy) = |
---|
| 700 | (p3_latch pseudo_assembly_program code_memory s)). |
---|
[2173] | 701 | #M #sigma #policy #code_memory #s #s' #s_refl <s_refl // |
---|
[2171] | 702 | qed. |
---|
| 703 | |
---|
| 704 | lemma get_bit_addressable_sfr_status_of_pseudo_status': |
---|
| 705 | let M ≝ pseudo_assembly_program in |
---|
| 706 | ∀code_memory: M. |
---|
| 707 | ∀s: PreStatus M code_memory. |
---|
| 708 | ∀d: Byte. |
---|
| 709 | ∀l: bool. |
---|
[2173] | 710 | Σp: Byte. ∀M. ∀sigma. ∀policy. ∀s'. |
---|
| 711 | status_of_pseudo_status M code_memory s sigma policy = s' → |
---|
[2171] | 712 | (get_bit_addressable_sfr (BitVectorTrie Byte 16) |
---|
| 713 | (code_memory_of_pseudo_assembly_program code_memory sigma policy) |
---|
[2173] | 714 | s' d l = |
---|
[2171] | 715 | map_address_Byte_using_internal_pseudo_address_map M sigma |
---|
| 716 | d (get_bit_addressable_sfr pseudo_assembly_program code_memory s d l)). |
---|
| 717 | whd in match get_bit_addressable_sfr; |
---|
| 718 | whd in match map_address_Byte_using_internal_pseudo_address_map; |
---|
| 719 | normalize nodelta |
---|
| 720 | @(let M ≝ pseudo_assembly_program in |
---|
| 721 | λcode_memory:M. |
---|
| 722 | λs: PreStatus M code_memory. |
---|
| 723 | λb: Byte. |
---|
| 724 | λl: bool. |
---|
| 725 | match sfr_of_Byte b with |
---|
| 726 | [ None ⇒ match not_implemented in False with [ ] |
---|
| 727 | | Some sfr8051_8052 ⇒ |
---|
| 728 | match sfr8051_8052 with |
---|
| 729 | [ inl sfr ⇒ |
---|
| 730 | match sfr with |
---|
| 731 | [ SFR_P1 ⇒ |
---|
| 732 | if l then |
---|
| 733 | p1_latch … s |
---|
| 734 | else |
---|
| 735 | get_8051_sfr … s SFR_P1 |
---|
| 736 | | SFR_P3 ⇒ |
---|
| 737 | if l then |
---|
| 738 | p3_latch … s |
---|
| 739 | else |
---|
| 740 | get_8051_sfr … s SFR_P3 |
---|
| 741 | | _ ⇒ get_8051_sfr … s sfr |
---|
| 742 | ] |
---|
| 743 | | inr sfr ⇒ get_8052_sfr M code_memory s sfr |
---|
| 744 | ] |
---|
| 745 | ]) |
---|
[2173] | 746 | #M #sigma #policy #s' #s_refl <s_refl normalize nodelta |
---|
| 747 | /2 by get_8051_sfr_status_of_pseudo_status, p1_latch_status_of_pseudo_status, p3_latch_status_of_pseudo_status/ |
---|
[2171] | 748 | qed. |
---|
| 749 | |
---|
| 750 | lemma get_bit_addressable_sfr_status_of_pseudo_status: |
---|
| 751 | let M ≝ pseudo_assembly_program in |
---|
| 752 | ∀code_memory: M. |
---|
| 753 | ∀s: PreStatus M code_memory. |
---|
| 754 | ∀d: Byte. |
---|
| 755 | ∀l: bool. |
---|
[2173] | 756 | ∀M. ∀sigma. ∀policy. ∀s'. |
---|
| 757 | (status_of_pseudo_status M code_memory s sigma policy) = s' → |
---|
[2171] | 758 | (get_bit_addressable_sfr (BitVectorTrie Byte 16) |
---|
| 759 | (code_memory_of_pseudo_assembly_program code_memory sigma policy) |
---|
[2173] | 760 | s' d l = |
---|
[2171] | 761 | map_address_Byte_using_internal_pseudo_address_map M sigma |
---|
| 762 | d (get_bit_addressable_sfr pseudo_assembly_program code_memory s d l)). |
---|
| 763 | #code #s #d #v cases (get_bit_addressable_sfr_status_of_pseudo_status' code s d v) #_ |
---|
| 764 | #H @H |
---|
| 765 | qed. |
---|
| 766 | |
---|
| 767 | lemma program_counter_status_of_pseudo_status: |
---|
[2173] | 768 | ∀M. ∀sigma. ∀policy. |
---|
[2171] | 769 | ∀code_memory: pseudo_assembly_program. |
---|
| 770 | ∀s: PreStatus ? code_memory. |
---|
[2173] | 771 | ∀s'. |
---|
| 772 | (status_of_pseudo_status M code_memory s sigma policy) = s' → |
---|
[2171] | 773 | program_counter … (code_memory_of_pseudo_assembly_program code_memory sigma policy) |
---|
[2173] | 774 | s' = |
---|
[2171] | 775 | sigma (program_counter … s). |
---|
[2173] | 776 | #M #sigma #policy #code_memory #s #s' #s_refl <s_refl // |
---|
[2171] | 777 | qed. |
---|
| 778 | |
---|
| 779 | lemma get_cy_flag_status_of_pseudo_status: |
---|
[2173] | 780 | ∀M, cm, sigma, policy, s, s'. |
---|
| 781 | (status_of_pseudo_status M cm s sigma policy) = s' → |
---|
[2171] | 782 | (get_cy_flag (BitVectorTrie Byte 16) |
---|
| 783 | (code_memory_of_pseudo_assembly_program cm sigma policy) |
---|
[2173] | 784 | s' = |
---|
[2171] | 785 | get_cy_flag pseudo_assembly_program cm s). |
---|
[2173] | 786 | #M #cm #sigma #policy #s #s' #s_refl <s_refl |
---|
[2171] | 787 | whd in match get_cy_flag; normalize nodelta |
---|
| 788 | >get_index_v_status_of_pseudo_status % |
---|
| 789 | qed. |
---|
| 790 | |
---|
| 791 | lemma get_arg_8_status_of_pseudo_status: |
---|
| 792 | ∀cm. |
---|
| 793 | ∀ps. |
---|
| 794 | ∀l. |
---|
| 795 | ∀addr:[[ direct ; indirect ; registr ; acc_a ; acc_b ; data ; acc_dptr ; acc_pc ; ext_indirect ; ext_indirect_dptr ]]. |
---|
[2173] | 796 | Σp: Byte. ∀M. ∀sigma. ∀policy. ∀s'. |
---|
| 797 | (status_of_pseudo_status M cm ps sigma policy) = s' → |
---|
[2171] | 798 | map_address_mode_using_internal_pseudo_address_map_ok1 M cm ps sigma addr → |
---|
| 799 | get_arg_8 (BitVectorTrie Byte 16) (code_memory_of_pseudo_assembly_program cm sigma policy) |
---|
[2173] | 800 | s' l addr = |
---|
[2171] | 801 | map_address_mode_using_internal_pseudo_address_map_ok2 … M sigma cm ps addr (get_arg_8 … cm ps l addr). |
---|
| 802 | whd in match get_arg_8; normalize nodelta |
---|
| 803 | @(let m ≝ pseudo_assembly_program in |
---|
| 804 | λcm: m. λs: PreStatus m cm. λl: bool. λa: [[direct; indirect; registr; acc_a; acc_b; data; acc_dptr; acc_pc; ext_indirect; ext_indirect_dptr]]. |
---|
| 805 | match a return λx. bool_to_Prop (is_in ? [[ direct; indirect; registr; acc_a; acc_b; data; acc_dptr; acc_pc; ext_indirect; ext_indirect_dptr ]] x) → Σp. ? with |
---|
| 806 | [ ACC_A ⇒ λacc_a: True. get_8051_sfr ?? s SFR_ACC_A |
---|
| 807 | | ACC_B ⇒ λacc_b: True. get_8051_sfr ?? s SFR_ACC_B |
---|
| 808 | | DATA d ⇒ λdata: True. d |
---|
| 809 | | REGISTER r ⇒ λregister: True. get_register ?? s r |
---|
| 810 | | EXT_INDIRECT_DPTR ⇒ |
---|
| 811 | λext_indirect_dptr: True. |
---|
| 812 | let address ≝ (get_8051_sfr ?? s SFR_DPH) @@ (get_8051_sfr ?? s SFR_DPL) in |
---|
| 813 | lookup ? 16 address (external_ram ?? s) (zero 8) |
---|
| 814 | | EXT_INDIRECT e ⇒ |
---|
| 815 | λext_indirect: True. |
---|
| 816 | let address ≝ get_register ?? s [[ false; false; e ]] in |
---|
| 817 | let padded_address ≝ pad 8 8 address in |
---|
| 818 | lookup ? 16 padded_address (external_ram ?? s) (zero 8) |
---|
| 819 | | ACC_DPTR ⇒ |
---|
| 820 | λacc_dptr: True. |
---|
| 821 | let dptr ≝ (get_8051_sfr ?? s SFR_DPH) @@ (get_8051_sfr ?? s SFR_DPL) in |
---|
| 822 | let padded_acc ≝ pad 8 8 (get_8051_sfr ?? s SFR_ACC_A) in |
---|
| 823 | let 〈carry, address〉 ≝ half_add 16 dptr padded_acc in |
---|
| 824 | lookup ? 16 address (external_ram ?? s) (zero 8) |
---|
| 825 | | ACC_PC ⇒ |
---|
| 826 | λacc_pc: True. |
---|
| 827 | let padded_acc ≝ pad 8 8 (get_8051_sfr ?? s SFR_ACC_A) in |
---|
| 828 | let 〈 carry, address 〉 ≝ half_add 16 (program_counter ?? s) padded_acc in |
---|
| 829 | lookup ? 16 address (external_ram ?? s) (zero 8) |
---|
| 830 | | DIRECT d ⇒ |
---|
| 831 | λdirect: True. |
---|
| 832 | let 〈hd, seven_bits〉 ≝ vsplit bool 1 7 d in |
---|
| 833 | match head' … hd with |
---|
| 834 | [ true ⇒ get_bit_addressable_sfr m cm s (true:::seven_bits) l |
---|
| 835 | | false ⇒ lookup ? 7 seven_bits (low_internal_ram … s) (zero …) |
---|
| 836 | ] |
---|
| 837 | | INDIRECT i ⇒ |
---|
| 838 | λindirect: True. |
---|
| 839 | let 〈hd, seven_bits〉 ≝ vsplit bool 1 7 (get_register … s [[false;false;i]]) in |
---|
| 840 | match head' … hd with |
---|
| 841 | [ true ⇒ lookup ? 7 seven_bits (high_internal_ram … s) (zero …) |
---|
| 842 | | false ⇒ lookup ? 7 seven_bits (low_internal_ram … s) (zero …) |
---|
| 843 | ] |
---|
| 844 | | _ ⇒ λother: False. |
---|
| 845 | match other in False with [ ] |
---|
| 846 | ] (subaddressing_modein … a)) normalize nodelta |
---|
[2173] | 847 | #M #sigma #policy #s' #s_refl <s_refl |
---|
[2171] | 848 | whd in match map_address_mode_using_internal_pseudo_address_map_ok1; normalize nodelta |
---|
| 849 | whd in match map_address_mode_using_internal_pseudo_address_map_ok2; normalize nodelta |
---|
| 850 | [1: |
---|
| 851 | #_ >p normalize nodelta >p1 normalize nodelta |
---|
[2173] | 852 | @get_bit_addressable_sfr_status_of_pseudo_status % |
---|
[2171] | 853 | |2: |
---|
| 854 | #_>p normalize nodelta >p1 normalize nodelta |
---|
| 855 | @lookup_low_internal_ram_of_pseudo_low_internal_ram |
---|
| 856 | |3,4: |
---|
[2173] | 857 | #assoc_list_assm >(get_register_status_of_pseudo_status … (refl …)) |
---|
[2171] | 858 | whd in match map_internal_ram_address_using_pseudo_address_map in ⊢ (??%?); normalize nodelta |
---|
| 859 | >assoc_list_assm normalize nodelta >p normalize nodelta >p1 normalize nodelta |
---|
| 860 | [1: |
---|
| 861 | >(lookup_high_internal_ram_of_pseudo_high_internal_ram … sigma) |
---|
| 862 | |2: |
---|
| 863 | >(lookup_low_internal_ram_of_pseudo_low_internal_ram … sigma) |
---|
| 864 | ] |
---|
| 865 | @eq_f2 try % <(vsplit_ok … (sym_eq … p)) <eq_cons_head_append >p1 % |
---|
| 866 | |5: |
---|
[2173] | 867 | #assoc_list_assm >(get_register_status_of_pseudo_status … (refl …)) |
---|
[2171] | 868 | whd in match map_internal_ram_address_using_pseudo_address_map in ⊢ (??%?); normalize nodelta |
---|
| 869 | >assoc_list_assm normalize nodelta % |
---|
| 870 | |6,7,8,9: |
---|
| 871 | #_ /2/ |
---|
| 872 | |10: |
---|
[2173] | 873 | #acc_a_assm >(get_8051_sfr_status_of_pseudo_status … (refl …)) |
---|
| 874 | >(get_8051_sfr_status_of_pseudo_status … (refl …)) |
---|
| 875 | >(get_8051_sfr_status_of_pseudo_status … (refl …)) |
---|
[2171] | 876 | whd in match map_address_using_internal_pseudo_address_map; normalize nodelta |
---|
| 877 | >acc_a_assm >p normalize nodelta // |
---|
| 878 | |11: |
---|
[2173] | 879 | * #map_acc_a_assm #sigma_assm >(get_8051_sfr_status_of_pseudo_status … (refl …)) |
---|
| 880 | >(program_counter_status_of_pseudo_status … (refl …)) |
---|
[2171] | 881 | whd in match map_address_using_internal_pseudo_address_map; normalize nodelta |
---|
| 882 | >sigma_assm >map_acc_a_assm >p normalize nodelta // |
---|
| 883 | |12: |
---|
[2173] | 884 | #_ >(get_8051_sfr_status_of_pseudo_status … (refl …)) |
---|
| 885 | >(get_8051_sfr_status_of_pseudo_status … (refl …)) |
---|
[2171] | 886 | >external_ram_status_of_pseudo_status // |
---|
| 887 | ] |
---|
| 888 | qed. |
---|
| 889 | |
---|
| 890 | lemma get_arg_16_status_of_pseudo_status: |
---|
| 891 | ∀cm. |
---|
| 892 | ∀ps. |
---|
| 893 | ∀addr: [[data16]]. |
---|
[2173] | 894 | ∀M. ∀sigma. ∀policy. ∀s'. |
---|
| 895 | status_of_pseudo_status M cm ps sigma policy = s' → |
---|
[2171] | 896 | get_arg_16 (BitVectorTrie Byte 16) (code_memory_of_pseudo_assembly_program cm sigma policy) |
---|
[2173] | 897 | s' addr = |
---|
[2171] | 898 | (get_arg_16 … cm ps addr). |
---|
[2173] | 899 | #cm #ps #addr #M #sigma #policy #s' #s_refl <s_refl // |
---|
[2171] | 900 | qed. |
---|
| 901 | |
---|
| 902 | lemma set_arg_16_status_of_pseudo_status: |
---|
| 903 | ∀cm. |
---|
| 904 | ∀ps. |
---|
| 905 | ∀addr: [[dptr]]. |
---|
| 906 | ∀v: Word. |
---|
[2173] | 907 | ∀M. ∀sigma. ∀policy. ∀s'. |
---|
| 908 | status_of_pseudo_status M cm ps sigma policy = s' → |
---|
[2171] | 909 | set_arg_16 (BitVectorTrie Byte 16) (code_memory_of_pseudo_assembly_program cm sigma policy) |
---|
[2173] | 910 | s' v addr = |
---|
[2171] | 911 | status_of_pseudo_status M cm (set_arg_16 ? cm ps v addr) sigma policy. |
---|
[2173] | 912 | #cm #ps #addr #v #M #sigma #policy #s' #s_refl <s_refl |
---|
[2171] | 913 | @(subaddressing_mode_elim … addr) |
---|
| 914 | whd in match set_arg_16; normalize nodelta |
---|
| 915 | whd in match set_arg_16'; normalize nodelta |
---|
| 916 | @(vsplit_elim bool ???) #bu #bl #bu_bl_refl normalize nodelta |
---|
[2173] | 917 | @set_8051_sfr_status_of_pseudo_status try % @sym_eq |
---|
| 918 | @set_8051_sfr_status_of_pseudo_status % |
---|
[2171] | 919 | qed. |
---|
| 920 | |
---|
| 921 | definition map_bit_address_mode_using_internal_pseudo_address_map_get ≝ |
---|
| 922 | λM:internal_pseudo_address_map.λcm: pseudo_assembly_program.λs:PreStatus ? cm.λsigma: Word → Word. λaddr. λl. |
---|
| 923 | match addr with |
---|
| 924 | [ BIT_ADDR b ⇒ |
---|
| 925 | let 〈bit_1, seven_bits〉 ≝ vsplit … 1 7 b in |
---|
| 926 | match head' … bit_1 with |
---|
| 927 | [ true ⇒ |
---|
| 928 | let address ≝ nat_of_bitvector … seven_bits in |
---|
| 929 | let d ≝ address ÷ 8 in |
---|
| 930 | let m ≝ address mod 8 in |
---|
| 931 | let trans ≝ bitvector_of_nat 8 ((d * 8) + 128) in |
---|
| 932 | map_address_Byte_using_internal_pseudo_address_map M sigma trans (get_bit_addressable_sfr pseudo_assembly_program cm s trans l) = get_bit_addressable_sfr … cm s trans l |
---|
| 933 | | false ⇒ |
---|
| 934 | let address ≝ nat_of_bitvector … seven_bits in |
---|
| 935 | let address' ≝ bitvector_of_nat 7 ((address ÷ 8) + 32) in |
---|
| 936 | let t ≝ lookup … 7 address' (low_internal_ram ?? s) (zero 8) in |
---|
| 937 | map_internal_ram_address_using_pseudo_address_map M sigma |
---|
| 938 | (false:::address') t = t |
---|
| 939 | ] |
---|
| 940 | | N_BIT_ADDR b ⇒ |
---|
| 941 | let 〈bit_1, seven_bits〉 ≝ vsplit … 1 7 b in |
---|
| 942 | match head' … bit_1 with |
---|
| 943 | [ true ⇒ |
---|
| 944 | let address ≝ nat_of_bitvector … seven_bits in |
---|
| 945 | let d ≝ address ÷ 8 in |
---|
| 946 | let m ≝ address mod 8 in |
---|
| 947 | let trans ≝ bitvector_of_nat 8 ((d * 8) + 128) in |
---|
| 948 | map_address_Byte_using_internal_pseudo_address_map M sigma trans (get_bit_addressable_sfr pseudo_assembly_program cm s trans l) = get_bit_addressable_sfr … cm s trans l |
---|
| 949 | | false ⇒ |
---|
| 950 | let address ≝ nat_of_bitvector … seven_bits in |
---|
| 951 | let address' ≝ bitvector_of_nat 7 ((address ÷ 8) + 32) in |
---|
| 952 | let t ≝ lookup … 7 address' (low_internal_ram ?? s) (zero 8) in |
---|
| 953 | map_internal_ram_address_using_pseudo_address_map M sigma |
---|
| 954 | (false:::address') t = t |
---|
| 955 | ] |
---|
| 956 | | _ ⇒ True ]. |
---|
| 957 | |
---|
| 958 | lemma get_arg_1_status_of_pseudo_status': |
---|
| 959 | ∀cm. |
---|
| 960 | ∀ps. |
---|
| 961 | ∀addr: [[bit_addr; n_bit_addr; carry]]. |
---|
| 962 | ∀l. |
---|
[2173] | 963 | Σb: bool. ∀M. ∀sigma. ∀policy. ∀s'. |
---|
| 964 | status_of_pseudo_status M cm ps sigma policy = s' → |
---|
[2171] | 965 | map_bit_address_mode_using_internal_pseudo_address_map_get M cm ps sigma addr l → |
---|
| 966 | get_arg_1 (BitVectorTrie Byte 16) (code_memory_of_pseudo_assembly_program cm sigma policy) |
---|
[2173] | 967 | s' addr l = |
---|
[2171] | 968 | (get_arg_1 … cm ps addr l). |
---|
| 969 | whd in match get_arg_1; normalize nodelta |
---|
| 970 | @(let m ≝ pseudo_assembly_program in |
---|
| 971 | λcm: m. λs: PseudoStatus cm. λa:[[bit_addr; n_bit_addr; carry]]. λl. |
---|
| 972 | match a return λx. bool_to_Prop (is_in ? [[ bit_addr ; |
---|
| 973 | n_bit_addr ; |
---|
| 974 | carry ]] x) → Σb: bool. ? with |
---|
| 975 | [ BIT_ADDR b ⇒ |
---|
| 976 | λbit_addr: True. |
---|
| 977 | let 〈bit_1, seven_bits〉 ≝ vsplit … 1 7 b in |
---|
| 978 | match head' … bit_1 with |
---|
| 979 | [ true ⇒ |
---|
| 980 | let address ≝ nat_of_bitvector … seven_bits in |
---|
| 981 | let d ≝ address ÷ 8 in |
---|
| 982 | let m ≝ address mod 8 in |
---|
| 983 | let trans ≝ bitvector_of_nat 8 ((d * 8) + 128) in |
---|
| 984 | let sfr ≝ get_bit_addressable_sfr ?? s trans l in |
---|
| 985 | get_index_v … sfr m ? |
---|
| 986 | | false ⇒ |
---|
| 987 | let address ≝ nat_of_bitvector … seven_bits in |
---|
| 988 | let address' ≝ bitvector_of_nat 7 ((address ÷ 8) + 32) in |
---|
| 989 | let t ≝ lookup … 7 address' (low_internal_ram ?? s) (zero 8) in |
---|
| 990 | get_index_v … t (modulus address 8) ? |
---|
| 991 | ] |
---|
| 992 | | N_BIT_ADDR n ⇒ |
---|
| 993 | λn_bit_addr: True. |
---|
| 994 | let 〈bit_1, seven_bits〉 ≝ vsplit … 1 7 n in |
---|
| 995 | match head' … bit_1 with |
---|
| 996 | [ true ⇒ |
---|
| 997 | let address ≝ nat_of_bitvector … seven_bits in |
---|
| 998 | let d ≝ address ÷ 8 in |
---|
| 999 | let m ≝ address mod 8 in |
---|
| 1000 | let trans ≝ bitvector_of_nat 8 ((d * 8) + 128) in |
---|
| 1001 | let sfr ≝ get_bit_addressable_sfr ?? s trans l in |
---|
| 1002 | ¬(get_index_v … sfr m ?) |
---|
| 1003 | | false ⇒ |
---|
| 1004 | let address ≝ nat_of_bitvector … seven_bits in |
---|
| 1005 | let address' ≝ bitvector_of_nat 7 ((address ÷ 8) + 32) in |
---|
| 1006 | let t ≝ lookup … 7 address' (low_internal_ram ?? s) (zero 8) in |
---|
| 1007 | ¬(get_index_v … t (modulus address 8) ?) |
---|
| 1008 | ] |
---|
| 1009 | | CARRY ⇒ λcarry: True. get_cy_flag ?? s |
---|
| 1010 | | _ ⇒ λother. |
---|
| 1011 | match other in False with [ ] |
---|
| 1012 | ] (subaddressing_modein … a)) normalize nodelta |
---|
| 1013 | try @modulus_less_than |
---|
[2173] | 1014 | #M #sigma #policy #s' #s_refl <s_refl |
---|
[2171] | 1015 | [1: |
---|
[2173] | 1016 | #_ >(get_cy_flag_status_of_pseudo_status … (refl …)) % |
---|
[2171] | 1017 | |2,4: |
---|
| 1018 | whd in ⊢ (% → ?); >p normalize nodelta >p1 normalize nodelta |
---|
[2173] | 1019 | >(get_bit_addressable_sfr_status_of_pseudo_status … (refl …)) #map_address_assm |
---|
[2171] | 1020 | >map_address_assm % |
---|
| 1021 | |3,5: |
---|
| 1022 | whd in ⊢ (% → ?); >p normalize nodelta >p1 normalize nodelta |
---|
| 1023 | whd in match status_of_pseudo_status; normalize nodelta |
---|
| 1024 | >(lookup_low_internal_ram_of_pseudo_low_internal_ram … sigma) |
---|
| 1025 | #map_address_assm >map_address_assm % |
---|
| 1026 | ] |
---|
| 1027 | qed. |
---|
| 1028 | |
---|
| 1029 | lemma get_arg_1_status_of_pseudo_status: |
---|
| 1030 | ∀cm. |
---|
| 1031 | ∀ps. |
---|
| 1032 | ∀addr: [[bit_addr; n_bit_addr; carry]]. |
---|
| 1033 | ∀l. |
---|
[2173] | 1034 | ∀M. ∀sigma. ∀policy. ∀s'. |
---|
| 1035 | status_of_pseudo_status M cm ps sigma policy = s' → |
---|
[2171] | 1036 | map_bit_address_mode_using_internal_pseudo_address_map_get M cm ps sigma addr l → |
---|
| 1037 | get_arg_1 (BitVectorTrie Byte 16) (code_memory_of_pseudo_assembly_program cm sigma policy) |
---|
[2173] | 1038 | s' addr l = |
---|
[2171] | 1039 | (get_arg_1 … cm ps addr l). |
---|
| 1040 | #cm #ps #addr #l |
---|
| 1041 | cases (get_arg_1_status_of_pseudo_status' cm ps addr l) #_ #assm |
---|
| 1042 | @assm |
---|
| 1043 | qed. |
---|
| 1044 | |
---|
| 1045 | definition map_bit_address_mode_using_internal_pseudo_address_map_set_1 ≝ |
---|
| 1046 | λM: internal_pseudo_address_map. |
---|
| 1047 | λcm: pseudo_assembly_program. |
---|
| 1048 | λs: PreStatus ? cm. |
---|
| 1049 | λsigma: Word → Word. |
---|
| 1050 | λaddr: [[bit_addr; carry]]. |
---|
| 1051 | λv: Bit. |
---|
| 1052 | match addr with |
---|
| 1053 | [ BIT_ADDR b ⇒ |
---|
| 1054 | let 〈bit_1, seven_bits〉 ≝ vsplit bool 1 7 (get_8051_sfr … s SFR_PSW) in |
---|
| 1055 | match head' … bit_1 with |
---|
| 1056 | [ true ⇒ |
---|
| 1057 | let address ≝ nat_of_bitvector … seven_bits in |
---|
| 1058 | let d ≝ address ÷ 8 in |
---|
| 1059 | let m ≝ address mod 8 in |
---|
| 1060 | let t ≝ bitvector_of_nat 8 ((d * 8) + 128) in |
---|
| 1061 | let sfr ≝ get_bit_addressable_sfr … s t true in |
---|
| 1062 | map_address_Byte_using_internal_pseudo_address_map M sigma t sfr = sfr |
---|
| 1063 | | false ⇒ |
---|
| 1064 | let address ≝ nat_of_bitvector … seven_bits in |
---|
| 1065 | let address' ≝ bitvector_of_nat 7 ((address ÷ 8) + 32) in |
---|
| 1066 | let t ≝ lookup ? 7 address' (low_internal_ram ?? s) (zero 8) in |
---|
| 1067 | map_internal_ram_address_using_pseudo_address_map M sigma |
---|
| 1068 | (false:::address') t = t |
---|
| 1069 | ] |
---|
| 1070 | | CARRY ⇒ True |
---|
| 1071 | | _ ⇒ True |
---|
| 1072 | ]. |
---|
| 1073 | |
---|
| 1074 | definition map_bit_address_mode_using_internal_pseudo_address_map_set_2 ≝ |
---|
| 1075 | λM: internal_pseudo_address_map. |
---|
| 1076 | λcm: pseudo_assembly_program. |
---|
| 1077 | λs: PreStatus ? cm. |
---|
| 1078 | λsigma: Word → Word. |
---|
| 1079 | λaddr: [[bit_addr; carry]]. |
---|
| 1080 | λv: Bit. |
---|
| 1081 | match addr with |
---|
| 1082 | [ BIT_ADDR b ⇒ |
---|
| 1083 | let 〈bit_1, seven_bits〉 ≝ vsplit bool 1 7 (get_8051_sfr … s SFR_PSW) in |
---|
| 1084 | match head' … bit_1 with |
---|
| 1085 | [ true ⇒ |
---|
| 1086 | let address ≝ nat_of_bitvector … seven_bits in |
---|
| 1087 | let d ≝ address ÷ 8 in |
---|
| 1088 | let m ≝ address mod 8 in |
---|
| 1089 | let t ≝ bitvector_of_nat 8 ((d * 8) + 128) in |
---|
| 1090 | let sfr ≝ get_bit_addressable_sfr … s t true in |
---|
| 1091 | let new_sfr ≝ set_index … sfr m v ? in |
---|
| 1092 | map_address_Byte_using_internal_pseudo_address_map M sigma new_sfr t = t |
---|
| 1093 | | false ⇒ |
---|
| 1094 | let address ≝ nat_of_bitvector … seven_bits in |
---|
| 1095 | let address' ≝ bitvector_of_nat 7 ((address ÷ 8) + 32) in |
---|
| 1096 | let t ≝ lookup ? 7 address' (low_internal_ram ?? s) (zero 8) in |
---|
| 1097 | let n_bit ≝ set_index … t (modulus address 8) v ? in |
---|
| 1098 | let memory ≝ insert ? 7 address' n_bit (low_internal_ram ?? s) in |
---|
| 1099 | map_internal_ram_address_using_pseudo_address_map M sigma |
---|
| 1100 | (false:::address') n_bit = n_bit |
---|
| 1101 | ] |
---|
| 1102 | | CARRY ⇒ True |
---|
| 1103 | | _ ⇒ True |
---|
| 1104 | ]. |
---|
| 1105 | @modulus_less_than |
---|
| 1106 | qed. |
---|
| 1107 | |
---|
| 1108 | lemma set_arg_1_status_of_pseudo_status: |
---|
| 1109 | ∀cm: pseudo_assembly_program. |
---|
| 1110 | ∀ps: PreStatus pseudo_assembly_program cm. |
---|
| 1111 | ∀addr: [[bit_addr; carry]]. |
---|
| 1112 | ∀b: Bit. |
---|
[2173] | 1113 | Σp: PreStatus … cm. ∀M. ∀sigma. ∀policy. ∀s'. |
---|
| 1114 | status_of_pseudo_status M cm ps sigma policy = s' → |
---|
[2171] | 1115 | map_bit_address_mode_using_internal_pseudo_address_map_set_1 M cm ps sigma addr b → |
---|
| 1116 | map_bit_address_mode_using_internal_pseudo_address_map_set_2 M cm ps sigma addr b → |
---|
| 1117 | set_arg_1 (BitVectorTrie Byte 16) |
---|
| 1118 | (code_memory_of_pseudo_assembly_program cm sigma policy) |
---|
[2173] | 1119 | s' addr b = |
---|
[2171] | 1120 | status_of_pseudo_status M cm (set_arg_1 … cm ps addr b) sigma policy. |
---|
| 1121 | whd in match set_arg_1; normalize nodelta |
---|
| 1122 | whd in match map_bit_address_mode_using_internal_pseudo_address_map_set_1; normalize nodelta |
---|
| 1123 | whd in match map_bit_address_mode_using_internal_pseudo_address_map_set_2; normalize nodelta |
---|
| 1124 | @(let m ≝ pseudo_assembly_program in |
---|
| 1125 | λcm. |
---|
| 1126 | λs: PreStatus m cm. |
---|
| 1127 | λa: [[bit_addr; carry]]. |
---|
| 1128 | λv: Bit. |
---|
| 1129 | match a return λx. bool_to_Prop (is_in ? [[bit_addr ; carry]] x) → Σp. ? with |
---|
| 1130 | [ BIT_ADDR b ⇒ λbit_addr: True. |
---|
| 1131 | let 〈bit_1, seven_bits〉 ≝ vsplit bool 1 7 (get_8051_sfr … s SFR_PSW) in |
---|
| 1132 | match head' … bit_1 with |
---|
| 1133 | [ true ⇒ |
---|
| 1134 | let address ≝ nat_of_bitvector … seven_bits in |
---|
| 1135 | let d ≝ address ÷ 8 in |
---|
| 1136 | let m ≝ address mod 8 in |
---|
| 1137 | let t ≝ bitvector_of_nat 8 ((d * 8) + 128) in |
---|
| 1138 | let sfr ≝ get_bit_addressable_sfr … s t true in |
---|
| 1139 | let new_sfr ≝ set_index … sfr m v ? in |
---|
| 1140 | set_bit_addressable_sfr … s new_sfr t |
---|
| 1141 | | false ⇒ |
---|
| 1142 | let address ≝ nat_of_bitvector … seven_bits in |
---|
| 1143 | let address' ≝ bitvector_of_nat 7 ((address ÷ 8) + 32) in |
---|
| 1144 | let t ≝ lookup ? 7 address' (low_internal_ram ?? s) (zero 8) in |
---|
| 1145 | let n_bit ≝ set_index … t (modulus address 8) v ? in |
---|
| 1146 | let memory ≝ insert ? 7 address' n_bit (low_internal_ram ?? s) in |
---|
| 1147 | set_low_internal_ram … s memory |
---|
| 1148 | ] |
---|
| 1149 | | CARRY ⇒ |
---|
| 1150 | λcarry: True. |
---|
| 1151 | let 〈ignore, seven_bits〉 ≝ vsplit bool 1 7 (get_8051_sfr … s SFR_PSW) in |
---|
| 1152 | let new_psw ≝ v:::seven_bits in |
---|
| 1153 | set_8051_sfr ?? s SFR_PSW new_psw |
---|
| 1154 | | _ ⇒ |
---|
| 1155 | λother: False. |
---|
| 1156 | match other in False with |
---|
| 1157 | [ ] |
---|
| 1158 | ] (subaddressing_modein … a)) normalize nodelta |
---|
[2173] | 1159 | try @modulus_less_than #M #sigma #policy #s' #s_refl <s_refl |
---|
[2171] | 1160 | [1: |
---|
[2173] | 1161 | #_ #_ >(get_8051_sfr_status_of_pseudo_status … (refl …)) |
---|
[2171] | 1162 | whd in match map_address_using_internal_pseudo_address_map; normalize nodelta |
---|
| 1163 | >p normalize nodelta @set_8051_sfr_status_of_pseudo_status % |
---|
| 1164 | |2,3: |
---|
[2173] | 1165 | >(get_8051_sfr_status_of_pseudo_status … (refl …)) |
---|
[2171] | 1166 | whd in match map_address_using_internal_pseudo_address_map; normalize nodelta |
---|
| 1167 | >p normalize nodelta >p1 normalize nodelta |
---|
| 1168 | #map_bit_address_assm_1 #map_bit_address_assm_2 |
---|
| 1169 | [1: |
---|
[2173] | 1170 | >(get_bit_addressable_sfr_status_of_pseudo_status … (refl …)) |
---|
[2171] | 1171 | >map_bit_address_assm_1 |
---|
| 1172 | >(set_bit_addressable_sfr_status_of_pseudo_status cm s … map_bit_address_assm_2) % |
---|
| 1173 | |2: |
---|
| 1174 | whd in match status_of_pseudo_status in ⊢ (??(????%)?); normalize nodelta |
---|
| 1175 | >(lookup_low_internal_ram_of_pseudo_low_internal_ram … sigma) |
---|
| 1176 | >map_bit_address_assm_1 |
---|
| 1177 | >(insert_low_internal_ram_of_pseudo_low_internal_ram … map_bit_address_assm_2) |
---|
| 1178 | >set_low_internal_ram_status_of_pseudo_status in ⊢ (??%?); % |
---|
| 1179 | ] |
---|
| 1180 | ] |
---|
[2172] | 1181 | qed. |
---|
| 1182 | |
---|
| 1183 | lemma clock_status_of_pseudo_status: |
---|
[2173] | 1184 | ∀M,cm,sigma,policy,s,s'. |
---|
| 1185 | (status_of_pseudo_status M cm s sigma policy) = s' → |
---|
[2172] | 1186 | clock … |
---|
| 1187 | (code_memory_of_pseudo_assembly_program cm sigma policy) |
---|
[2173] | 1188 | s' |
---|
[2172] | 1189 | = clock … cm s. |
---|
[2173] | 1190 | #M #cm #sigma #policy #s #s' #s_refl <s_refl // |
---|
[2172] | 1191 | qed. |
---|
| 1192 | |
---|
| 1193 | lemma set_clock_status_of_pseudo_status: |
---|
[2173] | 1194 | ∀M,cm,sigma,policy,s,s',v,v'. |
---|
| 1195 | status_of_pseudo_status M cm s sigma policy = s' → |
---|
| 1196 | v = v' → |
---|
[2172] | 1197 | set_clock … |
---|
| 1198 | (code_memory_of_pseudo_assembly_program cm sigma policy) |
---|
[2173] | 1199 | s' v |
---|
| 1200 | = status_of_pseudo_status M cm (set_clock … cm s v') sigma policy. |
---|
| 1201 | #M #cm #sigma #policy #s #s' #v #v' #s_refl #v_refl <s_refl <v_refl // |
---|
[2165] | 1202 | qed. |
---|