Changeset 1668 for src/ASM/Assembly.ma


Ignore:
Timestamp:
Jan 30, 2012, 11:41:08 AM (8 years ago)
Author:
boender
Message:
  • split build_maps into build_maps and build_maps_ok
  • work with CSC on partial proof of main_thm (cases Comment and Cost)
File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/Assembly.ma

    r1667 r1668  
    970970    eq_identifier tag l r = false → (l = r → False).
    971971
    972 definition build_maps:
     972definition build_maps0:
    973973 ∀pseudo_program.∀pol:policy pseudo_program.
    974974  Σres:((identifier_map ASMTag Word) × (BitVectorTrie costlabel 16)).
     
    10341034qed.
    10351035
     1036definition build_maps:
     1037 ∀pseudo_program. policy pseudo_program →
     1038  (identifier_map ASMTag Word) × (BitVectorTrie costlabel 16)
     1039 ≝ λpseudo_program,pol. build_maps0 pseudo_program pol.
     1040
     1041theorem build_maps_ok:
     1042 ∀pseudo_program.∀pol:policy pseudo_program.
     1043   let 〈labels, costs〉 ≝ build_maps pseudo_program pol in
     1044    ∀id. occurs_exactly_once id (\snd pseudo_program) →
     1045     lookup_def … labels id (zero ?) = sigma pseudo_program pol (address_of_word_labels_code_mem (\snd pseudo_program) id).
     1046 #pseudo_program #pol @(pi2 … (build_maps0 … pol))
     1047qed.
     1048
    10361049definition assembly:
    10371050 ∀p:pseudo_assembly_program. policy p → list Byte × (BitVectorTrie costlabel 16) ≝
Note: See TracChangeset for help on using the changeset viewer.