source: src/ASM/AssemblyProof.ma @ 836

include "ASM/Assembly.ma".
include "ASM/Interpret.ma".

let rec encoding_check (code_memory: BitVectorTrie Byte 16) (pc: Word) (final_pc: Word)
                       (encoding: list Byte) on encoding: Prop ≝
  match encoding with
  [ nil ⇒ final_pc = pc
  | cons hd tl ⇒
    let 〈new_pc, byte〉 ≝ next code_memory pc in
      hd = byte ∧ encoding_check code_memory new_pc final_pc tl
  ].

(*
definition assembly_specification:
  ∀sigma: Word → Word. ∀assembly_program: pseudo_assembly_program.
  ∀code_mem: BitVectorTrie Byte 16. Prop ≝
  λsigma.
  λpseudo_assembly_program.
  λcode_mem.
    ∀pc: Word.
      let 〈preamble, instr_list〉 ≝ pseudo_assembly_program in
      let 〈pre_instr, pre_new_pc〉 ≝ fetch_pseudo_instruction instr_list pc in
      let address_of ≝ ? in
      let labels ≝ λx. sigma (address_of_word_labels_code_mem instr_list x) in
      let datalabels ≝ λx. sigma (lookup ? ? x (construct_datalabels preamble) (zero ?)) in
      let pre_assembled ≝ assembly_1_pseudoinstruction labels datalabels address_of 〈None ?, pre_instr〉 in
        encoding_check code_mem pc (sigma pre_new_pc) pre_assembled.
      cases not_implemented
qed.

axiom assembly_meets_specification:
  ∀pseudo_assembly_program.
    match assembly pseudo_assembly_program with
    [ None ⇒ True
    | Some code_mem_cost ⇒
      let 〈code_mem, cost〉 ≝ code_mem_cost in
        assembly_specification ? pseudo_assembly_program (load_code_memory code_mem)
    ].
cases not_implemented (*
  # PROGRAM
  [ cases PROGRAM
    # PREAMBLE
    # INSTR_LIST
    elim INSTR_LIST
    [ whd
      whd in ⊢ (∀_. %)
      # PC
      whd
    | # INSTR
      # INSTR_LIST_TL
      # H
      whd
      whd in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ?])
    ]
  | cases not_implemented
  ] *)
qed.
*)

axiom sigma: pseudo_assembly_program → Word → Word.

(*
definition status_of_pseudo_status: PseudoStatus → option Status ≝
 λps.
  let pap ≝ code_memory … ps in
   match assembly pap with
    [ None ⇒ None …
    | Some p ⇒
       let cm ≝ load_code_memory (\fst p) in
       let pc ≝ sigma pap (program_counter ? ps) in
        Some …
         (mk_PreStatus (BitVectorTrie Byte 16)
           cm
           (low_internal_ram … ps)
           (high_internal_ram … ps)
           (external_ram … ps)
           pc
           (special_function_registers_8051 … ps)
           (special_function_registers_8052 … ps)
           (p1_latch … ps)
           (p3_latch … ps)
           (clock … ps)) ].
*)

(* RUSSEL **)

include "basics/jmeq.ma".

definition inject : ∀A.∀P:A → Prop.∀a.∀p:P a.Σx:A.P x ≝ λA,P,a,p. dp … a p.
definition eject : ∀A.∀P: A → Prop.(Σx:A.P x) → A ≝ λA,P,c.match c with [ dp w p ⇒ w].

coercion inject : ∀A.∀P:A → Prop.∀a.∀p:P a.Σx:A.P x ≝ inject on a:? to Σx:?.?.
coercion eject : ∀A.∀P:A → Prop.∀c:Σx:A.P x.A ≝ eject on _c:Σx:?.? to ?.

lemma sig2: ∀A.∀P:A → Prop. ∀p:Σx:A.P x. P (eject … p).
 #A #P #p cases p #w #q @q
qed.

(* END RUSSELL **)

definition write_at_stack_pointer:
 ∀M. ∀ps: PreStatus M. Byte → Σps':PreStatus M.(code_memory … ps = code_memory … ps') ≝
  λM: Type[0].
  λs: PreStatus M.
  λv: Byte.
    let 〈 nu, nl 〉 ≝ split … 4 4 (get_8051_sfr ? s SFR_SP) in
    let bit_zero ≝ get_index_v… nu O ? in
    let bit_1 ≝ get_index_v… nu 1 ? in
    let bit_2 ≝ get_index_v… nu 2 ? in
    let bit_3 ≝ get_index_v… nu 3 ? in
      if bit_zero then
        let memory ≝ insert … ([[ bit_1 ; bit_2 ; bit_3 ]] @@ nl)
                              v (low_internal_ram ? s) in
          set_low_internal_ram ? s memory
      else
        let memory ≝ insert … ([[ bit_1 ; bit_2 ; bit_3 ]] @@ nl)
                              v (high_internal_ram ? s) in
          set_high_internal_ram ? s memory.
  [ cases l0 %
  |2,3,4,5: cases not_implemented (* CSC: ???? normalize repeat (@ le_S_S) @ le_O_n *)
  ]
