Changeset 2204


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

Shuffling around, suggestions, improvements.

Location:
src/ASM
Files:
2 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:
  • src/ASM/Test.ma

    r2196 r2204  
    44include alias "arithmetics/nat.ma".
    55include "ASM/AssemblyProof.ma".
     6
     7lemma let_pair_in_status_of_pseudo_status:
     8  ∀A, B, M, cm, sigma, policy. ∀c, c': A × B. ∀s, s'.
     9    c = c' →
     10    (∀left, right. status_of_pseudo_status M cm (s left right c') sigma policy = s' left right c') →
     11    (let 〈left, right〉 ≝ c' in s' left right c') =
     12    status_of_pseudo_status M cm (let 〈left, right〉 ≝ c in s left right c) sigma policy.
     13  #A #B #M #cm #sigma #policy * #a #b * #a' #b' #s #s' normalize nodelta //
     14qed.
     15
     16lemma let_pair_as_in_status_of_pseudo_status:
     17  ∀A, B, M, cm, sigma, policy. ∀c, c': A × B. ∀s, s'.
     18    c = c' →
     19    (∀left, right, H, H'. status_of_pseudo_status M cm (s left right H c) sigma policy = s' left right H' c') →
     20    (let 〈left, right〉 as H' ≝ c' in s' left right H' c') =
     21    status_of_pseudo_status M cm (let 〈left, right〉 as H ≝ c in s left right H c) sigma policy.
     22  #A #B #M #cm #sigma #policy * #a #b * #a' #b' #s #s' normalize nodelta #destruct_refl
     23  destruct(destruct_refl) /2/
     24qed.
     25
     26lemma if_then_else_status_of_pseudo_status:
     27  ∀M: internal_pseudo_address_map.
     28  ∀cm: pseudo_assembly_program.
     29  ∀sigma: Word → Word.
     30  ∀policy: Word → bool.
     31  ∀s, s', s'', s'''.
     32  ∀t, t': bool.
     33    t = t' →
     34    status_of_pseudo_status M cm s sigma policy = s' →
     35    status_of_pseudo_status M cm s'' sigma policy = s''' →
     36      if t then
     37        s'
     38      else
     39        s''' =
     40      status_of_pseudo_status M cm (if t' then s else s'') sigma policy.
     41  #M #cm #sigma #policy #s #s' #s'' #s''' #t #t' #t_refl #s_refl
     42  >t_refl normalize nodelta >s_refl cases t' normalize nodelta //
     43qed.
    644
    745lemma set_program_counter_status_of_pseudo_status:
     
    2058  #M #cm #sigma #policy #s #s' #new_ppc #new_ppc'
    2159  #new_ppc_refl #s_refl <new_ppc_refl <s_refl //
    22 qed.
    23 
    24 lemma if_then_else_status_of_pseudo_status_true:
    25   ∀M: internal_pseudo_address_map.
    26   ∀cm: pseudo_assembly_program.
    27   ∀sigma: Word → Word.
    28   ∀policy: Word → bool.
    29   ∀s, s', s'', s'''.
    30   ∀t: bool.
    31     t = true →
    32     status_of_pseudo_status M cm s sigma policy = s' →
    33       if t then
    34         s'
    35       else
    36         s'' =
    37       status_of_pseudo_status M cm (if t then s else s''') sigma policy.
    38   #M #cm #sigma #policy #s #s' #s'' #s''' #t #t_refl #s_refl
    39   >t_refl normalize nodelta >s_refl %
    40 qed.
    41 
    42 lemma if_then_else_status_of_pseudo_status_false:
    43   ∀M: internal_pseudo_address_map.
    44   ∀cm: pseudo_assembly_program.
    45   ∀sigma: Word → Word.
    46   ∀policy: Word → bool.
    47   ∀s, s', s'', s'''.
    48   ∀t: bool.
    49     t = false →
    50     status_of_pseudo_status M cm s sigma policy = s' →
    51       if t then
    52         s''
    53       else
    54         s' =
    55       status_of_pseudo_status M cm (if t then s''' else s) sigma policy.
    56   #M #cm #sigma #policy #s #s' #s'' #s''' #t #t_refl #s_refl
    57   >t_refl normalize nodelta >s_refl %
    5860qed.
    5961
     
    13011303qed.
    13021304
    1303 lemma let_pair_in_status_of_pseudo_status:
    1304   ∀A, B, M, cm, sigma, policy. ∀c, c': A × B. ∀s, s'.
     1305lemma set_flags_status_of_pseudo_status:
     1306  ∀M.
     1307  ∀sigma.
     1308  ∀policy.
     1309  ∀code_memory: pseudo_assembly_program.
     1310  ∀s: PreStatus ? code_memory.
     1311  ∀s'.
     1312  ∀b, b': Bit.
     1313  ∀opt, opt': option Bit.
     1314  ∀c, c': Bit.
     1315    b = b' →
     1316    opt = opt' →
    13051317    c = c' →
    1306     (∀left, right. status_of_pseudo_status M cm (s left right c') sigma policy = s' left right c') →
    1307     let 〈left, right〉 ≝ c' in s' left right c' =
    1308     status_of_pseudo_status M cm (let 〈left, right〉 ≝ c in s left right c) sigma policy.
    1309   #A #B #M #cm #sigma #policy * #a #b * #a' #b' #s #s' normalize nodelta //
    1310 qed.
    1311 
    1312 lemma let_pair_as_in_status_of_pseudo_status:
    1313   ∀A, B, M, cm, sigma, policy. ∀c, c': A × B. ∀s, s'.
    1314   ∀c_refl: c = c'.
    1315     (∀left, right, H. status_of_pseudo_status M cm (s left right H c') sigma policy = s' left right H c) →
    1316     let 〈left, right〉 as H ≝ c' in s' left right H c =
    1317     status_of_pseudo_status M cm (let 〈left, right〉 as H' ≝ c in s left right ? c) sigma policy.
    1318   [2: >H' assumption ]
    1319   #A #B #M #cm #sigma #policy * #a #b * #a' #b' #s #s'
    1320   #destruct_assm destruct(destruct_assm) normalize nodelta
    1321   #status_of_pseudo_status_assm >status_of_pseudo_status_assm //
    1322 qed.
    1323 
    1324 lemma if_then_else_status_of_pseudo_status:
     1318    status_of_pseudo_status M code_memory s sigma policy = s' →
     1319      set_flags … s' b opt c =
     1320        status_of_pseudo_status M code_memory (set_flags … code_memory s b' opt' c') sigma policy.
     1321  #M #sigma #policy #code_memory #s #s' #b #b' #opt #opt' #c #c'
     1322  #b_refl #opt_refl #c_refl <b_refl <opt_refl <c_refl #s_refl <s_refl
     1323  whd in match status_of_pseudo_status; normalize nodelta
     1324  whd in match sfr_8051_of_pseudo_sfr_8051; normalize nodelta
     1325  cases (\snd M)
     1326  [1:
     1327    normalize nodelta %
     1328  |2:
     1329    * #address normalize nodelta
     1330    @(vsplit_elim bool ???) #high #low #high_low_refl normalize nodelta
     1331    whd in ⊢ (??%%); cases opt try #opt' normalize nodelta
     1332    @split_eq_status try % whd in match (sfr_8051_index ?);
     1333    cases daemon
     1334  ]
     1335qed.
     1336
     1337lemma get_ac_flag_status_of_pseudo_status:
    13251338  ∀M: internal_pseudo_address_map.
    1326   ∀cm: pseudo_assembly_program.
    13271339  ∀sigma: Word → Word.
    13281340  ∀policy: Word → bool.
    1329   ∀s, s', s'', s'''.
    1330   ∀t, t': bool.
    1331     t = t' →
    1332     status_of_pseudo_status M cm s sigma policy = s' →
    1333     status_of_pseudo_status M cm s'' sigma policy = s''' →
    1334       if t then
    1335         s'
    1336       else
    1337         s''' =
    1338       status_of_pseudo_status M cm (if t' then s else s'') sigma policy.
    1339   #M #cm #sigma #policy #s #s' #s'' #s''' #t #t' #t_refl #s_refl
    1340   >t_refl normalize nodelta >s_refl cases t' normalize nodelta //
    1341 qed.
     1341  ∀code_memory: pseudo_assembly_program.
     1342  ∀s: PreStatus ? code_memory.
     1343  ∀s'.
     1344    status_of_pseudo_status M code_memory s sigma policy = s' →
     1345      get_ac_flag ?? s' = get_ac_flag ? code_memory s.
     1346  #M #sigma #policy #code_memory #s #s' #s_refl <s_refl
     1347  whd in match get_ac_flag; normalize nodelta
     1348  whd in match status_of_pseudo_status; normalize nodelta
     1349  whd in match sfr_8051_of_pseudo_sfr_8051; normalize nodelta
     1350  cases (\snd M) try %
     1351  * normalize nodelta #address
     1352  @(vsplit_elim bool ???) #high #low #high_low_refl normalize nodelta
     1353  whd in match sfr_8051_index; normalize nodelta
     1354  >get_index_v_set_index_miss [2,4: /2/] %
     1355qed.
     1356
     1357lemma get_cy_flag_status_of_pseudo_status:
     1358  ∀M: internal_pseudo_address_map.
     1359  ∀sigma: Word → Word.
     1360  ∀policy: Word → bool.
     1361  ∀code_memory: pseudo_assembly_program.
     1362  ∀s: PreStatus ? code_memory.
     1363  ∀s'.
     1364    status_of_pseudo_status M code_memory s sigma policy = s' →
     1365      get_cy_flag ?? s' = get_cy_flag ? code_memory s.
     1366  #M #sigma #policy #code_memory #s #s' #s_refl <s_refl
     1367  whd in match get_cy_flag; normalize nodelta
     1368  whd in match status_of_pseudo_status; normalize nodelta
     1369  whd in match sfr_8051_of_pseudo_sfr_8051; normalize nodelta
     1370  cases (\snd M) try %
     1371  * normalize nodelta #address
     1372  @(vsplit_elim bool ???) #high #low #high_low_refl normalize nodelta
     1373  whd in match sfr_8051_index; normalize nodelta
     1374  >get_index_v_set_index_miss [2,4: /2/] %
     1375qed.
     1376
     1377lemma get_ov_flag_status_of_pseudo_status:
     1378  ∀M: internal_pseudo_address_map.
     1379  ∀sigma: Word → Word.
     1380  ∀policy: Word → bool.
     1381  ∀code_memory: pseudo_assembly_program.
     1382  ∀s: PreStatus ? code_memory.
     1383  ∀s'.
     1384    status_of_pseudo_status M code_memory s sigma policy = s' →
     1385      get_ov_flag ?? s' = get_ov_flag ? code_memory s.
     1386  #M #sigma #policy #code_memory #s #s' #s_refl <s_refl
     1387  whd in match get_ov_flag; normalize nodelta
     1388  whd in match status_of_pseudo_status; normalize nodelta
     1389  whd in match sfr_8051_of_pseudo_sfr_8051; normalize nodelta
     1390  cases (\snd M) try %
     1391  * normalize nodelta #address
     1392  @(vsplit_elim bool ???) #high #low #high_low_refl normalize nodelta
     1393  whd in match sfr_8051_index; normalize nodelta
     1394  >get_index_v_set_index_miss [2,4: /2/] %
     1395qed.
Note: See TracChangeset for help on using the changeset viewer.