Ignore:
Timestamp:
Jun 17, 2011, 5:17:43 PM (8 years ago)
Author:
mulligan
Message:

loads of axioms related to equality on instructions closed

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/AssemblyProof.ma

    r989 r991  
    415415  λi, j: instruction.
    416416    true.*)
    417 axiom eq_instruction: instruction → instruction → bool.
    418 axiom eq_instruction_refl: ∀i. eq_instruction i i = true.
     417
     418definition eq_addressing_mode: addressing_mode → addressing_mode → bool ≝
     419  λa, b: addressing_mode.
     420  match a with
     421  [ DIRECT d ⇒
     422    match b with
     423    [ DIRECT e ⇒ eq_bv ? d e
     424    | _ ⇒ false
     425    ]
     426  | INDIRECT b' ⇒
     427    match b with
     428    [ INDIRECT e ⇒ eq_b b' e
     429    | _ ⇒ false
     430    ]
     431  | EXT_INDIRECT b' ⇒
     432    match b with
     433    [ EXT_INDIRECT e ⇒ eq_b b' e
     434    | _ ⇒ false
     435    ]
     436  | REGISTER bv ⇒
     437    match b with
     438    [ REGISTER bv' ⇒ eq_bv ? bv bv'
     439    | _ ⇒ false
     440    ]
     441  | ACC_A ⇒ match b with [ ACC_A ⇒ true | _ ⇒ false ]
     442  | ACC_B ⇒ match b with [ ACC_B ⇒ true | _ ⇒ false ]
     443  | DPTR ⇒ match b with [ DPTR ⇒ true | _ ⇒ false ]
     444  | DATA b' ⇒
     445    match b with
     446    [ DATA e ⇒ eq_bv ? b' e
     447    | _ ⇒ false
     448    ]
     449  | DATA16 w ⇒
     450    match b with
     451    [ DATA16 e ⇒ eq_bv ? w e
     452    | _ ⇒ false
     453    ]
     454  | ACC_DPTR ⇒ match b with [ ACC_DPTR ⇒ true | _ ⇒ false ]
     455  | ACC_PC ⇒ match b with [ ACC_PC ⇒ true | _ ⇒ false ]
     456  | EXT_INDIRECT_DPTR ⇒ match b with [ EXT_INDIRECT_DPTR ⇒ true | _ ⇒ false ]
     457  | INDIRECT_DPTR ⇒ match b with [ INDIRECT_DPTR ⇒ true | _ ⇒ false ]
     458  | CARRY ⇒ match b with [ CARRY ⇒ true | _ ⇒ false ]
     459  | BIT_ADDR b' ⇒
     460    match b with
     461    [ BIT_ADDR e ⇒ eq_bv ? b' e
     462    | _ ⇒ false
     463    ]
     464  | N_BIT_ADDR b' ⇒
     465    match b with
     466    [ N_BIT_ADDR e ⇒ eq_bv ? b' e
     467    | _ ⇒ false
     468    ]
     469  | RELATIVE n ⇒
     470    match b with
     471    [ RELATIVE e ⇒ eq_bv ? n e
     472    | _ ⇒ false
     473    ]
     474  | ADDR11 w ⇒
     475    match b with
     476    [ ADDR11 e ⇒ eq_bv ? w e
     477    | _ ⇒ false
     478    ]
     479  | ADDR16 w ⇒
     480    match b with
     481    [ ADDR16 e ⇒ eq_bv ? w e
     482    | _ ⇒ false
     483    ]
     484  ].
     485
     486lemma eq_bv_refl:
     487  ∀n, b.
     488    eq_bv n b b = true.
     489  #n #b cases b //
     490qed.
     491
     492lemma eq_b_refl:
     493  ∀b.
     494    eq_b b b = true.
     495  #b cases b //
     496qed.
     497
     498lemma eq_addressing_mode_refl:
     499  ∀a. eq_addressing_mode a a = true.
     500  #a cases a try #arg1 try #arg2 try @eq_bv_refl try @eq_b_refl
     501  try normalize %
     502qed.
     503 
     504definition eq_sum: ∀A, B. (A → A → bool) → (B → B → bool) → (A ⊎ B) → (A ⊎ B) → bool ≝
     505  λlt, rt, leq, req, left, right.
     506    match left with
     507    [ inl l ⇒
     508      match right with
     509      [ inl l' ⇒ leq l l'
     510      | _ ⇒ false
     511      ]
     512    | inr r ⇒
     513      match right with
     514      [ inr r' ⇒ req r r'
     515      | _ ⇒ false
     516      ]
     517    ].
     518
     519definition eq_prod: ∀A, B. (A → A → bool) → (B → B → bool) → (A × B) → (A × B) → bool ≝
     520  λlt, rt, leq, req, left, right.
     521    let 〈l, r〉 ≝ left in
     522    let 〈l', r'〉 ≝ right in
     523      leq l l' ∧ req r r'.
     524
     525definition eq_preinstruction: preinstruction [[relative]] → preinstruction [[relative]] → bool ≝
     526  λi, j.
     527  match i with
     528  [ ADD arg1 arg2 ⇒
     529    match j with
     530    [ ADD arg1' arg2' ⇒ eq_addressing_mode arg1 arg1' ∧ eq_addressing_mode arg2 arg2'
     531    | _ ⇒ false
     532    ]
     533  | ADDC arg1 arg2 ⇒
     534    match j with
     535    [ ADDC arg1' arg2' ⇒ eq_addressing_mode arg1 arg1' ∧ eq_addressing_mode arg2 arg2'
     536    | _ ⇒ false
     537    ]
     538  | SUBB arg1 arg2 ⇒
     539    match j with
     540    [ SUBB arg1' arg2' ⇒ eq_addressing_mode arg1 arg1' ∧ eq_addressing_mode arg2 arg2'
     541    | _ ⇒ false
     542    ]
     543  | INC arg ⇒
     544    match j with
     545    [ INC arg' ⇒ eq_addressing_mode arg arg'
     546    | _ ⇒ false
     547    ]
     548  | DEC arg ⇒
     549    match j with
     550    [ DEC arg' ⇒ eq_addressing_mode arg arg'
     551    | _ ⇒ false
     552    ]
     553  | MUL arg1 arg2 ⇒
     554    match j with
     555    [ MUL arg1' arg2' ⇒ eq_addressing_mode arg1 arg1' ∧ eq_addressing_mode arg2 arg2'
     556    | _ ⇒ false
     557    ]
     558  | DIV arg1 arg2 ⇒
     559    match j with
     560    [ DIV arg1' arg2' ⇒ eq_addressing_mode arg1 arg1' ∧ eq_addressing_mode arg2 arg2'
     561    | _ ⇒ false
     562    ]
     563  | DA arg ⇒
     564    match j with
     565    [ DA arg' ⇒ eq_addressing_mode arg arg'
     566    | _ ⇒ false
     567    ]
     568  | JC arg ⇒
     569    match j with
     570    [ JC arg' ⇒ eq_addressing_mode arg arg'
     571    | _ ⇒ false
     572    ]
     573  | JNC arg ⇒
     574    match j with
     575    [ JNC arg' ⇒ eq_addressing_mode arg arg'
     576    | _ ⇒ false
     577    ]
     578  | JB arg1 arg2 ⇒
     579    match j with
     580    [ JB arg1' arg2' ⇒ eq_addressing_mode arg1 arg1' ∧ eq_addressing_mode arg2 arg2'
     581    | _ ⇒ false
     582    ]
     583  | JNB arg1 arg2 ⇒
     584    match j with
     585    [ JNB arg1' arg2' ⇒ eq_addressing_mode arg1 arg1' ∧ eq_addressing_mode arg2 arg2'
     586    | _ ⇒ false
     587    ]
     588  | JBC arg1 arg2 ⇒
     589    match j with
     590    [ JBC arg1' arg2' ⇒ eq_addressing_mode arg1 arg1' ∧ eq_addressing_mode arg2 arg2'
     591    | _ ⇒ false
     592    ]
     593  | JZ arg ⇒
     594    match j with
     595    [ JZ arg' ⇒ eq_addressing_mode arg arg'
     596    | _ ⇒ false
     597    ]
     598  | JNZ arg ⇒
     599    match j with
     600    [ JNZ arg' ⇒ eq_addressing_mode arg arg'
     601    | _ ⇒ false
     602    ]
     603  | CJNE arg1 arg2 ⇒
     604    match j with
     605    [ CJNE arg1' arg2' ⇒
     606      let prod_eq_left ≝ eq_prod [[acc_a]] [[direct; data]] eq_addressing_mode eq_addressing_mode in
     607      let prod_eq_right ≝ eq_prod [[registr; indirect]] [[data]] eq_addressing_mode eq_addressing_mode in
     608      let arg1_eq ≝ eq_sum ? ? prod_eq_left prod_eq_right in
     609        arg1_eq arg1 arg1' ∧ eq_addressing_mode arg2 arg2'
     610    | _ ⇒ false
     611    ]
     612  | DJNZ arg1 arg2 ⇒
     613    match j with
     614    [ DJNZ arg1' arg2' ⇒ eq_addressing_mode arg1 arg1' ∧ eq_addressing_mode arg2 arg2'
     615    | _ ⇒ false
     616    ]
     617  | CLR arg ⇒
     618    match j with
     619    [ CLR arg' ⇒ eq_addressing_mode arg arg'
     620    | _ ⇒ false
     621    ]
     622  | CPL arg ⇒
     623    match j with
     624    [ CPL arg' ⇒ eq_addressing_mode arg arg'
     625    | _ ⇒ false
     626    ]
     627  | RL arg ⇒
     628    match j with
     629    [ RL arg' ⇒ eq_addressing_mode arg arg'
     630    | _ ⇒ false
     631    ]
     632  | RLC arg ⇒
     633    match j with
     634    [ RLC arg' ⇒ eq_addressing_mode arg arg'
     635    | _ ⇒ false
     636    ]
     637  | RR arg ⇒
     638    match j with
     639    [ RR arg' ⇒ eq_addressing_mode arg arg'
     640    | _ ⇒ false
     641    ]
     642  | RRC arg ⇒
     643    match j with
     644    [ RRC arg' ⇒ eq_addressing_mode arg arg'
     645    | _ ⇒ false
     646    ]
     647  | SWAP arg ⇒
     648    match j with
     649    [ SWAP arg' ⇒ eq_addressing_mode arg arg'
     650    | _ ⇒ false
     651    ]
     652  | SETB arg ⇒
     653    match j with
     654    [ SETB arg' ⇒ eq_addressing_mode arg arg'
     655    | _ ⇒ false
     656    ]
     657  | PUSH arg ⇒
     658    match j with
     659    [ PUSH arg' ⇒ eq_addressing_mode arg arg'
     660    | _ ⇒ false
     661    ]
     662  | POP arg ⇒
     663    match j with
     664    [ POP arg' ⇒ eq_addressing_mode arg arg'
     665    | _ ⇒ false
     666    ]
     667  | XCH arg1 arg2 ⇒
     668    match j with
     669    [ XCH arg1' arg2' ⇒ eq_addressing_mode arg1 arg1' ∧ eq_addressing_mode arg2 arg2'
     670    | _ ⇒ false
     671    ]
     672  | XCHD arg1 arg2 ⇒
     673    match j with
     674    [ XCHD arg1' arg2' ⇒ eq_addressing_mode arg1 arg1' ∧ eq_addressing_mode arg2 arg2'
     675    | _ ⇒ false
     676    ]
     677  | RET ⇒ match j with [ RET ⇒ true | _ ⇒ false ]
     678  | RETI ⇒ match j with [ RETI ⇒ true | _ ⇒ false ]
     679  | NOP ⇒ match j with [ NOP ⇒ true | _ ⇒ false ]
     680  | MOVX arg ⇒
     681    match j with
     682    [ MOVX arg' ⇒
     683      let prod_eq_left ≝ eq_prod [[acc_a]] [[ext_indirect; ext_indirect_dptr]] eq_addressing_mode eq_addressing_mode in
     684      let prod_eq_right ≝ eq_prod [[ext_indirect; ext_indirect_dptr]] [[acc_a]] eq_addressing_mode eq_addressing_mode in
     685      let sum_eq ≝ eq_sum ? ? prod_eq_left prod_eq_right in
     686        sum_eq arg arg'
     687    | _ ⇒ false
     688    ]
     689  | XRL arg ⇒
     690    match j with
     691    [ XRL arg' ⇒
     692      let prod_eq_left ≝ eq_prod [[acc_a]] [[ data ; registr ; direct ; indirect ]] eq_addressing_mode eq_addressing_mode in
     693      let prod_eq_right ≝ eq_prod [[direct]] [[ acc_a ; data ]] eq_addressing_mode eq_addressing_mode in
     694      let sum_eq ≝ eq_sum ? ? prod_eq_left prod_eq_right in
     695        sum_eq arg arg'
     696    | _ ⇒ false
     697    ]
     698  | ORL arg ⇒
     699    match j with
     700    [ ORL arg' ⇒
     701      let prod_eq_left1 ≝ eq_prod [[acc_a]] [[ registr ; data ; direct ; indirect ]] eq_addressing_mode eq_addressing_mode in
     702      let prod_eq_left2 ≝ eq_prod [[direct]] [[ acc_a; data ]] eq_addressing_mode eq_addressing_mode in
     703      let prod_eq_left ≝ eq_sum ? ? prod_eq_left1 prod_eq_left2 in
     704      let prod_eq_right ≝ eq_prod [[carry]] [[ bit_addr ; n_bit_addr]] eq_addressing_mode eq_addressing_mode in
     705      let sum_eq ≝ eq_sum ? ? prod_eq_left prod_eq_right in
     706        sum_eq arg arg'
     707    | _ ⇒ false
     708    ]
     709  | ANL arg ⇒
     710    match j with
     711    [ ANL arg' ⇒
     712      let prod_eq_left1 ≝ eq_prod [[acc_a]] [[ registr ; direct ; indirect ; data ]] eq_addressing_mode eq_addressing_mode in
     713      let prod_eq_left2 ≝ eq_prod [[direct]] [[ acc_a; data ]] eq_addressing_mode eq_addressing_mode in
     714      let prod_eq_left ≝ eq_sum ? ? prod_eq_left1 prod_eq_left2 in
     715      let prod_eq_right ≝ eq_prod [[carry]] [[ bit_addr ; n_bit_addr]] eq_addressing_mode eq_addressing_mode in
     716      let sum_eq ≝ eq_sum ? ? prod_eq_left prod_eq_right in
     717        sum_eq arg arg'
     718    | _ ⇒ false
     719    ]
     720  | MOV arg ⇒
     721    match j with
     722    [ MOV arg' ⇒
     723      let prod_eq_6 ≝ eq_prod [[acc_a]] [[registr; direct; indirect; data]] eq_addressing_mode eq_addressing_mode in
     724      let prod_eq_5 ≝ eq_prod [[registr; indirect]] [[acc_a; direct; data]] eq_addressing_mode eq_addressing_mode in
     725      let prod_eq_4 ≝ eq_prod [[direct]] [[acc_a; registr; direct; indirect; data]] eq_addressing_mode eq_addressing_mode in
     726      let prod_eq_3 ≝ eq_prod [[dptr]] [[data16]] eq_addressing_mode eq_addressing_mode in
     727      let prod_eq_2 ≝ eq_prod [[carry]] [[bit_addr]] eq_addressing_mode eq_addressing_mode in
     728      let prod_eq_1 ≝ eq_prod [[bit_addr]] [[carry]] eq_addressing_mode eq_addressing_mode in
     729      let sum_eq_1 ≝ eq_sum ? ? prod_eq_6 prod_eq_5 in
     730      let sum_eq_2 ≝ eq_sum ? ? sum_eq_1 prod_eq_4 in
     731      let sum_eq_3 ≝ eq_sum ? ? sum_eq_2 prod_eq_3 in
     732      let sum_eq_4 ≝ eq_sum ? ? sum_eq_3 prod_eq_2 in
     733      let sum_eq_5 ≝ eq_sum ? ? sum_eq_4 prod_eq_1 in
     734        sum_eq_5 arg arg'
     735    | _ ⇒ false
     736    ]
     737  ].
     738
     739lemma eq_sum_refl:
     740  ∀A, B: Type[0].
     741  ∀leq, req.
     742  ∀s.
     743  ∀leq_refl: (∀t. leq t t = true).
     744  ∀req_refl: (∀u. req u u = true).
     745    eq_sum A B leq req s s = true.
     746  #A #B #leq #req #s #leq_refl #req_refl
     747  cases s whd in ⊢ (? → ??%?) //
     748qed.
     749
     750lemma eq_prod_refl:
     751  ∀A, B: Type[0].
     752  ∀leq, req.
     753  ∀s.
     754  ∀leq_refl: (∀t. leq t t = true).
     755  ∀req_refl: (∀u. req u u = true).
     756    eq_prod A B leq req s s = true.
     757  #A #B #leq #req #s #leq_refl #req_refl
     758  cases s whd in ⊢ (? → ? → ??%?) #l #r >leq_refl normalize @req_refl
     759qed.
     760
     761lemma eq_preinstruction_refl:
     762  ∀i.
     763    eq_preinstruction i i = true.
     764  #i cases i try #arg1 try #arg2
     765  try @eq_addressing_mode_refl
     766  [1,2,3,4,5,6,7,8,10,16,17,18,19,20:
     767    whd in ⊢ (??%?)
     768    try %
     769    >eq_addressing_mode_refl
     770    >eq_addressing_mode_refl %
     771  |13,15:
     772    whd in ⊢ (??%?)
     773    cases arg1
     774    [*:
     775      #arg1_left normalize nodelta
     776      >eq_prod_refl [*: try % #argr @eq_addressing_mode_refl]
     777    ]
     778  |11,12:
     779    whd in ⊢ (??%?)
     780    cases arg1
     781    [1:
     782      #arg1_left normalize nodelta
     783      >(eq_sum_refl …)
     784      [1: % | 2,3: #arg @eq_prod_refl ]
     785      @eq_addressing_mode_refl
     786    |2:
     787      #arg1_left normalize nodelta
     788      @eq_prod_refl [*: @eq_addressing_mode_refl ]
     789    |3:
     790      #arg1_left normalize nodelta
     791      >(eq_sum_refl …) [1: %
     792      |2,3: #arg @eq_prod_refl #arg @eq_addressing_mode_refl ]
     793    |4:
     794      #arg1_left normalize nodelta
     795      @eq_prod_refl [*: #arg @eq_addressing_mode_refl ]
     796    ]
     797  |14:
     798    whd in ⊢ (??%?)
     799    cases arg1
     800    [ #arg1_left normalize nodelta
     801      @eq_sum_refl
     802      [1: #arg @eq_sum_refl
     803        [1: #arg @eq_sum_refl
     804          [1: #arg @eq_sum_refl
     805            [1: #arg @eq_prod_refl
     806              [*: @eq_addressing_mode_refl ]
     807            |2: #arg @eq_prod_refl
     808              [*: #arg @eq_addressing_mode_refl ]
     809            ]
     810          |2: #arg @eq_prod_refl
     811            [*: #arg @eq_addressing_mode_refl ]
     812          ]
     813        |2: #arg @eq_prod_refl
     814          [*: #arg @eq_addressing_mode_refl ]
     815        ]
     816      |2: #arg @eq_prod_refl
     817        [*: #arg @eq_addressing_mode_refl ]
     818      ]
     819    |2: #arg1_right normalize nodelta
     820        @eq_prod_refl [*: #arg @eq_addressing_mode_refl ]
     821    ]
     822  |*:
     823    whd in ⊢ (??%?)
     824    cases arg1
     825    [*: #arg1 >eq_sum_refl
     826      [1,4: normalize @eq_addressing_mode_refl
     827      |2,3,5,6: #arg @eq_prod_refl
     828        [*: #arg @eq_addressing_mode_refl ]
     829      ]
     830    ]
     831  ]
     832qed.
     833
     834definition eq_instruction: instruction → instruction → bool ≝
     835  λi, j.
     836  match i with
     837  [ ACALL arg ⇒
     838    match j with
     839    [ ACALL arg' ⇒ eq_addressing_mode arg arg'
     840    | _ ⇒ false
     841    ]
     842  | LCALL arg ⇒
     843    match j with
     844    [ LCALL arg' ⇒ eq_addressing_mode arg arg'
     845    | _ ⇒ false
     846    ]
     847  | AJMP arg ⇒
     848    match j with
     849    [ AJMP arg' ⇒ eq_addressing_mode arg arg'
     850    | _ ⇒ false
     851    ]
     852  | LJMP arg ⇒
     853    match j with
     854    [ LJMP arg' ⇒ eq_addressing_mode arg arg'
     855    | _ ⇒ false
     856    ]
     857  | SJMP arg ⇒
     858    match j with
     859    [ SJMP arg' ⇒ eq_addressing_mode arg arg'
     860    | _ ⇒ false
     861    ]
     862  | JMP arg ⇒
     863    match j with
     864    [ JMP arg' ⇒ eq_addressing_mode arg arg'
     865    | _ ⇒ false
     866    ]
     867  | MOVC arg1 arg2 ⇒
     868    match j with
     869    [ MOVC arg1' arg2' ⇒ eq_addressing_mode arg1 arg1' ∧ eq_addressing_mode arg2 arg2'
     870    | _ ⇒ false
     871    ]
     872  | RealInstruction instr ⇒
     873    match j with
     874    [ RealInstruction instr' ⇒ eq_preinstruction instr instr'
     875    | _ ⇒ false
     876    ]
     877  ].
     878 
     879lemma eq_instruction_refl:
     880  ∀i. eq_instruction i i = true.
     881  #i cases i
     882  [1,2,3,4,5,6: #arg1 @eq_addressing_mode_refl
     883  |7: #arg1 #arg2
     884      whd in ⊢ (??%?)
     885      >eq_addressing_mode_refl
     886      >eq_addressing_mode_refl
     887      %
     888  |8: #arg @eq_preinstruction_refl
     889  ]
     890qed.
    419891
    420892let rec vect_member
Note: See TracChangeset for help on using the changeset viewer.