Changeset 924


Ignore:
Timestamp:
Jun 9, 2011, 4:14:54 PM (8 years ago)
Author:
sacerdot
Message:

...

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/AssemblyProof.ma

    r923 r924  
    13691369    bitvector_of_nat n (nat_of_bitvector n v) = v.
    13701370
     1371axiom assembly_ok_to_expand_pseudo_instruction_ok:
     1372 ∀program,assembled,costs.
     1373  Some … 〈assembled,costs〉 = assembly program →
     1374   ∀ppc.
     1375    let code_memory ≝ load_code_memory assembled in
     1376    let preamble ≝ \fst program in   
     1377    let data_labels ≝ construct_datalabels preamble in
     1378    let lookup_labels ≝ λx. sigma program (address_of_word_labels_code_mem (\snd program) x) in
     1379    let lookup_datalabels ≝ λx. lookup ? ? x data_labels (zero ?) in
     1380    let expansion ≝ jump_expansion ppc program in
     1381    let 〈pi,newppc〉 ≝ fetch_pseudo_instruction (\snd program) ppc in
     1382     ∃instructions.
     1383      Some ? instructions = expand_pseudo_instruction lookup_labels lookup_datalabels (sigma program ppc) expansion pi.
     1384
    13711385lemma fetch_assembly_pseudo2:
    13721386 ∀program,assembled,costs,labels.
    13731387  Some … 〈labels,costs〉 = build_maps program →
    13741388  Some … 〈assembled,costs〉 = assembly program →
    1375    ∀ppc,instructions.
     1389   ∀ppc.
    13761390    let code_memory ≝ load_code_memory assembled in
    13771391    let preamble ≝ \fst program in
     
    13811395    let expansion ≝ jump_expansion ppc program in
    13821396    let 〈pi,newppc〉 ≝ fetch_pseudo_instruction (\snd program) ppc in
    1383      Some ? instructions = expand_pseudo_instruction lookup_labels lookup_datalabels (sigma program ppc) expansion pi →
    1384       fetch_many code_memory (sigma program newppc) (sigma program ppc) instructions.
    1385  #program #assembled #costs #labels #BUILD_MAPS #ASSEMBLY #ppc #instructions
     1397     ∃instructions.
     1398      Some ? instructions = expand_pseudo_instruction lookup_labels lookup_datalabels (sigma program ppc) expansion pi ∧
     1399       fetch_many code_memory (sigma program newppc) (sigma program ppc) instructions.
     1400 #program #assembled #costs #labels #BUILD_MAPS #ASSEMBLY #ppc
     1401 generalize in match (assembly_ok_to_expand_pseudo_instruction_ok program assembled costs ASSEMBLY ppc)
    13861402 letin code_memory ≝ (load_code_memory assembled)
    13871403 letin preamble ≝ (\fst program)
     
    13891405 letin lookup_labels ≝ (λx. sigma program (address_of_word_labels_code_mem (\snd program) x))
    13901406 letin lookup_datalabels ≝ (λx. lookup ? ? x data_labels (zero ?))
    1391  whd
     1407 whd in ⊢ (% → %)
    13921408 generalize in match (assembly_ok … BUILD_MAPS ASSEMBLY ppc)
    13931409 cases (fetch_pseudo_instruction (\snd program) ppc) #pi #newppc
     
    13951411  (λx. sigma program (address_of_word_labels_code_mem (\snd program) x)) (λx. lookup ?? x data_labels (zero ?)) pi
    13961412  (load_code_memory assembled));
    1397  whd in ⊢ ((∀_.∀_.∀_.∀_.%) → (∀_.∀_.%) → ?)
    1398  #H1 #H2 whd #EXPAND whd in H1:(∀_.∀_.∀_.∀_.? → ???% → ?) H2:(∀_.∀_.???% → ?);
     1413 whd in ⊢ ((∀_.∀_.∀_.∀_.%) → (∀_.∀_.%) → % → %) #H1 #H2 * #instructions #EXPAND
     1414 whd in H1:(∀_.∀_.∀_.∀_.? → ???% → ?) H2:(∀_.∀_.???% → ?);
    13991415 normalize nodelta in EXPAND; (* HERE *)
    14001416 generalize in match (λlen, assembled.H1 len assembled instructions (nat_of_bitvector … (sigma program ppc))) -H1; #H1
     
    14041420 cases (H2 ?? (refl …)) -H2; #K1 #K2 >K2
    14051421 generalize in match (H1 ?? (refl …) (refl …) ?) -H1;
    1406   [ #K3 @K3 | @K1 ]
     1422  [ #K3 % [2: % [% | @K3]] | @K1 ]
    14071423qed.
    14081424
     
    16151631 whd in match (\snd 〈final_pc,assembled〉) in H;
    16161632 -s s'' labels costs final_ppc final_pc;
     1633 (* NICE STATEMENT HERE *)
Note: See TracChangeset for help on using the changeset viewer.