source: src/ASM/WellLabeled.ma @ 1487

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

definition well_labelled_p ≝
  ∀pc: Word.
  ∀program: BitVectorTrie Byte 16.
  ∀cost_labels.
    let 〈instruction, newpc, cost〉 ≝ fetch program pc in
      match instruction with
      [ LCALL lcall ⇒ ?
      | ACALL 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
            ]
        | _ ⇒ λ_. ⊥
        ] (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
          ]
        | _ ⇒ λ_. ⊥
        ] (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
            ]
        | _ ⇒ λ_. ⊥
        ] (subaddressing_modein … sjmp)
      | JMP jmp ⇒ ?
      | MOVC _ _ ⇒ True
      | RealInstruction instruction ⇒
        match instruction with
        [ JZ jz ⇒ ?
        | _ ⇒ ?
        ]
      ].