source: src/ASM/AssemblyProof.ma @ 828

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
      normalize
    ]
  | 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)) ].

lemma foo:
 ∀ticks_of.
 ∀ps: PseudoStatus.
  let ps' ≝ execute_1_pseudo_instruction ticks_of ps in
  match status_of_pseudo_status ps' with [ None ⇒ True | Some s'' ⇒
  match status_of_pseudo_status ps with [ None ⇒ True | Some s ⇒
  let s' ≝ execute_1 s in
   s = s'']].