[2160] | 1 | (**************************************************************************) |
---|
| 2 | (* ___ *) |
---|
| 3 | (* ||M|| *) |
---|
| 4 | (* ||A|| A project by Andrea Asperti *) |
---|
| 5 | (* ||T|| *) |
---|
| 6 | (* ||I|| Developers: *) |
---|
| 7 | (* ||T|| The HELM team. *) |
---|
| 8 | (* ||A|| http://helm.cs.unibo.it *) |
---|
| 9 | (* \ / *) |
---|
| 10 | (* \ / This file is distributed under the terms of the *) |
---|
| 11 | (* v GNU General Public License Version 2 *) |
---|
| 12 | (* *) |
---|
| 13 | (**************************************************************************) |
---|
| 14 | |
---|
| 15 | include "ASM/Assembly.ma". |
---|
| 16 | include "ASM/Interpret.ma". |
---|
| 17 | include "ASM/StatusProofs.ma". |
---|
| 18 | include alias "arithmetics/nat.ma". |
---|
| 19 | include "ASM/AssemblyProof.ma". |
---|
| 20 | |
---|
| 21 | lemma set_program_counter_status_of_pseudo_status: |
---|
| 22 | ∀M. |
---|
| 23 | ∀cm. |
---|
| 24 | ∀ps. |
---|
| 25 | ∀sigma. |
---|
| 26 | ∀policy. |
---|
| 27 | ∀new_ppc. |
---|
| 28 | set_program_counter (BitVectorTrie Byte 16) |
---|
| 29 | (code_memory_of_pseudo_assembly_program cm sigma policy) |
---|
| 30 | (status_of_pseudo_status M cm ps sigma policy) |
---|
| 31 | (sigma new_ppc) = |
---|
| 32 | status_of_pseudo_status M cm (set_program_counter … cm ps new_ppc) sigma policy. |
---|
| 33 | // |
---|
| 34 | qed. |
---|
| 35 | |
---|
| 36 | lemma set_p1_latch_status_of_pseudo_status: |
---|
| 37 | ∀M. |
---|
| 38 | ∀code_memory. |
---|
| 39 | ∀sigma. |
---|
| 40 | ∀policy. |
---|
| 41 | ∀s. |
---|
| 42 | ∀v. |
---|
| 43 | set_p1_latch (BitVectorTrie Byte 16) |
---|
| 44 | (code_memory_of_pseudo_assembly_program code_memory sigma policy) |
---|
| 45 | (status_of_pseudo_status M code_memory s sigma policy) v = |
---|
| 46 | status_of_pseudo_status M code_memory |
---|
| 47 | (set_p1_latch pseudo_assembly_program code_memory s v) sigma policy. |
---|
| 48 | // |
---|
| 49 | qed. |
---|
| 50 | |
---|
| 51 | lemma set_p3_latch_status_of_pseudo_status: |
---|
| 52 | ∀M. |
---|
| 53 | ∀code_memory. |
---|
| 54 | ∀sigma. |
---|
| 55 | ∀policy. |
---|
| 56 | ∀s. |
---|
| 57 | ∀v. |
---|
| 58 | set_p3_latch (BitVectorTrie Byte 16) |
---|
| 59 | (code_memory_of_pseudo_assembly_program code_memory sigma policy) |
---|
| 60 | (status_of_pseudo_status M code_memory s sigma policy) v = |
---|
| 61 | status_of_pseudo_status M code_memory |
---|
| 62 | (set_p3_latch pseudo_assembly_program code_memory s v) sigma policy. |
---|
| 63 | // |
---|
| 64 | qed. |
---|
| 65 | |
---|
| 66 | definition map_acc_a_using_internal_pseudo_address_map: |
---|
| 67 | ∀M: internal_pseudo_address_map. (Word → Word) → Byte → Byte ≝ |
---|
| 68 | λM, sigma, v. |
---|
| 69 | match \snd M with |
---|
| 70 | [ data ⇒ v |
---|
| 71 | | address upper_lower word ⇒ |
---|
| 72 | let mapped ≝ sigma word in |
---|
| 73 | let 〈high, low〉 ≝ vsplit bool 8 8 mapped in |
---|
| 74 | if eq_upper_lower upper_lower upper then |
---|
| 75 | high |
---|
| 76 | else |
---|
| 77 | low |
---|
| 78 | ]. |
---|
| 79 | |
---|
[2164] | 80 | (*CSC: Taken from AssemblyProofSplit.ma; there named map_lower_internal... *) |
---|
| 81 | definition map_internal_ram_address_using_pseudo_address_map: |
---|
| 82 | ∀M: internal_pseudo_address_map. (Word → Word) → Byte → Byte → Byte ≝ |
---|
| 83 | λM: internal_pseudo_address_map. |
---|
| 84 | λsigma: Word → Word. |
---|
| 85 | λaddress: Byte. |
---|
| 86 | λvalue: Byte. |
---|
| 87 | match assoc_list_lookup ?? address (eq_bv …) (\fst M) with |
---|
| 88 | [ None ⇒ value |
---|
| 89 | | Some upper_lower_word ⇒ |
---|
| 90 | let 〈upper_lower, word〉 ≝ upper_lower_word in |
---|
| 91 | let 〈high, low〉 ≝ vsplit bool 8 8 (sigma word) in |
---|
| 92 | if eq_upper_lower upper_lower upper then |
---|
| 93 | high |
---|
| 94 | else |
---|
| 95 | low |
---|
| 96 | ]. |
---|
| 97 | |
---|
[2160] | 98 | definition map_address_using_internal_pseudo_address_map: |
---|
| 99 | ∀M: internal_pseudo_address_map. (Word → Word) → SFR8051 → Byte → Byte ≝ |
---|
| 100 | λM, sigma, sfr, v. |
---|
| 101 | match sfr with |
---|
| 102 | [ SFR_ACC_A ⇒ map_acc_a_using_internal_pseudo_address_map M sigma v |
---|
| 103 | | _ ⇒ v |
---|
| 104 | ]. |
---|
| 105 | |
---|
| 106 | lemma set_index_set_index_overwrite: |
---|
| 107 | ∀A: Type[0]. |
---|
| 108 | ∀n: nat. |
---|
| 109 | ∀v: Vector A n. |
---|
| 110 | ∀index: nat. |
---|
| 111 | ∀e, e': A. |
---|
| 112 | ∀proof. |
---|
| 113 | ∀proof'. |
---|
| 114 | set_index A n v index e proof = |
---|
| 115 | set_index A n (set_index A n v index e' proof') index e proof. |
---|
| 116 | #A #n #v elim v normalize |
---|
| 117 | [1: |
---|
| 118 | #index #e #e' #absurd cases (lt_to_not_zero … absurd) |
---|
| 119 | |2: |
---|
| 120 | #n' #hd #tl #inductive_hypothesis #index #e #e' cases index #proof #proof' |
---|
| 121 | normalize // |
---|
| 122 | ] |
---|
| 123 | qed. |
---|
| 124 | |
---|
| 125 | lemma set_index_set_index_commutation: |
---|
| 126 | ∀A: Type[0]. |
---|
| 127 | ∀n: nat. |
---|
| 128 | ∀v: Vector A n. |
---|
| 129 | ∀m, o: nat. |
---|
| 130 | ∀m_lt_proof: m < n. |
---|
| 131 | ∀o_lt_proof: o < n. |
---|
| 132 | ∀e, f: A. |
---|
| 133 | m ≠ o → |
---|
| 134 | set_index A n (set_index A n v o f o_lt_proof) m e m_lt_proof = |
---|
| 135 | set_index A n (set_index A n v m e m_lt_proof) o f o_lt_proof. |
---|
| 136 | #A #n #v elim v |
---|
| 137 | [1: |
---|
| 138 | #m #o #m_lt_proof |
---|
| 139 | normalize in m_lt_proof; cases (lt_to_not_zero … m_lt_proof) |
---|
| 140 | |2: |
---|
| 141 | #n' #hd #tl #inductive_hypothesis |
---|
| 142 | #m #o |
---|
| 143 | cases m cases o |
---|
| 144 | [1: |
---|
| 145 | #m_lt_proof #o_lt_proof #e #f #absurd @⊥ cases absurd #relevant |
---|
| 146 | @relevant % |
---|
| 147 | |2,3: |
---|
| 148 | #o' normalize // |
---|
| 149 | |4: |
---|
| 150 | #m' #o' #m_lt_proof #o_lt_proof #e #f #o_neq_m_assm |
---|
| 151 | normalize @eq_f @inductive_hypothesis @nmk #relevant |
---|
| 152 | >relevant in o_neq_m_assm; #relevant @(absurd ?? relevant) % |
---|
| 153 | ] |
---|
| 154 | ] |
---|
| 155 | qed. |
---|
| 156 | |
---|
| 157 | lemma set_index_status_of_pseudo_status: |
---|
| 158 | ∀M, code_memory, sigma, policy, s, sfr, v, v'. |
---|
| 159 | map_address_using_internal_pseudo_address_map M sigma sfr v = v' → |
---|
| 160 | (set_index Byte 19 |
---|
| 161 | (special_function_registers_8051 (BitVectorTrie Byte 16) |
---|
| 162 | (code_memory_of_pseudo_assembly_program code_memory sigma policy) |
---|
| 163 | (status_of_pseudo_status M code_memory s sigma policy)) |
---|
| 164 | (sfr_8051_index sfr) v' (sfr8051_index_19 sfr) |
---|
| 165 | =sfr_8051_of_pseudo_sfr_8051 M |
---|
| 166 | (special_function_registers_8051 pseudo_assembly_program code_memory |
---|
| 167 | (set_8051_sfr pseudo_assembly_program code_memory s sfr v)) sigma). |
---|
| 168 | #M #code_memory #sigma #policy #s #sfr #v #v' #sfr_neq_acc_a_assm |
---|
| 169 | whd in match status_of_pseudo_status; normalize nodelta |
---|
| 170 | whd in match sfr_8051_of_pseudo_sfr_8051; normalize nodelta |
---|
| 171 | inversion (\snd M) try (#upper_lower #address) #sndM_refl normalize nodelta |
---|
| 172 | [1: |
---|
| 173 | <sfr_neq_acc_a_assm cases sfr |
---|
| 174 | [18: |
---|
| 175 | whd in match map_address_using_internal_pseudo_address_map; normalize nodelta |
---|
| 176 | whd in match map_acc_a_using_internal_pseudo_address_map; normalize nodelta |
---|
| 177 | >sndM_refl % |
---|
| 178 | ] |
---|
| 179 | % |
---|
| 180 | |2: |
---|
| 181 | @pair_elim #high #low #high_low_refl normalize nodelta |
---|
| 182 | inversion (eq_upper_lower upper_lower upper) #eq_upper_lower_refl normalize nodelta |
---|
| 183 | <sfr_neq_acc_a_assm cases sfr |
---|
| 184 | [18,37: |
---|
| 185 | whd in match map_address_using_internal_pseudo_address_map; normalize nodelta |
---|
| 186 | whd in match map_acc_a_using_internal_pseudo_address_map; normalize nodelta |
---|
| 187 | >sndM_refl normalize nodelta >high_low_refl normalize nodelta |
---|
| 188 | >eq_upper_lower_refl normalize nodelta |
---|
| 189 | whd in match (set_8051_sfr ?????); |
---|
| 190 | [1: |
---|
| 191 | <set_index_set_index_overwrite in ⊢ (??%?); |
---|
| 192 | <set_index_set_index_overwrite in ⊢ (???%); % |
---|
| 193 | |2: |
---|
| 194 | <set_index_set_index_overwrite in ⊢ (??%?); |
---|
| 195 | <set_index_set_index_overwrite in ⊢ (???%); % |
---|
| 196 | ] |
---|
| 197 | ] |
---|
| 198 | whd in match map_address_using_internal_pseudo_address_map; normalize nodelta |
---|
| 199 | whd in match (set_8051_sfr ?????); @set_index_set_index_commutation normalize |
---|
| 200 | @nmk #absurd destruct(absurd) |
---|
| 201 | ] |
---|
| 202 | qed. |
---|
| 203 | |
---|
| 204 | lemma set_8051_sfr_status_of_pseudo_status: |
---|
[2163] | 205 | ∀M, code_memory, sigma, policy, s, sfr, v,v'. |
---|
| 206 | map_address_using_internal_pseudo_address_map M sigma sfr v = v' → |
---|
[2160] | 207 | (set_8051_sfr (BitVectorTrie Byte 16) |
---|
| 208 | (code_memory_of_pseudo_assembly_program code_memory sigma policy) |
---|
[2163] | 209 | (status_of_pseudo_status M code_memory s sigma policy) sfr v' |
---|
[2160] | 210 | =status_of_pseudo_status M code_memory |
---|
| 211 | (set_8051_sfr pseudo_assembly_program code_memory s sfr v) sigma policy). |
---|
[2163] | 212 | #M #code_memory #sigma #policy #s #sfr #v #v' #v_ok |
---|
| 213 | whd in ⊢ (??%%); @split_eq_status try % /2/ |
---|
| 214 | qed. |
---|
[2160] | 215 | |
---|
[2163] | 216 | lemma set_8052_sfr_status_of_pseudo_status: |
---|
| 217 | ∀M, code_memory, sigma, policy, s, sfr, v. |
---|
| 218 | (set_8052_sfr (BitVectorTrie Byte 16) |
---|
| 219 | (code_memory_of_pseudo_assembly_program code_memory sigma policy) |
---|
| 220 | (status_of_pseudo_status M code_memory s sigma policy) sfr v |
---|
| 221 | =status_of_pseudo_status M code_memory |
---|
| 222 | (set_8052_sfr pseudo_assembly_program code_memory s sfr v) sigma policy). |
---|
| 223 | // |
---|
| 224 | qed. |
---|
| 225 | |
---|
| 226 | definition sfr_of_Byte: Byte → option (SFR8051 + SFR8052) ≝ |
---|
| 227 | λb: Byte. |
---|
| 228 | let address ≝ nat_of_bitvector … b in |
---|
| 229 | if (eqb address 128) then None ? |
---|
| 230 | else if (eqb address 144) then Some … (inl … SFR_P1) |
---|
| 231 | else if (eqb address 160) then None ? |
---|
| 232 | else if (eqb address 176) then Some … (inl … SFR_P3) |
---|
| 233 | else if (eqb address 153) then Some … (inl … SFR_SBUF) |
---|
| 234 | else if (eqb address 138) then Some … (inl … SFR_TL0) |
---|
| 235 | else if (eqb address 139) then Some … (inl … SFR_TL1) |
---|
| 236 | else if (eqb address 140) then Some … (inl … SFR_TH0) |
---|
| 237 | else if (eqb address 141) then Some … (inl … SFR_TH1) |
---|
| 238 | else if (eqb address 200) then Some … (inr … SFR_T2CON) |
---|
| 239 | else if (eqb address 202) then Some … (inr … SFR_RCAP2L) |
---|
| 240 | else if (eqb address 203) then Some … (inr … SFR_RCAP2H) |
---|
| 241 | else if (eqb address 204) then Some … (inr … SFR_TL2) |
---|
| 242 | else if (eqb address 205) then Some … (inr … SFR_TH2) |
---|
| 243 | else if (eqb address 135) then Some … (inl … SFR_PCON) |
---|
| 244 | else if (eqb address 136) then Some … (inl … SFR_TCON) |
---|
| 245 | else if (eqb address 137) then Some … (inl … SFR_TMOD) |
---|
| 246 | else if (eqb address 152) then Some … (inl … SFR_SCON) |
---|
| 247 | else if (eqb address 168) then Some … (inl … SFR_IE) |
---|
| 248 | else if (eqb address 184) then Some … (inl … SFR_IP) |
---|
| 249 | else if (eqb address 129) then Some … (inl … SFR_SP) |
---|
| 250 | else if (eqb address 130) then Some … (inl … SFR_DPL) |
---|
| 251 | else if (eqb address 131) then Some … (inl … SFR_DPH) |
---|
| 252 | else if (eqb address 208) then Some … (inl … SFR_PSW) |
---|
| 253 | else if (eqb address 224) then Some … (inl … SFR_ACC_A) |
---|
| 254 | else if (eqb address 240) then Some … (inl … SFR_ACC_B) |
---|
| 255 | else None ?. |
---|
| 256 | |
---|
[2160] | 257 | definition set_bit_addressable_sfr: |
---|
| 258 | ∀M: Type[0]. ∀code_memory: M. ∀s: PreStatus M code_memory. Byte → Byte → |
---|
| 259 | PreStatus M code_memory ≝ |
---|
| 260 | λM: Type[0]. |
---|
| 261 | λcode_memory:M. |
---|
| 262 | λs: PreStatus M code_memory. |
---|
| 263 | λb: Byte. |
---|
| 264 | λv: Byte. |
---|
[2163] | 265 | match sfr_of_Byte b with |
---|
| 266 | [ None ⇒ match not_implemented in False with [ ] |
---|
| 267 | | Some sfr8051_8052 ⇒ |
---|
| 268 | match sfr8051_8052 with |
---|
| 269 | [ inl sfr ⇒ |
---|
| 270 | match sfr with |
---|
| 271 | [ SFR_P1 ⇒ |
---|
| 272 | let status_1 ≝ set_8051_sfr ?? s SFR_P1 v in |
---|
| 273 | set_p1_latch ?? s v |
---|
| 274 | | SFR_P3 ⇒ |
---|
| 275 | let status_1 ≝ set_8051_sfr ?? s SFR_P3 v in |
---|
| 276 | set_p3_latch ?? s v |
---|
| 277 | | _ ⇒ set_8051_sfr ?? s sfr v ] |
---|
| 278 | | inr sfr ⇒ set_8052_sfr ?? s sfr v ]]. |
---|
[2160] | 279 | |
---|
[2163] | 280 | definition map_address_Byte_using_internal_pseudo_address_map ≝ |
---|
| 281 | λM,sigma,d,v. |
---|
| 282 | match sfr_of_Byte d with |
---|
| 283 | [ None ⇒ v |
---|
| 284 | | Some sfr8051_8052 ⇒ |
---|
| 285 | match sfr8051_8052 with |
---|
| 286 | [ inl sfr ⇒ |
---|
| 287 | map_address_using_internal_pseudo_address_map M sigma sfr v |
---|
| 288 | | inr _ ⇒ v ]]. |
---|
| 289 | |
---|
| 290 | lemma set_bit_addressable_sfr_status_of_pseudo_status': |
---|
[2160] | 291 | let M ≝ pseudo_assembly_program in ∀code_memory: M. ∀s: PreStatus M code_memory. ∀d: Byte. ∀v: Byte. |
---|
[2163] | 292 | Σp: PreStatus M code_memory. ∀M. ∀sigma. ∀policy. ∀v'. |
---|
| 293 | map_address_Byte_using_internal_pseudo_address_map M sigma d v = v' → |
---|
[2160] | 294 | (set_bit_addressable_sfr (BitVectorTrie Byte 16) |
---|
| 295 | (code_memory_of_pseudo_assembly_program code_memory sigma policy) |
---|
[2163] | 296 | (status_of_pseudo_status M code_memory s sigma policy) d v' |
---|
[2160] | 297 | =status_of_pseudo_status M code_memory |
---|
| 298 | (set_bit_addressable_sfr pseudo_assembly_program code_memory s d v) sigma policy). |
---|
[2163] | 299 | whd in match set_bit_addressable_sfr; |
---|
| 300 | whd in match map_address_Byte_using_internal_pseudo_address_map; |
---|
| 301 | normalize nodelta |
---|
[2160] | 302 | @(let M ≝ pseudo_assembly_program in |
---|
| 303 | λcode_memory:M. |
---|
| 304 | λs: PreStatus M code_memory. |
---|
| 305 | λb: Byte. |
---|
| 306 | λv: Byte. |
---|
[2163] | 307 | match sfr_of_Byte b with |
---|
| 308 | [ None ⇒ match not_implemented in False with [ ] |
---|
| 309 | | Some sfr8051_8052 ⇒ |
---|
| 310 | match sfr8051_8052 with |
---|
| 311 | [ inl sfr ⇒ |
---|
| 312 | match sfr with |
---|
| 313 | [ SFR_P1 ⇒ |
---|
| 314 | let status_1 ≝ set_8051_sfr ?? s SFR_P1 v in |
---|
| 315 | set_p1_latch ?? s v |
---|
| 316 | | SFR_P3 ⇒ |
---|
| 317 | let status_1 ≝ set_8051_sfr ?? s SFR_P3 v in |
---|
| 318 | set_p3_latch ?? s v |
---|
| 319 | | _ ⇒ set_8051_sfr ?? s sfr v ] |
---|
| 320 | | inr sfr ⇒ set_8052_sfr ?? s sfr v ]]) |
---|
| 321 | normalize nodelta |
---|
| 322 | /2 by refl, set_8051_sfr_status_of_pseudo_status, set_8052_sfr_status_of_pseudo_status/ |
---|
| 323 | whd in match map_address_using_internal_pseudo_address_map; normalize nodelta // |
---|
| 324 | qed. |
---|
[2160] | 325 | |
---|
[2163] | 326 | lemma set_bit_addressable_sfr_status_of_pseudo_status: |
---|
| 327 | ∀code_memory: pseudo_assembly_program. ∀s: PreStatus … code_memory. ∀d: Byte. ∀v: Byte. |
---|
| 328 | ∀M. ∀sigma. ∀policy. ∀v'. |
---|
| 329 | map_address_Byte_using_internal_pseudo_address_map M sigma d v = v' → |
---|
| 330 | (set_bit_addressable_sfr (BitVectorTrie Byte 16) |
---|
| 331 | (code_memory_of_pseudo_assembly_program code_memory sigma policy) |
---|
| 332 | (status_of_pseudo_status M code_memory s sigma policy) d v' |
---|
| 333 | =status_of_pseudo_status M code_memory |
---|
| 334 | (set_bit_addressable_sfr pseudo_assembly_program code_memory s d v) sigma policy). |
---|
| 335 | #code #s #d #v cases (set_bit_addressable_sfr_status_of_pseudo_status' code s d v) #_ |
---|
| 336 | #H @H |
---|
| 337 | qed. |
---|
| 338 | |
---|
[2164] | 339 | lemma set_low_internal_ram_status_of_pseudo_status: |
---|
[2163] | 340 | ∀cm,sigma,policy,M,s,ram. |
---|
| 341 | set_low_internal_ram (BitVectorTrie Byte 16) |
---|
| 342 | (code_memory_of_pseudo_assembly_program cm sigma policy) |
---|
| 343 | (status_of_pseudo_status M cm s sigma policy) |
---|
| 344 | (low_internal_ram_of_pseudo_low_internal_ram M ram) |
---|
| 345 | = status_of_pseudo_status M cm |
---|
| 346 | (set_low_internal_ram pseudo_assembly_program cm s ram) sigma policy. |
---|
| 347 | // |
---|
| 348 | qed. |
---|
[2164] | 349 | |
---|
| 350 | (* Real axiom ATM *) |
---|
| 351 | axiom insert_low_internal_ram_of_pseudo_low_internal_ram: |
---|
| 352 | ∀M,sigma,cm,s,addr,v,v'. |
---|
| 353 | map_internal_ram_address_using_pseudo_address_map M sigma (false:::addr) v = v' → |
---|
| 354 | insert Byte 7 addr v' |
---|
| 355 | (low_internal_ram_of_pseudo_low_internal_ram M |
---|
| 356 | (low_internal_ram pseudo_assembly_program cm s)) |
---|
| 357 | =low_internal_ram_of_pseudo_low_internal_ram M |
---|
| 358 | (insert Byte 7 addr v (low_internal_ram pseudo_assembly_program cm s)). |
---|
[2163] | 359 | |
---|
[2164] | 360 | lemma insert_low_internal_ram_status_of_pseudo_status: |
---|
| 361 | ∀M,cm,sigma,policy,s,addr,v,v'. |
---|
| 362 | map_internal_ram_address_using_pseudo_address_map M sigma (false:::addr) v = v' → |
---|
| 363 | insert Byte 7 addr v' |
---|
[2163] | 364 | (low_internal_ram (BitVectorTrie Byte 16) |
---|
| 365 | (code_memory_of_pseudo_assembly_program cm sigma policy) |
---|
| 366 | (status_of_pseudo_status M cm s sigma policy)) |
---|
| 367 | = low_internal_ram_of_pseudo_low_internal_ram M |
---|
| 368 | (insert Byte 7 addr v |
---|
| 369 | (low_internal_ram pseudo_assembly_program cm s)). |
---|
[2164] | 370 | /2 by insert_low_internal_ram_of_pseudo_low_internal_ram/ |
---|
| 371 | qed. |
---|
[2163] | 372 | |
---|
[2164] | 373 | (*CSC: Taken from AssemblyProofSplit *) |
---|
| 374 | lemma get_index_v_set_index_miss: |
---|
| 375 | ∀T: Type[0]. |
---|
| 376 | ∀n, i, j: nat. |
---|
| 377 | ∀v: Vector T n. |
---|
| 378 | ∀b: T. |
---|
| 379 | ∀i_proof: i < n. |
---|
| 380 | ∀j_proof: j < n. |
---|
| 381 | i ≠ j → |
---|
| 382 | get_index_v T n (set_index T n v i b i_proof) j j_proof = |
---|
| 383 | get_index_v T n v j j_proof. |
---|
| 384 | #T #n #i #j #v lapply i lapply j elim v #i #j |
---|
| 385 | [1: |
---|
| 386 | #b #i_proof |
---|
| 387 | cases (lt_to_not_zero … i_proof) |
---|
| 388 | |2: |
---|
| 389 | #tl #inductive_hypothesis #j' #i' #b #i_proof #j_proof #i_neq_j |
---|
| 390 | lapply i_proof lapply i_neq_j cases i' |
---|
| 391 | [1: |
---|
| 392 | -i_neq_j #i_neq_j -i_proof #i_proof |
---|
| 393 | whd in match (set_index ??????); |
---|
| 394 | lapply j_proof lapply i_neq_j cases j' |
---|
| 395 | [1: |
---|
| 396 | #relevant @⊥ cases relevant -relevant #absurd @absurd % |
---|
| 397 | |2: |
---|
| 398 | #j' #_ -j_proof #j_proof % |
---|
| 399 | ] |
---|
| 400 | |2: |
---|
| 401 | #i' -i_neq_j #i_neq_j -i_proof #i_proof |
---|
| 402 | lapply j_proof lapply i_neq_j cases j' |
---|
| 403 | [1: |
---|
| 404 | #_ #j_proof % |
---|
| 405 | |2: |
---|
| 406 | #j' #i_neq_j #j_proof |
---|
| 407 | @inductive_hypothesis @nmk #relevant |
---|
| 408 | cases i_neq_j #absurd @absurd >relevant % |
---|
| 409 | ] |
---|
| 410 | ] |
---|
| 411 | ] |
---|
| 412 | qed. |
---|
| 413 | |
---|
| 414 | lemma get_8051_sfr_status_of_pseudo_status: |
---|
| 415 | ∀M,cm,s,sigma,policy,sfr. |
---|
| 416 | get_8051_sfr … |
---|
| 417 | (code_memory_of_pseudo_assembly_program cm sigma policy) |
---|
| 418 | (status_of_pseudo_status M cm s sigma policy) sfr = |
---|
| 419 | map_address_using_internal_pseudo_address_map M sigma sfr |
---|
| 420 | (get_8051_sfr … cm s sfr). |
---|
| 421 | #M #cm #s #sigma #policy #sfr whd in ⊢ (??%%); |
---|
| 422 | whd in match status_of_pseudo_status; normalize nodelta |
---|
| 423 | whd in match sfr_8051_of_pseudo_sfr_8051; normalize nodelta |
---|
| 424 | whd in match map_acc_a_using_internal_pseudo_address_map; normalize nodelta |
---|
| 425 | cases (\snd M) normalize nodelta [cases sfr %] |
---|
| 426 | #map_mem #map_acc @pair_elim #high #low #_ normalize nodelta |
---|
| 427 | cases (eq_upper_lower ??) normalize nodelta cases sfr normalize nodelta |
---|
| 428 | [18,37: @get_index_v_set_index |
---|
| 429 | |*: >get_index_v_set_index_miss % normalize #abs destruct] |
---|
| 430 | qed. |
---|
| 431 | |
---|
| 432 | lemma bit_address_of_register_status_of_pseudo_status: |
---|
| 433 | ∀M,cm,s,sigma,policy,r. |
---|
| 434 | bit_address_of_register … |
---|
| 435 | (code_memory_of_pseudo_assembly_program cm sigma policy) |
---|
| 436 | (status_of_pseudo_status M cm s sigma policy) r = |
---|
| 437 | bit_address_of_register … cm s r. |
---|
| 438 | #M #cm #s #sigma #policy #r whd in ⊢ (??%%); |
---|
| 439 | >get_8051_sfr_status_of_pseudo_status |
---|
| 440 | @pair_elim #un #ln #_ |
---|
| 441 | @pair_elim #r1 #r0 #_ % |
---|
| 442 | qed. |
---|
| 443 | |
---|
| 444 | (*CSC: provable using the axiom in AssemblyProof, but this one seems more |
---|
| 445 | primitive *) |
---|
| 446 | axiom lookup_low_internal_ram_of_pseudo_low_internal_ram: |
---|
| 447 | ∀M,sigma,cm,s,addr. |
---|
| 448 | lookup Byte 7 addr |
---|
| 449 | (low_internal_ram_of_pseudo_low_internal_ram M |
---|
| 450 | (low_internal_ram pseudo_assembly_program cm s)) (zero 8) |
---|
| 451 | = |
---|
| 452 | map_internal_ram_address_using_pseudo_address_map M sigma (false:::addr) |
---|
| 453 | (lookup Byte 7 addr |
---|
| 454 | (low_internal_ram pseudo_assembly_program cm s) (zero 8)). |
---|
| 455 | |
---|
| 456 | lemma get_register_status_of_pseudo_status: |
---|
| 457 | ∀M,cm,sigma,policy,s,r. |
---|
| 458 | get_register … |
---|
| 459 | (code_memory_of_pseudo_assembly_program cm sigma policy) |
---|
| 460 | (status_of_pseudo_status M cm s sigma policy) r = |
---|
| 461 | map_internal_ram_address_using_pseudo_address_map M sigma (false:::bit_address_of_register pseudo_assembly_program cm s r) |
---|
| 462 | (get_register … cm s r). |
---|
| 463 | #M #cm #sigma #policy #s #r whd in match get_register; normalize nodelta |
---|
| 464 | whd in match status_of_pseudo_status; normalize nodelta |
---|
| 465 | >bit_address_of_register_status_of_pseudo_status |
---|
| 466 | @lookup_low_internal_ram_of_pseudo_low_internal_ram |
---|
| 467 | qed. |
---|
| 468 | |
---|
[2165] | 469 | lemma external_ram_status_of_pseudo_status: |
---|
| 470 | ∀M,cm,s,sigma,policy. |
---|
| 471 | external_ram … |
---|
| 472 | (code_memory_of_pseudo_assembly_program cm sigma policy) |
---|
| 473 | (status_of_pseudo_status M cm s sigma policy) = |
---|
| 474 | external_ram … cm s. |
---|
| 475 | // |
---|
| 476 | qed. |
---|
| 477 | |
---|
| 478 | lemma set_external_ram_status_of_pseudo_status: |
---|
| 479 | ∀M,cm,ps,sigma,policy,ram. |
---|
| 480 | set_external_ram … |
---|
| 481 | (code_memory_of_pseudo_assembly_program cm sigma policy) |
---|
| 482 | (status_of_pseudo_status M cm ps sigma policy) |
---|
| 483 | ram = |
---|
| 484 | status_of_pseudo_status M cm (set_external_ram … cm ps ram) sigma policy. |
---|
| 485 | // |
---|
| 486 | qed. |
---|
| 487 | |
---|
[2164] | 488 | definition map_address_mode_using_internal_pseudo_address_map_ok ≝ |
---|
| 489 | λM,sigma,cm.λs:PreStatus ? cm.λaddr,v,v'. |
---|
[2163] | 490 | match addr with |
---|
| 491 | [ DIRECT d ⇒ |
---|
[2164] | 492 | let 〈 bit_one, seven_bits 〉 as vsplit_refl ≝ vsplit … 1 7 d in |
---|
| 493 | match head' … bit_one with |
---|
[2163] | 494 | [ true ⇒ |
---|
[2164] | 495 | map_address_Byte_using_internal_pseudo_address_map M sigma (true:::seven_bits) v |
---|
| 496 | | false ⇒ |
---|
| 497 | map_internal_ram_address_using_pseudo_address_map M sigma (false:::seven_bits) v ] = v' |
---|
| 498 | | INDIRECT i ⇒ |
---|
| 499 | assoc_list_lookup ?? |
---|
| 500 | (false:::bit_address_of_register pseudo_assembly_program cm s [[false; false; i]]) (eq_bv …) (\fst M) = None … ∧ |
---|
| 501 | let register ≝ get_register ?? s [[ false; false; i ]] in |
---|
| 502 | map_internal_ram_address_using_pseudo_address_map M sigma register v = v' |
---|
[2165] | 503 | | EXT_INDIRECT e ⇒ |
---|
| 504 | assoc_list_lookup ?? |
---|
| 505 | (false:::bit_address_of_register pseudo_assembly_program cm s [[false; false; e]]) (eq_bv …) (\fst M) = None … ∧ |
---|
| 506 | v = v' |
---|
[2164] | 507 | | _ ⇒ v = v']. |
---|
[2163] | 508 | |
---|
[2160] | 509 | definition set_arg_8: ∀M: Type[0]. ∀code_memory:M. ∀s:PreStatus M code_memory. ∀addr: [[ direct ; indirect ; registr ; |
---|
| 510 | acc_a ; acc_b ; ext_indirect ; |
---|
| 511 | ext_indirect_dptr ]]. Byte → PreStatus M code_memory ≝ |
---|
| 512 | λm, cm, s, a, v. |
---|
| 513 | match a return λx. bool_to_Prop (is_in ? [[ direct ; indirect ; registr ; |
---|
| 514 | acc_a ; acc_b ; ext_indirect ; |
---|
| 515 | ext_indirect_dptr ]] x) → |
---|
| 516 | PreStatus m cm |
---|
| 517 | with |
---|
| 518 | [ DIRECT d ⇒ |
---|
| 519 | λdirect: True. |
---|
[2164] | 520 | let 〈 bit_one, seven_bits 〉 ≝ vsplit ? 1 7 d in |
---|
| 521 | match head' … bit_one with |
---|
| 522 | [ true ⇒ set_bit_addressable_sfr ?? s (true:::seven_bits) v |
---|
[2160] | 523 | | false ⇒ |
---|
[2164] | 524 | let memory ≝ insert ? 7 seven_bits v (low_internal_ram ?? s) in |
---|
[2160] | 525 | set_low_internal_ram ?? s memory |
---|
| 526 | ] |
---|
| 527 | | INDIRECT i ⇒ |
---|
| 528 | λindirect: True. |
---|
| 529 | let register ≝ get_register ?? s [[ false; false; i ]] in |
---|
[2164] | 530 | let 〈bit_one, seven_bits〉 ≝ vsplit ? 1 7 register in |
---|
| 531 | match head' … bit_one with |
---|
[2160] | 532 | [ false ⇒ |
---|
[2164] | 533 | let memory ≝ insert … seven_bits v (low_internal_ram ?? s) in |
---|
[2160] | 534 | set_low_internal_ram ?? s memory |
---|
| 535 | | true ⇒ |
---|
[2164] | 536 | let memory ≝ insert … seven_bits v (high_internal_ram ?? s) in |
---|
[2160] | 537 | set_high_internal_ram ?? s memory |
---|
| 538 | ] |
---|
| 539 | | REGISTER r ⇒ λregister: True. set_register ?? s r v |
---|
| 540 | | ACC_A ⇒ λacc_a: True. set_8051_sfr ?? s SFR_ACC_A v |
---|
| 541 | | ACC_B ⇒ λacc_b: True. set_8051_sfr ?? s SFR_ACC_B v |
---|
| 542 | | EXT_INDIRECT e ⇒ |
---|
| 543 | λext_indirect: True. |
---|
| 544 | let address ≝ get_register ?? s [[ false; false; e ]] in |
---|
| 545 | let padded_address ≝ pad 8 8 address in |
---|
| 546 | let memory ≝ insert ? 16 padded_address v (external_ram ?? s) in |
---|
| 547 | set_external_ram ?? s memory |
---|
| 548 | | EXT_INDIRECT_DPTR ⇒ |
---|
| 549 | λext_indirect_dptr: True. |
---|
| 550 | let address ≝ (get_8051_sfr ?? s SFR_DPH) @@ (get_8051_sfr ?? s SFR_DPL) in |
---|
| 551 | let memory ≝ insert ? 16 address v (external_ram ?? s) in |
---|
| 552 | set_external_ram ?? s memory |
---|
| 553 | | _ ⇒ |
---|
| 554 | λother: False. |
---|
| 555 | match other in False with [ ] |
---|
| 556 | ] (subaddressing_modein … a). |
---|
[2164] | 557 | |
---|
| 558 | (*CSC: move elsewhere*) |
---|
| 559 | lemma eq_head': ∀A,n,v. v = head' A n v ::: tail … v. |
---|
| 560 | #A #n #v inversion v in ⊢ ?; |
---|
| 561 | [ #abs @⊥ lapply (jmeq_to_eq ??? abs) /2/ |
---|
| 562 | | #m #hd #tl #_ #EQ <(injective_S … EQ) in tl; #tl #EQ' >EQ' % ] |
---|
[2160] | 563 | qed. |
---|
| 564 | |
---|
[2164] | 565 | (*CSC: move elsewhere*) |
---|
| 566 | lemma tail_singleton: ∀A,v. tail A 0 v = [[]]. |
---|
| 567 | #A #v inversion v in ⊢ ?; |
---|
| 568 | [ #abs @⊥ lapply (jmeq_to_eq ??? abs) #H destruct(H) |
---|
| 569 | | #n #hd #tl #_ #EQ <(injective_S … EQ) in tl; #tl #EQ1 >EQ1 normalize |
---|
| 570 | /2 by jmeq_to_eq/ |
---|
| 571 | ] |
---|
| 572 | qed. |
---|
| 573 | |
---|
| 574 | (*CSC: move elsewhere*) |
---|
| 575 | lemma eq_cons_head_append: |
---|
| 576 | ∀A,n.∀hd: Vector A 1. ∀tl: Vector A n. |
---|
| 577 | head' A 0 hd:::tl = hd@@tl. |
---|
| 578 | #A #n #hd #tl >(eq_head' … hd) >tail_singleton % |
---|
| 579 | qed. |
---|
| 580 | |
---|
[2160] | 581 | lemma set_arg_8_status_of_pseudo_status: |
---|
| 582 | ∀cm. |
---|
| 583 | ∀ps. |
---|
[2163] | 584 | ∀addr:[[ direct ; indirect ; registr ; acc_a ; acc_b ; ext_indirect ; ext_indirect_dptr ]]. |
---|
| 585 | ∀value. Σp: PreStatus ? cm. ∀M. ∀sigma. ∀policy. ∀value'. |
---|
[2164] | 586 | map_address_mode_using_internal_pseudo_address_map_ok … M sigma cm ps addr value value' → |
---|
[2160] | 587 | set_arg_8 (BitVectorTrie Byte 16) |
---|
| 588 | (code_memory_of_pseudo_assembly_program cm sigma policy) |
---|
| 589 | (status_of_pseudo_status M cm ps sigma policy) |
---|
[2163] | 590 | addr value' = |
---|
[2160] | 591 | status_of_pseudo_status M cm (set_arg_8 … cm ps addr value) sigma policy. |
---|
[2163] | 592 | whd in match set_arg_8; normalize nodelta |
---|
[2160] | 593 | @(let m ≝ pseudo_assembly_program in λcm, s. λa: [[ direct ; indirect ; registr ; |
---|
| 594 | acc_a ; acc_b ; ext_indirect ; |
---|
| 595 | ext_indirect_dptr ]]. λv. |
---|
| 596 | match a return λaddr. bool_to_Prop (is_in ? [[ direct ; indirect ; registr ; |
---|
| 597 | acc_a ; acc_b ; ext_indirect ; |
---|
| 598 | ext_indirect_dptr ]] addr) → |
---|
[2163] | 599 | Σp.? |
---|
[2160] | 600 | with |
---|
| 601 | [ DIRECT d ⇒ |
---|
| 602 | λdirect: True. |
---|
[2164] | 603 | deplet 〈 bit_one, seven_bits 〉 as vsplit_refl ≝ vsplit ? 1 7 d in |
---|
| 604 | match head' … bit_one with |
---|
| 605 | [ true ⇒ set_bit_addressable_sfr ?? s (true:::seven_bits) v |
---|
[2160] | 606 | | false ⇒ |
---|
[2164] | 607 | let memory ≝ insert ? 7 seven_bits v (low_internal_ram ?? s) in |
---|
[2160] | 608 | set_low_internal_ram ?? s memory |
---|
| 609 | ] |
---|
| 610 | | INDIRECT i ⇒ |
---|
| 611 | λindirect: True. |
---|
| 612 | let register ≝ get_register ?? s [[ false; false; i ]] in |
---|
[2164] | 613 | let 〈bit_one, seven_bits〉 ≝ vsplit ? 1 7 register in |
---|
| 614 | match head' … bit_one with |
---|
[2160] | 615 | [ false ⇒ |
---|
[2164] | 616 | let memory ≝ insert … seven_bits v (low_internal_ram ?? s) in |
---|
[2160] | 617 | set_low_internal_ram ?? s memory |
---|
| 618 | | true ⇒ |
---|
[2164] | 619 | let memory ≝ insert … seven_bits v (high_internal_ram ?? s) in |
---|
[2160] | 620 | set_high_internal_ram ?? s memory |
---|
| 621 | ] |
---|
| 622 | | REGISTER r ⇒ λregister: True. set_register ?? s r v |
---|
| 623 | | ACC_A ⇒ λacc_a: True. set_8051_sfr ?? s SFR_ACC_A v |
---|
| 624 | | ACC_B ⇒ λacc_b: True. set_8051_sfr ?? s SFR_ACC_B v |
---|
| 625 | | EXT_INDIRECT e ⇒ |
---|
| 626 | λext_indirect: True. |
---|
| 627 | let address ≝ get_register ?? s [[ false; false; e ]] in |
---|
| 628 | let padded_address ≝ pad 8 8 address in |
---|
| 629 | let memory ≝ insert ? 16 padded_address v (external_ram ?? s) in |
---|
| 630 | set_external_ram ?? s memory |
---|
| 631 | | EXT_INDIRECT_DPTR ⇒ |
---|
| 632 | λext_indirect_dptr: True. |
---|
| 633 | let address ≝ (get_8051_sfr ?? s SFR_DPH) @@ (get_8051_sfr ?? s SFR_DPL) in |
---|
| 634 | let memory ≝ insert ? 16 address v (external_ram ?? s) in |
---|
| 635 | set_external_ram ?? s memory |
---|
| 636 | | _ ⇒ |
---|
| 637 | λother: False. |
---|
| 638 | match other in False with [ ] |
---|
[2163] | 639 | ] (subaddressing_modein … a)) normalize nodelta |
---|
[2164] | 640 | #M #sigma #policy #v' whd in match map_address_mode_using_internal_pseudo_address_map_ok; normalize nodelta |
---|
[2163] | 641 | [1,2: |
---|
| 642 | <vsplit_refl normalize nodelta >p normalize nodelta |
---|
[2164] | 643 | [ >(vsplit_ok … vsplit_refl) @set_bit_addressable_sfr_status_of_pseudo_status |
---|
| 644 | | #v_ok >(insert_low_internal_ram_status_of_pseudo_status … v) // ] |
---|
| 645 | |3,4: * #EQ1 #EQ2 change with (get_register ????) in match register in p; |
---|
| 646 | >get_register_status_of_pseudo_status |
---|
| 647 | whd in match map_internal_ram_address_using_pseudo_address_map; normalize nodelta |
---|
| 648 | >EQ1 normalize nodelta >p normalize nodelta >p1 normalize nodelta |
---|
[2165] | 649 | [ cases daemon (*CSC*) |
---|
[2164] | 650 | | >(insert_low_internal_ram_status_of_pseudo_status … v) // <EQ2 |
---|
| 651 | @eq_f2 try % <(vsplit_ok … (sym_eq … p)) <eq_cons_head_append >p1 % ] |
---|
[2165] | 652 | |5: * #EQ1 #EQ2 <EQ2 >get_register_status_of_pseudo_status |
---|
| 653 | whd in match map_internal_ram_address_using_pseudo_address_map; normalize nodelta |
---|
| 654 | >EQ1 normalize nodelta |
---|
| 655 | >external_ram_status_of_pseudo_status @set_external_ram_status_of_pseudo_status |
---|
| 656 | |6: #EQ <EQ cases daemon (*CSC*) |
---|
| 657 | |7: #EQ <EQ @set_8051_sfr_status_of_pseudo_status cases daemon (*CSC*) |
---|
| 658 | |8: #EQ <EQ @set_8051_sfr_status_of_pseudo_status % |
---|
| 659 | |9: #EQ <EQ >get_8051_sfr_status_of_pseudo_status >get_8051_sfr_status_of_pseudo_status |
---|
| 660 | >external_ram_status_of_pseudo_status @set_external_ram_status_of_pseudo_status ] |
---|
| 661 | qed. |
---|