Changeset 2111


Ignore:
Timestamp:
Jun 26, 2012, 5:30:41 PM (5 years ago)
Author:
sacerdot
Message:

Cleanup: lemmas/theorems/axioms moved to the right places.

Location:
src
Files:
6 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/Arithmetic.ma

    r2108 r2111  
    189189  ∀b: BitVector n.
    190190    bitvector_of_nat n (nat_of_bitvector n b) = b.
     191
     192axiom lt_nat_of_bitvector: ∀n.∀w. nat_of_bitvector n w < 2^n.
    191193
    192194lemma nat_of_bitvector_aux_injective:
     
    689691    add … l r = add … r l.
    690692
     693axiom 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
    691698example add_SO:
    692699  ∀n: nat.
  • src/ASM/Assembly.ma

    r2110 r2111  
    581581    \fst (assembly_1_pseudoinstruction lookup_labels sigma policy ppc (λx.zero …) i).
    582582
    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 normalize
    589  [ #n #abs cases (absurd ? abs (not_le_Sn_O ?))
    590  | #hd #tl #IH #n cases n normalize
    591    [ #_ %{[]} /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 nodelta
    603 #EQ %{lbl0} @EQ
    604 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 r
    616     [1:
    617       #_ %
    618     |2,3:
    619       #l normalize in ⊢ (% → ?); #absurd destruct(absurd)
    620     ]
    621   |2:
    622     #l cases l
    623     [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_f
    630     @inductive_hypothesis @eqb_succ_injective_Pos
    631     assumption
    632   ]
    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 r
    641   #pos_l #pos_r
    642   cases pos_l cases pos_r
    643   [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     #relevant
    651     >(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).
    662583 
    663584(* label_map: identifier ↦ pseudo program counter *)
     
    772693qed.
    773694
    774 
    775 (*CSC: move elsewhere; practically equal to shift_nth_safe but for commutation
    776   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_safe
    781 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 in
    805   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 nodelta
    808  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_add
    811  >nat_of_bitvector_bitvector_of_nat_inverse try assumption
    812  [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 
    817695definition sigma_policy_specification ≝
    818696  λprogram: pseudo_assembly_program.
     
    832710      (  (nat_of_bitvector … ppc < |instr_list| → nat_of_bitvector … pc < nat_of_bitvector … next_pc)
    833711       ∨ (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.
    837712
    838713definition assembly:
  • src/ASM/AssemblyProof.ma

    r2110 r2111  
    33include "ASM/StatusProofs.ma".
    44include 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_internal
    11   (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 with
    15   [ 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 prefix
    20   try (@le_S_to_le assumption)
    21   letin res ≝ (bit ::: prefix)
    22   <minus_S_S >minus_Sn_m
    23   assumption
    24 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_n
    31   <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 #c
    38   cases b cases c normalize nodelta
    39   try (#_ % @I)
    40   #assm destruct %
    41 qed.
    425
    436definition bit_elim: ∀P: bool → bool. bool ≝
     
    6225  try @le_n
    6326  <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 #a
    76   elim p try (normalize >reflex #H %)
    77   #m' #hd #tl #inductive_hypothesis
    78   normalize
    79   cases (eq ??) normalize nodelta
    80   try (#irrelevant %)
    81   @inductive_hypothesis
    8227qed.
    8328
     
    13681  cases v try %
    13782  #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 #v
    149   >(vector_cons_append … h v)
    150   <(vector_cons_empty … ([[h]] @@ v))
    151   @(subvector_multiple_append … eq reflex [[ ]] v ? [[h]])
    15283qed.
    15384
     
    236167  ]
    237168qed.
    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.*)
    339169
    340170definition eq_addressing_mode: addressing_mode → addressing_mode → bool ≝
  • src/ASM/Status.ma

    r2055 r2111  
    11301130qed.
    11311131
     1132lemma 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 ???);
     1137cases (nth_safe_append … instr_list … ppc_ok) #pre * #suff #EQ %{pre} %{suff}
     1138lapply EQ -EQ cases (nth_safe labelled_instruction ???) #lbl0 #instr normalize nodelta
     1139#EQ %{lbl0} @EQ
     1140qed.
     1141
     1142lemma 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 %
     1155qed.
     1156
    11321157definition address_of_word_labels_code_mem ≝
    11331158  λcode_mem : list labelled_instruction.
  • src/ASM/Util.ma

    r2055 r2111  
    253253qed.
    254254
     255(*CSC: practically equal to shift_nth_safe but for commutation
     256  of addition. One of the two lemmas should disappear. *)
     257lemma 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
     261qed.
     262
     263lemma 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//
     267qed.
     268
     269lemma 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' %
     273qed.
     274
     275lemma 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 ]]
     285qed.
    255286
    256287definition last_safe ≝
  • src/common/Identifiers.ma

    r1949 r2111  
    8080@(eqb_elim x y P) [ /2 by / | * #H @F % #E destruct /2 by / ]
    8181qed.
     82
     83lemma 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  ]
     103qed.
     104
     105axiom neq_identifier_neq:
     106  ∀tag: String.
     107  ∀l, r: identifier tag.
     108    eq_identifier tag l r = false → (l = r → False).
    82109
    83110include "basics/deqsets.ma".
Note: See TracChangeset for help on using the changeset viewer.