source: src/ASM/ASMCosts.ma @ 1495

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

inductive instruction_nature: Type[0] ≝
  | goto: Word → instruction_nature
  | branch: Word → instruction_nature
  | direct_fun_call: Word → instruction_nature
  | ret: instruction_nature
  | other: instruction_nature.

definition addr16_of_addr11: Word → Word11 → Word ≝
  λpc: Word.
  λa: Word11.
  let 〈pc_upper, ignore〉 ≝ split … 8 8 pc in
  let 〈n1, n2〉 ≝ split … 4 4 pc_upper in
  let 〈b123, b〉 ≝ split … 3 8 a in
  let b1 ≝ get_index_v … b123 0 ? in
  let b2 ≝ get_index_v … b123 1 ? in
  let b3 ≝ get_index_v … b123 2 ? in
  let p5 ≝ get_index_v … n2 0 ? in
    (n1 @@ [[ p5; b1; b2; b3 ]]) @@ b.
  //
qed.

definition instruction_nature_next_pc_length ≝
  λvariety: instruction_nature.
  match variety with
  [ ret ⇒ 0
  | branch _ ⇒ 2
  | goto _ ⇒ 1
  | direct_fun_call _ ⇒ 1
  | other ⇒ 1
  ].

definition instruction_info:
    BitVectorTrie Byte 16 → Word → Σprod: (instruction_nature × Word × (list Word) × nat). |\snd (\fst prod)| = instruction_nature_next_pc_length (\fst (\fst (\fst prod))) ≝
  λmem.
  λpc.
  let 〈inst, next_pc, inst_cost〉 ≝ fetch mem pc in
  let nature_next_pcs_proof ≝
    match inst return λx. Σpair: (instruction_nature × (list Word)). |(\snd pair)| = instruction_nature_next_pc_length (\fst pair) with
    [ RealInstruction ri ⇒
      match ri with
      [ RET ⇒ dp … 〈ret, [ ]〉 ?
      | RETI ⇒ dp … 〈ret, [ ]〉 ?
      | JC addr ⇒
        match addr return λx. bool_to_Prop (is_in ? [[ relative ]] x) → ? with
        [ RELATIVE addr ⇒ λ_.
          let 〈carry, addr〉 ≝ half_add … 16 next_pc (sign_extend 8 8 addr) in
            dp … 〈branch addr, [ next_pc; addr ]〉 ?
        | _ ⇒ λp. match p in False with [ ]
        ] (subaddressing_modein … addr)
      | JNC addr ⇒
        match addr return λx. bool_to_Prop (is_in ? [[ relative ]] x) → ? with
        [ RELATIVE addr ⇒ λ_.
          let 〈carry, addr〉 ≝ half_add … 16 next_pc (sign_extend 8 8 addr) in
            dp … 〈branch addr, [ next_pc; addr ]〉 ?
        | _ ⇒ λp. match p in False with [ ]
        ] (subaddressing_modein … addr)
      | JZ addr ⇒
        match addr return λx. bool_to_Prop (is_in ? [[ relative ]] x) → ? with
        [ RELATIVE addr ⇒ λ_.
          let 〈carry, addr〉 ≝ half_add … 16 next_pc (sign_extend 8 8 addr) in
            dp … 〈branch addr, [ next_pc; addr ]〉 ?
        | _ ⇒ λp. match p in False with [ ]
        ] (subaddressing_modein … addr)
      | JNZ addr ⇒
        match addr return λx. bool_to_Prop (is_in ? [[ relative ]] x) → ? with
        [ RELATIVE addr ⇒ λ_.
          let 〈carry, addr〉 ≝ half_add … 16 next_pc (sign_extend 8 8 addr) in
            dp … 〈branch addr, [ next_pc; addr ]〉 ?
        | _ ⇒ λp. match p in False with [ ]
        ] (subaddressing_modein … addr)
      | JB addr1 addr2 ⇒
        match addr2 return λx. bool_to_Prop (is_in ? [[ relative ]] x) → ? with
        [ RELATIVE addr ⇒ λ_.
          let 〈carry, addr〉 ≝ half_add … 16 next_pc (sign_extend 8 8 addr) in
            dp … 〈branch addr, [ next_pc; addr ]〉 ?
        | _ ⇒ λp. match p in False with [ ]
        ] (subaddressing_modein … addr2)
      | JNB addr1 addr2 ⇒
        match addr2 return λx. bool_to_Prop (is_in ? [[ relative ]] x) → ? with
        [ RELATIVE addr ⇒ λ_.
          let 〈carry, addr〉 ≝ half_add … 16 next_pc (sign_extend 8 8 addr) in
            dp … 〈branch addr, [ next_pc; addr ]〉 ?
        | _ ⇒ λp. match p in False with [ ]
        ] (subaddressing_modein … addr2)
      | JBC addr1 addr2 ⇒
        match addr2 return λx. bool_to_Prop (is_in ? [[ relative ]] x) → ? with
        [ RELATIVE addr ⇒ λ_.
          let 〈carry, addr〉 ≝ half_add … 16 next_pc (sign_extend 8 8 addr) in
            dp … 〈branch addr, [ next_pc; addr ]〉 ?
        | _ ⇒ λp. match p in False with [ ]
        ] (subaddressing_modein … addr2)
      | DJNZ addr1 addr2 ⇒
        match addr2 return λx. bool_to_Prop (is_in ? [[ relative ]] x) → ? with
        [ RELATIVE addr ⇒ λ_.
          let 〈carry, addr〉 ≝ half_add … 16 next_pc (sign_extend 8 8 addr) in
            dp … 〈branch addr, [ next_pc; addr ]〉 ?
        | _ ⇒ λp. match p in False with [ ]
        ] (subaddressing_modein … addr2)
      | CJNE addr1 addr2 ⇒
        match addr2 return λx. bool_to_Prop (is_in ? [[ relative ]] x) → ? with
        [ RELATIVE addr ⇒ λ_.
          let 〈carry, addr〉 ≝ half_add … 16 next_pc (sign_extend 8 8 addr) in
            dp … 〈branch addr, [ next_pc; addr ]〉 ?
        | _ ⇒ λp. match p in False with [ ]
        ] (subaddressing_modein … addr2)
      | _ ⇒ dp … 〈other, [ next_pc ]〉 ?
      ]
    | ACALL addr ⇒
      match addr return λx. bool_to_Prop (is_in ? [[ addr11 ]] x) → ? with
      [ ADDR11 addr ⇒ λ_.
        let addr ≝ addr16_of_addr11 pc addr in
          dp … 〈direct_fun_call addr, [ next_pc ]〉 ?
      | _ ⇒ λp. match p in False with [ ]
      ] (subaddressing_modein … addr)
    | LCALL addr ⇒
      match addr return λx. bool_to_Prop (is_in ? [[ addr16 ]] x) → ? with
      [ ADDR16 addr ⇒ λ_. dp … 〈direct_fun_call addr, [ next_pc ]〉 ?
      | _ ⇒ λp. match p in False with [ ]
      ] (subaddressing_modein … addr)
    | AJMP addr ⇒
      match addr return λx. bool_to_Prop (is_in ? [[ addr11 ]] x) → ? with
      [ ADDR11 addr ⇒ λ_.
        let addr ≝ addr16_of_addr11 pc addr in
          dp … 〈goto addr, [ addr ]〉 ?
      | _ ⇒ λp. match p in False with [ ]
      ] (subaddressing_modein … addr)
    | LJMP addr ⇒
      match addr return λx. bool_to_Prop (is_in ? [[ addr16 ]] x) → ? with
      [ ADDR16 addr ⇒ λ_. dp … 〈goto addr, [ addr ]〉 ?
      | _ ⇒ λp. match p in False with [ ]
      ] (subaddressing_modein … addr)
    | SJMP addr ⇒
      match addr return λx. bool_to_Prop (is_in ? [[ relative ]] x) → ? with
      [ RELATIVE addr ⇒ λ_.
        let 〈carry, addr〉 ≝ half_add 16 next_pc (sign_extend 8 8 addr) in
          dp … 〈goto addr, [ addr ]〉 ?
      | _ ⇒ λp. match p in False with [ ]
      ] (subaddressing_modein … addr)
    | JMP addr ⇒ dp … 〈other, [ next_pc ]〉 ?
    | MOVC acc_a addr ⇒ dp … 〈other, [ next_pc ]〉 ?
    ]
  in
    match nature_next_pcs_proof with
    [ dp nature_next_pcs their_proof ⇒
      let nature ≝ \fst nature_next_pcs in
      let next_pcs ≝ \snd nature_next_pcs in
        dp … 〈〈〈nature, next_pc〉, next_pcs〉, inst_cost〉 ?
    ].
  [1: >their_proof %
  |*: %
  ]
