Changeset 1955 for src/ASM/AssemblyProof.ma
- Timestamp:
- May 16, 2012, 3:03:52 PM (9 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
src/ASM/AssemblyProof.ma
r1953 r1955 17 17 bit_elim_prop (λbit. bitvector_elim_prop_internal n P n' …) 18 18 ]. 19 [1: 20 applyS prefix 21 |2: 22 letin res ≝ (bit ::: prefix) 23 <minus_S_S >minus_Sn_m 24 try assumption @res 25 |3: 26 @le_S_to_le 27 assumption 28 ] 19 try applyS prefix 20 try (@le_S_to_le assumption) 21 letin res ≝ (bit ::: prefix) 22 <minus_S_S >minus_Sn_m 23 assumption 29 24 qed. 30 25 … … 33 28 λP: BitVector n → Prop. 34 29 bitvector_elim_prop_internal n P n ? ?. 35 [ @(le_n ?) 36 | <(minus_n_n ?) 37 @[[ ]] 38 ] 30 try @le_n 31 <minus_n_n @[[ ]] 39 32 qed. 40 33 … … 60 53 | S n' ⇒ λprf2. λprefix. bit_elim (λbit. bitvector_elim_internal n P n' ? ?) 61 54 ]. 62 [1: 63 applyS prefix 64 |2: 65 letin res ≝ (bit ::: prefix) 66 <(minus_S_S ? ?) >(minus_Sn_m ? ?) 67 try @prf2 @res 68 |3: 69 /2/ 70 ]. 55 /2/ 71 56 qed. 72 57 … … 1284 1269 ]. 1285 1270 1271 axiom add_commutative: 1272 ∀n: nat. 1273 ∀l, r: BitVector n. 1274 add n l r = add n r l. 1275 1286 1276 axiom add_bitvector_of_nat_Sm: 1287 1277 ∀n, m: nat. … … 1321 1311 qed. 1322 1312 1323 axiom bitvector_3_cases: 1313 lemma destruct_bug_fix: 1314 3 = 0 → False. 1315 #absurd destruct(absurd) 1316 qed. 1317 1318 definition bitvector_3_cases: 1324 1319 ∀b: BitVector 3. 1325 ∃l, c, r: bool. 1326 b = [[l; c; r]]. 1320 ∃l, c, r: bool. 1321 b ≃ [[l; c; r]] ≝ ?. 1322 #b 1323 @(Vector_inv_ind bool 3 b (λn: nat. λv: Vector bool n. ∃l:bool.∃c:bool.∃r:bool. v ≃ [[l; c; r]])) 1324 [1: 1325 #absurd @⊥ @destruct_bug_fix 1326 >absurd % 1327 |2: 1328 #n #hd #tl #_ #_ #_ %{hd} 1329 cases daemon 1330 ] 1331 qed. 1327 1332 1328 1333 lemma bitvector_3_elim_prop: … … 2187 2192 qed. 2188 2193 2194 definition is_present_in_machine_code_image_p: ∀pseudo_instruction. Prop ≝ 2195 λpseudo_instruction. 2196 match pseudo_instruction with 2197 [ Comment c ⇒ False 2198 | Cost c ⇒ False 2199 | _ ⇒ True 2200 ]. 2201 2189 2202 (*CSC: ???*) 2190 2203 lemma snd_assembly_1_pseudoinstruction_ok: … … 2194 2207 ∀ppc: Word. 2195 2208 ∀pi. 2209 ∀present_in_machine_code_image_witness: is_present_in_machine_code_image_p pi. 2196 2210 ∀lookup_labels. 2197 2211 ∀lookup_datalabels. … … 2199 2213 lookup_datalabels = (λx. lookup_def … (construct_datalabels (\fst program)) x (zero ?)) → 2200 2214 \fst (fetch_pseudo_instruction (\snd program) ppc) = pi → 2201 let len ≝ \fst (assembly_1_pseudoinstruction lookup_labels sigma policy ( sigma ppc)lookup_datalabels pi) in2215 let len ≝ \fst (assembly_1_pseudoinstruction lookup_labels sigma policy (*(sigma ppc)*) ppc lookup_datalabels pi) in 2202 2216 sigma (add … ppc (bitvector_of_nat ? 1)) = add … (sigma ppc) (bitvector_of_nat ? len). 2203 #program #sigma #policy #ppc #pi #lookup_labels #lookup_datalabels 2204 #lookup_labels_refl #lookup_datalabels_refl #fetch_pseudo_refl 2205 normalize nodelta cases daemon (* XXX: !!! *) 2217 #program #sigma #policy #ppc #pi #is_present_in_machine_code_image_witness 2218 #lookup_labels #lookup_datalabels #lookup_labels_refl #lookup_datalabels_refl 2219 #fetch_pseudo_refl 2220 normalize nodelta 2221 generalize in match fetch_pseudo_refl; -fetch_pseudo_refl 2222 generalize in match is_present_in_machine_code_image_witness; -is_present_in_machine_code_image_witness 2223 cases pi 2224 [1: 2225 #preinstruction #_ 2226 |2,3: 2227 (* XXX: bug in original statement here, to prove: sigma (ppc + 1) = sigma ppc *) 2228 #cost_or_comment normalize in ⊢ (% → ?); #absurd cases absurd 2229 |4,5: 2230 #identifier #_ 2231 |6: 2232 #dptr #identifier #_ 2233 ] 2234 #fetch_pseudo_refl 2235 letin assembled ≝ (\fst (assembly program sigma policy)) 2236 letin costs ≝ (\snd (assembly program sigma policy)) 2237 lapply (assembly_ok program sigma policy assembled costs) 2238 @pair_elim #labels #costs' #create_label_cost_map_refl 2239 <eq_pair_fst_snd #H cases (H (refl …)) -H #costs_refl #H 2240 lapply (H ppc) -H 2241 @pair_elim #pi' #newppc #fetch_pseudo_refl' 2242 @pair_elim #len #assembled #assembly1_refl #H cases H 2243 #encoding_check_assm #sigma_newppc_refl 2244 >fetch_pseudo_refl' in fetch_pseudo_refl; #pi_refl' 2245 >pi_refl' in assembly1_refl; #assembly1_refl 2246 >lookup_labels_refl >lookup_datalabels_refl >assembly1_refl 2247 <sigma_newppc_refl 2248 generalize in match fetch_pseudo_refl'; 2249 whd in match (fetch_pseudo_instruction ??); 2250 @pair_elim #lbl #instr #nth_refl normalize nodelta 2251 #G destruct % 2206 2252 qed. 2207 2253
Note: See TracChangeset
for help on using the changeset viewer.