Ignore:
Timestamp:
Jun 7, 2012, 3:20:53 PM (8 years ago)
Author:
mulligan
Message:

Updated AssemblyProof? to fix mismatch in definition of lookup_labels between that file and AssemblyProofSplit?. Noticed the precondition we need on fetch_assembly_pseudo2 (that ppc <= |instr_list|) is precisely what we need to remove the cases not_implemented in fetch_assembly_pseudo. Small amount of work, getting everything typechecking, on main theorem in AssemblyProofSplit?.ma.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/AssemblyProofSplit.ma

    r2023 r2024  
    13941394
    13951395theorem main_thm:
    1396   ∀M.
    1397   ∀M'.
     1396  ∀M, M': internal_pseudo_address_map.
    13981397  ∀program: pseudo_assembly_program.
    13991398  ∀sigma: Word → Word.
     
    14081407  change with (next_internal_pseudo_address_map0 ????? = ? → ?)
    14091408  @(pose … (program_counter ?? ps)) #ppc #EQppc
     1409  check fetch_assembly_pseudo2
    14101410  generalize in match (fetch_assembly_pseudo2 〈preamble,instr_list〉 sigma policy sigma_policy_witness ppc) in ⊢ ?;
    14111411  @pair_elim #labels #costs #create_label_cost_refl normalize nodelta
     
    14591459    >EQassembled in fetch_many_assm;
    14601460    cases (fetch ??) * #instr #newpc #ticks normalize nodelta *
    1461     #eq_instr #EQticks whd in EQticks:(???%); >EQticks
     1461    #eq_instr
    14621462    #fetch_many_assm whd in fetch_many_assm;
    14631463    lapply (eq_bv_eq … fetch_many_assm) -fetch_many_assm #EQnewpc
    1464     >(eq_instruction_to_eq … eq_instr) -instr whd in ⊢ (??%?);
     1464    destruct whd in ⊢ (??%?);
    14651465    (* XXX: now we start to work on the mk_PreStatus equality *)
    14661466    (* XXX: lhs *)
     
    14701470    >set_arg_16_mk_Status_commutation
    14711471    (* XXX: rhs *)
    1472     change with (? = status_of_pseudo_status ?? (set_arg_16 ?????) ??)
     1472    change with (status_of_pseudo_status ?? (set_arg_16 pseudo_assembly_program 〈preamble, instr_list〉 ?? arg1) ??) in ⊢ (???%);
    14731473    >set_program_counter_mk_Status_commutation
    14741474    >set_clock_mk_Status_commutation
     
    14801480    |2:
    14811481      @special_function_registers_8051_set_arg_16
    1482       [2: >EQlookup_datalabels %
     1482      [2: %
    14831483      |1: //
    14841484      ]
    14851485    ]
    14861486  |1: (* Instruction *) -pi; #instr
    1487     @(main_lemma_preinstruction M M' preamble instr_list … (refl …) … sigma_policy_witness
     1487    @(main_lemma_preinstruction M M' preamble instr_list 〈preamble, instr_list〉 (refl …) sigma policy
     1488        sigma_policy_witness ps ppc EQppc labels costs create_label_cost_refl ? lookup_datalabels)
     1489    check (main_lemma_preinstruction M M' preamble instr_list … (refl …) … sigma_policy_witness
    14881490      … EQppc … create_label_cost_refl … assembly_refl EQassembled … EQlookup_labels …
    14891491      EQlookup_datalabels EQnewppc instr … (refl …) … (refl …) … (refl …) … (refl …))
Note: See TracChangeset for help on using the changeset viewer.