Ignore:
Timestamp:
Jul 18, 2012, 10:08:37 AM (8 years ago)
Author:
sacerdot
Message:

Shuffling around, suggestions, improvements.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/AssemblyProofSplit.ma

    r2198 r2204  
    161161qed.
    162162
    163 lemma set_flags_status_of_pseudo_status:
    164   ∀M.
    165   ∀sigma.
    166   ∀policy.
    167   ∀code_memory: pseudo_assembly_program.
    168   ∀s: PreStatus ? code_memory.
    169   ∀s'.
    170   ∀b, b': Bit.
    171   ∀opt, opt': option Bit.
    172   ∀c, c': Bit.
    173     b = b' →
    174     opt = opt' →
    175     c = c' →
    176     status_of_pseudo_status M code_memory s sigma policy = s' →
    177       set_flags … s' b opt c =
    178         status_of_pseudo_status M code_memory (set_flags … code_memory s b' opt' c') sigma policy.
    179   #M #sigma #policy #code_memory #s #s' #b #b' #opt #opt' #c #c'
    180   #b_refl #opt_refl #c_refl <b_refl <opt_refl <c_refl #s_refl <s_refl
    181   whd in match status_of_pseudo_status; normalize nodelta
    182   whd in match sfr_8051_of_pseudo_sfr_8051; normalize nodelta
    183   cases (\snd M)
    184   [1:
    185     normalize nodelta %
    186   |2:
    187     * #address normalize nodelta
    188     @(vsplit_elim bool ???) #high #low #high_low_refl normalize nodelta
    189     whd in ⊢ (??%%); cases opt try #opt' normalize nodelta
    190     @split_eq_status try % whd in match (sfr_8051_index ?);
    191     cases daemon
    192   ]
    193 qed.
    194 
    195 lemma get_ac_flag_status_of_pseudo_status:
    196   ∀M: internal_pseudo_address_map.
    197   ∀sigma: Word → Word.
    198   ∀policy: Word → bool.
    199   ∀code_memory: pseudo_assembly_program.
    200   ∀s: PreStatus ? code_memory.
    201   ∀s'.
    202     status_of_pseudo_status M code_memory s sigma policy = s' →
    203       get_ac_flag ?? s' = get_ac_flag ? code_memory s.
    204   #M #sigma #policy #code_memory #s #s' #s_refl <s_refl
    205   whd in match get_ac_flag; normalize nodelta
    206   whd in match status_of_pseudo_status; normalize nodelta
    207   whd in match sfr_8051_of_pseudo_sfr_8051; normalize nodelta
    208   cases (\snd M) try %
    209   * normalize nodelta #address
    210   @(vsplit_elim bool ???) #high #low #high_low_refl normalize nodelta
    211   whd in match sfr_8051_index; normalize nodelta
    212   >get_index_v_set_index_miss [2,4: /2/] %
    213 qed.
    214 
    215 lemma get_cy_flag_status_of_pseudo_status:
    216   ∀M: internal_pseudo_address_map.
    217   ∀sigma: Word → Word.
    218   ∀policy: Word → bool.
    219   ∀code_memory: pseudo_assembly_program.
    220   ∀s: PreStatus ? code_memory.
    221   ∀s'.
    222     status_of_pseudo_status M code_memory s sigma policy = s' →
    223       get_cy_flag ?? s' = get_cy_flag ? code_memory s.
    224   #M #sigma #policy #code_memory #s #s' #s_refl <s_refl
    225   whd in match get_cy_flag; normalize nodelta
    226   whd in match status_of_pseudo_status; normalize nodelta
    227   whd in match sfr_8051_of_pseudo_sfr_8051; normalize nodelta
    228   cases (\snd M) try %
    229   * normalize nodelta #address
    230   @(vsplit_elim bool ???) #high #low #high_low_refl normalize nodelta
    231   whd in match sfr_8051_index; normalize nodelta
    232   >get_index_v_set_index_miss [2,4: /2/] %
    233 qed.
    234 
    235 lemma get_ov_flag_status_of_pseudo_status:
    236   ∀M: internal_pseudo_address_map.
    237   ∀sigma: Word → Word.
    238   ∀policy: Word → bool.
    239   ∀code_memory: pseudo_assembly_program.
    240   ∀s: PreStatus ? code_memory.
    241   ∀s'.
    242     status_of_pseudo_status M code_memory s sigma policy = s' →
    243       get_ov_flag ?? s' = get_ov_flag ? code_memory s.
    244   #M #sigma #policy #code_memory #s #s' #s_refl <s_refl
    245   whd in match get_ov_flag; normalize nodelta
    246   whd in match status_of_pseudo_status; normalize nodelta
    247   whd in match sfr_8051_of_pseudo_sfr_8051; normalize nodelta
    248   cases (\snd M) try %
    249   * normalize nodelta #address
    250   @(vsplit_elim bool ???) #high #low #high_low_refl normalize nodelta
    251   whd in match sfr_8051_index; normalize nodelta
    252   >get_index_v_set_index_miss [2,4: /2/] %
    253 qed.
    254 
    255 lemma match_nat_status_of_pseudo_status:
    256   ∀M, cm, sigma, policy, s, s', s'', s'''.
    257   ∀n, n': nat.
    258     n = n' →
    259     status_of_pseudo_status M cm s' sigma policy = s →
    260     status_of_pseudo_status M cm s''' sigma policy = s'' →
    261       match n with [ O ⇒ s | S n' ⇒ s'' ] =
    262         status_of_pseudo_status M cm (match n' with [ O ⇒ s' | S n'' ⇒ s''']) sigma policy.
    263   #M #cm #sigma #policy #s #s' #s'' #s''' #n #n'
    264   #n_refl #s_refl #s_refl' <n_refl <s_refl <s_refl'
    265   cases n normalize nodelta try % #n' %
    266 qed.
    267 
    268 (* XXX: copied from Test.ma *)
    269 lemma let_pair_in_status_of_pseudo_status:
    270   ∀A, B, M, cm, sigma, policy. ∀c, c': A × B. ∀s, s'.
    271     c = c' →
    272     (∀left, right. status_of_pseudo_status M cm (s left right c') sigma policy = s' left right c') →
    273     let 〈left, right〉 ≝ c' in (s' left right c') =
    274     status_of_pseudo_status M cm (let 〈left, right〉 ≝ c in s left right c) sigma policy.
    275   #A #B #M #cm #sigma #policy * #a #b * #a' #b' #s #s' normalize nodelta //
    276 qed.
    277 
    278 (* XXX: copied from Test.ma *)
    279 lemma let_pair_as_in_status_of_pseudo_status:
    280   ∀A, B, M, cm, sigma, policy. ∀c, c': A × B. ∀s, s'.
    281     c = c' →
    282     (∀left, right, H, H'. status_of_pseudo_status M cm (s left right H c) sigma policy = s' left right H' c') →
    283     let 〈left, right〉 as H' ≝ c' in (s' left right H' c') =
    284     status_of_pseudo_status M cm (let 〈left, right〉 as H ≝ c in s left right H c) sigma policy.
    285   #A #B #M #cm #sigma #policy * #a #b * #a' #b' #s #s' normalize nodelta #destruct_refl
    286   destruct(destruct_refl) /2/
    287 qed.
    288 
    289163lemma match_nat_replace:
    290164  ∀l, o, p, r, o', p': nat.
     
    301175  #l #l' #r #r' #l_refl #r_refl <l_refl <r_refl %
    302176qed.
     177
     178(*
     179lemma match_nat_status_of_pseudo_status:
     180  ∀M, cm, sigma, policy, s, s', s'', s'''.
     181  ∀n, n': nat.
     182    n = n' →
     183    status_of_pseudo_status M cm s' sigma policy = s →
     184    status_of_pseudo_status M cm s''' sigma policy = s'' →
     185      match n with [ O ⇒ s | S n' ⇒ s'' ] =
     186        status_of_pseudo_status M cm (match n' with [ O ⇒ s' | S n'' ⇒ s''']) sigma policy.
     187  #M #cm #sigma #policy #s #s' #s'' #s''' #n #n'
     188  #n_refl #s_refl #s_refl' <n_refl <s_refl <s_refl'
     189  cases n normalize nodelta try % #n' %
     190qed.
     191*)
    303192
    304193lemma main_lemma_preinstruction:
     
    773662      whd in ⊢ (??%?);
    774663      <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm
     664      change with (set_arg_8 ????? = ?)
     665      @set_arg_8_status_of_pseudo_status try %
     666      [ @sym_eq @set_clock_status_of_pseudo_status
     667        [ @sym_eq @set_program_counter_status_of_pseudo_status
     668          [
     669          |
     670          ]
     671        |
     672        ]
     673      |
     674      | @sym_eq
     675      ]
     676cases daemon (*
    775677      whd in ⊢ (??%?); normalize nodelta
    776678      lapply addr_refl @(subaddressing_mode_elim … acc_a) #addr_refl normalize nodelta
     
    836738      ]
    837739    |2:
    838     ]
     740    ]*)]
    839741  |4,5,6,7,8,9: (* INC and DEC *)
    840742    cases daemon
     
    904806    <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm >EQs >EQticks <instr_refl
    905807    whd in ⊢ (??%?);
     808    @let_pair_in_status_of_pseudo_status
     809    [1,3:
     810      @eq_f3
     811      [1,2,4,5:
     812       @sym_eq
     813       [ @(get_arg_8_status_of_pseudo_status) FOO
     814       normalize nodelta >EQs >EQticks <instr_refl %
     815      |3: %
     816      |6: normalize nodelta
     817          @eq_f @eq_f2
     818          [1: >EQs %
     819          |2: >EQticks @eq_f2 <instr_refl try % >EQs %
     820          ]
     821      ]
     822
     823
     824
    906825    @(pair_replace ?????????? p)
    907826    [2,4:
Note: See TracChangeset for help on using the changeset viewer.