# Changeset 2124

Ignore:
Timestamp:
Jun 27, 2012, 4:23:54 PM (7 years ago)
Message:

Much more shuffling around to proper places

Location:
src/ASM
Files:
10 edited

Unmodified
Removed

• ## src/ASM/Arithmetic.ma

 r2111 axiom lt_nat_of_bitvector: ∀n.∀w. nat_of_bitvector n w < 2^n. axiom eq_bitvector_of_nat_to_eq: ∀n,n1,n2. n1 < 2^n → n2 < 2^n → bitvector_of_nat n n1 = bitvector_of_nat n n2 → n1=n2. lemma nat_of_bitvector_aux_injective: add n (bitvector_of_nat ? p) (bitvector_of_nat ? q) = bitvector_of_nat ? (p+q). lemma add_bitvector_of_nat_Sm: ∀n, m: nat. add … (bitvector_of_nat … 1) (bitvector_of_nat … m) = bitvector_of_nat n (S m). #n #m @add_bitvector_of_nat_plus qed. definition sign_bit : ∀n. BitVector n → bool ≝ λn,v. match v with [ VEmpty ⇒ false | VCons _ h _ ⇒ h ]. ]. example sub_minus_one_seven_eight: ∀v: BitVector 7. false ::: (\fst (sub_7_with_carry v (bitvector_of_nat ? 1) false)) = \fst (sub_8_with_carry (false ::: v) (bitvector_of_nat ? 1) false). cases daemon. qed. axiom sub16_with_carry_overflow: ∀left, right, result: BitVector 16. ∀flags: BitVector 3. ∀upper: BitVector 9. ∀lower: BitVector 7. sub_16_with_carry left right false = 〈result, flags〉 → vsplit bool 9 7 result = 〈upper, lower〉 → get_index_v bool 3 flags 2 ? = true → upper = [[true; true; true; true; true; true; true; true; true]]. // qed. axiom sub_16_to_add_16_8_0: ∀v1,v2: BitVector 16. ∀v3: BitVector 7. ∀flags: BitVector 3. get_index' ? 2 0 flags = false → sub_16_with_carry v1 v2 false = 〈(zero 9)@@v3,flags〉 → v1 = add ? v2 (sign_extension (false:::v3)). axiom sub_16_to_add_16_8_1: ∀v1,v2: BitVector 16. ∀v3: BitVector 7. ∀flags: BitVector 3. get_index' ? 2 0 flags = true → sub_16_with_carry v1 v2 false = 〈[[true;true;true;true;true;true;true;true;true]]@@v3,flags〉 → v1 = add ? v2 (sign_extension (true:::v3)).

