Ignore:
Timestamp:
Jun 12, 2012, 2:18:16 PM (7 years ago)
Author:
mulligan
Message:

Big bugs in policy calculations found. Waiting for Jaap's commit.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/AssemblyProofSplitSplit.ma

    r2027 r2047  
    11include "ASM/AssemblyProofSplit.ma".
     2include "common/LabelledObjects.ma".
     3
     4check pseudo_instruction
     5
     6definition instruction_has_label ≝
     7  λid: Identifier.
     8  λi.
     9  match i with
     10  [ Jmp j ⇒ j = id
     11  | Call j ⇒ j = id
     12  | Instruction instr ⇒
     13    match instr with
     14    [ JC j ⇒ j = id
     15    | JNC j ⇒ j = id
     16    | JZ j ⇒ j = id
     17    | JNZ j ⇒ j = id
     18    | JB _ j ⇒ j = id
     19    | JBC _ j ⇒ j = id
     20    | DJNZ _ j ⇒ j = id
     21    | CJNE _ j ⇒ j = id
     22    | _ ⇒ False
     23    ]
     24  | _ ⇒ False
     25  ].
     26 
     27
     28definition is_well_labelled_p ≝
     29  λinstr_list.
     30  ∀id: Identifier.
     31  ∀ppc.
     32  ∀i.
     33    fetch_pseudo_instruction instr_list ppc = i →
     34      instruction_has_label id (\fst i) →
     35        occurs_exactly_once ASMTag pseudo_instruction id instr_list.
    236
    337theorem main_thm:
    438  ∀M, M': internal_pseudo_address_map.
    539  ∀program: pseudo_assembly_program.
     40  ∀is_well_labelled: is_well_labelled_p (\snd program).
    641  ∀sigma: Word → Word.
    742  ∀policy: Word → bool.
     
    1348        status_of_pseudo_status M' …
    1449          (execute_1_pseudo_instruction (ticks_of program sigma policy) program ps) sigma policy.
    15   #M #M' * #preamble #instr_list #sigma #policy #sigma_policy_witness #ps #program_counter_in_bounds
     50  #M #M' * #preamble #instr_list #is_well_labelled_witness #sigma #policy #sigma_policy_witness #ps #program_counter_in_bounds
    1651  change with (next_internal_pseudo_address_map0 ????? = ? → ?)
    1752  @(pose … (program_counter ?? ps)) #ppc #EQppc
     
    3166  generalize in match assm1; -assm1 -assm2 -assm3
    3267  normalize nodelta
    33   cases pi
     68  inversion pi
    3469  [2,3:
    35     #arg
     70    #arg #_
    3671    (* XXX: we first work on sigma_increment_commutation *)
    3772    #sigma_increment_commutation
     
    4984    [1,2: /demod/ >EQnewppc >sigma_increment_commutation <add_zero % (*CSC: auto not working, why? *) ]
    5085  |6: (* Mov *)
    51     #arg1 #arg2
     86    #arg1 #arg2 #_
    5287    (* XXX: we first work on sigma_increment_commutation *)
    5388    #sigma_increment_commutation
     
    83118    >set_arg_16_mk_Status_commutation in ⊢ (???%);
    84119    (* here we are *)
    85     @split_eq_status //
     120    @split_eq_status try %
    86121    [1:
    87122      assumption
    88123    |2:
    89       @special_function_registers_8051_set_arg_16
    90       [2: %
    91       |1: //
    92       ]
     124      @special_function_registers_8051_set_arg_16 %
    93125    ]
    94126  |1: (* Instruction *)
    95     -pi #instr #EQP #EQnext #fetch_many_assm
     127    #instr #_ #EQP #EQnext #fetch_many_assm
    96128    @(main_lemma_preinstruction M M' preamble instr_list 〈preamble, instr_list〉 (refl …) sigma policy sigma_policy_witness
    97129      ps ppc EQppc labels costs create_label_cost_refl newppc lookup_labels EQlookup_labels lookup_datalabels EQlookup_datalabels
     
    100132      (refl …) ? (refl …))
    101133    try assumption >assembly_refl <EQppc assumption
    102     check status_of_pseudo_status
    103134  |4:
     135    #arg1 #pi_refl
     136    (* XXX: we first work on sigma_increment_commutation *)
     137    whd in match (assembly_1_pseudoinstruction ??????) in ⊢ (% → ?);
     138    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
     144    [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
     148    ]
     149    #sigma_increment_commutation
     150    normalize in sigma_increment_commutation:(???(???(??%)));
     151    (* XXX: we work on the maps *)
     152    whd in ⊢ (??%? → ?); @Some_Some_elim #map_refl_assm <map_refl_assm
     153    (* XXX: we assume the fetch_many hypothesis *)
     154    * #fetch_refl #fetch_many_assm
     155    (* XXX: we give the existential *)
     156    %{1}
     157    (* XXX: work on the left hand side of the equality *)
     158    whd in ⊢ (??%?); whd in match (program_counter ???); <EQppc
     159    (* XXX: execute fetches some more *)
     160    whd in match code_memory_of_pseudo_assembly_program; normalize nodelta
     161    whd in fetch_many_assm;
     162    >EQassembled in fetch_refl; #fetch_refl <fetch_refl -fetch_refl
     163    lapply (eq_bv_eq … fetch_many_assm) -fetch_many_assm #EQnewpc
     164    whd in ⊢ (??%%);
     165    (* XXX: now we start to work on the mk_PreStatus equality *)
     166    (* XXX: lhs *)
     167    (* XXX: rhs *)
     168    (* here we are *)
     169    @split_eq_status try % /demod nohyps/
     170    [1,3,4:
     171      change with (add ???) in match (\snd (half_add ???));
     172      whd in match execute_1_pseudo_instruction0; normalize nodelta
     173      /demod nohyps/ >set_clock_set_program_counter
     174      >program_counter_set_program_counter
     175      whd in ⊢ (??%?); normalize nodelta whd in match address_of_word_labels; normalize nodelta
     176      lapply (create_label_cost_map_ok 〈preamble, instr_list〉) >create_label_cost_refl
     177      normalize nodelta #address_of_word_labels_assm <address_of_word_labels_assm
     178      [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
     184      |3:
     185        >EQnewpc >pc_refl normalize nodelta
     186        >(pair_destruct_2 ????? (sym_eq … addr_refl))
     187        >(pair_destruct_1 ????? (sym_eq … pc_refl)) >EQnewpc
     188        >EQlookup_labels normalize nodelta
     189        >address_of_word_labels_assm try %
     190      |5:
     191        >EQnewpc
     192      ]
     193      @(is_well_labelled_witness … fetch_pseudo_refl)
     194      >pi_refl %
     195    |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
     207    ]
     208  |5: (* Call *)
    104209    #arg1
    105210    (* XXX: we first work on sigma_increment_commutation *)
     
    119224    whd in fetch_many_assm;
    120225    >EQassembled in fetch_many_assm;
    121     cases (fetch ??) * #instr #newpc #ticks normalize nodelta *
     226    cases (fetch ??) * #instr #newpc #?ticks normalize nodelta *
    122227    #eq_instr
    123228    #fetch_many_assm whd in fetch_many_assm;
     
    145250      ]
    146251    ]
    147   |5: cases daemon
    148252  ]
    149253qed.
Note: See TracChangeset for help on using the changeset viewer.