Ignore:
Timestamp:
Feb 20, 2012, 10:04:54 AM (8 years ago)
Author:
mulligan
Message:

changes from friday afternoon

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/StatusProofs.ma

    r1666 r1710  
    333333qed.
    334334
     335axiom program_counter_set_bit_addressable_sfr:
     336  ∀m, cm, s, addr, v.
     337   program_counter m cm (set_bit_addressable_sfr m cm s addr v) = program_counter m cm s.
     338
     339(* XXX: to be moved elsewhere *)
     340lemma program_counter_set_arg_8:
     341  ∀m, cm, s, addr, v.
     342   program_counter m cm (set_arg_8 m cm s addr v) = program_counter m cm s.
     343  #m #cm #s #addr #byte
     344  whd in match set_arg_8; normalize nodelta
     345  whd in match set_arg_8'; normalize nodelta
     346  cases addr #subaddressing_modein_proof
     347  cases subaddressing_modein_proof
     348  try (#addr normalize in addr; cases addr)
     349  try (#ignore #addr normalize in addr; cases addr)
     350  normalize nodelta try #_ try /demod/ try %
     351  cases (split bool 4 4 ?) #nu #nl normalize nodelta
     352  cases (split bool 1 3 ?) #ignore #three_bits normalize nodelta
     353  cases (get_index_v bool 4 nu ? ?) normalize nodelta try /demod/ try %
     354qed.
     355
     356lemma program_counter_set_arg_1:
     357  ∀m, cm, s, addr, v.
     358   program_counter m cm (set_arg_1 m cm s addr v) = program_counter m cm s.
     359  #m #cm #s #addr #v
     360  whd in match set_arg_1; normalize nodelta
     361  whd in match set_arg_1'; normalize nodelta
     362  cases addr #subaddressing_modein_proof
     363  cases subaddressing_modein_proof
     364  try (#ignore #addr normalize in addr; cases addr)
     365  try (#addr normalize in addr; cases addr)
     366  normalize nodelta
     367  cases (split bool 4 4 ?) #nu #nl normalize nodelta try /demod/ try %
     368  cases (split bool 1 3 ?) #ignore #three_bits normalize nodelta
     369  cases (get_index_v bool 4 nu ??) normalize nodelta try /demod/ try %
     370qed.
     371
     372lemma program_counter_set_arg_16:
     373  ∀m, cm, s, addr, v.
     374   program_counter m cm (set_arg_16 m cm s v addr) = program_counter m cm s.
     375  #m #cm #s #addr #v
     376  whd in match set_arg_16; normalize nodelta
     377  whd in match set_arg_16'; normalize nodelta
     378  cases addr #subaddressing_modein_proof
     379  cases subaddressing_modein_proof
     380  try (#ignore #addr normalize in addr; cases addr)
     381  try (#addr normalize in addr; cases addr)
     382  normalize nodelta
     383  cases (split bool 8 8 v) #bu #bl normalize nodelta /demod/ %
     384qed.
     385
     386lemma program_counter_set_low_internal_ram:
     387  ∀m, cm, s, v.
     388   program_counter m cm (set_low_internal_ram m cm s v) = program_counter m cm s.
     389  #m #cm #s #v
     390  whd in match set_low_internal_ram; normalize nodelta %
     391qed.
     392
     393lemma program_counter_set_high_internal_ram:
     394  ∀m, cm, s, v.
     395   program_counter m cm (set_high_internal_ram m cm s v) = program_counter m cm s.
     396  #m #cm #s #v
     397  whd in match set_high_internal_ram; normalize nodelta %
     398qed.
     399
     400lemma program_counter_write_at_stack_pointer:
     401  ∀m, cm, s, v.
     402   program_counter m cm (write_at_stack_pointer m cm s v) = program_counter m cm s.
     403  #m #cm #s #v
     404  whd in match write_at_stack_pointer; normalize nodelta
     405  cases (split bool 4 4 ?) #nu #nl normalize nodelta
     406  cases (get_index_v bool 4 nu ??) normalize nodelta /demod/ %
     407qed.
     408
    335409axiom get_arg_8_set_low_internal_ram:
    336  ∀M,cm,s,x,b,z. get_arg_8 M cm (set_low_internal_ram … s x) b z = get_arg_8 … s b z.
     410  ∀M,cm,s,x,b,z.
     411    get_arg_8 M cm (set_low_internal_ram … s x) b z = get_arg_8 … s b z.
    337412
    338413lemma split_eq_status:
Note: See TracChangeset for help on using the changeset viewer.