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/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
Note: See TracChangeset for help on using the changeset viewer.