qed.

definition execute_1_pseudo_instruction': (Word → nat) → ∀ps:PseudoStatus.
 Σps':PseudoStatus.(code_memory … ps = code_memory … ps')
≝
  λticks_of.
  λs.
  let 〈instr, pc〉 ≝ fetch_pseudo_instruction (\snd (code_memory ? s)) (program_counter ? s) in
  let ticks ≝ ticks_of (program_counter ? s) in
  let s ≝ set_clock ? s (clock ? s + ticks) in
  let s ≝ set_program_counter ? s pc in
    match instr with
    [ Instruction instr ⇒
       execute_1_preinstruction … (λx, y. address_of_word_labels y x) instr s
    | Comment cmt ⇒ s
    | Cost cst ⇒ s
    | Jmp jmp ⇒ set_program_counter ? s (address_of_word_labels s jmp)
    | Call call ⇒
      let a ≝ address_of_word_labels s call in
      let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr ? s SFR_SP) (bitvector_of_nat 8 1) in
      let s ≝ set_8051_sfr ? s SFR_SP new_sp in
      let 〈pc_bu, pc_bl〉 ≝ split ? 8 8 (program_counter ? s) in
      let s ≝ write_at_stack_pointer ? s pc_bl in
      let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr ? s SFR_SP) (bitvector_of_nat 8 1) in
      let s ≝ set_8051_sfr ? s SFR_SP new_sp in
      let s ≝ write_at_stack_pointer ? s pc_bu in
        set_program_counter ? s a
    | Mov dptr ident ⇒
       set_arg_16 ? s (get_arg_16 ? s (DATA16 (address_of_word_labels s ident))) dptr
    ].
 [
 |2,3,4: %
 | <(sig2 … l7) whd in ⊢ (??? (??%)) <(sig2 … l5) %
 |
 | (*CSC: ??? *)
 | (*CSC: ??? *)
 | %
 ]
qed.




lemma execute_code_memory_unchanged:
 ∀ticks_of,ps. code_memory ? ps = code_memory ? (execute_1_pseudo_instruction ticks_of ps).
 #ticks #ps whd in ⊢ (??? (??%))
 cases (fetch_pseudo_instruction (\snd (code_memory pseudo_assembly_program ps))
  (program_counter pseudo_assembly_program ps)) #instr #pc
 whd in ⊢ (??? (??%)) cases instr
  [ #pre cases pre
     [ #a1 #a2 whd in ⊢ (??? (??%)) cases (add_8_with_carry ???) #y1 #y2 whd in ⊢ (??? (??%))
       cases (split ????) #z1 #z2 %
     | #a1 #a2 whd in ⊢ (??? (??%)) cases (add_8_with_carry ???) #y1 #y2 whd in ⊢ (??? (??%))
       cases (split ????) #z1 #z2 %
     | #a1 #a2 whd in ⊢ (??? (??%)) cases (sub_8_with_carry ???) #y1 #y2 whd in ⊢ (??? (??%))
       cases (split ????) #z1 #z2 %
     | #a1 whd in ⊢ (??? (??%)) cases a1 #x #H whd in ⊢ (??? (??%)) cases x
       [ #x1 whd in ⊢ (??? (??%)) 
     | *: cases not_implemented
     ]
  | #comment %
  | #cost %
  | #label %
  | #label whd in ⊢ (??? (??%)) cases (half_add ???) #x1 #x2 whd in ⊢ (??? (??%))
    cases (split ????) #y1 #y2 whd in ⊢ (??? (??%)) cases (half_add ???) #z1 #z2
    whd in ⊢ (??? (??%)) whd in ⊢ (??? (??%)) cases (split ????) #w1 #w2
    whd in ⊢ (??? (??%)) cases (get_index_v bool ????) whd in ⊢ (??? (??%))
    (* CSC: ??? *)
  | #dptr #label (* CSC: ??? *)
  ]
  cases not_implemented
qed.

lemma foo:
 ∀ticks_of.
 ∀ps: PseudoStatus.
  match status_of_pseudo_status ps with [ None ⇒ True | Some s ⇒
  let ps' ≝ execute_1_pseudo_instruction ticks_of ps in
  match status_of_pseudo_status ps' with [ None ⇒ True | Some s'' ⇒
  let s' ≝ execute_1 s in
   s = s'']].
 #ticks_of #ps
 whd in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ? ])
 cases (assembly (code_memory pseudo_assembly_program ps)) [%] * #cm #costs whd
 whd in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ? ])
 cases (status_of_pseudo_status (execute_1_pseudo_instruction ticks_of ps)) [%] #s'' whd