 Timestamp:
 Jan 29, 2012, 10:25:57 PM (8 years ago)
 Location:
 src/ASM
 Files:

 2 edited
Legend:
 Unmodified
 Added
 Removed

src/ASM/Assembly.ma
r1649 r1667 619 619 let pc_len ≝ length ? flattened in 620 620 〈pc_len, flattened〉. 621 621 622 622 definition construct_costs ≝ 623 623 λprogram_counter: nat. … … 701 701 cases abs /2/ 702 702 qed. 703 704 (*CSC: Main axiom here, needs to be proved soon! *) 705 axiom 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). 703 714 704 715 example sigma_0: ∀p,pol. sigma p pol (bitvector_of_nat ? 0) = bitvector_of_nat ? 0. 
src/ASM/AssemblyProof.ma
r1666 r1667 2031 2031 qed. 2032 2032 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 2044 lemma pose: ∀A:Type[0].∀B:A → Type[0].∀a:A. (∀a':A. a'=a → B a') → B a. 2045 /2/ 2046 qed. 2047 2033 2048 theorem main_thm: 2034 2049 ∀M,M',cm,ps,pol,lookup_labels. … … 2037 2052 execute n … (status_of_pseudo_status M … ps pol) 2038 2053 = 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 2042 2055 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 2044 2057 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 2048 2061 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) 2054 2066 inversion pi 2055 2067 [2,3: (* Comment, Cost *) #ARG #EQ >EQ in H1; #H1 whd in ⊢ (??%? → ?);
Note: See TracChangeset
for help on using the changeset viewer.