include "ASM/Status.ma".

(* clock_set_bit_addressable_sfr defined in ASM/Status.ma *)

lemma clock_set_low_internal_ram:
  ∀M: Type[0]. ∀cm.
  ∀s: PreStatus M cm.
  ∀ram: BitVectorTrie Byte 7.
    clock M cm (set_low_internal_ram … s ram) = clock M cm s.
  //
qed.

lemma clock_set_high_internal_ram:
  ∀m: Type[0]. ∀cm.
  ∀s: PreStatus m cm.
  ∀ram: BitVectorTrie Byte 7.
    clock ?? (set_high_internal_ram … s ram) = clock … s.
  //
qed.

lemma clock_write_at_stack_pointer:
  ∀m: Type[0].
  ∀cm:m.
  ∀s: PreStatus m cm.
  ∀v: Byte.
    clock ?? (write_at_stack_pointer … s v) = clock ?? s.
  #m #s #v
  whd in match write_at_stack_pointer; normalize nodelta
  cases(vsplit … 4 4 ?) #nu #nl normalize nodelta
  cases(get_index_v … 4 nu 0 ?) //
qed.

lemma clock_set_clock:
  ∀M: Type[0]. ∀cm.
  ∀s: PreStatus M cm.
  ∀v.
    clock ?? (set_clock … s v) = v.
 //
qed.

lemma clock_set_program_counter:
  ∀M: Type[0]. ∀cm.
  ∀s: PreStatus M cm.
  ∀pc: Word.
    clock M cm (set_program_counter … s pc) = clock … s.
  //
qed.

lemma clock_set_8051_sfr:
  ∀M: Type[0]. ∀cm.
  ∀s: PreStatus M cm.
  ∀sfr: SFR8051.
  ∀v: Byte.
    clock ?? (set_8051_sfr … s sfr v) = clock … s.
 //
qed.

lemma clock_set_flags:
 ∀M,cm,s,f1,f2,f3. clock M cm s = clock … (set_flags … s f1 f2 f3).
//
qed.

lemma get_register_set_program_counter:
 ∀T,cm,s,pc. get_register T cm (set_program_counter … s pc) = get_register … s.
 //
qed.

lemma get_8051_sfr_set_program_counter:
 ∀T,cm,s,pc. get_8051_sfr T cm (set_program_counter … s pc) = get_8051_sfr … s.
 //
qed.

lemma get_bit_addressable_sfr_set_program_counter:
 ∀T,cm,s,pc. get_bit_addressable_sfr T cm (set_program_counter … s pc) = get_bit_addressable_sfr … s.
 //
qed.

lemma low_internal_ram_set_program_counter:
 ∀T,cm,s,pc. low_internal_ram T cm (set_program_counter … s pc) = low_internal_ram … s.
 //
qed.

lemma get_arg_8_set_program_counter:
 ∀n.∀l:Vector addressing_mode_tag (S n).
  ∀T,cm,s,pc,b.∀arg:l.
   ∀prf:is_in ?
    [[direct;indirect;registr;acc_a;acc_b;data;acc_dptr;ext_indirect;ext_indirect_dptr]] arg.
   get_arg_8 T cm (set_program_counter … s pc) b arg = get_arg_8 … s b arg.
 [ #n #l #T #cm #s #pc #b * *; #X try (#Y #H) try #H try % @⊥ @H
 | cases arg in prf; *; normalize //
 | skip ]
qed.

