Ignore:
Timestamp:
Jul 10, 2012, 2:39:38 PM (8 years ago)
Author:
mulligan
Message:

Moved new versions of get_ / set_arg_* into Status.ma. Commented out proofs that are no longer working.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/StatusProofs.ma

    r2124 r2172  
    200200  #x try (#y #H) try #H whd in H; try cases H try %
    201201  whd in match set_arg_8; normalize nodelta
    202   whd in match set_arg_8'; normalize nodelta
    203   cases (vsplit bool 4 4 ?) #nu' #nl' normalize nodelta
    204   cases (vsplit bool 1 3 nu') #bit1' #ignore' normalize nodelta
    205   cases (get_index_v bool 4 nu' 0 ?) normalize nodelta
    206   try % cases daemon (*@(set_bit_addressable_sfr_set_program_counter)*)
     202  cases (vsplit bool ???) #bit_one #seven_bits normalize nodelta
     203  cases (head' bool ??) normalize nodelta
     204  try % cases daemon (* XXX: need @(set_bit_addressable_sfr_set_program_counter) *)
    207205qed.
    208206 
     
    349347  #m #cm #s #addr #byte
    350348  whd in match set_arg_8; normalize nodelta
     349  cases daemon (*
    351350  whd in match set_arg_8'; normalize nodelta
    352351  cases addr #subaddressing_modein_proof
     
    357356  cases (vsplit bool 4 4 ?) #nu #nl normalize nodelta
    358357  cases (vsplit bool 1 3 ?) #ignore #three_bits normalize nodelta
    359   cases (get_index_v bool 4 nu ? ?) normalize nodelta try /demod/ try %
     358  cases (get_index_v bool 4 nu ? ?) normalize nodelta try /demod/ try % *)
    360359qed.
    361360
     
    366365  #m #cm #s #addr #v
    367366  whd in match set_arg_1; normalize nodelta
     367  cases daemon (*
    368368  whd in match set_arg_1'; normalize nodelta
    369369  cases addr #subaddressing_modein_proof
     
    376376  cases (get_index_v bool 4 nu ??) normalize nodelta
    377377  (* XXX: try /demod/ try % *)
    378   cases daemon
     378  cases daemon *)
    379379qed.
    380380
Note: See TracChangeset for help on using the changeset viewer.