Changeset 2024


Ignore:
Timestamp:
Jun 7, 2012, 3:20:53 PM (5 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.

Location:
src/ASM
Files:
2 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/AssemblyProof.ma

    r2021 r2024  
    15171517  ∀sigma: Word → Word.
    15181518  ∀policy: Word → bool.
    1519   let lookup_labels ≝ λx:Identifier. sigma (address_of_word_labels_code_mem (\snd  program) x) in
     1519  let lookup_labels ≝ λx:Identifier. address_of_word_labels_code_mem (\snd  program) x in
    15201520  ∀ppc.
    15211521  ∀code_memory.
    1522   let lookup_datalabels ≝ λx:Identifier.lookup_def … (construct_datalabels (\fst  program)) x (zero 16) in
     1522  let lookup_datalabels ≝ λx:Identifier. lookup_def … (construct_datalabels (\fst  program)) x (zero 16) in
    15231523  let pi ≝  \fst  (fetch_pseudo_instruction (\snd program) ppc) in
    15241524  let pc ≝ sigma ppc in
     
    16101610      (* costs = costs' ∧ CSC: costs != costs', costs' = sigma costs! *)
    16111611        let code_memory ≝ load_code_memory assembled in
    1612         let lookup_labels ≝ λx. sigma (address_of_word_labels_code_mem instr_list x) in 
     1612        let lookup_labels ≝ λx. address_of_word_labels_code_mem instr_list x in 
    16131613          ∀ppc.
    16141614            let 〈pi, newppc〉 ≝ fetch_pseudo_instruction (\snd program) ppc in     
     
    16721672  let code_memory ≝ load_code_memory assembled in
    16731673  let data_labels ≝ construct_datalabels (\fst program) in
    1674   let lookup_labels ≝ λx. sigma (address_of_word_labels_code_mem (\snd program) x) in 
     1674  let lookup_labels ≝ λx. address_of_word_labels_code_mem (\snd program) x in 
    16751675  let lookup_datalabels ≝ λx. lookup_def ? ? data_labels x (zero ?) in
    16761676  let 〈pi,newppc〉 ≝ fetch_pseudo_instruction (\snd program) ppc in
     
    23472347   
    23482348(*CSC: ???*)
     2349(* XXX: we need a precondition here stating that the PPC is within the
     2350        bounds of the instruction list in order for Jaap's specification to
     2351        apply.
     2352*)
    23492353lemma snd_assembly_1_pseudoinstruction_ok:
    23502354  ∀program: pseudo_assembly_program.
     
    23532357  ∀sigma_policy_specification_witness: sigma_policy_specification program sigma policy.
    23542358  ∀ppc: Word.
     2359  ∀ppc_in_bounds: nat_of_bitvector 16 ppc ≤ |\snd program|.
    23552360  ∀pi.
    23562361  ∀lookup_labels.
    23572362  ∀lookup_datalabels.
    2358     lookup_labels = (λx. sigma (address_of_word_labels_code_mem (\snd program) x)) →
     2363    lookup_labels = (λx. (address_of_word_labels_code_mem (\snd program) x)) →
    23592364    lookup_datalabels = (λx. lookup_def … (construct_datalabels (\fst program)) x (zero ?)) →
    23602365    \fst (fetch_pseudo_instruction (\snd program) ppc) = pi →
    2361     let len ≝ \fst (assembly_1_pseudoinstruction lookup_labels sigma policy (*(sigma ppc)*) ppc lookup_datalabels  pi) in
     2366    let len ≝ \fst (assembly_1_pseudoinstruction lookup_labels sigma policy (*(sigma ppc)*) ppc lookup_datalabels pi) in
    23622367      sigma (add … ppc (bitvector_of_nat ? 1)) = add … (sigma ppc) (bitvector_of_nat ? len).
    2363   #program #sigma #policy #sigma_policy_specification_witness #ppc #pi
     2368  #program #sigma #policy #sigma_policy_specification_witness #ppc #ppc_in_bounds #pi
    23642369  #lookup_labels #lookup_datalabels
    23652370  #lookup_labels_refl #lookup_datalabels_refl #fetch_pseudo_refl
     
    23852390  <sigma_newppc_refl
    23862391  generalize in match fetch_pseudo_refl';
     2392  (* XXX: use ppc_in_bounds to get rid of the cases not_implemented in
     2393          fetch_pseudo_instruction, as this is exactly what we need now!
     2394  *)
    23872395  whd in match (fetch_pseudo_instruction ??);
    23882396  @pair_elim #lbl #instr #nth_refl normalize nodelta
    2389   #G cases (pair_destruct_right ?????? G) %
     2397  #G cases (pair_destruct_right ?????? G)
     2398  lapply (sigma_policy_specification_witness ppc)
     2399  >program_refl normalize nodelta #policy_hyp
     2400  cases policy_hyp -policy_hyp #policy_hyp1 #_
     2401  >policy_hyp1
     2402  [1:
     2403    -policy_hyp1 whd in match instruction_size; normalize nodelta
     2404    <pi_refl' >(?: pi' = \fst (fetch_pseudo_instruction (\snd program) ppc))
     2405    [1: >program_refl % ] >fetch_pseudo_refl' %
     2406  |2:
     2407    >program_refl in ppc_in_bounds; #relevant assumption
     2408  ]
    23902409qed.
    23912410
  • 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.