# Changeset 1891 for src/ASM/ASMCosts.ma

Ignore:
Timestamp:
Apr 18, 2012, 2:52:24 PM (9 years ago)
Message:

Nightmarish proofs on bitvectors. Trying to find some way of making sense of these.

File:
1 edited

Unmodified
Removed
• ## src/ASM/ASMCosts.ma

 r1869 qed. inverter nat_jmdiscr for nat. (* XXX: this is false in the general case.  For instance, if n = 0 then the base case requires us prove 1 = 0, as it is the carry bit that holds the result of the addition. *) axiom succ_nat_of_bitvector_half_add_1: ∀n: nat. ∀bv: BitVector n. ∀power_proof: nat_of_bitvector … bv < 2^n - 1. S (nat_of_bitvector … bv) = nat_of_bitvector … (\snd (half_add n (bitvector_of_nat … 1) bv)). lemma plus_lt_to_lt: ∀m, n, o: nat. m + n < o → m < o. #m #n #o elim n [1: <(plus_n_O m) in ⊢ (% → ?); #assumption assumption |2: #n' #inductive_hypothesis <(plus_n_Sm m n') in ⊢ (% → ?); #assm @inductive_hypothesis normalize in assm; normalize /2 by lt_S_to_lt/ ] qed. definition nat_of_bool: bool → nat ≝ λb: bool. match b with [ true ⇒ 1 | false ⇒ 0 ]. axiom nat_of_bitvector_aux_accum: ∀m: nat. ∀v: BitVector m. ∀acc: nat. ∃n: nat. nat_of_bitvector_aux m acc v = n + nat_of_bitvector m v. axiom nat_of_bitvector_plus: ∀n: nat. ∀tl: BitVector n. ∀hd: bool. nat_of_bitvector (S n) (hd:::tl) = (2 ^ n) * nat_of_bool hd + nat_of_bitvector n tl. axiom plus_refl_to_refl_lor_refl: ∀m, m', n, n': nat. m + m' = n + n' → (m = n ∧ m' = n') ∨ (m = n' ∧ m' = n). axiom mult_refl_to_refl_lor_refl: ∀m, m', n, n': nat. m * m' = n * n' → (m = n ∧ m' = n') ∨ (m = n' ∧ n = m'). axiom Vector_inv_ind_2: ∀a: Type[0]. ∀n: nat. ∀left: Vector a n. ∀right: Vector a n. ∀P: (∀m: nat. Vector a m → Vector a m → Prop). (n ≃ 0 → (left ≃ VEmpty a) → (right ≃ VEmpty a) → (P 0 [[ ]] [[ ]])) → (∀m: nat. ∀hd, hd': a. ∀tl, tl': Vector a m. (n ≃ m → left ≃ tl → right ≃ tl' → P m tl tl') → (n ≃ S m → left ≃ hd:::tl → right ≃ hd':::tl' → P (S m) (hd:::tl) (hd':::tl'))) → P n left right. lemma nat_of_bitvector_destruct: ∀n: nat. ∀l_hd, r_hd: bool. ∀l_tl, r_tl: BitVector n. nat_of_bitvector (S n) (l_hd:::l_tl) = nat_of_bitvector (S n) (r_hd:::r_tl) → l_hd = r_hd ∧ nat_of_bitvector n l_tl = nat_of_bitvector n r_tl. #n #l_hd #r_hd #l_tl #r_tl @(Vector_inv_ind_2 bool n l_tl r_tl) [1: #length_refl #l_tl_refl #r_tl_refl destruct cases l_hd cases r_hd normalize try (#absurd destruct(absurd)) @conj % |2: #m #l_hd' #r_hd' #l_tl' #r_tl' #inductive_hypothesis #n_refl #l_tl_refl #r_tl_refl destruct elim l_tl [1: #r_tl >(BitVector_O r_tl) normalize cases l_hd cases r_hd normalize try (#absurd destruct(absurd)) @conj % |2: #n' #hd #tl #inductive_hypothesis #r_tl cases (BitVector_Sn … r_tl) #hd' #tl_hypothesis' cases tl_hypothesis' #tl' #tl_refl' >tl_refl' cases daemon ] qed. axiom Vector_inv_ind_2: ∀a: Type[0]. ∀n: nat. ∀left: Vector a n. ∀right: Vector a n. ∀P: (∀m: nat. Vector a m → Vector a m → Prop). (n ≃ 0 → (left ≃ VEmpty a) → (right ≃ VEmpty a) → (P 0 [[ ]] [[ ]])) → (∀m: nat. ∀hd, hd': a. ∀tl, tl': Vector a m. (n ≃ m → left ≃ tl → right ≃ tl' → P m tl tl') → (n ≃ S m → left ≃ hd:::tl → right ≃ hd':::tl' → P (S m) (hd:::tl) (hd':::tl'))) → P n left right. lemma BitVector_cons_injective: ∀n: nat. ∀l_hd, r_hd: bool. ∀l_tl, r_tl: BitVector n. l_hd = r_hd → l_tl = r_tl → l_hd:::l_tl = r_hd:::r_tl. #l #l_hd #r_hd #l_tl #r_tl #l_refl #r_refl destruct % qed. lemma refl_nat_of_bitvector_to_refl: ∀n: nat. ∀l, r: BitVector n. nat_of_bitvector n l = nat_of_bitvector n r → l = r. #n elim n [1: #l #r >(BitVector_O l) >(BitVector_O r) #_ % |2: #n' #inductive_hypothesis #l #r lapply (BitVector_Sn ? l) #l_hypothesis lapply (BitVector_Sn ? r) #r_hypothesis cases l_hypothesis #l_hd #l_tail_hypothesis cases r_hypothesis #r_hd #r_tail_hypothesis cases l_tail_hypothesis #l_tl #l_hd_tl_refl cases r_tail_hypothesis #r_tl #r_hd_tl_refl destruct #cons_refl cases (nat_of_bitvector_destruct n' l_hd r_hd l_tl r_tl cons_refl) #hd_refl #tl_refl @BitVector_cons_injective try assumption @inductive_hypothesis assumption ] qed. let rec traverse_code_internal (code_memory: BitVectorTrie Byte 16) (cost_labels: BitVectorTrie costlabel 16) (good_program_witness: good_program code_memory fixed_program_size) (program_size_invariant: nat_of_bitvector … program_counter + program_size = fixed_program_size) (fixed_program_size_limit: fixed_program_size < 2^16 + 1) (fixed_program_size_limit: fixed_program_size < 2^16 - 1) on program_size: Σcost_map: identifier_map CostTag nat. ] (refl … program_size). cut((S (nat_of_bitvector 16 program_counter)) = nat_of_bitvector 16 (\snd  (half_add 16 (bitvector_of_nat 16 1) program_counter))) [1,3,5,7,9,11,13: [1: destruct @succ_nat_of_bitvector_half_add_1 lookup_opt_assm whd |2: #k #k_pres ] ]
Note: See TracChangeset for help on using the changeset viewer.