• ## src/ASM/AssemblyProofSplit.ma

 r2122 qed. (*CSC: move elsewhere*) lemma pair_replace: ∀A,B,T:Type[0].∀P:T → Prop. ∀t. ∀a,b.∀c,c': A × B. c'=c → c ≃ 〈a,b〉 → P (t a b) → P (let 〈a',b'〉 ≝ c' in t a' b'). #A #B #T #P #t #a #b * #x #y * #x' #y' #H1 #H2 destruct // qed. lemma get_arg_8_set_program_counter: ∀M: Type[0]. qed. (*CSC: move elsewhere*) lemma None_Some_elim: ∀P:Prop. ∀A,a. None A = Some A a → P. #P #A #a #abs destruct qed. (* lemma pi1_let_commute: include alias "basics/logic.ma". include alias "ASM/BitVectorTrie.ma". (*CSC: move elsewhere*) lemma jmpair_as_replace: ∀A,B,T:Type[0].∀P:T → Prop. ∀a:A. ∀b:B.∀c,c': A × B. ∀t: ∀a,b. c' ≃ 〈a, b〉 → T. ∀EQc: c'= c. ∀EQ:c ≃ 〈a,b〉. P (t a b ?) → P ((let 〈a',b'〉 (*as H*) ≝ c' in λH. t a' b' H) (refl_jmeq ? c')). [2: >EQc @EQ |1: #A #B #T #P #a #b #c #c' #t #EQc >EQc in t; -c' normalize #f #EQ letin eta ≝ (? : ∀ab:A × B.∀P:A × B → Type[0]. P ab → P 〈\fst ab,\snd ab〉) [2: * // ] change with (eta 〈a,b〉 (λab.c ≃ ab) EQ) in match EQ; @(jmeq_elim ?? (λab.λH.P (f (\fst ab) (\snd ab) ?) → ?) ?? EQ) normalize -eta -EQ cases c in f; normalize // ] qed. (*CSC: move elsewhere*) lemma if_then_else_replace: ∀T: Type[0]. ∀P: T → Prop. ∀t1, t2: T. ∀c, c', c'': bool. c' = c → c ≃ c'' → P (if c'' then t1 else t2) → P (if c' then t1 else t2). #T #P #t1 #t2 #c #c' #c'' #c_refl #c_refl' destruct #assm assumption qed. lemma fetch_many_singleton: #fetch_many_assm whd in fetch_many_assm; cases (eq_bv_eq … fetch_many_assm) assumption qed. (*CSC: move elsewhere*) lemma refl_to_jmrefl: ∀a: Type[0]. ∀l, r: a. l = r → l ≃ r. #a #l #r #refl destruct % qed.
• ## src/ASM/BitVector.ma

 r2122 String. example sub_minus_one_seven_eight: ∀v: BitVector 7. false ::: (\fst (sub_7_with_carry v (bitvector_of_nat ? 1) false)) = \fst (sub_8_with_carry (false ::: v) (bitvector_of_nat ? 1) false). cases daemon. qed. axiom sub16_with_carry_overflow: ∀left, right, result: BitVector 16. ∀flags: BitVector 3. ∀upper: BitVector 9. ∀lower: BitVector 7. sub_16_with_carry left right false = 〈result, flags〉 → vsplit bool 9 7 result = 〈upper, lower〉 → get_index_v bool 3 flags 2 ? = true → upper = [[true; true; true; true; true; true; true; true; true]]. // qed. axiom sub_16_to_add_16_8_0: ∀v1,v2: BitVector 16. ∀v3: BitVector 7. ∀flags: BitVector 3. get_index' ? 2 0 flags = false → sub_16_with_carry v1 v2 false = 〈(zero 9)@@v3,flags〉 → v1 = add ? v2 (sign_extension (false:::v3)). axiom sub_16_to_add_16_8_1: ∀v1,v2: BitVector 16. ∀v3: BitVector 7. ∀flags: BitVector 3. get_index' ? 2 0 flags = true → sub_16_with_carry v1 v2 false = 〈[[true;true;true;true;true;true;true;true;true]]@@v3,flags〉 → v1 = add ? v2 (sign_extension (true:::v3)). definition bitvector_3_cases: ∀b: BitVector 3. ∃l, c, r: bool. b ≃ [[l; c; r]]. #b @(Vector_inv_ind bool 3 b (λn: nat. λv: Vector bool n. ∃l:bool.∃c:bool.∃r:bool. v ≃ [[l; c; r]])) [1: #absurd @⊥ -b @(destruct_bug_fix_1 2) >absurd % |2: #n #hd #tl #_ #size_refl #hd_tl_refl %{hd} cut (n = 2) [1: @destruct_bug_fix_2 >size_refl % |2: #n_refl >n_refl in tl; #V @(Vector_inv_ind bool 2 V (λn: nat. λv: Vector bool n. ∃c:bool. ∃r:bool. hd:::v ≃ [[hd; c; r]])) [1: #absurd @⊥ -V @(destruct_bug_fix_1 1) >absurd % |2: #n' #hd' #tl' #_ #size_refl' #hd_tl_refl' %{hd'} cut (n' = 1) [1: @destruct_bug_fix_2 >size_refl' % |2: #n_refl' >n_refl' in tl'; #V' @(Vector_inv_ind bool 1 V' (λn: nat. λv: Vector bool n. ∃r: bool. hd:::hd':::v ≃ [[hd; hd'; r]])) [1: #absurd @⊥ -V' @(destruct_bug_fix_1 0) >absurd % |2: #n'' #hd'' #tl'' #_ #size_refl'' #hd_tl_refl'' %{hd''} cut (n'' = 0) [1: @destruct_bug_fix_2 >size_refl'' % |2: #n_refl'' >n_refl'' in tl''; #tl''' >(Vector_O … tl''') % ] ] ] ] ] ] qed. lemma bitvector_3_elim_prop: ∀P: BitVector 3 → Prop. P [[false;false;false]] → P [[false;false;true]] → P [[false;true;false]] → P [[false;true;true]] → P [[true;false;false]] → P [[true;false;true]] → P [[true;true;false]] → P [[true;true;true]] → ∀v. P v. #P #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 #H9 cases (bitvector_3_cases … H9) #l #assm cases assm -assm #c #assm cases assm -assm #r #assm cases assm destruct cases l cases c cases r assumption qed.
• ## src/ASM/Fetch.ma

 r2119 λpc: Word. 〈add … pc (bitvector_of_nat 16 1), lookup … pc pmem (zero …)〉. (*CSC: move elsewhere *) axiom eq_bitvector_of_nat_to_eq: ∀n,n1,n2. n1 < 2^n → n2 < 2^n → bitvector_of_nat n n1 = bitvector_of_nat n n2 → n1=n2. discriminator Prod. definition load_code_memory0:
• ## src/ASM/Interpret.ma

 r2108 qed. discriminator Prod. definition compute_target_of_unconditional_jump: ∀program_counter: Word.
• ## src/ASM/StatusProofs.ma

 r2032 program_counter m cm (set_bit_addressable_sfr m cm s addr v) = program_counter m cm s. (* XXX: to be moved elsewhere *) lemma program_counter_set_arg_8: ∀m, cm, s, addr, v.
• ## src/ASM/Util.ma

 r2123 qed. (*CSC: just a synonim, get rid of it!*) lemma Some_eq: ∀T:Type[0].∀x,y:T. Some T x = Some T y → x = y ≝ option_destruct_Some. lemma pi1_eq: ∀A:Type[0].∀P:A->Prop.∀s1:Σa1:A.P a1.∀s2:Σa2:A.P a2. s1 = s2 → (pi1 ?? s1) = (pi1 ?? s2). qed. lemma Some_eq: ∀T:Type[0].∀x,y:T. Some T x = Some T y → x = y. #T #x #y #H @option_destruct_Some @H qed. lemma not_neq_None_to_eq : ∀A.∀a : option A.¬a≠None ? → a = None ?. #A * [2: #a] * // #ABS elim (ABS ?) % #ABS' destruct(ABS') coercion not_neq_None : ∀A.∀a : option A.∀prf : ¬a≠None ?.a = None ? ≝ not_neq_None_to_eq on _prf : ¬?≠None ? to ? = None ?. lemma None_Some_elim: ∀P:Prop. ∀A,a. None A = Some A a → P. #P #A #a #abs destruct qed. discriminator Prod. lemma pair_replace: ∀A,B,T:Type[0].∀P:T → Prop. ∀t. ∀a,b.∀c,c': A × B. c'=c → c ≃ 〈a,b〉 → P (t a b) → P (let 〈a',b'〉 ≝ c' in t a' b'). #A #B #T #P #t #a #b * #x #y * #x' #y' #H1 #H2 destruct // qed. lemma jmpair_as_replace: ∀A,B,T:Type[0].∀P:T → Prop. ∀a:A. ∀b:B.∀c,c': A × B. ∀t: ∀a,b. c' ≃ 〈a, b〉 → T. ∀EQc: c'= c. ∀EQ:c ≃ 〈a,b〉. P (t a b ?) → P ((let 〈a',b'〉 (*as H*) ≝ c' in λH. t a' b' H) (refl_jmeq ? c')). [2: >EQc @EQ |1: #A #B #T #P #a #b #c #c' #t #EQc >EQc in t; -c' normalize #f #EQ letin eta ≝ (? : ∀ab:A × B.∀P:A × B → Type[0]. P ab → P 〈\fst ab,\snd ab〉) [2: * // ] change with (eta 〈a,b〉 (λab.c ≃ ab) EQ) in match EQ; @(jmeq_elim ?? (λab.λH.P (f (\fst ab) (\snd ab) ?) → ?) ?? EQ) normalize -eta -EQ cases c in f; normalize // ] qed. lemma if_then_else_replace: ∀T: Type[0]. ∀P: T → Prop. ∀t1, t2: T. ∀c, c', c'': bool. c' = c → c ≃ c'' → P (if c'' then t1 else t2) → P (if c' then t1 else t2). #T #P #t1 #t2 #c #c' #c'' #c_refl #c_refl' destruct #assm assumption qed. lemma refl_to_jmrefl: ∀a: Type[0]. ∀l, r: a. l = r → l ≃ r. #a #l #r #refl destruct % qed. lemma prod_eq_left: ∀A: Type[0]. ∀p, q, r: A. p = q → 〈p, r〉 = 〈q, r〉. #A #p #q #r #hyp destruct % qed. lemma prod_eq_right: ∀A: Type[0]. ∀p, q, r: A. p = q → 〈r, p〉 = 〈r, q〉. #A #p #q #r #hyp destruct % qed. lemma destruct_bug_fix_1: ∀n: nat. S n = 0 → False. #n #absurd destruct(absurd) qed. lemma destruct_bug_fix_2: ∀m, n: nat. S m = S n → m = n. #m #n #refl destruct % qed. lemma eq_rect_Type1_r: ∀A: Type[1]. ∀a: A. ∀P: ∀x:A. eq ? x a → Type[1]. P a (refl A a) → ∀x: A.∀p:eq ? x a. P x p. #A #a #P #H #x #p generalize in match H; generalize in match P; cases p // qed. lemma Some_Some_elim: ∀T:Type[0].∀x,y:T.∀P:Type[2]. (x=y → P) → Some T x = Some T y → P. #T #x #y #P #H #K @H @option_destruct_Some // qed. lemma pair_destruct_right: ∀A: Type[0]. ∀B: Type[0]. ∀a, c: A. ∀b, d: B. 〈a, b〉 = 〈c, d〉 → b = d. #A #B #a #b #c #d // qed. lemma pose: ∀A:Type[0].∀B:A → Type[0].∀a:A. (∀a':A. a'=a → B a') → B a. /2/ qed. definition eq_sum: ∀A, B. (A → A → bool) → (B → B → bool) → (A ⊎ B) → (A ⊎ B) → bool ≝ λlt, rt, leq, req, left, right. match left with [ inl l ⇒ match right with [ inl l' ⇒ leq l l' | _ ⇒ false ] | inr r ⇒ match right with [ inr r' ⇒ req r r' | _ ⇒ false ] ]. lemma eq_sum_refl: ∀A, B: Type[0]. ∀leq, req. ∀s. ∀leq_refl: (∀t. leq t t = true). ∀req_refl: (∀u. req u u = true). eq_sum A B leq req s s = true. #A #B #leq #req #s #leq_refl #req_refl cases s assumption qed. definition eq_prod: ∀A, B. (A → A → bool) → (B → B → bool) → (A × B) → (A × B) → bool ≝ λlt, rt, leq, req, left, right. let 〈l, r〉 ≝ left in let 〈l', r'〉 ≝ right in leq l l' ∧ req r r'. lemma eq_prod_refl: ∀A, B: Type[0]. ∀leq, req. ∀s. ∀leq_refl: (∀t. leq t t = true). ∀req_refl: (∀u. req u u = true). eq_prod A B leq req s s = true. #A #B #leq #req #s #leq_refl #req_refl cases s whd in ⊢ (? → ? → ??%?); #l #r >leq_refl @req_refl qed. lemma geb_to_leb: ∀a,b:ℕ.geb a b = leb b a.
• ## src/ASM/Vector.ma

 r2122 vsplit' A m n v. lemma vsplit_ok: ∀A: Type[0]. ∀m, n: nat. ∀v: Vector A (m + n). ∀upper: Vector A m. ∀lower: Vector A n. 〈upper, lower〉 = vsplit A m n v → upper @@ lower = v. #A #m #n #v #upper #lower cases daemon qed. lemma vsplit_zero: ∀A,m. interpretation "Vector append" 'vappend v1 v2 = (append ??? v1 v2). lemma vsplit_ok: ∀A: Type[0]. ∀m, n: nat. ∀v: Vector A (m + n). ∀upper: Vector A m. ∀lower: Vector A n. 〈upper, lower〉 = vsplit A m n v → upper @@ lower = v. #A #m #n #v #upper #lower cases daemon qed. lemma vector_append_zero:
Note: See TracChangeset for help on using the changeset viewer.