- Timestamp:
- Jun 26, 2012, 5:30:41 PM (9 years ago)
- Location:
- src
- Files:
-
- 6 edited
Legend:
- Unmodified
- Added
- Removed
-
src/ASM/Arithmetic.ma
r2108 r2111 189 189 ∀b: BitVector n. 190 190 bitvector_of_nat n (nat_of_bitvector n b) = b. 191 192 axiom lt_nat_of_bitvector: ∀n.∀w. nat_of_bitvector n w < 2^n. 191 193 192 194 lemma nat_of_bitvector_aux_injective: … … 689 691 add … l r = add … r l. 690 692 693 axiom nat_of_bitvector_add: 694 ∀n,v1,v2. 695 nat_of_bitvector n v1 + nat_of_bitvector n v2 < 2^n → 696 nat_of_bitvector n (add n v1 v2) = nat_of_bitvector n v1 + nat_of_bitvector n v2. 697 691 698 example add_SO: 692 699 ∀n: nat. -
src/ASM/Assembly.ma
r2110 r2111 581 581 \fst (assembly_1_pseudoinstruction lookup_labels sigma policy ppc (λx.zero …) i). 582 582 583 (*CSC: move elsewhere *)584 lemma nth_safe_append:585 ∀A,l,n,n_ok.586 ∃pre,suff.587 (pre @ [nth_safe A n l n_ok]) @ suff = l.588 #A #l elim l normalize589 [ #n #abs cases (absurd ? abs (not_le_Sn_O ?))590 | #hd #tl #IH #n cases n normalize591 [ #_ %{[]} /2/592 | #m #m_ok cases (IH m ?)593 [ #pre * #suff #EQ %{(hd::pre)} %{suff} <EQ in ⊢ (???%); % | skip ]]594 qed.595 596 lemma fetch_pseudo_instruction_vsplit:597 ∀instr_list,ppc,ppc_ok.598 ∃pre,suff,lbl.599 (pre @ [〈lbl,\fst (fetch_pseudo_instruction instr_list ppc ppc_ok)〉]) @ suff = instr_list.600 #instr_list #ppc #ppc_ok whd in match (fetch_pseudo_instruction ???);601 cases (nth_safe_append … instr_list … ppc_ok) #pre * #suff #EQ %{pre} %{suff}602 lapply EQ -EQ cases (nth_safe labelled_instruction ???) #lbl0 #instr normalize nodelta603 #EQ %{lbl0} @EQ604 qed.605 606 axiom eqb_succ_injective_Pos:607 ∀l, r: Pos.608 eqb (succ l) (succ r) = true → eqb l r = true.609 610 lemma eqb_true_to_refl_Pos:611 ∀l, r: Pos.612 eqb l r = true → l = r.613 #l #r @(pos_elim2 … l r)614 [1:615 #r cases r616 [1:617 #_ %618 |2,3:619 #l normalize in ⊢ (% → ?); #absurd destruct(absurd)620 ]621 |2:622 #l cases l623 [1:624 normalize in ⊢ (% → ?); #absurd destruct(absurd)625 |2,3:626 #l' normalize in ⊢ (% → ?); #absurd destruct(absurd)627 ]628 |3:629 #l #r #inductive_hypothesis #relevant @eq_f630 @inductive_hypothesis @eqb_succ_injective_Pos631 assumption632 ]633 qed.634 635 lemma eq_identifier_eq:636 ∀tag: String.637 ∀l.638 ∀r.639 eq_identifier tag l r = true → l = r.640 #tag #l #r cases l cases r641 #pos_l #pos_r642 cases pos_l cases pos_r643 [1:644 #_ %645 |2,3,4,7:646 #p1_l normalize in ⊢ (% → ?);647 #absurd destruct(absurd)648 |5,9:649 #p1_l #p1_r normalize in ⊢ (% → ?);650 #relevant651 >(eqb_true_to_refl_Pos … relevant) %652 |*:653 #p_l #p_r normalize in ⊢ (% → ?);654 #absurd destruct(absurd)655 ]656 qed.657 658 axiom neq_identifier_neq:659 ∀tag: String.660 ∀l, r: identifier tag.661 eq_identifier tag l r = false → (l = r → False).662 583 663 584 (* label_map: identifier ↦ pseudo program counter *) … … 772 693 qed. 773 694 774 775 (*CSC: move elsewhere; practically equal to shift_nth_safe but for commutation776 of addition. One of the two lemmas should disappear. *)777 lemma nth_safe_prepend:778 ∀A,l1,l2,j.∀H:j<|l2|.∀K:|l1|+j<|(l1@l2)|.779 nth_safe A j l2 H =nth_safe A (|l1|+j) (l1@l2) K.780 #A #l1 #l2 #j #H >commutative_plus @shift_nth_safe781 qed.782 783 lemma nth_safe_cons:784 ∀A,hd,tl,l2,j,j_ok,Sj_ok.785 nth_safe A j (tl@l2) j_ok =nth_safe A (1+j) (hd::tl@l2) Sj_ok.786 //787 qed.788 789 lemma eq_nth_safe_proof_irrelevant:790 ∀A,l,i,i_ok,i_ok'.791 nth_safe A l i i_ok = nth_safe A l i i_ok'.792 #A #l #i #i_ok #i_ok' %793 qed.794 795 (*CSC: move elsewhere *)796 axiom nat_of_bitvector_add:797 ∀n,v1,v2.798 nat_of_bitvector n v1 + nat_of_bitvector n v2 < 2^n →799 nat_of_bitvector n (add n v1 v2) = nat_of_bitvector n v1 + nat_of_bitvector n v2.800 801 (*CSC: move elsewhere *)802 lemma fetch_pseudo_instruction_append:803 ∀l1,l2. |l1@l2| ≤ 2^16 → ∀ppc,ppc_ok,ppc_ok'.804 let code_newppc ≝ fetch_pseudo_instruction l2 ppc ppc_ok in805 fetch_pseudo_instruction (l1@l2) (add … (bitvector_of_nat … (|l1|)) (ppc)) ppc_ok' =806 〈\fst code_newppc, add … (bitvector_of_nat … (|l1|)) (\snd code_newppc)〉.807 #l1 #l2 #l1l2_ok #ppc #ppc_ok whd in match fetch_pseudo_instruction; normalize nodelta808 cut (|l1| + nat_of_bitvector … ppc < 2^16)809 [ @(transitive_le … l1l2_ok) >length_append @monotonic_lt_plus_r assumption ]810 -l1l2_ok #l1ppc_ok >nat_of_bitvector_add811 >nat_of_bitvector_bitvector_of_nat_inverse try assumption812 [2,3: @(transitive_le … l1ppc_ok) @le_S_S // ]813 #ppc_ok' <nth_safe_prepend try assumption cases (nth_safe labelled_instruction ???)814 #lbl #instr normalize nodelta >add_associative %815 qed.816 817 695 definition sigma_policy_specification ≝ 818 696 λprogram: pseudo_assembly_program. … … 832 710 ( (nat_of_bitvector … ppc < |instr_list| → nat_of_bitvector … pc < nat_of_bitvector … next_pc) 833 711 ∨ (nat_of_bitvector … ppc = |instr_list| → next_pc = (zero …))). 834 835 (*CSC: Move elsewhere *)836 axiom lt_nat_of_bitvector: ∀n.∀w. nat_of_bitvector n w < 2^n.837 712 838 713 definition assembly: -
src/ASM/AssemblyProof.ma
r2110 r2111 3 3 include "ASM/StatusProofs.ma". 4 4 include alias "arithmetics/nat.ma". 5 6 definition bit_elim_prop: ∀P: bool → Prop. Prop ≝7 λP.8 P true ∧ P false.9 10 let rec bitvector_elim_prop_internal11 (n: nat) (P: BitVector n → Prop) (m: nat)12 on m:13 m ≤ n → BitVector (n - m) → Prop ≝14 match m return λm. m ≤ n → BitVector (n - m) → Prop with15 [ O ⇒ λprf1. λprefix. P ?16 | S n' ⇒ λprf2. λprefix.17 bit_elim_prop (λbit. bitvector_elim_prop_internal n P n' …)18 ].19 try applyS prefix20 try (@le_S_to_le assumption)21 letin res ≝ (bit ::: prefix)22 <minus_S_S >minus_Sn_m23 assumption24 qed.25 26 definition bitvector_elim_prop ≝27 λn: nat.28 λP: BitVector n → Prop.29 bitvector_elim_prop_internal n P n ? ?.30 try @le_n31 <minus_n_n @[[ ]]32 qed.33 34 lemma bool_eq_internal_eq:35 ∀b, c.36 (λb. λc. (if b then c else (if c then false else true))) b c = true → b = c.37 #b #c38 cases b cases c normalize nodelta39 try (#_ % @I)40 #assm destruct %41 qed.42 5 43 6 definition bit_elim: ∀P: bool → bool. bool ≝ … … 62 25 try @le_n 63 26 <minus_n_n @[[]] 64 qed.65 66 lemma mem_middle_vector:67 ∀A: Type[0].68 ∀m, o: nat.69 ∀eq: A → A → bool.70 ∀reflex: ∀a. eq a a = true.71 ∀p: Vector A m.72 ∀a: A.73 ∀r: Vector A o.74 mem A eq ? (p@@(a:::r)) a = true.75 #A #m #o #eq #reflex #p #a76 elim p try (normalize >reflex #H %)77 #m' #hd #tl #inductive_hypothesis78 normalize79 cases (eq ??) normalize nodelta80 try (#irrelevant %)81 @inductive_hypothesis82 27 qed. 83 28 … … 136 81 cases v try % 137 82 #n' #hd #tl % 138 qed.139 140 corollary subvector_hd_tl:141 ∀A: Type[0].142 ∀o: nat.143 ∀eq: A → A → bool.144 ∀refl: ∀a. eq a a = true.145 ∀h: A.146 ∀v: Vector A o.147 bool_to_Prop (subvector_with A ? ? eq v (h ::: v)).148 #A #o #eq #reflex #h #v149 >(vector_cons_append … h v)150 <(vector_cons_empty … ([[h]] @@ v))151 @(subvector_multiple_append … eq reflex [[ ]] v ? [[h]])152 83 qed. 153 84 … … 236 167 ] 237 168 qed. 238 239 definition product_elim ≝240 λm, n: nat.241 λv: Vector addressing_mode_tag (S m).242 λq: Vector addressing_mode_tag (S n).243 λP: (v × q) → bool.244 list_addressing_mode_tags_elim ? v (λx. list_addressing_mode_tags_elim ? q (λy. P 〈x, y〉)).245 246 definition union_elim ≝247 λA, B: Type[0].248 λelimA: (A → bool) → bool.249 λelimB: (B → bool) → bool.250 λelimU: A ⊎ B → bool.251 elimA (λa. elimB (λb. elimU (inl ? ? a) ∧ elimU (inr ? ? b))).252 253 (*254 definition preinstruction_elim: ∀P: preinstruction [[ relative ]] → bool. bool ≝255 λP.256 list_addressing_mode_tags_elim ? [[ registr ; direct ; indirect ; data ]] (λaddr. P (ADD ? ACC_A addr)) ∧257 list_addressing_mode_tags_elim ? [[ registr ; direct ; indirect ; data ]] (λaddr. P (ADDC ? ACC_A addr)) ∧258 list_addressing_mode_tags_elim ? [[ registr ; direct ; indirect ; data ]] (λaddr. P (SUBB ? ACC_A addr)) ∧259 list_addressing_mode_tags_elim ? [[ acc_a ; registr ; direct ; indirect ; dptr ]] (λaddr. P (INC ? addr)) ∧260 list_addressing_mode_tags_elim ? [[ acc_a ; registr ; direct ; indirect ]] (λaddr. P (DEC ? addr)) ∧261 list_addressing_mode_tags_elim ? [[acc_b]] (λaddr. P (MUL ? ACC_A addr)) ∧262 list_addressing_mode_tags_elim ? [[acc_b]] (λaddr. P (DIV ? ACC_A addr)) ∧263 list_addressing_mode_tags_elim ? [[ registr ; direct ]] (λaddr. bitvector_elim 8 (λr. P (DJNZ ? addr (RELATIVE r)))) ∧264 list_addressing_mode_tags_elim ? [[ acc_a ; carry ; bit_addr ]] (λaddr. P (CLR ? addr)) ∧265 list_addressing_mode_tags_elim ? [[ acc_a ; carry ; bit_addr ]] (λaddr. P (CPL ? addr)) ∧266 P (DA ? ACC_A) ∧267 bitvector_elim 8 (λr. P (JC ? (RELATIVE r))) ∧268 bitvector_elim 8 (λr. P (JNC ? (RELATIVE r))) ∧269 bitvector_elim 8 (λr. P (JZ ? (RELATIVE r))) ∧270 bitvector_elim 8 (λr. P (JNZ ? (RELATIVE r))) ∧271 bitvector_elim 8 (λr. (bitvector_elim 8 (λb: BitVector 8. P (JB ? (BIT_ADDR b) (RELATIVE r))))) ∧272 bitvector_elim 8 (λr. (bitvector_elim 8 (λb: BitVector 8. P (JNB ? (BIT_ADDR b) (RELATIVE r))))) ∧273 bitvector_elim 8 (λr. (bitvector_elim 8 (λb: BitVector 8. P (JBC ? (BIT_ADDR b) (RELATIVE r))))) ∧274 list_addressing_mode_tags_elim ? [[ registr; direct ]] (λaddr. bitvector_elim 8 (λr. P (DJNZ ? addr (RELATIVE r)))) ∧275 P (RL ? ACC_A) ∧276 P (RLC ? ACC_A) ∧277 P (RR ? ACC_A) ∧278 P (RRC ? ACC_A) ∧279 P (SWAP ? ACC_A) ∧280 P (RET ?) ∧281 P (RETI ?) ∧282 P (NOP ?) ∧283 bit_elim (λb. P (XCHD ? ACC_A (INDIRECT b))) ∧284 list_addressing_mode_tags_elim ? [[ carry; bit_addr ]] (λaddr. P (SETB ? addr)) ∧285 bitvector_elim 8 (λaddr. P (PUSH ? (DIRECT addr))) ∧286 bitvector_elim 8 (λaddr. P (POP ? (DIRECT addr))) ∧287 union_elim ? ? (product_elim ? ? [[ acc_a ]] [[ direct; data ]])288 (product_elim ? ? [[ registr; indirect ]] [[ data ]])289 (λd. bitvector_elim 8 (λb. P (CJNE ? d (RELATIVE b)))) ∧290 list_addressing_mode_tags_elim ? [[ registr; direct; indirect ]] (λaddr. P (XCH ? ACC_A addr)) ∧291 union_elim ? ? (product_elim ? ? [[acc_a]] [[ data ; registr ; direct ; indirect ]])292 (product_elim ? ? [[direct]] [[ acc_a ; data ]])293 (λd. P (XRL ? d)) ∧294 union_elim ? ? (union_elim ? ? (product_elim ? ? [[acc_a]] [[ registr ; direct ; indirect ; data ]])295 (product_elim ? ? [[direct]] [[ acc_a ; data ]]))296 (product_elim ? ? [[carry]] [[ bit_addr ; n_bit_addr]])297 (λd. P (ANL ? d)) ∧298 union_elim ? ? (union_elim ? ? (product_elim ? ? [[acc_a]] [[ registr ; data ; direct ; indirect ]])299 (product_elim ? ? [[direct]] [[ acc_a ; data ]]))300 (product_elim ? ? [[carry]] [[ bit_addr ; n_bit_addr]])301 (λd. P (ORL ? d)) ∧302 union_elim ? ? (product_elim ? ? [[acc_a]] [[ ext_indirect ; ext_indirect_dptr ]])303 (product_elim ? ? [[ ext_indirect ; ext_indirect_dptr ]] [[acc_a]])304 (λd. P (MOVX ? d)) ∧305 union_elim ? ? (306 union_elim ? ? (307 union_elim ? ? (308 union_elim ? ? (309 union_elim ? ? (product_elim ? ? [[acc_a]] [[ registr ; direct ; indirect ; data ]])310 (product_elim ? ? [[ registr ; indirect ]] [[ acc_a ; direct ; data ]]))311 (product_elim ? ? [[direct]] [[ acc_a ; registr ; direct ; indirect ; data ]]))312 (product_elim ? ? [[dptr]] [[data16]]))313 (product_elim ? ? [[carry]] [[bit_addr]]))314 (product_elim ? ? [[bit_addr]] [[carry]])315 (λd. P (MOV ? d)).316 %317 qed.318 319 definition instruction_elim: ∀P: instruction → bool. bool ≝320 λP. (*321 bitvector_elim 11 (λx. P (ACALL (ADDR11 x))) ∧322 bitvector_elim 16 (λx. P (LCALL (ADDR16 x))) ∧323 bitvector_elim 11 (λx. P (AJMP (ADDR11 x))) ∧324 bitvector_elim 16 (λx. P (LJMP (ADDR16 x))) ∧ *)325 bitvector_elim 8 (λx. P (SJMP (RELATIVE x))). (* ∧326 P (JMP INDIRECT_DPTR) ∧327 list_addressing_mode_tags_elim ? [[ acc_dptr; acc_pc ]] (λa. P (MOVC ACC_A a)) ∧328 preinstruction_elim (λp. P (RealInstruction p)). *)329 %330 qed.331 332 333 axiom instruction_elim_complete:334 ∀P. instruction_elim P = true → ∀i. P i = true.335 *)336 (*definition eq_instruction ≝337 λi, j: instruction.338 true.*)339 169 340 170 definition eq_addressing_mode: addressing_mode → addressing_mode → bool ≝ -
src/ASM/Status.ma
r2055 r2111 1130 1130 qed. 1131 1131 1132 lemma fetch_pseudo_instruction_vsplit: 1133 ∀instr_list,ppc,ppc_ok. 1134 ∃pre,suff,lbl. 1135 (pre @ [〈lbl,\fst (fetch_pseudo_instruction instr_list ppc ppc_ok)〉]) @ suff = instr_list. 1136 #instr_list #ppc #ppc_ok whd in match (fetch_pseudo_instruction ???); 1137 cases (nth_safe_append … instr_list … ppc_ok) #pre * #suff #EQ %{pre} %{suff} 1138 lapply EQ -EQ cases (nth_safe labelled_instruction ???) #lbl0 #instr normalize nodelta 1139 #EQ %{lbl0} @EQ 1140 qed. 1141 1142 lemma fetch_pseudo_instruction_append: 1143 ∀l1,l2. |l1@l2| ≤ 2^16 → ∀ppc,ppc_ok,ppc_ok'. 1144 let code_newppc ≝ fetch_pseudo_instruction l2 ppc ppc_ok in 1145 fetch_pseudo_instruction (l1@l2) (add … (bitvector_of_nat … (|l1|)) (ppc)) ppc_ok' = 1146 〈\fst code_newppc, add … (bitvector_of_nat … (|l1|)) (\snd code_newppc)〉. 1147 #l1 #l2 #l1l2_ok #ppc #ppc_ok whd in match fetch_pseudo_instruction; normalize nodelta 1148 cut (|l1| + nat_of_bitvector … ppc < 2^16) 1149 [ @(transitive_le … l1l2_ok) >length_append @monotonic_lt_plus_r assumption ] 1150 -l1l2_ok #l1ppc_ok >nat_of_bitvector_add 1151 >nat_of_bitvector_bitvector_of_nat_inverse try assumption 1152 [2,3: @(transitive_le … l1ppc_ok) @le_S_S // ] 1153 #ppc_ok' <nth_safe_prepend try assumption cases (nth_safe labelled_instruction ???) 1154 #lbl #instr normalize nodelta >add_associative % 1155 qed. 1156 1132 1157 definition address_of_word_labels_code_mem ≝ 1133 1158 λcode_mem : list labelled_instruction. -
src/ASM/Util.ma
r2055 r2111 253 253 qed. 254 254 255 (*CSC: practically equal to shift_nth_safe but for commutation 256 of addition. One of the two lemmas should disappear. *) 257 lemma nth_safe_prepend: 258 ∀A,l1,l2,j.∀H:j<|l2|.∀K:|l1|+j<|(l1@l2)|. 259 nth_safe A j l2 H =nth_safe A (|l1|+j) (l1@l2) K. 260 #A #l1 #l2 #j #H >commutative_plus @shift_nth_safe 261 qed. 262 263 lemma nth_safe_cons: 264 ∀A,hd,tl,l2,j,j_ok,Sj_ok. 265 nth_safe A j (tl@l2) j_ok =nth_safe A (1+j) (hd::tl@l2) Sj_ok. 266 // 267 qed. 268 269 lemma eq_nth_safe_proof_irrelevant: 270 ∀A,l,i,i_ok,i_ok'. 271 nth_safe A l i i_ok = nth_safe A l i i_ok'. 272 #A #l #i #i_ok #i_ok' % 273 qed. 274 275 lemma nth_safe_append: 276 ∀A,l,n,n_ok. 277 ∃pre,suff. 278 (pre @ [nth_safe A n l n_ok]) @ suff = l. 279 #A #l elim l normalize 280 [ #n #abs cases (absurd ? abs (not_le_Sn_O ?)) 281 | #hd #tl #IH #n cases n normalize 282 [ #_ %{[]} /2/ 283 | #m #m_ok cases (IH m ?) 284 [ #pre * #suff #EQ %{(hd::pre)} %{suff} <EQ in ⊢ (???%); % | skip ]] 285 qed. 255 286 256 287 definition last_safe ≝ -
src/common/Identifiers.ma
r1949 r2111 80 80 @(eqb_elim x y P) [ /2 by / | * #H @F % #E destruct /2 by / ] 81 81 qed. 82 83 lemma eq_identifier_eq: 84 ∀tag: String. 85 ∀l. 86 ∀r. 87 eq_identifier tag l r = true → l = r. 88 #tag #l #r cases l cases r 89 #pos_l #pos_r 90 cases pos_l cases pos_r 91 [1: 92 #_ % 93 |2,3,4,7: 94 #p1_l normalize in ⊢ (% → ?); 95 #absurd destruct(absurd) 96 |5,9: 97 #p1_l #p1_r normalize in ⊢ (% → ?); 98 #relevant lapply (eqb_true_to_eq … relevant) #EQ >EQ % 99 |*: 100 #p_l #p_r normalize in ⊢ (% → ?); 101 #absurd destruct(absurd) 102 ] 103 qed. 104 105 axiom neq_identifier_neq: 106 ∀tag: String. 107 ∀l, r: identifier tag. 108 eq_identifier tag l r = false → (l = r → False). 82 109 83 110 include "basics/deqsets.ma".
Note: See TracChangeset
for help on using the changeset viewer.