Changeset 1667


Ignore:
Timestamp:
Jan 29, 2012, 10:25:57 PM (6 years ago)
Author:
sacerdot
Message:

Main lemma for the main_thm of AssemblyProof? re-declared as an axiom in
Assembly.ma. However, we need to understand again the role of lookup_labels.

Location:
src/ASM
Files:
2 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/Assembly.ma

    r1649 r1667  
    619619  let pc_len ≝ length ? flattened in
    620620   〈pc_len, flattened〉.
    621  
     621
    622622definition construct_costs ≝
    623623  λprogram_counter: nat.
     
    701701 cases abs /2/
    702702qed.
     703
     704(*CSC: Main axiom here, needs to be proved soon! *)
     705axiom snd_assembly_1_pseudoinstruction_ok:
     706 ∀program:pseudo_assembly_program.∀pol: policy program.
     707 ∀ppc:Word.∀pi,lookup_labels,lookup_datalabels.
     708  lookup_labels = (λx. sigma program pol (address_of_word_labels_code_mem (\snd program) x)) →
     709  lookup_datalabels = (λx. lookup_def … (construct_datalabels (\fst program)) x (zero ?)) →
     710  \fst (fetch_pseudo_instruction (\snd program) ppc) = pi →
     711   let len ≝ \fst (assembly_1_pseudoinstruction lookup_labels (pol lookup_labels) (sigma program pol ppc) lookup_datalabels  pi) in
     712    sigma program pol (\snd (half_add ? ppc (bitvector_of_nat ? 1))) =
     713     bitvector_of_nat … (nat_of_bitvector … (sigma program pol ppc) + len).
    703714
    704715example sigma_0: ∀p,pol. sigma p pol (bitvector_of_nat ? 0) = bitvector_of_nat ? 0.
  • src/ASM/AssemblyProof.ma

    r1666 r1667  
    20312031qed.
    20322032
     2033(*usare snd_assembly_1_pseudoinstruction_ok:
     2034 ∀program:pseudo_assembly_program.∀pol: policy program.
     2035 ∀ppc:Word.∀pi,lookup_labels,lookup_datalabels.
     2036  lookup_labels = (λx. sigma program pol (address_of_word_labels_code_mem (\snd program) x)) →
     2037  lookup_datalabels = (λx. lookup_def … (construct_datalabels (\fst program)) x (zero ?)) →
     2038  \fst (fetch_pseudo_instruction (\snd program) ppc) = pi →
     2039   let len ≝ \fst (assembly_1_pseudoinstruction lookup_labels (pol lookup_labels) (sigma program pol ppc) lookup_datalabels  pi) in
     2040    sigma program pol (\snd (half_add ? ppc (bitvector_of_nat ? 1))) =
     2041     bitvector_of_nat … (nat_of_bitvector … (sigma program pol ppc) + len).
     2042*)
     2043
     2044lemma pose: ∀A:Type[0].∀B:A → Type[0].∀a:A. (∀a':A. a'=a → B a') → B a.
     2045 /2/
     2046qed.
     2047
    20332048theorem main_thm:
    20342049 ∀M,M',cm,ps,pol,lookup_labels.
     
    20372052      execute n … (status_of_pseudo_status M … ps pol)
    20382053    = status_of_pseudo_status M' … (execute_1_pseudo_instruction (ticks_of cm pol lookup_labels) cm ps) pol.
    2039  #M #M' * #preamble #instr_list #ps
    2040  letin ppc ≝ (program_counter ?? ps)
    2041  #pol #lookup_labels
     2054 #M #M' * #preamble #instr_list #ps #pol #lookup_labels
    20422055 change with (next_internal_pseudo_address_map0 ????? = ? → ?)
    2043  change with (next_internal_pseudo_address_map0 ? (\fst (fetch_pseudo_instruction ? ppc)) ??? = ? → ?)
     2056 @(pose … (program_counter ?? ps)) #ppc #EQppc
    20442057 generalize in match (fetch_assembly_pseudo2 ? pol ppc) in ⊢ ?;
    2045  letin assembled ≝ (\fst (assembly ? pol))
    2046  letin lookup_labels ≝ (λx.(address_of_word_labels_code_mem instr_list x))
    2047  letin lookup_datalabels ≝ (λx. lookup_def … (construct_datalabels preamble) x (zero 16))
     2058 @(pose … (\fst (assembly ? pol))) #assembled #EQassembled
     2059 @(pose … (λx.(address_of_word_labels_code_mem instr_list x))) #lookup_labels #EQlookup_labels
     2060 @(pose … (λx. lookup_def … (construct_datalabels preamble) x (zero 16))) #lookup_datalabels #EQlookup_datalabels
    20482061 whd in match execute_1_pseudo_instruction; normalize nodelta
    2049  @pair_elim #pi #newppc change with (fetch_pseudo_instruction ? ppc = ? → ?) #EQ2
    2050  whd in match ticks_of;
    2051  normalize nodelta change with ppc in match ppc; change with assembled in match assembled;
    2052  change with lookup_labels in match lookup_labels; change with lookup_datalabels in match lookup_datalabels;
    2053  #H1 >EQ2
     2062 @pair_elim #pi #newppc #H1
     2063 whd in match ticks_of; normalize nodelta <EQppc #H2 >H1 normalize nodelta;
     2064 lapply (snd_fetch_pseudo_instruction instr_list ppc) >H1 #EQnewppc >EQnewppc
     2065 lapply (snd_assembly_1_pseudoinstruction_ok … EQlookup_labels EQlookup_datalabels)
    20542066 inversion pi
    20552067  [2,3: (* Comment, Cost *) #ARG #EQ >EQ in H1; #H1 whd in ⊢ (??%? → ?);
Note: See TracChangeset for help on using the changeset viewer.