Changeset 1984 for src/ASM/AssemblyProof.ma
 Timestamp:
 May 22, 2012, 5:37:09 PM (8 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/ASM/AssemblyProof.ma
r1983 r1984 1435 1435 [ nil ⇒ eq_bv … pc final_pc = true 1436 1436  cons i tl ⇒ 1437 (∃pc': Word. 〈i, pc', ticks_of_instruction i〉 = fetch code_memory pc ∧ 1437 let pc' ≝ add 16 pc (bitvector_of_nat 16 (assembly1 … i)) in 1438 (〈i, pc', ticks_of_instruction i〉 = fetch code_memory pc ∧ 1438 1439 fetch_many code_memory final_pc pc' tl) 1439 1440 ]. … … 1507 1508 lapply (conjunction_true ?? H3) * #H4 #H5 1508 1509 lapply (conjunction_true … H4) * #B1 #B2 1509 %{pc'} <(eq_instruction_to_eq … B1) >(eq_bv_eq … H5)1510 >(eqb_true_to_refl … B2) %try % @IH @H21510 >(eq_instruction_to_eq … B1) >(eq_bv_eq … H5) % 1511 >(eqb_true_to_refl … B2) >(eq_instruction_to_eq … B1) try % @IH @H2 1511 1512 ] 1512 1513 qed. … … 2364 2365 // 2365 2366 qed. 2367 2368 (* XXX: easy but tedious *) 2369 axiom assembly1_lt_128: 2370 ∀i: instruction. 2371 (assembly1 i) < 128. 2372 2373 axiom most_significant_bit_zero: 2374 ∀size, m: nat. 2375 ∀size_proof: 0 < size. 2376 m < 2^size → get_index_v bool (S size) (bitvector_of_nat (S size) m) 1 ? = false. 2377 normalize in size_proof; /2/ 2378 qed. 2379 2380 lemma bitvector_of_nat_sign_extension_equivalence: 2381 ∀m: nat. 2382 ∀size_proof: m < 128. 2383 sign_extension … (bitvector_of_nat 8 m) = bitvector_of_nat 16 m. 2384 #m #size_proof whd in ⊢ (??%?); 2385 >most_significant_bit_zero 2386 [1: 2387 cases daemon 2388 2: 2389 assumption 2390 3: 2391 // 2392 ] 2393 qed.
Note: See TracChangeset
for help on using the changeset viewer.