Changeset 1039 for src/ASM/AssemblyProof.ma
- Timestamp:
- Jun 24, 2011, 2:11:08 PM (8 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
src/ASM/AssemblyProof.ma
r1037 r1039 1252 1252 1253 1253 axiom assembly_ok: 1254 ∀program,pol,assembled .1254 ∀program,pol,assembled,costs'. 1255 1255 let 〈labels,costs〉 ≝ build_maps program pol in 1256 〈assembled,costs〉 = assembly program pol → 1256 〈assembled,costs'〉 = assembly program pol → 1257 costs = costs' ∧ 1257 1258 let code_memory ≝ load_code_memory assembled in 1258 1259 let preamble ≝ \fst program in … … 1281 1282 Some ? instructions = expand_pseudo_instruction_safe lookup_labels lookup_datalabels (sigma program pol ppc) expansion pi. 1282 1283 1283 (*CSC: repair me!*) 1284 axiom fetch_assembly_pseudo2: 1284 lemma fetch_assembly_pseudo2: 1285 1285 ∀program,pol,ppc. 1286 1286 (* let 〈labels,costs〉 ≝ build_maps program pol in *) … … 1293 1293 let instructions ≝ expand_pseudo_instruction program pol ppc lookup_labels lookup_datalabels (sigma program pol ppc) (refl …) (refl …) (refl …) in 1294 1294 fetch_many code_memory (sigma program pol newppc) (sigma program pol ppc) instructions. 1295 (* 1296 #program #pol #assembled generalize in match (assembly_ok program pol assembled) 1297 @pair_elim' #labels #costs #BUILD_MAPS 1298 #H #ASSEMBLY #ppc #pi #newppc 1295 * #preamble #instr_list #pol #ppc 1296 letin assembled ≝ (\fst (assembly 〈preamble,instr_list〉 pol)) 1299 1297 letin code_memory ≝ (load_code_memory assembled) 1300 letin preamble ≝ (\fst program)1301 1298 letin data_labels ≝ (construct_datalabels preamble) 1302 letin lookup_labels ≝ (λx. sigma program pol (address_of_word_labels_code_mem (\snd program)x))1299 letin lookup_labels ≝ (λx. sigma … pol (address_of_word_labels_code_mem instr_list x)) 1303 1300 letin lookup_datalabels ≝ (λx. lookup ? ? x data_labels (zero ?)) 1304 normalize nodelta #EQ generalize in match (H ASSEMBLY ppc) -H; 1305 generalize in match (fetch_assembly_pseudo program pol ppc code_memory) in ⊢ ? normalize nodelta 1306 @pair_elim' #len #assembledi #ASSEMBLE1 #H1 #H2 1307 generalize in match (H1 ?) [2: cases (H2 len assembledi (refl …)) #H1 #_ @H1] 1308 >bitvector_of_nat_nat_of_bitvector 1309 #K 1310 1311 1312 cases 1313 (assembly_1_pseudoinstruction program pol ppc lookup_labels lookup_datalabels ????) 1314 @split_elim' #len #assembledi #ASSEMBLY1 1315 1316 @pair_elim' 1317 1318 normalize nodelta; 1319 whd in ⊢ (% → %) generalize in match (assembly_ok program pol assembled) >BUILD_MAPS #XX generalize in match (XX ASSEMBLY ppc) -XX; 1320 cases (fetch_pseudo_instruction (\snd program) ppc) #pi #newppc 1321 generalize in match (fetch_assembly_pseudo program pol ppc 1322 (λx. sigma program pol (address_of_word_labels_code_mem (\snd program) x)) (λx. lookup ?? x data_labels (zero ?)) pi 1323 (load_code_memory assembled)); 1324 whd in ⊢ ((∀_.∀_.∀_.∀_.%) → (∀_.∀_.%) → % → %) #H1 #H2 * #instructions #EXPAND 1325 whd in H1:(∀_.∀_.∀_.∀_.? → ???% → ?) H2:(∀_.∀_.???% → ?); 1326 normalize nodelta in EXPAND; (* HERE *) 1327 generalize in match (λlen, assembled.H1 len assembled instructions (nat_of_bitvector … (sigma program pol ppc))) -H1; #H1 1328 >bitvector_of_nat_nat_of_bitvector in H1; #H1 1329 <EXPAND in H1 H2; whd in ⊢ ((∀_.∀_.? → ???% → ?) → (∀_.∀_.???% → ?) → ?) 1330 #H1 #H2 1331 cases (H2 ?? (refl …)) -H2; #K1 #K2 >K2 1332 generalize in match (H1 ?? (refl …) (refl …) ?) -H1; 1333 [ #K3 % [2: % [% | @K3]] | @K1 ] 1334 qed. 1335 *) 1336 1337 (* 1338 lemma fetch_assembly_pseudo2: 1339 ∀program,pol,assembled. 1340 let 〈labels,costs〉 ≝ build_maps program pol in 1341 〈assembled,costs〉 = assembly program pol → 1342 ∀ppc. 1343 let code_memory ≝ load_code_memory assembled in 1344 let preamble ≝ \fst program in 1345 let data_labels ≝ construct_datalabels preamble in 1346 let lookup_labels ≝ λx. sigma program pol (address_of_word_labels_code_mem (\snd program) x) in 1347 let lookup_datalabels ≝ λx. lookup ? ? x data_labels (zero ?) in 1348 let expansion ≝ pol ppc in 1349 let 〈pi,newppc〉 ≝ fetch_pseudo_instruction (\snd program) ppc in 1350 ∃instructions. 1351 Some ? instructions = expand_pseudo_instruction_safe lookup_labels lookup_datalabels (sigma program pol ppc) expansion pi ∧ 1352 fetch_many code_memory (sigma program pol newppc) (sigma program pol ppc) instructions. 1353 #program #pol #assembled @pair_elim' #labels #costs #BUILD_MAPS #ASSEMBLY #ppc 1354 generalize in match (assembly_ok_to_expand_pseudo_instruction_ok program pol assembled costs ASSEMBLY ppc) 1355 letin code_memory ≝ (load_code_memory assembled) 1356 letin preamble ≝ (\fst program) 1357 letin data_labels ≝ (construct_datalabels preamble) 1358 letin lookup_labels ≝ (λx. sigma program pol (address_of_word_labels_code_mem (\snd program) x)) 1359 letin lookup_datalabels ≝ (λx. lookup ? ? x data_labels (zero ?)) 1360 whd in ⊢ (% → %) generalize in match (assembly_ok program pol assembled) >BUILD_MAPS #XX generalize in match (XX ASSEMBLY ppc) -XX; 1361 cases (fetch_pseudo_instruction (\snd program) ppc) #pi #newppc 1362 generalize in match (fetch_assembly_pseudo program pol ppc 1363 (λx. sigma program pol (address_of_word_labels_code_mem (\snd program) x)) (λx. lookup ?? x data_labels (zero ?)) 1364 (load_code_memory assembled)); 1365 whd in ⊢ ((∀_.∀_.∀_.∀_.%) → (∀_.∀_.%) → % → %) #H1 #H2 * #instructions #EXPAND 1366 whd in H1:(∀_.∀_.∀_.∀_.? → ???% → ?) H2:(∀_.∀_.???% → ?); 1367 normalize nodelta in EXPAND; (* HERE *) 1368 generalize in match (λlen, assembled.H1 len assembled instructions (nat_of_bitvector … (sigma program pol ppc))) -H1; #H1 1369 >bitvector_of_nat_nat_of_bitvector in H1; #H1 1370 <EXPAND in H1 H2; whd in ⊢ ((∀_.∀_.? → ???% → ?) → (∀_.∀_.???% → ?) → ?) 1371 #H1 #H2 1372 cases (H2 ?? (refl …)) -H2; #K1 #K2 >K2 1373 generalize in match (H1 ?? (refl …) (refl …) ?) -H1; 1374 [ #K3 % [2: % [% | @K3]] | @K1 ] 1375 qed. 1376 *) 1301 @pair_elim' #pi #newppc #EQ1 change in EQ1 with (fetch_pseudo_instruction instr_list ? = ?) 1302 generalize in match (assembly_ok ? pol assembled (\snd (assembly 〈preamble,instr_list〉 pol))) 1303 @pair_elim' #labels #costs #EQ2 <eq_pair_fst_snd 1304 #H cases (H (refl \ldots)) -H; #EQ3 1305 generalize in match (refl … (assembly_1_pseudoinstruction … pol ppc lookup_labels lookup_datalabels ? (refl …) (refl …) (refl …))) 1306 cases (assembly_1_pseudoinstruction ?????????) in ⊢ (???% → ?) #len #assembledi #EQ4 1307 #H cases (H ppc len assembledi ?) [2: <EQ4 %] -H; #H1 #H2 1308 generalize in match (fetch_assembly_pseudo … pol ppc (load_code_memory assembled)) in ⊢ ? 1309 >EQ4 #H generalize in match (H H1) in ⊢ ? -H; >(pair_destruct_2 ????? (sym_eq … EQ1)) 1310 >H2 #K @K 1311 qed. 1377 1312 1378 1313 (* OLD? … … 2023 1958 (* Dependent types madness ends here *) 2024 1959 letin ppc ≝ (program_counter … ps) 2025 generalize in match (fetch_assembly_pseudo2 ? pol ppc) 1960 generalize in match (fetch_assembly_pseudo2 ? pol ppc) in ⊢ ? 2026 1961 letin assembled ≝ (\fst (assembly ? pol)) 2027 1962 letin lookup_labels ≝ (λx. sigma ? pol (address_of_word_labels_code_mem instr_list x)) … … 2045 1980 #H2 #EQ %[1,3:@0] 2046 1981 <MAP >(eq_bv_eq … H2) >EQ % 2047 2048 lemma main_thm0: 2049 ∀M,M',ps,preamble,instr_list,pol. 2050 ∀EQ0 : (code_memory pseudo_assembly_program ps=〈preamble,instr_list〉). 2051 ∀assembled. 2052 ∀H: 2053 (∀ppc. 2054 let 〈pi,newppc〉 ≝ fetch_pseudo_instruction instr_list ppc in 2055 let instructions ≝ 2056 expand_pseudo_instruction 2057 〈preamble,instr_list〉 pol ppc 2058 (λx:Identifier 2059 .sigma 〈preamble,instr_list〉 pol 2060 (address_of_word_labels_code_mem instr_list x)) 2061 (λx:BitVector 16 2062 .lookup Identifier 16 x (construct_datalabels preamble) (zero 16)) 2063 (sigma 〈preamble,instr_list〉 pol ppc) 2064 (refl …) (refl …) (refl …) 2065 in 2066 fetch_many (load_code_memory assembled) 2067 (sigma 〈preamble,instr_list〉 pol newppc) (sigma 〈preamble,instr_list〉 pol ppc) 2068 instructions). 2069 ∀MAP:(next_internal_pseudo_address_map0 pseudo_assembly_program 2070 (\fst (fetch_pseudo_instruction instr_list 2071 (program_counter pseudo_assembly_program ps))) M ps 2072 =Some internal_pseudo_address_map M'). 2073 ∀ps'. 2074 (ps'=execute_1_pseudo_instruction (ticks_of 〈preamble,instr_list〉 pol) ps 2075 →∃n:ℕ 2076 .execute n 2077 (set_low_internal_ram (BitVectorTrie Byte 16) 2078 (set_high_internal_ram (BitVectorTrie Byte 16) 2079 (set_program_counter (BitVectorTrie Byte 16) 2080 (set_code_memory pseudo_assembly_program (BitVectorTrie Byte 16) ps 2081 (load_code_memory assembled)) 2082 (sigma 〈preamble,instr_list〉 pol (program_counter pseudo_assembly_program ps))) 2083 (high_internal_ram_of_pseudo_high_internal_ram M 2084 (high_internal_ram pseudo_assembly_program ps))) 2085 (low_internal_ram_of_pseudo_low_internal_ram M 2086 (low_internal_ram pseudo_assembly_program ps))) 2087 =set_low_internal_ram (BitVectorTrie Byte 16) 2088 (set_high_internal_ram (BitVectorTrie Byte 16) 2089 (set_program_counter (BitVectorTrie Byte 16) 2090 (set_code_memory pseudo_assembly_program (BitVectorTrie Byte 16) ps' 2091 (load_code_memory assembled)) 2092 (sigma 〈preamble,instr_list〉 pol 2093 (program_counter pseudo_assembly_program ps'))) 2094 (high_internal_ram_of_pseudo_high_internal_ram M' 2095 (high_internal_ram pseudo_assembly_program ps'))) 2096 (low_internal_ram_of_pseudo_low_internal_ram M' 2097 (low_internal_ram pseudo_assembly_program ps'))). 2098 #M #M' #ps #preamble #instr_list #pol #EQ0 #assembled #H #MAP #ps' 2099 whd in ⊢ (???(?%?) → ?) normalize nodelta 2100 generalize in match (H (program_counter … ps)) -H; >EQ0 normalize nodelta; 2101 2102 whd in match expand_pseudo_instruction normalize nodelta; 2103 whd in match execute_1_pseudo_instruction (*!!! USARE 0 !!!*) normalize nodelta; >EQ0 2104 normalize in match (\snd 〈preamble,instr_list〉); 2105 cases (fetch_pseudo_instruction instr_list (program_counter pseudo_assembly_program ps)) in MAP ⊢ % 2106 #pi #newppc normalize nodelta; #MAP 2107 cases pi in MAP; normalize nodelta; 2108 [2,3: (* Comment, Cost *) #ARG #MAP whd in ⊢ (% → ?) #H2 #EQ %[1,3:@0] 2109 generalize in match (option_destruct_Some ??? MAP) -MAP; #MAP <MAP -MAP M'; 2110 (* 2111 normalize in H1; generalize in match (option_destruct_Some ??? H1) #K1 >K1 i 2112 n H2; whd in ⊢ (% → ?) 2113 #H2*) >(eq_bv_eq … H2) >EQ % 2114 2115 2116 2117 lemma main_thm0: 2118 ∀M,M',ps,s,s'',pol. 2119 next_internal_pseudo_address_map M ps = Some … M' → 2120 status_of_pseudo_status M ps pol = s → 2121 status_of_pseudo_status M' (execute_1_pseudo_instruction (ticks_of (code_memory … ps) pol) ps) ? = s'' → 2122 ∃n. execute n s = s''. 2123 [2: >execute_1_pseudo_instruction_preserves_code_memory @pol] 2124 #M #M' #ps #s #s'' #pol 2125 generalize in match (fetch_assembly_pseudo2 (code_memory … ps) pol) 2126 >execute_1_pseudo_instruction_preserves_code_memory 2127 generalize in match (refl … (assembly (code_memory … ps) pol)) 2128 generalize in match (assembly (code_memory … ps) pol) in ⊢ (??%? → ?) #ASS #K <K generalize in match K; -K; 2129 2130 2131 whd in ⊢ (? → ? → ??%? → ??%? → ?) 2132 >execute_1_pseudo_instruction_preserves_code_memory 2133 generalize in match (refl … (assembly (code_memory … ps) pol)) 2134 generalize in match (assembly (code_memory … ps) pol) in ⊢ (??%? → ?) #ASS #K <K generalize in match K; -K; 2135 whd in ⊢ (???% → ?) 2136 cases (build_maps (code_memory … ps) pol) 2137 #labels #costs change in ⊢ (? → ? → ??%? → ?) with (next_internal_pseudo_address_map0 ? ? ? ?) 2138 cases (code_memory … ps) in pol ⊢ %; 2139 generalize in match pol; -pol; 2140 @(match code_memory … ps return λx. ∀e:code_memory … ps = x.? with [pair preamble instr_list ⇒ ?]) [%] 2141 #EQ0 #pol normalize nodelta; 1982 |4: (* Jmp *) #label whd in ⊢ (??%? → ???% → ?) 1983 @Some_Some_elim #MAP cases (pol ?) normalize nodelta 1984 [3: (* long *) #EQ3 @(Some_Some_elim ????? EQ3) #EQ3' 1985 whd in match eject normalize nodelta >EQ3' in ⊢ (% → ?) whd in ⊢ (% → ?) 1986 @pair_elim' * #instr #newppc' #ticks #EQ4 1987 * * #H2a #H2b whd in ⊢ (% → ?) #H2 1988 >H2b >(eq_instruction_to_eq … H2a) 1989 #EQ %[@1] 1990 <MAP >(eq_bv_eq … H2) >EQ 1991 whd in ⊢ (??%?) >EQ4 whd in ⊢ (??%?) 1992 cases ps in EQ4; #A1 #A2 #A3 #A4 #A5 #A6 #A7 #A8 #A9 #A10 #XXX >XXX % 1993 whd in ⊢ (??%?) 1994 whd in ⊢ (??(match ?%? with [_ ⇒ ?])?) 1995 cases ps in EQ0 ⊢ %; #A1 #A2 #A3 #A4 #A5 #A6 #A7 #A8 #A9 #A10 #XXXX >XXXX % 2142 1996 2143 1997
Note: See TracChangeset
for help on using the changeset viewer.