Changeset 2204 for src/ASM/Test.ma


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/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.