Changeset 2278


Ignore:
Timestamp:
Jul 30, 2012, 6:33:11 PM (7 years ago)
Author:
mulligan
Message:

Half of JC case complete

Location:
src/ASM
Files:
2 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/AssemblyProofSplit.ma

    r2276 r2278  
    1010  ∀i: instruction.
    1111    fetch_many code_memory final_pc start_pc [i] →
    12       〈i, final_pc, ticks_of_instruction i〉 = fetch code_memory
    13 start_pc.
     12      〈i, final_pc, ticks_of_instruction i〉 = fetch code_memory start_pc.
    1413  #code_memory #final_pc #start_pc #i * #new_pc
    1514  #fetch_many_assm whd in fetch_many_assm;
     
    6867 #cm #ps #l #addr #M #sigma #policy #s #H1 #H2 #H3 @get_arg_8_status_of_pseudo_status
    6968 try assumption %
     69qed.
     70
     71lemma short_jump_cond_ok:
     72  ∀v1, v1', v2, v2': Word.
     73  ∀is_possible, offset.
     74    v1 = v1' → v2 = v2' →
     75    〈is_possible, offset〉 = short_jump_cond v1 v2 →
     76      is_possible → v2' = add 16 v1' (sign_extension offset).
     77  #v1 #v1' #v2 #v2' #is_possible #offset #v1_refl #v2_refl <v1_refl <v2_refl
     78  whd in match short_jump_cond; normalize nodelta
     79  @pair_elim #result #flags #sub16_refl
     80  @pair_elim #upper #lower #vsplit_refl
     81  inversion (get_index' bool ???) #get_index_refl normalize nodelta
     82  #relevant destruct(relevant) #relevant
     83  [1:
     84    @(sub_16_to_add_16_8_1 … flags)
     85  |2:
     86    @(sub_16_to_add_16_8_0 … flags)
     87  ]
     88  try assumption >sub16_refl
     89  <(eq_bv_eq … relevant)
     90  >(vsplit_ok … (sym_eq … vsplit_refl)) %
    7091qed.
    7192
     
    11391160      ]
    11401161    ]
    1141   |12: (* JC *)
     1162  |*)12: (* JC *)
    11421163    >EQP -P normalize nodelta
     1164    whd in match assembly_1_pseudoinstruction; normalize nodelta
    11431165    whd in match expand_pseudo_instruction; normalize nodelta
    11441166    whd in match expand_relative_jump; normalize nodelta
    11451167    whd in match expand_relative_jump_internal; normalize nodelta
     1168    >EQppc in ⊢ (% → ?);
    11461169    @pair_elim #sj_possible #disp #sj_possible_disp_refl
    11471170    inversion sj_possible #sj_possible_refl normalize nodelta
     
    11561179      >EQs >EQticks <instr_refl normalize nodelta
    11571180      [1:
    1158         @(get_cy_flag_status_of_pseudo_status M') %
    1159       |2:
    1160         @sym_eq @set_program_counter_status_of_pseudo_status
    1161         [1:
    1162         |2:
    1163           @sym_eq @set_clock_status_of_pseudo_status try %
     1181        @(get_cy_flag_status_of_pseudo_status 〈low, high, accA〉) %
     1182      |2:
     1183        @set_program_counter_status_of_pseudo_status
     1184        [1:
     1185          >EQaddr_of normalize nodelta
     1186          whd in match addr_of_relative; normalize nodelta
     1187          @(short_jump_cond_ok … sj_possible … (sym_eq ??? sj_possible_disp_refl))
     1188          [1:
     1189            @sym_eq whd in ⊢ (??%?); >EQppc %
     1190          |2:
     1191            >EQlookup_labels %
     1192          |3:
     1193            >sj_possible_refl @I
     1194          ]
     1195        |2:
     1196          @set_clock_status_of_pseudo_status try %
    11641197          whd in match ticks_of0; normalize nodelta
    11651198          @(pair_replace ?????????? (eq_to_jmeq … sj_possible_disp_refl))
    11661199          [1:
    1167             @eq_f2 try %
    1168             >sigma_increment_commutation
    1169             lapply sigma_policy_witness whd in match sigma_policy_specification; normalize nodelta
    1170             * #sigma_zero_assm #relevant cases (relevant ppc ?)
    1171             [1:
    1172               -relevant
    1173               [2:
    1174                 >EQcm assumption
    1175               |1:
    1176                 #relevant #_ <EQppc >relevant @eq_f @eq_f @eq_f
    1177                 >EQlookup_labels >EQcm >create_label_cost_refl @eq_f2
    1178               ]
    1179             |2:
    1180             ]
     1200            >EQppc %
    11811201          |2:
    11821202            >sj_possible_refl %
     
    11841204        ]
    11851205      |3:
    1186       ]
     1206        @set_clock_status_of_pseudo_status try % @eq_f2 try %
     1207        whd in match ticks_of0; normalize nodelta
     1208        @(pair_replace ?????????? (eq_to_jmeq … sj_possible_disp_refl))
     1209        [1:
     1210          >EQppc %
     1211        |2:
     1212          >sj_possible_refl %
     1213        ]
     1214      ]
     1215    |2:
     1216      #sigma_increment_commutation #maps_assm
     1217      whd in maps_assm:(??%?); lapply maps_assm @Some_Some_elim #Mrefl destruct(Mrefl)
     1218      whd in ⊢ (% → ?); * #jc_fetch_refl * #sjmp_fetch_refl * #ljmp_fetch_refl
     1219      whd in ⊢ (% → ?); #ppc_eq_bv_refl %{2}
     1220      @(if_then_else_replace ???????? p) try % normalize nodelta
     1221      change with (execute_1 ?? = ?) destruct
     1222      whd in ⊢ (??%?); >EQs >EQticks <instr_refl
     1223      change with (set_program_counter ???? = ?)
    11871224    ]
    11881225    cases daemon
  • src/ASM/AssemblyProofSplitSplit.ma

    r2273 r2278  
    11include "ASM/AssemblyProofSplit.ma".
    22include "common/LabelledObjects.ma".
    3 
    4 lemma short_jump_cond_ok:
    5   ∀v1, v2: Word.
    6   ∀is_possible, offset.
    7     〈is_possible, offset〉 = short_jump_cond v1 v2 →
    8       is_possible → v2 = add 16 v1 (sign_extension offset).
    9   #v1 #v2 #is_possible #offset
    10   whd in match short_jump_cond; normalize nodelta
    11   @pair_elim #result #flags #sub16_refl
    12   @pair_elim #upper #lower #vsplit_refl
    13   inversion (get_index' bool ???) #get_index_refl normalize nodelta
    14   #relevant destruct(relevant) #relevant
    15   [1:
    16     @(sub_16_to_add_16_8_1 … flags)
    17   |2:
    18     @(sub_16_to_add_16_8_0 … flags)
    19   ]
    20   try assumption >sub16_refl
    21   <(eq_bv_eq … relevant)
    22   >(vsplit_ok … (sym_eq … vsplit_refl)) %
    23 qed.
    243
    254lemma absolute_jump_cond_ok:
Note: See TracChangeset for help on using the changeset viewer.