Changeset 908


Ignore:
Timestamp:
Jun 9, 2011, 1:22:15 AM (8 years ago)
Author:
sacerdot
Message:

Next big lemma proved!

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/AssemblyProof.ma

    r906 r908  
    13641364       sigma program newppc = bitvector_of_nat … (nat_of_bitvector … (sigma program ppc) + len).
    13651365
     1366axiom bitvector_of_nat_nat_of_bitvector:
     1367 ∀n,v. bitvector_of_nat n (nat_of_bitvector n v) = v.
     1368
     1369lemma fetch_assembly_pseudo2:
     1370 ∀program,assembled,costs,labels,datalabels.
     1371  Some … 〈labels,datalabels〉 = build_maps program →
     1372  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
     1376   ∀ppc,instructions.
     1377    let expansion ≝ jump_expansion_policy program ppc in
     1378    let 〈pi,newppc〉 ≝ fetch_pseudo_instruction (\snd program) ppc in
     1379     Some ? instructions = expand_pseudo_instruction lookup_labels lookup_datalabels ppc expansion pi →
     1380      fetch_many code_memory (sigma program newppc) (sigma program ppc) instructions.
     1381 #program #assembled #costs #labels #datalabels #BUILD_MAPS #ASSEMBLY #ppc #instructions whd
     1382 generalize in match (assembly_ok … BUILD_MAPS ASSEMBLY ppc)
     1383 cases (fetch_pseudo_instruction (\snd program) ppc) #pi #newppc
     1384 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))
     1387 whd in ⊢ ((∀_.∀_.∀_.∀_.%) → (∀_.∀_.%) → ?)
     1388 #H1 #H2 whd #EXPAND whd in H1:(∀_.∀_.∀_.∀_.? → ???% → ?) H2:(∀_.∀_.???% → ?);
     1389 <EXPAND in H1 H2; whd in ⊢ ((∀_.∀_.∀_.∀_.? → ???% → ?) → (∀_.∀_.???% → ?) → ?)
     1390 #H1 #H2
     1391 cases (H2 ?? (refl …)) -H2; #K1 #K2 >K2
     1392 generalize in match (H1 ??? (nat_of_bitvector … (sigma program ppc)) (refl …) (refl …) ?) -H1;
     1393  [ #K3 >bitvector_of_nat_nat_of_bitvector in K3; #R @R
     1394  | >bitvector_of_nat_nat_of_bitvector @K1 ]
     1395qed.
     1396
    13661397(* OLD?
    13671398definition assembly_specification:
Note: See TracChangeset for help on using the changeset viewer.