include "ASM/ASMCosts.ma".
include "ASM/UtilBranch.ma".
include alias "arithmetics/nat.ma".
include alias "basics/logic.ma".

let rec traverse_code_internal
  (code_memory: BitVectorTrie Byte 16) (cost_labels: BitVectorTrie costlabel 16)
    (program_counter: Word) (program_size: nat)
      (program_size_invariant: program_size = 0 ∨ nat_of_bitvector … program_counter + program_size = 2^16)
        on program_size:
          Σcost_map: identifier_map CostTag nat.
            (∀pc,k. nat_of_bitvector … program_counter ≤ nat_of_bitvector 16 pc → nat_of_bitvector … pc < program_size + nat_of_bitvector … program_counter → lookup_opt … pc cost_labels = Some … k → present … cost_map k) ∧
            (∀k. ∀k_pres:present … cost_map k. ∃pc. lookup_opt … pc cost_labels = Some … k ∧
               pi1 … (block_cost code_memory pc cost_labels) = lookup_present … k_pres) ≝
  match program_size return λx. x = program_size → Σcost_map: ?. ? with
  [ O ⇒ λprogram_size_refl. empty_map CostTag nat
  | S program_size' ⇒ λprogram_size_refl.
    let new_program_counter' ≝ add 16 (bitvector_of_nat 16 1) program_counter in
    let cost_mapping ≝ traverse_code_internal code_memory cost_labels new_program_counter' program_size' ? in
    match lookup_opt … program_counter cost_labels return λx. x = lookup_opt … program_counter cost_labels → Σcost_map: ?. ? with
    [ None ⇒ λlookup_refl. pi1 … cost_mapping
    | Some lbl ⇒ λlookup_refl.
      let cost ≝ block_cost code_memory program_counter cost_labels in
        cic:/matita/cerco/common/Identifiers/add.fix(0,2,3) ?? cost_mapping lbl cost
    ] (refl … (lookup_opt … program_counter cost_labels))
  ] (refl … program_size).
  [3:
    cases program_size_invariant
    [1:
      #destruct_assm @⊥ -traverse_code_internal destruct
    |2:
      #program_size_invariant'
      %
      [1:
        #pc #k #H1 #H2 #lookup_opt_assm @(eq_identifier_elim … k lbl)
        [1:
          #eq_assm >eq_assm
          cases cost_mapping #cost_mapping' * #ind_hyp #_
          @present_add_hit
        |2:
          #neq_assm @present_add_miss try assumption
          cases cost_mapping #cost_mapping' * #ind_hyp #_
          inversion program_size'
          [1:
            #program_size_refl_0 -traverse_code_internal destruct @⊥ cases neq_assm #assm @assm
            cut (Some … k = Some … lbl → k = lbl) (* XXX: lemma *)
            [1:
              #Some_assm destruct(Some_assm) %
            |2:
              #Some_assm @Some_assm <lookup_opt_assm >lookup_refl
              >(?:pc=program_counter)
              [1:
                %
              |2:
                @refl_nat_of_bitvector_to_refl
                @le_to_le_to_eq
                try assumption
                change with (? ≤ ?) in H2;
                @le_S_S_to_le
                assumption
              ]
            ]
          |2:
            #n' #_ #program_size_refl_Sn' -traverse_code_internal destruct
            cut((S (nat_of_bitvector 16 program_counter)) = nat_of_bitvector 16 (add 16 (bitvector_of_nat 16 1) program_counter))
            [1:
              destruct
              @succ_nat_of_bitvector_half_add_1
              @le_plus_to_minus_r
              change with (S ? ≤ ?) >plus_n_Sm
              <program_size_invariant'
              @monotonic_le_plus_r
              @le_S_S @le_S_S @le_O_n
            |2:
              #S_assm
              @(ind_hyp … lookup_opt_assm)
              [1:
                @(eqb_elim (nat_of_bitvector … program_counter)
                  (nat_of_bitvector … pc))
                [1:
                  #eqb_refl_assm
                  -ind_hyp -H1 -H2
                  lapply (refl_nat_of_bitvector_to_refl 16 program_counter pc eqb_refl_assm)
                  #program_counter_refl_assm -eqb_refl_assm
                  <program_counter_refl_assm in lookup_opt_assm; <lookup_refl
                  #Some_assm destruct(Some_assm)
                  cases neq_assm #absurd_assm
                  cases (absurd_assm (refl … k))
                |2:
                  #eqb_ref_assm
                  -ind_hyp
                  <S_assm
                  change with (? < ?)
                  @le_neq_to_lt assumption
                ]
              |2:
                generalize in match H2; whd in ⊢ (??% → ?);
                >plus_n_Sm in ⊢ (% → ?);
                cut(new_program_counter' = add 16 (bitvector_of_nat 16 1) program_counter)
                [1: %
                |2:
                  #new_program_counter_assm' >new_program_counter_assm'
                  >S_assm #relevant assumption
                ]
              ]
            ]
          ]
        ]
      |2:
        #k #k_pres
        @(eq_identifier_elim … k lbl)
        [1:
          #eq_assm %{program_counter} %
          [1:
            >eq_assm >lookup_refl %
          |2:
            >eq_assm in k_pres ⊢ (???%); #k_pres >lookup_present_add_hit %
          ]
        |2:
          #neq_assm 
          cases cost_mapping in k_pres; #cost_mapping' #ind_hyp #present_assm
          cases ind_hyp #_ #relevant cases (relevant k ?)
          [2:
            @(present_add_present … present_assm) assumption
          |1:
            #program_counter' #ind_hyp' %{program_counter'} %
            [1:
              cases ind_hyp' #assm #_ assumption
            |2:
              cases ind_hyp' #lookup_opt_assm #ind_hyp'' >ind_hyp''
              @sym_eq @lookup_present_add_miss assumption
            ]
          ]
        ]
      ]
    ]
  |1:
    %
    [1:
      #pc #k #absurd1 #absurd2
      @⊥ lapply(lt_to_not_le … absurd2) *
      #absurd @absurd assumption
    |2:
      #k #k_pres
      @⊥ normalize in k_pres; /2/
    ]
  |2:
    cases cost_mapping
    -traverse_code_internal #cost_mapping *
    #inductive_hypothesis1 #inductive_hypothesis2 %
    [1:
      #pc #k #H1 #H2
      cases program_size_invariant
      [1:
        #destruct_assm @⊥ destruct
      |2:
        -program_size_invariant #program_size_invariant
        inversion program_size'
        [1:
          #program_size_refl_0 destruct
          #lookup_opt_Some_assm
          >(?:pc = program_counter) in lookup_opt_Some_assm;
          [1:
            #absurd <lookup_refl in absurd;
            #absurd destruct
          |2:
            @refl_nat_of_bitvector_to_refl
            @le_to_le_to_eq
            try assumption
            change with (? ≤ ?) in H2;
            @le_S_S_to_le
            assumption
          ]
        |2:
          #n' #_ #program_size_Sn_refl #Some_lookup_opt_refl
          @(inductive_hypothesis1 … pc) try assumption
          [1:
            @(eqb_elim … (nat_of_bitvector … program_counter)
              (nat_of_bitvector … pc));
            [1:
              #eq_assm
              lapply (refl_nat_of_bitvector_to_refl … eq_assm) #pc_refl
              <pc_refl in Some_lookup_opt_refl; <lookup_refl #absurd
              destruct
            |2:
              #neq_assm
              @(transitive_le ? (S (nat_of_bitvector … program_counter)))
              [1:
                cut((S (nat_of_bitvector 16 program_counter)) = nat_of_bitvector 16 (add 16 (bitvector_of_nat 16 1) program_counter))
                [1:
                  destruct
                  @succ_nat_of_bitvector_half_add_1
                  @le_plus_to_minus_r
                  change with (S ? ≤ ?) >plus_n_Sm
                  <program_size_invariant
                  @monotonic_le_plus_r
                  @le_S_S @le_S_S @le_O_n
                |2:
                  #Sn_refl_assm >Sn_refl_assm @le_n
                ]
              |2:
                change with (? < ?)
                @le_neq_to_lt
                assumption
              ]
            ]
          |2:
            destruct
            @(transitive_le … H2)
            cut((S (nat_of_bitvector 16 program_counter)) = nat_of_bitvector 16 (add 16 (bitvector_of_nat 16 1) program_counter))
            [1:
              destruct
              @succ_nat_of_bitvector_half_add_1
              @le_plus_to_minus_r
              change with (S ? ≤ ?) >plus_n_Sm
              <program_size_invariant
              @monotonic_le_plus_r
              @le_S_S @le_S_S @le_O_n
            |2:
              #S_assm
              change with (S (S n' + ?) ≤ ?)
              >plus_n_Sm @monotonic_le_plus_r >S_assm
              @le_n
            ]
          ]
        ]
      ]
    |2:
      assumption
    ]
  |4:
    inversion program_size'
    [1:
      #_ %1 %
    |2:
      #n' #_ #program_size_refl_Sn @or_intror
      cases program_size_invariant
      [1:
        #absurd destruct
      |2:
        #relevant <relevant <plus_n_Sm <program_size_refl <plus_n_Sm
        @eq_f >program_size_refl_Sn <plus_n_Sm
        change with (? = (S ?) + ?) @eq_f2 try %
        cut((S (nat_of_bitvector 16 program_counter)) = nat_of_bitvector 16 (add 16 (bitvector_of_nat 16 1) program_counter))
        [1:
          destruct
          @succ_nat_of_bitvector_half_add_1
          @le_plus_to_minus_r
          change with (S ? ≤ ?) >plus_n_Sm
          <relevant
          @monotonic_le_plus_r
          @le_S_S @le_S_S @le_O_n
        |2:
          #S_assm
          cut(new_program_counter' = add … (bitvector_of_nat … 1) program_counter)
          [1: %
          |2:
           #new_program_counter_assm' >new_program_counter_assm'
           cases program_size_invariant
           [1:
             #destruct_assm @⊥ >destruct_assm in program_size_refl; #abs destruct(abs)
           |2:
             #program_size_invariant
             <program_size_invariant <program_size_refl
             <S_assm normalize <plus_n_Sm %
           ]
         ]
      ]
    ]
    ]
  ]
qed.

(* XXX:
 * At the moment we do a full traversal of the code memory, however we could do
 * a fold over the domain of the cost labels map.
 *
 *)
definition traverse_code:
  ∀code_memory: BitVectorTrie Byte 16.
  ∀cost_labels: BitVectorTrie costlabel 16.
  ∀cost_labels_injective:
    ∀pc, pc',l.
      lookup_opt … pc cost_labels = Some … l → lookup_opt … pc' cost_labels = Some … l →
        pc = pc'.
    Σcost_map: identifier_map CostTag nat.
      (∀pc,k. nat_of_bitvector … pc < 2^16 → lookup_opt … pc cost_labels = Some … k → present … cost_map k) ∧
      (∀k. ∀k_pres:present … cost_map k. ∀pc. lookup_opt … pc cost_labels = Some … k →
          pi1 … (block_cost code_memory pc cost_labels) = lookup_present … k_pres) ≝
  λcode_memory: BitVectorTrie Byte 16.
  λcost_labels: BitVectorTrie costlabel 16.
  λcost_labels_injective.
    pi1 ? ? (traverse_code_internal code_memory cost_labels (zero …) (2^16) ?).
  [1:
    @or_intror %
  |2:
    cases (traverse_code_internal ?????)
    #cost_mapping * #inductive_hypothesis1 #inductive_hypothesis2 %
    [1:
      #pc #k #pc_program_size_assm
      @inductive_hypothesis1
      [1:
        @le_O_n
      |2:
        normalize in match (nat_of_bitvector 16 (zero 16));
        <plus_n_O assumption
      ]
    |2:
      #k #k_pres #pc #lookup_opt_assm
      cases (inductive_hypothesis2 ? k_pres)
      #program_counter' * #lookup_opt_assm' #block_cost_assm
      >(cost_labels_injective … lookup_opt_assm lookup_opt_assm')
      assumption
    ]
  ]
qed.
    
definition compute_costs ≝
  λprogram: list Byte.
  λcost_labels: BitVectorTrie costlabel 16.
  λcost_labels_injective:
    ∀pc, pc',l.
      lookup_opt … pc cost_labels = Some … l → lookup_opt … pc' cost_labels = Some … l →
        pc = pc'.
    (* let program_size ≝ |program| in *)
    let code_memory ≝ load_code_memory program in
      traverse_code code_memory cost_labels cost_labels_injective.

definition ASM_cost_map :
  ∀p: (list Byte) × (BitVectorTrie costlabel 16).
  let code_memory ≝ load_code_memory (\fst p) in
  let a_s ≝ ASM_abstract_status code_memory (\snd p) in 
  ? → as_cost_map a_s ≝
  λp.
  λcost_labels_injective.
  let cost_map ≝ compute_costs (\fst p) (\snd p) cost_labels_injective in
  λl_sig.
  lookup_present … cost_map (as_cost_get_label ? l_sig) ?.
  cases cost_map #m * #prf #_ cases l_sig
  #l * #pc #Hl whd in Hl; whd whd in match (as_cost_get_label ??);
  whd in Hl:(??%?); lapply (prf … Hl) //
qed.