Changeset 2181 for src/ASM/Test.ma


Ignore:
Timestamp:
Jul 13, 2012, 11:00:04 AM (9 years ago)
Author:
mulligan
Message:

Work from the last week on the new formulation of the main lemma for assembler correctness.

File:
1 edited

Legend:

Unmodified
Added
Removed

  • src/ASM/Test.ma

    r2173 r2181  
    1919    status_of_pseudo_status M cm (set_program_counter … cm s new_ppc) sigma policy.
    2020  #M #cm #sigma #policy #s #s' #new_ppc #s_refl <s_refl //
     21qed.
     22
     23lemma if_then_else_status_of_pseudo_status_true:
     24  ∀M: internal_pseudo_address_map.
     25  ∀cm: pseudo_assembly_program.
     26  ∀sigma: Word → Word.
     27  ∀policy: Word → bool.
     28  ∀s, s', s'', s'''.
     29  ∀t: bool.
     30    t = true →
     31    status_of_pseudo_status M cm s sigma policy = s' →
     32      if t then
     33        s'
     34      else
     35        s'' =
     36      status_of_pseudo_status M cm (if t then s else s''') sigma policy.
     37  #M #cm #sigma #policy #s #s' #s'' #s''' #t #t_refl #s_refl
     38  >t_refl normalize nodelta >s_refl %
     39qed.
     40
     41lemma if_then_else_status_of_pseudo_status_false:
     42  ∀M: internal_pseudo_address_map.
     43  ∀cm: pseudo_assembly_program.
     44  ∀sigma: Word → Word.
     45  ∀policy: Word → bool.
     46  ∀s, s', s'', s'''.
     47  ∀t: bool.
     48    t = false →
     49    status_of_pseudo_status M cm s sigma policy = s' →
     50      if t then
     51        s''
     52      else
     53        s' =
     54      status_of_pseudo_status M cm (if t then s''' else s) sigma policy.
     55  #M #cm #sigma #policy #s #s' #s'' #s''' #t #t_refl #s_refl
     56  >t_refl normalize nodelta >s_refl %
    2157qed.
    2258
    … …  
    225261
    226262lemma get_index_v_status_of_pseudo_status:
    227   ∀M, code_memory, sigma, policy, s, sfr.
    228     (get_index_v Byte 19
     263  ∀M, code_memory, sigma, policy, s, s', sfr.
     264    map_address_using_internal_pseudo_address_map M sigma sfr
     265      (get_index_v Byte 19
     266        (special_function_registers_8051 pseudo_assembly_program code_memory s)
     267        (sfr_8051_index sfr) (sfr8051_index_19 sfr)) = s' →
     268    get_index_v Byte 19
    229269      (special_function_registers_8051 (BitVectorTrie Byte 16)
    230270      (code_memory_of_pseudo_assembly_program code_memory sigma policy)
    231271      (status_of_pseudo_status M code_memory s sigma policy))
    232       (sfr_8051_index sfr) (sfr8051_index_19 sfr) =
    233     map_address_using_internal_pseudo_address_map M sigma sfr
    234       (get_index_v Byte 19
    235         (special_function_registers_8051 pseudo_assembly_program code_memory s)
    236         (sfr_8051_index sfr) (sfr8051_index_19 sfr))).
    237   #M #code_memory #sigma #policy #s #sfr
     272      (sfr_8051_index sfr) (sfr8051_index_19 sfr) = s'.
     273  #M #code_memory #sigma #policy #s #s' #sfr #s_refl <s_refl
    238274  whd in match status_of_pseudo_status; normalize nodelta
    239275  whd in match sfr_8051_of_pseudo_sfr_8051; normalize nodelta
    … …  
    275311
    276312lemma get_8051_sfr_status_of_pseudo_status:
    277   ∀M, code_memory, sigma, policy, s, s', sfr.
     313  ∀M, code_memory, sigma, policy, s, s', s'', sfr.
    278314    status_of_pseudo_status M code_memory s sigma policy = s' →
    279   (get_8051_sfr (BitVectorTrie Byte 16)
     315    map_address_using_internal_pseudo_address_map M sigma sfr
     316     (get_8051_sfr pseudo_assembly_program code_memory s sfr) = s'' →
     317  get_8051_sfr (BitVectorTrie Byte 16)
    280318    (code_memory_of_pseudo_assembly_program code_memory sigma policy)
    281      s' sfr =
    282   map_address_using_internal_pseudo_address_map M sigma sfr
    283    (get_8051_sfr pseudo_assembly_program code_memory s sfr)).
    284   #M #code_memory #sigma #policy #s #s' #sfr #s_refl <s_refl
     319     s' sfr = s''.
     320  #M #code_memory #sigma #policy #s #s' #s'' #sfr #s_refl #s_refl' <s_refl <s_refl'
    285321  whd in match get_8051_sfr; normalize nodelta
    286   @get_index_v_status_of_pseudo_status
     322  @get_index_v_status_of_pseudo_status %
    287323qed.
    288324
    … …  
    444480  bit_address_of_register … cm s r.
    445481 #M #cm #s #sigma #policy #r whd in ⊢ (??%%);
    446  >(get_8051_sfr_status_of_pseudo_status … (refl …))
     482 >(get_8051_sfr_status_of_pseudo_status … (refl …) (refl …))
    447483 @pair_elim #un #ln #_
    448484 @pair_elim #r1 #r0 #_ %
    … …  
    452488  primitive *)
    453489axiom lookup_low_internal_ram_of_pseudo_low_internal_ram:
    454  ∀M,sigma,cm,s,addr.
     490 ∀M,sigma,cm,s,s',addr.
     491  map_internal_ram_address_using_pseudo_address_map M sigma (false:::addr)
     492  (lookup Byte 7 addr
     493   (low_internal_ram pseudo_assembly_program cm s) (zero 8)) = s' →
    455494  lookup Byte 7 addr
    456495  (low_internal_ram_of_pseudo_low_internal_ram M
    457496   (low_internal_ram pseudo_assembly_program cm s)) (zero 8)
    458   =
    459   map_internal_ram_address_using_pseudo_address_map M sigma (false:::addr)
    460   (lookup Byte 7 addr
    461    (low_internal_ram pseudo_assembly_program cm s) (zero 8)).
     497  = s'.
    462498
    463499(*CSC: provable using the axiom in AssemblyProof, but this one seems more
    464500  primitive *)
    465501axiom lookup_high_internal_ram_of_pseudo_high_internal_ram:
    466  ∀M,sigma,cm,s,addr.
     502 ∀M,sigma,cm,s,s',addr.
     503  map_internal_ram_address_using_pseudo_address_map M sigma (true:::addr)
     504  (lookup Byte 7 addr
     505   (high_internal_ram pseudo_assembly_program cm s) (zero 8)) = s' →
    467506  lookup Byte 7 addr
    468507  (high_internal_ram_of_pseudo_high_internal_ram M
    469508   (high_internal_ram pseudo_assembly_program cm s)) (zero 8)
    470   =
    471   map_internal_ram_address_using_pseudo_address_map M sigma (true:::addr)
    472   (lookup Byte 7 addr
    473    (high_internal_ram pseudo_assembly_program cm s) (zero 8)).
     509  = s'.
    474510
    475511lemma get_register_status_of_pseudo_status:
    476  ∀M,cm,sigma,policy,s,s',r.
     512 ∀M,cm,sigma,policy,s,s',s'',r.
    477513  status_of_pseudo_status M cm s sigma policy = s' →
     514  map_internal_ram_address_using_pseudo_address_map M sigma (false:::bit_address_of_register pseudo_assembly_program cm s r)
     515   (get_register … cm s r) = s'' →
    478516  get_register …
    479517   (code_memory_of_pseudo_assembly_program cm sigma policy)
    480    s' r =
    481   map_internal_ram_address_using_pseudo_address_map M sigma (false:::bit_address_of_register pseudo_assembly_program cm s r)
    482    (get_register … cm s r).
    483  #M #cm #sigma #policy #s #s' #r #s_refl <s_refl whd in match get_register; normalize nodelta
     518   s' r = s''.
     519 #M #cm #sigma #policy #s #s' #s'' #r #s_refl #s_refl' <s_refl <s_refl'
     520 whd in match get_register; normalize nodelta
    484521 whd in match status_of_pseudo_status; normalize nodelta
    485522 >bit_address_of_register_status_of_pseudo_status
    486  @lookup_low_internal_ram_of_pseudo_low_internal_ram
     523 @(lookup_low_internal_ram_of_pseudo_low_internal_ram … (refl …))
    487524qed.
    488525
    … …  
    586623qed.
    587624
    588 lemma set_arg_8_status_of_pseudo_status:
     625lemma set_arg_8_status_of_pseudo_status':
    589626  ∀cm.
    590627  ∀ps.
    … …  
    654691    | #_ #v_ok >(insert_low_internal_ram_status_of_pseudo_status … v) // ]
    655692  |3,4: #EQ1 #EQ2 change with (get_register ????) in match register in p;
    656       >(get_register_status_of_pseudo_status … (refl …))
     693      >(get_register_status_of_pseudo_status … (refl …) (refl …))
    657694      whd in match map_internal_ram_address_using_pseudo_address_map; normalize nodelta
    658695      >EQ1 normalize nodelta >p normalize nodelta >p1 normalize nodelta
    … …  
    660697      | >(insert_low_internal_ram_status_of_pseudo_status … v) ]
    661698      // <EQ2 @eq_f2 try % <(vsplit_ok … (sym_eq … p)) <eq_cons_head_append >p1 %
    662   |5: #EQ1 #EQ2 <EQ2 >(get_register_status_of_pseudo_status … (refl …))
     699  |5: #EQ1 #EQ2 <EQ2 >(get_register_status_of_pseudo_status … (refl …) (refl …))
    663700      whd in match map_internal_ram_address_using_pseudo_address_map; normalize nodelta
    664701      >EQ1 normalize nodelta
    … …  
    667704  |7: #EQ1 #EQ2 <EQ2 /2 by set_8051_sfr_status_of_pseudo_status/
    668705  |8: #_ #EQ <EQ @set_8051_sfr_status_of_pseudo_status %
    669   |9: #_ #EQ <EQ >(get_8051_sfr_status_of_pseudo_status … (refl …))
    670       >(get_8051_sfr_status_of_pseudo_status … (refl …))
     706  |9: #_ #EQ <EQ >(get_8051_sfr_status_of_pseudo_status … (refl …) (refl …))
     707      >(get_8051_sfr_status_of_pseudo_status … (refl …) (refl …))
    671708      >external_ram_status_of_pseudo_status @set_external_ram_status_of_pseudo_status ] %
     709qed.
     710
     711lemma set_arg_8_status_of_pseudo_status:
     712  ∀cm.
     713  ∀ps.
     714  ∀addr:[[ direct ; indirect ; registr ; acc_a ; acc_b ; ext_indirect ; ext_indirect_dptr ]].
     715  ∀value.
     716  ∀M. ∀sigma. ∀policy. ∀s'. ∀value'.
     717   status_of_pseudo_status M cm ps sigma policy = s' →
     718   map_address_mode_using_internal_pseudo_address_map_ok1 M cm ps sigma addr →
     719   map_address_mode_using_internal_pseudo_address_map_ok2 … M sigma cm ps addr value = value' →
     720    set_arg_8 (BitVectorTrie Byte 16)
     721      (code_memory_of_pseudo_assembly_program cm sigma policy)
     722      s' addr value' =
     723    status_of_pseudo_status M cm (set_arg_8 … cm ps addr value) sigma policy.
     724  #cm #ps #addr #value
     725  cases (set_arg_8_status_of_pseudo_status' cm ps addr value) #_ #relevant
     726  @relevant
    672727qed.
    673728
    … …  
    754809    ∀d: Byte.
    755810    ∀l: bool.
    756     ∀M. ∀sigma. ∀policy. ∀s'.
     811    ∀M. ∀sigma. ∀policy. ∀s'. ∀s''.
     812      map_address_Byte_using_internal_pseudo_address_map M sigma
     813         d (get_bit_addressable_sfr pseudo_assembly_program code_memory s d l) = s'' →
    757814      (status_of_pseudo_status M code_memory s sigma policy) = s' →
    758815        (get_bit_addressable_sfr (BitVectorTrie Byte 16)
    759816          (code_memory_of_pseudo_assembly_program code_memory sigma policy)
    760           s' d l =
    761         map_address_Byte_using_internal_pseudo_address_map M sigma
    762          d (get_bit_addressable_sfr pseudo_assembly_program code_memory s d l)).
    763  #code #s #d #v cases (get_bit_addressable_sfr_status_of_pseudo_status' code s d v) #_
    764  #H @H
     817          s' d l) = s''.
     818 #code #s #d #v
     819 cases (get_bit_addressable_sfr_status_of_pseudo_status' code s d v) #_ #relevant
     820 #M #sigma #policy #s' #s'' #s_refl #s_refl' <s_refl <s_refl' @relevant %
    765821qed.
    766822
    767823lemma program_counter_status_of_pseudo_status:
    768     ∀M. ∀sigma. ∀policy.
     824    ∀M. ∀sigma: Word → Word. ∀policy.
    769825    ∀code_memory: pseudo_assembly_program.
    770826    ∀s: PreStatus ? code_memory.
    771827    ∀s'.
     828    ∀s''.
     829    sigma (program_counter … s) = s'' →
    772830    (status_of_pseudo_status M code_memory s sigma policy) = s' →
    773831      program_counter … (code_memory_of_pseudo_assembly_program code_memory sigma policy)
    774         s' =
    775         sigma (program_counter … s).
    776   #M #sigma #policy #code_memory #s #s' #s_refl <s_refl //
     832        s' = s''.
     833  #M #sigma #policy #code_memory #s #s' #s'' #s_refl #s_refl' <s_refl <s_refl' //
    777834qed.
    778835
    … …  
    786843  #M #cm #sigma #policy #s #s' #s_refl <s_refl
    787844  whd in match get_cy_flag; normalize nodelta
    788   >get_index_v_status_of_pseudo_status %
    789 qed.
    790 
    791 lemma get_arg_8_status_of_pseudo_status:
     845  >(get_index_v_status_of_pseudo_status … (refl …)) %
     846qed.
     847
     848lemma get_arg_8_status_of_pseudo_status':
    792849  ∀cm.
    793850  ∀ps.
    … …  
    850907  [1:
    851908    #_ >p normalize nodelta >p1 normalize nodelta
    852     @get_bit_addressable_sfr_status_of_pseudo_status %
     909    @(get_bit_addressable_sfr_status_of_pseudo_status … (refl …)) %
    853910  |2:
    854911    #_>p normalize nodelta >p1 normalize nodelta
    855     @lookup_low_internal_ram_of_pseudo_low_internal_ram
     912    @(lookup_low_internal_ram_of_pseudo_low_internal_ram … sigma) %
    856913  |3,4:
    857     #assoc_list_assm >(get_register_status_of_pseudo_status … (refl …))
     914    #assoc_list_assm >(get_register_status_of_pseudo_status … (refl …) (refl …))
    858915    whd in match map_internal_ram_address_using_pseudo_address_map in ⊢ (??%?); normalize nodelta
    859916    >assoc_list_assm normalize nodelta >p normalize nodelta >p1 normalize nodelta
    860917    [1:
    861       >(lookup_high_internal_ram_of_pseudo_high_internal_ram … sigma)
     918      @(lookup_high_internal_ram_of_pseudo_high_internal_ram … sigma)
    862919    |2:
    863       >(lookup_low_internal_ram_of_pseudo_low_internal_ram … sigma)
     920      @(lookup_low_internal_ram_of_pseudo_low_internal_ram … sigma)
    864921    ]
    865922    @eq_f2 try % <(vsplit_ok … (sym_eq … p)) <eq_cons_head_append >p1 %
    866923  |5:
    867     #assoc_list_assm >(get_register_status_of_pseudo_status … (refl …))
     924    #assoc_list_assm >(get_register_status_of_pseudo_status … (refl …) (refl …))
    868925    whd in match map_internal_ram_address_using_pseudo_address_map in ⊢ (??%?); normalize nodelta
    869926    >assoc_list_assm normalize nodelta %
    870927  |6,7,8,9:
    871     #_ /2/
     928    #_ /2 by refl, get_register_status_of_pseudo_status, get_index_v_status_of_pseudo_status/
    872929  |10:
    873     #acc_a_assm >(get_8051_sfr_status_of_pseudo_status … (refl …))
    874     >(get_8051_sfr_status_of_pseudo_status … (refl …))
    875     >(get_8051_sfr_status_of_pseudo_status … (refl …))
     930    #acc_a_assm >(get_8051_sfr_status_of_pseudo_status … (refl …) (refl …))
     931    >(get_8051_sfr_status_of_pseudo_status … (refl …) (refl …))
     932    >(get_8051_sfr_status_of_pseudo_status … (refl …) (refl …))
    876933    whd in match map_address_using_internal_pseudo_address_map; normalize nodelta
    877934    >acc_a_assm >p normalize nodelta //
    878935  |11:
    879     * #map_acc_a_assm #sigma_assm >(get_8051_sfr_status_of_pseudo_status … (refl …))
    880     >(program_counter_status_of_pseudo_status … (refl …))
     936    * #map_acc_a_assm #sigma_assm >(get_8051_sfr_status_of_pseudo_status … (refl …) (refl …))
     937    >(program_counter_status_of_pseudo_status … (refl …) (refl …))
    881938    whd in match map_address_using_internal_pseudo_address_map; normalize nodelta
    882939    >sigma_assm >map_acc_a_assm >p normalize nodelta //
    883940  |12:
    884     #_ >(get_8051_sfr_status_of_pseudo_status … (refl …))
    885     >(get_8051_sfr_status_of_pseudo_status … (refl …))
     941    #_ >(get_8051_sfr_status_of_pseudo_status … (refl …) (refl …))
     942    >(get_8051_sfr_status_of_pseudo_status … (refl …) (refl …))
    886943    >external_ram_status_of_pseudo_status //
    887944  ]
     945qed.
     946
     947lemma get_arg_8_status_of_pseudo_status:
     948  ∀cm.
     949  ∀ps.
     950  ∀l.
     951  ∀addr:[[ direct ; indirect ; registr ; acc_a ; acc_b ; data ; acc_dptr ; acc_pc ; ext_indirect ; ext_indirect_dptr ]].
     952  ∀M. ∀sigma. ∀policy. ∀s', s''.
     953      (status_of_pseudo_status M cm ps sigma policy) = s' →
     954      map_address_mode_using_internal_pseudo_address_map_ok2 … M sigma cm ps addr (get_arg_8 … cm ps l addr) = s'' →
     955      map_address_mode_using_internal_pseudo_address_map_ok1 M cm ps sigma addr →
     956      get_arg_8 (BitVectorTrie Byte 16) (code_memory_of_pseudo_assembly_program cm sigma policy)
     957      s' l addr = s''.
     958  #cm #ps #l #addr
     959  cases (get_arg_8_status_of_pseudo_status' cm ps l addr) #_ #relevant
     960  #M #sigma #policy #s' #s'' #s_refl #s_refl' <s_refl'
     961  @relevant assumption
    888962qed.
    889963
    … …  
    10171091  |2,4:
    10181092    whd in ⊢ (% → ?); >p normalize nodelta >p1 normalize nodelta
    1019     >(get_bit_addressable_sfr_status_of_pseudo_status … (refl …)) #map_address_assm
     1093    >(get_bit_addressable_sfr_status_of_pseudo_status … (refl …) (refl …)) #map_address_assm
    10201094    >map_address_assm %
    10211095  |3,5:
    10221096    whd in ⊢ (% → ?); >p normalize nodelta >p1 normalize nodelta
    10231097    whd in match status_of_pseudo_status; normalize nodelta
    1024     >(lookup_low_internal_ram_of_pseudo_low_internal_ram … sigma)
     1098    >(lookup_low_internal_ram_of_pseudo_low_internal_ram … sigma … (refl …))
    10251099    #map_address_assm >map_address_assm %
    10261100  ]
    … …  
    11061180qed.
    11071181
    1108 lemma set_arg_1_status_of_pseudo_status:
     1182lemma set_arg_1_status_of_pseudo_status':
    11091183  ∀cm: pseudo_assembly_program.
    11101184  ∀ps: PreStatus pseudo_assembly_program cm.
    11111185  ∀addr: [[bit_addr; carry]].
    11121186  ∀b: Bit.
    1113     Σp: PreStatus … cm. ∀M. ∀sigma. ∀policy. ∀s'.
     1187    Σp: PreStatus … cm. ∀M. ∀sigma. ∀policy. ∀s'. ∀b'.
     1188      b = b' →
    11141189      status_of_pseudo_status M cm ps sigma policy = s' →
    11151190      map_bit_address_mode_using_internal_pseudo_address_map_set_1 M cm ps sigma addr b →
    … …  
    11181193          (code_memory_of_pseudo_assembly_program cm sigma policy)
    11191194          s' addr b =
    1120         status_of_pseudo_status M cm (set_arg_1 … cm ps addr b) sigma policy.
     1195        status_of_pseudo_status M cm (set_arg_1 … cm ps addr b') sigma policy.
    11211196  whd in match set_arg_1; normalize nodelta
    11221197  whd in match map_bit_address_mode_using_internal_pseudo_address_map_set_1; normalize nodelta
    … …  
    11571232            [ ]
    11581233      ] (subaddressing_modein … a)) normalize nodelta
    1159   try @modulus_less_than #M #sigma #policy #s' #s_refl <s_refl
     1234  try @modulus_less_than #M #sigma #policy #s' #b' #b_refl <b_refl #s_refl <s_refl
    11601235  [1:
    1161     #_ #_ >(get_8051_sfr_status_of_pseudo_status … (refl …))
     1236    #_ #_ >(get_8051_sfr_status_of_pseudo_status … (refl …) (refl …))
    11621237    whd in match map_address_using_internal_pseudo_address_map; normalize nodelta
    11631238    >p normalize nodelta @set_8051_sfr_status_of_pseudo_status %
    11641239  |2,3:
    1165     >(get_8051_sfr_status_of_pseudo_status … (refl …))
     1240    >(get_8051_sfr_status_of_pseudo_status … (refl …) (refl …))
    11661241    whd in match map_address_using_internal_pseudo_address_map; normalize nodelta
    11671242    >p normalize nodelta >p1 normalize nodelta
    11681243    #map_bit_address_assm_1 #map_bit_address_assm_2
    11691244    [1:
    1170       >(get_bit_addressable_sfr_status_of_pseudo_status … (refl …))
     1245      >(get_bit_addressable_sfr_status_of_pseudo_status … (refl …) (refl …))
    11711246      >map_bit_address_assm_1
    11721247      >(set_bit_addressable_sfr_status_of_pseudo_status cm s … map_bit_address_assm_2) %
    11731248    |2:
    11741249      whd in match status_of_pseudo_status in ⊢ (??(????%)?); normalize nodelta
    1175       >(lookup_low_internal_ram_of_pseudo_low_internal_ram … sigma)
     1250      >(lookup_low_internal_ram_of_pseudo_low_internal_ram … sigma … (refl …))
    11761251      >map_bit_address_assm_1
    11771252      >(insert_low_internal_ram_of_pseudo_low_internal_ram … map_bit_address_assm_2)
    … …  
    11791254    ]
    11801255  ]
     1256qed.
     1257
     1258lemma set_arg_1_status_of_pseudo_status:
     1259  ∀cm: pseudo_assembly_program.
     1260  ∀ps: PreStatus pseudo_assembly_program cm.
     1261  ∀addr: [[bit_addr; carry]].
     1262  ∀b: Bit.
     1263  ∀M. ∀sigma. ∀policy. ∀s'. ∀b'.
     1264      b = b' →
     1265      status_of_pseudo_status M cm ps sigma policy = s' →
     1266      map_bit_address_mode_using_internal_pseudo_address_map_set_1 M cm ps sigma addr b →
     1267      map_bit_address_mode_using_internal_pseudo_address_map_set_2 M cm ps sigma addr b →
     1268        set_arg_1 (BitVectorTrie Byte 16)
     1269          (code_memory_of_pseudo_assembly_program cm sigma policy)
     1270          s' addr b =
     1271        status_of_pseudo_status M cm (set_arg_1 … cm ps addr b') sigma policy.
     1272  #cm #ps #addr #b
     1273  cases (set_arg_1_status_of_pseudo_status' cm ps addr b) #_ #relevant
     1274  @relevant
    11811275qed.
    11821276
    … …  
    12011295  #M #cm #sigma #policy #s #s' #v #v' #s_refl #v_refl <s_refl <v_refl //
    12021296qed.
     1297
     1298lemma let_pair_in_status_of_pseudo_status:
     1299  ∀A, B, M, cm, sigma, policy. ∀c, c': A × B. ∀s, s'.
     1300    c = c' →
     1301    (∀left, right. status_of_pseudo_status M cm (s left right c') sigma policy = s' left right c') →
     1302    let 〈left, right〉 ≝ c' in s' left right c' =
     1303    status_of_pseudo_status M cm (let 〈left, right〉 ≝ c in s left right c) sigma policy.
     1304  #A #B #M #cm #sigma #policy * #a #b * #a' #b' #s #s' normalize nodelta //
     1305qed.
     1306
     1307lemma let_pair_as_in_status_of_pseudo_status:
     1308  ∀A, B, M, cm, sigma, policy. ∀c, c': A × B. ∀s, s'.
     1309  ∀c_refl: c = c'.
     1310    (∀left, right, H. status_of_pseudo_status M cm (s left right H c') sigma policy = s' left right H c) →
     1311    let 〈left, right〉 as H ≝ c' in s' left right H c =
     1312    status_of_pseudo_status M cm (let 〈left, right〉 as H' ≝ c in s left right ? c) sigma policy.
     1313  [2: >H' assumption ]
     1314  #A #B #M #cm #sigma #policy * #a #b * #a' #b' #s #s'
     1315  #destruct_assm destruct(destruct_assm) normalize nodelta
     1316  #status_of_pseudo_status_assm >status_of_pseudo_status_assm //
     1317qed.
     1318
     1319lemma if_then_else_status_of_pseudo_status:
     1320  ∀M: internal_pseudo_address_map.
     1321  ∀cm: pseudo_assembly_program.
     1322  ∀sigma: Word → Word.
     1323  ∀policy: Word → bool.
     1324  ∀s, s', s'', s'''.
     1325  ∀t, t': bool.
     1326    t = t' →
     1327    status_of_pseudo_status M cm s sigma policy = s' →
     1328    status_of_pseudo_status M cm s'' sigma policy = s''' →
     1329      if t then
     1330        s'
     1331      else
     1332        s''' =
     1333      status_of_pseudo_status M cm (if t' then s else s'') sigma policy.
     1334  #M #cm #sigma #policy #s #s' #s'' #s''' #t #t' #t_refl #s_refl
     1335  >t_refl normalize nodelta >s_refl cases t' normalize nodelta //
     1336qed.
Note: See TracChangeset for help on using the changeset viewer.