qed.

let rec compare
  (a: Type[0]) (the_list: list (a × nat))
    on the_list: nat ≝
  match the_list with
  [ nil ⇒ ⊥ (* XXX: was assert false *)
  | cons hd tl ⇒
    match tl with
    [ nil ⇒
      let 〈pc, cost〉 ≝ hd in
        cost
    | cons hd' tl' ⇒
      let 〈pc1, cost1〉 ≝ hd in
      let 〈pc2, cost2〉 ≝ hd' in
        match eq_nat cost1 cost2 with
        [ true ⇒ max cost1 (compare … tl)
        | false ⇒ compare … tl'
        ]
    ]
  ].
  cases daemon
qed.

let rec block_cost'
  (mem: BitVectorTrie Byte 16) (cost_labels: BitVectorTrie Byte 16)
    (program_counter: Word) (program_size: nat) (cost_so_far: nat)
      on program_size ≝
  match program_size with
  [ O ⇒ 0
  | S program_size ⇒        
    let sigma ≝ instruction_info mem program_counter in
      match sigma with
      [ dp variety_costs their_proof ⇒
        let variety ≝ \fst (\fst (\fst variety_costs)) in
        let next_pc ≝ \snd (\fst (\fst variety_costs)) in
        let next_pcs ≝ \snd (\fst variety_costs) in
        let inst_cost ≝ \snd variety_costs in
          match variety return λx. |next_pcs| = instruction_nature_next_pc_length x → nat with
          [ other ⇒ λproof.
            match next_pcs return λx. |x| = 1 → nat with
            [ nil ⇒ λabsurd. ⊥
            | cons hd tl ⇒ λproof.
              match lookup_opt … hd cost_labels with
              [ None ⇒ block_cost' mem cost_labels hd program_size (cost_so_far + inst_cost)
              | Some _ ⇒ inst_cost + cost_so_far
              ]
            ] proof
          | _ ⇒ λ_. inst_cost + cost_so_far
          ] their_proof
      ]
  ].
  normalize in absurd
  destruct(absurd)
