include "ASM/Interpret.ma".

definition ASMRegisterRets: list [[ acc_a; direct; registr ]] ≝
 [ DIRECT (bitvector_of_nat 8 130);       (* DPL *)
   DIRECT (bitvector_of_nat 8 131);       (* DPH *)
   REGISTER [[ false; false; false ]];   (* Register00 *)
   REGISTER [[ false; false; true ]] ].  (* Register01 *)
% qed.

definition as_result_of_finaladdr: ∀T:Type[0]. ∀cm:T. PreStatus … cm → Word → option int ≝
 λT,cm,st,finaladdr.
  if eq_bv ? (program_counter ?? st) finaladdr then
   let vals ≝
    map [[acc_a;direct;registr]] ? (get_arg_8 ?? st false) (ASMRegisterRets⌈list ? ↦ ?⌉) in
   let dummy ≝ zero ? in
   let first_byte ≝ λl. match l with [ nil ⇒ 〈dummy,[]〉 | cons hd tl ⇒ 〈hd,tl〉] in
   let 〈b1,tl1〉 ≝ first_byte vals in
   let 〈b2,tl2〉 ≝ first_byte tl1 in
   let 〈b3,tl3〉 ≝ first_byte tl2 in
   let 〈b4,tl4〉 ≝ first_byte tl3 in
    Some ? (b4 @@ b3 @@ b2 @@ b1)
  else
   None ?.
[ @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) % | % ]
qed.

definition OC_as_call_ident:
 ∀prog:labelled_object_code.∀cm. (Σs:Status cm. OC_classify … s = cl_call) → ident
