Changeset 2276 for src/ASM/Test.ma


Ignore:
Timestamp:
Jul 30, 2012, 2:36:41 PM (8 years ago)
Author:
sacerdot
Message:

...

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/Test.ma

    r2274 r2276  
    77lemma let_pair_in_status_of_pseudo_status:
    88  ∀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') →
     9    c' = c →
     10    (∀left, right.
     11      s' left right c' = status_of_pseudo_status M cm (s left right c') sigma policy) →
    1112    (let 〈left, right〉 ≝ c' in s' left right c') =
    1213    status_of_pseudo_status M cm (let 〈left, right〉 ≝ c in s left right c) sigma policy.
     
    1617lemma let_pair_as_in_status_of_pseudo_status:
    1718  ∀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') →
     19    c' = c
     20    (∀left, right, H, H'. s' left right H' c' = status_of_pseudo_status M cm (s left right H c) sigma policy) →
    2021    (let 〈left, right〉 as H' ≝ c' in s' left right H' c') =
    2122    status_of_pseudo_status M cm (let 〈left, right〉 as H ≝ c in s left right H c) sigma policy.
     
    3233  ∀t, t': bool.
    3334    t = t' →
    34     status_of_pseudo_status M cm s sigma policy = s'
    35     status_of_pseudo_status M cm s'' sigma policy = s'''
     35    s' = status_of_pseudo_status M cm s sigma policy
     36    s''' = status_of_pseudo_status M cm s'' sigma policy
    3637      if t then
    3738        s'
     
    5152  ∀new_ppc, new_ppc'.
    5253    sigma new_ppc = new_ppc' →
    53     status_of_pseudo_status M cm s sigma policy = s'
     54    s' = status_of_pseudo_status M cm s sigma policy
    5455    set_program_counter (BitVectorTrie Byte 16)
    5556      (code_memory_of_pseudo_assembly_program cm sigma policy)
     
    5758    status_of_pseudo_status M cm (set_program_counter … cm s new_ppc) sigma policy.
    5859  #M #cm #sigma #policy #s #s' #new_ppc #new_ppc'
    59   #new_ppc_refl #s_refl <new_ppc_refl <s_refl //
     60  #new_ppc_refl #s_refl <new_ppc_refl >s_refl //
    6061qed.
    6162
     
    6768  ∀s,s'.
    6869  ∀v.
    69    status_of_pseudo_status M code_memory s sigma policy = s'
     70   s' = status_of_pseudo_status M code_memory s sigma policy
    7071    set_p1_latch (BitVectorTrie Byte 16)
    7172      (code_memory_of_pseudo_assembly_program code_memory sigma policy)
     
    7374    status_of_pseudo_status M code_memory
    7475      (set_p1_latch pseudo_assembly_program code_memory s v) sigma policy.
    75   #M #cm #sigma #policy #s #s' #new_ppc #s_refl <s_refl //
     76  #M #cm #sigma #policy #s #s' #new_ppc #s_refl >s_refl //
    7677qed.
    7778
     
    8384  ∀s, s'.
    8485  ∀v.
    85   status_of_pseudo_status M code_memory s sigma policy = s'
     86  s' = status_of_pseudo_status M code_memory s sigma policy
    8687    set_p3_latch (BitVectorTrie Byte 16)
    8788      (code_memory_of_pseudo_assembly_program code_memory sigma policy)
     
    8990    status_of_pseudo_status M code_memory
    9091      (set_p3_latch pseudo_assembly_program code_memory s v) sigma policy.
    91   #M #code_memory #sigma #policy #s #s' #v #s_refl <s_refl //
    92 qed.
    93 
    94 definition map_acc_a_using_internal_pseudo_address_map:
    95     ∀M: internal_pseudo_address_map. (Word → Word) → Byte → Byte ≝
    96   λM, sigma, v.
    97   match \snd M with
    98   [ None ⇒ v
    99   | Some upper_lower_addr ⇒
    100     let 〈upper_lower, addr〉 ≝ upper_lower_addr in
    101       if eq_upper_lower upper_lower upper then
    102         let 〈high, low〉 ≝ vsplit bool 8 8 (sigma (v@@addr)) in
    103           high
    104       else
    105         let 〈high, low〉 ≝ vsplit bool 8 8 (sigma (addr@@v)) in
    106           low
    107   ].
    108 
    109 (*CSC: Taken from AssemblyProofSplit.ma; there named map_lower_internal... *)
    110 definition map_internal_ram_address_using_pseudo_address_map:
    111   ∀M: internal_pseudo_address_map. (Word → Word) → Byte → Byte → Byte ≝
    112   λM: internal_pseudo_address_map.
    113   λsigma: Word → Word.
    114   λaddress: Byte.
    115   λvalue: Byte.
    116   match lookup_from_internal_ram … address M with
    117   [ None ⇒ value
    118   | Some upper_lower_word ⇒
    119     let 〈upper_lower, word〉 ≝ upper_lower_word in
    120       if eq_upper_lower upper_lower upper then
    121         let 〈high, low〉 ≝ vsplit bool 8 8 (sigma (value@@word)) in
    122           high
    123       else
    124         let 〈high, low〉 ≝ vsplit bool 8 8 (sigma (word@@value)) in
    125           low
    126   ].
     92  #M #code_memory #sigma #policy #s #s' #v #s_refl >s_refl //
     93qed.
    12794
    12895definition map_address_using_internal_pseudo_address_map:
     
    277244      whd in match map_address_using_internal_pseudo_address_map; normalize nodelta
    278245      whd in match map_acc_a_using_internal_pseudo_address_map; normalize nodelta
    279       >sndM_refl normalize nodelta
     246      >sndM_refl normalize nodelta whd in match map_value_using_opt_address_entry; normalize nodelta
    280247      >eq_upper_lower_refl normalize nodelta
    281248      [1:
     
    331298      whd in match map_address_using_internal_pseudo_address_map; normalize nodelta
    332299      whd in match map_acc_a_using_internal_pseudo_address_map; normalize nodelta
    333       >sndM_refl normalize nodelta >high_low_refl normalize nodelta
     300      whd in match map_value_using_opt_address_entry; normalize nodelta
     301      >sndM_refl normalize nodelta >high_low_refl normalize nodelta
    334302      >eq_upper_lower_refl normalize nodelta
    335303      whd in match (set_8051_sfr ?????); //
     
    342310lemma set_8051_sfr_status_of_pseudo_status:
    343311  ∀M, code_memory, sigma, policy, s, s', sfr, v,v'.
    344     status_of_pseudo_status M code_memory s sigma policy = s'
     312    s' = status_of_pseudo_status M code_memory s sigma policy
    345313    map_address_using_internal_pseudo_address_map M sigma sfr v = v' →
    346314      set_8051_sfr ? (code_memory_of_pseudo_assembly_program code_memory sigma policy) s' sfr v' =
     
    348316        (set_8051_sfr pseudo_assembly_program code_memory s sfr v) sigma policy.
    349317  #M #code_memory #sigma #policy #s #s' #sfr #v #v' #s_ok #v_ok
    350   <s_ok whd in ⊢ (??%%); @split_eq_status try % /2 by set_index_status_of_pseudo_status/
     318  >s_ok whd in ⊢ (??%%); @split_eq_status try % /2 by set_index_status_of_pseudo_status/
    351319qed.
    352320
     
    374342lemma get_8051_sfr_status_of_pseudo_status:
    375343  ∀M, code_memory, sigma, policy, s, s', s'', sfr.
    376     status_of_pseudo_status M code_memory s sigma policy = s'
     344    s' = status_of_pseudo_status M code_memory s sigma policy
    377345    map_address_using_internal_pseudo_address_map M sigma sfr
    378346     (get_8051_sfr pseudo_assembly_program code_memory s sfr) = s'' →
     
    380348    (code_memory_of_pseudo_assembly_program code_memory sigma policy)
    381349     s' sfr = s''.
    382   #M #code_memory #sigma #policy #s #s' #s'' #sfr #s_refl #s_refl' <s_refl <s_refl'
     350  #M #code_memory #sigma #policy #s #s' #s'' #sfr #s_refl #s_refl' >s_refl <s_refl'
    383351  whd in match get_8051_sfr; normalize nodelta
    384352  @get_index_v_status_of_pseudo_status %
     
    387355lemma get_8052_sfr_status_of_pseudo_status:
    388356  ∀M, code_memory, sigma, policy, s, s', sfr.
    389   status_of_pseudo_status M code_memory s sigma policy = s'
     357  s' = status_of_pseudo_status M code_memory s sigma policy
    390358  (get_8052_sfr (BitVectorTrie Byte 16)
    391359    (code_memory_of_pseudo_assembly_program code_memory sigma policy)
    392360    s' sfr =
    393361   (get_8052_sfr pseudo_assembly_program code_memory s sfr)).
    394   #M #code_memory #sigma #policy #s #s' #sfr #s_refl <s_refl //
     362  #M #code_memory #sigma #policy #s #s' #sfr #s_refl >s_refl //
    395363qed.
    396364
    397365lemma set_8052_sfr_status_of_pseudo_status:
    398366  ∀M, code_memory, sigma, policy, s, s', sfr, v.
    399   status_of_pseudo_status M code_memory s sigma policy = s'
     367  s' = status_of_pseudo_status M code_memory s sigma policy
    400368    (set_8052_sfr (BitVectorTrie Byte 16)
    401369      (code_memory_of_pseudo_assembly_program code_memory sigma policy) s' sfr v =
    402370    status_of_pseudo_status M code_memory
    403371     (set_8052_sfr pseudo_assembly_program code_memory s sfr v) sigma policy).
    404   #M #code_memory #sigma #policy #s #s' #sfr #v #s_refl <s_refl //
     372  #M #code_memory #sigma #policy #s #s' #sfr #v #s_refl >s_refl //
    405373qed.
    406374 
     
    429397        ∀s'.
    430398        ∀v'.
    431           status_of_pseudo_status M code_memory s sigma policy = s'
     399          s' = status_of_pseudo_status M code_memory s sigma policy
    432400            map_address_Byte_using_internal_pseudo_address_map M sigma d v = v' →
    433401              (set_bit_addressable_sfr (BitVectorTrie Byte 16)
     
    457425         | _ ⇒ set_8051_sfr ?? s sfr v ]
    458426      | inr sfr ⇒ set_8052_sfr ?? s sfr v ]])
    459   normalize nodelta #M #sigma #policy #s' #v' #s_refl <s_refl
     427  normalize nodelta #M #sigma #policy #s' #v' #s_refl >s_refl
    460428  /2 by refl, set_8051_sfr_status_of_pseudo_status, set_8052_sfr_status_of_pseudo_status/
    461429  whd in match map_address_using_internal_pseudo_address_map; normalize nodelta
     
    466434 ∀code_memory: pseudo_assembly_program. ∀s: PreStatus … code_memory. ∀d: Byte. ∀v: Byte.
    467435  ∀M. ∀sigma. ∀policy. ∀s': Status ?. ∀v'.
    468   status_of_pseudo_status M code_memory s sigma policy = s'
     436  s' = status_of_pseudo_status M code_memory s sigma policy
    469437  map_address_Byte_using_internal_pseudo_address_map M sigma d v = v' →
    470438 (set_bit_addressable_sfr (BitVectorTrie Byte 16)
     
    479447lemma set_low_internal_ram_status_of_pseudo_status:
    480448 ∀cm,sigma,policy,M,s,s',ram.
    481   status_of_pseudo_status M cm s sigma policy = s'
     449  s' = status_of_pseudo_status M cm s sigma policy
    482450  set_low_internal_ram (BitVectorTrie Byte 16)
    483451  (code_memory_of_pseudo_assembly_program cm sigma policy)
     
    486454  = status_of_pseudo_status M cm
    487455    (set_low_internal_ram pseudo_assembly_program cm s ram) sigma policy.
    488   #cm #sigma #policy #M #s #s' #ram #s_refl <s_refl //
     456  #cm #sigma #policy #M #s #s' #ram #s_refl >s_refl //
    489457qed.
    490458
     
    607575lemma set_register_status_of_pseudo_status:
    608576 ∀M,sigma,policy,cm,s,s',r,v,v'.
    609   status_of_pseudo_status M cm s sigma policy = s'
     577  s' = status_of_pseudo_status M cm s sigma policy
    610578  map_internal_ram_address_using_pseudo_address_map M sigma
    611579   (false:::bit_address_of_register pseudo_assembly_program cm s r) v =v' →
     
    615583  = status_of_pseudo_status M cm (set_register pseudo_assembly_program cm s r v)
    616584    sigma policy.
    617   #M #sigma #policy #cm #s #s' #r #v #v' #s_refl <s_refl #v_ok
     585  #M #sigma #policy #cm #s #s' #r #v #v' #s_refl >s_refl #v_ok
    618586 whd in match set_register; normalize nodelta
    619587 >bit_address_of_register_status_of_pseudo_status
     
    691659  ∀addr:[[ direct ; indirect ; registr ; acc_a ; acc_b ; ext_indirect ; ext_indirect_dptr ]].
    692660  ∀value. Σp: PreStatus ? cm. ∀M. ∀sigma. ∀policy. ∀s'. ∀value'.
    693    status_of_pseudo_status M cm ps sigma policy = s'
     661   s' = status_of_pseudo_status M cm ps sigma policy
    694662   map_address_mode_using_internal_pseudo_address_map_ok1 M cm ps sigma addr →
    695663   map_address_mode_using_internal_pseudo_address_map_ok2 … M sigma cm ps addr value = value' →
     
    747715          match other in False with [ ]
    748716      ] (subaddressing_modein … a)) normalize nodelta
    749   #M #sigma #policy #s' #v' #s_refl <s_refl
     717  #M #sigma #policy #s' #v' #s_refl >s_refl
    750718  whd in match map_address_mode_using_internal_pseudo_address_map_ok1; normalize nodelta
    751719  whd in match map_address_mode_using_internal_pseudo_address_map_ok2; normalize nodelta
     
    784752  ∀M. ∀sigma. ∀policy. ∀s'. ∀value'.
    785753   addr = addr' →
    786    status_of_pseudo_status M cm ps sigma policy = s'
     754   s' = status_of_pseudo_status M cm ps sigma policy
    787755   map_address_mode_using_internal_pseudo_address_map_ok1 M cm ps sigma addr →
    788756   map_address_mode_using_internal_pseudo_address_map_ok2 … M sigma cm ps addr value = value' →
     
    804772    ∀s: PreStatus … code_memory.
    805773    ∀s'.
    806     (status_of_pseudo_status M code_memory s sigma policy) = s'
     774    s' = status_of_pseudo_status M code_memory s sigma policy
    807775    (p1_latch (BitVectorTrie Byte 16)
    808776      (code_memory_of_pseudo_assembly_program code_memory sigma policy)
    809777      s' =
    810778    (p1_latch pseudo_assembly_program code_memory s)).
    811   #M #sigma #policy #code_memory #s #s' #s_refl <s_refl //
     779  #M #sigma #policy #code_memory #s #s' #s_refl >s_refl //
    812780qed.
    813781
     
    819787    ∀s: PreStatus … code_memory.
    820788    ∀s'.
    821     (status_of_pseudo_status M code_memory s sigma policy) = s'
     789    s' = status_of_pseudo_status M code_memory s sigma policy
    822790    (p3_latch (BitVectorTrie Byte 16)
    823791      (code_memory_of_pseudo_assembly_program code_memory sigma policy)
    824792      (status_of_pseudo_status M code_memory s sigma policy) =
    825793    (p3_latch pseudo_assembly_program code_memory s)).
    826   #M #sigma #policy #code_memory #s #s' #s_refl <s_refl //
     794  #M #sigma #policy #code_memory #s #s' #s_refl >s_refl //
    827795qed.
    828796
     
    834802    ∀l: bool.
    835803      Σp: Byte. ∀M. ∀sigma. ∀policy. ∀s'.
    836         status_of_pseudo_status M code_memory s sigma policy = s'
     804        s' = status_of_pseudo_status M code_memory s sigma policy
    837805        (get_bit_addressable_sfr (BitVectorTrie Byte 16)
    838806          (code_memory_of_pseudo_assembly_program code_memory sigma policy)
     
    869837    ]
    870838    ])
    871   #M #sigma #policy #s' #s_refl <s_refl normalize nodelta
     839  #M #sigma #policy #s' #s_refl >s_refl normalize nodelta
    872840  /2 by get_8051_sfr_status_of_pseudo_status, p1_latch_status_of_pseudo_status, p3_latch_status_of_pseudo_status/
    873841qed.
     
    882850      map_address_Byte_using_internal_pseudo_address_map M sigma
    883851         d (get_bit_addressable_sfr pseudo_assembly_program code_memory s d l) = s'' →
    884       (status_of_pseudo_status M code_memory s sigma policy) = s'
     852      s' = status_of_pseudo_status M code_memory s sigma policy
    885853        (get_bit_addressable_sfr (BitVectorTrie Byte 16)
    886854          (code_memory_of_pseudo_assembly_program code_memory sigma policy)
     
    888856 #code #s #d #v
    889857 cases (get_bit_addressable_sfr_status_of_pseudo_status' code s d v) #_ #relevant
    890  #M #sigma #policy #s' #s'' #s_refl #s_refl' <s_refl <s_refl' @relevant %
     858 #M #sigma #policy #s' #s'' #s_refl #s_refl' <s_refl >s_refl' @relevant %
    891859qed.
    892860
     
    898866    ∀s''.
    899867    sigma (program_counter … s) = s'' →
    900     (status_of_pseudo_status M code_memory s sigma policy) = s'
     868    s' = status_of_pseudo_status M code_memory s sigma policy
    901869      program_counter … (code_memory_of_pseudo_assembly_program code_memory sigma policy)
    902870        s' = s''.
    903   #M #sigma #policy #code_memory #s #s' #s'' #s_refl #s_refl' <s_refl <s_refl' //
     871  #M #sigma #policy #code_memory #s #s' #s'' #s_refl #s_refl' <s_refl >s_refl' //
    904872qed.
    905873
    906874lemma get_cy_flag_status_of_pseudo_status:
    907875  ∀M, cm, sigma, policy, s, s'.
    908   (status_of_pseudo_status M cm s sigma policy) = s'
     876  s' = status_of_pseudo_status M cm s sigma policy
    909877  (get_cy_flag (BitVectorTrie Byte 16)
    910878    (code_memory_of_pseudo_assembly_program cm sigma policy)
    911879    s' =
    912880  get_cy_flag pseudo_assembly_program cm s).
    913   #M #cm #sigma #policy #s #s' #s_refl <s_refl
     881  #M #cm #sigma #policy #s #s' #s_refl >s_refl
    914882  whd in match get_cy_flag; normalize nodelta
    915883  >(get_index_v_status_of_pseudo_status … (refl …)) %
     
    922890  ∀addr:[[ direct ; indirect ; registr ; acc_a ; acc_b ; data ; acc_dptr ; acc_pc ; ext_indirect ; ext_indirect_dptr ]].
    923891    Σp: Byte. ∀M. ∀sigma. ∀policy. ∀s'.
    924       (status_of_pseudo_status M cm ps sigma policy) = s'
     892      s' = status_of_pseudo_status M cm ps sigma policy
    925893      map_address_mode_using_internal_pseudo_address_map_ok1 M cm ps sigma addr →
    926894      get_arg_8 (BitVectorTrie Byte 16) (code_memory_of_pseudo_assembly_program cm sigma policy)
     
    972940        match other in False with [ ]
    973941      ] (subaddressing_modein … a)) normalize nodelta
    974   #M #sigma #policy #s' #s_refl <s_refl
     942  #M #sigma #policy #s' #s_refl >s_refl
    975943  whd in match map_address_mode_using_internal_pseudo_address_map_ok1; normalize nodelta
    976944  whd in match map_address_mode_using_internal_pseudo_address_map_ok2; normalize nodelta
     
    1023991  ∀addr:[[ direct ; indirect ; registr ; acc_a ; acc_b ; data ; acc_dptr ; acc_pc ; ext_indirect ; ext_indirect_dptr ]].
    1024992  ∀M. ∀sigma. ∀policy. ∀s', s''.
    1025       (status_of_pseudo_status M cm ps sigma policy) = s'
     993      s' = status_of_pseudo_status M cm ps sigma policy
    1026994      map_address_mode_using_internal_pseudo_address_map_ok2 … M sigma cm ps addr (get_arg_8 … cm ps l addr) = s'' →
    1027995      map_address_mode_using_internal_pseudo_address_map_ok1 M cm ps sigma addr →
     
    10391007  ∀addr: [[data16]].
    10401008  ∀M. ∀sigma. ∀policy. ∀s'.
    1041     status_of_pseudo_status M cm ps sigma policy = s'
     1009    s' = status_of_pseudo_status M cm ps sigma policy
    10421010      get_arg_16 (BitVectorTrie Byte 16) (code_memory_of_pseudo_assembly_program cm sigma policy)
    10431011      s' addr =
     
    10521020  ∀v,v': Word.
    10531021  ∀M. ∀sigma. ∀policy. ∀s'.
    1054     status_of_pseudo_status M cm ps sigma policy = s'
     1022    s' = status_of_pseudo_status M cm ps sigma policy
    10551023    v=v' → addr=addr' →
    10561024      set_arg_16 (BitVectorTrie Byte 16) (code_memory_of_pseudo_assembly_program cm sigma policy)
    10571025      s' v' addr' =
    10581026      status_of_pseudo_status M cm (set_arg_16 ? cm ps v addr) sigma policy.
    1059   #cm #ps #addr #addr' #v #v' #M #sigma #policy #s' #s_refl <s_refl #addr_refl
     1027  #cm #ps #addr #addr' #v #v' #M #sigma #policy #s' #s_refl >s_refl #addr_refl
    10601028  <addr_refl #v_refl <v_refl
    10611029  @(subaddressing_mode_elim … addr)
     
    10631031  whd in match set_arg_16'; normalize nodelta
    10641032  @(vsplit_elim bool ???) #bu #bl #bu_bl_refl normalize nodelta
    1065   @set_8051_sfr_status_of_pseudo_status try % @sym_eq
     1033  @set_8051_sfr_status_of_pseudo_status try %
    10661034  @set_8051_sfr_status_of_pseudo_status %
    10671035qed.
     
    11061074  ∀l.
    11071075    Σb: bool. ∀M. ∀sigma. ∀policy. ∀s'.
    1108       status_of_pseudo_status M cm ps sigma policy = s'
     1076      s' = status_of_pseudo_status M cm ps sigma policy
    11091077      map_bit_address_mode_using_internal_pseudo_address_map_get M cm ps sigma addr l →
    11101078      get_arg_1 (BitVectorTrie Byte 16) (code_memory_of_pseudo_assembly_program cm sigma policy)
     
    11521120      ] (subaddressing_modein … a)) normalize nodelta
    11531121  [4,5,8,9: //]
    1154   #M #sigma #policy #s' #s_refl <s_refl
     1122  #M #sigma #policy #s' #s_refl >s_refl
    11551123  [1:
    11561124    #_ >(get_cy_flag_status_of_pseudo_status … (refl …)) %
     
    11751143  ∀M. ∀sigma. ∀policy. ∀s'.
    11761144    addr = addr' →
    1177     status_of_pseudo_status M cm ps sigma policy = s'
     1145    s' = status_of_pseudo_status M cm ps sigma policy
    11781146      map_bit_address_mode_using_internal_pseudo_address_map_get M cm ps sigma addr l →
    11791147      get_arg_1 (BitVectorTrie Byte 16) (code_memory_of_pseudo_assembly_program cm sigma policy)
     
    13451313lemma clock_status_of_pseudo_status:
    13461314 ∀M,cm,sigma,policy,s,s'.
    1347   (status_of_pseudo_status M cm s sigma policy) = s'
     1315  s' = status_of_pseudo_status M cm s sigma policy
    13481316  clock …
    13491317   (code_memory_of_pseudo_assembly_program cm sigma policy)
    13501318   s'
    13511319  = clock … cm s.
    1352   #M #cm #sigma #policy #s #s' #s_refl <s_refl //
     1320  #M #cm #sigma #policy #s #s' #s_refl >s_refl //
    13531321qed.
    13541322
    13551323lemma set_clock_status_of_pseudo_status:
    13561324 ∀M,cm,sigma,policy,s,s',v,v'.
    1357  status_of_pseudo_status M cm s sigma policy = s'
     1325 s' = status_of_pseudo_status M cm s sigma policy
    13581326 v = v' →
    13591327  set_clock …
     
    13611329   s' v
    13621330  = status_of_pseudo_status M cm (set_clock … cm s v') sigma policy.
    1363   #M #cm #sigma #policy #s #s' #v #v' #s_refl #v_refl <s_refl <v_refl //
    1364 qed.
    1365 
    1366 (*CSC: daemon
     1331  #M #cm #sigma #policy #s #s' #v #v' #s_refl #v_refl >s_refl <v_refl //
     1332qed.
     1333
    13671334lemma set_flags_status_of_pseudo_status:
    13681335  ∀M.
     
    13781345    opt = opt' →
    13791346    c = c' →
    1380     status_of_pseudo_status M code_memory s sigma policy = s'
     1347    s' = status_of_pseudo_status M code_memory s sigma policy
    13811348      set_flags … s' b opt c =
    13821349        status_of_pseudo_status M code_memory (set_flags … code_memory s b' opt' c') sigma policy.
    1383   #M #sigma #policy #code_memory #s #s' #b #b' #opt #opt' #c #c'
    1384   #b_refl #opt_refl #c_refl <b_refl <opt_refl <c_refl #s_refl <s_refl
    1385   whd in match status_of_pseudo_status; normalize nodelta
    1386   whd in match sfr_8051_of_pseudo_sfr_8051; normalize nodelta
    1387   cases (\snd M)
    1388   [1:
    1389     normalize nodelta %
    1390   |2: ** #address normalize nodelta
    1391     @(vsplit_elim bool ???) #high #low #high_low_refl normalize nodelta
    1392     whd in ⊢ (??%%); cases opt try #opt' normalize nodelta
    1393     @split_eq_status try % whd in match (sfr_8051_index ?);
    1394     cases daemon
    1395   ]
    1396 qed.*)
     1350  ** #low #high #accA #sigma #policy #code_memory #s #s' #b #b' #opt #opt' #c #c'
     1351  #b_refl #opt_refl #c_refl <b_refl <opt_refl <c_refl #s_refl >s_refl
     1352  whd in match set_flags; normalize nodelta
     1353  @set_8051_sfr_status_of_pseudo_status try %
     1354  whd in match map_address_using_internal_pseudo_address_map; normalize nodelta
     1355  @eq_f2 [ >(get_8051_sfr_status_of_pseudo_status … (refl …)) [2: % | skip] %]
     1356  @eq_f2 [ >(get_8051_sfr_status_of_pseudo_status … (refl …)) [2: % | skip] %] 
     1357  @eq_f2 [ >(get_8051_sfr_status_of_pseudo_status … (refl …)) [2: % | skip] %]
     1358  @eq_f2 [ >(get_8051_sfr_status_of_pseudo_status … (refl …)) [2: % | skip] %]
     1359  @eq_f2 [ >(get_8051_sfr_status_of_pseudo_status … (refl …)) [2: % | skip] %]
     1360  @eq_f2 [ >(get_8051_sfr_status_of_pseudo_status … (refl …)) [2: % | skip] %] 
     1361  @eq_f2 [ >(get_8051_sfr_status_of_pseudo_status … (refl …)) [2: % | skip] %]
     1362  @eq_f2 [ >(get_8051_sfr_status_of_pseudo_status … (refl …)) [2: % | skip] %]
     1363  %
     1364qed.
    13971365
    13981366lemma get_ac_flag_status_of_pseudo_status:
     
    14031371  ∀s: PreStatus ? code_memory.
    14041372  ∀s'.
    1405     status_of_pseudo_status M code_memory s sigma policy = s'
     1373    s' = status_of_pseudo_status M code_memory s sigma policy
    14061374      get_ac_flag ?? s' = get_ac_flag ? code_memory s.
    1407   #M #sigma #policy #code_memory #s #s' #s_refl <s_refl
     1375  #M #sigma #policy #code_memory #s #s' #s_refl >s_refl
    14081376  whd in match get_ac_flag; normalize nodelta
    14091377  whd in match status_of_pseudo_status; normalize nodelta
     
    14231391  ∀s: PreStatus ? code_memory.
    14241392  ∀s'.
    1425     status_of_pseudo_status M code_memory s sigma policy = s'
     1393    s' = status_of_pseudo_status M code_memory s sigma policy
    14261394      get_ov_flag ?? s' = get_ov_flag ? code_memory s.
    1427   #M #sigma #policy #code_memory #s #s' #s_refl <s_refl
     1395  #M #sigma #policy #code_memory #s #s' #s_refl >s_refl
    14281396  whd in match get_ov_flag; normalize nodelta
    14291397  whd in match status_of_pseudo_status; normalize nodelta
Note: See TracChangeset for help on using the changeset viewer.