(*
lemma set_bit_addressable_sfr_set_code_memory:
  ∀T, U: Type[0].
  ∀ps: PreStatus ?.
  ∀code_mem.
  ∀x.
  ∀val.
  set_bit_addressable_sfr ? (set_code_memory T U ps code_mem) x val =
  set_code_memory T U (set_bit_addressable_sfr ? ps x val) code_mem.
  #T #U #ps #code_mem #x #val
  whd in ⊢ (??%?);
  whd in ⊢ (???(???%?));
  cases (eqb ? 128) [ normalize nodelta cases not_implemented
  | normalize nodelta
  cases (eqb (nat_of_bitvector 8 x) ?) [ normalize nodelta cases not_implemented
  | normalize nodelta
  cases (eqb (nat_of_bitvector 8 x) ?) [ normalize nodelta cases not_implemented
  | normalize nodelta
  cases (eqb ? 176) [ normalize nodelta %
  | normalize nodelta
  cases (eqb ? 153) [ normalize nodelta %
  | normalize nodelta
  cases (eqb ? 138) [ normalize nodelta %
  | normalize nodelta
  cases (eqb ? 139) [ normalize nodelta %
  | normalize nodelta
  cases (eqb ? 140) [ normalize nodelta %
  | normalize nodelta
  cases (eqb ? 141) [ normalize nodelta %
  | normalize nodelta
  cases (eqb ? 200) [ normalize nodelta %
  | normalize nodelta
  cases (eqb ? 202) [ normalize nodelta %
  | normalize nodelta
  cases (eqb ? 203) [ normalize nodelta %
  | normalize nodelta
  cases (eqb ? 204) [ normalize nodelta % 
  | normalize nodelta
  cases (eqb ? 205) [ normalize nodelta % 
  | normalize nodelta
  cases (eqb ? 135) [ normalize nodelta % 
  | normalize nodelta
  cases (eqb ? 136) [ normalize nodelta % 
  | normalize nodelta
  cases (eqb ? 137) [ normalize nodelta % 
  | normalize nodelta
  cases (eqb ? 152) [ normalize nodelta % 
  | normalize nodelta
  cases (eqb ? 168) [ normalize nodelta % 
  | normalize nodelta
  cases (eqb ? 184) [ normalize nodelta % 
  | normalize nodelta
  cases (eqb ? 129) [ normalize nodelta % 
  | normalize nodelta
  cases (eqb ? 130) [ normalize nodelta % 
  | normalize nodelta
  cases (eqb ? 131) [ normalize nodelta % 
  | normalize nodelta
  cases (eqb ? 208) [ normalize nodelta %
  | normalize nodelta
  cases (eqb ? 224) [ normalize nodelta % 
  | normalize nodelta
  cases (eqb ? 240) [ normalize nodelta % 
  | normalize nodelta
    cases not_implemented
  ]]]]]]]]]]]]]]]]]]]]]]]]]]
qed.

example set_arg_8_set_code_memory:
  ∀n:nat.
  ∀l:Vector addressing_mode_tag (S n).
    ∀T: Type[0].
    ∀U: Type[0].
    ∀ps: PreStatus ?.
    ∀code_mem.
    ∀val.
    ∀b: l.
    ∀prf:is_in ?
     [[direct;indirect;registr;acc_a;acc_b;ext_indirect;ext_indirect_dptr]] b. 
  set_arg_8 ? (set_code_memory T U ps code_mem) b val =
  set_code_memory T U (set_arg_8 ? ps b val) code_mem.
  [2,3: cases b in prf; *; normalize //]
  #n #l #T #U #ps #code_mem #val * *;
  #x try (#y #H) try #H whd in H; try cases H try %
  whd in match set_arg_8; normalize nodelta
  whd in match set_arg_8'; normalize nodelta
  cases (vsplit bool 4 4 ?) #nu' #nl' normalize nodelta
  cases (vsplit bool 1 3 nu') #bit1' #ignore' normalize nodelta
  cases (get_index_v bool 4 nu' 0 ?) normalize nodelta
  try % @set_bit_addressable_sfr_set_code_memory
qed. *)

lemma set_arg_8_set_program_counter:
  ∀n:nat.
  ∀l:Vector addressing_mode_tag (S n).
    ∀T: Type[0]. ∀cm.
    ∀ps: PreStatus ? cm.
    ∀pc.
    ∀val.
    ∀b: l.
    ∀prf:is_in ?
     [[direct;indirect;registr;acc_a;acc_b;ext_indirect;ext_indirect_dptr]] b.
  set_arg_8 … (set_program_counter T cm ps pc) b val =
  set_program_counter T cm (set_arg_8 ?? ps b val) pc.
  [2,3: cases b in prf; *; normalize //]
  #n #l #T #cm #ps #pc #val * *;
  #x try (#y #H) try #H whd in H; try cases H try %
  whd in match set_arg_8; normalize nodelta
  cases (vsplit bool ???) #bit_one #seven_bits normalize nodelta
  cases (head' bool ??) normalize nodelta
  try % cases daemon (* XXX: need @(set_bit_addressable_sfr_set_program_counter) *)
qed.
  
(*lemma get_arg_8_set_code_memory:
 ∀T1,T2,s,code_mem,b,arg.
   get_arg_8 T1 (set_code_memory T2 T1 s code_mem) b arg = get_arg_8 … s b arg.
 #T1 #T2 #s #code_mem #b #arg %
qed.

lemma set_code_memory_set_flags:
 ∀T1,T2,s,f1,f2,f3,code_mem.
  set_code_memory T1 T2 (set_flags T1 s f1 f2 f3) code_mem =
   set_flags … (set_code_memory … s code_mem) f1 f2 f3.
 #T1 #T2 #s #f1 #f2 #f3 #code_mem %
qed.*)

lemma set_program_counter_set_flags:
 ∀T1,cm,s,f1,f2,f3,pc.
  set_program_counter T1 cm (set_flags T1 cm s f1 f2 f3) pc =
   set_flags … (set_program_counter … s pc) f1 f2 f3.
 //
qed.

lemma program_counter_set_flags:
 ∀T1,cm,s,f1,f2,f3.
  program_counter T1 cm (set_flags T1 cm s f1 f2 f3) = program_counter … s.
 //
qed.

lemma special_function_registers_8051_write_at_stack_pointer:
 ∀T,cm,s,x.
    special_function_registers_8051 T cm (write_at_stack_pointer T cm s x)
  = special_function_registers_8051 T cm s.
 #T #cm #s #x whd in ⊢ (??(???%)?);
 cases (vsplit ????) #nu #nl normalize nodelta;
 cases (get_index_v bool ????) %
qed.

lemma get_8051_sfr_write_at_stack_pointer:
 ∀T,cm,s,x,y. get_8051_sfr T cm (write_at_stack_pointer T cm s x) y = get_8051_sfr T cm s y.
 #T #cm #s #x #y whd in ⊢ (??%%); >special_function_registers_8051_write_at_stack_pointer @refl
qed.

(*lemma code_memory_write_at_stack_pointer:
 ∀T,s,x. code_memory T (write_at_stack_pointer T s x) = code_memory T s.
 #T #s #x whd in ⊢ (??(??%)?);
 cases (vsplit ????) #nu #nl normalize nodelta;
 cases (get_index_v bool ????) %
qed.*)

lemma set_program_counter_set_low_internal_ram:
 ∀T,cm,s,x,y.
  set_program_counter T cm (set_low_internal_ram … s x) y =
   set_low_internal_ram … (set_program_counter … s y) x.
 //
qed.

lemma set_clock_set_low_internal_ram:
 ∀T,cm,s,x,y.
  set_clock T cm (set_low_internal_ram … s x) y =
   set_low_internal_ram … (set_clock … s y) x.
 //
qed.

lemma set_program_counter_set_high_internal_ram:
 ∀T,cm,s,x,y.
  set_program_counter T cm (set_high_internal_ram … s x) y =
   set_high_internal_ram … (set_program_counter … s y) x.
 //
qed.

lemma set_clock_set_high_internal_ram:
 ∀T,cm,s,x,y.
  set_clock T cm (set_high_internal_ram … s x) y =
   set_high_internal_ram … (set_clock … s y) x.
 //
qed.

lemma set_clock_set_program_counter:
  ∀T,cm,s,x,y.
    set_clock T cm (set_program_counter … s x) y =
      set_program_counter … (set_clock … s y) x.
 //
qed.

lemma set_low_internal_ram_set_high_internal_ram:
 ∀T,cm,s,x,y.
  set_low_internal_ram T cm (set_high_internal_ram … s x) y =
   set_high_internal_ram … (set_low_internal_ram … s y) x.
 //
qed.

lemma external_ram_write_at_stack_pointer:
 ∀T,cm,s,x. external_ram T cm (write_at_stack_pointer T cm s x) = external_ram T cm s.
 #T #cm #s #x whd in ⊢ (??(???%)?);
 cases (vsplit ????) #nu #nl normalize nodelta;
 cases (get_index_v bool ????) %
qed.

lemma special_function_registers_8052_write_at_stack_pointer:
 ∀T,cm,s,x.
    special_function_registers_8052 T cm (write_at_stack_pointer T cm s x)
  = special_function_registers_8052 T cm s.
 #T #cm #s #x whd in ⊢ (??(???%)?);
 cases (vsplit ????) #nu #nl normalize nodelta;
 cases (get_index_v bool ????) %
qed.

lemma p1_latch_write_at_stack_pointer:
 ∀T,cm,s,x. p1_latch T cm (write_at_stack_pointer T cm s x) = p1_latch T cm s.
 #T #cm #s #x whd in ⊢ (??(???%)?);
 cases (vsplit ????) #nu #nl normalize nodelta;
 cases (get_index_v bool ????) %
qed.

lemma p3_latch_write_at_stack_pointer:
 ∀T,cm,s,x. p3_latch T cm (write_at_stack_pointer T cm s x) = p3_latch T cm s.
 #T #cm #s #x whd in ⊢ (??(???%)?);
 cases (vsplit ????) #nu #nl normalize nodelta;
 cases (get_index_v bool ????) %
qed.

axiom get_index_v_set_index:
 ∀T,n,x,m,p,y. get_index_v T n (set_index T n x m y p) m p = y.

lemma get_8051_sfr_set_8051_sfr:
 ∀T,cm,s,x,y. get_8051_sfr T cm (set_8051_sfr … s x y) x = y.
 #T #cm * #A #B #C #D #E #F #G #H #I * #y whd in ⊢ (??(???%?)?);
 whd in match get_8051_sfr; normalize nodelta @get_index_v_set_index
qed.

lemma program_counter_set_8051_sfr:
 ∀T,cm,s,x,y. program_counter T cm (set_8051_sfr … s x y) = program_counter … s.
 //
qed.

axiom program_counter_set_bit_addressable_sfr:
  ∀m, cm, s, addr, v.
   program_counter m cm (set_bit_addressable_sfr m cm s addr v) = program_counter m cm s.

lemma program_counter_set_arg_8:
  ∀m, cm, s, addr, v.
   program_counter m cm (set_arg_8 m cm s addr v) = program_counter m cm s.
  #m #cm #s #addr #byte
  whd in match set_arg_8; normalize nodelta
  cases daemon (*
  whd in match set_arg_8'; normalize nodelta
  cases addr #subaddressing_modein_proof
  cases subaddressing_modein_proof
  try (#addr normalize in addr; cases addr)
  try (#ignore #addr normalize in addr; cases addr)
  normalize nodelta try #_ try /demod/ try %
  cases (vsplit bool 4 4 ?) #nu #nl normalize nodelta
  cases (vsplit bool 1 3 ?) #ignore #three_bits normalize nodelta
  cases (get_index_v bool 4 nu ? ?) normalize nodelta try /demod/ try % *)
qed.

(* XXX: this was compiling before! *)
lemma program_counter_set_arg_1:
  ∀m, cm, s, addr, v.
   program_counter m cm (set_arg_1 m cm s addr v) = program_counter m cm s.
  #m #cm #s #addr #v
  whd in match set_arg_1; normalize nodelta
  cases daemon (*
  whd in match set_arg_1'; normalize nodelta
  cases addr #subaddressing_modein_proof
  cases subaddressing_modein_proof
  try (#ignore #addr normalize in addr; cases addr)
  try (#addr normalize in addr; cases addr)
  normalize nodelta
  cases (vsplit bool 4 4 ?) #nu #nl normalize nodelta try /demod/ try %
  cases (vsplit bool 1 3 ?) #ignore #three_bits normalize nodelta
  cases (get_index_v bool 4 nu ??) normalize nodelta
  (* XXX: try /demod/ try % *)
  cases daemon *)
qed.

lemma program_counter_set_arg_16:
  ∀m, cm, s, addr, v.
   program_counter m cm (set_arg_16 m cm s v addr) = program_counter m cm s.
  #m #cm #s #addr #v
  whd in match set_arg_16; normalize nodelta
  whd in match set_arg_16'; normalize nodelta
  cases addr #subaddressing_modein_proof
  cases subaddressing_modein_proof
  try (#ignore #addr normalize in addr; cases addr)
  try (#addr normalize in addr; cases addr)
  normalize nodelta
  cases (vsplit bool 8 8 v) #bu #bl normalize nodelta /demod/ %
qed.

lemma program_counter_set_low_internal_ram:
  ∀m, cm, s, v.
   program_counter m cm (set_low_internal_ram m cm s v) = program_counter m cm s.
  #m #cm #s #v
  whd in match set_low_internal_ram; normalize nodelta %
qed.

lemma program_counter_set_high_internal_ram:
  ∀m, cm, s, v.
   program_counter m cm (set_high_internal_ram m cm s v) = program_counter m cm s.
  #m #cm #s #v
  whd in match set_high_internal_ram; normalize nodelta %
qed.

lemma program_counter_write_at_stack_pointer:
  ∀m, cm, s, v.
   program_counter m cm (write_at_stack_pointer m cm s v) = program_counter m cm s.
  #m #cm #s #v
  whd in match write_at_stack_pointer; normalize nodelta
  cases (vsplit bool 4 4 ?) #nu #nl normalize nodelta
  cases (get_index_v bool 4 nu ??) normalize nodelta /demod/ %
qed.

axiom get_arg_8_set_low_internal_ram:
  ∀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.

lemma split_eq_status:
 ∀T,cm.
 ∀A1,A2,A3,A4,A5,A6,A7,A8,A9.
 ∀B1,B2,B3,B4,B5,B6,B7,B8,B9.
  A1=B1 → A2=B2 → A3=B3 → A4=B4 → A5=B5 → A6=B6 → A7=B7 → A8=B8 → A9=B9 →
   mk_PreStatus T cm A1 A2 A3 A4 A5 A6 A7 A8 A9 =
   mk_PreStatus T cm B1 B2 B3 B4 B5 B6 B7 B8 B9.
 //
qed.