Changeset 2051


Ignore:
Timestamp:
Jun 12, 2012, 5:49:02 PM (5 years ago)
Author:
mulligan
Message:

Finished the Jmp case in the main theorem.

Location:
src/ASM
Files:
3 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/Assembly.ma

    r2048 r2051  
    2020  λpc_plus_jmp_length.λaddr.(*λinstr.*)
    2121  let 〈result, flags〉 ≝ sub_16_with_carry addr pc_plus_jmp_length false in
    22   let 〈upper, lower〉 ≝ vsplit ? 8 8 result in
     22  let 〈upper, lower〉 ≝ vsplit ? 9 7 result in
    2323    if get_index' ? 2 0 flags then
    24       〈eq_bv 8 upper [[true;true;true;true;true;true;true;true]], lower〉
     24      〈eq_bv 9 upper [[true;true;true;true;true;true;true;true;true]], true:::lower〉
    2525    else
    26       〈eq_bv 8 upper (zero 8), zero 8〉.
     26      〈eq_bv 9 upper (zero …), false:::lower〉.
    2727 
    2828definition medium_jump_cond: Word → Word → (*pseudo_instruction →*)
  • src/ASM/AssemblyProofSplitSplit.ma

    r2047 r2051  
    11include "ASM/AssemblyProofSplit.ma".
    22include "common/LabelledObjects.ma".
    3 
    4 check pseudo_instruction
    53
    64definition instruction_has_label ≝
     
    3533        occurs_exactly_once ASMTag pseudo_instruction id instr_list.
    3634
     35(*CSC: move elsewhere *)
     36axiom sub_16_to_add_16_8_0:
     37 ∀v1,v2: BitVector 16. ∀v3: BitVector 7. ∀flags: BitVector 3.
     38  get_index' ? 2 0 flags = false →
     39  sub_16_with_carry v1 v2 false = 〈(zero 9)@@v3,flags〉 →
     40   v1 = add ? v2 (sign_extension (false:::v3)).
     41
     42(*CSC: move elsewhere *)
     43axiom sub_16_to_add_16_8_1:
     44 ∀v1,v2: BitVector 16. ∀v3: BitVector 7. ∀flags: BitVector 3.
     45  get_index' ? 2 0 flags = true →
     46  sub_16_with_carry v1 v2 false = 〈[[true;true;true;true;true;true;true;true;true]]@@v3,flags〉 →
     47   v1 = add ? v2 (sign_extension (true:::v3)).
     48
     49(*CSC: move elsewhere *)
     50lemma vsplit_ok:
     51  ∀A: Type[0].
     52  ∀m, n: nat.
     53  ∀v: Vector A (m + n).
     54  ∀upper: Vector A m.
     55  ∀lower: Vector A n.
     56    〈upper, lower〉 = vsplit A m n v →
     57      upper @@ lower = v.
     58  #A #m #n #v #upper #lower
     59  cases daemon
     60qed.
     61
     62lemma short_jump_cond_ok:
     63  ∀v1, v2: Word.
     64  ∀is_possible, offset.
     65    〈is_possible, offset〉 = short_jump_cond v1 v2 →
     66      is_possible → v2 = add 16 v1 (sign_extension offset).
     67  #v1 #v2 #is_possible #offset
     68  whd in match short_jump_cond; normalize nodelta
     69  @pair_elim #result #flags #sub16_refl
     70  @pair_elim #upper #lower #vsplit_refl
     71  inversion (get_index' bool ???) #get_index_refl normalize nodelta
     72  #relevant destruct(relevant) #relevant
     73  [1:
     74    @(sub_16_to_add_16_8_1 … flags)
     75  |2:
     76    @(sub_16_to_add_16_8_0 … flags)
     77  ]
     78  try assumption >sub16_refl
     79  <(eq_bv_eq … relevant)
     80  >(vsplit_ok … (sym_eq … vsplit_refl)) %
     81qed.
     82
     83lemma medium_jump_cond_ok:
     84  ∀v1, v2: Word.
     85  ∀is_possible, offset, v1_upper, v1_lower.
     86    〈is_possible, offset〉 = medium_jump_cond v1 v2 →
     87      〈v1_upper, v1_lower〉 = vsplit ? 5 11 v1 →
     88        is_possible → v2 = v1_upper @@ offset.
     89  #v1 #v2 #is_possible #offset #v1_upper #v1_lower
     90  whd in match medium_jump_cond; normalize nodelta
     91  @pair_elim #fst_5_addr #rest_addr #vsplit_v2_refl
     92  @pair_elim #fst_5_pc #rest_pc #vsplit_v1_refl
     93  #relevant destruct(relevant) normalize nodelta #relevant
     94  destruct(relevant) #relevant
     95  <(vsplit_ok … (sym_eq … vsplit_v2_refl))
     96  >(eq_bv_eq … relevant) %
     97qed.
     98       
    3799theorem main_thm:
    38100  ∀M, M': internal_pseudo_address_map.
     
    81143    (* XXX: work on the left hand side of the equality *)
    82144    whd in ⊢ (??%?);
    83     @split_eq_status //
    84     [1,2: /demod/ >EQnewppc >sigma_increment_commutation <add_zero % (*CSC: auto not working, why? *) ]
     145    @split_eq_status try %
     146    /demod/ >EQnewppc >sigma_increment_commutation <add_zero % (*CSC: auto not working, why? *)
    85147  |6: (* Mov *)
    86148    #arg1 #arg2 #_
     
    137199    whd in match (assembly_1_pseudoinstruction ??????) in ⊢ (% → ?);
    138200    whd in match (expand_pseudo_instruction ??????);
    139 (*    generalize in match (refl … (expand_pseudo_instruction lookup_labels sigma policy ppc lookup_datalabels (Jmp arg1)));
    140     whd in match (expand_pseudo_instruction ??????) in ⊢ (??%? → % → ?); *)
    141     inversion (sub_16_with_carry ???) #result #flags #sub16_refl normalize nodelta
    142     inversion (vsplit ????) #upper #lower #vsplit_refl normalize nodelta
    143     inversion (eq_bv ??? ∧ ¬ policy ?) #eq_bv_policy_refl normalize nodelta
     201    inversion (short_jump_cond ??) #sj_possible #offset #sjc_refl normalize nodelta
     202    inversion (sj_possible ∧ ¬ policy ?) #sj_possible_refl normalize nodelta
    144203    [2:
    145       inversion (vsplit ????) #fst_5_addr #rest_addr #addr_refl normalize nodelta
    146       inversion (vsplit ????) #fst_5_pc #rest_pc #pc_refl normalize nodelta
    147       cases (eq_bv ??? ∧ ¬ policy ?) normalize nodelta
     204      inversion (medium_jump_cond ??) #mj_possible #address #mjc_refl normalize nodelta
     205      inversion (mj_possible ∧ ¬ policy ?) #mj_possible_refl normalize nodelta
    148206    ]
    149207    #sigma_increment_commutation
     
    160218    whd in match code_memory_of_pseudo_assembly_program; normalize nodelta
    161219    whd in fetch_many_assm;
    162     >EQassembled in fetch_refl; #fetch_refl <fetch_refl -fetch_refl
     220    >EQassembled in fetch_refl; #fetch_refl <fetch_refl
    163221    lapply (eq_bv_eq … fetch_many_assm) -fetch_many_assm #EQnewpc
    164222    whd in ⊢ (??%%);
     
    177235      normalize nodelta #address_of_word_labels_assm <address_of_word_labels_assm
    178236      [1:
    179         -address_of_word_labels_assm >EQnewpc >pc_refl normalize nodelta
    180         >(pair_destruct_2 ????? (sym_eq … addr_refl))
    181         >(pair_destruct_1 ????? (sym_eq … pc_refl)) >EQnewpc
    182         (* XXX: true but needs lemma about splitting *)
    183         cases daemon
     237        >EQnewpc
     238        inversion (vsplit bool ???) #pc_bu #pc_bl #vsplit_refl normalize nodelta
     239        @sym_eq >address_of_word_labels_assm
     240        [1:
     241          >EQlookup_labels in mjc_refl; #mjc_refl
     242          @(medium_jump_cond_ok ?????? (sym_eq … mjc_refl) (sym_eq … vsplit_refl))
     243          >(andb_true_l … mj_possible_refl) @I
     244        ]
    184245      |3:
    185         >EQnewpc >pc_refl normalize nodelta
    186         >(pair_destruct_2 ????? (sym_eq … addr_refl))
    187         >(pair_destruct_1 ????? (sym_eq … pc_refl)) >EQnewpc
    188246        >EQlookup_labels normalize nodelta
    189247        >address_of_word_labels_assm try %
    190248      |5:
    191249        >EQnewpc
     250        inversion (half_add ???) #carry #new_pc #half_add_refl normalize nodelta
     251        @sym_eq >address_of_word_labels_assm
     252        [1:
     253          >EQlookup_labels in sjc_refl; #sjc_refl
     254          >(pair_destruct_2 ????? (sym_eq … half_add_refl))
     255          @(short_jump_cond_ok ???? (sym_eq … sjc_refl))
     256          >(andb_true_l … sj_possible_refl) @I
     257        ]
    192258      ]
    193259      @(is_well_labelled_witness … fetch_pseudo_refl)
    194260      >pi_refl %
    195261    |2:
    196       whd in match compute_target_of_unconditional_jump; normalize nodelta
    197       >program_counter_set_program_counter
    198       cases (vsplit ????) #pc_bu #pc_bl normalize nodelta
    199       cases (vsplit ????) #nu #nl normalize nodelta
    200       cases (vsplit ????) #relevant1 #relevant2 normalize nodelta
    201       change with (add ???) in match (\snd (half_add ???)); >EQnewpc
    202       cases daemon
    203     |3:
    204       whd in ⊢ (??%%);
    205       /demod nohyps/
    206       cases daemon
     262      whd in ⊢ (??(?%%)%);
     263      cut (∃b1,b2,b3,b4,b5,b6,b7,b8,b9,b10,b11. address = [[b1;b2;b3;b4;b5;b6;b7;b8;b9;b10;b11]])
     264      [1:
     265        cases daemon (* XXX: easy but massive proof, move into separate lemma *)
     266      |2:
     267        * * * * * * * #b4 * #b5
     268        * #b6 * #b7 * #b8 * #b9 * #b10 * #b11 #address_refl >address_refl
     269        normalize in match (fetch ??); <plus_n_Sm @eq_f
     270        @commutative_plus
     271      ]
    207272    ]
    208273  |5: (* Call *)
  • src/ASM/Interpret.ma

    r2047 r2051  
    11701170
    11711171lemma execute_1_ok: ∀cm.∀s.
    1172   let instr_pc_ticks ≝ fetch cm (program_counter … s) in
    1173     (clock ?? (execute_1 cm s) = current_instruction_cost … s + clock … s) ∧
     1172  (clock ?? (execute_1 cm s) = current_instruction_cost … s + clock … s) ∧
     1173    let instr_pc_ticks ≝ fetch cm (program_counter … s) in
    11741174      (ASM_classify0 (\fst (\fst instr_pc_ticks)) = cl_other →
    11751175        program_counter ? cm (execute_1 cm s) =
Note: See TracChangeset for help on using the changeset viewer.