Changeset 2111 for src/ASM/AssemblyProof.ma
 Timestamp:
 Jun 26, 2012, 5:30:41 PM (9 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/ASM/AssemblyProof.ma
r2110 r2111 3 3 include "ASM/StatusProofs.ma". 4 4 include alias "arithmetics/nat.ma". 5 6 definition bit_elim_prop: ∀P: bool → Prop. Prop ≝7 λP.8 P true ∧ P false.9 10 let rec bitvector_elim_prop_internal11 (n: nat) (P: BitVector n → Prop) (m: nat)12 on m:13 m ≤ n → BitVector (n  m) → Prop ≝14 match m return λm. m ≤ n → BitVector (n  m) → Prop with15 [ O ⇒ λprf1. λprefix. P ?16  S n' ⇒ λprf2. λprefix.17 bit_elim_prop (λbit. bitvector_elim_prop_internal n P n' …)18 ].19 try applyS prefix20 try (@le_S_to_le assumption)21 letin res ≝ (bit ::: prefix)22 <minus_S_S >minus_Sn_m23 assumption24 qed.25 26 definition bitvector_elim_prop ≝27 λn: nat.28 λP: BitVector n → Prop.29 bitvector_elim_prop_internal n P n ? ?.30 try @le_n31 <minus_n_n @[[ ]]32 qed.33 34 lemma bool_eq_internal_eq:35 ∀b, c.36 (λb. λc. (if b then c else (if c then false else true))) b c = true → b = c.37 #b #c38 cases b cases c normalize nodelta39 try (#_ % @I)40 #assm destruct %41 qed.42 5 43 6 definition bit_elim: ∀P: bool → bool. bool ≝ … … 62 25 try @le_n 63 26 <minus_n_n @[[]] 64 qed.65 66 lemma mem_middle_vector:67 ∀A: Type[0].68 ∀m, o: nat.69 ∀eq: A → A → bool.70 ∀reflex: ∀a. eq a a = true.71 ∀p: Vector A m.72 ∀a: A.73 ∀r: Vector A o.74 mem A eq ? (p@@(a:::r)) a = true.75 #A #m #o #eq #reflex #p #a76 elim p try (normalize >reflex #H %)77 #m' #hd #tl #inductive_hypothesis78 normalize79 cases (eq ??) normalize nodelta80 try (#irrelevant %)81 @inductive_hypothesis82 27 qed. 83 28 … … 136 81 cases v try % 137 82 #n' #hd #tl % 138 qed.139 140 corollary subvector_hd_tl:141 ∀A: Type[0].142 ∀o: nat.143 ∀eq: A → A → bool.144 ∀refl: ∀a. eq a a = true.145 ∀h: A.146 ∀v: Vector A o.147 bool_to_Prop (subvector_with A ? ? eq v (h ::: v)).148 #A #o #eq #reflex #h #v149 >(vector_cons_append … h v)150 <(vector_cons_empty … ([[h]] @@ v))151 @(subvector_multiple_append … eq reflex [[ ]] v ? [[h]])152 83 qed. 153 84 … … 236 167 ] 237 168 qed. 238 239 definition product_elim ≝240 λm, n: nat.241 λv: Vector addressing_mode_tag (S m).242 λq: Vector addressing_mode_tag (S n).243 λP: (v × q) → bool.244 list_addressing_mode_tags_elim ? v (λx. list_addressing_mode_tags_elim ? q (λy. P 〈x, y〉)).245 246 definition union_elim ≝247 λA, B: Type[0].248 λelimA: (A → bool) → bool.249 λelimB: (B → bool) → bool.250 λelimU: A ⊎ B → bool.251 elimA (λa. elimB (λb. elimU (inl ? ? a) ∧ elimU (inr ? ? b))).252 253 (*254 definition preinstruction_elim: ∀P: preinstruction [[ relative ]] → bool. bool ≝255 λP.256 list_addressing_mode_tags_elim ? [[ registr ; direct ; indirect ; data ]] (λaddr. P (ADD ? ACC_A addr)) ∧257 list_addressing_mode_tags_elim ? [[ registr ; direct ; indirect ; data ]] (λaddr. P (ADDC ? ACC_A addr)) ∧258 list_addressing_mode_tags_elim ? [[ registr ; direct ; indirect ; data ]] (λaddr. P (SUBB ? ACC_A addr)) ∧259 list_addressing_mode_tags_elim ? [[ acc_a ; registr ; direct ; indirect ; dptr ]] (λaddr. P (INC ? addr)) ∧260 list_addressing_mode_tags_elim ? [[ acc_a ; registr ; direct ; indirect ]] (λaddr. P (DEC ? addr)) ∧261 list_addressing_mode_tags_elim ? [[acc_b]] (λaddr. P (MUL ? ACC_A addr)) ∧262 list_addressing_mode_tags_elim ? [[acc_b]] (λaddr. P (DIV ? ACC_A addr)) ∧263 list_addressing_mode_tags_elim ? [[ registr ; direct ]] (λaddr. bitvector_elim 8 (λr. P (DJNZ ? addr (RELATIVE r)))) ∧264 list_addressing_mode_tags_elim ? [[ acc_a ; carry ; bit_addr ]] (λaddr. P (CLR ? addr)) ∧265 list_addressing_mode_tags_elim ? [[ acc_a ; carry ; bit_addr ]] (λaddr. P (CPL ? addr)) ∧266 P (DA ? ACC_A) ∧267 bitvector_elim 8 (λr. P (JC ? (RELATIVE r))) ∧268 bitvector_elim 8 (λr. P (JNC ? (RELATIVE r))) ∧269 bitvector_elim 8 (λr. P (JZ ? (RELATIVE r))) ∧270 bitvector_elim 8 (λr. P (JNZ ? (RELATIVE r))) ∧271 bitvector_elim 8 (λr. (bitvector_elim 8 (λb: BitVector 8. P (JB ? (BIT_ADDR b) (RELATIVE r))))) ∧272 bitvector_elim 8 (λr. (bitvector_elim 8 (λb: BitVector 8. P (JNB ? (BIT_ADDR b) (RELATIVE r))))) ∧273 bitvector_elim 8 (λr. (bitvector_elim 8 (λb: BitVector 8. P (JBC ? (BIT_ADDR b) (RELATIVE r))))) ∧274 list_addressing_mode_tags_elim ? [[ registr; direct ]] (λaddr. bitvector_elim 8 (λr. P (DJNZ ? addr (RELATIVE r)))) ∧275 P (RL ? ACC_A) ∧276 P (RLC ? ACC_A) ∧277 P (RR ? ACC_A) ∧278 P (RRC ? ACC_A) ∧279 P (SWAP ? ACC_A) ∧280 P (RET ?) ∧281 P (RETI ?) ∧282 P (NOP ?) ∧283 bit_elim (λb. P (XCHD ? ACC_A (INDIRECT b))) ∧284 list_addressing_mode_tags_elim ? [[ carry; bit_addr ]] (λaddr. P (SETB ? addr)) ∧285 bitvector_elim 8 (λaddr. P (PUSH ? (DIRECT addr))) ∧286 bitvector_elim 8 (λaddr. P (POP ? (DIRECT addr))) ∧287 union_elim ? ? (product_elim ? ? [[ acc_a ]] [[ direct; data ]])288 (product_elim ? ? [[ registr; indirect ]] [[ data ]])289 (λd. bitvector_elim 8 (λb. P (CJNE ? d (RELATIVE b)))) ∧290 list_addressing_mode_tags_elim ? [[ registr; direct; indirect ]] (λaddr. P (XCH ? ACC_A addr)) ∧291 union_elim ? ? (product_elim ? ? [[acc_a]] [[ data ; registr ; direct ; indirect ]])292 (product_elim ? ? [[direct]] [[ acc_a ; data ]])293 (λd. P (XRL ? d)) ∧294 union_elim ? ? (union_elim ? ? (product_elim ? ? [[acc_a]] [[ registr ; direct ; indirect ; data ]])295 (product_elim ? ? [[direct]] [[ acc_a ; data ]]))296 (product_elim ? ? [[carry]] [[ bit_addr ; n_bit_addr]])297 (λd. P (ANL ? d)) ∧298 union_elim ? ? (union_elim ? ? (product_elim ? ? [[acc_a]] [[ registr ; data ; direct ; indirect ]])299 (product_elim ? ? [[direct]] [[ acc_a ; data ]]))300 (product_elim ? ? [[carry]] [[ bit_addr ; n_bit_addr]])301 (λd. P (ORL ? d)) ∧302 union_elim ? ? (product_elim ? ? [[acc_a]] [[ ext_indirect ; ext_indirect_dptr ]])303 (product_elim ? ? [[ ext_indirect ; ext_indirect_dptr ]] [[acc_a]])304 (λd. P (MOVX ? d)) ∧305 union_elim ? ? (306 union_elim ? ? (307 union_elim ? ? (308 union_elim ? ? (309 union_elim ? ? (product_elim ? ? [[acc_a]] [[ registr ; direct ; indirect ; data ]])310 (product_elim ? ? [[ registr ; indirect ]] [[ acc_a ; direct ; data ]]))311 (product_elim ? ? [[direct]] [[ acc_a ; registr ; direct ; indirect ; data ]]))312 (product_elim ? ? [[dptr]] [[data16]]))313 (product_elim ? ? [[carry]] [[bit_addr]]))314 (product_elim ? ? [[bit_addr]] [[carry]])315 (λd. P (MOV ? d)).316 %317 qed.318 319 definition instruction_elim: ∀P: instruction → bool. bool ≝320 λP. (*321 bitvector_elim 11 (λx. P (ACALL (ADDR11 x))) ∧322 bitvector_elim 16 (λx. P (LCALL (ADDR16 x))) ∧323 bitvector_elim 11 (λx. P (AJMP (ADDR11 x))) ∧324 bitvector_elim 16 (λx. P (LJMP (ADDR16 x))) ∧ *)325 bitvector_elim 8 (λx. P (SJMP (RELATIVE x))). (* ∧326 P (JMP INDIRECT_DPTR) ∧327 list_addressing_mode_tags_elim ? [[ acc_dptr; acc_pc ]] (λa. P (MOVC ACC_A a)) ∧328 preinstruction_elim (λp. P (RealInstruction p)). *)329 %330 qed.331 332 333 axiom instruction_elim_complete:334 ∀P. instruction_elim P = true → ∀i. P i = true.335 *)336 (*definition eq_instruction ≝337 λi, j: instruction.338 true.*)339 169 340 170 definition eq_addressing_mode: addressing_mode → addressing_mode → bool ≝
Note: See TracChangeset
for help on using the changeset viewer.