include "ASM/ASM.ma".
include "ASM/Fetch.ma".
include "ASM/Arithmetic.ma".

let rec member_p
  (a: Type[0]) (eq: a → a → bool) (element: a) (the_list: list a)
    on the_list: Prop ≝
  match the_list with
  [ nil ⇒ False
  | cons hd tl ⇒
    match eq hd element with
    [ true ⇒ True
    | false ⇒ member_p … eq element tl
    ]
  ].

definition well_labelled_p ≝
  ∀pc: Word.
  ∀acc_a: Byte.
  ∀function_locations: list Word.
  ∀program: BitVectorTrie Byte 16.
  ∀cost_labels.
    let 〈instruction, newpc, cost〉 ≝ fetch program pc in
      match instruction with
      [ LCALL lcall ⇒
        match lcall return λx. bool_to_Prop (is_in … [[ addr16 ]] x) → ? with
        [ ADDR16 addr16 ⇒ λ_. member_p … (eq_bv …) addr16 function_locations
        | _ ⇒ λabsurd. ⊥
        ] (subaddressing_modein … lcall)
      | ACALL acall ⇒
        match acall return λx. bool_to_Prop (is_in … [[ addr11 ]] x) → ? with
        [ ADDR11 addr11 ⇒ λ_.
          let 〈pc_bu, pc_bl〉 ≝ split … 8 8 pc in
          let 〈thr, eig〉 ≝ split … 3 8 addr11 in
          let 〈fiv, thr'〉 ≝ split … 5 3 pc_bu in
          let new_pc ≝ (fiv @@ thr) @@ pc_bl in
            match lookup_opt … new_pc cost_labels with
            [ None ⇒ False
            | _    ⇒ True
            ]
        | _ ⇒ λabsurd. ⊥
        ] (subaddressing_modein … acall)
      | AJMP ajmp ⇒
        match ajmp return λx. bool_to_Prop (is_in … [[ addr11 ]] x) → ? with
        [ ADDR11 addr11 ⇒ λ_.
          let 〈pc_bu, pc_bl〉 ≝ split … 8 8 pc in
          let 〈nu, nl〉 ≝ split … 4 4 pc_bu in
          let bit ≝ get_index' … O ? nl in
          let 〈relevant1, relevant2〉 ≝ split … 3 8 addr11 in
          let new_addr ≝ (nu @@ (bit ::: relevant1)) @@ relevant2 in
          let 〈carry, new_pc〉 ≝ half_add … pc new_addr in
            match lookup_opt … new_pc cost_labels with
            [ None ⇒ False
            | _    ⇒ True
            ]
        | _ ⇒ λabsurd. ⊥
        ] (subaddressing_modein … ajmp)
      | LJMP ljmp ⇒
        match ljmp return λx. bool_to_Prop (is_in … [[ addr16 ]] x) → ? with
        [ ADDR16 addr16 ⇒ λ_.
          match lookup_opt … addr16 cost_labels with
          [ None ⇒ False
          | _    ⇒ True
          ]
        | _ ⇒ λabsurd. ⊥
        ] (subaddressing_modein … ljmp)
      | SJMP sjmp ⇒
        match sjmp return λx. bool_to_Prop (is_in … [[ relative ]] x) → ? with
        [ RELATIVE rel ⇒ λ_.
          let 〈carry, new_pc〉 ≝ half_add … pc (sign_extend 8 8 rel) in
            match lookup_opt … new_pc cost_labels with
            [ None ⇒ False
            | _    ⇒ True
            ]
        | _ ⇒ λabsurd. ⊥
        ] (subaddressing_modein … sjmp)
      | JMP jmp ⇒ True (* XXX: check is dynamic, as we can only jump to functions *)
      | MOVC _ _ ⇒ True
      | RealInstruction instruction ⇒
        match instruction with
        [ JZ jz ⇒
          match jz return λx. bool_to_Prop (is_in … [[ relative ]] x) → ? with
          [ RELATIVE rel ⇒ λ_.
            let 〈carry, new_pc〉 ≝ half_add … pc (sign_extend 8 8 rel) in
              match lookup_opt … new_pc cost_labels with
              [ None ⇒ False
              | _    ⇒ True
              ]
          | _ ⇒ λabsurd. ⊥
          ] (subaddressing_modein … jz)
        | JNZ jnz ⇒ 
          match jnz return λx. bool_to_Prop (is_in … [[ relative ]] x) → ? with
          [ RELATIVE rel ⇒ λ_.
            let 〈carry, new_pc〉 ≝ half_add … pc (sign_extend 8 8 rel) in
              match lookup_opt … new_pc cost_labels with
              [ None ⇒ False
              | _    ⇒ True
              ]
          | _ ⇒ λabsurd. ⊥
          ] (subaddressing_modein … jnz)
        | JC jc ⇒
          match jc return λx. bool_to_Prop (is_in … [[ relative ]] x) → ? with
          [ RELATIVE rel ⇒ λ_.
            let 〈carry, new_pc〉 ≝ half_add … pc (sign_extend 8 8 rel) in
              match lookup_opt … new_pc cost_labels with
              [ None ⇒ False
              | _    ⇒ True
              ]
          | _ ⇒ λabsurd. ⊥
          ] (subaddressing_modein … jc)
        | JNC jnc ⇒ 
          match jnc return λx. bool_to_Prop (is_in … [[ relative ]] x) → ? with
          [ RELATIVE rel ⇒ λ_.
            let 〈carry, new_pc〉 ≝ half_add … pc (sign_extend 8 8 rel) in
              match lookup_opt … new_pc cost_labels with
              [ None ⇒ False
              | _    ⇒ True
              ]
          | _ ⇒ λabsurd. ⊥
          ] (subaddressing_modein … jnc)
        | JB baddr jb ⇒
          match jb return λx. bool_to_Prop (is_in … [[ relative ]] x) → ? with
          [ RELATIVE rel ⇒ λ_.
            let 〈carry, new_pc〉 ≝ half_add … pc (sign_extend 8 8 rel) in
              match lookup_opt … new_pc cost_labels with
              [ None ⇒ False
              | _    ⇒ True
              ]
          | _ ⇒ λabsurd. ⊥
          ] (subaddressing_modein … jb)
        | JNB baddr jnb ⇒
          match jnb return λx. bool_to_Prop (is_in … [[ relative ]] x) → ? with
          [ RELATIVE rel ⇒ λ_.
            let 〈carry, new_pc〉 ≝ half_add … pc (sign_extend 8 8 rel) in
              match lookup_opt … new_pc cost_labels with
              [ None ⇒ False
              | _    ⇒ True
              ]
          | _ ⇒ λabsurd. ⊥
          ] (subaddressing_modein … jnb)
        | JBC baddr jbc ⇒
          match jbc return λx. bool_to_Prop (is_in … [[ relative ]] x) → ? with
          [ RELATIVE rel ⇒ λ_.
            let 〈carry, new_pc〉 ≝ half_add … pc (sign_extend 8 8 rel) in
              match lookup_opt … new_pc cost_labels with
              [ None ⇒ False
              | _    ⇒ True
              ]
          | _ ⇒ λabsurd. ⊥
          ] (subaddressing_modein … jbc)
        | CJNE args cjne ⇒
          match cjne return λx. bool_to_Prop (is_in … [[ relative ]] x) → ? with
          [ RELATIVE rel ⇒ λ_.
            let 〈carry, new_pc〉 ≝ half_add … pc (sign_extend 8 8 rel) in
              match lookup_opt … new_pc cost_labels with
              [ None ⇒ False
              | _    ⇒ True
              ]
          | _ ⇒ λabsurd. ⊥
          ] (subaddressing_modein … cjne)
        | DJNZ args djnz ⇒
          match djnz return λx. bool_to_Prop (is_in … [[ relative ]] x) → ? with
          [ RELATIVE rel ⇒ λ_.
            let 〈carry, new_pc〉 ≝ half_add … pc (sign_extend 8 8 rel) in
              match lookup_opt … new_pc cost_labels with
              [ None ⇒ False
              | _    ⇒ True
              ]
          | _ ⇒ λabsurd. ⊥
          ] (subaddressing_modein … djnz)
        | _ ⇒ True
        ]
      ].
  [*: normalize in absurd; // ]
qed.