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/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.