Changeset 2062


Ignore:
Timestamp:
Jun 13, 2012, 5:00:35 PM (5 years ago)
Author:
sacerdot
Message:

Everything repaired (broken because of new proof obligation for fetch).

Location:
src/ASM
Files:
2 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/AssemblyProofSplitSplit.ma

    r2051 r2062  
    2727  λinstr_list.
    2828  ∀id: Identifier.
    29   ∀ppc.
     29  ∀ppc. ∀ppc_ok.
    3030  ∀i.
    31     fetch_pseudo_instruction instr_list ppc = i →
     31    fetch_pseudo_instruction instr_list ppc ppc_ok = i →
    3232      instruction_has_label id (\fst i) →
    3333        occurs_exactly_once ASMTag pseudo_instruction id instr_list.
     
    105105  ∀sigma_policy_specification_witness: sigma_policy_specification program sigma policy.
    106106  ∀ps: PseudoStatus program.
    107   ∀program_counter_in_bounds: nat_of_bitvector 16 (program_counter … ps) |\snd program|.
    108     next_internal_pseudo_address_map M program ps = Some … M' →
     107  ∀program_counter_in_bounds: nat_of_bitvector 16 (program_counter … ps) < |\snd program|.
     108    next_internal_pseudo_address_map M program ps program_counter_in_bounds = Some … M' →
    109109      ∃n. execute n … (status_of_pseudo_status M … ps sigma policy) =
    110110        status_of_pseudo_status M' …
    111           (execute_1_pseudo_instruction (ticks_of program sigma policy) program ps) sigma policy.
    112   #M #M' * #preamble #instr_list #is_well_labelled_witness #sigma #policy #sigma_policy_witness #ps #program_counter_in_bounds
     111          (execute_1_pseudo_instruction program (ticks_of program sigma policy) ps program_counter_in_bounds) sigma policy.
     112  #M #M' * #preamble #instr_list #is_well_labelled_witness #sigma #policy #sigma_policy_witness #ps
     113  letin ppc ≝ (program_counter pseudo_assembly_program ? ps) #ppc_in_bounds
    113114  change with (next_internal_pseudo_address_map0 ????? = ? → ?)
    114   @(pose … (program_counter ?? ps)) #ppc #EQppc
    115   generalize in match (fetch_assembly_pseudo2 〈preamble,instr_list〉 sigma policy sigma_policy_witness ppc) in ⊢ ?;
     115  generalize in match (fetch_assembly_pseudo2 〈preamble,instr_list〉 sigma policy sigma_policy_witness ppc ppc_in_bounds) in ⊢ ?;
    116116  @pair_elim #labels #costs #create_label_cost_refl normalize nodelta
    117117  @pair_elim #assembled #costs' #assembly_refl normalize nodelta
     
    121121  @(pose … (λx. lookup_def … (construct_datalabels preamble) x (zero 16))) #lookup_datalabels #EQlookup_datalabels
    122122  whd in match execute_1_pseudo_instruction; normalize nodelta
    123   whd in match ticks_of; normalize nodelta <EQppc >fetch_pseudo_refl normalize nodelta
    124   lapply (snd_fetch_pseudo_instruction instr_list ppc) >fetch_pseudo_refl #EQnewppc >EQnewppc
     123  whd in match ticks_of; normalize nodelta >fetch_pseudo_refl normalize nodelta
     124  lapply (snd_fetch_pseudo_instruction instr_list ppc ppc_in_bounds) >fetch_pseudo_refl #EQnewppc >EQnewppc
    125125  lapply (snd_assembly_1_pseudoinstruction_ok 〈preamble,instr_list〉 … sigma policy sigma_policy_witness … ppc ? pi … EQlookup_labels EQlookup_datalabels ?)
    126   [1: >fetch_pseudo_refl % |2: >EQppc assumption ]
     126  [1: >fetch_pseudo_refl % |2: skip ]
    127127  #assm1 #assm2 #assm3 generalize in match assm2; generalize in match assm3;
    128128  generalize in match assm1; -assm1 -assm2 -assm3
     
    144144    whd in ⊢ (??%?);
    145145    @split_eq_status try %
    146     /demod/ >EQnewppc >sigma_increment_commutation <add_zero % (*CSC: auto not working, why? *)
     146    /demod/ >add_commutative <add_zero % (*CSC: auto not working, why? *)
    147147  |6: (* Mov *)
    148148    #arg1 #arg2 #_
     
    158158    whd in match (execute_1_pseudo_instruction0 ?????);
    159159    (* XXX: work on the left hand side of the equality *)
    160     whd in ⊢ (??%?); whd in match (program_counter ???); <EQppc
     160    whd in ⊢ (??%?); whd in match (program_counter ???);
    161161    (* XXX: execute fetches some more *)
    162162    whd in match code_memory_of_pseudo_assembly_program; normalize nodelta
     
    189189    #instr #_ #EQP #EQnext #fetch_many_assm
    190190    @(main_lemma_preinstruction M M' preamble instr_list 〈preamble, instr_list〉 (refl …) sigma policy sigma_policy_witness
    191       ps ppc EQppc labels costs create_label_cost_refl newppc lookup_labels EQlookup_labels lookup_datalabels EQlookup_datalabels
     191      ps ppc ? labels costs create_label_cost_refl newppc lookup_labels EQlookup_labels lookup_datalabels EQlookup_datalabels
    192192      EQnewppc instr (ticks_of0 〈preamble, instr_list〉 sigma policy ppc (Instruction instr)) (refl …)
    193193      (λx:Identifier. λy:PreStatus pseudo_assembly_program 〈preamble, instr_list〉. address_of_word_labels 〈preamble, instr_list〉 x) (refl …) (set_program_counter pseudo_assembly_program 〈preamble, instr_list〉 ps (add 16 ppc (bitvector_of_nat 16 1)))
    194194      (refl …) ? (refl …))
    195     try assumption >assembly_refl <EQppc assumption
    196   |4:
     195    try assumption try % >assembly_refl assumption
     196  |4: (* Jmp *)
    197197    #arg1 #pi_refl
    198198    (* XXX: we first work on sigma_increment_commutation *)
     
    214214    %{1}
    215215    (* XXX: work on the left hand side of the equality *)
    216     whd in ⊢ (??%?); whd in match (program_counter ???); <EQppc
     216    whd in ⊢ (??%?); whd in match (program_counter ???);
    217217    (* XXX: execute fetches some more *)
    218218    whd in match code_memory_of_pseudo_assembly_program; normalize nodelta
     
    272272    ]
    273273  |5: (* Call *)
    274     #arg1
     274    #arg1 #_
    275275    (* XXX: we first work on sigma_increment_commutation *)
    276276    #sigma_increment_commutation
  • src/ASM/Interpret.ma

    r2056 r2062  
    12221222
    12231223definition execute_1_pseudo_instruction:
    1224  (Word → nat × nat) → ∀cm. ∀s:PseudoStatus cm.
     1224 ∀cm. (∀ppc:Word. nat_of_bitvector … ppc < |\snd cm| → nat × nat) → ∀s:PseudoStatus cm.
    12251225   nat_of_bitvector 16 (program_counter pseudo_assembly_program cm s) <|\snd  cm| →
    12261226    PseudoStatus cm
    12271227
    1228   λticks_of,cm,s,pc_ok.
     1228  λcm,ticks_of,s,pc_ok.
    12291229  let 〈instr, pc〉 ≝ fetch_pseudo_instruction (\snd cm) (program_counter … s) pc_ok in
    1230   let ticks ≝ ticks_of (program_counter … s) in
     1230  let ticks ≝ ticks_of (program_counter … s) pc_ok in
    12311231   execute_1_pseudo_instruction0 ticks cm s instr pc.
    12321232
Note: See TracChangeset for help on using the changeset viewer.