Changeset 991 for src/ASM/AssemblyProof.ma

Timestamp:

Jun 17, 2011, 5:17:43 PM (8 years ago)

Author:

mulligan

Message:

loads of axioms related to equality on instructions closed

File:

• src/ASM/AssemblyProof.ma (modified) (1 diff)

src/ASM/AssemblyProof.ma

@@ -415 +415 @@
   λ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