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