≝
 λprog,cm,s0.
 let dummy : ident ≝ an_identifier … one in
  let pc ≝ program_counter ?? (execute_1' cm s0) in
  match lookup_opt ?? pc (symboltable prog) with
  [ None ⇒ dummy (* in order to avoid this case we need a specification of the symboltable for this *)
  | Some id ⇒ id ].

definition OC_result : ∀loc.Status (cm loc) → option int ≝
λprog,st. as_result_of_finaladdr … st (final_pc prog).

lemma OC_exclude_tailcall :
∀p : labelled_object_code.
∀st : Status (cm p).
OC_classify … st ≠ cl_tailcall.
#p #st whd in ⊢ (?(??%?));
cases current_instruction [7: * ] normalize
try #x try #y % #ABS destruct
qed.

definition OC_abstract_status: labelled_object_code → abstract_status ≝
 λprog.
    mk_abstract_status
      (Status (cm prog))
      (λs1,s2.OC_result … s1 = None ? ∧ execute_1 … s1 = s2)
      word_deqset
      (program_counter …)
      (OC_classify …)
      (λpc.lookup_opt … pc (costlabels prog))
      (next_instruction_properly_relates_program_counters …)
      (OC_result ?)
      (OC_as_call_ident prog …)
      (λst.⊥).
@hide_prf cases st -st #st #ABS @(absurd … ABS) @OC_exclude_tailcall qed.

lemma OC_costed_is_nop : ∀loc.
let S ≝ OC_abstract_status loc in
∀st,l.as_label S st = Some ? l → current_instruction (cm loc) st = NOP ?.
#loc #st #l #EQ
whd in ⊢ (??%?);
whd in match fetch; normalize nodelta
>(oc_costlabels_are_zero loc … EQ) % qed.

lemma OC_class_to_uncosted : ∀loc.
let S ≝ OC_abstract_status loc in
∀st.
match as_classify S st with
[ cl_other ⇒ True | _ ⇒ ¬as_costed … st ].
#loc #st
whd in match (as_costed ??); inversion (as_label ??)
[ #_ cases (as_classify ??) %* #A @A % ]
#l #EQ whd in match (as_classify ??); >(OC_costed_is_nop … EQ) %
qed.

definition trace_any_label_length ≝
  λprog: labelled_object_code.
  λtrace_ends_flag: trace_ends_with_ret.
  λstart_status: Status (cm prog).
  λfinal_status: Status (cm prog).
  λthe_trace: trace_any_label (OC_abstract_status prog) trace_ends_flag start_status final_status.
    as_trace_any_label_length' … the_trace.

let rec all_program_counter_list
  (n: nat)
    on n ≝
  match n with
  [ O ⇒ [ ]
  | S n' ⇒ (bitvector_of_nat 16 n')::(all_program_counter_list n')
  ].

lemma all_program_counter_list_bound_eq:
  ∀bound: nat.
    |all_program_counter_list bound| = bound.
  #bound elim bound try %
  #bound' #inductive_hypothesis normalize
  >inductive_hypothesis %
qed.

lemma mem_all_program_counter_list_lt_bound:
  ∀bound: nat.
  ∀bound_proof: bound ≤ 2^16.
  ∀e: Word.
    memb word_deqset e (all_program_counter_list bound) = true →
      nat_of_bitvector … e < bound.
  #bound elim bound
  [1:
    #bound_proof #e
    normalize #absurd destruct(absurd)
  |2:
    #bound' #inductive_hypothesis
    #bound_proof #e
    change with (if eq_bv ??? then ? else ? = ? → ?)
    @eq_bv_elim
    [1:
      #eq_assm
      normalize nodelta destruct #_
      >nat_of_bitvector_bitvector_of_nat_inverse try assumption
      normalize %
    |2:
      #neq_assm normalize nodelta
      #memb_assm %2 @inductive_hypothesis
      try assumption
      @(transitive_le bound' (S bound'))
      try assumption %2 %
    ]
  ]
qed.

lemma lt_bound_mem_all_program_counter_list:
  ∀bound: nat.
  ∀bound_proof: bound ≤ 2^16.
  ∀e: Word.
    nat_of_bitvector … e < bound →
      memb word_deqset e (all_program_counter_list bound) = true.
  #bound elim bound
  [1:
    #bound_proof #e normalize
    #absurd cases (lt_to_not_zero … absurd)
  |2:
    #bound' #inductive_hypothesis
    #bound_proof #e
    change with (? → if eq_bv ??? then ? else ? = ?)
    #assm
    cases (le_to_or_lt_eq … (nat_of_bitvector ? e) bound' ?)
    [1:
      #e_lt_assm
      @eq_bv_elim
      [1:
        #eq_assm normalize nodelta %
      |2:
        #neq_assm normalize nodelta
        @inductive_hypothesis try assumption
        @(transitive_le bound' (S bound')) try assumption
        %2 %
      ]
    |2:
      #relevant >eq_eq_bv normalize nodelta try %
      destruct >bitvector_of_nat_inverse_nat_of_bitvector %
    |3:
      normalize in assm;
      @le_S_S_to_le assumption
    ]
  ]
qed.

include alias "arithmetics/nat.ma".

lemma execute_1_and_program_counter_after_other_in_lockstep00:
  ∀code_memory: BitVectorTrie Byte 16.
  ∀start_status: Status code_memory.
      let 〈instruction, pc, ticks〉 ≝ fetch code_memory (program_counter … start_status) in
    ASM_classify0 instruction = cl_other →
        program_counter ? ? (execute_1 … start_status) =
          program_counter_after_other pc instruction.
  #code_memory #start_status 
  whd in match execute_1; normalize nodelta  
  cases (execute_1' code_memory start_status) #the_status; * #_ 
  cases (fetch ? ?); * #instruction #pc #ticks
  #classify_assm #classify_assm0 @classify_assm assumption
qed.

lemma execute_1_and_program_counter_after_other_in_lockstep0:
  ∀code_memory: BitVectorTrie Byte 16.
  ∀start_status: Status code_memory.
    OC_classify … start_status = cl_other →
      let 〈instruction, pc, ticks〉 ≝ fetch code_memory (program_counter … start_status) in
        program_counter ? ? (execute_1 … start_status) =
          program_counter_after_other pc instruction.
  #code_memory #start_status #classify_assm
  whd in match execute_1; normalize nodelta
  cases (execute_1' code_memory start_status) #the_status 
  * #_ whd in classify_assm:(??%?); whd in match (current_instruction ??) in classify_assm;
  cases (fetch ? ?) in classify_assm; * #instruction #pc #ticks
  #classify_assm #classify_assm' @classify_assm' assumption
qed.

lemma execute_1_and_program_counter_after_other_in_lockstep:
  ∀prog: labelled_object_code.
  ∀start_status: Status (cm prog).
    as_classifier (OC_abstract_status prog) start_status cl_other →
      let 〈instruction, pc, ticks〉 ≝ fetch (cm prog) (program_counter … start_status) in
        program_counter ? ? (execute_1 … start_status) =
          program_counter_after_other pc instruction.
  #prog #start_status #classify_assm
  change with (ASM_classify0 ? = ?) in classify_assm;
  destruct (classify_assm)
  @execute_1_and_program_counter_after_other_in_lockstep0 assumption.
qed.  

lemma sublist_tal_pc_list_all_program_counter_list:
  ∀prog: labelled_object_code.
  ∀start, final: Status (cm prog).
  ∀trace_ends_flag.
  ∀the_trace: trace_any_label (OC_abstract_status prog) trace_ends_flag start final.
    sublist ? (tal_pc_list … the_trace) (all_program_counter_list (2^16)).
  #prog #start #final #trace_ends_flag #the_trace
  whd in match (sublist ???); #pc #memb_assm
  @lt_bound_mem_all_program_counter_list try %
  @nat_of_bitvector_lt_bound
qed.

corollary tal_pc_list_length_leq_total_program_size:
  ∀prog: labelled_object_code.
  ∀start, final: Status (cm prog).
  ∀trace_ends_flag.
  ∀the_trace: trace_any_label (OC_abstract_status prog) trace_ends_flag start final.
  ∀unrepeating_witness: tal_unrepeating … the_trace.
    |tal_pc_list … the_trace| ≤ 2^16.
  #prog #start #final #trace_ends_flag #the_trace #unrepeating_witness
  <(all_program_counter_list_bound_eq (2^16))
  @sublist_length
  [1:
    @tal_unrepeating_uniqueb
    assumption
  |2:
    @sublist_tal_pc_list_all_program_counter_list
    assumption
  ]
qed.

let rec compute_paid_trace_any_label
  (prog: labelled_object_code) (trace_ends_flag: trace_ends_with_ret)
   (start_status: Status (cm prog))
   (final_status: Status (cm prog))
        (the_trace: trace_any_label (OC_abstract_status prog) trace_ends_flag start_status final_status)
       on the_trace: nat ≝
  match the_trace with
  [ tal_base_not_return the_status _ _ _ _ ⇒ current_instruction_cost … the_status
  | tal_base_return the_status _ _ _ ⇒ current_instruction_cost … the_status
  | tal_base_call pre_fun_call start_fun_call final _ _ _ _ _ ⇒ current_instruction_cost … pre_fun_call
  | tal_base_tailcall pre_fun_call start_fun_call final _ _ _ ⇒ current_instruction_cost … pre_fun_call
  | tal_step_call end_flag pre_fun_call start_fun_call after_fun_call final
     _ _ _ call_trace _ final_trace ⇒
      let current_instruction_cost ≝ current_instruction_cost … pre_fun_call in
      let final_trace_cost ≝ compute_paid_trace_any_label prog end_flag … final_trace in
        current_instruction_cost + final_trace_cost
  | tal_step_default end_flag status_pre status_init status_end _ tail_trace _ _ ⇒
      let current_instruction_cost ≝ current_instruction_cost … status_pre in
      let tail_trace_cost ≝
       compute_paid_trace_any_label prog end_flag
        status_init status_end tail_trace
      in
        current_instruction_cost + tail_trace_cost
  ].

definition compute_paid_trace_label_label ≝
  λprog: labelled_object_code.
  λtrace_ends_flag: trace_ends_with_ret.
  λstart_status: Status (cm prog).
  λfinal_status: Status (cm prog).
  λthe_trace: (trace_label_label (OC_abstract_status prog) trace_ends_flag start_status final_status).
  match the_trace with
  [ tll_base ends_flag initial final given_trace labelled_proof ⇒
      compute_paid_trace_any_label … given_trace
  ].

lemma trace_compute_paid_trace_cl_other:
  ∀prog : labelled_object_code.
  ∀program_counter' : Word.
  ∀program_size' : ℕ.
  ∀ticks : ℕ.
  ∀instruction : instruction.
  ∀program_counter'' : Word.
  ∀FETCH : (〈instruction,program_counter'',ticks〉=fetch (cm prog) program_counter').
  let program_counter''' ≝ program_counter_after_other program_counter'' instruction in
  ∀start_status : (Status (cm prog)).
  ∀final_status : (Status (cm prog)).
  ∀trace_ends_flag : trace_ends_with_ret.
  ∀the_trace : (trace_any_label (OC_abstract_status prog) trace_ends_flag start_status final_status).
  ∀program_counter_refl : (program_counter' = program_counter … start_status).
  ∀size_invariant : trace_any_label_length … the_trace ≤S program_size'.
  ∀classify_assm: ASM_classify0 instruction = cl_other.
  ∀pi1 : ℕ.
   (if match lookup_opt ?? program_counter''' (costlabels prog) with 
         [None ⇒ true
         |Some _ ⇒ false
         ] 
    then
      ∀start_status0:Status (cm prog).
      ∀final_status0:Status (cm prog).
      ∀trace_ends_flag0:trace_ends_with_ret.
      ∀the_trace0:trace_any_label (OC_abstract_status prog) trace_ends_flag0 start_status0 final_status0.
        trace_any_label_length … the_trace0 ≤ program_size' →
        program_counter''' = program_counter … start_status0 →
                  pi1
                    =compute_paid_trace_any_label … the_trace0
    else (pi1=O) )
   → ticks+pi1
     =compute_paid_trace_any_label … the_trace. 
  #prog #program_counter' #program_size' #ticks #instruction
  #program_counter'' #FETCH #start_status #final_status #trace_ends_flag #the_trace
  #program_counter_refl #size_invariant #classify_assm #recursive_block_cost
  #recursive_assm
  @(trace_any_label_inv_ind … the_trace)
    [2:
      #start_status' #final_status' * #no_result #execute_assm #classifier_assm #trace_ends_assm
      #start_status_refl #final_status_refl #the_trace_assm destruct @⊥
    |3:
      #status_pre_fun_call #status_start_fun_call #status_final * #no_result #execute_assm
      #classifier_assm #after_return_assm #trace_label_return #costed_assm
      #ends_flag_refl #start_status_refl #final_status_refl #the_trace_refl
      destruct @⊥
    |4: 
      #status_pre_fun_call #status_start_fun_call #status_final * #no_result #execute_assm
      #classifier_assm #trace_label_return
      #ends_flag_refl #start_status_refl #final_status_refl #the_trace_refl
      destruct @⊥
    |5:
      #end_flag #status_pre_fun_call #status_start_fun_call #status_after_fun_call
      #status_final * #no_result #execute_assm #classifier_assm #after_return_assm #trace_label_return
      #costed_assm #trace_any_label #trace_ends_flag_refl #start_status_refl
      #final_status_refl #the_trace_refl destruct @⊥
    |6:
      #end_flag #status_pre #status_init #status_end * #no_result #execute_assm #trace_any_label
      #classifier_assm #costed_assm #trace_ends_refl #start_status_refl #final_status_refl
      #the_trace_refl
      destruct
      whd in match (trace_any_label_length … (tal_step_default …));
      whd in match (compute_paid_trace_any_label … (tal_step_default …));
      whd in costed_assm:(?%);
      generalize in match costed_assm;
      generalize in match (refl … (lookup_opt … (program_counter … (execute_1 … status_pre)) (costlabels prog)));
      whd in match (as_label ??);
      generalize in match (lookup_opt … (program_counter … (execute_1 … status_pre)) (costlabels prog))
        in ⊢ (??%? → % → ?);
      #lookup_assm cases lookup_assm
      [1:
        #None_lookup_opt_assm normalize nodelta #_
        generalize in match recursive_assm;
        lapply (execute_1_and_program_counter_after_other_in_lockstep … classifier_assm)
        <FETCH normalize nodelta #rewrite_assm >rewrite_assm in None_lookup_opt_assm;
        #None_lookup_opt_assm <None_lookup_opt_assm
        normalize nodelta #new_recursive_assm
        cases(new_recursive_assm (execute_1 ? status_pre) status_end
          end_flag trace_any_label ? ?) try (>rewrite_assm %)
        whd in match (current_instruction_cost … status_pre);
        cut(ticks = \snd (fetch (cm prog) (program_counter … status_pre)))
        [1,3:
          <FETCH %
        |2:
          #ticks_refl_assm
          >ticks_refl_assm %
        |4:
          #ticks_refl_assm
          change with (S ? ≤ S ?) in size_invariant;
          lapply (le_S_S_to_le … size_invariant) #assm
          assumption
        ]
      |2:
        #costlabel #Some_lookup_opt_assm <Some_lookup_opt_assm
        #absurd
        cases (not_Some_neq_None_to_False ?? absurd)
      ]
    |1:
      #status_start #status_final * #no_result #execute_assm #classifier_assm #costed_assm
      #trace_ends_flag_refl #start_status_refl #final_status_refl #the_trace_refl
      destruct
      whd in match (trace_any_label_length … (tal_base_not_return …));
      whd in match (compute_paid_trace_any_label … (tal_base_not_return …));
      whd in costed_assm;
      generalize in match costed_assm;
      generalize in match (refl … (lookup_opt … (program_counter … (execute_1 … status_start)) ?));
      whd in match (as_label ??);
      generalize in match (lookup_opt … (program_counter … (execute_1 … status_start)) (costlabels prog))
        in ⊢ (??%? → % → ?);
      #lookup_assm cases lookup_assm
      [1:
        #None_lookup_opt_assm
        #absurd @⊥ cases absurd -absurd #absurd @absurd %
      |2:
        #costlabel #Some_lookup_opt_assm normalize nodelta #ignore
        generalize in match recursive_assm;
        cases classifier_assm -classifier_assm #classifier_assm
        [2:
          lapply (execute_1_and_program_counter_after_other_in_lockstep … classifier_assm)
          <FETCH normalize nodelta #rewrite_assm >rewrite_assm in Some_lookup_opt_assm;
          #Some_lookup_opt_assm <Some_lookup_opt_assm
          normalize nodelta #new_recursive_assm >new_recursive_assm
          cut(ticks = \snd (fetch (cm prog) (program_counter … status_start)))
          [1:
            <FETCH %
          |2:
            #ticks_refl_assm >ticks_refl_assm
            <plus_n_O % 
          ]
        |1: 
	        (* JHM: wicked failure because Some prevent previous unfolding of OC_classify here *)
	        @⊥
	        (* *** (* previously: unnecessary case analysis on instruction *)
          change with ((Some ? (ASM_classify0 ?) = ?) → ?);
          whd in match (current_instruction code_memory' status_start);
          <FETCH generalize in match classify_assm;
          cases instruction
          [8:
            #preinstruction normalize nodelta
            whd in match ASM_classify0; normalize nodelta
            #contradiction >contradiction #absurd destruct(absurd)
          ]
          try(#addr1 #addr2 normalize nodelta #ignore #absurd destruct(absurd))
          try(#addr normalize nodelta #ignore #absurd destruct(absurd))
          normalize in ignore; destruct(ignore)
	        *** *)
        ]
      ]
    ]
  change with (ASM_classify0 ? = ?) in classifier_assm;
  whd in match current_instruction in classifier_assm; normalize nodelta in classifier_assm;
  <FETCH in classifier_assm; >classify_assm #absurd destruct(absurd)
qed.

lemma trace_compute_paid_trace_cl_jump:
  ∀prog: labelled_object_code.
  ∀program_counter': Word.
  ∀first_time_around: bool.
  ∀program_size': ℕ.
  ∀ticks: ℕ.
  ∀instruction: instruction.
  ∀program_counter'': Word.
  ∀FETCH: 〈instruction,program_counter'',ticks〉 = fetch (cm prog) program_counter'.
  ∀start_status: (Status (cm prog)).
  ∀final_status: (Status (cm prog)).
  ∀trace_ends_flag: trace_ends_with_ret.
  ∀the_trace: (trace_any_label (OC_abstract_status prog) trace_ends_flag start_status final_status).
  ∀program_counter_refl: (program_counter' = program_counter … start_status).
  ∀classify_assm: ASM_classify0 instruction = cl_jump.
    ticks
     =compute_paid_trace_any_label … the_trace.
  #prog #program_counter' #first_time_around
  #program_size' #ticks #instruction #program_counter'' #FETCH
  #start_status #final_status
  #trace_ends_flag #the_trace #program_counter_refl #classify_assm
  @(trace_any_label_inv_ind … the_trace)
  [6:
    #end_flag #status_pre #status_init #status_end * #no_result #execute_assm #trace_any_label
    #classifier_assm #costed_assm #trace_ends_refl #start_status_refl #final_status_refl
    #the_trace_refl destruct @⊥
  |1:
    #status_start #status_final * #no_result #execute_assm #classifier_assm #costed_assm
    #trace_ends_flag_refl #start_status_refl #final_status_refl #the_trace_refl
    destruct
    whd in match (trace_any_label_length … (tal_base_not_return …));
    whd in match (compute_paid_trace_any_label … (tal_base_not_return …));
    <FETCH %
  |2:
    #start_status' #final_status' * #no_result #execute_assm #classifier_assm #trace_ends_assm
    #start_status_refl #final_status_refl #the_trace_assm destruct @⊥
  |3:
    #status_pre_fun_call #status_start_fun_call #status_final * #no_result #execute_assm
    #classifier_assm #after_return_assm #trace_label_return #costed_assm
    #ends_flag_refl #start_status_refl #final_status_refl #the_trace_refl
    destruct @⊥
  |4:
    #status_pre_fun_call #status_start_fun_call #status_final * #no_result #execute_assm
    #classifier_assm #trace_label_return
    #ends_flag_refl #start_status_refl #final_status_refl #the_trace_refl
    destruct @⊥
  |5:
    #end_flag #status_pre_fun_call #status_start_fun_call #status_after_fun_call
    #status_final * #no_result #execute_assm #classifier_assm #after_return_assm #trace_label_return
    #costed_assm #trace_any_label #trace_ends_flag_refl #start_status_refl
    #final_status_refl #the_trace_refl destruct @⊥
  ]
  change with (ASM_classify0 ? = ?) in classifier_assm;
  whd in match current_instruction in classifier_assm; normalize nodelta in classifier_assm;
  <FETCH in classifier_assm; >classify_assm #absurd destruct(absurd)
qed.

lemma trace_compute_paid_trace_cl_call:
  ∀prog: labelled_object_code.
  ∀program_counter' : Word.
  ∀program_size' : ℕ.
  ∀ticks : ℕ.
  ∀instruction : instruction.
  ∀program_counter'' : Word.
  ∀FETCH : (〈instruction,program_counter'',ticks〉=fetch (cm prog) program_counter').
  ∀start_status : (Status (cm prog)).
  ∀final_status : (Status (cm prog)).
  ∀trace_ends_flag : trace_ends_with_ret.
  ∀the_trace : trace_any_label (OC_abstract_status prog) trace_ends_flag start_status final_status.
  ∀program_counter_refl : (program_counter' = program_counter … start_status).
  ∀size_invariant : trace_any_label_length … the_trace ≤S program_size'.
  ∀classify_assm: ASM_classify0 instruction = cl_call.
  (∀pi1:ℕ
  .if match lookup_opt ?? program_counter'' (costlabels prog) with 
      [None ⇒ true | Some _ ⇒ false] 
   then (∀start_status0:Status (cm prog)
             .∀final_status0:Status (cm prog)
              .∀trace_ends_flag0:trace_ends_with_ret
               .∀the_trace0:trace_any_label
                                        (OC_abstract_status prog)
                                        trace_ends_flag0 start_status0 final_status0.
                trace_any_label_length … the_trace0
                   ≤ program_size' →
                program_counter''
                 =program_counter … start_status0
                 → pi1
                   =compute_paid_trace_any_label … the_trace0) 
   else (pi1=O) 
   → ticks+pi1
     =compute_paid_trace_any_label … the_trace).
  #prog #program_counter' #program_size'
  #ticks #instruction #program_counter'' #FETCH
  #start_status #final_status #trace_ends_flag
  #the_trace #program_counter_refl #size_invariant #classify_assm
  #recursive_block_cost #recursive_assm
  @(trace_any_label_inv_ind … the_trace)
  [6:
    #end_flag #status_pre #status_init #status_end * #no_result #execute_assm #trace_any_label
    #classifier_assm #costed_assm #trace_ends_refl #start_status_refl #final_status_refl
    #the_trace_refl destruct @⊥
  |1:
    #status_start #status_final * #no_result #execute_assm #classifier_assm #costed_assm
    #trace_ends_flag_refl #start_status_refl #final_status_refl #the_trace_refl
    destruct @⊥
  |2:
    #start_status' #final_status' * #no_result #execute_assm #classifier_assm #trace_ends_assm
    #start_status_refl #final_status_refl #the_trace_assm destruct @⊥
  |3:
    #status_pre_fun_call #status_start_fun_call #status_final * #no_result #execute_assm
    #classifier_assm #after_return_assm #trace_label_return #costed_assm
    #ends_flag_refl #start_status_refl #final_status_refl #the_trace_refl
    destruct
    whd in match (trace_any_label_length … (tal_base_call …));
    whd in match (compute_paid_trace_any_label … (tal_base_call …));
    whd in costed_assm;
    generalize in match costed_assm;
    generalize in match (refl … (lookup_opt … (program_counter … status_final) (costlabels prog)));
    whd in match (as_label ??);
    generalize in match (lookup_opt … (program_counter … status_final) ?)
      in ⊢ (??%? → % → ?);
    #lookup_assm cases lookup_assm
    [1:
      #None_lookup_opt normalize nodelta #absurd cases absurd
      -absurd #absurd @⊥ @absurd %
    |2:
      #costlabel #Some_lookup_opt normalize nodelta #ignore
      generalize in match recursive_assm;
      cut(program_counter'' = (program_counter … status_final))
      [1:
        generalize in match after_return_assm;
        whd in ⊢ (% → ?); <FETCH normalize nodelta #relevant <relevant %
      |2:
        #program_counter_assm >program_counter_assm <Some_lookup_opt
        normalize nodelta #new_recursive_assm >new_recursive_assm
        cut(ticks = \snd (fetch (cm prog) (program_counter … status_pre_fun_call)))
        [1:
          <FETCH %
        |2:
          #ticks_refl_assm >ticks_refl_assm
          <plus_n_O %
        ]
      ]
    ]
  |4:
    #status_pre_fun_call #status_start_fun_call #status_final * #no_result #execute_assm
    #classifier_assm #trace_label_return
    #ends_flag_refl #start_status_refl #final_status_refl #the_trace_refl
    destruct @⊥
  |5:
    #end_flag #status_pre_fun_call #status_start_fun_call #status_after_fun_call
    #status_final * #no_result #execute_assm #classifier_assm #after_return_assm #trace_label_return
    #costed_assm #trace_any_label #trace_ends_flag_refl #start_status_refl
    #final_status_refl #the_trace_refl
    generalize in match execute_assm; destruct #execute_assm
    whd in match (trace_any_label_length … (tal_step_call …));
    whd in match (compute_paid_trace_any_label … (tal_step_call …));
    whd in costed_assm:(?%);
    generalize in match costed_assm;
    generalize in match (refl … (lookup_opt … (program_counter … status_after_fun_call) (costlabels ?)));
    whd in match (as_label ??);
    generalize in match (lookup_opt … (program_counter … status_after_fun_call) (costlabels prog))
      in ⊢ (??%? → % → ?);
    #lookup_assm cases lookup_assm
    [1:
      #None_lookup_opt_assm normalize nodelta #ignore
      generalize in match recursive_assm;
      cut(program_counter'' = program_counter … status_after_fun_call)
      [1:
        generalize in match after_return_assm;
        whd in ⊢ (% → ?); <FETCH normalize nodelta #relevant >relevant %
      |2:
        #program_counter_refl >program_counter_refl <None_lookup_opt_assm
        normalize nodelta #new_recursive_assm
        cases (new_recursive_assm … trace_any_label ? ?)
        [1:
          @plus_right_monotone whd in ⊢ (???%); <FETCH %
        |2:
          @le_S_S_to_le @size_invariant
        |3:
          %
        ]
      ]
    |2:
      #cost_label #Some_lookup_opt_assm #absurd
      cases (not_Some_neq_None_to_False ?? absurd)
    ]
  ]
  try (change with (ASM_classify0 ? = ? ∨ ASM_classify0 ? = ?) in classifier_assm;)
  try (change with (ASM_classify0 ? = ?) in classifier_assm;)
  whd in match current_instruction in classifier_assm; normalize nodelta in classifier_assm;
  <FETCH in classifier_assm; >classify_assm #absurd destruct(absurd) cases absurd
  #absurd destruct(absurd)
qed.

lemma trace_compute_paid_trace_cl_return:
  ∀prog: labelled_object_code.
  ∀program_counter' : Word.
  ∀program_size' : ℕ.
  ∀ticks : ℕ.
  ∀instruction : instruction.
  ∀program_counter'' : Word.
  ∀FETCH : (〈instruction,program_counter'',ticks〉=fetch (cm prog) program_counter').
  ∀start_status : (Status (cm prog)).
  ∀final_status : (Status (cm prog)).
  ∀trace_ends_flag : trace_ends_with_ret.
  ∀the_trace : trace_any_label (OC_abstract_status prog) trace_ends_flag start_status final_status.
  ∀program_counter_refl : (program_counter' = program_counter … start_status).
  ∀classify_assm: ASM_classify0 instruction = cl_return.
    ticks
     =compute_paid_trace_any_label … the_trace.
  #prog #program_counter' #program_size'
  #ticks #instruction #program_counter'' #FETCH
  #start_status #final_status #trace_ends_flag
  #the_trace #program_counter_refl #classify_assm
  @(trace_any_label_inv_ind … the_trace)
  [1:
    #start_status' #final_status' * #no_result #execute_assm #classifier_assm #costed_assm
    #trace_ends_flag_refl #start_status_refl #final_status_refl #the_trace_refl
    destruct @⊥
  |2:
    #start_status' #final_status' * #no_result #execute_assm #classifier_assm #trace_ends_flag_refl
    #start_status_refl #final_status_refl #the_trace_refl destruct
    whd in match (trace_any_label_length … (tal_base_return …));
    whd in match (compute_paid_trace_any_label … (tal_base_return …));
    <FETCH %
  |3:
    #status_pre_fun_call #status_start_fun_call #status_final * #no_result #execute_assm
    #classifier_assm #after_return_assm #trace_label_return #costed_assm
    #trace_ends_flag_refl #start_status_refl #final_status_refl #the_trace_refl
    destruct @⊥
  |4:
    #status_pre_fun_call #status_start_fun_call #status_final * #no_result #execute_assm
    #classifier_assm
    destruct @⊥
    change with (ASM_classify0 ? = ?) in classifier_assm;
    cases (current_instruction ??) in classifier_assm;
    [7: #preinstruction cases preinstruction ]
    try(#addr1 #addr2 #absurd normalize in absurd; destruct(absurd))
    try(#addr #absurd normalize in absurd; destruct(absurd))
    #absurd normalize in absurd; destruct(absurd)
  |5:
    #end_flag #status_pre_fun_call #status_start_fun_call #status_after_fun_call
    #status_final * #no_result #execute_assm #classifier_assm #after_return_assm #trace_label_return
    #costed_assm #trace_any_label #trace_ends_flag_refl #start_status_refl
    #final_status_refl #the_trace_refl
    destruct @⊥
  |6:
    #end_flag #status_pre #status_init #status_end * #no_result #execute_assm #trace_any_label
    #classifier_assm #costed_assm #trace_ends_flag_refl #start_status_refl
    #final_status_refl #the_trace_refl destruct @⊥
  ]
  try (change with (ASM_classify0 ? = ? ∨ ASM_classify0 ? = ?) in classifier_assm;)
  try (change with (ASM_classify0 ? = ?) in classifier_assm;)
  whd in match current_instruction in classifier_assm; normalize nodelta in classifier_assm;
  <FETCH in classifier_assm; >classify_assm
  #absurd try (destruct(absurd))
  cases absurd
  #absurd destruct(absurd)
qed.

lemma trace_any_label_length_leq_0_to_False:
  ∀prog: labelled_object_code.
  ∀trace_ends_flag: trace_ends_with_ret.
  ∀start_status: Status (cm prog).
  ∀final_status: Status (cm prog).
  ∀the_trace: trace_any_label (OC_abstract_status prog) trace_ends_flag start_status final_status.
   trace_any_label_length … the_trace ≤ 0 → False.
  #prog #trace_ends_flag #start_status #final_status #the_trace
  cases the_trace /2 by absurd/
qed.
      
let rec block_cost'
 (prog: labelled_object_code) (program_counter': Word)
    (program_size: nat)
      (first_time_around: bool)
        on program_size:
          Σcost_of_block: nat.
          if (match lookup_opt … program_counter' (costlabels prog) with [ None ⇒ true | _ ⇒ first_time_around ]) then
            ∀start_status,final_status: Status (cm prog).
            ∀trace_ends_flag.
            ∀the_trace: trace_any_label (OC_abstract_status prog) trace_ends_flag start_status final_status.
              trace_any_label_length … the_trace ≤ program_size →
              program_counter' = program_counter … start_status →
                cost_of_block = compute_paid_trace_any_label … the_trace
          else
            (cost_of_block = 0) ≝
  match program_size return λx. x = program_size → ? with
  [ O ⇒ λbase_case. 0 (* XXX: dummy to be inserted here *)
  | S program_size' ⇒ λstep_case.
    let 〈instruction, program_counter'', ticks〉 as FETCH ≝ fetch (cm prog) program_counter' in
    let to_continue ≝
      match lookup_opt … program_counter' (costlabels prog) with
      [ None ⇒ true
      | Some _ ⇒ first_time_around
      ]
    in
      ((if to_continue then
       pi1 … (match instruction return λx. x = instruction → ? with
        [ RealInstruction real_instruction ⇒ λreal_instruction_refl.
          match real_instruction return λx. x = real_instruction →
          Σcost_of_block: nat.
            ∀start_status,final_status: Status (cm prog).
            ∀trace_ends_flag.
            ∀the_trace: trace_any_label (OC_abstract_status prog) trace_ends_flag start_status final_status.
              trace_any_label_length … the_trace ≤ S program_size' →
              program_counter' = program_counter … start_status →
                cost_of_block = compute_paid_trace_any_label … the_trace with
          [ RET                    ⇒ λinstr. ticks
          | RETI                   ⇒ λinstr. ticks
          | JC   relative          ⇒ λinstr. ticks
          | JNC  relative          ⇒ λinstr. ticks
          | JB   bit_addr relative ⇒ λinstr. ticks
          | JNB  bit_addr relative ⇒ λinstr. ticks
          | JBC  bit_addr relative ⇒ λinstr. ticks
          | JZ   relative          ⇒ λinstr. ticks
          | JNZ  relative          ⇒ λinstr. ticks
          | CJNE src_trgt relative ⇒ λinstr. ticks
          | DJNZ src_trgt relative ⇒ λinstr. ticks
          | JMP   addr             ⇒ λinstr. (* XXX: actually a call due to use with fptrs *)
              ticks + block_cost' prog program_counter'' program_size' false
          | _                      ⇒ λinstr.
              ticks + block_cost' prog program_counter'' program_size' false
          ] (refl …)
        | ACALL addr     ⇒ λinstr.
            ticks + block_cost' prog program_counter'' program_size' false
        | AJMP  addr     ⇒ λinstr.
          let jump_target ≝ compute_target_of_unconditional_jump program_counter'' instruction in
            ticks + block_cost' prog jump_target program_size' false
        | LCALL addr     ⇒ λinstr.
            ticks + block_cost' prog program_counter'' program_size' false
        | LJMP  addr     ⇒ λinstr.
          let jump_target ≝ compute_target_of_unconditional_jump program_counter'' instruction in
            ticks + block_cost' prog jump_target program_size' false
        | SJMP  addr     ⇒ λinstr.
          let jump_target ≝ compute_target_of_unconditional_jump program_counter'' instruction in
            ticks + block_cost' prog jump_target program_size' false
        | MOVC  src trgt ⇒ λinstr.
            ticks + block_cost' prog program_counter'' program_size' false
        ] (refl …))
      else
        0)
      : Σcost_of_block: nat.
          match (match lookup_opt … program_counter' (costlabels prog) with [ None ⇒ true | _ ⇒ first_time_around ]) with
          [ true ⇒
            ∀start_status: Status (cm prog).
            ∀final_status: Status (cm prog).
            ∀trace_ends_flag.
            ∀the_trace: trace_any_label (OC_abstract_status prog) trace_ends_flag start_status final_status.
              trace_any_label_length … the_trace ≤ S program_size' →
              program_counter' = program_counter … start_status →
                cost_of_block = compute_paid_trace_any_label … the_trace
          | false ⇒
            (cost_of_block = 0)
          ])
  ] (refl …).
  [2:
    change with (if to_continue then ? else (? = 0))
    >p in ⊢ (match % return ? with [ _ ⇒ ? | _ ⇒ ? ]); normalize nodelta
    @pi2
  |1:
    destruct
    cases (lookup_opt ????) normalize nodelta
    [1:
      #start_status #final_status #trace_ends_flag #the_trace
      #absurd
      cases (trace_any_label_length_leq_0_to_False … absurd)
    |2:
      #cost cases first_time_around normalize nodelta try %
      #start_status #final_status #trace_ends_flag #the_trace #absurd
      cases (trace_any_label_length_leq_0_to_False … absurd)
    ]
  |3:
    change with (if to_continue then ? else (0 = 0))
    >p normalize nodelta %
  |6,7:
    #start_status #final_status #trace_ends_flag #the_trace #size_invariant #program_counter_refl
    @(trace_compute_paid_trace_cl_return … program_size' … FETCH … the_trace program_counter_refl)
    destruct %
  |4,46,47:
    #start_status #final_status #trace_ends_flag #the_trace #size_invariant #program_counter_refl
    cases(block_cost' ???) -block_cost'
    @(trace_compute_paid_trace_cl_call … program_size' … FETCH … the_trace program_counter_refl size_invariant)
    destruct %
  |43,44,45: (* XXX: unconditional jumps *)
    #start_status #final_status #trace_ends_flag #the_trace #size_invariant #program_counter_refl
    cases (block_cost' ???) -block_cost'
    lapply (trace_compute_paid_trace_cl_other … program_size' … FETCH … the_trace program_counter_refl size_invariant)
    whd in match (program_counter_after_other ??); normalize nodelta destruct
    whd in match (is_unconditional_jump ?); normalize nodelta #assm @assm %
  |25,26,27,28,29,30,31,32,33:
    #start_status #final_status #trace_ends_flag #the_trace #size_invariant #program_counter_refl
    @(trace_compute_paid_trace_cl_jump prog … first_time_around program_size' … FETCH … the_trace program_counter_refl)
   destruct %
  |4,33:
  |*:
    #start_status #final_status #trace_ends_flag #the_trace #size_invariant #program_counter_refl
    cases(block_cost' ???) -block_cost'
    lapply (trace_compute_paid_trace_cl_other … program_size' … FETCH … the_trace program_counter_refl size_invariant)      
    destruct #assm @assm %
  ]
qed.

definition block_cost:
    ∀prog: labelled_object_code.
    ∀program_counter': Word.
      Σcost_of_block: nat.
        ∀start_status: Status (cm prog).
        ∀final_status: Status (cm prog).
        ∀trace_ends_flag.
        ∀the_trace: trace_any_label (OC_abstract_status prog) trace_ends_flag start_status final_status.
        ∀unrepeating_witness: tal_unrepeating … the_trace.
          program_counter' = program_counter … start_status →
            cost_of_block = compute_paid_trace_any_label … the_trace.
  #prog #program_counter
  cases(block_cost' prog program_counter (2^16) true)
  #cost_of_block #block_cost_hyp
  %{cost_of_block}
  cases(lookup_opt … (costlabels prog)) in block_cost_hyp;
  [2: #cost_label] normalize nodelta
  #hyp #start_status #final_status #trace_ends_flag #the_trace #unrepeating_witness
  @hyp @tal_pc_list_length_leq_total_program_size try assumption
qed.