source: src/ASM/WellLabeled.ma @ 2714

Last change on this file since 2714 was 2710, checked in by sacerdot, 7 years ago

ASMCosts.ma repaired

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