Changeset 884


Ignore:
Timestamp:
Jun 4, 2011, 6:16:08 PM (8 years ago)
Author:
sacerdot
Message:

...

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/AssemblyProof.ma

    r883 r884  
    455455  (n: nat)
    456456  (l: Vector addressing_mode_tag (S n))
    457   (P: addressing_mode → Prop) on l:
     457  on l:
     458  ∀P: l → Prop.
    458459  ∀direct_a. ∀indirect_a. ∀ext_indirect_a. ∀register_a. ∀acc_a_a.
    459460  ∀acc_b_a. ∀dptr_a. ∀data_a. ∀data16_a. ∀acc_dptr_a. ∀acc_pc_a.
     
    465466      match y with
    466467      [ O    ⇒ λm: Vector addressing_mode_tag O. ∀prf: 0 = S n. True
    467       | S y' ⇒ λl: Vector addressing_mode_tag (S y'). ∀prf: S y' = S n.
     468      | S y' ⇒ λl: Vector addressing_mode_tag (S y'). ∀prf: S y' = S n.∀P:l → Prop.
    468469               ∀direct_a: if vect_member … eq_a l direct then ∀x. P (DIRECT x) else True.
    469470               ∀indirect_a: if vect_member … eq_a l indirect then ∀x. P (INDIRECT x) else True.
     
    489490  [ VEmpty          ⇒ λAbsurd. ⊥
    490491  | VCons len hd tl ⇒ λProof. ?
    491   ] (refl ? (S n)).
     492  ] (refl ? (S n)). cases daemon. qed. (*
    492493  [ destruct(Absurd)
    493494  | # A1 # A2 # A3 # A4 # A5 # A6 # A7
     
    495496    # A15 # A16 # A17 # A18 # A19 # X
    496497    cases X
    497     # SUB cases daemon ] qed.(*
     498    # SUB cases daemon ] qed.
    498499    cases SUB
    499500    [ # BYTE
     
    681682 (¬eq_bv 16 (bitvector_of_nat 16 pc) (bitvector_of_nat 16 (S (S pc)))).
    682683
     684axiom bitvector_elim_complete:
     685 ∀n,P. bitvector_elim n P = true → ∀bv. P bv.
     686
     687lemma bitvector_elim_complete':
     688 ∀n,P. bitvector_elim n P = true → ∀bv. P bv = true.
     689 #n #P #H generalize in match (bitvector_elim_complete … H) #K #bv
     690 generalize in match (K bv) normalize cases (P bv) normalize // #abs @⊥ //
     691qed.
     692
     693lemma andb_elim':
     694 ∀b1,b2. (b1 = true) → (b2 = true) → (b1 ∧ b2) = true.
     695 #b1 #b2 #H1 #H2 @andb_elim cases b1 in H1; normalize //
     696qed.
     697
    683698lemma test:
    684699  ∀pc,i.
     
    689704        eq_instruction (\fst instr_pc)) i = true.
    690705 #pc #i cases i #arg try #arg2 whd in ⊢ (??%?)
    691    [2,4: @(list_addressing_mode_tags_elim_prop ? [[addr16]] ???????????????????? arg) whd try % #XX
     706   [2,4: @(list_addressing_mode_tags_elim_prop arg) whd try % #XX
    692707         whd in ⊢ (??(match ? (? ? %) ? with [ _ ⇒ ?] ?)?)
    693        cases arg #sam cases sam #XX try #PP normalize in PP; try cases PP;
    694        whd in ⊢ (??(match ? (? ? %) ? with [ _ ⇒ ?] ?)?) try cases PP normalize in XX;
    695        [1,2,3,4,5,6,7,8,10,11,12,13,14,15,16,17: cases XX
    696        |*:@split_elim #b1 #b2 #EQ >EQ -EQ;
     708         @split_elim #b1 #b2 #EQ >EQ -EQ;
    697709        change in ⊢ (??(match % with [ _ ⇒ ?] ?)?) with (fetch0 ??)
    698         whd in ⊢ (??(match ??% with [ _ ⇒ ?] ?)?)
    699         >lookup_insert_miss //
     710        whd in ⊢ (??(match ?%% with [ _ ⇒ ?] ?)?)
     711        >lookup_insert_miss try @not_eqvb_SS
    700712        >lookup_insert_miss //
    701713        >lookup_insert_hit
    702         whd in ⊢ (??(match % with [ _ ⇒ ?] ?)?)
    703714        whd in ⊢ (??%?) whd in ⊢ (??(?%?)?)
    704715        >half_add_SO >half_add_SO
    705         >lookup_insert_miss [2,4: @not_eqvb_S]
    706         >lookup_insert_hit >lookup_insert_hit]
    707    |
    708        
     716        >lookup_insert_miss try @not_eqvb_S
     717        >lookup_insert_hit
     718        >lookup_insert_hit
     719        (* REFL MISSING *)
     720        cases daemon
     721   |1,3: @(list_addressing_mode_tags_elim_prop … arg) whd try % #XX
     722     whd in ⊢ (??(match ? (? ? %) ? with [ _ ⇒ ?] ?)?)
     723     @split_elim #b1 #b2 #EQ >EQ -EQ;
     724     change in ⊢ (??(match % with [ _ ⇒ ?] ?)?) with (fetch0 ??)
     725     whd in ⊢ (??(match ?%% with [ _ ⇒ ?] ?)?)
     726     >lookup_insert_miss //
     727     >lookup_insert_hit
     728     generalize in match b1 @(bitvector_elim_complete')
     729     @andb_elim' @andb_elim' @andb_elim' whd in ⊢ (??%?)
     730     >half_add_SO >lookup_insert_hit normalize
     731     (* FALSO!!! AJMP vs ACALL *)
     732   
     733     
     734     whd in ⊢ (??%?) whd in ⊢ (??(match % with [ _ ⇒ % | _ ⇒ ?])?)
     735     check andb_elim.
     736      (λV.(let 〈instr_pc,ticks〉 ≝
     737           fetch0
     738           (insert Byte 16 (bitvector_of_nat 16 (S pc)) b2
     739            (insert Byte 16 (bitvector_of_nat 16 pc)
     740             (V@@[[true; false; false; false; true]]) (Stub Byte 16)))
     741           〈\snd  (half_add 16 (bitvector_of_nat 16 pc) (bitvector_of_nat 16 1)),
     742           V@@[[true; false; false; false; true]]〉 in 
     743    eq_instruction (\fst  instr_pc))
     744   (ACALL (ADDR11 (V@@b2)))) ?)
     745     whd in ⊢ (??%?) whd in ⊢ (??(?%?)?)
     746     >half_add_SO
     747     
    709748       
    710749         
Note: See TracChangeset for help on using the changeset viewer.