Changeset 1945 for src/ASM/AssemblyProof.ma
 Timestamp:
 May 14, 2012, 10:40:38 PM (8 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/ASM/AssemblyProof.ma
r1941 r1945 1610 1610 1611 1611 axiom low_internal_ram_of_pseudo_internal_ram_hit: 1612 ∀M:internal_pseudo_address_map.∀cm.∀s:PseudoStatus cm.∀ pol:policy cm.∀addr:BitVector 7.1612 ∀M:internal_pseudo_address_map.∀cm.∀s:PseudoStatus cm.∀sigma:Word → Word × bool.∀addr:BitVector 7. 1613 1613 member ? (eq_bv 8) (false:::addr) M = true → 1614 1614 let ram ≝ low_internal_ram_of_pseudo_low_internal_ram M (low_internal_ram … s) in … … 1617 1617 let bl ≝ lookup ? 7 addr ram (zero 8) in 1618 1618 let bu ≝ lookup ? 7 (\snd (half_add ? addr (bitvector_of_nat 7 1))) ram (zero 8) in 1619 bu@@bl = sigma cm pol (pbu@@pbl).1619 bu@@bl = \fst (sigma (pbu@@pbl)). 1620 1620 1621 1621 (* changed from add to sub *) … … 1702 1702 1703 1703 definition code_memory_of_pseudo_assembly_program: 1704 ∀pap:pseudo_assembly_program. policy pap→ BitVectorTrie Byte 161705 ≝ λpap, pol.1706 let p ≝ assembly pap polin1704 ∀pap:pseudo_assembly_program. (Word → Word × bool) → BitVectorTrie Byte 16 1705 ≝ λpap,sigma. 1706 let p ≝ assembly pap sigma in 1707 1707 load_code_memory (\fst p). 1708 1708 1709 1709 definition status_of_pseudo_status: 1710 internal_pseudo_address_map → ∀pap.∀ps:PseudoStatus pap. ∀ pol:policy pap.1711 Status (code_memory_of_pseudo_assembly_program … pol) ≝1712 λM,pap,ps, pol.1713 let cm ≝ code_memory_of_pseudo_assembly_program … polin1714 let pc ≝ sigma pap pol (program_counter … ps) in1710 internal_pseudo_address_map → ∀pap.∀ps:PseudoStatus pap. ∀sigma: Word → Word × bool. 1711 Status (code_memory_of_pseudo_assembly_program pap sigma) ≝ 1712 λM,pap,ps,sigma. 1713 let cm ≝ code_memory_of_pseudo_assembly_program … sigma in 1714 let pc ≝ \fst (sigma (program_counter … ps)) in 1715 1715 let lir ≝ low_internal_ram_of_pseudo_low_internal_ram M (low_internal_ram … ps) in 1716 1716 let hir ≝ high_internal_ram_of_pseudo_high_internal_ram M (high_internal_ram … ps) in … … 1840 1840 *) 1841 1841 1842 definition ticks_of0: ∀p:pseudo_assembly_program. policy p → (Identifier→Word) → Word → ?→ nat × nat ≝1843 λprogram: pseudo_assembly_program.λ pol.λlookup_labels.1842 definition ticks_of0: ∀p:pseudo_assembly_program. (Word → Word × bool) → Word → pseudo_instruction → nat × nat ≝ 1843 λprogram: pseudo_assembly_program.λsigma. 1844 1844 λppc: Word. 1845 λfetched. 1845 λfetched. ?. 1846 cases daemon(* 1846 1847 match fetched with 1847 1848 [ Instruction instr ⇒ … … 1993 1994 ]. 1994 1995 cases not_implemented (* policy returned medium_jump for conditional jumping = impossible *) 1995 qed.1996 1997 definition ticks_of: ∀p:pseudo_assembly_program. policy p → (Identifier→Word) → Word → nat × nat ≝1998 λprogram: pseudo_assembly_program.λ pol.λlookup_labels.1996 *)qed. 1997 1998 definition ticks_of: ∀p:pseudo_assembly_program. (Word → Word × bool) → Word → nat × nat ≝ 1999 λprogram: pseudo_assembly_program.λsigma. 1999 2000 λppc: Word. 2000 2001 let 〈preamble, pseudo〉 ≝ program in 2001 2002 let 〈fetched, new_ppc〉 ≝ fetch_pseudo_instruction pseudo ppc in 2002 ticks_of0 program pol lookup_labelsppc fetched.2003 ticks_of0 program sigma ppc fetched. 2003 2004 2004 2005 lemma eq_rect_Type1_r: … … 2110 2111 2111 2112 axiom low_internal_ram_write_at_stack_pointer: 2112 ∀T1,T2,M,cm1,s1,cm2,s2,cm3,s3.∀ pol.∀pbu,pbl,bu,bl,sp1,sp2:BitVector 8.2113 get_8051_sfr ?cm2 s2 SFR_SP = get_8051_sfr ? cm3 s3 SFR_SP →2113 ∀T1,T2,M,cm1,s1,cm2,s2,cm3,s3.∀sigma: Word → Word × bool.∀pbu,pbl,bu,bl,sp1,sp2:BitVector 8. 2114 get_8051_sfr T2 cm2 s2 SFR_SP = get_8051_sfr ? cm3 s3 SFR_SP → 2114 2115 low_internal_ram ? cm2 s2 = low_internal_ram T2 cm3 s3 → 2115 2116 sp1 = \snd (half_add ? (get_8051_sfr … cm1 s1 SFR_SP) (bitvector_of_nat 8 1)) → 2116 2117 sp2 = \snd (half_add ? sp1 (bitvector_of_nat 8 1)) → 2117 bu@@bl = sigma cm2 pol (pbu@@pbl) →2118 bu@@bl = \fst (sigma (pbu@@pbl)) → 2118 2119 low_internal_ram T1 cm1 2119 2120 (write_at_stack_pointer … … … 2136 2137 2137 2138 axiom high_internal_ram_write_at_stack_pointer: 2138 ∀T1,T2,M,cm1,s1,cm2,s2,cm3,s3 ,pol.∀pbu,pbl,bu,bl,sp1,sp2:BitVector 8.2139 get_8051_sfr ?cm2 s2 SFR_SP = get_8051_sfr ? cm3 s3 SFR_SP →2139 ∀T1,T2,M,cm1,s1,cm2,s2,cm3,s3.∀sigma:Word → Word × bool.∀pbu,pbl,bu,bl,sp1,sp2:BitVector 8. 2140 get_8051_sfr T2 cm2 s2 SFR_SP = get_8051_sfr ? cm3 s3 SFR_SP → 2140 2141 high_internal_ram ?? s2 = high_internal_ram T2 cm3 s3 → 2141 2142 sp1 = \snd (half_add ? (get_8051_sfr ? cm1 s1 SFR_SP) (bitvector_of_nat 8 1)) → 2142 2143 sp2 = \snd (half_add ? sp1 (bitvector_of_nat 8 1)) → 2143 bu@@bl = sigma cm2 pol (pbu@@pbl) →2144 bu@@bl = \fst (sigma (pbu@@pbl)) → 2144 2145 high_internal_ram T1 cm1 2145 2146 (write_at_stack_pointer … … … 2166 2167 qed. 2167 2168 2168 (*usare snd_assembly_1_pseudoinstruction_ok: 2169 ∀program:pseudo_assembly_program.∀pol: policy program. 2169 (*CSC: ???*) 2170 axiom snd_assembly_1_pseudoinstruction_ok: 2171 ∀program:pseudo_assembly_program.∀sigma. 2170 2172 ∀ppc:Word.∀pi,lookup_labels,lookup_datalabels. 2171 lookup_labels = (λx. sigma program pol (address_of_word_labels_code_mem (\snd program) x)) →2173 lookup_labels = (λx. \fst (sigma (address_of_word_labels_code_mem (\snd program) x))) → 2172 2174 lookup_datalabels = (λx. lookup_def … (construct_datalabels (\fst program)) x (zero ?)) → 2173 2175 \fst (fetch_pseudo_instruction (\snd program) ppc) = pi → 2174 let len ≝ \fst (assembly_1_pseudoinstruction lookup_labels (pol lookup_labels) (sigma program pol ppc) lookup_datalabels pi) in 2175 sigma program pol (\snd (half_add ? ppc (bitvector_of_nat ? 1))) = 2176 bitvector_of_nat … (nat_of_bitvector … (sigma program pol ppc) + len). 2177 *) 2176 let len ≝ \fst (assembly_1_pseudoinstruction lookup_labels sigma (\fst (sigma ppc)) lookup_datalabels pi) in 2177 \fst (sigma (add … ppc (bitvector_of_nat ? 1))) = 2178 add … (\fst (sigma ppc)) (bitvector_of_nat ? len). 2178 2179 2179 2180 lemma pose: ∀A:Type[0].∀B:A → Type[0].∀a:A. (∀a':A. a'=a → B a') → B a. … … 2188 2189 2189 2190 theorem main_thm: 2190 ∀M,M',cm,ps, pol,lookup_labels.2191 ∀M,M',cm,ps,sigma. 2191 2192 next_internal_pseudo_address_map M cm ps = Some … M' → 2192 2193 ∃n. 2193 execute n … (status_of_pseudo_status M … ps pol)2194 = status_of_pseudo_status M' … (execute_1_pseudo_instruction (ticks_of cm pol lookup_labels) cm ps) pol.2195 #M #M' * #preamble #instr_list #ps # pol #lookup_labels2194 execute n … (status_of_pseudo_status M … ps sigma) 2195 = status_of_pseudo_status M' … (execute_1_pseudo_instruction (ticks_of cm sigma) cm ps) sigma. 2196 #M #M' * #preamble #instr_list #ps #sigma 2196 2197 change with (next_internal_pseudo_address_map0 ????? = ? → ?) 2197 2198 @(pose … (program_counter ?? ps)) #ppc #EQppc 2198 generalize in match (fetch_assembly_pseudo2 ? pol ppc) in ⊢ ?; 2199 @(pose … (\fst (assembly ? pol))) #assembled #EQassembled 2200 @(pose … (λx.sigma … pol (address_of_word_labels_code_mem instr_list x))) #lookup_labels #EQlookup_labels 2199 generalize in match (fetch_assembly_pseudo2 〈preamble,instr_list〉 sigma ppc) in ⊢ ?; 2200 @pair_elim #labels #costs #H0 normalize nodelta 2201 @pair_elim #assembled #costs' #EQ1 normalize nodelta 2202 @pair_elim #pi #newppc #EQ2 normalize nodelta 2203 @(pose … (λx. \fst (sigma (address_of_word_labels_code_mem instr_list x)))) #lookup_labels #EQlookup_labels 2201 2204 @(pose … (λx. lookup_def … (construct_datalabels preamble) x (zero 16))) #lookup_datalabels #EQlookup_datalabels 2202 2205 whd in match execute_1_pseudo_instruction; normalize nodelta 2203 @pair_elim #pi #newppc #H1 2204 whd in match ticks_of; normalize nodelta <EQppc #H2 >H1 normalize nodelta; 2205 lapply (snd_fetch_pseudo_instruction instr_list ppc) >H1 #EQnewppc >EQnewppc 2206 lapply (snd_assembly_1_pseudoinstruction_ok … ppc pi … EQlookup_labels EQlookup_datalabels ?) 2207 [>H1 %] 2206 whd in match ticks_of; normalize nodelta <EQppc #H2 >EQ2 normalize nodelta 2207 lapply (snd_fetch_pseudo_instruction instr_list ppc) >EQ2 #EQnewppc >EQnewppc 2208 lapply (snd_assembly_1_pseudoinstruction_ok 〈preamble,instr_list〉 … ppc pi … EQlookup_labels EQlookup_datalabels ?) 2209 [>EQ2 %] 2208 2210 inversion pi 2209 2211 [2,3: (* Comment, Cost *) #ARG #EQ … … 2211 2213 whd in ⊢ (??%? → ?); @Some_Some_elim #MAP <MAP 2212 2214 whd in match (execute_1_pseudo_instruction0 ?????); 2213 %{0} @split_eq_status //2215 %{0} @split_eq_status CSC:STOP HERE // 2214 2216 4: (* Jmp *) #label whd in ⊢ (??%? → ???% → ?) 2215 2217 @Some_Some_elim #MAP cases (pol ?) normalize nodelta
Note: See TracChangeset
for help on using the changeset viewer.