Ignore:
Timestamp:
Jun 25, 2012, 2:39:06 PM (8 years ago)
Author:
mulligan
Message:

Various axioms closed and others moved around. Uncommented main lemma and found that it no longer compiles due to changing how we expand jumps. Problem in proof highlighted with XXX for Claudio.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/AssemblyProofSplit.ma

    r2047 r2108  
    405405include alias "ASM/Vector.ma".
    406406
    407 axiom main_lemma_preinstruction:
    408   ∀M, M': internal_pseudo_address_map.
    409   ∀preamble: preamble.
    410   ∀instr_list: list labelled_instruction.
    411   ∀cm: pseudo_assembly_program.
    412   ∀EQcm: cm = 〈preamble, instr_list〉.
    413   ∀sigma: Word → Word.
    414   ∀policy: Word → bool.
    415   ∀sigma_policy_witness: sigma_policy_specification cm sigma policy.
    416   ∀ps: PseudoStatus cm.
    417   ∀ppc: Word.
    418   ∀EQppc: ppc = program_counter pseudo_assembly_program cm ps.
    419   ∀labels: label_map.
    420   ∀costs: BitVectorTrie costlabel 16.
    421   ∀create_label_cost_refl: create_label_cost_map instr_list = 〈labels, costs〉.
    422   ∀newppc: Word.
    423   ∀lookup_labels: Identifier → Word.
    424   ∀EQlookup_labels: lookup_labels = (λx:Identifier. address_of_word_labels_code_mem instr_list x).
    425   ∀lookup_datalabels: Identifier → Word.
    426   ∀EQlookup_datalabels: lookup_datalabels = (λx.lookup_def ASMTag Word (construct_datalabels preamble) x (zero 16)).
    427   ∀EQnewppc: newppc = add 16 ppc (bitvector_of_nat 16 1).
    428   ∀instr: preinstruction Identifier.
    429   ∀ticks: nat × nat.
    430   ∀EQticks: ticks = ticks_of0 〈preamble, instr_list〉 sigma policy ppc (Instruction instr).
    431   ∀addr_of: Identifier → PreStatus pseudo_assembly_program cm → BitVector 16.
    432   ∀EQaddr_of: addr_of = (λx:Identifier. λy:PreStatus pseudo_assembly_program cm. address_of_word_labels cm x).
    433   ∀s: PreStatus pseudo_assembly_program cm.
    434   ∀EQs: s = (set_program_counter pseudo_assembly_program cm ps (add 16 ppc (bitvector_of_nat 16 1))).
    435   ∀P: preinstruction Identifier → PseudoStatus cm → Prop.
    436   ∀EQP: P = (λinstr, s. sigma (add 16 ppc (bitvector_of_nat 16 1)) = add 16 (sigma ppc)
    437               (bitvector_of_nat 16 (\fst (assembly_1_pseudoinstruction lookup_labels sigma policy ppc
    438                   lookup_datalabels (Instruction instr)))) →
    439               next_internal_pseudo_address_map0 pseudo_assembly_program (Instruction instr) M cm ps = Some internal_pseudo_address_map M' →
    440                 fetch_many (load_code_memory (\fst (pi1 … (assembly cm sigma policy)))) (sigma (add 16 ppc (bitvector_of_nat 16 1))) (sigma (program_counter pseudo_assembly_program cm ps))
    441                   (expand_pseudo_instruction lookup_labels sigma policy (program_counter pseudo_assembly_program cm ps) lookup_datalabels (Instruction instr)) →
    442                     ∃n: nat. execute n (code_memory_of_pseudo_assembly_program cm sigma policy) (status_of_pseudo_status M cm ps sigma policy) =
    443                       status_of_pseudo_status M' cm s sigma policy).
    444     P instr (execute_1_preinstruction ticks Identifier pseudo_assembly_program cm addr_of instr s).
    445 
    446 (*
     407axiom sub16_with_carry_overflow:
     408  ∀left, right, result: BitVector 16.
     409  ∀flags: BitVector 3.
     410  ∀upper: BitVector 9.
     411  ∀lower: BitVector 7.
     412    sub_16_with_carry left right false = 〈result, flags〉 →
     413      vsplit bool 9 7 result = 〈upper, lower〉 →
     414        get_index_v bool 3 flags 2 ? = true →
     415          upper = [[true; true; true; true; true; true; true; true; true]].
     416  //
     417qed.
     418
    447419lemma main_lemma_preinstruction:
    448420  ∀M, M': internal_pseudo_address_map.
     
    477449              (bitvector_of_nat 16 (\fst (assembly_1_pseudoinstruction lookup_labels sigma policy ppc
    478450                  lookup_datalabels (Instruction instr)))) →
    479               next_internal_pseudo_address_map0 pseudo_assembly_program (Instruction instr) M cm ps = Some internal_pseudo_address_map M' →
     451              next_internal_pseudo_address_map0 ? cm addr_of (Instruction instr) M ps = Some internal_pseudo_address_map M' →
    480452                fetch_many (load_code_memory (\fst (pi1 … (assembly cm sigma policy)))) (sigma (add 16 ppc (bitvector_of_nat 16 1))) (sigma (program_counter pseudo_assembly_program cm ps))
    481453                  (expand_pseudo_instruction lookup_labels sigma policy (program_counter pseudo_assembly_program cm ps) lookup_datalabels (Instruction instr)) →
     
    899871  [31,32: (* DJNZ *)
    900872  (* XXX: work on the right hand side *)
    901   >p normalize nodelta
     873  >p normalize nodelta >p1 normalize nodelta
    902874  (* XXX: switch to the left hand side *)
    903875  -instr_refl >EQP -P normalize nodelta
    904876  #sigma_increment_commutation #maps_assm #fetch_many_assm
    905877  whd in match (expand_pseudo_instruction ??????) in fetch_many_assm;
    906   whd in match (expand_relative_jump ????);
    907878  <EQppc in fetch_many_assm;
     879  whd in match (short_jump_cond ??);
     880  @pair_elim #sj_possible #disp
    908881  @pair_elim #result #flags #sub16_refl
    909882  @pair_elim #upper #lower #vsplit_refl
    910   cases (eq_bv ???) normalize nodelta
     883  inversion (get_index' bool ???) #get_index_refl' normalize nodelta
     884  #sj_possible_pair destruct(sj_possible_pair)
     885  >p1 normalize nodelta
    911886  [1,3:
    912887    >EQppc in ⊢ (% → ?); #fetch_many_assm %{1}
    913888    whd in ⊢ (??%?);
     889    >(sub16_with_carry_overflow … sub16_refl vsplit_refl get_index_refl') in fetch_many_assm;
     890    normalize nodelta in ⊢ (% → ?); #fetch_many_assm
    914891    <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm whd in ⊢ (??%?);
    915892    (* XXX: work on the left hand side *)
     
    927904    cases daemon
    928905  |2,4:
     906    XXX: here
    929907    >EQppc
    930908    * @(pose … (add 16 ??)) #intermediate_pc #EQintermediate_pc #fetch_refl
Note: See TracChangeset for help on using the changeset viewer.