Changeset 893 for src


Ignore:
Timestamp:
Jun 7, 2011, 5:32:30 PM (10 years ago)
Author:
sacerdot
Message:

Cleanup.

File:
1 edited

Legend:

Unmodified
Added
Removed

  • src/ASM/AssemblyProof.ma

    r892 r893  
    694694qed.
    695695
     696(*
    696697lemma andb_elim':
    697698 ∀b1,b2. (b1 = true) → (b2 = true) → (b1 ∧ b2) = true.
    698699 #b1 #b2 #H1 #H2 @andb_elim cases b1 in H1; normalize //
    699700qed.
     701*)
    700702
    701703let rec encoding_check (code_memory: BitVectorTrie Byte 16) (pc: Word) (final_pc: Word)
    … …  
    709711
    710712axiom eq_bv_refl: ∀n,v. eq_bv n v v = true.
    711 
    712 (*
    713 lemma test:
    714   ∀pc,i.
    715      (let assembled ≝ assembly1 i in
    716       let code_memory ≝ load_code_memory_aux pc assembled in
    717       let fetched ≝ fetch code_memory (bitvector_of_nat … pc) in
    718       let 〈instr_pc, ticks〉 ≝ fetched in
    719         eq_instruction (\fst instr_pc)) i = true.
    720 *)
    721713
    722714lemma test:
    … …  
    754746 whd >eq_instruction_refl >H4 try @eq_bv_refl
    755747qed.
    756      
    757 
    758  |*:
    759  >eq_instruction_refl >H4 @eq_bv_refl
    760 qed.
    761 
    762  
    763   whd
    764  [ @(list_addressing_mode_tags_elim_prop … arg) whd try %
    765    @(list_addressing_mode_tags_elim_prop … arg2) whd try %
    766    * #H1 #H2 whd in H2; whd change in ⊢ match % with [_ ⇒ ?] with (fetch0 ??)
    767    whd in ⊢ match ??% with [_ ⇒ ?] <H1 whd <H2 >eq_instruction_refl @eq_bv_refl
    768  |6: @(list_addressing_mode_tags_elim_prop … arg) whd try % #XX
    769    * #H1 * #H2 #H3 whd in H3; whd change in ⊢ match % with [_ ⇒ ?] with (fetch0 ??)
    770    whd in ⊢ match ??% with [_ ⇒ ?] <H1 whd <H2 <H3 >eq_instruction_refl @eq_bv_refl
    771  |7: @(list_addressing_mode_tags_elim_prop … arg) whd try %
    772    * #H1 #H2 whd in H2; whd change in ⊢ match % with [_ ⇒ ?] with (fetch0 ??)
    773  |3,5: @(list_addressing_mode_tags_elim_prop … arg) whd try % #XX
    774    
    775    @split_elim
    776 
    777  
    778    whd in ⊢ (??%?)
    779    [2,4: @(list_addressing_mode_tags_elim_prop … arg) whd try % #XX
    780          whd in ⊢ (??(match ? (? ? %) ? with [ _ ⇒ ?] ?)?)
    781          @split_elim #b1 #b2 #EQ >EQ -EQ;
    782         change in ⊢ (??(match % with [ _ ⇒ ?] ?)?) with (fetch0 ??)
    783         whd in ⊢ (??(match ?%% with [ _ ⇒ ?] ?)?)
    784         >lookup_insert_miss try @not_eqvb_SS
    785         >lookup_insert_miss //
    786         >lookup_insert_hit
    787         whd in ⊢ (??%?) whd in ⊢ (??(?%?)?)
    788         >half_add_SO >half_add_SO
    789         >lookup_insert_miss try @not_eqvb_S
    790         >lookup_insert_hit
    791         >lookup_insert_hit
    792         @eq_instruction_refl
    793    |1,3: @(list_addressing_mode_tags_elim_prop … arg) whd try % #XX
    794      whd in ⊢ (??(match ? (? ? %) ? with [ _ ⇒ ?] ?)?)
    795      @split_elim #b1 #b2 #EQ >EQ -EQ;
    796      change in ⊢ (??(match % with [ _ ⇒ ?] ?)?) with (fetch0 ??)
    797      whd in ⊢ (??(match ?%% with [ _ ⇒ ?] ?)?)
    798      >lookup_insert_miss //
    799      >lookup_insert_hit
    800      >half_add_SO
    801      @(bitvector_elim_complete' … b1) @andb_elim' @andb_elim' @andb_elim'
    802      whd in ⊢ (??%?) normalize in ⊢ (??(?(???(?))%)?) >lookup_insert_hit
    803      normalize
    804      (* FALSO!!! AJMP vs ACALL *)
    805      cases daemon
    806    | @(list_addressing_mode_tags_elim_prop … arg) whd try % #XX
    807      whd in ⊢ (??(match ?%? with [ _ ⇒ ?] ?)?)
    808      change in ⊢ (??(match % with [ _ ⇒ ?] ?)?) with (fetch0 ??)
    809      whd in ⊢ (??(match ??% with [ _ ⇒ ?] ?)?)
    810      >lookup_insert_miss //
    811      >lookup_insert_hit
    812      >half_add_SO
    813      whd in ⊢ (??%?)
    814      >lookup_insert_hit
    815      normalize
    816      @eq_instruction_refl
    817    | @(list_addressing_mode_tags_elim_prop … arg) whd try %
    818      whd in ⊢ (??(match ?%? with [ _ ⇒ ?] ?)?)
    819      change in ⊢ (??(match % with [ _ ⇒ ?] ?)?) with (fetch0 ??)
    820      whd in ⊢ (??(match ??% with [ _ ⇒ ?] ?)?)
    821      >lookup_insert_hit
    822      >half_add_SO
    823      normalize
    824      @eq_instruction_refl
    825    | @(list_addressing_mode_tags_elim_prop … arg) whd try %
    826      @(list_addressing_mode_tags_elim_prop … arg2) whd try %
    827      whd in ⊢ (??(match ?%? with [ _ ⇒ ?] ?)?)
    828      change in ⊢ (??(match % with [ _ ⇒ ?] ?)?) with (fetch0 ??)
    829      whd in ⊢ (??(match ??% with [ _ ⇒ ?] ?)?)
    830      >lookup_insert_hit
    831      >half_add_SO
    832      normalize
    833      @eq_instruction_refl
    834    | cases arg -i arg;
    835 (* 
    836 16,17,18,19,20,28,19
    837 *)
    838      [1,2,3: #arg1 #arg2
    839        @(list_addressing_mode_tags_elim_prop … arg1) whd try %
    840        @(list_addressing_mode_tags_elim_prop … arg2) whd try % #XX
    841        whd in ⊢ (??(match ?%? with [ _ ⇒ ?] ?)?)
    842        change in ⊢ (??(match % with [ _ ⇒ ?] ?)?) with (fetch0 ??)
    843        whd in ⊢ (??(match ??% with [ _ ⇒ ?] ?)?)
    844        [1,4,5,8,9,12: >lookup_insert_miss //]
    845        >lookup_insert_hit >half_add_SO
    846        [1,2,3,4,5,6: whd in ⊢ (??%?) >lookup_insert_hit]
    847        normalize
    848        @eq_instruction_refl
    849      |35,36,37:
    850        whd in ⊢ (??(match ?%? with [ _ ⇒ ?] ?)?)
    851        change in ⊢ (??(match % with [ _ ⇒ ?] ?)?) with (fetch0 ??)
    852        whd in ⊢ (??(match ??% with [ _ ⇒ ?] ?)?)
    853        >lookup_insert_hit >half_add_SO
    854        normalize
    855        @eq_instruction_refl
    856      |6,7,8,23,24,25,26,27: #arg1 try #arg2
    857        @(list_addressing_mode_tags_elim_prop … arg1) whd try %
    858        try (@(list_addressing_mode_tags_elim_prop … arg2) whd try %)
    859        whd in ⊢ (??(match ?%? with [ _ ⇒ ?] ?)?)
    860        change in ⊢ (??(match % with [ _ ⇒ ?] ?)?) with (fetch0 ??)
    861        whd in ⊢ (??(match ??% with [ _ ⇒ ?] ?)?)
    862        >lookup_insert_hit >half_add_SO
    863        normalize
    864        @eq_instruction_refl
    865      |9,10,14,15,31,32: #arg1
    866        @(list_addressing_mode_tags_elim_prop … arg1) whd try % #XX
    867        whd in ⊢ (??(match ?%? with [ _ ⇒ ?] ?)?)
    868        change in ⊢ (??(match % with [ _ ⇒ ?] ?)?) with (fetch0 ??)
    869        whd in ⊢ (??(match ??% with [ _ ⇒ ?] ?)?)
    870        >lookup_insert_miss //
    871        >lookup_insert_hit
    872        >half_add_SO
    873        whd in ⊢ (??%?)
    874        >lookup_insert_hit
    875        normalize
    876        @eq_instruction_refl
    877      |33,34: #arg1 #arg2
    878        @(list_addressing_mode_tags_elim_prop … arg1) whd try %
    879        @(list_addressing_mode_tags_elim_prop … arg2) whd try % #XX2
    880        whd in ⊢ (??(match ?%? with [ _ ⇒ ?] ?)?)
    881        whd in ⊢ (??(match ?(????%?)? with [_ ⇒ ?] ?)?)
    882        change in ⊢ (??(match % with [ _ ⇒ ?] ?)?) with (fetch0 ??)
    883        whd in ⊢ (??(match ??% with [ _ ⇒ ?] ?)?)
    884        [>lookup_insert_miss //] >lookup_insert_hit >half_add_SO whd in ⊢ (??%?)
    885        [>lookup_insert_hit]
    886        normalize
    887        @eq_instruction_refl
    888      |4,5,21,22,30: #arg1
    889        @(list_addressing_mode_tags_elim_prop … arg1) whd try % try #XX1
    890        whd in ⊢ (??(match ?%? with [ _ ⇒ ?] ?)?)
    891        change in ⊢ (??(match % with [ _ ⇒ ?] ?)?) with (fetch0 ??)
    892        whd in ⊢ (??(match ??% with [ _ ⇒ ?] ?)?)
    893        [1,6,12,15,17: >lookup_insert_miss //] >lookup_insert_hit >half_add_SO whd in ⊢ (??%?)
    894        [1,2,3,4,5: >lookup_insert_hit] normalize @eq_instruction_refl
    895      |11,12,13: #arg1 #arg2
    896        @(list_addressing_mode_tags_elim_prop … arg1) whd try % #XX1
    897        @(list_addressing_mode_tags_elim_prop … arg2) whd try % #XX2
    898        whd in ⊢ (??(match ?%? with [ _ ⇒ ?] ?)?)
    899        whd in ⊢ (??(match ?(????%?)? with [_ ⇒ ?] ?)?)
    900        change in ⊢ (??(match % with [ _ ⇒ ?] ?)?) with (fetch0 ??)
    901        whd in ⊢ (??(match ??% with [ _ ⇒ ?] ?)?)
    902        >lookup_insert_miss try @not_eqvb_SS
    903        >lookup_insert_miss //
    904        >lookup_insert_hit
    905        >half_add_SO
    906        whd in ⊢ (??%?) whd in ⊢ (??(?%?)?)
    907        >half_add_SO
    908        >lookup_insert_hit
    909        >lookup_insert_miss //
    910        >lookup_insert_hit
    911        normalize
    912        @eq_instruction_refl
    913  ]
    914 qed.   
    915748 
    916749(* This establishes the correspondence between pseudo program counters and
    … …  
    15471380      hd = byte ∧ encoding_check' code_memory new_pc tl
    15481381  ].
    1549 
    1550 (* prove later *)
    1551 axiom test:
    1552   ∀pc: Word.
    1553   ∀code_memory: BitVectorTrie Byte 16.
    1554   ∀i: instruction.
    1555     let assembled ≝ assembly1 i in
    1556       encoding_check' code_memory pc assembled →
    1557         let 〈instr_pc, ignore〉 ≝ fetch code_memory pc in
    1558         let 〈instr, pc〉 ≝ instr_pc in
    1559           instr = i.
    15601382 
    15611383lemma main_thm:
Note: See TracChangeset for help on using the changeset viewer.