Ignore:
Timestamp:
Jul 30, 2012, 12:46:19 AM (8 years ago)
Author:
sacerdot
Message:
  1. lemmas moved from all files to Test.ma
  2. most of the lemmas in Test.ma repaired. A few are commented out. Several needs to be slightly generalized.
File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/AssemblyProofSplit.ma

    r2272 r2273  
    2020include "ASM/Test.ma".
    2121
    22 lemma addressing_mode_ok_to_map_address_using_internal_pseudo_address_map:
    23   ∀M, cm, ps, sigma, x.
    24   ∀addr1: [[acc_a]].
    25     addressing_mode_ok pseudo_assembly_program M cm ps addr1=true →
    26       map_address_using_internal_pseudo_address_map M sigma SFR_ACC_A x = x.
    27   #M #cm #ps #sigma #x #addr1
    28   @(subaddressing_mode_elim … addr1)
    29   whd in ⊢ (??%? → ??%?);
    30   cases (\snd M)
    31   [1:
    32     //
    33   |2:
    34     #upper_lower #address normalize nodelta #absurd
    35     destruct(absurd)
    36   ]
    37 qed.
    38 
    39 lemma addressing_mode_ok_to_snd_M_data:
    40   ∀M, cm, ps.
    41   ∀addr: [[acc_a]].
    42   addressing_mode_ok pseudo_assembly_program M cm ps addr = true →
    43     \snd M = data.
    44   #M #addr #ps #addr
    45   @(subaddressing_mode_elim … addr)
    46   whd in ⊢ (??%? → ?);
    47   cases (\snd M) normalize nodelta
    48   [2:
    49     * #address #absurd destruct(absurd)
    50   ]
    51   #_ %
    52 qed.
    53 
    54 lemma assoc_list_exists_true_to_assoc_list_lookup_Some:
    55   ∀A, B: Type[0].
    56   ∀e: A.
    57   ∀the_list: list (A × B).
    58   ∀eq_f: A → A → bool.
    59     assoc_list_exists A B e eq_f the_list = true →
    60       ∃e'. assoc_list_lookup A B e eq_f the_list = Some … e'.
    61   #A #B #e #the_list #eq_f elim the_list
    62   [1:
    63     whd in ⊢ (??%? → ?); #absurd destruct(absurd)
    64   |2:
    65     #hd #tl #inductive_hypothesis
    66     whd in ⊢ (??%? → ?); whd in match (assoc_list_lookup ?????);
    67     cases (eq_f (\fst hd) e) normalize nodelta
    68     [1:
    69       #_ %{(\snd hd)} %
    70     |2:
    71       @inductive_hypothesis
    72     ]
    73   ]
    74 qed.
    75 
    76 lemma assoc_list_exists_false_to_assoc_list_lookup_None:
    77   ∀A, B: Type[0].
    78   ∀e, e': A.
    79   ∀the_list, the_list': list (A × B).
    80   ∀eq_f: A → A → bool.
    81     e = e' →
    82     the_list = the_list' →
    83       assoc_list_exists A B e eq_f the_list = false →
    84         assoc_list_lookup A B e' eq_f the_list' = None ….
    85   #A #B #e #e' #the_list elim the_list
    86   [1:
    87     #the_list' #eq_f #e_refl <e_refl #the_list_refl <the_list_refl #_ %
    88   |2:
    89     #hd #tl #inductive_hypothesis #the_list' #eq_f #e_refl #the_list_refl <the_list_refl
    90     whd in ⊢ (??%? → ??%?); <e_refl
    91     cases (eq_f (\fst hd) e) normalize nodelta
    92     [1:
    93       #absurd destruct(absurd)
    94     |2:
    95       >e_refl in ⊢ (? → %); @inductive_hypothesis try % assumption
    96     ]
    97   ]
    98 qed.
    99 
    100 lemma sfr_psw_eq_to_bit_address_of_register_eq:
    101   ∀A: Type[0].
    102   ∀code_memory: A.
    103   ∀status, status', register_address.
    104     get_8051_sfr … status SFR_PSW = get_8051_sfr … status' SFR_PSW →
    105       bit_address_of_register A code_memory status register_address = bit_address_of_register A code_memory status' register_address.
    106   #A #code_memory #status #status' #register_address #sfr_psw_refl
    107   whd in match bit_address_of_register; normalize nodelta
    108   <sfr_psw_refl %
    109 qed.
    110 
    111 lemma sfr_psw_and_low_internal_ram_eq_to_get_register_eq:
    112   ∀A: Type[0].
    113   ∀code_memory: A.
    114   ∀status, status', register_address.
    115     get_8051_sfr … status SFR_PSW = get_8051_sfr … status' SFR_PSW →
    116       low_internal_ram A code_memory status = low_internal_ram A code_memory status' →
    117         get_register A code_memory status register_address = get_register A code_memory status' register_address.
    118   #A #code_memory #status #status' #register_address #sfr_psw_refl #low_internal_ram_refl
    119   whd in match get_register; normalize nodelta <low_internal_ram_refl
    120   >(sfr_psw_eq_to_bit_address_of_register_eq … status status') //
    121 qed.
    122 
    123 lemma map_address_mode_using_internal_pseudo_address_map_ok1_addr:
    124   ∀M', cm, status, status', sigma.
    125   ∀addr1: [[acc_a; registr; direct; indirect; data; ext_indirect; ext_indirect_dptr]]. (* XXX: expand as needed *)
    126     get_8051_sfr … status SFR_PSW = get_8051_sfr … status' SFR_PSW →
    127     addressing_mode_ok pseudo_assembly_program M' cm status addr1 = true →
    128     map_address_mode_using_internal_pseudo_address_map_ok1 M' cm status' sigma addr1.
    129   #M' #cm #status #status' #sigma #addr1 #sfr_refl
    130   @(subaddressing_mode_elim … addr1) try (#w #_ @I)
    131   [1,4: #_ @I ] #w
    132   whd in ⊢ (??%? → %);
    133   inversion (assoc_list_exists ?????) #assoc_list_exists_refl normalize nodelta
    134   [1,3:
    135     #absurd destruct(absurd)
    136   |2,4:
    137     #_
    138     @(assoc_list_exists_false_to_assoc_list_lookup_None … (refl …) … assoc_list_exists_refl)
    139     <(sfr_psw_eq_to_bit_address_of_register_eq … status status') try % assumption
    140   ]
    141 qed.
    142 
     22(*CSC: move elsewhere*)
    14323lemma not_b_c_to_b_not_c:
    14424  ∀b, c: bool.
    14525    (¬b) = c → b = (¬c).
    14626  //
    147 qed.
    148 (* XXX: move above elsewhere *)
    149 
    150 lemma sfr8051_neq_acc_a_to_map_address_using_internal_pseudo_address_map:
    151   ∀M.
    152   ∀sigma.
    153   ∀sfr8051.
    154   ∀b.
    155     sfr8051 ≠ SFR_ACC_A →
    156       map_address_using_internal_pseudo_address_map M sigma sfr8051 b = b.
    157   #M #sigma * #b
    158   [18:
    159     #relevant cases (absurd … (refl ??) relevant)
    160   ]
    161   #_ %
    162 qed.
    163 
    164 lemma w_neq_224_to_map_address_Byte_using_internal_pseudo_address_map:
    165   ∀M.
    166   ∀sigma: Word → Word.
    167   ∀w: BitVector 8.
    168   ∀b.
    169     w ≠ bitvector_of_nat … 224 →
    170       map_address_Byte_using_internal_pseudo_address_map M sigma w b = b.
    171   #M #sigma #w #b #w_neq_assm
    172   whd in ⊢ (??%?); inversion (sfr_of_Byte ?)
    173   [1:
    174     #sfr_of_Byte_refl %
    175   |2:
    176     * #sfr8051 #sfr_of_Byte_refl normalize nodelta try %
    177     @sfr8051_neq_acc_a_to_map_address_using_internal_pseudo_address_map %
    178     #relevant >relevant in sfr_of_Byte_refl; #sfr_of_Byte_refl
    179     @(absurd ?? w_neq_assm)
    180     lapply sfr_of_Byte_refl -b -sfr_of_Byte_refl -relevant -w_neq_assm -sfr8051 -sigma
    181     whd in match sfr_of_Byte; normalize nodelta
    182     cases (eqb ??) normalize nodelta [1: #absurd destruct(absurd) ]
    183     cases (eqb ??) normalize nodelta [1: #absurd destruct(absurd) ]
    184     cases (eqb ??) normalize nodelta [1: #absurd destruct(absurd) ]
    185     cases (eqb ??) normalize nodelta [1: #absurd destruct(absurd) ]
    186     cases (eqb ??) normalize nodelta [1: #absurd destruct(absurd) ]
    187     cases (eqb ??) normalize nodelta [1: #absurd destruct(absurd) ]
    188     cases (eqb ??) normalize nodelta [1: #absurd destruct(absurd) ]
    189     cases (eqb ??) normalize nodelta [1: #absurd destruct(absurd) ]
    190     cases (eqb ??) normalize nodelta [1: #absurd destruct(absurd) ]
    191     cases (eqb ??) normalize nodelta [1: #absurd destruct(absurd) ]
    192     cases (eqb ??) normalize nodelta [1: #absurd destruct(absurd) ]
    193     cases (eqb ??) normalize nodelta [1: #absurd destruct(absurd) ]
    194     cases (eqb ??) normalize nodelta [1: #absurd destruct(absurd) ]
    195     cases (eqb ??) normalize nodelta [1: #absurd destruct(absurd) ]
    196     cases (eqb ??) normalize nodelta [1: #absurd destruct(absurd) ]
    197     cases (eqb ??) normalize nodelta [1: #absurd destruct(absurd) ]
    198     cases (eqb ??) normalize nodelta [1: #absurd destruct(absurd) ]
    199     cases (eqb ??) normalize nodelta [1: #absurd destruct(absurd) ]
    200     cases (eqb ??) normalize nodelta [1: #absurd destruct(absurd) ]
    201     cases (eqb ??) normalize nodelta [1: #absurd destruct(absurd) ]
    202     cases (eqb ??) normalize nodelta [1: #absurd destruct(absurd) ]
    203     cases (eqb ??) normalize nodelta [1: #absurd destruct(absurd) ]
    204     cases (eqb ??) normalize nodelta [1: #absurd destruct(absurd) ]
    205     cases (eqb ??) normalize nodelta [1: #absurd destruct(absurd) ]
    206     @eqb_elim #eqb_refl normalize nodelta [1: #_ <eqb_refl >bitvector_of_nat_inverse_nat_of_bitvector % ]
    207     cases (eqb ??) normalize nodelta [1: #absurd destruct(absurd) ]
    208     #absurd destruct(absurd)
    209 qed.
    210 
    211 lemma assoc_list_exists_false_to_map_internal_ram_address_using_pseudo_address_map:
    212   ∀M, sigma, w, b.
    213     assoc_list_exists Byte (upper_lower×Word) w (eq_bv 8) (\fst  M) = false →
    214       map_internal_ram_address_using_pseudo_address_map M sigma w b = b.
    215   #M #sigma #w #b #assoc_list_exists_assm
    216   whd in ⊢ (??%?);
    217   >(assoc_list_exists_false_to_assoc_list_lookup_None … (refl …) … assoc_list_exists_assm) %
    218 qed.
    219    
    220 lemma addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2:
    221   ∀M', cm.
    222   ∀sigma, status, status', b, b'.
    223   ∀addr1: [[acc_a; registr; direct; indirect; data; bit_addr; ext_indirect; ext_indirect_dptr]]. (* XXX: expand as needed *)
    224     get_8051_sfr … status SFR_PSW = get_8051_sfr … status' SFR_PSW →
    225     low_internal_ram pseudo_assembly_program cm status = low_internal_ram pseudo_assembly_program cm status' →
    226     b = b' →
    227     addressing_mode_ok pseudo_assembly_program M' cm status addr1 = true →
    228       map_address_mode_using_internal_pseudo_address_map_ok2 pseudo_assembly_program M' sigma cm status' addr1 b = b'.
    229   #M' #cm #sigma #status #status' #b #b' #addr1 #sfr_refl #low_internal_ram_refl #b_refl <b_refl
    230   @(subaddressing_mode_elim … addr1)
    231   [1:
    232     whd in ⊢ (??%? → ??%?); cases (\snd M')
    233     [1:
    234       normalize nodelta #_ %
    235     |2:
    236       * #address normalize nodelta #absurd destruct(absurd)
    237     ]
    238   |2,4:
    239     #w whd in ⊢ (??%? → ??%?);
    240     inversion (assoc_list_exists ?????) #assoc_list_exists_refl normalize nodelta
    241     [1,3:
    242       #absurd destruct(absurd)
    243     |2:
    244       #_
    245       <(sfr_psw_eq_to_bit_address_of_register_eq … status status' w … sfr_refl)
    246       >(assoc_list_exists_false_to_assoc_list_lookup_None … (refl …) … assoc_list_exists_refl)
    247       normalize nodelta %
    248     |4:
    249       #assoc_list_exists_assm lapply (not_b_c_to_b_not_c … assoc_list_exists_assm)
    250       -assoc_list_exists_assm #assoc_list_exists_assm
    251       <(sfr_psw_and_low_internal_ram_eq_to_get_register_eq … status status' [[false; false; w]] … sfr_refl low_internal_ram_refl)
    252       >(assoc_list_exists_false_to_assoc_list_lookup_None … (refl …) … assoc_list_exists_assm)
    253       normalize nodelta %
    254     ]
    255   |3:
    256     #w whd in ⊢ (??%? → ??%?);
    257     @eq_bv_elim #eq_bv_refl normalize nodelta
    258     [1:
    259       #assoc_list_exists_assm cases (conjunction_true … assoc_list_exists_assm)
    260       #assoc_list_exists_refl #eq_accumulator_refl
    261       >eq_bv_refl change with (map_address_Byte_using_internal_pseudo_address_map M' sigma (bitvector_of_nat 8 224) b = b)
    262       whd in ⊢ (??%?); >(eq_accumulator_address_map_entry_true_to_eq … eq_accumulator_refl)
    263       %
    264     |2:
    265       #assoc_list_exists_assm
    266       @(vsplit_elim bool ???) #bit_one #seven_bits #bit_one_seven_bits_refl normalize nodelta
    267       cases (Vector_Sn … bit_one) #bit * #tl >(Vector_O … tl) #bit_one_refl >bit_one_refl
    268       <head_head' inversion bit #bit_refl normalize nodelta
    269       >bit_one_refl in bit_one_seven_bits_refl; >bit_refl #w_refl normalize in w_refl;
    270       [1:
    271         @w_neq_224_to_map_address_Byte_using_internal_pseudo_address_map <w_refl assumption
    272       |2:
    273         @assoc_list_exists_false_to_map_internal_ram_address_using_pseudo_address_map
    274         <w_refl @(not_b_c_to_b_not_c … assoc_list_exists_assm)
    275       ]
    276     ]
    277   |5,6,7,8:
    278     #w try #w' %
    279   ]
    280 qed.
    281 
    282 lemma addressing_mode_ok_to_map_bit_address_mode_using_internal_pseudo_address_map_get:
    283   ∀M: internal_pseudo_address_map.
    284   ∀cm: pseudo_assembly_program.
    285   ∀s: PreStatus pseudo_assembly_program cm.
    286   ∀sigma: Word → Word.
    287   ∀addr: [[bit_addr]]. (* XXX: expand as needed *)
    288   ∀f: bool.
    289   addressing_mode_ok pseudo_assembly_program M cm s addr = true →
    290     map_bit_address_mode_using_internal_pseudo_address_map_get M cm s sigma addr f.
    291   #M #cm #s #sigma #addr #f
    292   @(subaddressing_mode_elim … addr) #w
    293   whd in ⊢ (??%? → %);
    294   @(vsplit_elim bool ???) #bit_one #seven_bits #bit_one_seven_bits_refl normalize nodelta
    295   cases (head' bool ??) normalize nodelta
    296   [1:
    297     #eq_accumulator_assm whd in ⊢ (??%?);
    298     cases (sfr_of_Byte ?) try %
    299     * * normalize nodelta try %
    300     whd in ⊢ (??%?);
    301     >(eq_accumulator_address_map_entry_true_to_eq … eq_accumulator_assm) %
    302   |2:
    303     #assoc_list_exists_assm whd in ⊢ (??%?);
    304     >(assoc_list_exists_false_to_assoc_list_lookup_None … (refl …) (not_b_c_to_b_not_c … assoc_list_exists_assm)) %
    305   ]
    306 qed.
    307 
    308 lemma addressing_mode_ok_to_map_bit_address_mode_using_internal_pseudo_address_map_set_1:
    309   ∀M: internal_pseudo_address_map.
    310   ∀cm: pseudo_assembly_program.
    311   ∀s, s': PreStatus pseudo_assembly_program cm.
    312   ∀sigma: Word → Word.
    313   ∀addr: [[bit_addr; carry]]. (* XXX: expand as needed *)
    314   ∀f: bool.
    315   s = s' →
    316   addressing_mode_ok pseudo_assembly_program M cm s addr = true →
    317     map_bit_address_mode_using_internal_pseudo_address_map_set_1 M cm s' sigma addr f.
    318   #M #cm #s #s' #sigma #addr #f #s_refl <s_refl
    319   @(subaddressing_mode_elim … addr) [1: #w ]
    320   whd in ⊢ (??%? → %); [2: #_ @I ]
    321   inversion (vsplit bool 1 7 w) #bit_one #seven_bits #bit_one_seven_bits_refl normalize nodelta
    322   cases (head' bool ??) normalize nodelta
    323   [1:
    324     #eq_accumulator_assm whd in ⊢ (??%?);
    325     cases (sfr_of_Byte ?) try % * * try % normalize nodelta
    326     whd in ⊢ (??%?);
    327     >(eq_accumulator_address_map_entry_true_to_eq … eq_accumulator_assm) %
    328   |2:
    329     #assoc_list_exists_assm whd in ⊢ (??%?);
    330     lapply (not_b_c_to_b_not_c ?? assoc_list_exists_assm) -assoc_list_exists_assm #assoc_list_exists_assm
    331     whd in assoc_list_exists_assm:(???%);
    332     >(assoc_list_exists_false_to_assoc_list_lookup_None … (refl …) assoc_list_exists_assm) %
    333   ]
    334 qed.
    335 
    336 lemma addressing_mode_ok_to_map_bit_address_mode_using_internal_pseudo_address_map_set_2:
    337   ∀M: internal_pseudo_address_map.
    338   ∀cm: pseudo_assembly_program.
    339   ∀s, s': PreStatus pseudo_assembly_program cm.
    340   ∀sigma: Word → Word.
    341   ∀addr: [[bit_addr; carry]]. (* XXX: expand as needed *)
    342   ∀f: bool.
    343   s = s' →
    344   addressing_mode_ok pseudo_assembly_program M cm s addr = true →
    345     map_bit_address_mode_using_internal_pseudo_address_map_set_2 M cm s' sigma addr f.
    346   #M #cm #s #s' #sigma #addr #f #s_refl <s_refl
    347   @(subaddressing_mode_elim … addr) [1: #w ]
    348   whd in ⊢ (??%? → %); [2: #_ @I ]
    349   inversion (vsplit bool 1 7 w) #bit_one #seven_bits #bit_one_seven_bits_refl normalize nodelta
    350   cases (head' bool ??) normalize nodelta
    351   [1:
    352     #eq_accumulator_assm whd in ⊢ (??%?);
    353     cases (sfr_of_Byte ?) try % * * try % normalize nodelta
    354     whd in ⊢ (??%?);
    355     >(eq_accumulator_address_map_entry_true_to_eq … eq_accumulator_assm) %
    356   |2:
    357     #assoc_list_exists_assm whd in ⊢ (??%?);
    358     lapply (not_b_c_to_b_not_c ?? assoc_list_exists_assm) -assoc_list_exists_assm #assoc_list_exists_assm
    359     whd in assoc_list_exists_assm:(???%);
    360     >(assoc_list_exists_false_to_assoc_list_lookup_None … (refl …) assoc_list_exists_assm) %
    361   ]
    36227qed.
    36328 
     
    37136qed.
    37237
     38(*CSC: move elsewhere*)
    37339lemma conjunction_split:
    37440  ∀l, l', r, r': bool.
     
    38854  #n_refl #s_refl #s_refl' <n_refl <s_refl
    38955  cases n normalize nodelta try % #n' <(s_refl' n') %
    390 qed.
    391 
    392 axiom insert_low_internal_ram_of_pseudo_low_internal_ram':
    393   ∀M, M', sigma,cm,s,addr,v,v'.
    394     (∀addr'.
    395       ((false:::addr) = addr' →
    396         map_internal_ram_address_using_pseudo_address_map M sigma (false:::addr) v =
    397         map_internal_ram_address_using_pseudo_address_map M' sigma (false:::addr) v') ∧
    398       ((false:::addr) ≠ addr' →
    399         let 〈callM, accM〉 ≝ M in
    400         let 〈callM', accM'〉 ≝ M' in
    401           accM = accM' ∧
    402             assoc_list_lookup … addr' (eq_bv 8) … callM =
    403               assoc_list_lookup … addr' (eq_bv 8) … callM')) →
    404     insert Byte 7 addr v'
    405       (low_internal_ram_of_pseudo_low_internal_ram M'
    406       (low_internal_ram pseudo_assembly_program cm s)) =
    407     low_internal_ram_of_pseudo_low_internal_ram M
    408       (insert Byte 7 addr v (low_internal_ram pseudo_assembly_program cm s)).
    409 
    410 lemma write_at_stack_pointer_status_of_pseudo_status:
    411   ∀M, M'.
    412   ∀cm.
    413   ∀sigma.
    414   ∀policy.
    415   ∀s, s'.
    416   ∀new_b, new_b'.
    417     map_internal_ram_address_using_pseudo_address_map M sigma (get_8051_sfr pseudo_assembly_program cm s SFR_SP) new_b = new_b' →
    418     status_of_pseudo_status M cm s sigma policy = s' →
    419     write_at_stack_pointer ?? s' new_b' =
    420     status_of_pseudo_status M' cm (write_at_stack_pointer ? cm s new_b) sigma policy.
    421   #M #M' #cm #sigma #policy #s #s' #new_b #new_b'
    422   #new_b_refl #s_refl <new_b_refl <s_refl
    423   whd in match write_at_stack_pointer; normalize nodelta
    424   @pair_elim #nu #nl #nu_nl_refl normalize nodelta
    425   @(pair_replace ?????????? (eq_to_jmeq … nu_nl_refl))
    426   [1:
    427     @eq_f
    428     whd in match get_8051_sfr; normalize nodelta
    429     whd in match sfr_8051_index; normalize nodelta
    430     whd in match status_of_pseudo_status; normalize nodelta
    431     whd in match sfr_8051_of_pseudo_sfr_8051; normalize nodelta
    432     cases (\snd M) [2: * #address ] normalize nodelta
    433     [1,2:
    434       cases (vsplit bool ???) #high #low normalize nodelta
    435       whd in match sfr_8051_index; normalize nodelta
    436       >get_index_v_set_index_miss %
    437       #absurd destruct(absurd)
    438     |3:
    439       %
    440     ]
    441   |2:
    442     @if_then_else_status_of_pseudo_status try %
    443     [2:
    444       @sym_eq <set_low_internal_ram_status_of_pseudo_status
    445       [1:
    446         @eq_f2
    447         [2:
    448           @insert_low_internal_ram_of_pseudo_low_internal_ram'
    449     @sym_eq
    450     [2:
    451       <set_low_internal_ram_status_of_pseudo_status
    452       [1:
    453         @eq_f2
    454         [2:
    455           @sym_eq
    456           >(insert_low_internal_ram_of_pseudo_low_internal_ram … sigma … new_b')
    457           [2:
    458             >new_b_refl
    459     ]
    460   ]
    46156qed.
    46257
Note: See TracChangeset for help on using the changeset viewer.