Changeset 2112


Ignore:
Timestamp:
Jun 26, 2012, 11:47:52 PM (5 years ago)
Author:
sacerdot
Message:

WARNING: this commit may break some code.

  • dead/useless code removed
File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/AssemblyProof.ma

    r2111 r2112  
    33include "ASM/StatusProofs.ma".
    44include alias "arithmetics/nat.ma".
    5 
    6 definition bit_elim: ∀P: bool → bool. bool ≝
    7   λP.
    8     P true ∧ P false.
    9 
    10 let rec bitvector_elim_internal
    11   (n: nat) (P: BitVector n → bool) (m: nat)
    12     on m:
    13       m ≤ n → BitVector (n - m) → bool ≝
    14   match m return λm. m ≤ n → BitVector (n - m) → bool with
    15   [ O    ⇒ λprf1. λprefix. P ?
    16   | S n' ⇒ λprf2. λprefix. bit_elim (λbit. bitvector_elim_internal n P n' ? ?)
    17   ].
    18   /2/
    19 qed.
    20 
    21 definition bitvector_elim ≝
    22   λn: nat.
    23   λP: BitVector n → bool.
    24     bitvector_elim_internal n P n ? ?.
    25   try @le_n
    26   <minus_n_n @[[]]
    27 qed.
    285
    296lemma mem_monotonic_wrt_append:
     
    11390    @(is_in_monotonic_wrt_append … ([[hd']]@@tl) [[hd]] to_search)
    11491    assumption
    115   ]
    116 qed.
    117  
    118 let rec list_addressing_mode_tags_elim
    119   (n: nat) (l: Vector addressing_mode_tag (S n))
    120     on l: (l → bool) → bool ≝
    121   match l return λx.
    122     match x with
    123     [ O ⇒ λl: Vector … O. bool
    124     | S x' ⇒ λl: Vector addressing_mode_tag (S x'). (l → bool) → bool
    125     ] with
    126   [ VEmpty      ⇒  true 
    127   | VCons len hd tl ⇒ λP.
    128     let process_hd ≝
    129       match hd return λhd. ∀P: hd:::tl → bool. bool with
    130       [ direct ⇒ λP.bitvector_elim 8 (λx. P (DIRECT x))
    131       | indirect ⇒ λP.bit_elim (λx. P (INDIRECT x))
    132       | ext_indirect ⇒ λP.bit_elim (λx. P (EXT_INDIRECT x))
    133       | registr ⇒ λP.bitvector_elim 3 (λx. P (REGISTER x))
    134       | acc_a ⇒ λP.P ACC_A
    135       | acc_b ⇒ λP.P ACC_B
    136       | dptr ⇒ λP.P DPTR
    137       | data ⇒ λP.bitvector_elim 8 (λx. P (DATA x))
    138       | data16 ⇒ λP.bitvector_elim 16 (λx. P (DATA16 x))
    139       | acc_dptr ⇒ λP.P ACC_DPTR
    140       | acc_pc ⇒ λP.P ACC_PC
    141       | ext_indirect_dptr ⇒ λP.P EXT_INDIRECT_DPTR
    142       | indirect_dptr ⇒ λP.P INDIRECT_DPTR
    143       | carry ⇒ λP.P CARRY
    144       | bit_addr ⇒ λP.bitvector_elim 8 (λx. P (BIT_ADDR x))
    145       | n_bit_addr ⇒ λP.bitvector_elim 8 (λx. P (N_BIT_ADDR x))
    146       | relative ⇒ λP.bitvector_elim 8 (λx. P (RELATIVE x))
    147       | addr11 ⇒ λP.bitvector_elim 11 (λx. P (ADDR11 x))
    148       | addr16 ⇒ λP.bitvector_elim 16 (λx. P (ADDR16 x))
    149       ]
    150     in
    151       andb (process_hd P)
    152        (match len return λx. x = len → bool with
    153          [ O ⇒ λprf. true
    154          | S y ⇒ λprf. list_addressing_mode_tags_elim y ? P ] (refl ? len))
    155   ].
    156   try %
    157   [2:
    158     cases (sym_eq ??? prf); assumption
    159   |1:
    160     generalize in match H; generalize in match tl;
    161     destruct #tl
    162     normalize in ⊢ (∀_: %. ?);
    163     #H
    164     whd normalize in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ?]);
    165     cases (is_a hd (subaddressing_modeel y tl H))
    166     whd try @I normalize nodelta //
    16792  ]
    16893qed.
     
    675600qed.
    676601
    677 let rec vect_member
    678   (A: Type[0]) (n: nat) (eq: A → A → bool) (v: Vector A n) (a: A)
    679     on v: bool ≝
    680   match v with
    681   [ VEmpty          ⇒ false
    682   | VCons len hd tl ⇒
    683       eq hd a ∨ (vect_member A ? eq tl a)
    684   ].
    685 
    686 let rec list_addressing_mode_tags_elim_prop
    687   (n: nat)
    688   (l: Vector addressing_mode_tag (S n))
    689   on l:
    690   ∀P: l → Prop.
    691   ∀direct_a. ∀indirect_a. ∀ext_indirect_a. ∀register_a. ∀acc_a_a.
    692   ∀acc_b_a. ∀dptr_a. ∀data_a. ∀data16_a. ∀acc_dptr_a. ∀acc_pc_a.
    693   ∀ext_indirect_dptr_a. ∀indirect_dptr_a. ∀carry_a. ∀bit_addr_a.
    694   ∀n_bit_addr_a. ∀relative_a. ∀addr11_a. ∀addr16_a.
    695   ∀x: l. P x ≝
    696   match l return
    697     λy.
    698       match y with
    699       [ O    ⇒ λm: Vector addressing_mode_tag O. ∀prf: 0 = S n. True
    700       | S y' ⇒ λl: Vector addressing_mode_tag (S y'). ∀prf: S y' = S n.∀P:l → Prop.
    701                ∀direct_a: if vect_member … eq_a l direct then ∀x. P (DIRECT x) else True.
    702                ∀indirect_a: if vect_member … eq_a l indirect then ∀x. P (INDIRECT x) else True.
    703                ∀ext_indirect_a: if vect_member … eq_a l ext_indirect then ∀x. P (EXT_INDIRECT x) else True.
    704                ∀register_a: if vect_member … eq_a l registr then ∀x. P (REGISTER x) else True.
    705                ∀acc_a_a: if vect_member … eq_a l acc_a then P (ACC_A) else True.
    706                ∀acc_b_a: if vect_member … eq_a l acc_b then P (ACC_B) else True.
    707                ∀dptr_a: if vect_member … eq_a l dptr then P DPTR else True.
    708                ∀data_a: if vect_member … eq_a l data then ∀x. P (DATA x) else True.
    709                ∀data16_a: if vect_member … eq_a l data16 then ∀x. P (DATA16 x) else True.
    710                ∀acc_dptr_a: if vect_member … eq_a l acc_dptr then P ACC_DPTR else True.
    711                ∀acc_pc_a: if vect_member … eq_a l acc_pc then P ACC_PC else True.
    712                ∀ext_indirect_dptr_a: if vect_member … eq_a l ext_indirect_dptr then P EXT_INDIRECT_DPTR else True.
    713                ∀indirect_dptr_a: if vect_member … eq_a l indirect_dptr then P INDIRECT_DPTR else True.
    714                ∀carry_a: if vect_member … eq_a l carry then P CARRY else True.
    715                ∀bit_addr_a: if vect_member … eq_a l bit_addr then ∀x. P (BIT_ADDR x) else True.
    716                ∀n_bit_addr_a: if vect_member … eq_a l n_bit_addr then ∀x. P (N_BIT_ADDR x) else True.
    717                ∀relative_a: if vect_member … eq_a l relative then ∀x. P (RELATIVE x) else True.
    718                ∀addr11_a: if vect_member … eq_a l addr11 then ∀x. P (ADDR11 x) else True.
    719                ∀addr_16_a: if vect_member … eq_a l addr16 then ∀x. P (ADDR16 x) else True.
    720                ∀x:l. P x
    721       ] with
    722   [ VEmpty          ⇒ λAbsurd. ⊥
    723   | VCons len hd tl ⇒ λProof. ?
    724   ] (refl ? (S n)). cases daemon. qed. (*
    725   [ destruct(Absurd)
    726   | # A1 # A2 # A3 # A4 # A5 # A6 # A7
    727     # A8 # A9 # A10 # A11 # A12 # A13 # A14
    728     # A15 # A16 # A17 # A18 # A19 # X
    729     cases X
    730     # SUB cases daemon ] qed.
    731     cases SUB
    732     [ # BYTE
    733     normalize
    734   ].
    735  
    736  
    737 (*    let prepare_hd ≝
    738       match hd with
    739       [ direct ⇒ λdirect_prf. ?
    740       | indirect ⇒ λindirect_prf. ?
    741       | ext_indirect ⇒ λext_indirect_prf. ?
    742       | registr ⇒ λregistr_prf. ?
    743       | acc_a ⇒ λacc_a_prf. ?
    744       | acc_b ⇒ λacc_b_prf. ?
    745       | dptr ⇒ λdptr_prf. ?
    746       | data ⇒ λdata_prf. ?
    747       | data16 ⇒ λdata16_prf. ?
    748       | acc_dptr ⇒ λacc_dptr_prf. ?
    749       | acc_pc ⇒ λacc_pc_prf. ?
    750       | ext_indirect_dptr ⇒ λext_indirect_prf. ?
    751       | indirect_dptr ⇒ λindirect_prf. ?
    752       | carry ⇒ λcarry_prf. ?
    753       | bit_addr ⇒ λbit_addr_prf. ?
    754       | n_bit_addr ⇒ λn_bit_addr_prf. ?
    755       | relative ⇒ λrelative_prf. ?
    756       | addr11 ⇒ λaddr11_prf. ?
    757       | addr16 ⇒ λaddr16_prf. ?
    758       ]
    759     in ? *)
    760   ].
    761   [ 1: destruct(absd)
    762   | 2: # A1 # A2 # A3 # A4 # A5 # A6
    763        # A7 # A8 # A9 # A10 # A11 # A12
    764        # A13 # A14 # A15 # A16 # A17 # A18
    765        # A19 *
    766   ].
    767 
    768 
    769   match l return λx.match x with [O ⇒ λl: Vector … O. bool | S x' ⇒ λl: Vector addressing_mode_tag (S x').
    770    (l → bool) → bool ] with
    771   [ VEmpty      ⇒  true 
    772   | VCons len hd tl ⇒ λP.
    773     let process_hd ≝
    774       match hd return λhd. ∀P: hd:::tl → bool. bool with
    775       [ direct ⇒ λP.bitvector_elim 8 (λx. P (DIRECT x))
    776       | indirect ⇒ λP.bit_elim (λx. P (INDIRECT x))
    777       | ext_indirect ⇒ λP.bit_elim (λx. P (EXT_INDIRECT x))
    778       | registr ⇒ λP.bitvector_elim 3 (λx. P (REGISTER x))
    779       | acc_a ⇒ λP.P ACC_A
    780       | acc_b ⇒ λP.P ACC_B
    781       | dptr ⇒ λP.P DPTR
    782       | data ⇒ λP.bitvector_elim 8 (λx. P (DATA x))
    783       | data16 ⇒ λP.bitvector_elim 16 (λx. P (DATA16 x))
    784       | acc_dptr ⇒ λP.P ACC_DPTR
    785       | acc_pc ⇒ λP.P ACC_PC
    786       | ext_indirect_dptr ⇒ λP.P EXT_INDIRECT_DPTR
    787       | indirect_dptr ⇒ λP.P INDIRECT_DPTR
    788       | carry ⇒ λP.P CARRY
    789       | bit_addr ⇒ λP.bitvector_elim 8 (λx. P (BIT_ADDR x))
    790       | n_bit_addr ⇒ λP.bitvector_elim 8 (λx. P (N_BIT_ADDR x))
    791       | relative ⇒ λP.bitvector_elim 8 (λx. P (RELATIVE x))
    792       | addr11 ⇒ λP.bitvector_elim 11 (λx. P (ADDR11 x))
    793       | addr16 ⇒ λP.bitvector_elim 16 (λx. P (ADDR16 x))
    794       ]
    795     in
    796       andb (process_hd P)
    797        (match len return λx. x = len → bool with
    798          [ O ⇒ λprf. true
    799          | S y ⇒ λprf. list_addressing_mode_tags_elim y ? P ] (refl ? len))
    800   ].
    801   try %
    802   [ 2: cases (sym_eq ??? prf); @tl
    803   | generalize in match H; generalize in match tl; cases prf;
    804     (* cases prf in tl H; : ??? WAS WORKING BEFORE *)
    805     #tl
    806     normalize in ⊢ (∀_: %. ?)
    807     # H
    808     whd
    809     normalize in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ?])
    810     cases (is_a hd (subaddressing_modeel y tl H)) whd // ]
    811 qed.
    812 *)
     602(*CSC: in is_a_to_mem_to_is_in use vect_member in place of mem … *)
     603definition vect_member ≝
     604 λA,n,eq,v,a. mem A eq (S n) v a.
     605
     606definition tech_if_vect_member ≝
     607 λn,l,am,H.
     608  bool_inv_rect_Type0 (vect_member … n … eq_a l am) ? H (λ_.True).
     609
     610definition is_in_cons_elim:
     611 ∀len.∀hd,tl.∀m:addressing_mode
     612  .is_in (S len) (hd:::tl) m →
     613    (bool_to_Prop (is_a hd m)) ∨ (bool_to_Prop (is_in len tl m)).
     614 #len #hd #tl #am #ISIN whd in match (is_in ???) in ISIN;
     615 cases (is_a hd am) in ISIN; /2/
     616qed.
    813617
    814618definition load_code_memory_aux ≝
     
    960764qed.
    961765
    962 (*
    963 lemma vsplit_prod_exists:
    964   ∀A, m, n.
    965   ∀p: Vector A (m + n).
    966   ∃v: Vector A m.
    967   ∃q: Vector A n.
    968     〈v, q〉 = vsplit A m n p.
    969   #A #m #n #p
    970   elim m
    971   @ex_intro
    972   [1:
    973   |2: @ex_intro
    974       [1:
    975       |2:
    976       ]
    977   ]
    978 *)
    979 
    980766definition vsplit_elim:
    981767  ∀A: Type[0].
     
    993779qed.
    994780
    995 (*
    996 axiom not_eqvb_S:
    997  ∀pc.
    998  (¬eq_bv 16 (bitvector_of_nat 16 pc) (bitvector_of_nat 16 (S pc))).
    999 
    1000 axiom not_eqvb_SS:
    1001  ∀pc.
    1002  (¬eq_bv 16 (bitvector_of_nat 16 pc) (bitvector_of_nat 16 (S (S pc)))).
    1003  
    1004 axiom bitvector_elim_complete:
    1005  ∀n,P. bitvector_elim n P = true → ∀bv. P bv.
    1006 
    1007 lemma bitvector_elim_complete':
    1008  ∀n,P. bitvector_elim n P = true → ∀bv. P bv = true.
    1009  #n #P #H generalize in match (bitvector_elim_complete … H) #K #bv
    1010  generalize in match (K bv) normalize cases (P bv) normalize // #abs @⊥ //
    1011 qed.
    1012 *)
    1013 
    1014 (*
    1015 lemma andb_elim':
    1016  ∀b1,b2. (b1 = true) → (b2 = true) → (b1 ∧ b2) = true.
    1017  #b1 #b2 #H1 #H2 @andb_elim cases b1 in H1; normalize //
    1018 qed.
    1019 *)
    1020 
    1021781let rec encoding_check
    1022782  (code_memory: BitVectorTrie Byte 16) (pc: Word) (final_pc: Word)
     
    1030790  ].
    1031791
    1032 axiom add_commutative:
    1033   ∀n: nat.
    1034   ∀l, r: BitVector n.
    1035     add n l r = add n r l.
    1036 
    1037 axiom add_bitvector_of_nat_Sm:
     792lemma add_bitvector_of_nat_Sm:
    1038793  ∀n, m: nat.
    1039794    add … (bitvector_of_nat … 1) (bitvector_of_nat … m) =
    1040795      bitvector_of_nat n (S m).
     796 #n #m @add_bitvector_of_nat_plus
     797qed.
    1041798
    1042799lemma encoding_check_append:
     
    1164921 [16,20,29: * * |18,19: * * [1,2,4,5: *] |28: * * [1,2: * [1,2: * [1,2: * [1,2: *]]]]]
    1165922 [47,48,49:
    1166  |*: #arg @(list_addressing_mode_tags_elim_prop … arg) whd try % -arg
    1167   [2,3,5,7,10,12,16,17,18,21,25,26,27,30,31,32,37,38,39,40,41,42,43,44,45,48,51,58,
     923 |*: #arg @(subaddressing_mode_elim … arg)
     924  [2,3,5,7,10,12,16,17,18,21,26,27,28,31,32,33,37,38,39,40,41,42,43,44,45,48,51,58,
    1168925   59,60,63,64,65,66,67: #ARG]]
    1169926 [4,5,6,7,8,9,10,11,12,13,22,23,24,27,28,39,40,41,42,43,44,45,46,47,48,49,50,51,52,
    1170   56,57,69,70,72,73,75: #arg2 @(list_addressing_mode_tags_elim_prop … arg2) whd try % -arg2
    1171   [1,2,4,7,9,10,12,13,15,16,17,18,20,22,23,24,25,26,27,28,29,30,31,32,33,36,37,38,
     927  56,57,69,70,72: #arg2 @(subaddressing_mode_elim … arg2)
     928  [1,2,4,7,9,11,12,14,15,17,18,19,20,22,23,24,25,26,27,28,29,30,31,32,33,36,37,38,
    1172929   39,40,41,42,43,44,45,46,47,48,49,50,51,52,53,54,55,56,57,58,59,60,61,62,63,64,65,
    1173930   68,69,70,71: #ARG2]]
    1174  [1,2,19,20: #arg3 @(list_addressing_mode_tags_elim_prop … arg3) whd try % -arg3 #ARG3]
     931 [1,2,19,20: #arg3 @(subaddressing_mode_elim … arg3) #ARG3]
    1175932 normalize in ⊢ (???% → ?);
    1176933 [92,94,42,93,95: @vsplit_elim #vl #vm #E >E -E; [2,4: @(bitvector_3_elim_prop … vl)]
     
    1178935 #H >H * #H1 try (whd in ⊢ (% → ?); * #H2)
    1179936 try (whd in ⊢ (% → ?); * #H3) whd in ⊢ (% → ?); #H4
     937 XXX
    1180938 [ whd in match fetch; normalize nodelta <H1 ] cases daemon
    1181939(*
Note: See TracChangeset for help on using the changeset viewer.