# Changeset 991 for src/ASM

Ignore:
Timestamp:
Jun 17, 2011, 5:17:43 PM (9 years ago)
Message:

loads of axioms related to equality on instructions closed

File:
1 edited

Unmodified
Added
Removed
• ## src/ASM/AssemblyProof.ma

 r989 λi, j: instruction. true.*) axiom eq_instruction: instruction → instruction → bool. axiom eq_instruction_refl: ∀i. eq_instruction i i = true. definition eq_addressing_mode: addressing_mode → addressing_mode → bool ≝ λa, b: addressing_mode. match a with [ DIRECT d ⇒ match b with [ DIRECT e ⇒ eq_bv ? d e | _ ⇒ false ] | INDIRECT b' ⇒ match b with [ INDIRECT e ⇒ eq_b b' e | _ ⇒ false ] | EXT_INDIRECT b' ⇒ match b with [ EXT_INDIRECT e ⇒ eq_b b' e | _ ⇒ false ] | REGISTER bv ⇒ match b with [ REGISTER bv' ⇒ eq_bv ? bv bv' | _ ⇒ false ] | ACC_A ⇒ match b with [ ACC_A ⇒ true | _ ⇒ false ] | ACC_B ⇒ match b with [ ACC_B ⇒ true | _ ⇒ false ] | DPTR ⇒ match b with [ DPTR ⇒ true | _ ⇒ false ] | DATA b' ⇒ match b with [ DATA e ⇒ eq_bv ? b' e | _ ⇒ false ] | DATA16 w ⇒ match b with [ DATA16 e ⇒ eq_bv ? w e | _ ⇒ false ] | ACC_DPTR ⇒ match b with [ ACC_DPTR ⇒ true | _ ⇒ false ] | ACC_PC ⇒ match b with [ ACC_PC ⇒ true | _ ⇒ false ] | EXT_INDIRECT_DPTR ⇒ match b with [ EXT_INDIRECT_DPTR ⇒ true | _ ⇒ false ] | INDIRECT_DPTR ⇒ match b with [ INDIRECT_DPTR ⇒ true | _ ⇒ false ] | CARRY ⇒ match b with [ CARRY ⇒ true | _ ⇒ false ] | BIT_ADDR b' ⇒ match b with [ BIT_ADDR e ⇒ eq_bv ? b' e | _ ⇒ false ] | N_BIT_ADDR b' ⇒ match b with [ N_BIT_ADDR e ⇒ eq_bv ? b' e | _ ⇒ false ] | RELATIVE n ⇒ match b with [ RELATIVE e ⇒ eq_bv ? n e | _ ⇒ false ] | ADDR11 w ⇒ match b with [ ADDR11 e ⇒ eq_bv ? w e | _ ⇒ false ] | ADDR16 w ⇒ match b with [ ADDR16 e ⇒ eq_bv ? w e | _ ⇒ false ] ]. lemma eq_bv_refl: ∀n, b. eq_bv n b b = true. #n #b cases b // qed. lemma eq_b_refl: ∀b. eq_b b b = true. #b cases b // qed. lemma eq_addressing_mode_refl: ∀a. eq_addressing_mode a a = true. #a cases a try #arg1 try #arg2 try @eq_bv_refl try @eq_b_refl try normalize % qed. definition eq_sum: ∀A, B. (A → A → bool) → (B → B → bool) → (A ⊎ B) → (A ⊎ B) → bool ≝ λlt, rt, leq, req, left, right. match left with [ inl l ⇒ match right with [ inl l' ⇒ leq l l' | _ ⇒ false ] | inr r ⇒ match right with [ inr r' ⇒ req r r' | _ ⇒ false ] ]. definition eq_prod: ∀A, B. (A → A → bool) → (B → B → bool) → (A × B) → (A × B) → bool ≝ λlt, rt, leq, req, left, right. let 〈l, r〉 ≝ left in let 〈l', r'〉 ≝ right in leq l l' ∧ req r r'. definition eq_preinstruction: preinstruction [[relative]] → preinstruction [[relative]] → bool ≝ λi, j. match i with [ ADD arg1 arg2 ⇒ match j with [ ADD arg1' arg2' ⇒ eq_addressing_mode arg1 arg1' ∧ eq_addressing_mode arg2 arg2' | _ ⇒ false ] | ADDC arg1 arg2 ⇒ match j with [ ADDC arg1' arg2' ⇒ eq_addressing_mode arg1 arg1' ∧ eq_addressing_mode arg2 arg2' | _ ⇒ false ] | SUBB arg1 arg2 ⇒ match j with [ SUBB arg1' arg2' ⇒ eq_addressing_mode arg1 arg1' ∧ eq_addressing_mode arg2 arg2' | _ ⇒ false ] | INC arg ⇒ match j with [ INC arg' ⇒ eq_addressing_mode arg arg' | _ ⇒ false ] | DEC arg ⇒ match j with [ DEC arg' ⇒ eq_addressing_mode arg arg' | _ ⇒ false ] | MUL arg1 arg2 ⇒ match j with [ MUL arg1' arg2' ⇒ eq_addressing_mode arg1 arg1' ∧ eq_addressing_mode arg2 arg2' | _ ⇒ false ] | DIV arg1 arg2 ⇒ match j with [ DIV arg1' arg2' ⇒ eq_addressing_mode arg1 arg1' ∧ eq_addressing_mode arg2 arg2' | _ ⇒ false ] | DA arg ⇒ match j with [ DA arg' ⇒ eq_addressing_mode arg arg' | _ ⇒ false ] | JC arg ⇒ match j with [ JC arg' ⇒ eq_addressing_mode arg arg' | _ ⇒ false ] | JNC arg ⇒ match j with [ JNC arg' ⇒ eq_addressing_mode arg arg' | _ ⇒ false ] | JB arg1 arg2 ⇒ match j with [ JB arg1' arg2' ⇒ eq_addressing_mode arg1 arg1' ∧ eq_addressing_mode arg2 arg2' | _ ⇒ false ] | JNB arg1 arg2 ⇒ match j with [ JNB arg1' arg2' ⇒ eq_addressing_mode arg1 arg1' ∧ eq_addressing_mode arg2 arg2' | _ ⇒ false ] | JBC arg1 arg2 ⇒ match j with [ JBC arg1' arg2' ⇒ eq_addressing_mode arg1 arg1' ∧ eq_addressing_mode arg2 arg2' | _ ⇒ false ] | JZ arg ⇒ match j with [ JZ arg' ⇒ eq_addressing_mode arg arg' | _ ⇒ false ] | JNZ arg ⇒ match j with [ JNZ arg' ⇒ eq_addressing_mode arg arg' | _ ⇒ false ] | CJNE arg1 arg2 ⇒ match j with [ CJNE arg1' arg2' ⇒ let prod_eq_left ≝ eq_prod [[acc_a]] [[direct; data]] eq_addressing_mode eq_addressing_mode in let prod_eq_right ≝ eq_prod [[registr; indirect]] [[data]] eq_addressing_mode eq_addressing_mode in let arg1_eq ≝ eq_sum ? ? prod_eq_left prod_eq_right in arg1_eq arg1 arg1' ∧ eq_addressing_mode arg2 arg2' | _ ⇒ false ] | DJNZ arg1 arg2 ⇒ match j with [ DJNZ arg1' arg2' ⇒ eq_addressing_mode arg1 arg1' ∧ eq_addressing_mode arg2 arg2' | _ ⇒ false ] | CLR arg ⇒ match j with [ CLR arg' ⇒ eq_addressing_mode arg arg' | _ ⇒ false ] | CPL arg ⇒ match j with [ CPL arg' ⇒ eq_addressing_mode arg arg' | _ ⇒ false ] | RL arg ⇒ match j with [ RL arg' ⇒ eq_addressing_mode arg arg' | _ ⇒ false ] | RLC arg ⇒ match j with [ RLC arg' ⇒ eq_addressing_mode arg arg' | _ ⇒ false ] | RR arg ⇒ match j with [ RR arg' ⇒ eq_addressing_mode arg arg' | _ ⇒ false ] | RRC arg ⇒ match j with [ RRC arg' ⇒ eq_addressing_mode arg arg' | _ ⇒ false ] | SWAP arg ⇒ match j with [ SWAP arg' ⇒ eq_addressing_mode arg arg' | _ ⇒ false ] | SETB arg ⇒ match j with [ SETB arg' ⇒ eq_addressing_mode arg arg' | _ ⇒ false ] | PUSH arg ⇒ match j with [ PUSH arg' ⇒ eq_addressing_mode arg arg' | _ ⇒ false ] | POP arg ⇒ match j with [ POP arg' ⇒ eq_addressing_mode arg arg' | _ ⇒ false ] | XCH arg1 arg2 ⇒ match j with [ XCH arg1' arg2' ⇒ eq_addressing_mode arg1 arg1' ∧ eq_addressing_mode arg2 arg2' | _ ⇒ false ] | XCHD arg1 arg2 ⇒ match j with [ XCHD arg1' arg2' ⇒ eq_addressing_mode arg1 arg1' ∧ eq_addressing_mode arg2 arg2' | _ ⇒ false ] | RET ⇒ match j with [ RET ⇒ true | _ ⇒ false ] | RETI ⇒ match j with [ RETI ⇒ true | _ ⇒ false ] | NOP ⇒ match j with [ NOP ⇒ true | _ ⇒ false ] | MOVX arg ⇒ match j with [ MOVX arg' ⇒ let prod_eq_left ≝ eq_prod [[acc_a]] [[ext_indirect; ext_indirect_dptr]] eq_addressing_mode eq_addressing_mode in let prod_eq_right ≝ eq_prod [[ext_indirect; ext_indirect_dptr]] [[acc_a]] eq_addressing_mode eq_addressing_mode in let sum_eq ≝ eq_sum ? ? prod_eq_left prod_eq_right in sum_eq arg arg' | _ ⇒ false ] | XRL arg ⇒ match j with [ XRL arg' ⇒ let prod_eq_left ≝ eq_prod [[acc_a]] [[ data ; registr ; direct ; indirect ]] eq_addressing_mode eq_addressing_mode in let prod_eq_right ≝ eq_prod [[direct]] [[ acc_a ; data ]] eq_addressing_mode eq_addressing_mode in let sum_eq ≝ eq_sum ? ? prod_eq_left prod_eq_right in sum_eq arg arg' | _ ⇒ false ] | ORL arg ⇒ match j with [ ORL arg' ⇒ let prod_eq_left1 ≝ eq_prod [[acc_a]] [[ registr ; data ; direct ; indirect ]] eq_addressing_mode eq_addressing_mode in let prod_eq_left2 ≝ eq_prod [[direct]] [[ acc_a; data ]] eq_addressing_mode eq_addressing_mode in let prod_eq_left ≝ eq_sum ? ? prod_eq_left1 prod_eq_left2 in let prod_eq_right ≝ eq_prod [[carry]] [[ bit_addr ; n_bit_addr]] eq_addressing_mode eq_addressing_mode in let sum_eq ≝ eq_sum ? ? prod_eq_left prod_eq_right in sum_eq arg arg' | _ ⇒ false ] | ANL arg ⇒ match j with [ ANL arg' ⇒ let prod_eq_left1 ≝ eq_prod [[acc_a]] [[ registr ; direct ; indirect ; data ]] eq_addressing_mode eq_addressing_mode in let prod_eq_left2 ≝ eq_prod [[direct]] [[ acc_a; data ]] eq_addressing_mode eq_addressing_mode in let prod_eq_left ≝ eq_sum ? ? prod_eq_left1 prod_eq_left2 in let prod_eq_right ≝ eq_prod [[carry]] [[ bit_addr ; n_bit_addr]] eq_addressing_mode eq_addressing_mode in let sum_eq ≝ eq_sum ? ? prod_eq_left prod_eq_right in sum_eq arg arg' | _ ⇒ false ] | MOV arg ⇒ match j with [ MOV arg' ⇒ let prod_eq_6 ≝ eq_prod [[acc_a]] [[registr; direct; indirect; data]] eq_addressing_mode eq_addressing_mode in let prod_eq_5 ≝ eq_prod [[registr; indirect]] [[acc_a; direct; data]] eq_addressing_mode eq_addressing_mode in let prod_eq_4 ≝ eq_prod [[direct]] [[acc_a; registr; direct; indirect; data]] eq_addressing_mode eq_addressing_mode in let prod_eq_3 ≝ eq_prod [[dptr]] [[data16]] eq_addressing_mode eq_addressing_mode in let prod_eq_2 ≝ eq_prod [[carry]] [[bit_addr]] eq_addressing_mode eq_addressing_mode in let prod_eq_1 ≝ eq_prod [[bit_addr]] [[carry]] eq_addressing_mode eq_addressing_mode in let sum_eq_1 ≝ eq_sum ? ? prod_eq_6 prod_eq_5 in let sum_eq_2 ≝ eq_sum ? ? sum_eq_1 prod_eq_4 in let sum_eq_3 ≝ eq_sum ? ? sum_eq_2 prod_eq_3 in let sum_eq_4 ≝ eq_sum ? ? sum_eq_3 prod_eq_2 in let sum_eq_5 ≝ eq_sum ? ? sum_eq_4 prod_eq_1 in sum_eq_5 arg arg' | _ ⇒ false ] ]. lemma eq_sum_refl: ∀A, B: Type[0]. ∀leq, req. ∀s. ∀leq_refl: (∀t. leq t t = true). ∀req_refl: (∀u. req u u = true). eq_sum A B leq req s s = true. #A #B #leq #req #s #leq_refl #req_refl cases s whd in ⊢ (? → ??%?) // qed. lemma eq_prod_refl: ∀A, B: Type[0]. ∀leq, req. ∀s. ∀leq_refl: (∀t. leq t t = true). ∀req_refl: (∀u. req u u = true). eq_prod A B leq req s s = true. #A #B #leq #req #s #leq_refl #req_refl cases s whd in ⊢ (? → ? → ??%?) #l #r >leq_refl normalize @req_refl qed. lemma eq_preinstruction_refl: ∀i. eq_preinstruction i i = true. #i cases i try #arg1 try #arg2 try @eq_addressing_mode_refl [1,2,3,4,5,6,7,8,10,16,17,18,19,20: whd in ⊢ (??%?) try % >eq_addressing_mode_refl >eq_addressing_mode_refl % |13,15: whd in ⊢ (??%?) cases arg1 [*: #arg1_left normalize nodelta >eq_prod_refl [*: try % #argr @eq_addressing_mode_refl] ] |11,12: whd in ⊢ (??%?) cases arg1 [1: #arg1_left normalize nodelta >(eq_sum_refl …) [1: % | 2,3: #arg @eq_prod_refl ] @eq_addressing_mode_refl |2: #arg1_left normalize nodelta @eq_prod_refl [*: @eq_addressing_mode_refl ] |3: #arg1_left normalize nodelta >(eq_sum_refl …) [1: % |2,3: #arg @eq_prod_refl #arg @eq_addressing_mode_refl ] |4: #arg1_left normalize nodelta @eq_prod_refl [*: #arg @eq_addressing_mode_refl ] ] |14: whd in ⊢ (??%?) cases arg1 [ #arg1_left normalize nodelta @eq_sum_refl [1: #arg @eq_sum_refl [1: #arg @eq_sum_refl [1: #arg @eq_sum_refl [1: #arg @eq_prod_refl [*: @eq_addressing_mode_refl ] |2: #arg @eq_prod_refl [*: #arg @eq_addressing_mode_refl ] ] |2: #arg @eq_prod_refl [*: #arg @eq_addressing_mode_refl ] ] |2: #arg @eq_prod_refl [*: #arg @eq_addressing_mode_refl ] ] |2: #arg @eq_prod_refl [*: #arg @eq_addressing_mode_refl ] ] |2: #arg1_right normalize nodelta @eq_prod_refl [*: #arg @eq_addressing_mode_refl ] ] |*: whd in ⊢ (??%?) cases arg1 [*: #arg1 >eq_sum_refl [1,4: normalize @eq_addressing_mode_refl |2,3,5,6: #arg @eq_prod_refl [*: #arg @eq_addressing_mode_refl ] ] ] ] qed. definition eq_instruction: instruction → instruction → bool ≝ λi, j. match i with [ ACALL arg ⇒ match j with [ ACALL arg' ⇒ eq_addressing_mode arg arg' | _ ⇒ false ] | LCALL arg ⇒ match j with [ LCALL arg' ⇒ eq_addressing_mode arg arg' | _ ⇒ false ] | AJMP arg ⇒ match j with [ AJMP arg' ⇒ eq_addressing_mode arg arg' | _ ⇒ false ] | LJMP arg ⇒ match j with [ LJMP arg' ⇒ eq_addressing_mode arg arg' | _ ⇒ false ] | SJMP arg ⇒ match j with [ SJMP arg' ⇒ eq_addressing_mode arg arg' | _ ⇒ false ] | JMP arg ⇒ match j with [ JMP arg' ⇒ eq_addressing_mode arg arg' | _ ⇒ false ] | MOVC arg1 arg2 ⇒ match j with [ MOVC arg1' arg2' ⇒ eq_addressing_mode arg1 arg1' ∧ eq_addressing_mode arg2 arg2' | _ ⇒ false ] | RealInstruction instr ⇒ match j with [ RealInstruction instr' ⇒ eq_preinstruction instr instr' | _ ⇒ false ] ]. lemma eq_instruction_refl: ∀i. eq_instruction i i = true. #i cases i [1,2,3,4,5,6: #arg1 @eq_addressing_mode_refl |7: #arg1 #arg2 whd in ⊢ (??%?) >eq_addressing_mode_refl >eq_addressing_mode_refl % |8: #arg @eq_preinstruction_refl ] qed. let rec vect_member
Note: See TracChangeset for help on using the changeset viewer.