1 | include "ASM/ASM.ma". |
---|
2 | include "ASM/Arithmetic.ma". |
---|
3 | include "ASM/Fetch.ma". |
---|
4 | include "ASM/Status.ma". |
---|
5 | include "utilities/extralib.ma". |
---|
6 | include "ASM/Assembly.ma". |
---|
7 | |
---|
8 | (* Internal types *) |
---|
9 | |
---|
10 | (* ppc_pc_map: program length × (pseudo program counter ↦ 〈pc, jump_length〉) *) |
---|
11 | definition ppc_pc_map ≝ ℕ × (BitVectorTrie (ℕ × jump_length) 16). |
---|
12 | |
---|
13 | (* The different properties that we want/need to prove at some point *) |
---|
14 | (* During our iteration, everything not yet seen is None, and vice versa *) |
---|
15 | definition out_of_program_none ≝ |
---|
16 | λprefix:list labelled_instruction.λsigma:ppc_pc_map. |
---|
17 | ∀i.i < 2^16 → (i > |prefix| ↔ bvt_lookup_opt … (bitvector_of_nat ? i) (\snd sigma) = None ?). |
---|
18 | |
---|
19 | (* If instruction i is a jump, then there will be something in the policy at |
---|
20 | * position i *) |
---|
21 | definition is_jump' ≝ |
---|
22 | λx:preinstruction Identifier. |
---|
23 | match x with |
---|
24 | [ JC _ ⇒ True |
---|
25 | | JNC _ ⇒ True |
---|
26 | | JZ _ ⇒ True |
---|
27 | | JNZ _ ⇒ True |
---|
28 | | JB _ _ ⇒ True |
---|
29 | | JNB _ _ ⇒ True |
---|
30 | | JBC _ _ ⇒ True |
---|
31 | | CJNE _ _ ⇒ True |
---|
32 | | DJNZ _ _ ⇒ True |
---|
33 | | _ ⇒ False |
---|
34 | ]. |
---|
35 | |
---|
36 | definition is_relative_jump ≝ |
---|
37 | λinstr:pseudo_instruction. |
---|
38 | match instr with |
---|
39 | [ Instruction i ⇒ is_jump' i |
---|
40 | | _ ⇒ False |
---|
41 | ]. |
---|
42 | |
---|
43 | definition is_jump ≝ |
---|
44 | λinstr:pseudo_instruction. |
---|
45 | match instr with |
---|
46 | [ Instruction i ⇒ is_jump' i |
---|
47 | | Call _ ⇒ True |
---|
48 | | Jmp _ ⇒ True |
---|
49 | | _ ⇒ False |
---|
50 | ]. |
---|
51 | |
---|
52 | definition is_call ≝ |
---|
53 | λinstr:pseudo_instruction. |
---|
54 | match instr with |
---|
55 | [ Call _ ⇒ True |
---|
56 | | _ ⇒ False |
---|
57 | ]. |
---|
58 | |
---|
59 | definition is_jump_to ≝ |
---|
60 | λx:pseudo_instruction.λd:Identifier. |
---|
61 | match x with |
---|
62 | [ Instruction i ⇒ match i with |
---|
63 | [ JC j ⇒ d = j |
---|
64 | | JNC j ⇒ d = j |
---|
65 | | JZ j ⇒ d = j |
---|
66 | | JNZ j ⇒ d = j |
---|
67 | | JB _ j ⇒ d = j |
---|
68 | | JNB _ j ⇒ d = j |
---|
69 | | JBC _ j ⇒ d = j |
---|
70 | | CJNE _ j ⇒ d = j |
---|
71 | | DJNZ _ j ⇒ d = j |
---|
72 | | _ ⇒ False |
---|
73 | ] |
---|
74 | | Call c ⇒ d = c |
---|
75 | | Jmp j ⇒ d = j |
---|
76 | | _ ⇒ False |
---|
77 | ]. |
---|
78 | |
---|
79 | definition not_jump_default ≝ |
---|
80 | λprefix:list labelled_instruction.λsigma:ppc_pc_map. |
---|
81 | ∀i:ℕ.i < |prefix| → |
---|
82 | ¬is_jump (\snd (nth i ? prefix 〈None ?, Comment []〉)) → |
---|
83 | \snd (bvt_lookup … (bitvector_of_nat ? i) (\snd sigma) 〈0,short_jump〉) = short_jump. |
---|
84 | |
---|
85 | (* Between two policies, jumps cannot decrease *) |
---|
86 | definition jmpeqb: jump_length → jump_length → bool ≝ |
---|
87 | λj1.λj2. |
---|
88 | match j1 with |
---|
89 | [ short_jump ⇒ match j2 with [ short_jump ⇒ true | _ ⇒ false ] |
---|
90 | | absolute_jump ⇒ match j2 with [ absolute_jump ⇒ true | _ ⇒ false ] |
---|
91 | | long_jump ⇒ match j2 with [ long_jump ⇒ true | _ ⇒ false ] |
---|
92 | ]. |
---|
93 | |
---|
94 | lemma jmpeqb_to_eq: ∀j1,j2.jmpeqb j1 j2 → j1 = j2. |
---|
95 | #j1 #j2 cases j1 cases j2 |
---|
96 | [1,5,9: / by /] |
---|
97 | #H cases H |
---|
98 | qed. |
---|
99 | |
---|
100 | definition jmple: jump_length → jump_length → Prop ≝ |
---|
101 | λj1.λj2. |
---|
102 | match j1 with |
---|
103 | [ short_jump ⇒ |
---|
104 | match j2 with |
---|
105 | [ short_jump ⇒ False |
---|
106 | | _ ⇒ True |
---|
107 | ] |
---|
108 | | absolute_jump ⇒ |
---|
109 | match j2 with |
---|
110 | [ long_jump ⇒ True |
---|
111 | | _ ⇒ False |
---|
112 | ] |
---|
113 | | long_jump ⇒ False |
---|
114 | ]. |
---|
115 | |
---|
116 | definition jmpleq: jump_length → jump_length → Prop ≝ |
---|
117 | λj1.λj2.jmple j1 j2 ∨ j1 = j2. |
---|
118 | |
---|
119 | definition jump_increase ≝ |
---|
120 | λprefix:list labelled_instruction.λop:ppc_pc_map.λp:ppc_pc_map. |
---|
121 | ∀i.i ≤ |prefix| → |
---|
122 | let 〈opc,oj〉 ≝ bvt_lookup … (bitvector_of_nat ? i) (\snd op) 〈0,short_jump〉 in |
---|
123 | let 〈pc,j〉 ≝ bvt_lookup … (bitvector_of_nat ? i) (\snd p) 〈0,short_jump〉 in |
---|
124 | (*opc ≤ pc ∧*) jmpleq oj j. |
---|
125 | |
---|
126 | (* this is the instruction size as determined by the jump length given *) |
---|
127 | definition expand_relative_jump_internal_unsafe: |
---|
128 | jump_length → ([[relative]] → preinstruction [[relative]]) → list instruction ≝ |
---|
129 | λjmp_len:jump_length.λi. |
---|
130 | match jmp_len with |
---|
131 | [ short_jump ⇒ [ RealInstruction (i (RELATIVE (zero 8))) ] |
---|
132 | | absolute_jump ⇒ [ ] (* this should not happen *) |
---|
133 | | long_jump ⇒ |
---|
134 | [ RealInstruction (i (RELATIVE (bitvector_of_nat ? 2))); |
---|
135 | SJMP (RELATIVE (bitvector_of_nat ? 3)); (* LJMP size? *) |
---|
136 | LJMP (ADDR16 (zero 16)) |
---|
137 | ] |
---|
138 | ]. |
---|
139 | @I |
---|
140 | qed. |
---|
141 | |
---|
142 | definition expand_relative_jump_unsafe: |
---|
143 | jump_length → preinstruction Identifier → list instruction ≝ |
---|
144 | λjmp_len:jump_length.λi. |
---|
145 | match i with |
---|
146 | [ JC jmp ⇒ expand_relative_jump_internal_unsafe jmp_len (JC ?) |
---|
147 | | JNC jmp ⇒ expand_relative_jump_internal_unsafe jmp_len (JNC ?) |
---|
148 | | JB baddr jmp ⇒ expand_relative_jump_internal_unsafe jmp_len (JB ? baddr) |
---|
149 | | JZ jmp ⇒ expand_relative_jump_internal_unsafe jmp_len (JZ ?) |
---|
150 | | JNZ jmp ⇒ expand_relative_jump_internal_unsafe jmp_len (JNZ ?) |
---|
151 | | JBC baddr jmp ⇒ expand_relative_jump_internal_unsafe jmp_len (JBC ? baddr) |
---|
152 | | JNB baddr jmp ⇒ expand_relative_jump_internal_unsafe jmp_len (JNB ? baddr) |
---|
153 | | CJNE addr jmp ⇒ expand_relative_jump_internal_unsafe jmp_len (CJNE ? addr) |
---|
154 | | DJNZ addr jmp ⇒ expand_relative_jump_internal_unsafe jmp_len (DJNZ ? addr) |
---|
155 | | ADD arg1 arg2 ⇒ [ ADD ? arg1 arg2 ] |
---|
156 | | ADDC arg1 arg2 ⇒ [ ADDC ? arg1 arg2 ] |
---|
157 | | SUBB arg1 arg2 ⇒ [ SUBB ? arg1 arg2 ] |
---|
158 | | INC arg ⇒ [ INC ? arg ] |
---|
159 | | DEC arg ⇒ [ DEC ? arg ] |
---|
160 | | MUL arg1 arg2 ⇒ [ MUL ? arg1 arg2 ] |
---|
161 | | DIV arg1 arg2 ⇒ [ DIV ? arg1 arg2 ] |
---|
162 | | DA arg ⇒ [ DA ? arg ] |
---|
163 | | ANL arg ⇒ [ ANL ? arg ] |
---|
164 | | ORL arg ⇒ [ ORL ? arg ] |
---|
165 | | XRL arg ⇒ [ XRL ? arg ] |
---|
166 | | CLR arg ⇒ [ CLR ? arg ] |
---|
167 | | CPL arg ⇒ [ CPL ? arg ] |
---|
168 | | RL arg ⇒ [ RL ? arg ] |
---|
169 | | RR arg ⇒ [ RR ? arg ] |
---|
170 | | RLC arg ⇒ [ RLC ? arg ] |
---|
171 | | RRC arg ⇒ [ RRC ? arg ] |
---|
172 | | SWAP arg ⇒ [ SWAP ? arg ] |
---|
173 | | MOV arg ⇒ [ MOV ? arg ] |
---|
174 | | MOVX arg ⇒ [ MOVX ? arg ] |
---|
175 | | SETB arg ⇒ [ SETB ? arg ] |
---|
176 | | PUSH arg ⇒ [ PUSH ? arg ] |
---|
177 | | POP arg ⇒ [ POP ? arg ] |
---|
178 | | XCH arg1 arg2 ⇒ [ XCH ? arg1 arg2 ] |
---|
179 | | XCHD arg1 arg2 ⇒ [ XCHD ? arg1 arg2 ] |
---|
180 | | RET ⇒ [ RET ? ] |
---|
181 | | RETI ⇒ [ RETI ? ] |
---|
182 | | NOP ⇒ [ RealInstruction (NOP ?) ] |
---|
183 | ]. |
---|
184 | |
---|
185 | definition instruction_size_jmplen: |
---|
186 | jump_length → pseudo_instruction → ℕ ≝ |
---|
187 | λjmp_len. |
---|
188 | λi. |
---|
189 | let pseudos ≝ match i with |
---|
190 | [ Cost cost ⇒ [ ] |
---|
191 | | Comment comment ⇒ [ ] |
---|
192 | | Call call ⇒ |
---|
193 | match jmp_len with |
---|
194 | [ short_jump ⇒ [ ] (* this should not happen *) |
---|
195 | | absolute_jump ⇒ [ ACALL (ADDR11 (zero 11)) ] |
---|
196 | | long_jump ⇒ [ LCALL (ADDR16 (zero 16)) ] |
---|
197 | ] |
---|
198 | | Mov d trgt ⇒ |
---|
199 | [ RealInstruction (MOV ? (inl ? ? (inl ? ? (inr ? ? 〈DPTR, DATA16 (zero 16)〉))))] |
---|
200 | | Instruction instr ⇒ expand_relative_jump_unsafe jmp_len instr |
---|
201 | | Jmp jmp ⇒ |
---|
202 | match jmp_len with |
---|
203 | [ short_jump ⇒ [ SJMP (RELATIVE (zero 8)) ] |
---|
204 | | absolute_jump ⇒ [ AJMP (ADDR11 (zero 11)) ] |
---|
205 | | long_jump ⇒ [ LJMP (ADDR16 (zero 16)) ] |
---|
206 | ] |
---|
207 | ] in |
---|
208 | let mapped ≝ map ? ? assembly1 pseudos in |
---|
209 | let flattened ≝ flatten ? mapped in |
---|
210 | let pc_len ≝ length ? flattened in |
---|
211 | pc_len. |
---|
212 | @I. |
---|
213 | qed. |
---|
214 | |
---|
215 | definition sigma_compact_unsafe ≝ |
---|
216 | λprefix:list labelled_instruction.λlabels:label_map.λsigma:ppc_pc_map. |
---|
217 | ∀n.n < |prefix| → |
---|
218 | match bvt_lookup_opt … (bitvector_of_nat ? n) (\snd sigma) with |
---|
219 | [ None ⇒ False |
---|
220 | | Some x ⇒ let 〈pc,j〉 ≝ x in |
---|
221 | match bvt_lookup_opt … (bitvector_of_nat ? (S n)) (\snd sigma) with |
---|
222 | [ None ⇒ False |
---|
223 | | Some x1 ⇒ let 〈pc1,j1〉 ≝ x1 in |
---|
224 | pc1 = pc + instruction_size_jmplen j (\snd (nth n ? prefix 〈None ?, Comment []〉)) |
---|
225 | ] |
---|
226 | ]. |
---|
227 | |
---|
228 | (* new safety condition: sigma corresponds to program and resulting program is compact *) |
---|
229 | definition sigma_compact ≝ |
---|
230 | λprogram:list labelled_instruction.λlabels:label_map.λsigma:ppc_pc_map. |
---|
231 | ∀n.n < |program| → |
---|
232 | match bvt_lookup_opt … (bitvector_of_nat ? n) (\snd sigma) with |
---|
233 | [ None ⇒ False |
---|
234 | | Some x ⇒ let 〈pc,j〉 ≝ x in |
---|
235 | match bvt_lookup_opt … (bitvector_of_nat ? (S n)) (\snd sigma) with |
---|
236 | [ None ⇒ False |
---|
237 | | Some x1 ⇒ let 〈pc1,j1〉 ≝ x1 in |
---|
238 | pc1 = pc + instruction_size (λid.bitvector_of_nat ? (lookup_def ?? labels id 0)) |
---|
239 | (λppc.bitvector_of_nat ? (\fst (bvt_lookup ?? ppc (\snd sigma) 〈0,short_jump〉))) |
---|
240 | (λppc.jmpeqb long_jump (\snd (bvt_lookup ?? ppc (\snd sigma) 〈0,short_jump〉))) |
---|
241 | (bitvector_of_nat ? n) (\snd (nth n ? program 〈None ?, Comment []〉)) |
---|
242 | ] |
---|
243 | ]. |
---|
244 | |
---|
245 | (* jumps are of the proper size *) |
---|
246 | definition sigma_safe ≝ |
---|
247 | λprefix:list labelled_instruction.λlabels:label_map.λadded:ℕ. |
---|
248 | λold_sigma:ppc_pc_map.λsigma:ppc_pc_map. |
---|
249 | ∀i.i < |prefix| → |
---|
250 | let 〈pc,j〉 ≝ bvt_lookup … (bitvector_of_nat ? i) (\snd sigma) 〈0,short_jump〉 in |
---|
251 | let pc_plus_jmp_length ≝ bitvector_of_nat ? (\fst (bvt_lookup … (bitvector_of_nat ? (S i)) (\snd sigma) 〈0,short_jump〉)) in |
---|
252 | let 〈label,instr〉 ≝ nth i ? prefix 〈None ?, Comment [ ]〉 in |
---|
253 | ∀dest.is_jump_to instr dest → |
---|
254 | let paddr ≝ lookup_def … labels dest 0 in |
---|
255 | let addr ≝ bitvector_of_nat ? (if leb i paddr (* forward jump *) |
---|
256 | then \fst (bvt_lookup … (bitvector_of_nat ? paddr) (\snd old_sigma) 〈0,short_jump〉) + added |
---|
257 | else \fst (bvt_lookup … (bitvector_of_nat ? paddr) (\snd sigma) 〈0,short_jump〉)) in |
---|
258 | match j with |
---|
259 | [ short_jump ⇒ \fst (short_jump_cond pc_plus_jmp_length addr) = true ∧ |
---|
260 | ¬is_call instr |
---|
261 | | absolute_jump ⇒ \fst (absolute_jump_cond pc_plus_jmp_length addr) = true ∧ |
---|
262 | \fst (short_jump_cond pc_plus_jmp_length addr) = false ∧ |
---|
263 | ¬is_relative_jump instr |
---|
264 | | long_jump ⇒ \fst (short_jump_cond pc_plus_jmp_length addr) = false ∧ |
---|
265 | \fst (absolute_jump_cond pc_plus_jmp_length addr) = false |
---|
266 | ]. |
---|
267 | |
---|
268 | |
---|
269 | (* Definitions and theorems for the jump_length type (itself defined in Assembly) *) |
---|
270 | definition max_length: jump_length → jump_length → jump_length ≝ |
---|
271 | λj1.λj2. |
---|
272 | match j1 with |
---|
273 | [ long_jump ⇒ long_jump |
---|
274 | | absolute_jump ⇒ |
---|
275 | match j2 with |
---|
276 | [ absolute_jump ⇒ absolute_jump |
---|
277 | | _ ⇒ long_jump |
---|
278 | ] |
---|
279 | | short_jump ⇒ |
---|
280 | match j2 with |
---|
281 | [ short_jump ⇒ short_jump |
---|
282 | | _ ⇒ long_jump |
---|
283 | ] |
---|
284 | ]. |
---|
285 | |
---|
286 | lemma dec_jmple: ∀x,y:jump_length.Sum (jmple x y) (¬(jmple x y)). |
---|
287 | #x #y cases x cases y /3 by inl, inr, nmk, I/ |
---|
288 | qed. |
---|
289 | |
---|
290 | lemma jmpleq_max_length: ∀ol,nl. |
---|
291 | jmpleq ol (max_length ol nl). |
---|
292 | #ol #nl cases ol cases nl |
---|
293 | /2 by or_introl, or_intror, I/ |
---|
294 | qed. |
---|
295 | |
---|
296 | lemma dec_eq_jump_length: ∀a,b:jump_length.Sum (a = b) (a ≠ b). |
---|
297 | #a #b cases a cases b /2/ |
---|
298 | %2 @nmk #H destruct (H) |
---|
299 | qed. |
---|
300 | |
---|
301 | (* The function that creates the label-to-address map *) |
---|
302 | definition create_label_map: ∀program:list labelled_instruction. |
---|
303 | (Σlabels:label_map. |
---|
304 | ∀l.occurs_exactly_once ?? l program → |
---|
305 | bitvector_of_nat ? (lookup_def ?? labels l 0) = |
---|
306 | address_of_word_labels_code_mem program l |
---|
307 | ) ≝ |
---|
308 | λprogram. |
---|
309 | \fst (create_label_cost_map program). |
---|
310 | #l #Hl lapply (pi2 ?? (create_label_cost_map0 program)) @pair_elim |
---|
311 | #labels #costs #EQ normalize nodelta #H whd in match create_label_cost_map; |
---|
312 | normalize nodelta >EQ @(H l Hl) |
---|
313 | qed. |
---|
314 | |
---|
315 | (* General note on jump length selection: the jump displacement is added/replaced |
---|
316 | * AFTER the fetch (and attendant PC increase), but we calculate before the |
---|
317 | * fetch, which means that in the case of a short and medium jump we are 2 |
---|
318 | * bytes off and have to compensate. |
---|
319 | * For the long jump we don't care, because the PC gets replaced integrally anyway. *) |
---|
320 | definition select_reljump_length: label_map → ppc_pc_map → ppc_pc_map → ℕ → ℕ → |
---|
321 | Identifier → jump_length ≝ |
---|
322 | λlabels.λold_sigma.λinc_sigma.λadded.λppc.λlbl. |
---|
323 | let pc ≝ \fst inc_sigma in |
---|
324 | let pc_plus_jmp_length ≝ bitvector_of_nat ? (pc+2) in |
---|
325 | let paddr ≝ lookup_def … labels lbl 0 in |
---|
326 | let addr ≝ bitvector_of_nat ? (if leb ppc paddr (* forward jump *) |
---|
327 | then \fst (bvt_lookup … (bitvector_of_nat 16 paddr) (\snd old_sigma) 〈0,short_jump〉) + added |
---|
328 | else \fst (bvt_lookup … (bitvector_of_nat 16 paddr) (\snd inc_sigma) 〈0,short_jump〉)) in |
---|
329 | let 〈sj_possible, disp〉 ≝ short_jump_cond pc_plus_jmp_length addr in |
---|
330 | if sj_possible |
---|
331 | then short_jump |
---|
332 | else long_jump. |
---|
333 | |
---|
334 | definition select_call_length: label_map → ppc_pc_map → ppc_pc_map → ℕ → ℕ → |
---|
335 | Identifier → jump_length ≝ |
---|
336 | λlabels.λold_sigma.λinc_sigma.λadded.λppc.λlbl. |
---|
337 | let pc ≝ \fst inc_sigma in |
---|
338 | let pc_plus_jmp_length ≝ bitvector_of_nat ? (pc+2) in |
---|
339 | let paddr ≝ lookup_def ? ? labels lbl 0 in |
---|
340 | let addr ≝ bitvector_of_nat ? |
---|
341 | (if leb ppc paddr (* forward jump *) |
---|
342 | then \fst (bvt_lookup … (bitvector_of_nat ? paddr) (\snd old_sigma) 〈0,short_jump〉) |
---|
343 | + added |
---|
344 | else \fst (bvt_lookup … (bitvector_of_nat ? paddr) (\snd inc_sigma) 〈0,short_jump〉)) in |
---|
345 | let 〈aj_possible, disp〉 ≝ absolute_jump_cond pc_plus_jmp_length addr in |
---|
346 | if aj_possible |
---|
347 | then absolute_jump |
---|
348 | else long_jump. |
---|
349 | |
---|
350 | definition select_jump_length: label_map → ppc_pc_map → ppc_pc_map → ℕ → ℕ → |
---|
351 | Identifier → jump_length ≝ |
---|
352 | λlabels.λold_sigma.λinc_sigma.λadded.λppc.λlbl. |
---|
353 | let pc ≝ \fst inc_sigma in |
---|
354 | let pc_plus_jmp_length ≝ bitvector_of_nat ? (pc+2) in |
---|
355 | let paddr ≝ lookup_def … labels lbl 0 in |
---|
356 | let addr ≝ bitvector_of_nat ? (if leb ppc paddr (* forward jump *) |
---|
357 | then \fst (bvt_lookup … (bitvector_of_nat 16 paddr) (\snd old_sigma) 〈0,short_jump〉) + added |
---|
358 | else \fst (bvt_lookup … (bitvector_of_nat 16 paddr) (\snd inc_sigma) 〈0,short_jump〉)) in |
---|
359 | let 〈sj_possible, disp〉 ≝ short_jump_cond pc_plus_jmp_length addr in |
---|
360 | if sj_possible |
---|
361 | then short_jump |
---|
362 | else select_call_length labels old_sigma inc_sigma added ppc lbl. |
---|
363 | |
---|
364 | definition jump_expansion_step_instruction: label_map → ppc_pc_map → ppc_pc_map → |
---|
365 | ℕ → ℕ → preinstruction Identifier → option jump_length ≝ |
---|
366 | λlabels.λold_sigma.λinc_sigma.λadded.λppc.λi. |
---|
367 | match i with |
---|
368 | [ JC j ⇒ Some ? (select_reljump_length labels old_sigma inc_sigma added ppc j) |
---|
369 | | JNC j ⇒ Some ? (select_reljump_length labels old_sigma inc_sigma added ppc j) |
---|
370 | | JZ j ⇒ Some ? (select_reljump_length labels old_sigma inc_sigma added ppc j) |
---|
371 | | JNZ j ⇒ Some ? (select_reljump_length labels old_sigma inc_sigma added ppc j) |
---|
372 | | JB _ j ⇒ Some ? (select_reljump_length labels old_sigma inc_sigma added ppc j) |
---|
373 | | JBC _ j ⇒ Some ? (select_reljump_length labels old_sigma inc_sigma added ppc j) |
---|
374 | | JNB _ j ⇒ Some ? (select_reljump_length labels old_sigma inc_sigma added ppc j) |
---|
375 | | CJNE _ j ⇒ Some ? (select_reljump_length labels old_sigma inc_sigma added ppc j) |
---|
376 | | DJNZ _ j ⇒ Some ? (select_reljump_length labels old_sigma inc_sigma added ppc j) |
---|
377 | | _ ⇒ None ? |
---|
378 | ]. |
---|
379 | |
---|
380 | lemma dec_is_jump: ∀x.Sum (is_jump x) (¬is_jump x). |
---|
381 | #i cases i |
---|
382 | [#id cases id |
---|
383 | [1,2,3,6,7,33,34: |
---|
384 | #x #y %2 whd in match (is_jump ?); /2 by nmk/ |
---|
385 | |4,5,8,18,19,20,21,22,23,24,25,26,27,28,29,30,31,32: |
---|
386 | #x %2 whd in match (is_jump ?); /2 by nmk/ |
---|
387 | |35,36,37: %2 whd in match (is_jump ?); /2 by nmk/ |
---|
388 | |9,10,14,15: #x %1 / by I/ |
---|
389 | |11,12,13,16,17: #x #y %1 / by I/ |
---|
390 | ] |
---|
391 | |2,3: #x %2 /2 by nmk/ |
---|
392 | |4,5: #x %1 / by I/ |
---|
393 | |6: #x #y %2 /2 by nmk/ |
---|
394 | ] |
---|
395 | qed. |
---|
396 | |
---|
397 | lemma geb_to_leb: ∀a,b:ℕ.geb a b = leb b a. |
---|
398 | #a #b / by refl/ |
---|
399 | qed. |
---|
400 | |
---|
401 | lemma nth_last: ∀A,a,l. |
---|
402 | nth (|l|) A l a = a. |
---|
403 | #A #a #l elim l |
---|
404 | [ / by / |
---|
405 | | #h #t #Hind whd in match (nth ????); whd in match (tail ??); @Hind |
---|
406 | ] |
---|
407 | qed. |
---|
408 | |
---|
409 | (* The first step of the jump expansion: everything to short. *) |
---|
410 | definition jump_expansion_start: |
---|
411 | ∀program:(Σl:list labelled_instruction.S (|l|) < 2^16). |
---|
412 | ∀labels:label_map. |
---|
413 | Σpolicy:option ppc_pc_map. |
---|
414 | match policy with |
---|
415 | [ None ⇒ True |
---|
416 | | Some p ⇒ And (And (And (And (And (And (And |
---|
417 | (out_of_program_none (pi1 ?? program) p) |
---|
418 | (not_jump_default (pi1 ?? program) p)) |
---|
419 | (sigma_compact_unsafe program labels p)) |
---|
420 | (\fst (bvt_lookup … (bitvector_of_nat ? 0) (\snd p) 〈0,short_jump〉) = 0)) |
---|
421 | (\fst p = \fst (bvt_lookup … (bitvector_of_nat ? (|program|)) (\snd p) 〈0,short_jump〉))) |
---|
422 | (∀i.i ≤ |program| → ∃pc. |
---|
423 | bvt_lookup_opt … (bitvector_of_nat ? i) (\snd p) = Some ? 〈pc,short_jump〉)) |
---|
424 | (bvt_lookup_opt … (bitvector_of_nat ? (|program|)) (\snd p) = Some ? 〈\fst p,short_jump〉)) |
---|
425 | (\fst p < 2^16) |
---|
426 | ] ≝ |
---|
427 | λprogram.λlabels. |
---|
428 | let final_policy ≝ foldl_strong (option Identifier × pseudo_instruction) |
---|
429 | (λprefix.Σpolicy:ppc_pc_map.And (And (And (And (And (And |
---|
430 | (out_of_program_none prefix policy) |
---|
431 | (not_jump_default prefix policy)) |
---|
432 | (sigma_compact_unsafe prefix labels policy)) |
---|
433 | (\fst (bvt_lookup … (bitvector_of_nat ? 0) (\snd policy) 〈0,short_jump〉) = 0)) |
---|
434 | (\fst policy = \fst (bvt_lookup … (bitvector_of_nat ? (|prefix|)) (\snd policy) 〈0,short_jump〉))) |
---|
435 | (∀i.i ≤ |prefix| → ∃pc. |
---|
436 | bvt_lookup_opt … (bitvector_of_nat ? i) (\snd policy) = Some ? 〈pc,short_jump〉)) |
---|
437 | (bvt_lookup_opt … (bitvector_of_nat ? (|prefix|)) (\snd policy) = |
---|
438 | Some ? 〈\fst policy,short_jump〉)) |
---|
439 | program |
---|
440 | (λprefix.λx.λtl.λprf.λp. |
---|
441 | let 〈pc,sigma〉 ≝ pi1 ?? p in |
---|
442 | let 〈label,instr〉 ≝ x in |
---|
443 | let isize ≝ instruction_size_jmplen short_jump instr in |
---|
444 | 〈pc + isize, bvt_insert … (bitvector_of_nat 16 (S (|prefix|))) 〈pc+isize,short_jump〉 sigma〉 |
---|
445 | ) 〈0, bvt_insert ?? (bitvector_of_nat 16 0) 〈0,short_jump〉 (Stub ??)〉 in |
---|
446 | if geb (\fst (pi1 ?? final_policy)) 2^16 then |
---|
447 | None ? |
---|
448 | else |
---|
449 | Some ? (pi1 ?? final_policy). |
---|
450 | [ / by I/ |
---|
451 | | lapply p -p generalize in match (foldl_strong ?????); * #p #Hp #hg |
---|
452 | @conj [ @Hp | @not_le_to_lt @leb_false_to_not_le <geb_to_leb @hg ] |
---|
453 | | @conj [ @conj [ @conj [ @conj [ @conj [ @conj |
---|
454 | [ (* out_of_program_none *) |
---|
455 | #i #Hi2 >append_length <commutative_plus @conj |
---|
456 | [ (* → *) #Hi normalize in Hi; cases (le_to_or_lt_eq … Hi) -Hi #Hi |
---|
457 | cases p -p #p cases p -p #pc #p #Hp cases x -x #l #pi |
---|
458 | [ >lookup_opt_insert_miss |
---|
459 | [ @(proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hp))))) i Hi2)) |
---|
460 | @le_S_to_le @le_S_to_le @Hi |
---|
461 | | @bitvector_of_nat_abs |
---|
462 | [ @Hi2 |
---|
463 | | @(transitive_lt … Hi2) @le_S_to_le @Hi |
---|
464 | | @sym_neq @lt_to_not_eq @le_S_to_le @Hi |
---|
465 | ] |
---|
466 | ] |
---|
467 | | >lookup_opt_insert_miss |
---|
468 | [ <Hi |
---|
469 | @(proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hp))))) (S (S (|prefix|))) ?)) |
---|
470 | [ >Hi @Hi2 |
---|
471 | | @le_S @le_n |
---|
472 | ] |
---|
473 | | @bitvector_of_nat_abs |
---|
474 | [ @Hi2 |
---|
475 | | @(transitive_lt … Hi2) <Hi @le_n |
---|
476 | | @sym_neq @lt_to_not_eq <Hi @le_n |
---|
477 | ] |
---|
478 | ] |
---|
479 | ] |
---|
480 | | (* ← *) cases p -p #p cases p -p #pc #p #Hp cases x in prf; -x #l #pi #prf |
---|
481 | normalize nodelta cases (decidable_eq_nat i (S (|prefix|))) |
---|
482 | [ #Hi >Hi >lookup_opt_insert_hit #H destruct (H) |
---|
483 | | #Hi >lookup_opt_insert_miss |
---|
484 | [ #Hl |
---|
485 | elim (le_to_or_lt_eq … (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hp))))) i Hi2) Hl)) |
---|
486 | [ #Hi3 @Hi3 |
---|
487 | | #Hi3 @⊥ @(absurd ? Hi3) @sym_neq @Hi |
---|
488 | ] |
---|
489 | | @bitvector_of_nat_abs |
---|
490 | [ @Hi2 |
---|
491 | | @(transitive_lt … (pi2 ?? program)) >prf @le_S_S >append_length |
---|
492 | <plus_n_Sm @le_S_S @le_plus_n_r |
---|
493 | | @Hi |
---|
494 | ] |
---|
495 | ] |
---|
496 | ] |
---|
497 | ] |
---|
498 | | (* not_jump_default *) cases p -p #p cases p -p #pc #sigma #Hp |
---|
499 | cases x in prf; #lbl #ins #prf #i >append_length <commutative_plus #Hi |
---|
500 | normalize in Hi; normalize nodelta cases (le_to_or_lt_eq … (le_S_S_to_le … Hi)) -Hi #Hi |
---|
501 | [ >lookup_insert_miss |
---|
502 | [ lapply ((proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hp)))))) i Hi) |
---|
503 | >nth_append_first |
---|
504 | [ #H #H2 @H @H2 |
---|
505 | | @Hi |
---|
506 | ] |
---|
507 | | @bitvector_of_nat_abs |
---|
508 | [ @(transitive_lt … (pi2 ?? program)) >prf >append_length <commutative_plus >plus_n_Sm |
---|
509 | @le_plus_a @le_S @Hi |
---|
510 | | @(transitive_lt … (pi2 ?? program)) @le_S_S >prf >append_length <plus_n_Sm @le_S_S |
---|
511 | @le_plus_n_r |
---|
512 | | @lt_to_not_eq @le_S @Hi |
---|
513 | ] |
---|
514 | ] |
---|
515 | | >Hi >lookup_insert_miss |
---|
516 | [ #_ elim (proj2 ?? (proj1 ?? Hp) (|prefix|) (le_n (|prefix|))) #pc #Hl |
---|
517 | >(lookup_opt_lookup_hit … Hl 〈0,short_jump〉) @refl |
---|
518 | | @bitvector_of_nat_abs |
---|
519 | [ @(transitive_lt … (pi2 ?? program)) >prf @le_S_S >append_length @le_plus_n_r |
---|
520 | | @(transitive_lt … (pi2 ?? program)) >prf @le_S_S >append_length <plus_n_Sm @le_S_S |
---|
521 | @le_plus_n_r |
---|
522 | | @lt_to_not_eq @le_n |
---|
523 | ] |
---|
524 | ] |
---|
525 | ] |
---|
526 | ] |
---|
527 | | (* policy_compact_unsafe *) #i >append_length <commutative_plus #Hi normalize in Hi; |
---|
528 | cases p -p #p cases p -p #fpc #sigma #Hp cases x #lbl #instr normalize nodelta |
---|
529 | cases (le_to_or_lt_eq … (le_S_S_to_le … Hi)) -Hi #Hi |
---|
530 | [ >lookup_opt_insert_miss |
---|
531 | [ >lookup_opt_insert_miss |
---|
532 | [ lapply (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hp)))) i Hi) |
---|
533 | lapply (refl ? (bvt_lookup_opt … (bitvector_of_nat ? i) sigma)) |
---|
534 | cases (bvt_lookup_opt … (bitvector_of_nat ? i) sigma) in ⊢ (???% → %); |
---|
535 | [ #_ normalize nodelta / by / |
---|
536 | | #x cases x -x #pci #ji #EQi |
---|
537 | lapply (refl ? (bvt_lookup_opt … (bitvector_of_nat ? (S i)) sigma)) |
---|
538 | cases (bvt_lookup_opt … (bitvector_of_nat ? (S i)) sigma) in ⊢ (???% → %); |
---|
539 | [ #_ normalize nodelta / by / |
---|
540 | | #x cases x -x #pcSi #jSi #EQSi normalize nodelta >nth_append_first |
---|
541 | [ / by / |
---|
542 | | @Hi |
---|
543 | ] |
---|
544 | ] |
---|
545 | ] |
---|
546 | ] |
---|
547 | ] |
---|
548 | [2: lapply (le_S_to_le … Hi) -Hi #Hi] |
---|
549 | @bitvector_of_nat_abs |
---|
550 | [1,4: @(transitive_lt … (pi2 ?? program)) >prf @le_S_S >append_length <commutative_plus |
---|
551 | @le_plus_a @Hi |
---|
552 | |2,5: @(transitive_lt … (pi2 ?? program)) >prf @le_S_S >append_length <plus_n_Sm |
---|
553 | @le_S_S @le_plus_n_r |
---|
554 | |3,6: @lt_to_not_eq @le_S_S @Hi |
---|
555 | ] |
---|
556 | | >lookup_opt_insert_miss |
---|
557 | [ >Hi >lookup_opt_insert_hit normalize nodelta |
---|
558 | >(proj2 ?? Hp) normalize nodelta >nth_append_second |
---|
559 | [ <minus_n_n whd in match (nth ????); @refl |
---|
560 | | @le_n |
---|
561 | ] |
---|
562 | | @bitvector_of_nat_abs |
---|
563 | [ @(transitive_lt … (pi2 ?? program)) >Hi >prf @le_S_S >append_length <commutative_plus |
---|
564 | @le_plus_a @le_n |
---|
565 | | @(transitive_lt … (pi2 ?? program)) >prf @le_S_S >append_length <plus_n_Sm |
---|
566 | @le_S_S @le_plus_n_r |
---|
567 | | @lt_to_not_eq @le_S_S >Hi @le_n |
---|
568 | ] |
---|
569 | ] |
---|
570 | ] |
---|
571 | ] |
---|
572 | | (* 0 ↦ 0 *) |
---|
573 | cases p -p #p cases p -p #pc #sigma #Hp cases x #lbl #instr normalize nodelta |
---|
574 | >lookup_insert_miss |
---|
575 | [ @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hp)))) |
---|
576 | | @bitvector_of_nat_abs |
---|
577 | [ / by / |
---|
578 | | @(transitive_lt … (pi2 ?? program)) >prf >append_length @le_S_S <plus_n_Sm |
---|
579 | @le_S_S @le_plus_n_r |
---|
580 | | @lt_to_not_eq / by / |
---|
581 | ] |
---|
582 | ] |
---|
583 | ] |
---|
584 | | (* fst p = pc *) |
---|
585 | cases p -p #p cases p -p #pc #sigma #Hp cases x #lbl #instr normalize nodelta |
---|
586 | >append_length >(commutative_plus (|prefix|)) >lookup_insert_hit @refl |
---|
587 | ] |
---|
588 | | (* lookup = short_jump *) #i >append_length <commutative_plus #Hi normalize in Hi; |
---|
589 | cases p -p #p cases p -p #pc #sigma #Hp cases x #lbl #instr normalize nodelta |
---|
590 | cases (le_to_or_lt_eq … Hi) -Hi #Hi |
---|
591 | [ >lookup_opt_insert_miss |
---|
592 | [ @(proj2 ?? (proj1 ?? Hp) i (le_S_S_to_le … Hi)) |
---|
593 | | @bitvector_of_nat_abs |
---|
594 | [ @(transitive_lt … (pi2 ?? program)) >prf >append_length @le_S_S >commutative_plus |
---|
595 | @le_plus_a @le_S_S_to_le @Hi |
---|
596 | | @(transitive_lt … (pi2 ?? program)) >prf >append_length <plus_n_Sm @le_S_S |
---|
597 | @le_S_S @le_plus_n_r |
---|
598 | | @lt_to_not_eq @Hi |
---|
599 | ] |
---|
600 | ] |
---|
601 | | >Hi >lookup_opt_insert_hit @(ex_intro ?? (pc+instruction_size_jmplen short_jump instr)) |
---|
602 | @refl |
---|
603 | ] |
---|
604 | ] |
---|
605 | | (* lookup at the end *) cases p -p #p cases p -p #pc #sigma #Hp cases x |
---|
606 | #lbl #instr >append_length <plus_n_Sm <plus_n_O >lookup_opt_insert_hit |
---|
607 | / by refl/ |
---|
608 | ] |
---|
609 | | @conj [ @conj [ @conj [ @conj [ @conj [ @conj |
---|
610 | [ #i cases i |
---|
611 | [ #Hi2 @conj |
---|
612 | [ (* → *) #Hi @⊥ @(absurd ? Hi) @le_to_not_lt / by / |
---|
613 | | (* ← *) >lookup_opt_insert_hit #Hl destruct (Hl) |
---|
614 | ] |
---|
615 | | -i #i #Hi2 @conj |
---|
616 | [ #Hi >lookup_opt_insert_miss |
---|
617 | [ / by refl/ |
---|
618 | | @bitvector_of_nat_abs |
---|
619 | [ @Hi2 |
---|
620 | | / by / |
---|
621 | | @sym_neq @lt_to_not_eq / by / |
---|
622 | ] |
---|
623 | ] |
---|
624 | | #_ @le_S_S @le_O_n |
---|
625 | ] |
---|
626 | ] |
---|
627 | | #i cases i |
---|
628 | [ #Hi @⊥ @(absurd … Hi) @not_le_Sn_O |
---|
629 | | -i #i #Hi #Hj @⊥ @(absurd … Hi) @not_le_Sn_O |
---|
630 | ] |
---|
631 | ] |
---|
632 | | #i cases i |
---|
633 | [ #Hi @⊥ @(absurd … Hi) @le_to_not_lt @le_n |
---|
634 | | -i #i #Hi @⊥ @(absurd … Hi) @not_le_Sn_O |
---|
635 | ] |
---|
636 | ] |
---|
637 | | >lookup_insert_hit @refl |
---|
638 | ] |
---|
639 | | >lookup_insert_hit @refl |
---|
640 | ] |
---|
641 | | #i cases i |
---|
642 | [ #Hi >lookup_opt_insert_hit @(ex_intro ?? 0) @refl |
---|
643 | | -i #i #Hi @⊥ @(absurd … Hi) @not_le_Sn_O |
---|
644 | ] |
---|
645 | ] |
---|
646 | | >lookup_opt_insert_hit @refl |
---|
647 | ] |
---|
648 | ] |
---|
649 | qed. |
---|
650 | |
---|
651 | (* NOTE: we only compare the first elements here because otherwise the |
---|
652 | * added = 0 → policy_equal property of jump_expansion_step doesn't hold: |
---|
653 | * if we have not added anything to the pc, we only know the PC hasn't changed, |
---|
654 | * there might still have been a short/medium jump change *) |
---|
655 | definition sigma_pc_equal ≝ |
---|
656 | λprogram:list labelled_instruction.λp1,p2:ppc_pc_map. |
---|
657 | (∀n.n ≤ |program| → |
---|
658 | \fst (bvt_lookup … (bitvector_of_nat 16 n) (\snd p1) 〈0,short_jump〉) = |
---|
659 | \fst (bvt_lookup … (bitvector_of_nat 16 n) (\snd p2) 〈0,short_jump〉)). |
---|
660 | |
---|
661 | definition sigma_jump_equal ≝ |
---|
662 | λprogram:list labelled_instruction.λp1,p2:ppc_pc_map. |
---|
663 | (∀n.n < |program| → |
---|
664 | \snd (bvt_lookup … (bitvector_of_nat 16 n) (\snd p1) 〈0,short_jump〉) = |
---|
665 | \snd (bvt_lookup … (bitvector_of_nat 16 n) (\snd p2) 〈0,short_jump〉)). |
---|
666 | |
---|
667 | definition nec_plus_ultra ≝ |
---|
668 | λprogram:list labelled_instruction.λp:ppc_pc_map. |
---|
669 | ¬(∀i.i < |program| → is_jump (\snd (nth i ? program 〈None ?, Comment []〉)) → |
---|
670 | \snd (bvt_lookup … (bitvector_of_nat 16 i) (\snd p) 〈0,short_jump〉) = long_jump). |
---|
671 | |
---|
672 | (*include alias "common/Identifiers.ma".*) |
---|
673 | include alias "ASM/BitVector.ma". |
---|
674 | include alias "basics/lists/list.ma". |
---|
675 | include alias "arithmetics/nat.ma". |
---|
676 | include alias "basics/logic.ma". |
---|
677 | |
---|
678 | lemma blerpque: ∀a,b,i. |
---|
679 | is_jump i → instruction_size_jmplen (max_length a b) i = instruction_size_jmplen a i → |
---|
680 | (max_length a b) = a. |
---|
681 | #a #b #i cases i |
---|
682 | [1: #pi cases pi |
---|
683 | [1,2,3,4,5,6,7,8,18,19,20,21,22,23,24,25,26,27,28,29,30,31,32,33,34,35,36,37: |
---|
684 | try (#x #y #H #_) try (#x #H #_) try (#H #_) cases H |
---|
685 | |9,10,11,12,13,14,15,16,17: #x [3,4,5,8,9: #y] #_ try (#_ %) |
---|
686 | try (#abs normalize in abs; destruct (abs) @I) |
---|
687 | cases a; cases b; try (#_ %) try (#abs normalize in abs; destruct(abs) @I) |
---|
688 | try (@(subaddressing_mode_elim … x) #w #abs normalize in abs; destruct (abs) @I) |
---|
689 | cases x * #a1 #a2 @(subaddressing_mode_elim … a2) #w |
---|
690 | try ( #abs normalize in abs; destruct (abs) @I) |
---|
691 | @(subaddressing_mode_elim … a1) #w2 #abs normalize in abs; destruct (abs) |
---|
692 | ] |
---|
693 | |2,3,6: #x [3: #y] #H cases H |
---|
694 | |4,5: #id #_ cases a cases b |
---|
695 | [2,3,4,6,11,12,13,15: normalize #H destruct (H) |
---|
696 | |1,5,7,8,9,10,14,16,17,18: #H / by refl/ |
---|
697 | ] |
---|
698 | ] |
---|
699 | qed. |
---|
700 | |
---|
701 | lemma etblorp: ∀a,b,i.is_jump i → |
---|
702 | instruction_size_jmplen a i ≤ instruction_size_jmplen (max_length a b) i. |
---|
703 | #a #b #i cases i |
---|
704 | [2,3,6: #x [3: #y] #H cases H |
---|
705 | |4,5: #id #_ cases a cases b / by le_n/ |
---|
706 | |1: #pi cases pi |
---|
707 | [1,2,3,4,5,6,7,8,18,19,20,21,22,23,24,25,26,27,28,29,30,31,32,33,34,35,36,37: |
---|
708 | [1,2,3,6,7,24,25: #x #y |
---|
709 | |4,5,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23: #x] |
---|
710 | #H cases H |
---|
711 | |9,10,11,12,13,14,15,16,17: #x [3,4,5,8,9: #y] |
---|
712 | #_ cases a cases b |
---|
713 | [2,3: cases x #ad cases ad |
---|
714 | [15,34: #b #Hb / by le_n/ |
---|
715 | |1,2,3,4,8,9,16,17,18,19,20,21,22,23,27,28,35,36,37,38: #b] #Hb cases Hb |
---|
716 | |1,4,5,6,7,8,9: / by le_n/ |
---|
717 | |11,12: cases x #ad cases ad |
---|
718 | [15,34: #b #Hb / by le_n/ |
---|
719 | |1,2,3,4,8,9,16,17,18,19,20,21,22,23,27,28,35,36,37,38: #b] #Hb cases Hb |
---|
720 | |10,13,14,15,16,17,18: / by le_n/ |
---|
721 | |20,21: cases x #ad cases ad |
---|
722 | [15,34: #b #Hb / by le_n/ |
---|
723 | |1,2,3,4,8,9,16,17,18,19,20,21,22,23,27,28,35,36,37,38: #b] #Hb cases Hb |
---|
724 | |19,22,23,24,25,26,27: / by le_n/ |
---|
725 | |29,30: cases x #ad cases ad #a1 #a2 |
---|
726 | [1,3: cases a2 #ad2 cases ad2 |
---|
727 | [1,8,20,27: #b #Hb / by le_n/ |
---|
728 | |2,3,4,9,15,16,17,18,19,21,22,23,28,34,35,36,37,38: #b] #Hb cases Hb |
---|
729 | |2,4: cases a1 #ad1 cases ad1 |
---|
730 | [2,4,21,23: #b #Hb / by le_n/ |
---|
731 | |1,3,8,9,15,16,17,18,19,20,22,27,28,34,35,36,37,38: #b] #Hb cases Hb |
---|
732 | ] |
---|
733 | |28,31,32,33,34,35,36: / by le_n/ |
---|
734 | |38,39: cases x #ad cases ad |
---|
735 | [1,4,20,23: #b #Hb / by le_n/ |
---|
736 | |2,3,8,9,15,16,17,18,19,21,22,27,28,34,35,36,37,38: #b] #Hb cases Hb |
---|
737 | |37,40,41,42,43,44,45: / by le_n/ |
---|
738 | |46,47,48,49,50,51,52,53,54: / by le_n/ |
---|
739 | |55,56,57,58,59,60,61,62,63: / by le_n/ |
---|
740 | |64,65,66,67,68,69,70,71,72: / by le_n/ |
---|
741 | |73,74,75,76,77,78,79,80,81: / by le_n/ |
---|
742 | ] |
---|
743 | ] |
---|
744 | ] |
---|
745 | qed. |
---|
746 | |
---|
747 | lemma minus_zero_to_le: ∀n,m:ℕ.n - m = 0 → n ≤ m. |
---|
748 | #n |
---|
749 | elim n |
---|
750 | [ #m #_ @le_O_n |
---|
751 | | #n' #Hind #m cases m |
---|
752 | [ #H -n whd in match (minus ??) in H; >H @le_n |
---|
753 | | #m' -m #H whd in match (minus ??) in H; @le_S_S @Hind @H |
---|
754 | ] |
---|
755 | ] |
---|
756 | qed. |
---|
757 | |
---|
758 | lemma plus_zero_zero: ∀n,m:ℕ.n + m = 0 → m = 0. |
---|
759 | #n #m #Hn @sym_eq @le_n_O_to_eq <Hn >commutative_plus @le_plus_n_r |
---|
760 | qed. |
---|
761 | |
---|
762 | lemma not_true_is_false: |
---|
763 | ∀b:bool.b ≠ true → b = false. |
---|
764 | #b cases b |
---|
765 | [ #H @⊥ @(absurd ?? H) @refl |
---|
766 | | #H @refl |
---|
767 | ] |
---|
768 | qed. |
---|