Changeset 867


Ignore:
Timestamp:
May 31, 2011, 5:01:07 PM (8 years ago)
Author:
mulligan
Message:

changes to assembly proof

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/AssemblyProof.ma

    r866 r867  
    106106qed.
    107107
    108 axiom vector_associativity_of_append:
     108axiom vector_associative_append:
    109109  ∀A: Type[0].
    110110  ∀n, m, o:  nat.
     
    116116    (v @@ (q @@ r)).
    117117       
    118 axiom vector_cons_append:
     118lemma vector_cons_append:
    119119  ∀A: Type[0].
    120120  ∀n: nat.
    121   ∀a: A.
     121  ∀e: A.
    122122  ∀v: Vector A n.
    123     a ::: v = [[ a ]] @@ v.
     123    e ::: v = [[ e ]] @@ v.
     124  # A # N # E # V
     125  elim V
     126  [ normalize %
     127  | # NN # AA # VV # IH
     128    normalize
     129    %
     130  ]
     131qed.
    124132
    125133lemma super_rewrite2:
     
    198206        (λSS.λVS.bool_to_Prop (subvector_with ?? (O+SS) ?? (H@@VS)))
    199207        ?
    200         (vector_associativity_of_append A ? ? ? QQ [[AA]] VV))
     208        (vector_associative_append A ? ? ? QQ [[AA]] VV))
    201209      [ >associative_plus //
    202210      | @IH ]
     
    214222qed.
    215223
    216 (*
    217 lemma subvector_hd_tl:
     224lemma vector_cons_empty:
     225  ∀A: Type[0].
     226  ∀n: nat.
     227  ∀v: Vector A n.
     228    [[ ]] @@ v = v.
     229  # A # N # V
     230  elim V
     231  [ normalize %
     232  | # NN # HH # VV #H %
     233  ]
     234qed.
     235
     236corollary subvector_hd_tl:
    218237  ∀A: Type[0].
    219238  ∀o: nat.
     
    223242  ∀v: Vector A o.
    224243    bool_to_Prop (subvector_with A ? ? eq v (h ::: v)).
    225 
    226 axiom eq_a_reflexive:
     244  # A # O # EQ # REFLEX # H # V
     245  > (vector_cons_append A ? H V)
     246  < (vector_cons_empty A ? ([[H]] @@ V))
     247  @ (subvector_multiple_append A ? ? EQ REFLEX [[]] V ? [[ H ]])
     248qed.
     249
     250lemma eq_a_reflexive:
    227251  ∀a. eq_a a a = true.
    228 
     252  # A
     253  cases A
     254  %
     255qed.
     256
     257lemma is_in_monotonic_wrt_append:
     258  ∀m, n: nat.
     259  ∀p: Vector addressing_mode_tag m.
     260  ∀q: Vector addressing_mode_tag n.
     261  ∀to_search: addressing_mode.
     262    bool_to_Prop (is_in ? p to_search) → bool_to_Prop (is_in ? (q @@ p) to_search).
     263  # M # N # P # Q # TO_SEARCH
     264  # H
     265  elim Q
     266  [ normalize
     267    @ H
     268  | # NN # PP # QQ # IH
     269    normalize
     270    cases (is_a PP TO_SEARCH)
     271    [ normalize
     272      %
     273    | normalize
     274      normalize in IH
     275      @ IH
     276    ]
     277  ]
     278qed.
     279
     280corollary is_in_hd_tl:
     281  ∀to_search: addressing_mode.
     282  ∀hd: addressing_mode_tag.
     283  ∀n: nat.
     284  ∀v: Vector addressing_mode_tag n.
     285    bool_to_Prop (is_in ? v to_search) → bool_to_Prop (is_in ? (hd:::v) to_search).
     286  # TO_SEARCH # HD # N # V
     287  elim V
     288  [ # H
     289    normalize in H;
     290    cases H
     291  | # NN # HHD # VV # IH # HH
     292    > vector_cons_append
     293    > (vector_cons_append ? ? HHD VV)
     294    @ (is_in_monotonic_wrt_append ? 1 ([[HHD]]@@VV) [[HD]] TO_SEARCH)
     295    @ HH
     296  ]
     297qed.
     298 
    229299let rec list_addressing_mode_tags_elim
    230300  (n: nat) (l: Vector addressing_mode_tag (S n)) on l: (l → bool) → bool ≝
     
    257327    in
    258328      andb (process_hd P)
    259        (match len return λlen. Vector addressing_mode_tag len → bool with
    260          [ O ⇒ λ_.true
    261          | S y ⇒ λtl.list_addressing_mode_tags_elim y tl (λaddr.P addr) ] tl)
     329       (match len return λx. x = len → bool with
     330         [ O ⇒ λprf. true
     331         | S y ⇒ λprf. list_addressing_mode_tags_elim y ? P ] (refl ? len))
    262332  ].
    263   [1: @ (execute_1_technical ? ? tl)
    264       [ //
    265       | @ (subvector_hd_tl addressing_mode_tag (S y) (S len) eq_a eq_a_reflexive)
    266       ]
    267   ].
     333  try %
     334  [ 2: cases (sym_eq ??? prf); @tl
     335  | cases prf in tl H; #tl
     336    normalize in ⊢ (∀_: %. ?)
     337    # H
     338    whd
     339    normalize in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ?])
     340    cases (is_a hd (subaddressing_modeel y tl H)) whd // ]
     341qed.
     342
     343definition product_elim ≝
     344  λm, n: nat.
     345  λv: Vector addressing_mode_tag (S m).
     346  λq: Vector addressing_mode_tag (S n).
     347  λP: (Vector addressing_mode_tag (S m) × (Vector addressing_mode_tag (S n))) → bool.
     348    P 〈v, q〉.
     349
     350axiom union_elim:
     351  ∀m, n: nat. ((Vector addressing_mode_tag m ⊎ Vector addressing_mode_tag n) → bool) → bool.
    268352
    269353definition preinstruction_elim: ∀P: preinstruction [[ relative ]] → bool. bool ≝
    270  λP.
    271    P (ADD … ACC_A
    272    P (DA … ACC_A).lemma jmeq_to_eq: ∀A:Type[0]. ∀x,y:A. x≃y → x=y.
    273  #A #x #y #JMEQ @(jmeq_elim ? x … JMEQ) %
    274 qed.
    275  %
    276 qed.
     354  λP.
     355    list_addressing_mode_tags_elim ? [[ registr ; direct ; indirect ; data ]] (λaddr. P (ADD ? ACC_A addr)) ∧
     356    list_addressing_mode_tags_elim ? [[ registr ; direct ; indirect ; data ]] (λaddr. P (ADDC ? ACC_A addr)) ∧
     357    list_addressing_mode_tags_elim ? [[ registr ; direct ; indirect ; data ]] (λaddr. P (SUBB ? ACC_A addr)) ∧
     358    list_addressing_mode_tags_elim ? [[ acc_a ; registr ; direct ; indirect ; dptr ]] (λaddr. P (INC ? addr)) ∧
     359    list_addressing_mode_tags_elim ? [[ acc_a ; registr ; direct ; indirect ]] (λaddr. P (DEC ? addr)) ∧
     360    list_addressing_mode_tags_elim ? [[acc_b]] (λaddr. P (MUL ? ACC_A addr)) ∧
     361    list_addressing_mode_tags_elim ? [[acc_b]] (λaddr. P (DIV ? ACC_A addr)) ∧
     362    list_addressing_mode_tags_elim ? [[ registr ; direct ]] (λaddr. P (DJNZ ? ? addr)) ∧
     363    list_addressing_mode_tags_elim ? [[ acc_a ; carry ; bit_addr ]] (λaddr. P (CLR ? addr)) ∧
     364    list_addressing_mode_tags_elim ? [[ acc_a ; carry ; bit_addr ]] (λaddr. P (CPL ? addr)) ∧
     365    P (DA ? ACC_A) ∧
     366    P (JC ? ?) ∧
     367    P (JNC ? ?) ∧
     368    P (JZ ? ?) ∧
     369    P (JNZ ? ?) ∧
     370    P (JB ? (BIT_ADDR ?) ?) ∧
     371    P (JNB ? [[ bit_addr ]] ?) ∧
     372    P (JBC ? [[ bit_addr ]] ?) ∧
     373    P (RL ? ACC_A).
     374   
     375   
     376   
     377   
     378   
     379   
     380    list_addressing_mode_tags_elim ? [[ data ]] (λaddr. P (CJNE ? (inl ? ? (〈ACC_A, addr)).
     381
     382    list_addressing_mode_tags_elim ? [[ acc_a ; registr ; direct ; indirect ]] (λaddr. P (ANL ? addr)) ∧
     383    list_addressing_mode_tags_elim ? [[ acc_a ; registr ; direct ; indirect ]] (λaddr. P (ORL ? addr)) ∧
     384    list_addressing_mode_tags_elim ? [[ acc_a ; registr ; direct ; indirect ]] (λaddr. P (XRL ? addr)) ∧
     385    list_addressing_mode_tags_elim ? [[ acc_a ; registr ; direct ; indirect ]] (λaddr. P (RL ? addr)) ∧
     386    list_addressing_mode_tags_elim ? [[ acc_a ; registr ; direct ; indirect ]] (λaddr. P (RLC ? addr)) ∧
     387    list_addressing_mode_tags_elim ? [[ acc_a ; registr ; direct ; indirect ]] (λaddr. P (RR ? addr)) ∧
     388    list_addressing_mode_tags_elim ? [[ acc_a ; registr ; direct ; indirect ]] (λaddr. P (RRC ? addr)) ∧
     389    list_addressing_mode_tags_elim ? [[ acc_a ; registr ; direct ; indirect ]] (λaddr. P (SWAP ? addr)) ∧
     390    list_addressing_mode_tags_elim ? [[ acc_a ; registr ; direct ; indirect ]] (λaddr. P (MOV ? addr)) ∧
     391    list_addressing_mode_tags_elim ? [[ acc_a ; registr ; direct ; indirect ]] (λaddr. P (MOVX ? addr)) ∧
     392    list_addressing_mode_tags_elim ? [[ acc_a ; registr ; direct ; indirect ]] (λaddr. P (SETB ? addr)) ∧
     393    list_addressing_mode_tags_elim ? [[ acc_a ; registr ; direct ; indirect ]] (λaddr. P (PUSH ? addr)) ∧
     394    list_addressing_mode_tags_elim ? [[ acc_a ; registr ; direct ; indirect ]] (λaddr. P (POP ? addr)) ∧
     395    list_addressing_mode_tags_elim ? [[ acc_a ; registr ; direct ; indirect ]] (λaddr. P (XCH ? addr)) ∧
     396    list_addressing_mode_tags_elim ? [[ acc_a ; registr ; direct ; indirect ]] (λaddr. P (XCHD ? addr)) ∧
     397    P (RET ?) ∧
     398    P (RETI ?) ∧
     399    P (NOP ?).
    277400 
    278401
     
    298421  | @ (instruction_elim INSTR)
    299422  ].
    300 *)
    301423 
    302424(* This establishes the correspondence between pseudo program counters and
Note: See TracChangeset for help on using the changeset viewer.