Changeset 1668


Ignore:
Timestamp:
Jan 30, 2012, 11:41:08 AM (6 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)
Location:
src/ASM
Files:
2 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) ≝
  • src/ASM/AssemblyProof.ma

    r1667 r1668  
    13471347lemma fetch_assembly_pseudo:
    13481348  ∀program:pseudo_assembly_program.
    1349   let lookup_labels ≝ λx:Identifier.(address_of_word_labels_code_mem (\snd  program) x) in
    1350   ∀pol:(policy program).∀ppc.∀code_memory.
     1349  ∀pol:policy program.
     1350  let lookup_labels ≝ λx:Identifier.sigma … pol (address_of_word_labels_code_mem (\snd  program) x) in
     1351  ∀ppc.∀code_memory.
    13511352  let lookup_datalabels ≝ λx:Identifier.lookup_def … (construct_datalabels (\fst  program)) x (zero 16) in
    13521353  let pc ≝ sigma program pol ppc in
     
    13561357    encoding_check code_memory pc (bitvector_of_nat … (nat_of_bitvector ? pc + len)) assembled →
    13571358     fetch_many code_memory (bitvector_of_nat … (nat_of_bitvector ? pc + len)) pc instructions.
    1358  #program letin lookup_labels ≝ (λx.?) #pol #ppc #code_memory
     1359 #program #pol letin lookup_labels ≝ (λx.?) #ppc #code_memory
    13591360 letin lookup_datalabels ≝ (λx.?)
    13601361 letin pc ≝ (sigma ???) letin pi ≝ (fst ???) 
     
    13801381  let preamble ≝ \fst program in
    13811382  let datalabels ≝ construct_datalabels preamble in
    1382   let lookup_labels ≝ λx. address_of_word_labels_code_mem (\snd program) x in
     1383  let lookup_labels ≝ λx.sigma … pol (address_of_word_labels_code_mem (\snd program) x) in 
    13831384  let lookup_datalabels ≝ λx. lookup_def ?? datalabels x (zero ?) in
    13841385  ∀ppc.
     
    13951396  let code_memory ≝ load_code_memory assembled in
    13961397  let data_labels ≝ construct_datalabels (\fst program) in
    1397   let lookup_labels ≝ λx.address_of_word_labels_code_mem (\snd program) x in
     1398  let lookup_labels ≝ λx.sigma … pol (address_of_word_labels_code_mem (\snd program) x) in
    13981399  let lookup_datalabels ≝ λx. lookup_def ? ? data_labels x (zero ?) in
    13991400  let 〈pi,newppc〉 ≝ fetch_pseudo_instruction (\snd program) ppc in
     
    14041405 letin code_memory ≝ (load_code_memory assembled)
    14051406 letin data_labels ≝ (construct_datalabels preamble)
    1406  letin lookup_labels ≝ (λx. address_of_word_labels_code_mem instr_list x)
     1407 letin lookup_labels ≝ (λx. sigma … pol (address_of_word_labels_code_mem instr_list x))
    14071408 letin lookup_datalabels ≝ (λx. lookup_def ? ? data_labels x (zero ?))
    14081409 @pair_elim #pi #newppc #EQ1 change with (fetch_pseudo_instruction instr_list ? = ?) in EQ1;
     
    20462047qed.
    20472048
     2049(* To be moved in ProofStatus *)
     2050lemma program_counter_set_program_counter:
     2051 ∀T,cm,s,x. program_counter T cm (set_program_counter T cm s x) = x.
     2052 //
     2053qed.
     2054
    20482055theorem main_thm:
    20492056 ∀M,M',cm,ps,pol,lookup_labels.
     
    20572064 generalize in match (fetch_assembly_pseudo2 ? pol ppc) in ⊢ ?;
    20582065 @(pose … (\fst (assembly ? pol))) #assembled #EQassembled
    2059  @(pose … (λx.(address_of_word_labels_code_mem instr_list x))) #lookup_labels #EQlookup_labels
     2066 @(pose … (λx.sigma … pol (address_of_word_labels_code_mem instr_list x))) #lookup_labels #EQlookup_labels
    20602067 @(pose … (λx. lookup_def … (construct_datalabels preamble) x (zero 16))) #lookup_datalabels #EQlookup_datalabels
    20612068 whd in match execute_1_pseudo_instruction; normalize nodelta
     
    20632070 whd in match ticks_of; normalize nodelta <EQppc #H2 >H1 normalize nodelta;
    20642071 lapply (snd_fetch_pseudo_instruction instr_list ppc) >H1 #EQnewppc >EQnewppc
    2065  lapply (snd_assembly_1_pseudoinstruction_ok … EQlookup_labels EQlookup_datalabels)
     2072 lapply (snd_assembly_1_pseudoinstruction_ok … ppc pi … EQlookup_labels EQlookup_datalabels ?)
     2073 [>H1 %]
    20662074 inversion pi
    2067   [2,3: (* Comment, Cost *) #ARG #EQ >EQ in H1; #H1 whd in ⊢ (??%? → ?);
    2068    @Some_Some_elim #MAP <MAP NEEDS assembly_1_pseudoinstruction_ok now commented out
    2069    in Assembly.ma
    2070    %{0} @split_eq_status try %
    2071    lapply (snd_fetch_pseudo_instruction instr_list ppc) >EQ2 #EQ3 >EQ3
    2072    
    2073    >(eq_bv_eq … H2) >EQ %
     2075  [2,3: (* Comment, Cost *) #ARG #EQ
     2076   #H3 normalize nodelta in H3; normalize in match (assembly_1_pseudoinstruction ?????) in H3;
     2077   whd in ⊢ (??%? → ?); @Some_Some_elim #MAP <MAP
     2078   whd in match (execute_1_pseudo_instruction0 ?????);
     2079   %{0} @split_eq_status //
    20742080  |4: (* Jmp *) #label whd in ⊢ (??%? → ???% → ?)
    20752081   @Some_Some_elim #MAP cases (pol ?) normalize nodelta
Note: See TracChangeset for help on using the changeset viewer.