Changeset 2173


Ignore:
Timestamp:
Jul 10, 2012, 5:29:32 PM (5 years ago)
Author:
mulligan
Message:

MUL case of main lemma nearly complete (subject to two small holes that require a lemma) using new proof strategy.

Location:
src/ASM
Files:
2 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/AssemblyProofSplit.ma

    r2172 r2173  
    1919include alias "ASM/Vector.ma".
    2020include "ASM/Test.ma".
     21
     22lemma addressing_mode_ok_to_map_address_using_internal_pseudo_address_map:
     23  ∀M, cm, ps, sigma, x.
     24  ∀addr1: [[acc_a]].
     25    addressing_mode_ok pseudo_assembly_program M cm ps addr1=true →
     26      map_address_using_internal_pseudo_address_map M sigma SFR_ACC_A x = x.
     27  #M #cm #ps #sigma #x #addr1
     28  @(subaddressing_mode_elim … addr1)
     29  whd in ⊢ (??%? → ??%?);
     30  cases (\snd M)
     31  [1:
     32    //
     33  |2:
     34    #upper_lower #address normalize nodelta #absurd
     35    destruct(absurd)
     36  ]
     37qed.
    2138
    2239lemma main_lemma_preinstruction:
     
    477494  try (@(execute_1_technical … (subaddressing_modein …)) @I) (*66s*)
    478495  whd in match execute_1_preinstruction; normalize nodelta
    479   [31,32: (* DJNZ *)
     496
     497(*  [31,32: (* DJNZ *)
    480498  (* XXX: work on the right hand side *)
    481499  >p normalize nodelta >p1 normalize nodelta
     
    10491067  (* XXX: finally, prove the equality using sigma commutation *)
    10501068  try @split_eq_status try %
    1051   cases daemon
    1052   |10,42,43,44,45,49,52,56: (* MUL *)
     1069  cases daemon *)
     1070  [42,43,44,45,49,52,56:
     1071  |10: (* MUL *)
    10531072  (* XXX: work on the right hand side *)
    10541073  (* XXX: switch to the left hand side *)
    1055   -instr_refl >EQP -P normalize nodelta
     1074  >EQP -P normalize nodelta
    10561075  #sigma_increment_commutation #maps_assm #fetch_many_assm %{1}
     1076  whd in maps_assm:(??%%);
     1077  inversion (addressing_mode_ok ?????) in maps_assm; #addressing_mode_ok_assm_1
     1078  [2: normalize nodelta #absurd destruct(absurd) ]
     1079  inversion (addressing_mode_ok ?????) #addressing_mode_ok_assm_2
     1080  [2: normalize nodelta #absurd destruct(absurd) ]
     1081  normalize nodelta @Some_Some_elim #Mrefl destruct(Mrefl)
    10571082  whd in ⊢ (??%?);
    1058   <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm whd in ⊢ (??%?);
     1083  <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm >EQs >EQticks <instr_refl
     1084  change with (set_8051_sfr ????? = ?) @set_8051_sfr_status_of_pseudo_status
     1085  [2:
     1086    whd in ⊢ (??%?); @eq_f2 try % @eq_f2 try % @eq_f2 @eq_f
     1087    @sym_eq
     1088    [1:
     1089      @(get_8051_sfr_status_of_pseudo_status … policy)
     1090      cases daemon (* XXX: need a lemma *)
     1091    |2:
     1092      @(get_8051_sfr_status_of_pseudo_status M' … policy)
     1093      @sym_eq @set_clock_status_of_pseudo_status [2: % ]
     1094      @sym_eq @set_program_counter_status_of_pseudo_status %
     1095    ]
     1096  ]
     1097  @sym_eq @set_8051_sfr_status_of_pseudo_status
     1098  [2:
     1099    >(addressing_mode_ok_to_map_address_using_internal_pseudo_address_map … addressing_mode_ok_assm_1)
     1100    @eq_f @eq_f2 try % @eq_f2 @eq_f
     1101    @sym_eq
     1102    [1:
     1103      @(get_8051_sfr_status_of_pseudo_status … policy)
     1104      cases daemon (* XXX: needs a lemma *)
     1105    |2:
     1106      @(get_8051_sfr_status_of_pseudo_status M' … policy)
     1107      @sym_eq @set_clock_status_of_pseudo_status [2: % ]
     1108      @sym_eq @set_program_counter_status_of_pseudo_status %
     1109    ]
     1110  ]
     1111  @sym_eq @set_clock_status_of_pseudo_status
     1112  [2:
     1113    @eq_f %
     1114  ]
     1115  @sym_eq @set_program_counter_status_of_pseudo_status %
     1116   
    10591117  (* XXX: work on the left hand side *)
    10601118  (* XXX: switch to the right hand side *)
  • src/ASM/Test.ma

    r2172 r2173  
    88  ∀M.
    99  ∀cm.
    10   ∀ps.
    1110  ∀sigma.
    1211  ∀policy.
     12  ∀s, s'.
    1313  ∀new_ppc.
     14    status_of_pseudo_status M cm s sigma policy = s' →
    1415    set_program_counter (BitVectorTrie Byte 16)
    1516      (code_memory_of_pseudo_assembly_program cm sigma policy)
    16       (status_of_pseudo_status M cm ps sigma policy)
     17      s'
    1718      (sigma new_ppc) =
    18     status_of_pseudo_status M cm (set_program_counter … cm ps new_ppc) sigma policy.
    19   //
     19    status_of_pseudo_status M cm (set_program_counter … cm s new_ppc) sigma policy.
     20  #M #cm #sigma #policy #s #s' #new_ppc #s_refl <s_refl //
    2021qed.
    2122
     
    2526  ∀sigma.
    2627  ∀policy.
    27   ∀s.
     28  ∀s,s'.
    2829  ∀v.
     30   status_of_pseudo_status M code_memory s sigma policy = s' →
    2931    set_p1_latch (BitVectorTrie Byte 16)
    3032      (code_memory_of_pseudo_assembly_program code_memory sigma policy)
    31       (status_of_pseudo_status M code_memory s sigma policy) v =
     33      s' v =
    3234    status_of_pseudo_status M code_memory
    3335      (set_p1_latch pseudo_assembly_program code_memory s v) sigma policy.
    34   //
     36  #M #cm #sigma #policy #s #s' #new_ppc #s_refl <s_refl //
    3537qed.
    3638
     
    4042  ∀sigma.
    4143  ∀policy.
    42   ∀s.
     44  ∀s, s'.
    4345  ∀v.
     46  status_of_pseudo_status M code_memory s sigma policy = s' →
    4447    set_p3_latch (BitVectorTrie Byte 16)
    4548      (code_memory_of_pseudo_assembly_program code_memory sigma policy)
    46       (status_of_pseudo_status M code_memory s sigma policy) v =
     49      s' v =
    4750    status_of_pseudo_status M code_memory
    4851      (set_p3_latch pseudo_assembly_program code_memory s v) sigma policy.
    49   //
     52  #M #code_memory #sigma #policy #s #s' #v #s_refl <s_refl //
    5053qed.
    5154
     
    261264
    262265lemma set_8051_sfr_status_of_pseudo_status:
    263   ∀M, code_memory, sigma, policy, s, sfr, v,v'.
    264   map_address_using_internal_pseudo_address_map M sigma sfr v = v' →
    265 (set_8051_sfr (BitVectorTrie Byte 16)
    266   (code_memory_of_pseudo_assembly_program code_memory sigma policy)
    267   (status_of_pseudo_status M code_memory s sigma policy) sfr v'
    268   =status_of_pseudo_status M code_memory
    269    (set_8051_sfr pseudo_assembly_program code_memory s sfr v) sigma policy).
    270   #M #code_memory #sigma #policy #s #sfr #v #v' #v_ok
    271   whd in ⊢ (??%%); @split_eq_status try % /2/
     266  ∀M, code_memory, sigma, policy, s, s', sfr, v,v'.
     267    status_of_pseudo_status M code_memory s sigma policy = s' →
     268    map_address_using_internal_pseudo_address_map M sigma sfr v = v' →
     269      set_8051_sfr ? (code_memory_of_pseudo_assembly_program code_memory sigma policy) s' sfr v' =
     270      status_of_pseudo_status M code_memory
     271        (set_8051_sfr pseudo_assembly_program code_memory s sfr v) sigma policy.
     272  #M #code_memory #sigma #policy #s #s' #sfr #v #v' #s_ok #v_ok
     273  <s_ok whd in ⊢ (??%%); @split_eq_status try % /2/
    272274qed.
    273275
    274276lemma get_8051_sfr_status_of_pseudo_status:
    275   ∀M, code_memory, sigma, policy, s, sfr.
     277  ∀M, code_memory, sigma, policy, s, s', sfr.
     278    status_of_pseudo_status M code_memory s sigma policy = s' →
    276279  (get_8051_sfr (BitVectorTrie Byte 16)
    277280    (code_memory_of_pseudo_assembly_program code_memory sigma policy)
    278     (status_of_pseudo_status M code_memory s sigma policy) sfr =
     281     s' sfr =
    279282  map_address_using_internal_pseudo_address_map M sigma sfr
    280283   (get_8051_sfr pseudo_assembly_program code_memory s sfr)).
    281   #M #code_memory #sigma #policy #s #sfr
     284  #M #code_memory #sigma #policy #s #s' #sfr #s_refl <s_refl
    282285  whd in match get_8051_sfr; normalize nodelta
    283286  @get_index_v_status_of_pseudo_status
     
    285288
    286289lemma get_8052_sfr_status_of_pseudo_status:
    287   ∀M, code_memory, sigma, policy, s, sfr.
     290  ∀M, code_memory, sigma, policy, s, s', sfr.
     291  status_of_pseudo_status M code_memory s sigma policy = s' →
    288292  (get_8052_sfr (BitVectorTrie Byte 16)
    289293    (code_memory_of_pseudo_assembly_program code_memory sigma policy)
    290     (status_of_pseudo_status M code_memory s sigma policy) sfr =
     294    s' sfr =
    291295   (get_8052_sfr pseudo_assembly_program code_memory s sfr)).
    292   //
     296  #M #code_memory #sigma #policy #s #s' #sfr #s_refl <s_refl //
    293297qed.
    294298
    295299lemma set_8052_sfr_status_of_pseudo_status:
    296   ∀M, code_memory, sigma, policy, s, sfr, v.
    297 (set_8052_sfr (BitVectorTrie Byte 16)
    298   (code_memory_of_pseudo_assembly_program code_memory sigma policy)
    299   (status_of_pseudo_status M code_memory s sigma policy) sfr v
    300   =status_of_pseudo_status M code_memory
    301    (set_8052_sfr pseudo_assembly_program code_memory s sfr v) sigma policy).
    302  //
     300  ∀M, code_memory, sigma, policy, s, s', sfr, v.
     301  status_of_pseudo_status M code_memory s sigma policy = s' →
     302    (set_8052_sfr (BitVectorTrie Byte 16)
     303      (code_memory_of_pseudo_assembly_program code_memory sigma policy) s' sfr v =
     304    status_of_pseudo_status M code_memory
     305     (set_8052_sfr pseudo_assembly_program code_memory s sfr v) sigma policy).
     306  #M #code_memory #sigma #policy #s #s' #sfr #v #s_refl <s_refl //
    303307qed.
    304308 
     
    316320
    317321lemma set_bit_addressable_sfr_status_of_pseudo_status':
    318       let M ≝ pseudo_assembly_program in ∀code_memory: M. ∀s: PreStatus M code_memory. ∀d: Byte. ∀v: Byte.
    319         Σp: PreStatus M code_memory. ∀M. ∀sigma. ∀policy. ∀v'.
    320   map_address_Byte_using_internal_pseudo_address_map M sigma d v = v' →
    321  (set_bit_addressable_sfr (BitVectorTrie Byte 16)
    322   (code_memory_of_pseudo_assembly_program code_memory sigma policy)
    323   (status_of_pseudo_status M code_memory s sigma policy) d v'
    324   =status_of_pseudo_status M code_memory
    325    (set_bit_addressable_sfr pseudo_assembly_program code_memory s d v) sigma policy).
     322  let M ≝ pseudo_assembly_program in
     323    ∀code_memory: M.
     324    ∀s: PreStatus M code_memory.
     325    ∀d: Byte.
     326    ∀v: Byte.
     327      Σp: PreStatus M code_memory.
     328        ∀M.
     329        ∀sigma.
     330        ∀policy.
     331        ∀s'.
     332        ∀v'.
     333          status_of_pseudo_status M code_memory s sigma policy = s' →
     334            map_address_Byte_using_internal_pseudo_address_map M sigma d v = v' →
     335              (set_bit_addressable_sfr (BitVectorTrie Byte 16)
     336                (code_memory_of_pseudo_assembly_program code_memory sigma policy) s' d v' =
     337              status_of_pseudo_status M code_memory
     338                (set_bit_addressable_sfr pseudo_assembly_program code_memory s d v) sigma policy).
    326339  whd in match map_address_Byte_using_internal_pseudo_address_map;
    327340  whd in match set_bit_addressable_sfr;
     
    346359         | _ ⇒ set_8051_sfr ?? s sfr v ]
    347360      | inr sfr ⇒ set_8052_sfr ?? s sfr v ]])
    348   normalize nodelta
     361  normalize nodelta #M #sigma #policy #s' #v' #s_refl <s_refl
    349362  /2 by refl, set_8051_sfr_status_of_pseudo_status, set_8052_sfr_status_of_pseudo_status/
    350   whd in match map_address_using_internal_pseudo_address_map; normalize nodelta //
     363  whd in match map_address_using_internal_pseudo_address_map; normalize nodelta
     364  #v_refl >v_refl //
    351365qed.
    352366
    353367lemma set_bit_addressable_sfr_status_of_pseudo_status:
    354368 ∀code_memory: pseudo_assembly_program. ∀s: PreStatus … code_memory. ∀d: Byte. ∀v: Byte.
    355   ∀M. ∀sigma. ∀policy. ∀v'.
     369  ∀M. ∀sigma. ∀policy. ∀s': Status ?. ∀v'.
     370  status_of_pseudo_status M code_memory s sigma policy = s' →
    356371  map_address_Byte_using_internal_pseudo_address_map M sigma d v = v' →
    357372 (set_bit_addressable_sfr (BitVectorTrie Byte 16)
    358373  (code_memory_of_pseudo_assembly_program code_memory sigma policy)
    359   (status_of_pseudo_status M code_memory s sigma policy) d v'
     374  s' d v'
    360375  =status_of_pseudo_status M code_memory
    361376   (set_bit_addressable_sfr pseudo_assembly_program code_memory s d v) sigma policy).
     
    365380
    366381lemma set_low_internal_ram_status_of_pseudo_status:
    367  ∀cm,sigma,policy,M,s,ram.
     382 ∀cm,sigma,policy,M,s,s',ram.
     383  status_of_pseudo_status M cm s sigma policy = s' →
    368384  set_low_internal_ram (BitVectorTrie Byte 16)
    369385  (code_memory_of_pseudo_assembly_program cm sigma policy)
    370   (status_of_pseudo_status M cm s sigma policy)
     386  s'
    371387  (low_internal_ram_of_pseudo_low_internal_ram M ram)
    372388  = status_of_pseudo_status M cm
    373389    (set_low_internal_ram pseudo_assembly_program cm s ram) sigma policy.
    374  //
     390  #cm #sigma #policy #M #s #s' #ram #s_refl <s_refl //
    375391qed.
    376392
     
    428444  bit_address_of_register … cm s r.
    429445 #M #cm #s #sigma #policy #r whd in ⊢ (??%%);
    430  >get_8051_sfr_status_of_pseudo_status
     446 >(get_8051_sfr_status_of_pseudo_status … (refl …))
    431447 @pair_elim #un #ln #_
    432448 @pair_elim #r1 #r0 #_ %
     
    458474
    459475lemma get_register_status_of_pseudo_status:
    460  ∀M,cm,sigma,policy,s,r.
     476 ∀M,cm,sigma,policy,s,s',r.
     477  status_of_pseudo_status M cm s sigma policy = s' →
    461478  get_register …
    462479   (code_memory_of_pseudo_assembly_program cm sigma policy)
    463    (status_of_pseudo_status M cm s sigma policy) r =
     480   s' r =
    464481  map_internal_ram_address_using_pseudo_address_map M sigma (false:::bit_address_of_register pseudo_assembly_program cm s r)
    465482   (get_register … cm s r).
    466  #M #cm #sigma #policy #s #r whd in match get_register; normalize nodelta
     483 #M #cm #sigma #policy #s #s' #r #s_refl <s_refl whd in match get_register; normalize nodelta
    467484 whd in match status_of_pseudo_status; normalize nodelta
    468485 >bit_address_of_register_status_of_pseudo_status
     
    490507
    491508lemma set_register_status_of_pseudo_status:
    492  ∀M,cm,s,sigma,policy,r,v,v'.
     509 ∀M,sigma,policy,cm,s,s',r,v,v'.
     510  status_of_pseudo_status M cm s sigma policy = s' →
    493511  map_internal_ram_address_using_pseudo_address_map M sigma
    494512   (false:::bit_address_of_register pseudo_assembly_program cm s r) v =v' →
    495513  set_register (BitVectorTrie Byte 16)
    496514   (code_memory_of_pseudo_assembly_program cm sigma policy)
    497    (status_of_pseudo_status M cm s sigma policy) r v'
     515   s' r v'
    498516  = status_of_pseudo_status M cm (set_register pseudo_assembly_program cm s r v)
    499517    sigma policy.
    500  #M #cm #s #sigma #policy #r #v #v' #v_ok
     518  #M #sigma #policy #cm #s #s' #r #v #v' #s_refl <s_refl #v_ok
    501519 whd in match set_register; normalize nodelta
    502520 >bit_address_of_register_status_of_pseudo_status
    503521 >(insert_low_internal_ram_status_of_pseudo_status … v_ok)
    504  @set_low_internal_ram_status_of_pseudo_status
     522 @set_low_internal_ram_status_of_pseudo_status %
    505523qed.
    506524
     
    572590  ∀ps.
    573591  ∀addr:[[ direct ; indirect ; registr ; acc_a ; acc_b ; ext_indirect ; ext_indirect_dptr ]].
    574   ∀value. Σp: PreStatus ? cm. ∀M. ∀sigma. ∀policy. ∀value'.
     592  ∀value. Σp: PreStatus ? cm. ∀M. ∀sigma. ∀policy. ∀s'. ∀value'.
     593   status_of_pseudo_status M cm ps sigma policy = s' →
    575594   map_address_mode_using_internal_pseudo_address_map_ok1 M cm ps sigma addr →
    576595   map_address_mode_using_internal_pseudo_address_map_ok2 … M sigma cm ps addr value = value' →
    577596    set_arg_8 (BitVectorTrie Byte 16)
    578597      (code_memory_of_pseudo_assembly_program cm sigma policy)
    579       (status_of_pseudo_status M cm ps sigma policy)
    580       addr value' =
     598      s' addr value' =
    581599    status_of_pseudo_status M cm (set_arg_8 … cm ps addr value) sigma policy.
    582600  whd in match set_arg_8; normalize nodelta
     
    628646          match other in False with [ ]
    629647      ] (subaddressing_modein … a)) normalize nodelta
    630   #M #sigma #policy #v'
     648  #M #sigma #policy #s' #v' #s_refl <s_refl
    631649  whd in match map_address_mode_using_internal_pseudo_address_map_ok1; normalize nodelta
    632650  whd in match map_address_mode_using_internal_pseudo_address_map_ok2; normalize nodelta
     
    636654    | #_ #v_ok >(insert_low_internal_ram_status_of_pseudo_status … v) // ]
    637655  |3,4: #EQ1 #EQ2 change with (get_register ????) in match register in p;
    638       >get_register_status_of_pseudo_status
     656      >(get_register_status_of_pseudo_status … (refl …))
    639657      whd in match map_internal_ram_address_using_pseudo_address_map; normalize nodelta
    640658      >EQ1 normalize nodelta >p normalize nodelta >p1 normalize nodelta
     
    642660      | >(insert_low_internal_ram_status_of_pseudo_status … v) ]
    643661      // <EQ2 @eq_f2 try % <(vsplit_ok … (sym_eq … p)) <eq_cons_head_append >p1 %
    644   |5: #EQ1 #EQ2 <EQ2 >get_register_status_of_pseudo_status
     662  |5: #EQ1 #EQ2 <EQ2 >(get_register_status_of_pseudo_status … (refl …))
    645663      whd in match map_internal_ram_address_using_pseudo_address_map; normalize nodelta
    646664      >EQ1 normalize nodelta
     
    649667  |7: #EQ1 #EQ2 <EQ2 /2 by set_8051_sfr_status_of_pseudo_status/
    650668  |8: #_ #EQ <EQ @set_8051_sfr_status_of_pseudo_status %
    651   |9: #_ #EQ <EQ >get_8051_sfr_status_of_pseudo_status >get_8051_sfr_status_of_pseudo_status
    652       >external_ram_status_of_pseudo_status @set_external_ram_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 …))
     671      >external_ram_status_of_pseudo_status @set_external_ram_status_of_pseudo_status ] %
    653672qed.
    654673
    655674lemma p1_latch_status_of_pseudo_status:
    656675    ∀M.
     676    ∀sigma.
     677    ∀policy.
    657678    ∀code_memory: pseudo_assembly_program.
    658679    ∀s: PreStatus … code_memory.
     680    ∀s'.
     681    (status_of_pseudo_status M code_memory s sigma policy) = s' →
     682    (p1_latch (BitVectorTrie Byte 16)
     683      (code_memory_of_pseudo_assembly_program code_memory sigma policy)
     684      s' =
     685    (p1_latch pseudo_assembly_program code_memory s)).
     686  #M #sigma #policy #code_memory #s #s' #s_refl <s_refl //
     687qed.
     688
     689lemma p3_latch_status_of_pseudo_status:
     690    ∀M.
    659691    ∀sigma.
    660692    ∀policy.
    661     (p1_latch (BitVectorTrie Byte 16)
    662       (code_memory_of_pseudo_assembly_program code_memory sigma policy)
    663       (status_of_pseudo_status M code_memory s sigma policy) =
    664     (p1_latch pseudo_assembly_program code_memory s)).
    665   //
    666 qed.
    667 
    668 lemma p3_latch_status_of_pseudo_status:
    669     ∀M.
    670693    ∀code_memory: pseudo_assembly_program.
    671694    ∀s: PreStatus … code_memory.
    672     ∀sigma.
    673     ∀policy.
     695    ∀s'.
     696    (status_of_pseudo_status M code_memory s sigma policy) = s' →
    674697    (p3_latch (BitVectorTrie Byte 16)
    675698      (code_memory_of_pseudo_assembly_program code_memory sigma policy)
    676699      (status_of_pseudo_status M code_memory s sigma policy) =
    677700    (p3_latch pseudo_assembly_program code_memory s)).
    678   //
     701  #M #sigma #policy #code_memory #s #s' #s_refl <s_refl //
    679702qed.
    680703
     
    685708    ∀d: Byte.
    686709    ∀l: bool.
    687       Σp: Byte. ∀M. ∀sigma. ∀policy.
     710      Σp: Byte. ∀M. ∀sigma. ∀policy. ∀s'.
     711        status_of_pseudo_status M code_memory s sigma policy = s' →
    688712        (get_bit_addressable_sfr (BitVectorTrie Byte 16)
    689713          (code_memory_of_pseudo_assembly_program code_memory sigma policy)
    690           (status_of_pseudo_status M code_memory s sigma policy) d l =
     714          s' d l =
    691715        map_address_Byte_using_internal_pseudo_address_map M sigma
    692716         d (get_bit_addressable_sfr pseudo_assembly_program code_memory s d l)).
     
    720744    ]
    721745    ])
    722   #M #sigma #policy normalize nodelta
    723   /by get_8051_sfr_status_of_pseudo_status, p1_latch_status_of_pseudo_status, p3_latch_status_of_pseudo_status/
     746  #M #sigma #policy #s' #s_refl <s_refl normalize nodelta
     747  /2 by get_8051_sfr_status_of_pseudo_status, p1_latch_status_of_pseudo_status, p3_latch_status_of_pseudo_status/
    724748qed.
    725749
     
    730754    ∀d: Byte.
    731755    ∀l: bool.
    732     ∀M. ∀sigma. ∀policy.
     756    ∀M. ∀sigma. ∀policy. ∀s'.
     757      (status_of_pseudo_status M code_memory s sigma policy) = s' →
    733758        (get_bit_addressable_sfr (BitVectorTrie Byte 16)
    734759          (code_memory_of_pseudo_assembly_program code_memory sigma policy)
    735           (status_of_pseudo_status M code_memory s sigma policy) d l =
     760          s' d l =
    736761        map_address_Byte_using_internal_pseudo_address_map M sigma
    737762         d (get_bit_addressable_sfr pseudo_assembly_program code_memory s d l)).
     
    741766
    742767lemma program_counter_status_of_pseudo_status:
     768    ∀M. ∀sigma. ∀policy.
    743769    ∀code_memory: pseudo_assembly_program.
    744770    ∀s: PreStatus ? code_memory.
    745     ∀M. ∀sigma. ∀policy.
     771    ∀s'.
     772    (status_of_pseudo_status M code_memory s sigma policy) = s' →
    746773      program_counter … (code_memory_of_pseudo_assembly_program code_memory sigma policy)
    747           (status_of_pseudo_status M code_memory s sigma policy) =
     774        s' =
    748775        sigma (program_counter … s).
    749   //
     776  #M #sigma #policy #code_memory #s #s' #s_refl <s_refl //
    750777qed.
    751778
    752779lemma get_cy_flag_status_of_pseudo_status:
    753   ∀M, cm, sigma, policy, s.
     780  ∀M, cm, sigma, policy, s, s'.
     781  (status_of_pseudo_status M cm s sigma policy) = s' →
    754782  (get_cy_flag (BitVectorTrie Byte 16)
    755783    (code_memory_of_pseudo_assembly_program cm sigma policy)
    756     (status_of_pseudo_status M cm s sigma policy) =
     784    s' =
    757785  get_cy_flag pseudo_assembly_program cm s).
    758   #M #cm #sigma #policy #s
     786  #M #cm #sigma #policy #s #s' #s_refl <s_refl
    759787  whd in match get_cy_flag; normalize nodelta
    760788  >get_index_v_status_of_pseudo_status %
     
    766794  ∀l.
    767795  ∀addr:[[ direct ; indirect ; registr ; acc_a ; acc_b ; data ; acc_dptr ; acc_pc ; ext_indirect ; ext_indirect_dptr ]].
    768     Σp: Byte. ∀M. ∀sigma. ∀policy.
     796    Σp: Byte. ∀M. ∀sigma. ∀policy. ∀s'.
     797      (status_of_pseudo_status M cm ps sigma policy) = s' →
    769798      map_address_mode_using_internal_pseudo_address_map_ok1 M cm ps sigma addr →
    770799      get_arg_8 (BitVectorTrie Byte 16) (code_memory_of_pseudo_assembly_program cm sigma policy)
    771       (status_of_pseudo_status M cm ps sigma policy) l addr =
     800      s' l addr =
    772801      map_address_mode_using_internal_pseudo_address_map_ok2 … M sigma cm ps addr (get_arg_8 … cm ps l addr).
    773802  whd in match get_arg_8; normalize nodelta
     
    816845        match other in False with [ ]
    817846      ] (subaddressing_modein … a)) normalize nodelta
    818   #M #sigma #policy
     847  #M #sigma #policy #s' #s_refl <s_refl
    819848  whd in match map_address_mode_using_internal_pseudo_address_map_ok1; normalize nodelta
    820849  whd in match map_address_mode_using_internal_pseudo_address_map_ok2; normalize nodelta
    821850  [1:
    822851    #_ >p normalize nodelta >p1 normalize nodelta
    823     @get_bit_addressable_sfr_status_of_pseudo_status
     852    @get_bit_addressable_sfr_status_of_pseudo_status %
    824853  |2:
    825854    #_>p normalize nodelta >p1 normalize nodelta
    826855    @lookup_low_internal_ram_of_pseudo_low_internal_ram
    827856  |3,4:
    828     #assoc_list_assm >get_register_status_of_pseudo_status
     857    #assoc_list_assm >(get_register_status_of_pseudo_status … (refl …))
    829858    whd in match map_internal_ram_address_using_pseudo_address_map in ⊢ (??%?); normalize nodelta
    830859    >assoc_list_assm normalize nodelta >p normalize nodelta >p1 normalize nodelta
     
    836865    @eq_f2 try % <(vsplit_ok … (sym_eq … p)) <eq_cons_head_append >p1 %
    837866  |5:
    838     #assoc_list_assm >get_register_status_of_pseudo_status
     867    #assoc_list_assm >(get_register_status_of_pseudo_status … (refl …))
    839868    whd in match map_internal_ram_address_using_pseudo_address_map in ⊢ (??%?); normalize nodelta
    840869    >assoc_list_assm normalize nodelta %
     
    842871    #_ /2/
    843872  |10:
    844     #acc_a_assm >get_8051_sfr_status_of_pseudo_status >get_8051_sfr_status_of_pseudo_status
    845     >get_8051_sfr_status_of_pseudo_status
     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 …))
    846876    whd in match map_address_using_internal_pseudo_address_map; normalize nodelta
    847877    >acc_a_assm >p normalize nodelta //
    848878  |11:
    849     * #map_acc_a_assm #sigma_assm >get_8051_sfr_status_of_pseudo_status >program_counter_status_of_pseudo_status
     879    * #map_acc_a_assm #sigma_assm >(get_8051_sfr_status_of_pseudo_status … (refl …))
     880    >(program_counter_status_of_pseudo_status … (refl …))
    850881    whd in match map_address_using_internal_pseudo_address_map; normalize nodelta
    851882    >sigma_assm >map_acc_a_assm >p normalize nodelta //
    852883  |12:
    853     #_ >get_8051_sfr_status_of_pseudo_status >get_8051_sfr_status_of_pseudo_status
     884    #_ >(get_8051_sfr_status_of_pseudo_status … (refl …))
     885    >(get_8051_sfr_status_of_pseudo_status … (refl …))
    854886    >external_ram_status_of_pseudo_status //
    855887  ]
     
    860892  ∀ps.
    861893  ∀addr: [[data16]].
    862   ∀M. ∀sigma. ∀policy.
     894  ∀M. ∀sigma. ∀policy. ∀s'.
     895    status_of_pseudo_status M cm ps sigma policy = s' →
    863896      get_arg_16 (BitVectorTrie Byte 16) (code_memory_of_pseudo_assembly_program cm sigma policy)
    864       (status_of_pseudo_status M cm ps sigma policy) addr =
     897      s' addr =
    865898      (get_arg_16 … cm ps addr).
    866   //
     899  #cm #ps #addr #M #sigma #policy #s' #s_refl <s_refl //
    867900qed.
    868901
     
    872905  ∀addr: [[dptr]].
    873906  ∀v: Word.
    874   ∀M. ∀sigma. ∀policy.
     907  ∀M. ∀sigma. ∀policy. ∀s'.
     908    status_of_pseudo_status M cm ps sigma policy = s' →
    875909      set_arg_16 (BitVectorTrie Byte 16) (code_memory_of_pseudo_assembly_program cm sigma policy)
    876       (status_of_pseudo_status M cm ps sigma policy) v addr =
     910      s' v addr =
    877911      status_of_pseudo_status M cm (set_arg_16 ? cm ps v addr) sigma policy.
    878   #cm #ps #addr #v #M #sigma #policy
     912  #cm #ps #addr #v #M #sigma #policy #s' #s_refl <s_refl
    879913  @(subaddressing_mode_elim … addr)
    880914  whd in match set_arg_16; normalize nodelta
    881915  whd in match set_arg_16'; normalize nodelta
    882916  @(vsplit_elim bool ???) #bu #bl #bu_bl_refl normalize nodelta
    883   >(set_8051_sfr_status_of_pseudo_status … bu)
    884   [1: >(set_8051_sfr_status_of_pseudo_status … bl) ]
    885   //
     917  @set_8051_sfr_status_of_pseudo_status try % @sym_eq
     918  @set_8051_sfr_status_of_pseudo_status %
    886919qed.
    887920
     
    928961  ∀addr: [[bit_addr; n_bit_addr; carry]].
    929962  ∀l.
    930     Σb: bool. ∀M. ∀sigma. ∀policy.
     963    Σb: bool. ∀M. ∀sigma. ∀policy. ∀s'.
     964      status_of_pseudo_status M cm ps sigma policy = s' →
    931965      map_bit_address_mode_using_internal_pseudo_address_map_get M cm ps sigma addr l →
    932966      get_arg_1 (BitVectorTrie Byte 16) (code_memory_of_pseudo_assembly_program cm sigma policy)
    933       (status_of_pseudo_status M cm ps sigma policy) addr l =
     967      s' addr l =
    934968      (get_arg_1 … cm ps addr l).
    935969  whd in match get_arg_1; normalize nodelta
     
    9781012      ] (subaddressing_modein … a)) normalize nodelta
    9791013  try @modulus_less_than
    980   #M #sigma #policy
     1014  #M #sigma #policy #s' #s_refl <s_refl
    9811015  [1:
    982     #_ @get_cy_flag_status_of_pseudo_status
     1016    #_ >(get_cy_flag_status_of_pseudo_status … (refl …)) %
    9831017  |2,4:
    9841018    whd in ⊢ (% → ?); >p normalize nodelta >p1 normalize nodelta
    985     >get_bit_addressable_sfr_status_of_pseudo_status #map_address_assm
     1019    >(get_bit_addressable_sfr_status_of_pseudo_status … (refl …)) #map_address_assm
    9861020    >map_address_assm %
    9871021  |3,5:
     
    9981032  ∀addr: [[bit_addr; n_bit_addr; carry]].
    9991033  ∀l.
    1000   ∀M. ∀sigma. ∀policy.
     1034  ∀M. ∀sigma. ∀policy. ∀s'.
     1035    status_of_pseudo_status M cm ps sigma policy = s' →
    10011036      map_bit_address_mode_using_internal_pseudo_address_map_get M cm ps sigma addr l →
    10021037      get_arg_1 (BitVectorTrie Byte 16) (code_memory_of_pseudo_assembly_program cm sigma policy)
    1003       (status_of_pseudo_status M cm ps sigma policy) addr l =
     1038      s' addr l =
    10041039      (get_arg_1 … cm ps addr l).
    10051040  #cm #ps #addr #l
     
    10761111  ∀addr: [[bit_addr; carry]].
    10771112  ∀b: Bit.
    1078     Σp: PreStatus … cm. ∀M. ∀sigma. ∀policy.
     1113    Σp: PreStatus … cm. ∀M. ∀sigma. ∀policy. ∀s'.
     1114      status_of_pseudo_status M cm ps sigma policy = s' →
    10791115      map_bit_address_mode_using_internal_pseudo_address_map_set_1 M cm ps sigma addr b →
    10801116      map_bit_address_mode_using_internal_pseudo_address_map_set_2 M cm ps sigma addr b →
    10811117        set_arg_1 (BitVectorTrie Byte 16)
    10821118          (code_memory_of_pseudo_assembly_program cm sigma policy)
    1083           (status_of_pseudo_status M cm ps sigma policy) addr b =
     1119          s' addr b =
    10841120        status_of_pseudo_status M cm (set_arg_1 … cm ps addr b) sigma policy.
    10851121  whd in match set_arg_1; normalize nodelta
     
    11211157            [ ]
    11221158      ] (subaddressing_modein … a)) normalize nodelta
    1123   try @modulus_less_than #M #sigma #policy
     1159  try @modulus_less_than #M #sigma #policy #s' #s_refl <s_refl
    11241160  [1:
    1125     #_ #_ >get_8051_sfr_status_of_pseudo_status
     1161    #_ #_ >(get_8051_sfr_status_of_pseudo_status … (refl …))
    11261162    whd in match map_address_using_internal_pseudo_address_map; normalize nodelta
    11271163    >p normalize nodelta @set_8051_sfr_status_of_pseudo_status %
    11281164  |2,3:
    1129     >get_8051_sfr_status_of_pseudo_status
     1165    >(get_8051_sfr_status_of_pseudo_status … (refl …))
    11301166    whd in match map_address_using_internal_pseudo_address_map; normalize nodelta
    11311167    >p normalize nodelta >p1 normalize nodelta
    11321168    #map_bit_address_assm_1 #map_bit_address_assm_2
    11331169    [1:
    1134       >get_bit_addressable_sfr_status_of_pseudo_status
     1170      >(get_bit_addressable_sfr_status_of_pseudo_status … (refl …))
    11351171      >map_bit_address_assm_1
    11361172      >(set_bit_addressable_sfr_status_of_pseudo_status cm s … map_bit_address_assm_2) %
     
    11461182
    11471183lemma clock_status_of_pseudo_status:
    1148  ∀M,cm,sigma,policy,s.
     1184 ∀M,cm,sigma,policy,s,s'.
     1185  (status_of_pseudo_status M cm s sigma policy) = s' →
    11491186  clock …
    11501187   (code_memory_of_pseudo_assembly_program cm sigma policy)
    1151    (status_of_pseudo_status M cm s sigma policy)
     1188   s'
    11521189  = clock … cm s.
    1153 //
     1190  #M #cm #sigma #policy #s #s' #s_refl <s_refl //
    11541191qed.
    11551192
    11561193lemma set_clock_status_of_pseudo_status:
    1157  ∀M,cm,sigma,policy,s,v.
     1194 ∀M,cm,sigma,policy,s,s',v,v'.
     1195 status_of_pseudo_status M cm s sigma policy = s' →
     1196 v = v' →
    11581197  set_clock …
    11591198   (code_memory_of_pseudo_assembly_program cm sigma policy)
    1160    (status_of_pseudo_status M cm s sigma policy) v
    1161   = status_of_pseudo_status M cm (set_clock … cm s v) sigma policy.
    1162 //
    1163 qed.
     1199   s' v
     1200  = status_of_pseudo_status M cm (set_clock … cm s v') sigma policy.
     1201  #M #cm #sigma #policy #s #s' #v #v' #s_refl #v_refl <s_refl <v_refl //
     1202qed.
Note: See TracChangeset for help on using the changeset viewer.