source: src/ASM/WellLabeled.ma @ 1493

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

finished well labeled check, up to injectivity of the label map

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