Changeset 885


Ignore:
Timestamp:
Jun 5, 2011, 2:04:22 AM (8 years ago)
Author:
sacerdot
Message:

Proof almost finished, but rewritings are extremely slow.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/AssemblyProof.ma

    r884 r885  
    443443    true.*)
    444444axiom eq_instruction: instruction → instruction → bool.
     445axiom eq_instruction_refl: ∀i. eq_instruction i i = true.
     446
    445447let rec vect_member
    446448  (A: Type[0]) (n: nat) (eq: A → A → bool)
     
    717719        >lookup_insert_hit
    718720        >lookup_insert_hit
    719         (* REFL MISSING *)
    720         cases daemon
     721        @eq_instruction_refl
    721722   |1,3: @(list_addressing_mode_tags_elim_prop … arg) whd try % #XX
    722723     whd in ⊢ (??(match ? (? ? %) ? with [ _ ⇒ ?] ?)?)
     
    726727     >lookup_insert_miss //
    727728     >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
     729     >half_add_SO
     730     @(bitvector_elim_complete' … b1) @andb_elim' @andb_elim' @andb_elim'
     731     whd in ⊢ (??%?) normalize in ⊢ (??(?(???(?))%)?) >lookup_insert_hit
     732     normalize
    731733     (* 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 ⊢ (??(?%?)?)
     734     cases daemon
     735   | @(list_addressing_mode_tags_elim_prop … arg) whd try % #XX
     736     whd in ⊢ (??(match ?%? with [ _ ⇒ ?] ?)?)
     737     change in ⊢ (??(match % with [ _ ⇒ ?] ?)?) with (fetch0 ??)
     738     whd in ⊢ (??(match ??% with [ _ ⇒ ?] ?)?)
     739     >lookup_insert_miss //
     740     >lookup_insert_hit
    746741     >half_add_SO
    747      
    748        
    749          
    750  
    751    [2: #addr whd in ⊢ (??%?)
    752  
    753    @ (instruction_elim_complete )
    754  | @ zero
     742     whd in ⊢ (??%?)
     743     >lookup_insert_hit
     744     normalize
     745     @eq_instruction_refl
     746   | @(list_addressing_mode_tags_elim_prop … arg) whd try %
     747     whd in ⊢ (??(match ?%? with [ _ ⇒ ?] ?)?)
     748     change in ⊢ (??(match % with [ _ ⇒ ?] ?)?) with (fetch0 ??)
     749     whd in ⊢ (??(match ??% with [ _ ⇒ ?] ?)?)
     750     >lookup_insert_hit
     751     >half_add_SO
     752     normalize
     753     @eq_instruction_refl
     754   | @(list_addressing_mode_tags_elim_prop … arg) whd try %
     755     @(list_addressing_mode_tags_elim_prop … arg2) whd try %
     756     whd in ⊢ (??(match ?%? with [ _ ⇒ ?] ?)?)
     757     change in ⊢ (??(match % with [ _ ⇒ ?] ?)?) with (fetch0 ??)
     758     whd in ⊢ (??(match ??% with [ _ ⇒ ?] ?)?)
     759     >lookup_insert_hit
     760     >half_add_SO
     761     normalize
     762     @eq_instruction_refl
     763   | cases arg -i arg;
     764     [1,2,3: #arg1 #arg2
     765       @(list_addressing_mode_tags_elim_prop … arg1) whd try %
     766       @(list_addressing_mode_tags_elim_prop … arg2) whd try % #XX
     767       whd in ⊢ (??(match ?%? with [ _ ⇒ ?] ?)?)
     768       change in ⊢ (??(match % with [ _ ⇒ ?] ?)?) with (fetch0 ??)
     769       whd in ⊢ (??(match ??% with [ _ ⇒ ?] ?)?)
     770       [1,4,5,8,9,12: >lookup_insert_miss //]
     771       >lookup_insert_hit >half_add_SO
     772       [1,2,3,4,5,6: whd in ⊢ (??%?) >lookup_insert_hit]
     773       normalize
     774       @eq_instruction_refl
     775     |35,36,37:
     776       whd in ⊢ (??(match ?%? with [ _ ⇒ ?] ?)?)
     777       change in ⊢ (??(match % with [ _ ⇒ ?] ?)?) with (fetch0 ??)
     778       whd in ⊢ (??(match ??% with [ _ ⇒ ?] ?)?)
     779       >lookup_insert_hit >half_add_SO
     780       normalize
     781       @eq_instruction_refl
     782     |6,7,8,23,24,25,26,27: #arg1 try #arg2
     783       @(list_addressing_mode_tags_elim_prop … arg1) whd try %
     784       try (@(list_addressing_mode_tags_elim_prop … arg2) whd try %)
     785       whd in ⊢ (??(match ?%? with [ _ ⇒ ?] ?)?)
     786       change in ⊢ (??(match % with [ _ ⇒ ?] ?)?) with (fetch0 ??)
     787       whd in ⊢ (??(match ??% with [ _ ⇒ ?] ?)?)
     788       >lookup_insert_hit >half_add_SO
     789       normalize
     790       @eq_instruction_refl
     791     |9,10,14,15,31,32: #arg1
     792       @(list_addressing_mode_tags_elim_prop … arg1) whd try % #XX
     793       whd in ⊢ (??(match ?%? with [ _ ⇒ ?] ?)?)
     794       change in ⊢ (??(match % with [ _ ⇒ ?] ?)?) with (fetch0 ??)
     795       whd in ⊢ (??(match ??% with [ _ ⇒ ?] ?)?)
     796       >lookup_insert_miss //
     797       >lookup_insert_hit
     798       >half_add_SO
     799       whd in ⊢ (??%?)
     800       >lookup_insert_hit
     801       normalize
     802       @eq_instruction_refl
     803     |33,34: #arg1 #arg2
     804       @(list_addressing_mode_tags_elim_prop … arg1) whd try %
     805       @(list_addressing_mode_tags_elim_prop … arg2) whd try % #XX2
     806       whd in ⊢ (??(match ?%? with [ _ ⇒ ?] ?)?)
     807       whd in ⊢ (??(match ?(????%?)? with [_ ⇒ ?] ?)?)
     808       change in ⊢ (??(match % with [ _ ⇒ ?] ?)?) with (fetch0 ??)
     809       whd in ⊢ (??(match ??% with [ _ ⇒ ?] ?)?)
     810       [>lookup_insert_miss //] >lookup_insert_hit >half_add_SO whd in ⊢ (??%?)
     811       [>lookup_insert_hit]
     812       normalize
     813       @eq_instruction_refl
     814     |4,5,21,22,30: #arg1
     815       @(list_addressing_mode_tags_elim_prop … arg1) whd try % try #XX1
     816       whd in ⊢ (??(match ?%? with [ _ ⇒ ?] ?)?)
     817       change in ⊢ (??(match % with [ _ ⇒ ?] ?)?) with (fetch0 ??)
     818       whd in ⊢ (??(match ??% with [ _ ⇒ ?] ?)?)
     819       [1,6,12,15,17: >lookup_insert_miss //] >lookup_insert_hit >half_add_SO whd in ⊢ (??%?)
     820       [1,2,3,4,5: >lookup_insert_hit] normalize @eq_instruction_refl
     821     |11,12,13: #arg1 #arg2
     822       @(list_addressing_mode_tags_elim_prop … arg1) whd try % #XX1
     823       @(list_addressing_mode_tags_elim_prop … arg2) whd try % #XX2
     824       whd in ⊢ (??(match ?%? with [ _ ⇒ ?] ?)?)
     825       whd in ⊢ (??(match ?(????%?)? with [_ ⇒ ?] ?)?)
     826       change in ⊢ (??(match % with [ _ ⇒ ?] ?)?) with (fetch0 ??)
     827       whd in ⊢ (??(match ??% with [ _ ⇒ ?] ?)?)
     828       >lookup_insert_miss try @not_eqvb_SS
     829       >lookup_insert_miss //
     830       >lookup_insert_hit
     831       >half_add_SO
     832       whd in ⊢ (??%?) whd in ⊢ (??(?%?)?)
     833       >half_add_SO
     834       >lookup_insert_hit
     835       >lookup_insert_miss try @not_eqvb_SS
     836       >lookup_insert_hit
     837       normalize
     838       @eq_instruction_refl
    755839 ]
    756  normalize
    757    
     840qed.   
    758841 
    759842(* This establishes the correspondence between pseudo program counters and
Note: See TracChangeset for help on using the changeset viewer.