Changeset 2273


Ignore:
Timestamp:
Jul 30, 2012, 12:46:19 AM (9 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.
Location:
src/ASM
Files:
4 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

  • src/ASM/AssemblyProofSplitSplit.ma

    r2269 r2273  
    5151qed.
    5252
    53 (*CSC: move elsewhere*)
    54 lemma bv_append_eq_to_eq:
    55  ∀A,n. ∀v1,v2: Vector A n. ∀m. ∀v3,v4: Vector A m.
    56   v1@@v3 = v2@@v4 → v1=v2 ∧ v3=v4.
    57  #A #n #v1 elim v1
    58  [ #v2 >(Vector_O … v2) #m #v3 #v4 normalize * %%
    59  | #n' #hd1 #tl1 #IH #v2 cases (Vector_Sn … v2) #hd2 * #tl2 #EQ2 >EQ2
    60    #m #v3 #v4 #EQ normalize in EQ; destruct(EQ) cases (IH … e0) * * %% ]
    61 qed.
    62    
    6353theorem main_thm:
    6454  ∀M, M': internal_pseudo_address_map.

  • src/ASM/PolicyFront.ma

    r2264 r2273  
    238238    ]
    239239  ].
    240    
     240
    241241(* new safety condition: sigma corresponds to program and resulting program is compact *)
    242242definition sigma_compact ≝

  • src/ASM/Test.ma

    r2272 r2273  
    301301qed.
    302302
    303 (*
    304303lemma get_index_v_status_of_pseudo_status:
    305304  ∀M, code_memory, sigma, policy, s, s', sfr.
    … …  
    316315  whd in match status_of_pseudo_status; normalize nodelta
    317316  whd in match sfr_8051_of_pseudo_sfr_8051; normalize nodelta
    318   inversion (\snd M) try (#upper_lower #address) #sndM_refl normalize nodelta
     317  inversion (\snd M) try ( * #upper_lower #address) #sndM_refl normalize nodelta
    319318 [1:
    320319    cases sfr
    … …  
    326325    %
    327326  |2:
     327   inversion (eq_upper_lower upper_lower upper) #eq_upper_lower_refl normalize nodelta
    328328    @pair_elim #high #low #high_low_refl normalize nodelta
    329     inversion (eq_upper_lower upper_lower upper) #eq_upper_lower_refl normalize nodelta
    330329    cases sfr
    331330    [18,37:
    … …  
    340339  ]
    341340qed.
    342 *)
    343341
    344342lemma set_8051_sfr_status_of_pseudo_status:
    … …  
    350348        (set_8051_sfr pseudo_assembly_program code_memory s sfr v) sigma policy.
    351349  #M #code_memory #sigma #policy #s #s' #sfr #v #v' #s_ok #v_ok
    352   <s_ok whd in ⊢ (??%%); @split_eq_status try % /2/
    353 qed.
    354 
    355 (*
     350  <s_ok whd in ⊢ (??%%); @split_eq_status try % /2 by set_index_status_of_pseudo_status/
     351qed.
     352
     353(*lemma get_8051_sfr_status_of_pseudo_status:
     354  ∀M.
     355  ∀cm, ps, sigma, policy.
     356  ∀sfr.
     357    (sfr = SFR_ACC_A → \snd M = None …) →
     358    get_8051_sfr (BitVectorTrie Byte 16)
     359      (code_memory_of_pseudo_assembly_program cm sigma policy)
     360      (status_of_pseudo_status M cm ps sigma policy) sfr =
     361    get_8051_sfr pseudo_assembly_program cm ps sfr.
     362  #M #cm #ps #sigma #policy * cases M #fstM #sndM #relevant
     363  [18: >relevant % ]
     364  cases sndM try % * #address
     365  whd in match get_8051_sfr;
     366  whd in match status_of_pseudo_status; normalize nodelta
     367  whd in match sfr_8051_of_pseudo_sfr_8051; normalize nodelta #address
     368  cases (eq_upper_lower ??) normalize nodelta
     369  @pair_elim #upper #lower #upper_lower_refl
     370  @get_index_v_set_index_miss @nmk #relevant
     371  normalize in relevant; destruct(relevant)
     372qed.*)
     373
    356374lemma get_8051_sfr_status_of_pseudo_status:
    357375  ∀M, code_memory, sigma, policy, s, s', s'', sfr.
    … …  
    365383  whd in match get_8051_sfr; normalize nodelta
    366384  @get_index_v_status_of_pseudo_status %
    367 qed.*)
     385qed.
    368386
    369387lemma get_8052_sfr_status_of_pseudo_status:
    … …  
    537555   (low_internal_ram pseudo_assembly_program cm s) (zero 8)) = s' →
    538556  lookup Byte 7 addr
    539   (low_internal_ram_of_pseudo_low_internal_ram M
     557  (low_internal_ram_of_pseudo_low_internal_ram M sigma
    540558   (low_internal_ram pseudo_assembly_program cm s)) (zero 8)
    541559  = s'.
    … …  
    549567   (high_internal_ram pseudo_assembly_program cm s) (zero 8)) = s' →
    550568  lookup Byte 7 addr
    551   (high_internal_ram_of_pseudo_high_internal_ram M
     569  (high_internal_ram_of_pseudo_high_internal_ram M sigma
    552570   (high_internal_ram pseudo_assembly_program cm s)) (zero 8)
    553571  = s'.
    … …  
    606624definition map_address_mode_using_internal_pseudo_address_map_ok1 ≝
    607625 λM:internal_pseudo_address_map.λcm.λs:PreStatus ? cm.λsigma. λaddr.
     626  let 〈low,high,accA〉 ≝ M in
    608627  match addr with
    609628  [ INDIRECT i ⇒
    610      assoc_list_lookup ??
    611       (false:::bit_address_of_register pseudo_assembly_program cm s [[false; false; i]]) (eq_bv …) (\fst M) = None …
     629     lookup_opt …
     630      (bit_address_of_register pseudo_assembly_program cm s [[false; false; i]]) low = None …
    612631  | EXT_INDIRECT e ⇒
    613      assoc_list_lookup ??
    614       (false:::bit_address_of_register pseudo_assembly_program cm s [[false; false; e]]) (eq_bv …) (\fst M) = None …
     632     lookup_opt …
     633      (bit_address_of_register pseudo_assembly_program cm s [[false; false; e]]) low = None …
    615634  | ACC_DPTR ⇒
    616635    (* XXX: \snd M = None plus in the very rare case when we are trying to dereference a null (O) pointer
    … …  
    697716                  set_low_internal_ram ?? s memory
    698717              ]
     718             
    699719      | INDIRECT i ⇒
    700720        λindirect: True.
    … …  
    734754    [ >(vsplit_ok … vsplit_refl) #_ @set_bit_addressable_sfr_status_of_pseudo_status
    735755    | #_ #v_ok >(insert_low_internal_ram_status_of_pseudo_status … v) // ]
    736   |3,4: #EQ1 #EQ2 change with (get_register ????) in match register in p;
     756  |3,4: cases M * -M #low #high #accA normalize nodelta
     757      #EQ1 #EQ2 change with (get_register ????) in match register in p;
    737758      >(get_register_status_of_pseudo_status … (refl …) (refl …))
    738759      whd in match map_internal_ram_address_using_pseudo_address_map; normalize nodelta
     760      whd in match (lookup_from_internal_ram ??);
    739761      >EQ1 normalize nodelta >p normalize nodelta >p1 normalize nodelta
    740762      [ >(insert_high_internal_ram_status_of_pseudo_status … v)
    741763      | >(insert_low_internal_ram_status_of_pseudo_status … v) ]
    742764      // <EQ2 @eq_f2 try % <(vsplit_ok … (sym_eq … p)) <eq_cons_head_append >p1 %
    743   |5: #EQ1 #EQ2 <EQ2 >(get_register_status_of_pseudo_status … (refl …) (refl …))
     765  |5: cases M * -M #low #high #accA normalize nodelta
     766      #EQ1 #EQ2 <EQ2 >(get_register_status_of_pseudo_status … (refl …) (refl …))
    744767      whd in match map_internal_ram_address_using_pseudo_address_map; normalize nodelta
     768      whd in match lookup_from_internal_ram; normalize nodelta
    745769      >EQ1 normalize nodelta
    746770      >external_ram_status_of_pseudo_status @set_external_ram_status_of_pseudo_status
    … …  
    957981    #_>p normalize nodelta >p1 normalize nodelta
    958982    @(lookup_low_internal_ram_of_pseudo_low_internal_ram … sigma) %
    959   |3,4:
     983  |3,4: cases M -M * #low #high #accA
    960984    #assoc_list_assm >(get_register_status_of_pseudo_status … (refl …) (refl …))
    961985    whd in match map_internal_ram_address_using_pseudo_address_map in ⊢ (??%?); normalize nodelta
     986    whd in match lookup_from_internal_ram; normalize nodelta
    962987    >assoc_list_assm normalize nodelta >p normalize nodelta >p1 normalize nodelta
    963988    [1:
    964       @(lookup_high_internal_ram_of_pseudo_high_internal_ram … sigma)
     989      @(lookup_high_internal_ram_of_pseudo_high_internal_ram … 〈low,high,accA〉 sigma)
    965990    |2:
    966       @(lookup_low_internal_ram_of_pseudo_low_internal_ram … sigma)
     991      @(lookup_low_internal_ram_of_pseudo_low_internal_ram … 〈low,high,accA〉 sigma)
    967992    ]
    968993    @eq_f2 try % <(vsplit_ok … (sym_eq … p)) <eq_cons_head_append >p1 %
    969   |5:
     994  |5: cases M -M * #low #high #accA
    970995    #assoc_list_assm >(get_register_status_of_pseudo_status … (refl …) (refl …))
    971996    whd in match map_internal_ram_address_using_pseudo_address_map in ⊢ (??%?); normalize nodelta
     997    whd in match lookup_from_internal_ram; normalize nodelta
    972998    >assoc_list_assm normalize nodelta %
    973999  |6,7,8,9:
    9741000    #_ /2 by refl, get_register_status_of_pseudo_status, get_index_v_status_of_pseudo_status/
    975   |10:
     1001  |10: cases M -M * #low #high #accA
    9761002    #acc_a_assm >(get_8051_sfr_status_of_pseudo_status … (refl …) (refl …))
    9771003    >(get_8051_sfr_status_of_pseudo_status … (refl …) (refl …))
    … …  
    9791005    whd in match map_address_using_internal_pseudo_address_map; normalize nodelta
    9801006    >acc_a_assm >p normalize nodelta //
    981   |11:
     1007  |11: cases M -M * #low #high #accA
    9821008    * #map_acc_a_assm #sigma_assm >(get_8051_sfr_status_of_pseudo_status … (refl …) (refl …))
    9831009    >(program_counter_status_of_pseudo_status … (refl …) (refl …))
    … …  
    10481074    match head' … bit_1 with
    10491075    [ true ⇒
    1050       let address ≝ nat_of_bitvector … seven_bits in
    1051       let d ≝ address ÷ 8 in
    1052       let m ≝ address mod 8 in
    1053       let trans ≝ bitvector_of_nat 8 ((d * 8) + 128) in
     1076      let 〈four_bits, three_bits〉 ≝ vsplit bool 4 3 seven_bits in
     1077      let trans ≝ true:::four_bits @@ [[false; false; false]] in
    10541078        map_address_Byte_using_internal_pseudo_address_map M sigma trans (get_bit_addressable_sfr pseudo_assembly_program cm s trans l) = get_bit_addressable_sfr … cm s trans l
    10551079    | false ⇒
    1056       let address ≝ nat_of_bitvector … seven_bits in
    1057       let address' ≝ bitvector_of_nat 7 ((address ÷ 8) + 32) in
     1080      let 〈four_bits, three_bits〉 ≝ vsplit bool 4 3 seven_bits in
     1081      let address' ≝ [[true; false; false]]@@four_bits in
    10581082      let t ≝ lookup … 7 address' (low_internal_ram ?? s) (zero 8) in
    1059         map_internal_ram_address_using_pseudo_address_map M sigma
     1083      map_internal_ram_address_using_pseudo_address_map M sigma
    10601084          (false:::address') t = t
    10611085    ]
    … …  
    10641088    match head' … bit_1 with
    10651089    [ true ⇒
    1066       let address ≝ nat_of_bitvector … seven_bits in
    1067       let d ≝ address ÷ 8 in
    1068       let m ≝ address mod 8 in
    1069       let trans ≝ bitvector_of_nat 8 ((d * 8) + 128) in
     1090      let 〈four_bits, three_bits〉 ≝ vsplit bool 4 3 seven_bits in
     1091      let trans ≝ true:::four_bits @@ [[false; false; false]] in
    10701092        map_address_Byte_using_internal_pseudo_address_map M sigma trans (get_bit_addressable_sfr pseudo_assembly_program cm s trans l) = get_bit_addressable_sfr … cm s trans l
    10711093    | false ⇒
    1072       let address ≝ nat_of_bitvector … seven_bits in
    1073       let address' ≝ bitvector_of_nat 7 ((address ÷ 8) + 32) in
     1094      let 〈four_bits, three_bits〉 ≝ vsplit bool 4 3 seven_bits in
     1095      let address' ≝ [[true; false; false]]@@four_bits in
    10741096      let t ≝ lookup … 7 address' (low_internal_ram ?? s) (zero 8) in
    1075         map_internal_ram_address_using_pseudo_address_map M sigma
     1097      map_internal_ram_address_using_pseudo_address_map M sigma
    10761098          (false:::address') t = t
    10771099    ]
    … …  
    11001122        match head' … bit_1 with
    11011123        [ true ⇒
    1102           let address ≝ nat_of_bitvector … seven_bits in
    1103           let d ≝ address ÷ 8 in
    1104           let m ≝ address mod 8 in
    1105           let trans ≝ bitvector_of_nat 8 ((d * 8) + 128) in
     1124          let 〈four_bits, three_bits〉 ≝ vsplit bool 4 3 seven_bits in
     1125          let trans ≝ true:::four_bits @@ [[false; false; false]] in
    11061126          let sfr ≝ get_bit_addressable_sfr ?? s trans l in
    1107             get_index_v … sfr m ?
     1127            get_index_v … sfr (nat_of_bitvector … three_bits) ?
    11081128        | false ⇒
    1109           let address ≝ nat_of_bitvector … seven_bits in
    1110           let address' ≝ bitvector_of_nat 7 ((address ÷ 8) + 32) in
     1129          let 〈four_bits, three_bits〉 ≝ vsplit bool 4 3 seven_bits in
     1130          let address' ≝ [[true; false; false]]@@four_bits in
    11111131          let t ≝ lookup … 7 address' (low_internal_ram ?? s) (zero 8) in
    1112             get_index_v … t (modulus address 8) ?
     1132            get_index_v … t (nat_of_bitvector … three_bits) ?
    11131133        ]
    11141134      | N_BIT_ADDR n ⇒
    … …  
    11171137        match head' … bit_1 with
    11181138        [ true ⇒
    1119           let address ≝ nat_of_bitvector … seven_bits in
    1120           let d ≝ address ÷ 8 in
    1121           let m ≝ address mod 8 in
    1122           let trans ≝ bitvector_of_nat 8 ((d * 8) + 128) in
     1139          let 〈four_bits, three_bits〉 ≝ vsplit bool 4 3 seven_bits in
     1140          let trans ≝ true:::four_bits @@ [[false; false; false]] in
    11231141          let sfr ≝ get_bit_addressable_sfr ?? s trans l in
    1124             ¬(get_index_v … sfr m ?)
     1142            ¬(get_index_v ?? sfr (nat_of_bitvector … three_bits) ?)
    11251143        | false ⇒
    1126           let address ≝ nat_of_bitvector … seven_bits in
    1127           let address' ≝ bitvector_of_nat 7 ((address ÷ 8) + 32) in
     1144          let 〈four_bits, three_bits〉 ≝ vsplit bool 4 3 seven_bits in
     1145          let address' ≝ [[true; false; false]]@@four_bits in
    11281146          let t ≝ lookup … 7 address' (low_internal_ram ?? s) (zero 8) in
    1129             ¬(get_index_v … t (modulus address 8) ?)
     1147            ¬(get_index_v … t (nat_of_bitvector … three_bits) ?)
    11301148        ]
    11311149      | CARRY ⇒ λcarry: True. get_cy_flag ?? s
    … …  
    11331151        match other in False with [ ]
    11341152      ] (subaddressing_modein … a)) normalize nodelta
    1135   try @modulus_less_than
     1153  [4,5,8,9: //]
    11361154  #M #sigma #policy #s' #s_refl <s_refl
    11371155  [1:
    11381156    #_ >(get_cy_flag_status_of_pseudo_status … (refl …)) %
    11391157  |2,4:
    1140     whd in ⊢ (% → ?); >p normalize nodelta >p1 normalize nodelta
     1158    whd in ⊢ (% → ?); >p normalize nodelta >p1 normalize nodelta destruct >p2
     1159    normalize nodelta
    11411160    >(get_bit_addressable_sfr_status_of_pseudo_status … (refl …) (refl …)) #map_address_assm
    11421161    >map_address_assm %
    11431162  |3,5:
    11441163    whd in ⊢ (% → ?); >p normalize nodelta >p1 normalize nodelta
    1145     whd in match status_of_pseudo_status; normalize nodelta
     1164    whd in match status_of_pseudo_status; normalize nodelta destruct >p2 normalize nodelta
    11461165    >(lookup_low_internal_ram_of_pseudo_low_internal_ram … sigma … (refl …))
    11471166    #map_address_assm >map_address_assm %
    … …  
    11671186qed.
    11681187
     1188(*CSC: daemon
    11691189definition map_bit_address_mode_using_internal_pseudo_address_map_set_1 ≝
    11701190  λM: internal_pseudo_address_map.
    … …  
    13211341  cases (set_arg_1_status_of_pseudo_status' cm ps addr b) #_ #relevant
    13221342  @relevant
    1323 qed.
     1343qed.*)
    13241344
    13251345lemma clock_status_of_pseudo_status:
    … …  
    13441364qed.
    13451365
     1366(*CSC: daemon
    13461367lemma set_flags_status_of_pseudo_status:
    13471368  ∀M.
    … …  
    13671388  [1:
    13681389    normalize nodelta %
    1369   |2:
    1370     * #address normalize nodelta
     1390  |2: ** #address normalize nodelta
    13711391    @(vsplit_elim bool ???) #high #low #high_low_refl normalize nodelta
    13721392    whd in ⊢ (??%%); cases opt try #opt' normalize nodelta
    … …  
    13741394    cases daemon
    13751395  ]
    1376 qed.
     1396qed.*)
    13771397
    13781398lemma get_ac_flag_status_of_pseudo_status:
    … …  
    13891409  whd in match status_of_pseudo_status; normalize nodelta
    13901410  whd in match sfr_8051_of_pseudo_sfr_8051; normalize nodelta
    1391   cases (\snd M) try %
    1392   * normalize nodelta #address
     1411  cases (\snd M) try % normalize nodelta ** normalize nodelta
     1412  #address
    13931413  @(vsplit_elim bool ???) #high #low #high_low_refl normalize nodelta
    13941414  whd in match sfr_8051_index; normalize nodelta
    … …  
    14101430  whd in match sfr_8051_of_pseudo_sfr_8051; normalize nodelta
    14111431  cases (\snd M) try %
    1412   * normalize nodelta #address
     1432  ** normalize nodelta #address
    14131433  @(vsplit_elim bool ???) #high #low #high_low_refl normalize nodelta
    14141434  whd in match sfr_8051_index; normalize nodelta
    … …  
    14161436qed.
    14171437
    1418 lemma get_8051_sfr_status_of_pseudo_status:
    1419   ∀M.
    1420   ∀cm, ps, sigma, policy.
    1421   ∀sfr.
    1422     (sfr = SFR_ACC_A → \snd M = None …) →
    1423     get_8051_sfr (BitVectorTrie Byte 16)
    1424       (code_memory_of_pseudo_assembly_program cm sigma policy)
    1425       (status_of_pseudo_status M cm ps sigma policy) sfr =
    1426     get_8051_sfr pseudo_assembly_program cm ps sfr.
    1427   #M #cm #ps #sigma #policy * cases M #fstM #sndM #relevant
    1428   [18:
    1429      >relevant %
    1430   ]
    1431   cases sndM try % * #address
    1432   whd in match get_8051_sfr;
    1433   whd in match status_of_pseudo_status; normalize nodelta
    1434   whd in match sfr_8051_of_pseudo_sfr_8051; normalize nodelta #address
    1435   cases (eq_upper_lower ??) normalize nodelta
    1436   @pair_elim #upper #lower #upper_lower_refl
    1437   @get_index_v_set_index_miss @nmk #relevant
    1438   normalize in relevant; destruct(relevant)
    1439 qed.
    1440 
     1438(*CSC: useless?
    14411439lemma get_arg_8_pseudo_addressing_mode_ok:
    14421440  ∀M: internal_pseudo_address_map.
    … …  
    14851483  |2:
    14861484    #addressing_mode_ok_refl whd in ⊢ (??%?);
    1487     @pair_elim #nu #nl #nu_nl_refl normalize nodelta cases daemon (*
     1485    @pair_elim #nu #nl #nu_nl_refl normalize nodelta XXX cases daemon (*
    14881486    @pair_elim #ignore #three_bits #ignore_three_bits_refl normalize nodelta
    14891487    inversion (get_index_v bool ????) #get_index_v_refl normalize nodelta
    … …  
    16101608      ]
    16111609    ]
    1612   ] *)
    1613 qed.
     1610  ]
     1611qed.*)*)
     1612
     1613lemma addressing_mode_ok_to_map_address_using_internal_pseudo_address_map:
     1614  ∀M, cm, ps, sigma, x.
     1615  ∀addr1: [[acc_a]].
     1616    assert_data pseudo_assembly_program M cm ps addr1=true →
     1617      map_address_using_internal_pseudo_address_map M sigma SFR_ACC_A x = x.
     1618  #M #cm #ps #sigma #x #addr1
     1619  @(subaddressing_mode_elim … addr1)
     1620  whd in ⊢ (??%? → ??%?); cases M -M * #low #high * [//]
     1621  * #upper_lower #address normalize nodelta #absurd destruct(absurd)
     1622qed.
     1623
     1624lemma addressing_mode_ok_to_snd_M_data:
     1625  ∀M, cm, ps.
     1626  ∀addr: [[acc_a]].
     1627  assert_data pseudo_assembly_program M cm ps addr = true →
     1628    \snd M = None ….
     1629  #M #cm #ps #addr
     1630  @(subaddressing_mode_elim … addr)
     1631  whd in ⊢ (??%? → ?); cases M * #low #high * normalize nodelta
     1632  [ #_ %
     1633  | #addr #abs destruct(abs) ]
     1634qed.
     1635
     1636(*(*CSC: move elsewhere*)
     1637lemma assoc_list_exists_true_to_assoc_list_lookup_Some:
     1638  ∀A, B: Type[0].
     1639  ∀e: A.
     1640  ∀the_list: list (A × B).
     1641  ∀eq_f: A → A → bool.
     1642    assoc_list_exists A B e eq_f the_list = true →
     1643      ∃e'. assoc_list_lookup A B e eq_f the_list = Some … e'.
     1644  #A #B #e #the_list #eq_f elim the_list
     1645  [1:
     1646    whd in ⊢ (??%? → ?); #absurd destruct(absurd)
     1647  |2:
     1648    #hd #tl #inductive_hypothesis
     1649    whd in ⊢ (??%? → ?); whd in match (assoc_list_lookup ?????);
     1650    cases (eq_f (\fst hd) e) normalize nodelta
     1651    [1:
     1652      #_ %{(\snd hd)} %
     1653    |2:
     1654      @inductive_hypothesis
     1655    ]
     1656  ]
     1657qed.
     1658
     1659(*CSC: move elsewhere*)
     1660lemma assoc_list_exists_false_to_assoc_list_lookup_None:
     1661  ∀A, B: Type[0].
     1662  ∀e, e': A.
     1663  ∀the_list, the_list': list (A × B).
     1664  ∀eq_f: A → A → bool.
     1665    e = e' →
     1666    the_list = the_list' →
     1667      assoc_list_exists A B e eq_f the_list = false →
     1668        assoc_list_lookup A B e' eq_f the_list' = None ….
     1669  #A #B #e #e' #the_list elim the_list
     1670  [1:
     1671    #the_list' #eq_f #e_refl <e_refl #the_list_refl <the_list_refl #_ %
     1672  |2:
     1673    #hd #tl #inductive_hypothesis #the_list' #eq_f #e_refl #the_list_refl <the_list_refl
     1674    whd in ⊢ (??%? → ??%?); <e_refl
     1675    cases (eq_f (\fst hd) e) normalize nodelta
     1676    [1:
     1677      #absurd destruct(absurd)
     1678    |2:
     1679      >e_refl in ⊢ (? → %); @inductive_hypothesis try % assumption
     1680    ]
     1681  ]
     1682qed.*)
     1683
     1684lemma sfr_psw_eq_to_bit_address_of_register_eq:
     1685  ∀A: Type[0].
     1686  ∀code_memory: A.
     1687  ∀status, status', register_address.
     1688    get_8051_sfr … status SFR_PSW = get_8051_sfr … status' SFR_PSW →
     1689      bit_address_of_register A code_memory status register_address = bit_address_of_register A code_memory status' register_address.
     1690  #A #code_memory #status #status' #register_address #sfr_psw_refl
     1691  whd in match bit_address_of_register; normalize nodelta
     1692  <sfr_psw_refl %
     1693qed.
     1694
     1695lemma sfr_psw_and_low_internal_ram_eq_to_get_register_eq:
     1696  ∀A: Type[0].
     1697  ∀code_memory: A.
     1698  ∀status, status', register_address.
     1699    get_8051_sfr … status SFR_PSW = get_8051_sfr … status' SFR_PSW →
     1700      low_internal_ram A code_memory status = low_internal_ram A code_memory status' →
     1701        get_register A code_memory status register_address = get_register A code_memory status' register_address.
     1702  #A #code_memory #status #status' #register_address #sfr_psw_refl #low_internal_ram_refl
     1703  whd in match get_register; normalize nodelta <low_internal_ram_refl
     1704  >(sfr_psw_eq_to_bit_address_of_register_eq … status status') //
     1705qed.
     1706
     1707lemma map_address_mode_using_internal_pseudo_address_map_ok1_addr:
     1708  ∀M, cm, status, status', sigma.
     1709  ∀addr1: [[acc_a; registr; direct; indirect; data; ext_indirect; ext_indirect_dptr]]. (* XXX: expand as needed *)
     1710    get_8051_sfr … status SFR_PSW = get_8051_sfr … status' SFR_PSW →
     1711    assert_data pseudo_assembly_program M cm status addr1 = true →
     1712    map_address_mode_using_internal_pseudo_address_map_ok1 M cm status' sigma addr1.
     1713  * * #low #high #accA #cm #status #status' #sigma #addr1 #sfr_refl
     1714  @(subaddressing_mode_elim … addr1) try (#w #_ @I) [1,4: #_ @I ] #w
     1715  whd in ⊢ (??%? → %); whd in match (data_or_address ?????);
     1716  whd in match exists; normalize nodelta
     1717  <(sfr_psw_eq_to_bit_address_of_register_eq … status status') try assumption
     1718  cases (lookup_opt ????); normalize nodelta #x try % #abs destruct(abs)
     1719qed.
     1720
     1721lemma sfr8051_neq_acc_a_to_map_address_using_internal_pseudo_address_map:
     1722  ∀M.
     1723  ∀sigma.
     1724  ∀sfr8051.
     1725  ∀b.
     1726    sfr8051 ≠ SFR_ACC_A →
     1727      map_address_using_internal_pseudo_address_map M sigma sfr8051 b = b.
     1728  #M #sigma * #b
     1729  [18:
     1730    #relevant cases (absurd … (refl ??) relevant)
     1731  ]
     1732  #_ %
     1733qed.
     1734
     1735lemma w_neq_224_to_map_address_Byte_using_internal_pseudo_address_map:
     1736  ∀M.
     1737  ∀sigma: Word → Word.
     1738  ∀w: BitVector 8.
     1739  ∀b.
     1740    w ≠ bitvector_of_nat … 224 →
     1741      map_address_Byte_using_internal_pseudo_address_map M sigma w b = b.
     1742  #M #sigma #w #b #w_neq_assm
     1743  whd in ⊢ (??%?); inversion (sfr_of_Byte ?)
     1744  [1:
     1745    #sfr_of_Byte_refl %
     1746  |2:
     1747    * #sfr8051 #sfr_of_Byte_refl normalize nodelta try %
     1748    @sfr8051_neq_acc_a_to_map_address_using_internal_pseudo_address_map %
     1749    #relevant >relevant in sfr_of_Byte_refl; #sfr_of_Byte_refl
     1750    @(absurd ?? w_neq_assm)
     1751    lapply sfr_of_Byte_refl -b -sfr_of_Byte_refl -relevant -w_neq_assm -sfr8051 -sigma
     1752    whd in match sfr_of_Byte; normalize nodelta
     1753    cases (eqb ??) normalize nodelta [1: #absurd destruct(absurd) ]
     1754    cases (eqb ??) normalize nodelta [1: #absurd destruct(absurd) ]
     1755    cases (eqb ??) normalize nodelta [1: #absurd destruct(absurd) ]
     1756    cases (eqb ??) normalize nodelta [1: #absurd destruct(absurd) ]
     1757    cases (eqb ??) normalize nodelta [1: #absurd destruct(absurd) ]
     1758    cases (eqb ??) normalize nodelta [1: #absurd destruct(absurd) ]
     1759    cases (eqb ??) normalize nodelta [1: #absurd destruct(absurd) ]
     1760    cases (eqb ??) normalize nodelta [1: #absurd destruct(absurd) ]
     1761    cases (eqb ??) normalize nodelta [1: #absurd destruct(absurd) ]
     1762    cases (eqb ??) normalize nodelta [1: #absurd destruct(absurd) ]
     1763    cases (eqb ??) normalize nodelta [1: #absurd destruct(absurd) ]
     1764    cases (eqb ??) normalize nodelta [1: #absurd destruct(absurd) ]
     1765    cases (eqb ??) normalize nodelta [1: #absurd destruct(absurd) ]
     1766    cases (eqb ??) normalize nodelta [1: #absurd destruct(absurd) ]
     1767    cases (eqb ??) normalize nodelta [1: #absurd destruct(absurd) ]
     1768    cases (eqb ??) normalize nodelta [1: #absurd destruct(absurd) ]
     1769    cases (eqb ??) normalize nodelta [1: #absurd destruct(absurd) ]
     1770    cases (eqb ??) normalize nodelta [1: #absurd destruct(absurd) ]
     1771    cases (eqb ??) normalize nodelta [1: #absurd destruct(absurd) ]
     1772    cases (eqb ??) normalize nodelta [1: #absurd destruct(absurd) ]
     1773    cases (eqb ??) normalize nodelta [1: #absurd destruct(absurd) ]
     1774    cases (eqb ??) normalize nodelta [1: #absurd destruct(absurd) ]
     1775    cases (eqb ??) normalize nodelta [1: #absurd destruct(absurd) ]
     1776    cases (eqb ??) normalize nodelta [1: #absurd destruct(absurd) ]
     1777    @eqb_elim #eqb_refl normalize nodelta [1: #_ <eqb_refl >bitvector_of_nat_inverse_nat_of_bitvector % ]
     1778    cases (eqb ??) normalize nodelta [1: #absurd destruct(absurd) ]
     1779    #absurd destruct(absurd)
     1780qed.
     1781
     1782(*lemma assoc_list_exists_false_to_map_internal_ram_address_using_pseudo_address_map:
     1783  ∀M, sigma, w, b.
     1784    assoc_list_exists Byte (upper_lower×Word) w (eq_bv 8) (\fst  M) = false →
     1785      map_internal_ram_address_using_pseudo_address_map M sigma w b = b.
     1786  #M #sigma #w #b #assoc_list_exists_assm
     1787  whd in ⊢ (??%?);
     1788  >(assoc_list_exists_false_to_assoc_list_lookup_None … (refl …) … assoc_list_exists_assm) %
     1789qed.*)
     1790   
     1791lemma addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2:
     1792  ∀M', cm.
     1793  ∀sigma, status, status', b, b'.
     1794  ∀addr1: [[acc_a; registr; direct; indirect; data; bit_addr; ext_indirect; ext_indirect_dptr]]. (* XXX: expand as needed *)
     1795    get_8051_sfr … status SFR_PSW = get_8051_sfr … status' SFR_PSW →
     1796    low_internal_ram pseudo_assembly_program cm status = low_internal_ram pseudo_assembly_program cm status' →
     1797    b = b' →
     1798    assert_data pseudo_assembly_program M' cm status addr1 = true →
     1799      map_address_mode_using_internal_pseudo_address_map_ok2 pseudo_assembly_program M' sigma cm status' addr1 b = b'.
     1800  #M' #cm #sigma #status #status' #b #b' #addr1 #sfr_refl #low_internal_ram_refl #b_refl <b_refl
     1801  @(subaddressing_mode_elim … addr1)
     1802  [1:
     1803    whd in ⊢ (??%? → ??%?); cases M' -M' * #low #high *
     1804    [1:
     1805      normalize nodelta #_ %
     1806    |2:
     1807      * #upper_lower #address normalize nodelta #absurd destruct(absurd)
     1808    ]
     1809  |2: cases M' -M' * #low #high #accA
     1810    #w whd in ⊢ (??%? → ??%?); whd in match (lookup_from_internal_ram ??);
     1811    <(sfr_psw_eq_to_bit_address_of_register_eq … status status' w … sfr_refl)
     1812    cases (lookup_opt ????); normalize nodelta #x try % #abs destruct(abs)
     1813  |4: cases M' -M' * #low #high #accA
     1814    #w whd in ⊢ (??%? → ??%?); whd in match lookup_from_internal_ram;
     1815    whd in match data_or_address; normalize nodelta whd in match exists; normalize nodelta
     1816    whd in match get_register; normalize nodelta
     1817    <(sfr_psw_eq_to_bit_address_of_register_eq … status status' … sfr_refl)
     1818    cases (lookup_opt ????) normalize nodelta [2: #_ #abs destruct(abs)]
     1819    <low_internal_ram_refl @vsplit_elim #one #seven #EQone_seven normalize nodelta
     1820    cases (head' bool ??) normalize nodelta cases (lookup_opt ????) normalize nodelta
     1821    #x try % #abs destruct(abs)
     1822  |3: cases M' -M' * #low #high #accA
     1823    #w whd in ⊢ (??%? → ??%?); whd in match data_or_address; normalize nodelta
     1824    @vsplit_elim #hd #tl #w_refl normalize nodelta
     1825    lapply (eq_head' ?? … hd) >(Vector_O … (tail … hd))
     1826    cases (head' bool ??) normalize nodelta
     1827    [2: #_ whd in match (map_internal_ram_address_using_pseudo_address_map ????);
     1828        whd in match (lookup_from_internal_ram ??); cases (lookup_opt ????);
     1829        normalize nodelta // #x #abs destruct(abs) ] #EQhd
     1830    >w_refl >EQhd @eq_bv_elim #eq_bv_refl normalize nodelta
     1831    [1: cases accA normalize nodelta try (#x #abs destruct(abs)) #_
     1832        normalize in eq_bv_refl; >eq_bv_refl %
     1833    |2: #_ @w_neq_224_to_map_address_Byte_using_internal_pseudo_address_map assumption ]
     1834  |5,6,7,8:
     1835    #w try #w' %
     1836  ]
     1837qed.
     1838
     1839(*CSC: move elsewhere*)
     1840lemma bv_append_eq_to_eq:
     1841 ∀A,n. ∀v1,v2: Vector A n. ∀m. ∀v3,v4: Vector A m.
     1842  v1@@v3 = v2@@v4 → v1=v2 ∧ v3=v4.
     1843 #A #n #v1 elim v1
     1844 [ #v2 >(Vector_O … v2) #m #v3 #v4 normalize * %%
     1845 | #n' #hd1 #tl1 #IH #v2 cases (Vector_Sn … v2) #hd2 * #tl2 #EQ2 >EQ2
     1846   #m #v3 #v4 #EQ normalize in EQ; destruct(EQ) cases (IH … e0) * * %% ]
     1847qed.
     1848
     1849lemma addressing_mode_ok_to_map_bit_address_mode_using_internal_pseudo_address_map_get:
     1850  ∀M: internal_pseudo_address_map.
     1851  ∀cm: pseudo_assembly_program.
     1852  ∀s: PreStatus pseudo_assembly_program cm.
     1853  ∀sigma: Word → Word.
     1854  ∀addr: [[bit_addr]]. (* XXX: expand as needed *)
     1855  ∀f: bool.
     1856  assert_data pseudo_assembly_program M cm s addr = true →
     1857    map_bit_address_mode_using_internal_pseudo_address_map_get M cm s sigma addr f.
     1858  ** #low #high #accA #cm #s #sigma #addr #f
     1859  @(subaddressing_mode_elim … addr) #w
     1860  whd in ⊢ (??%? → %); whd in match data_or_address; normalize nodelta
     1861  @vsplit_elim #bit_one #seven_bits #bit_one_seven_bits_refl normalize nodelta
     1862  @vsplit_elim #four #three #four_three_refl normalize nodelta
     1863  cases (head' bool ??) normalize nodelta
     1864  [1: @eq_bv_elim normalize nodelta
     1865      [1: #EQfour cases accA normalize nodelta #x [2: #abs destruct(abs)] >EQfour %
     1866      |2: #NEQ #_ >w_neq_224_to_map_address_Byte_using_internal_pseudo_address_map
     1867          try % normalize #EQ @(absurd ?? NEQ)
     1868          cases (bv_append_eq_to_eq … [[true]] [[true]] … EQ) #_ #EQ1
     1869          cases (bv_append_eq_to_eq … four [[true;true;false;false]] … EQ1) // ]
     1870  |2: whd in match map_internal_ram_address_using_pseudo_address_map; normalize nodelta
     1871      whd in match lookup_from_internal_ram; normalize nodelta
     1872      cases (lookup_opt ????); normalize nodelta #x try % #abs destruct(abs) ]
     1873qed.
     1874
     1875(*
     1876lemma addressing_mode_ok_to_map_bit_address_mode_using_internal_pseudo_address_map_set_1:
     1877  ∀M: internal_pseudo_address_map.
     1878  ∀cm: pseudo_assembly_program.
     1879  ∀s, s': PreStatus pseudo_assembly_program cm.
     1880  ∀sigma: Word → Word.
     1881  ∀addr: [[bit_addr; carry]]. (* XXX: expand as needed *)
     1882  ∀f: bool.
     1883  s = s' →
     1884  addressing_mode_ok pseudo_assembly_program M cm s addr = true →
     1885    map_bit_address_mode_using_internal_pseudo_address_map_set_1 M cm s' sigma addr f.
     1886  #M #cm #s #s' #sigma #addr #f #s_refl <s_refl
     1887  @(subaddressing_mode_elim … addr) [1: #w ]
     1888  whd in ⊢ (??%? → %); [2: #_ @I ]
     1889  inversion (vsplit bool 1 7 w) #bit_one #seven_bits #bit_one_seven_bits_refl normalize nodelta
     1890  cases (head' bool ??) normalize nodelta
     1891  [1:
     1892    #eq_accumulator_assm whd in ⊢ (??%?);
     1893    cases (sfr_of_Byte ?) try % * * try % normalize nodelta
     1894    whd in ⊢ (??%?);
     1895    >(eq_accumulator_address_map_entry_true_to_eq … eq_accumulator_assm) %
     1896  |2:
     1897    #assoc_list_exists_assm whd in ⊢ (??%?);
     1898    lapply (not_b_c_to_b_not_c ?? assoc_list_exists_assm) -assoc_list_exists_assm #assoc_list_exists_assm
     1899    whd in assoc_list_exists_assm:(???%);
     1900    >(assoc_list_exists_false_to_assoc_list_lookup_None … (refl …) assoc_list_exists_assm) %
     1901  ]
     1902qed.
     1903
     1904lemma addressing_mode_ok_to_map_bit_address_mode_using_internal_pseudo_address_map_set_2:
     1905  ∀M: internal_pseudo_address_map.
     1906  ∀cm: pseudo_assembly_program.
     1907  ∀s, s': PreStatus pseudo_assembly_program cm.
     1908  ∀sigma: Word → Word.
     1909  ∀addr: [[bit_addr; carry]]. (* XXX: expand as needed *)
     1910  ∀f: bool.
     1911  s = s' →
     1912  addressing_mode_ok pseudo_assembly_program M cm s addr = true →
     1913    map_bit_address_mode_using_internal_pseudo_address_map_set_2 M cm s' sigma addr f.
     1914  #M #cm #s #s' #sigma #addr #f #s_refl <s_refl
     1915  @(subaddressing_mode_elim … addr) [1: #w ]
     1916  whd in ⊢ (??%? → %); [2: #_ @I ]
     1917  inversion (vsplit bool 1 7 w) #bit_one #seven_bits #bit_one_seven_bits_refl normalize nodelta
     1918  cases (head' bool ??) normalize nodelta
     1919  [1:
     1920    #eq_accumulator_assm whd in ⊢ (??%?);
     1921    cases (sfr_of_Byte ?) try % * * try % normalize nodelta
     1922    whd in ⊢ (??%?);
     1923    >(eq_accumulator_address_map_entry_true_to_eq … eq_accumulator_assm) %
     1924  |2:
     1925    #assoc_list_exists_assm whd in ⊢ (??%?);
     1926    lapply (not_b_c_to_b_not_c ?? assoc_list_exists_assm) -assoc_list_exists_assm #assoc_list_exists_assm
     1927    whd in assoc_list_exists_assm:(???%);
     1928    >(assoc_list_exists_false_to_assoc_list_lookup_None … (refl …) assoc_list_exists_assm) %
     1929  ]
     1930qed.*)
     1931
     1932(*
     1933axiom insert_low_internal_ram_of_pseudo_low_internal_ram':
     1934  ∀M, M', sigma,cm,s,addr,v,v'.
     1935    (∀addr'.
     1936      ((false:::addr) = addr' →
     1937        map_internal_ram_address_using_pseudo_address_map M sigma (false:::addr) v =
     1938        map_internal_ram_address_using_pseudo_address_map M' sigma (false:::addr) v') ∧
     1939      ((false:::addr) ≠ addr' →
     1940        let 〈callM, accM〉 ≝ M in
     1941        let 〈callM', accM'〉 ≝ M' in
     1942          accM = accM' ∧
     1943            assoc_list_lookup … addr' (eq_bv 8) … callM =
     1944              assoc_list_lookup … addr' (eq_bv 8) … callM')) →
     1945    insert Byte 7 addr v'
     1946      (low_internal_ram_of_pseudo_low_internal_ram M'
     1947      (low_internal_ram pseudo_assembly_program cm s)) =
     1948    low_internal_ram_of_pseudo_low_internal_ram M
     1949      (insert Byte 7 addr v (low_internal_ram pseudo_assembly_program cm s)).
     1950*)
     1951
     1952(*
     1953lemma write_at_stack_pointer_status_of_pseudo_status:
     1954  ∀M, M'.
     1955  ∀cm.
     1956  ∀sigma.
     1957  ∀policy.
     1958  ∀s, s'.
     1959  ∀new_b, new_b'.
     1960    map_internal_ram_address_using_pseudo_address_map M sigma (get_8051_sfr pseudo_assembly_program cm s SFR_SP) new_b = new_b' →
     1961    status_of_pseudo_status M cm s sigma policy = s' →
     1962    write_at_stack_pointer ?? s' new_b' =
     1963    status_of_pseudo_status M' cm (write_at_stack_pointer ? cm s new_b) sigma policy.
     1964  #M #M' #cm #sigma #policy #s #s' #new_b #new_b'
     1965  #new_b_refl #s_refl <new_b_refl <s_refl
     1966  whd in match write_at_stack_pointer; normalize nodelta
     1967  @pair_elim #nu #nl #nu_nl_refl normalize nodelta
     1968  @(pair_replace ?????????? (eq_to_jmeq … nu_nl_refl))
     1969  [1:
     1970    @eq_f
     1971    whd in match get_8051_sfr; normalize nodelta
     1972    whd in match sfr_8051_index; normalize nodelta
     1973    whd in match status_of_pseudo_status; normalize nodelta
     1974    whd in match sfr_8051_of_pseudo_sfr_8051; normalize nodelta
     1975    cases (\snd M) [2: * #address ] normalize nodelta
     1976    [1,2:
     1977      cases (vsplit bool ???) #high #low normalize nodelta
     1978      whd in match sfr_8051_index; normalize nodelta
     1979      >get_index_v_set_index_miss %
     1980      #absurd destruct(absurd)
     1981    |3:
     1982      %
     1983    ]
     1984  |2:
     1985    @if_then_else_status_of_pseudo_status try %
     1986    [2:
     1987      @sym_eq <set_low_internal_ram_status_of_pseudo_status
     1988      [1:
     1989        @eq_f2
     1990        [2:
     1991          @insert_low_internal_ram_of_pseudo_low_internal_ram'
     1992    @sym_eq
     1993    [2:
     1994      <set_low_internal_ram_status_of_pseudo_status
     1995      [1:
     1996        @eq_f2
     1997        [2:
     1998          @sym_eq
     1999          >(insert_low_internal_ram_of_pseudo_low_internal_ram … sigma … new_b')
     2000          [2:
     2001            >new_b_refl
     2002    ]
     2003  ]
     2004qed.*)
Note: See TracChangeset for help on using the changeset viewer.