Changeset 2124 for src/ASM/ASM.ma


Ignore:
Timestamp:
Jun 27, 2012, 4:23:54 PM (8 years ago)
Author:
sacerdot
Message:

Much more shuffling around to proper places

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/ASM.ma

    r2123 r2124  
    2828| ADDR11: Word11 → addressing_mode
    2929| ADDR16: Word → addressing_mode.
     30
     31definition eq_addressing_mode: addressing_mode → addressing_mode → bool ≝
     32  λa, b: addressing_mode.
     33  match a with
     34  [ DIRECT d ⇒
     35    match b with
     36    [ DIRECT e ⇒ eq_bv ? d e
     37    | _ ⇒ false
     38    ]
     39  | INDIRECT b' ⇒
     40    match b with
     41    [ INDIRECT e ⇒ eq_b b' e
     42    | _ ⇒ false
     43    ]
     44  | EXT_INDIRECT b' ⇒
     45    match b with
     46    [ EXT_INDIRECT e ⇒ eq_b b' e
     47    | _ ⇒ false
     48    ]
     49  | REGISTER bv ⇒
     50    match b with
     51    [ REGISTER bv' ⇒ eq_bv ? bv bv'
     52    | _ ⇒ false
     53    ]
     54  | ACC_A ⇒ match b with [ ACC_A ⇒ true | _ ⇒ false ]
     55  | ACC_B ⇒ match b with [ ACC_B ⇒ true | _ ⇒ false ]
     56  | DPTR ⇒ match b with [ DPTR ⇒ true | _ ⇒ false ]
     57  | DATA b' ⇒
     58    match b with
     59    [ DATA e ⇒ eq_bv ? b' e
     60    | _ ⇒ false
     61    ]
     62  | DATA16 w ⇒
     63    match b with
     64    [ DATA16 e ⇒ eq_bv ? w e
     65    | _ ⇒ false
     66    ]
     67  | ACC_DPTR ⇒ match b with [ ACC_DPTR ⇒ true | _ ⇒ false ]
     68  | ACC_PC ⇒ match b with [ ACC_PC ⇒ true | _ ⇒ false ]
     69  | EXT_INDIRECT_DPTR ⇒ match b with [ EXT_INDIRECT_DPTR ⇒ true | _ ⇒ false ]
     70  | INDIRECT_DPTR ⇒ match b with [ INDIRECT_DPTR ⇒ true | _ ⇒ false ]
     71  | CARRY ⇒ match b with [ CARRY ⇒ true | _ ⇒ false ]
     72  | BIT_ADDR b' ⇒
     73    match b with
     74    [ BIT_ADDR e ⇒ eq_bv ? b' e
     75    | _ ⇒ false
     76    ]
     77  | N_BIT_ADDR b' ⇒
     78    match b with
     79    [ N_BIT_ADDR e ⇒ eq_bv ? b' e
     80    | _ ⇒ false
     81    ]
     82  | RELATIVE n ⇒
     83    match b with
     84    [ RELATIVE e ⇒ eq_bv ? n e
     85    | _ ⇒ false
     86    ]
     87  | ADDR11 w ⇒
     88    match b with
     89    [ ADDR11 e ⇒ eq_bv ? w e
     90    | _ ⇒ false
     91    ]
     92  | ADDR16 w ⇒
     93    match b with
     94    [ ADDR16 e ⇒ eq_bv ? w e
     95    | _ ⇒ false
     96    ]
     97  ].
     98
     99lemma eq_addressing_mode_refl:
     100  ∀a. eq_addressing_mode a a = true.
     101  #a
     102  cases a try #arg1 try #arg2
     103  try @eq_bv_refl try @eq_b_refl
     104  try normalize %
     105qed.
    30106
    31107(* dpm: renamed register to registr to avoid clash with brian's types *)
     
    161237  | VCons m he (tl: Vector addressing_mode_tag m) ⇒
    162238     is_a he A ∨ is_in ? tl A ].
     239
     240definition is_in_cons_elim:
     241 ∀len.∀hd,tl.∀m:addressing_mode
     242  .is_in (S len) (hd:::tl) m →
     243    (bool_to_Prop (is_a hd m)) ∨ (bool_to_Prop (is_in len tl m)).
     244 #len #hd #tl #am #ISIN whd in match (is_in ???) in ISIN;
     245 cases (is_a hd am) in ISIN; /2/
     246qed.
    163247
    164248lemma is_a_to_mem_to_is_in:
     
    425509| NOP: preinstruction A.
    426510
     511definition eq_preinstruction: preinstruction [[relative]] → preinstruction [[relative]] → bool ≝
     512  λi, j.
     513  match i with
     514  [ ADD arg1 arg2 ⇒
     515    match j with
     516    [ ADD arg1' arg2' ⇒ eq_addressing_mode arg1 arg1' ∧ eq_addressing_mode arg2 arg2'
     517    | _ ⇒ false
     518    ]
     519  | ADDC arg1 arg2 ⇒
     520    match j with
     521    [ ADDC arg1' arg2' ⇒ eq_addressing_mode arg1 arg1' ∧ eq_addressing_mode arg2 arg2'
     522    | _ ⇒ false
     523    ]
     524  | SUBB arg1 arg2 ⇒
     525    match j with
     526    [ SUBB arg1' arg2' ⇒ eq_addressing_mode arg1 arg1' ∧ eq_addressing_mode arg2 arg2'
     527    | _ ⇒ false
     528    ]
     529  | INC arg ⇒
     530    match j with
     531    [ INC arg' ⇒ eq_addressing_mode arg arg'
     532    | _ ⇒ false
     533    ]
     534  | DEC arg ⇒
     535    match j with
     536    [ DEC arg' ⇒ eq_addressing_mode arg arg'
     537    | _ ⇒ false
     538    ]
     539  | MUL arg1 arg2 ⇒
     540    match j with
     541    [ MUL arg1' arg2' ⇒ eq_addressing_mode arg1 arg1' ∧ eq_addressing_mode arg2 arg2'
     542    | _ ⇒ false
     543    ]
     544  | DIV arg1 arg2 ⇒
     545    match j with
     546    [ DIV arg1' arg2' ⇒ eq_addressing_mode arg1 arg1' ∧ eq_addressing_mode arg2 arg2'
     547    | _ ⇒ false
     548    ]
     549  | DA arg ⇒
     550    match j with
     551    [ DA arg' ⇒ eq_addressing_mode arg arg'
     552    | _ ⇒ false
     553    ]
     554  | JC arg ⇒
     555    match j with
     556    [ JC arg' ⇒ eq_addressing_mode arg arg'
     557    | _ ⇒ false
     558    ]
     559  | JNC arg ⇒
     560    match j with
     561    [ JNC arg' ⇒ eq_addressing_mode arg arg'
     562    | _ ⇒ false
     563    ]
     564  | JB arg1 arg2 ⇒
     565    match j with
     566    [ JB arg1' arg2' ⇒ eq_addressing_mode arg1 arg1' ∧ eq_addressing_mode arg2 arg2'
     567    | _ ⇒ false
     568    ]
     569  | JNB arg1 arg2 ⇒
     570    match j with
     571    [ JNB arg1' arg2' ⇒ eq_addressing_mode arg1 arg1' ∧ eq_addressing_mode arg2 arg2'
     572    | _ ⇒ false
     573    ]
     574  | JBC arg1 arg2 ⇒
     575    match j with
     576    [ JBC arg1' arg2' ⇒ eq_addressing_mode arg1 arg1' ∧ eq_addressing_mode arg2 arg2'
     577    | _ ⇒ false
     578    ]
     579  | JZ arg ⇒
     580    match j with
     581    [ JZ arg' ⇒ eq_addressing_mode arg arg'
     582    | _ ⇒ false
     583    ]
     584  | JNZ arg ⇒
     585    match j with
     586    [ JNZ arg' ⇒ eq_addressing_mode arg arg'
     587    | _ ⇒ false
     588    ]
     589  | CJNE arg1 arg2 ⇒
     590    match j with
     591    [ CJNE arg1' arg2' ⇒
     592      let prod_eq_left ≝ eq_prod [[acc_a]] [[direct; data]] eq_addressing_mode eq_addressing_mode in
     593      let prod_eq_right ≝ eq_prod [[registr; indirect]] [[data]] eq_addressing_mode eq_addressing_mode in
     594      let arg1_eq ≝ eq_sum ? ? prod_eq_left prod_eq_right in
     595        arg1_eq arg1 arg1' ∧ eq_addressing_mode arg2 arg2'
     596    | _ ⇒ false
     597    ]
     598  | DJNZ arg1 arg2 ⇒
     599    match j with
     600    [ DJNZ arg1' arg2' ⇒ eq_addressing_mode arg1 arg1' ∧ eq_addressing_mode arg2 arg2'
     601    | _ ⇒ false
     602    ]
     603  | CLR arg ⇒
     604    match j with
     605    [ CLR arg' ⇒ eq_addressing_mode arg arg'
     606    | _ ⇒ false
     607    ]
     608  | CPL arg ⇒
     609    match j with
     610    [ CPL arg' ⇒ eq_addressing_mode arg arg'
     611    | _ ⇒ false
     612    ]
     613  | RL arg ⇒
     614    match j with
     615    [ RL arg' ⇒ eq_addressing_mode arg arg'
     616    | _ ⇒ false
     617    ]
     618  | RLC arg ⇒
     619    match j with
     620    [ RLC arg' ⇒ eq_addressing_mode arg arg'
     621    | _ ⇒ false
     622    ]
     623  | RR arg ⇒
     624    match j with
     625    [ RR arg' ⇒ eq_addressing_mode arg arg'
     626    | _ ⇒ false
     627    ]
     628  | RRC arg ⇒
     629    match j with
     630    [ RRC arg' ⇒ eq_addressing_mode arg arg'
     631    | _ ⇒ false
     632    ]
     633  | SWAP arg ⇒
     634    match j with
     635    [ SWAP arg' ⇒ eq_addressing_mode arg arg'
     636    | _ ⇒ false
     637    ]
     638  | SETB arg ⇒
     639    match j with
     640    [ SETB arg' ⇒ eq_addressing_mode arg arg'
     641    | _ ⇒ false
     642    ]
     643  | PUSH arg ⇒
     644    match j with
     645    [ PUSH arg' ⇒ eq_addressing_mode arg arg'
     646    | _ ⇒ false
     647    ]
     648  | POP arg ⇒
     649    match j with
     650    [ POP arg' ⇒ eq_addressing_mode arg arg'
     651    | _ ⇒ false
     652    ]
     653  | XCH arg1 arg2 ⇒
     654    match j with
     655    [ XCH arg1' arg2' ⇒ eq_addressing_mode arg1 arg1' ∧ eq_addressing_mode arg2 arg2'
     656    | _ ⇒ false
     657    ]
     658  | XCHD arg1 arg2 ⇒
     659    match j with
     660    [ XCHD arg1' arg2' ⇒ eq_addressing_mode arg1 arg1' ∧ eq_addressing_mode arg2 arg2'
     661    | _ ⇒ false
     662    ]
     663  | RET ⇒ match j with [ RET ⇒ true | _ ⇒ false ]
     664  | RETI ⇒ match j with [ RETI ⇒ true | _ ⇒ false ]
     665  | NOP ⇒ match j with [ NOP ⇒ true | _ ⇒ false ]
     666  | MOVX arg ⇒
     667    match j with
     668    [ MOVX arg' ⇒
     669      let prod_eq_left ≝ eq_prod [[acc_a]] [[ext_indirect; ext_indirect_dptr]] eq_addressing_mode eq_addressing_mode in
     670      let prod_eq_right ≝ eq_prod [[ext_indirect; ext_indirect_dptr]] [[acc_a]] eq_addressing_mode eq_addressing_mode in
     671      let sum_eq ≝ eq_sum ? ? prod_eq_left prod_eq_right in
     672        sum_eq arg arg'
     673    | _ ⇒ false
     674    ]
     675  | XRL arg ⇒
     676    match j with
     677    [ XRL arg' ⇒
     678      let prod_eq_left ≝ eq_prod [[acc_a]] [[ data ; registr ; direct ; indirect ]] eq_addressing_mode eq_addressing_mode in
     679      let prod_eq_right ≝ eq_prod [[direct]] [[ acc_a ; data ]] eq_addressing_mode eq_addressing_mode in
     680      let sum_eq ≝ eq_sum ? ? prod_eq_left prod_eq_right in
     681        sum_eq arg arg'
     682    | _ ⇒ false
     683    ]
     684  | ORL arg ⇒
     685    match j with
     686    [ ORL arg' ⇒
     687      let prod_eq_left1 ≝ eq_prod [[acc_a]] [[ registr ; data ; direct ; indirect ]] eq_addressing_mode eq_addressing_mode in
     688      let prod_eq_left2 ≝ eq_prod [[direct]] [[ acc_a; data ]] eq_addressing_mode eq_addressing_mode in
     689      let prod_eq_left ≝ eq_sum ? ? prod_eq_left1 prod_eq_left2 in
     690      let prod_eq_right ≝ eq_prod [[carry]] [[ bit_addr ; n_bit_addr]] eq_addressing_mode eq_addressing_mode in
     691      let sum_eq ≝ eq_sum ? ? prod_eq_left prod_eq_right in
     692        sum_eq arg arg'
     693    | _ ⇒ false
     694    ]
     695  | ANL arg ⇒
     696    match j with
     697    [ ANL arg' ⇒
     698      let prod_eq_left1 ≝ eq_prod [[acc_a]] [[ registr ; direct ; indirect ; data ]] eq_addressing_mode eq_addressing_mode in
     699      let prod_eq_left2 ≝ eq_prod [[direct]] [[ acc_a; data ]] eq_addressing_mode eq_addressing_mode in
     700      let prod_eq_left ≝ eq_sum ? ? prod_eq_left1 prod_eq_left2 in
     701      let prod_eq_right ≝ eq_prod [[carry]] [[ bit_addr ; n_bit_addr]] eq_addressing_mode eq_addressing_mode in
     702      let sum_eq ≝ eq_sum ? ? prod_eq_left prod_eq_right in
     703        sum_eq arg arg'
     704    | _ ⇒ false
     705    ]
     706  | MOV arg ⇒
     707    match j with
     708    [ MOV arg' ⇒
     709      let prod_eq_6 ≝ eq_prod [[acc_a]] [[registr; direct; indirect; data]] eq_addressing_mode eq_addressing_mode in
     710      let prod_eq_5 ≝ eq_prod [[registr; indirect]] [[acc_a; direct; data]] eq_addressing_mode eq_addressing_mode in
     711      let prod_eq_4 ≝ eq_prod [[direct]] [[acc_a; registr; direct; indirect; data]] eq_addressing_mode eq_addressing_mode in
     712      let prod_eq_3 ≝ eq_prod [[dptr]] [[data16]] eq_addressing_mode eq_addressing_mode in
     713      let prod_eq_2 ≝ eq_prod [[carry]] [[bit_addr]] eq_addressing_mode eq_addressing_mode in
     714      let prod_eq_1 ≝ eq_prod [[bit_addr]] [[carry]] eq_addressing_mode eq_addressing_mode in
     715      let sum_eq_1 ≝ eq_sum ? ? prod_eq_6 prod_eq_5 in
     716      let sum_eq_2 ≝ eq_sum ? ? sum_eq_1 prod_eq_4 in
     717      let sum_eq_3 ≝ eq_sum ? ? sum_eq_2 prod_eq_3 in
     718      let sum_eq_4 ≝ eq_sum ? ? sum_eq_3 prod_eq_2 in
     719      let sum_eq_5 ≝ eq_sum ? ? sum_eq_4 prod_eq_1 in
     720        sum_eq_5 arg arg'
     721    | _ ⇒ false
     722    ]
     723  ].
     724
     725lemma eq_preinstruction_refl:
     726  ∀i.
     727    eq_preinstruction i i = true.
     728  #i cases i try #arg1 try #arg2
     729  try @eq_addressing_mode_refl
     730  [1,2,3,4,5,6,7,8,10,16,17,18,19,20:
     731    whd in ⊢ (??%?); try %
     732    >eq_addressing_mode_refl
     733    >eq_addressing_mode_refl %
     734  |13,15:
     735    whd in ⊢ (??%?);
     736    cases arg1
     737    [*:
     738      #arg1_left normalize nodelta
     739      >eq_prod_refl [*: try % #argr @eq_addressing_mode_refl]
     740    ]
     741  |11,12:
     742    whd in ⊢ (??%?);
     743    cases arg1
     744    [1:
     745      #arg1_left normalize nodelta
     746      >(eq_sum_refl …)
     747      [1: % | 2,3: #arg @eq_prod_refl ]
     748      @eq_addressing_mode_refl
     749    |2:
     750      #arg1_left normalize nodelta
     751      @eq_prod_refl [*: @eq_addressing_mode_refl ]
     752    |3:
     753      #arg1_left normalize nodelta
     754      >(eq_sum_refl …)
     755      [1:
     756        %
     757      |2,3:
     758        #arg @eq_prod_refl #arg @eq_addressing_mode_refl
     759      ]
     760    |4:
     761      #arg1_left normalize nodelta
     762      @eq_prod_refl [*: #arg @eq_addressing_mode_refl ]
     763    ]
     764  |14:
     765    whd in ⊢ (??%?);
     766    cases arg1
     767    [1:
     768      #arg1_left normalize nodelta
     769      @eq_sum_refl
     770      [1:
     771        #arg @eq_sum_refl
     772        [1:
     773          #arg @eq_sum_refl
     774          [1:
     775            #arg @eq_sum_refl
     776            [1:
     777              #arg @eq_prod_refl
     778              [*:
     779                @eq_addressing_mode_refl
     780              ]
     781            |2:
     782              #arg @eq_prod_refl
     783              [*:
     784                #arg @eq_addressing_mode_refl
     785              ]
     786            ]
     787          |2:
     788            #arg @eq_prod_refl
     789            [*:
     790              #arg @eq_addressing_mode_refl
     791            ]
     792          ]
     793        |2:
     794          #arg @eq_prod_refl
     795          [*:
     796            #arg @eq_addressing_mode_refl
     797          ]
     798        ]
     799      |2:
     800        #arg @eq_prod_refl
     801        [*:
     802          #arg @eq_addressing_mode_refl
     803        ]
     804      ]
     805    |2:
     806      #arg1_right normalize nodelta
     807      @eq_prod_refl
     808      [*:
     809        #arg @eq_addressing_mode_refl
     810      ]
     811    ]
     812  |*:
     813    whd in ⊢ (??%?);
     814    cases arg1
     815    [*:
     816      #arg1 >eq_sum_refl
     817      [1,4:
     818        @eq_addressing_mode_refl
     819      |2,3,5,6:
     820        #arg @eq_prod_refl
     821        [*:
     822          #arg @eq_addressing_mode_refl
     823        ]
     824      ]
     825    ]
     826  ]
     827qed.
     828
    427829inductive instruction: Type[0] ≝
    428830  | ACALL: [[addr11]] → instruction
     
    437839coercion RealInstruction: ∀p: preinstruction [[ relative ]]. instruction ≝
    438840  RealInstruction on _p: preinstruction ? to instruction.
     841
     842definition eq_instruction: instruction → instruction → bool ≝
     843  λi, j.
     844  match i with
     845  [ ACALL arg ⇒
     846    match j with
     847    [ ACALL arg' ⇒ eq_addressing_mode arg arg'
     848    | _ ⇒ false
     849    ]
     850  | LCALL arg ⇒
     851    match j with
     852    [ LCALL arg' ⇒ eq_addressing_mode arg arg'
     853    | _ ⇒ false
     854    ]
     855  | AJMP arg ⇒
     856    match j with
     857    [ AJMP arg' ⇒ eq_addressing_mode arg arg'
     858    | _ ⇒ false
     859    ]
     860  | LJMP arg ⇒
     861    match j with
     862    [ LJMP arg' ⇒ eq_addressing_mode arg arg'
     863    | _ ⇒ false
     864    ]
     865  | SJMP arg ⇒
     866    match j with
     867    [ SJMP arg' ⇒ eq_addressing_mode arg arg'
     868    | _ ⇒ false
     869    ]
     870  | JMP arg ⇒
     871    match j with
     872    [ JMP arg' ⇒ eq_addressing_mode arg arg'
     873    | _ ⇒ false
     874    ]
     875  | MOVC arg1 arg2 ⇒
     876    match j with
     877    [ MOVC arg1' arg2' ⇒ eq_addressing_mode arg1 arg1' ∧ eq_addressing_mode arg2 arg2'
     878    | _ ⇒ false
     879    ]
     880  | RealInstruction instr ⇒
     881    match j with
     882    [ RealInstruction instr' ⇒ eq_preinstruction instr instr'
     883    | _ ⇒ false
     884    ]
     885  ].
     886 
     887lemma eq_instruction_refl:
     888  ∀i. eq_instruction i i = true.
     889  #i cases i [*: #arg1 ]
     890  try @eq_addressing_mode_refl
     891  try @eq_preinstruction_refl
     892  #arg2 whd in ⊢ (??%?);
     893  >eq_addressing_mode_refl >eq_addressing_mode_refl %
     894qed.
     895
     896lemma eq_instruction_to_eq:
     897  ∀i1, i2: instruction.
     898    eq_instruction i1 i2 = true → i1 ≃ i2.
     899  #i1 #i2
     900  cases i1 cases i2 cases daemon (* easy but tedious
     901  [1,10,19,28,37,46:
     902    #arg1 #arg2
     903    whd in match (eq_instruction ??);
     904    cases arg1 #subaddressing_mode
     905    cases subaddressing_mode
     906    try (#arg1' #arg2' normalize in ⊢ (% → ?); #absurd cases absurd @I)
     907    try (#arg1' normalize in ⊢ (% → ?); #absurd cases absurd @I)
     908    try (normalize in ⊢ (% → ?); #absurd cases absurd @I)
     909    #word11 #irrelevant
     910    cases arg2 #subaddressing_mode
     911    cases subaddressing_mode
     912    try (#arg1' #arg2' normalize in ⊢ (% → ?); #absurd cases absurd @I)
     913    try (#arg1' normalize in ⊢ (% → ?); #absurd cases absurd @I)
     914    try (normalize in ⊢ (% → ?); #absurd cases absurd @I)
     915    #word11' #irrelevant normalize nodelta
     916    #eq_bv_assm cases (eq_bv_eq … eq_bv_assm) % *)
     917qed.
    439918
    440919inductive pseudo_instruction: Type[0] ≝
Note: See TracChangeset for help on using the changeset viewer.