qed.

definition block_cost ≝
  λmem: BitVectorTrie Byte 16.
  λcost_labels: BitVectorTrie Byte 16.
  λprogram_counter: Word.
  λprogram_size: nat.
    block_cost' mem cost_labels program_counter program_size 0.

let rec traverse_code_internal
  (program: list Byte) (mem: BitVectorTrie Byte 16)
    (cost_labels: BitVectorTrie Byte 16) (pc: Word) (program_size: nat)
      on program: BitVectorTrie nat 8 ≝
  match instruction_info mem pc with
  [ dp info proof ⇒
    let newpc ≝ \snd (\fst (\fst info)) in
    match program with
    [ nil ⇒ Stub …
    | cons hd tl ⇒
      match lookup_opt … pc cost_labels with
      [ None ⇒ traverse_code_internal tl mem cost_labels newpc program_size
      | Some lbl ⇒
        let cost ≝ block_cost mem cost_labels pc program_size in
        let cost_mapping ≝ traverse_code_internal tl mem cost_labels newpc program_size in
          insert … lbl cost cost_mapping
      ]
    ]
  ].

definition traverse_code ≝
  λprogram: list Byte.
  λmem: BitVectorTrie Byte 16.
  λcost_labels.
  λprogram_size: nat.
    traverse_code_internal program mem cost_labels (zero …) program_size.

let rec first_cost_label_internal
  (mem: BitVectorTrie Byte 16) (cost_labels: BitVectorTrie Byte 16)
    (program_size: nat) (oldpc: Word)
      on program_size: (Byte × nat) ≝
  match program_size with
  [ O ⇒ ⊥ (* XXX: ummm ... ? *)
  | S program_size ⇒
    match lookup_opt … oldpc cost_labels with
    [ None ⇒
      match instruction_info mem oldpc with
      [ dp info proof ⇒
        let nature ≝ \fst (\fst (\fst info)) in
        let pc ≝ \snd (\fst (\fst info)) in
        let inst_cost ≝ \snd info in
        match nature with
        [ direct_fun_call addr ⇒
          let 〈lbl, cost〉 ≝ first_cost_label_internal mem cost_labels program_size addr in
            〈lbl, inst_cost + cost〉
        | other ⇒
          let 〈lbl, cost〉 ≝ first_cost_label_internal mem cost_labels program_size pc in
            〈lbl, inst_cost + cost〉
        | _ ⇒ ⊥ (* XXX: was assert false in o'caml *)
        ]
      ]
    | Some cost ⇒ 〈cost, 0〉
    ]
  ].
  cases daemon
qed.

definition first_cost_label ≝
  λmem: BitVectorTrie Byte 16.
  λcost_labels: BitVectorTrie Byte 16.
  λprogram_size: nat.
    first_cost_label_internal mem cost_labels program_size (zero …).

definition initialize_costs ≝
  λmem: BitVectorTrie Byte 16.
  λcost_labels: BitVectorTrie Byte 16.
  λcost_mapping: BitVectorTrie nat 8.
  λprogram_size: nat.
  let 〈lbl, cost〉 ≝ first_cost_label mem cost_labels program_size in
  let old_cost ≝
    match lookup_opt … lbl cost_mapping with
    [ None ⇒ 0
    | Some cost ⇒ cost
    ]
  in
  let new_cost ≝ old_cost + cost in
    insert … lbl new_cost cost_mapping.

definition compute_costs ≝
  λprogram: list Byte.
  λcost_labels: BitVectorTrie Byte 16.
  λhas_main: bool.
  let program_size ≝ |program| in
  let memory ≝ load_code_memory program in
  let costs_mapping ≝ traverse_code program memory cost_labels program_size in
    match has_main with
    [ true ⇒
      initialize_costs memory cost_labels costs_mapping program_size
    | false ⇒ costs_mapping
    ].