Ignore:
Timestamp:
Jul 26, 2012, 12:38:42 AM (7 years ago)
Author:
sacerdot
Message:

1) Major change: we now always use the efficient way of resolving labels

for the interpretation of pseudo assembly code. The inefficient way is
only used locally in ASM/Interpret.ma to prove some properties more easily.

2) AssemblyProofSplitSplit?.ma partially repaired. In particular, the main

lemma is now called correctly thanks to the previous change.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/AssemblyProofSplitSplit.ma

    r2140 r2264  
    3838  >(eq_bv_eq … relevant) %
    3939qed.
    40  
     40
    4141theorem main_thm:
    4242  ∀M, M': internal_pseudo_address_map.
    4343  ∀program: pseudo_assembly_program.
    4444  ∀program_in_bounds: |\snd program| ≤ 2^16.
    45   ∀addr_of: Identifier → PreStatus pseudo_assembly_program program → BitVector 16.
     45  let 〈labels, costs〉 ≝ create_label_cost_map (\snd program) in
     46  let addr_of ≝ λid.λ_.bitvector_of_nat 16 (lookup_def ASMTag ℕ labels id O) in
    4647  ∀is_well_labelled: is_well_labelled_p (\snd program).
    4748  ∀sigma: Word → Word.
     
    5354      ∃n. execute n … (status_of_pseudo_status M … ps sigma policy) =
    5455        status_of_pseudo_status M' …
    55           (execute_1_pseudo_instruction program (ticks_of program sigma policy) ps program_counter_in_bounds) sigma policy.
    56     #M #M' * #preamble #instr_list #program_in_bounds #addr_of
     56          (execute_1_pseudo_instruction program (ticks_of program (λid. addr_of id ps) sigma policy) ps program_counter_in_bounds) sigma policy.
     57    #M #M' * #preamble #instr_list #program_in_bounds
     58    @pair_elim #labels #cost #create_label_cost_refl
    5759    #is_well_labelled_witness #sigma #policy #sigma_policy_witness #ps
    5860    letin ppc ≝ (program_counter pseudo_assembly_program ? ps) #ppc_in_bounds
    5961    change with (next_internal_pseudo_address_map0 ?????? = ? → ?)
    6062    generalize in match (fetch_assembly_pseudo2 〈preamble,instr_list〉 program_in_bounds sigma policy sigma_policy_witness ppc ppc_in_bounds) in ⊢ ?;
    61     @pair_elim #labels #costs #create_label_cost_refl normalize nodelta
     63    >create_label_cost_refl normalize nodelta
    6264    @pair_elim #assembled #costs' #assembly_refl normalize nodelta
    6365    lapply (pair_destruct_1 ????? (sym_eq ??? assembly_refl)) #EQassembled
     
    8789      (* XXX: we give the existential *)
    8890      %{0}
     91      whd in match execute_1_pseudo_instruction0; normalize nodelta
     92      change with (status_of_pseudo_status ????? = ?) cases daemon (*CSC: ???
    8993      whd in match (execute_1_pseudo_instruction0 ?????);
    9094      (* XXX: work on the left hand side of the equality *)
    9195      whd in ⊢ (??%?);
    9296      @split_eq_status try %
    93       /demod/ >add_commutative <add_zero % (*CSC: auto not working, why? *)
     97      /demod/ >add_commutative <add_zero % (*CSC: auto not working, why? *) *)
    9498    |6: (* Mov *)
    9599      #arg1 #arg2 #_
     
    114118      #fetch_many_assm whd in fetch_many_assm;
    115119      lapply (eq_bv_eq … fetch_many_assm) -fetch_many_assm #EQnewpc
    116       destruct whd in ⊢ (??%?);
     120      destruct
    117121      (* XXX: now we start to work on the mk_PreStatus equality *)
    118122      (* XXX: lhs *)
    119123      change with (set_arg_16 ????? = ?)
    120       >set_program_counter_mk_Status_commutation
    121       >set_clock_mk_Status_commutation
    122       >set_arg_16_mk_Status_commutation
    123       (* XXX: rhs *)
    124       change with (status_of_pseudo_status ?? (set_arg_16 pseudo_assembly_program 〈preamble, instr_list〉 ?? arg1) ??) in ⊢ (???%);
    125       >set_program_counter_mk_Status_commutation
    126       >set_clock_mk_Status_commutation
    127       >set_arg_16_mk_Status_commutation in ⊢ (???%);
    128       (* here we are *)
    129       @split_eq_status try %
    130       [1:
    131         assumption
    132       |2:
    133         @special_function_registers_8051_set_arg_16 %
    134       ]
     124      @set_arg_16_status_of_pseudo_status
     125      [3: @(subaddressing_mode_elim … arg1) %
     126      |2: %
     127      | @sym_eq @set_clock_status_of_pseudo_status
     128        [ @sym_eq @set_program_counter_status_of_pseudo_status [<EQnewpc % | %]
     129        | % ]]
    135130    |1: (* Instruction *)
    136       #instr #pi_refl #EQP #EQnext #fetch_many_assm
    137       @(main_lemma_preinstruction M M' preamble instr_list 〈preamble, instr_list〉 (refl …) ? sigma policy sigma_policy_witness
    138         ps ppc ? ? labels costs create_label_cost_refl newppc lookup_labels EQlookup_labels lookup_datalabels EQlookup_datalabels
    139         EQnewppc instr ? (ticks_of0 〈preamble, instr_list〉 sigma policy ppc (Instruction instr)) (refl …)
    140         (λ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)))
    141         (refl …) ? (refl …))
    142       [1,2:
    143         assumption
    144       |3:
    145         %
    146       |4:
    147         >fetch_pseudo_refl @pi_refl
    148       |5:
    149         <EQP %
    150       |6:
    151         >assembly_refl assumption
    152       |7:
    153         <EQassembled assumption
    154       ]
     131      #instr #pi_refl
     132      change with (execute_1_preinstruction ???????) in match (execute_1_pseudo_instruction0 ?????);
     133      >EQassembled whd in match address_of_word_labels; normalize nodelta
     134        >create_label_cost_refl in ⊢ (? → ? → ? → %);
     135       @(main_lemma_preinstruction M M' preamble instr_list 〈preamble, instr_list〉 (refl …) ? sigma policy sigma_policy_witness
     136        ps ppc ? ? labels cost create_label_cost_refl newppc lookup_labels EQlookup_labels lookup_datalabels EQlookup_datalabels
     137        EQnewppc instr ? ? (refl …) ? (refl …)
     138        (set_program_counter pseudo_assembly_program 〈preamble, instr_list〉 ps (add 16 ppc (bitvector_of_nat 16 1)))
     139        (refl …) ? (refl …))
     140        try % try assumption >fetch_pseudo_refl assumption
    155141    |4: (* Jmp *)
    156142      #arg1 #pi_refl
Note: See TracChangeset for help on using the changeset viewer.