Changeset 915


Ignore:
Timestamp:
Jun 9, 2011, 11:30:59 AM (8 years ago)
Author:
mulligan
Message:

finished changes to fetch_assembly_pseudo2

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/AssemblyProof.ma

    r912 r915  
    13511351
    13521352axiom assembly_ok:
    1353  ∀program,assembled,costs,labels,datalabels.
    1354   Some … 〈labels,datalabels〉 = build_maps program →
     1353 ∀program,assembled,costs,labels.
     1354  Some … 〈labels,costs〉 = build_maps program →
    13551355  Some … 〈assembled,costs〉 = assembly program →
    13561356  let code_memory ≝ load_code_memory assembled in
    1357   let lookup_labels ≝ λx. lookup ?? x labels (zero ?) in
     1357  let preamble ≝ \fst program in
     1358  let datalabels ≝ construct_datalabels preamble in
     1359  let lookup_labels ≝ λx. sigma program (address_of_word_labels_code_mem (\snd program) x) in
    13581360  let lookup_datalabels ≝ λx. lookup ?? x datalabels (zero ?) in
    13591361   ∀ppc,len,assembledi.
     
    13651367
    13661368axiom bitvector_of_nat_nat_of_bitvector:
    1367  ∀n,v. bitvector_of_nat n (nat_of_bitvector n v) = v.
     1369  ∀n,v.
     1370    bitvector_of_nat n (nat_of_bitvector n v) = v.
    13681371
    13691372lemma fetch_assembly_pseudo2:
    1370  ∀program,assembled,costs,labels,datalabels.
    1371   Some … 〈labels,datalabels〉 = build_maps program →
     1373 ∀program,assembled,costs,labels.
     1374  Some … 〈labels,costs〉 = build_maps program →
    13721375  Some … 〈assembled,costs〉 = assembly program →
    1373   let code_memory ≝ load_code_memory assembled in
    1374   let lookup_labels ≝ λx. lookup ?? x labels (zero ?) in
    1375   let lookup_datalabels ≝ λx. lookup ?? x datalabels (zero ?) in
    13761376   ∀ppc,instructions.
     1377    let code_memory ≝ load_code_memory assembled in
     1378    let preamble ≝ \fst program in
     1379    let data_labels ≝ construct_datalabels preamble in
     1380    let lookup_labels ≝ λx. sigma program (address_of_word_labels_code_mem (\snd program) x) in
     1381    let lookup_datalabels ≝ λx. lookup ? ? x data_labels (zero ?) in
    13771382    let expansion ≝ jump_expansion_policy program ppc in
    13781383    let 〈pi,newppc〉 ≝ fetch_pseudo_instruction (\snd program) ppc in
    13791384     Some ? instructions = expand_pseudo_instruction lookup_labels lookup_datalabels ppc expansion pi →
    13801385      fetch_many code_memory (sigma program newppc) (sigma program ppc) instructions.
    1381  #program #assembled #costs #labels #datalabels #BUILD_MAPS #ASSEMBLY #ppc #instructions whd
     1386 #program #assembled #costs #labels #BUILD_MAPS #ASSEMBLY #ppc #instructions
     1387 letin code_memory ≝ (load_code_memory assembled)
     1388 letin preamble ≝ (\fst program)
     1389 letin data_labels ≝ (construct_datalabels preamble)
     1390 letin lookup_labels ≝ (λx. sigma program (address_of_word_labels_code_mem (\snd program) x))
     1391 letin lookup_datalabels ≝ (λx. lookup ? ? x data_labels (zero ?))
     1392 whd
    13821393 generalize in match (assembly_ok … BUILD_MAPS ASSEMBLY ppc)
    13831394 cases (fetch_pseudo_instruction (\snd program) ppc) #pi #newppc
    13841395 generalize in match (fetch_assembly_pseudo program ppc
    1385   (λx. lookup ?? x labels (zero ?)) (λx. lookup ?? x datalabels (zero ?)) pi
    1386   (load_code_memory assembled)) 
     1396  (λx. sigma program (address_of_word_labels_code_mem (\snd program) x)) (λx. lookup ?? x data_labels (zero ?)) pi
     1397  (load_code_memory assembled));
    13871398 whd in ⊢ ((∀_.∀_.∀_.∀_.%) → (∀_.∀_.%) → ?)
    13881399 #H1 #H2 whd #EXPAND whd in H1:(∀_.∀_.∀_.∀_.? → ???% → ?) H2:(∀_.∀_.???% → ?);
Note: See TracChangeset for help on using the changeset viewer.