Changeset 2266 for src/ASM


Ignore:
Timestamp:
Jul 26, 2012, 10:43:55 AM (7 years ago)
Author:
sacerdot
Message:

All daemons closed in Jmp case.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/AssemblyProofSplitSplit.ma

    r2264 r2266  
    3737  <(vsplit_ok … (sym_eq … vsplit_v2_refl))
    3838  >(eq_bv_eq … relevant) %
     39qed.
     40
     41lemma ticks_of_instruction_AJMP:
     42 ∀address. ticks_of_instruction (AJMP (ADDR11 address)) = 2.
     43try % #addr @(vsplit_elim … 3 8 addr) #vl #vm #EQ >EQ
     44@(bitvector_3_elim_prop … vl) %
     45qed.
     46
     47lemma ticks_of_instruction_ACALL:
     48 ∀address. ticks_of_instruction (ACALL (ADDR11 address)) = 2.
     49try % #addr @(vsplit_elim … 3 8 addr) #vl #vm #EQ >EQ
     50@(bitvector_3_elim_prop … vl) %
    3951qed.
    4052
     
    144156      whd in match (assembly_1_pseudoinstruction ??????) in ⊢ (% → ?);
    145157      whd in match (expand_pseudo_instruction ??????);
     158      whd in match (ticks_of0 ??????);
    146159      inversion (short_jump_cond ??) #sj_possible #offset #sjc_refl normalize nodelta
    147160      inversion (sj_possible ∧ ¬ policy ?) #sj_possible_refl normalize nodelta
     
    165178      >EQassembled in fetch_refl; #fetch_refl <fetch_refl
    166179      lapply (eq_bv_eq … fetch_many_assm) -fetch_many_assm #EQnewpc
    167       whd in ⊢ (??%%);
    168       (* XXX: now we start to work on the mk_PreStatus equality *)
    169       (* XXX: lhs *)
    170       (* XXX: rhs *)
    171       (* here we are *)
    172       @split_eq_status try % /demod nohyps/
    173       [1,3,4:
    174         change with (add ???) in match (\snd (half_add ???));
    175         whd in match execute_1_pseudo_instruction0; normalize nodelta
    176         /demod nohyps/ >set_clock_set_program_counter
    177         >program_counter_set_program_counter
    178         whd in ⊢ (??%?); normalize nodelta whd in match address_of_word_labels; normalize nodelta
    179         lapply (create_label_cost_map_ok 〈preamble, instr_list〉) >create_label_cost_refl
    180         normalize nodelta #address_of_word_labels_assm <address_of_word_labels_assm
    181         [1:
    182           >EQnewpc
    183           inversion (vsplit bool ???) #pc_bu #pc_bl #vsplit_refl normalize nodelta
    184           @sym_eq
    185           >EQlookup_labels in mjc_refl; #mjc_refl
    186           @(absolute_jump_cond_ok ?????? (sym_eq … mjc_refl) (sym_eq … vsplit_refl))
    187           >(andb_true_l … mj_possible_refl) @I
    188         |3:
    189           >EQlookup_labels normalize nodelta %
    190         |5:
    191           >EQnewpc
    192           inversion (half_add ???) #carry #new_pc #half_add_refl normalize nodelta
    193           @sym_eq
     180      change with (set_program_counter ???? =
     181       status_of_pseudo_status ?? (set_program_counter ????) ??)
     182       @set_program_counter_status_of_pseudo_status
     183       [2,4,6: @sym_eq @set_clock_status_of_pseudo_status try %
     184         [1,3,4: @sym_eq @set_program_counter_status_of_pseudo_status try %
     185                 @sigma_increment_commutation
     186         | @eq_f2 try % @ticks_of_instruction_AJMP ]]
     187       whd in ⊢ (??%%); normalize nodelta whd in match address_of_word_labels;
     188       normalize nodelta
     189       [ inversion (vsplit bool ???) #pc_bu #pc_bl #vsplit_refl normalize nodelta
     190         >EQlookup_labels in mjc_refl; >create_label_cost_refl #mjc_refl
     191         @(absolute_jump_cond_ok ????? pc_bl (sym_eq … mjc_refl))
     192         [2: >(andb_true_l … mj_possible_refl) %
     193         | <vsplit_refl @eq_f <EQnewpc % ]
     194       | >EQlookup_labels >create_label_cost_refl %
     195       |  inversion (half_add ???) #carry #new_pc #half_add_refl normalize nodelta
     196          >create_label_cost_refl
    194197          >EQlookup_labels in sjc_refl; #sjc_refl
    195198          >(pair_destruct_2 ????? (sym_eq … half_add_refl))
    196           @(short_jump_cond_ok ???? (sym_eq … sjc_refl))
    197           >(andb_true_l … sj_possible_refl) @I
    198         ]
    199         whd in is_well_labelled_witness;
    200         @(is_well_labelled_witness ? ppc ppc_in_bounds pi)
    201         try (>fetch_pseudo_refl %)
    202         >pi_refl %
    203       |2:
    204         whd in ⊢ (??(?%%)%);
    205         cases (bitvector_11_cases address)
    206         * * * * * * #b4 * #b5
    207         * #b6 * #b7 * #b8 * #b9 * #b10 * #b11 #address_refl >address_refl
    208         normalize in match (fetch ??); <plus_n_Sm @eq_f
    209         @commutative_plus
     199          >(short_jump_cond_ok ???? (sym_eq … sjc_refl))
     200          [2: >(andb_true_l … sj_possible_refl) %
     201          | >EQnewpc % ]]
     202    |5: (* Call *)
     203      #arg1 #pi_refl
     204      (* XXX: we first work on sigma_increment_commutation *)
     205      whd in match (assembly_1_pseudoinstruction ??????) in ⊢ (% → ?);
     206      whd in match (expand_pseudo_instruction ??????);
     207      whd in match (ticks_of0 ??????);
     208      inversion (short_jump_cond ??) #sj_possible #offset #sjc_refl normalize nodelta
     209      inversion (sj_possible ∧ ¬ policy ?) #sj_possible_refl normalize nodelta
     210      [2:
     211        inversion (absolute_jump_cond ??) #mj_possible #address #mjc_refl normalize nodelta
     212        inversion (mj_possible ∧ ¬ policy ?) #mj_possible_refl normalize nodelta
    210213      ]
    211     |5: (* Call *)
     214      #sigma_increment_commutation
     215      normalize in sigma_increment_commutation:(???(???(??%)));
     216      (* XXX: we work on the maps *)
     217      whd in ⊢ (??%? → ?); @Some_Some_elim #map_refl_assm <map_refl_assm
     218      (* XXX: we assume the fetch_many hypothesis *)
     219      * #fetch_refl #fetch_many_assm
     220      (* XXX: we give the existential *)
     221      %{1}
     222      (* XXX: work on the left hand side of the equality *)
     223      whd in ⊢ (??%?); whd in match (program_counter ???);
     224      (* XXX: execute fetches some more *)
     225      whd in match code_memory_of_pseudo_assembly_program; normalize nodelta
     226      whd in fetch_many_assm;
     227      >EQassembled in fetch_refl; #fetch_refl <fetch_refl
     228      lapply (eq_bv_eq … fetch_many_assm) -fetch_many_assm #EQnewpc
     229      change with (set_program_counter ???? =
     230       status_of_pseudo_status ?? (set_program_counter ????) ??)
     231       @set_program_counter_status_of_pseudo_status
     232       [2,4,6: @sym_eq @set_clock_status_of_pseudo_status try %
     233         [1,3,4: @sym_eq @set_program_counter_status_of_pseudo_status try %
     234                 @sigma_increment_commutation
     235         | @eq_f2 try % @ticks_of_instruction_AJMP ]]
     236       whd in ⊢ (??%%); normalize nodelta whd in match address_of_word_labels;
     237       normalize nodelta
     238       [ inversion (vsplit bool ???) #pc_bu #pc_bl #vsplit_refl normalize nodelta
     239         >EQlookup_labels in mjc_refl; >create_label_cost_refl #mjc_refl
     240         @(absolute_jump_cond_ok ????? pc_bl (sym_eq … mjc_refl))
     241         [2: >(andb_true_l … mj_possible_refl) %
     242         | <vsplit_refl @eq_f <EQnewpc % ]
     243       | >EQlookup_labels >create_label_cost_refl %
     244       |  inversion (half_add ???) #carry #new_pc #half_add_refl normalize nodelta
     245          >create_label_cost_refl
     246          >EQlookup_labels in sjc_refl; #sjc_refl
     247          >(pair_destruct_2 ????? (sym_eq … half_add_refl))
     248          >(short_jump_cond_ok ???? (sym_eq … sjc_refl))
     249          [2: >(andb_true_l … sj_possible_refl) %
     250          | >EQnewpc % ]]
     251   
     252   
     253   
     254   
     255   
     256   
     257   
     258   
     259   
     260   
     261   
     262   
    212263      #arg1 #pi_refl
    213264      (* XXX: we first work on sigma_increment_commutation *)
Note: See TracChangeset for help on using the changeset viewer.