Changeset 2907 for src/ASM/ASMCosts.ma


Ignore:
Timestamp:
Mar 19, 2013, 7:48:19 PM (7 years ago)
Author:
sacerdot
Message:
  1. a few bugs fixed
  2. as_return implemented for ASM & OC
File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/ASMCosts.ma

    r2899 r2907  
    1 (* JHM: redundant includes
    2 include "ASM/ASM.ma".
    3 include "ASM/Arithmetic.ma".
    4 include "ASM/Fetch.ma".     (* includes ASM/ASM.ma and ASM/Arithmetic.ma *)
    5 *)
    6 
    7 include "ASM/Interpret.ma". (* includes ASM/Fetch.ma and ASM/AbstractStatus.ma *)
    8 
    9 (*include "common/StructuredTraces.ma". (* included by ASM/AbstractStatus.ma *) *)
    10 
    11 definition OC_abstract_status: ∀code_memory. BitVectorTrie costlabel 16 → abstract_status ≝
    12   λcode_memory.
    13   λcost_labels.
     1include "ASM/Interpret.ma".
     2
     3definition ASMRegisterRets: list [[ acc_a; direct; registr ]] ≝
     4 [ DIRECT (bitvector_of_nat 8 82);       (* DPL *)
     5   DIRECT (bitvector_of_nat 8 83);       (* DPH *)
     6   REGISTER [[ false; false; false ]];   (* Register00 *)
     7   REGISTER [[ false; false; true ]] ].  (* Register01 *)
     8% qed.
     9
     10definition as_result_of_finaladdr: ∀T:Type[0]. ∀cm:T. PreStatus … cm → Word → option int ≝
     11 λT,cm,st,finaladdr.
     12  if eq_bv ? (program_counter ?? st) finaladdr then
     13   let vals ≝
     14    map [[acc_a;direct;registr]] ? (get_arg_8 ?? st false) (ASMRegisterRets⌈list ? ↦ ?⌉) in
     15   let dummy ≝ zero ? in
     16   let first_byte ≝ λl. match l with [ nil ⇒ 〈dummy,[]〉 | cons hd tl ⇒ 〈hd,tl〉] in
     17   let 〈b1,tl1〉 ≝ first_byte vals in
     18   let 〈b2,tl2〉 ≝ first_byte tl1 in
     19   let 〈b3,tl3〉 ≝ first_byte tl2 in
     20   let 〈b4,tl4〉 ≝ first_byte tl3 in
     21    Some ? (b4 @@ b3 @@ b2 @@ b1)
     22  else
     23   None ?.
     24[ @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) % | % ]
     25qed.
     26
     27definition OC_abstract_status: labelled_object_code → abstract_status ≝
     28 λprog.
     29  let code_memory ≝ load_code_memory (oc prog) in
    1430    mk_abstract_status
    1531      (Status code_memory)
     
    1834      (program_counter …)
    1935      (OC_classify …)
    20       (λpc.lookup_opt … pc cost_labels)
     36      (λpc.lookup_opt … pc (costlabels prog))
    2137      (next_instruction_properly_relates_program_counters code_memory)
    22       ? (* (λs.False) *)
     38      (λst. as_result_of_finaladdr … st (final_pc prog))
    2339      ?
    2440      ?.
    25   #x cases daemon (* XXX: is_final predicate, (tail)call_ident function *)
     41  #x cases daemon (* XXX: (tail)call_ident function *)
    2642qed.
    2743
    2844definition trace_any_label_length ≝
    29   λcode_memory: BitVectorTrie Byte 16.
    30   λcost_labels: BitVectorTrie costlabel 16.
     45  λprog: labelled_object_code.
     46  let code_memory ≝ load_code_memory (oc prog) in
    3147  λtrace_ends_flag: trace_ends_with_ret.
    3248  λstart_status: Status code_memory.
    3349  λfinal_status: Status code_memory.
    34   λthe_trace: trace_any_label (OC_abstract_status … cost_labels) trace_ends_flag start_status final_status.
     50  λthe_trace: trace_any_label (OC_abstract_status prog) trace_ends_flag start_status final_status.
    3551    as_trace_any_label_length' … the_trace.
    3652
     
    150166
    151167lemma execute_1_and_program_counter_after_other_in_lockstep:
    152   ∀code_memory: BitVectorTrie Byte 16.
    153   ∀cost_labels: BitVectorTrie costlabel 16.
     168  ∀prog: labelled_object_code.
     169  let code_memory ≝ load_code_memory (oc prog) in
    154170  ∀start_status: Status code_memory.
    155     as_classifier (OC_abstract_status code_memory cost_labels) start_status cl_other →
     171    as_classifier (OC_abstract_status prog) start_status cl_other →
    156172      let 〈instruction, pc, ticks〉 ≝ fetch code_memory (program_counter … start_status) in
    157173        program_counter ? ? (execute_1 … start_status) =
    158174          program_counter_after_other pc instruction.
    159   #code_memory #cost_labels #start_status #classify_assm
     175  #prog #start_status #classify_assm
    160176  change with (ASM_classify0 ? = ?) in classify_assm;
    161177  destruct (classify_assm)
     
    164180
    165181lemma sublist_tal_pc_list_all_program_counter_list:
    166   ∀code_memory: BitVectorTrie Byte 16.
    167   ∀cost_labels: BitVectorTrie costlabel 16.
     182  ∀prog: labelled_object_code.
     183  let code_memory ≝ load_code_memory (oc prog) in
    168184  ∀start, final: Status code_memory.
    169185  ∀trace_ends_flag.
    170   ∀the_trace: trace_any_label (OC_abstract_status … cost_labels) trace_ends_flag start final.
     186  ∀the_trace: trace_any_label (OC_abstract_status prog) trace_ends_flag start final.
    171187    sublist ? (tal_pc_list … the_trace) (all_program_counter_list (2^16)).
    172   #code_memory #cost_labels #start #final #trace_ends_flag #the_trace
     188  #prog #start #final #trace_ends_flag #the_trace
    173189  whd in match (sublist ???); #pc #memb_assm
    174190  @lt_bound_mem_all_program_counter_list try %
     
    177193
    178194corollary tal_pc_list_length_leq_total_program_size:
    179   ∀code_memory: BitVectorTrie Byte 16.
    180   ∀cost_labels: BitVectorTrie costlabel 16.
     195  ∀prog: labelled_object_code.
     196  let code_memory ≝ load_code_memory (oc prog) in
    181197  ∀start, final: Status code_memory.
    182198  ∀trace_ends_flag.
    183   ∀the_trace: trace_any_label (OC_abstract_status … cost_labels) trace_ends_flag start final.
     199  ∀the_trace: trace_any_label (OC_abstract_status prog) trace_ends_flag start final.
    184200  ∀unrepeating_witness: tal_unrepeating … the_trace.
    185201    |tal_pc_list … the_trace| ≤ 2^16.
    186   #code_memory #cost_labels #start #final #trace_ends_flag #the_trace #unrepeating_witness
     202  #prog #start #final #trace_ends_flag #the_trace #unrepeating_witness
    187203  <(all_program_counter_list_bound_eq (2^16))
    188204  @sublist_length
     
    197213
    198214let rec compute_paid_trace_any_label
    199   (code_memory: BitVectorTrie Byte 16) (cost_labels: BitVectorTrie costlabel 16)
    200     (trace_ends_flag: trace_ends_with_ret) (start_status: Status code_memory)
    201       (final_status: Status code_memory)
    202         (the_trace: trace_any_label (OC_abstract_status … cost_labels) trace_ends_flag start_status final_status)
     215  (prog: labelled_object_code) (trace_ends_flag: trace_ends_with_ret)
     216   (start_status: Status (load_code_memory (oc prog)))
     217   (final_status: Status (load_code_memory (oc prog)))
     218        (the_trace: trace_any_label (OC_abstract_status prog) trace_ends_flag start_status final_status)
    203219       on the_trace: nat ≝
    204220  match the_trace with
     
    210226     _ _ _ call_trace _ final_trace ⇒
    211227      let current_instruction_cost ≝ current_instruction_cost … pre_fun_call in
    212       let final_trace_cost ≝ compute_paid_trace_any_label … cost_labels end_flag … final_trace in
     228      let final_trace_cost ≝ compute_paid_trace_any_label prog end_flag … final_trace in
    213229        current_instruction_cost + final_trace_cost
    214230  | tal_step_default end_flag status_pre status_init status_end _ tail_trace _ _ ⇒
    215231      let current_instruction_cost ≝ current_instruction_cost … status_pre in
    216232      let tail_trace_cost ≝
    217        compute_paid_trace_any_label … cost_labels end_flag
     233       compute_paid_trace_any_label prog end_flag
    218234        status_init status_end tail_trace
    219235      in
     
    222238
    223239definition compute_paid_trace_label_label ≝
    224   λcode_memory: BitVectorTrie Byte 16.
    225   λcost_labels: BitVectorTrie costlabel 16.
     240  λprog: labelled_object_code.
     241  let code_memory ≝ load_code_memory (oc prog) in
    226242  λtrace_ends_flag: trace_ends_with_ret.
    227243  λstart_status: Status code_memory.
    228244  λfinal_status: Status code_memory.
    229   λthe_trace: (trace_label_label (OC_abstract_status … cost_labels) trace_ends_flag start_status final_status).
     245  λthe_trace: (trace_label_label (OC_abstract_status prog) trace_ends_flag start_status final_status).
    230246  match the_trace with
    231247  [ tll_base ends_flag initial final given_trace labelled_proof ⇒
     
    234250
    235251lemma trace_compute_paid_trace_cl_other:
    236   ∀code_memory' : (BitVectorTrie Byte 16).
     252  ∀prog : labelled_object_code.
     253  let code_memory' ≝ load_code_memory (oc prog) in
    237254  ∀program_counter' : Word.
    238   ∀cost_labels : BitVectorTrie costlabel 16.
    239255  ∀program_size' : ℕ.
    240256  ∀ticks : ℕ.
     
    246262  ∀final_status : (Status code_memory').
    247263  ∀trace_ends_flag : trace_ends_with_ret.
    248   ∀the_trace : (trace_any_label (OC_abstract_status … cost_labels) trace_ends_flag start_status final_status).
     264  ∀the_trace : (trace_any_label (OC_abstract_status prog) trace_ends_flag start_status final_status).
    249265  ∀program_counter_refl : (program_counter' = program_counter … start_status).
    250266  ∀size_invariant : trace_any_label_length … the_trace ≤S program_size'.
    251267  ∀classify_assm: ASM_classify0 instruction = cl_other.
    252268  ∀pi1 : ℕ.
    253    (if match lookup_opt costlabel 16 program_counter''' cost_labels with 
     269   (if match lookup_opt costlabel 16 program_counter''' (costlabels prog) with 
    254270         [None ⇒ true
    255271         |Some _ ⇒ false
     
    259275      ∀final_status0:Status code_memory'.
    260276      ∀trace_ends_flag0:trace_ends_with_ret.
    261       ∀the_trace0:trace_any_label (OC_abstract_status … cost_labels) trace_ends_flag0 start_status0 final_status0.
     277      ∀the_trace0:trace_any_label (OC_abstract_status prog) trace_ends_flag0 start_status0 final_status0.
    262278        trace_any_label_length … the_trace0 ≤ program_size' →
    263279        program_counter''' = program_counter … start_status0 →
     
    267283   → ticks+pi1
    268284     =compute_paid_trace_any_label … the_trace.
    269   #code_memory' #program_counter' #cost_labels #program_size' #ticks #instruction
     285  #prog #program_counter' #program_size' #ticks #instruction
    270286  #program_counter'' #FETCH #start_status #final_status #trace_ends_flag #the_trace
    271287  #program_counter_refl #size_invariant #classify_assm #recursive_block_cost
     
    299315      whd in costed_assm:(?%);
    300316      generalize in match costed_assm;
    301       generalize in match (refl … (lookup_opt … (program_counter … (execute_1 … status_pre)) cost_labels));
     317      generalize in match (refl … (lookup_opt … (program_counter … (execute_1 … status_pre)) (costlabels prog)));
    302318      whd in match (as_label ??);
    303       generalize in match (lookup_opt … (program_counter … (execute_1 … status_pre)) cost_labels)
     319      generalize in match (lookup_opt … (program_counter … (execute_1 … status_pre)) (costlabels prog))
    304320        in ⊢ (??%? → % → ?);
    305321      #lookup_assm cases lookup_assm
     
    311327        #None_lookup_opt_assm <None_lookup_opt_assm
    312328        normalize nodelta #new_recursive_assm
    313         cases(new_recursive_assm (execute_1 code_memory' status_pre) status_end
     329        cases(new_recursive_assm (execute_1 ? status_pre) status_end
    314330          end_flag trace_any_label ? ?) try (>rewrite_assm %)
    315331        whd in match (current_instruction_cost … status_pre);
    316         cut(ticks = \snd (fetch code_memory'
     332        cut(ticks = \snd (fetch (load_code_memory (oc prog))
    317333           (program_counter … status_pre)))
    318334        [1,3:
     
    340356      whd in costed_assm;
    341357      generalize in match costed_assm;
    342       generalize in match (refl … (lookup_opt … (program_counter … (execute_1 … status_start)) cost_labels));
     358      generalize in match (refl … (lookup_opt … (program_counter … (execute_1 … status_start)) ?));
    343359      whd in match (as_label ??);
    344       generalize in match (lookup_opt … (program_counter … (execute_1 … status_start)) cost_labels)
     360      generalize in match (lookup_opt … (program_counter … (execute_1 … status_start)) (costlabels prog))
    345361        in ⊢ (??%? → % → ?);
    346362      #lookup_assm cases lookup_assm
     
    357373          #Some_lookup_opt_assm <Some_lookup_opt_assm
    358374          normalize nodelta #new_recursive_assm >new_recursive_assm
    359           cut(ticks = \snd (fetch code_memory'
     375          cut(ticks = \snd (fetch (load_code_memory (oc prog))
    360376             (program_counter … status_start)))
    361377          [1:
     
    392408
    393409lemma trace_compute_paid_trace_cl_jump:
    394   ∀code_memory': BitVectorTrie Byte 16.
     410  ∀prog: labelled_object_code.
     411  let code_memory' ≝ load_code_memory (oc prog) in
    395412  ∀program_counter': Word.
    396   ∀cost_labels: BitVectorTrie costlabel 16.
    397413  ∀first_time_around: bool.
    398414  ∀program_size': ℕ.
     
    404420  ∀final_status: (Status code_memory').
    405421  ∀trace_ends_flag: trace_ends_with_ret.
    406   ∀the_trace: (trace_any_label (OC_abstract_status … cost_labels) trace_ends_flag start_status final_status).
     422  ∀the_trace: (trace_any_label (OC_abstract_status prog) trace_ends_flag start_status final_status).
    407423  ∀program_counter_refl: (program_counter' = program_counter … start_status).
    408424  ∀classify_assm: ASM_classify0 instruction = cl_jump.
    409425    ticks
    410426     =compute_paid_trace_any_label … the_trace.
    411   #code_memory' #program_counter' #cost_labels #first_time_around
     427  #prog letin code_memory' ≝ (load_code_memory ?) #program_counter' #first_time_around
    412428  #program_size' #ticks #instruction #program_counter'' #FETCH
    413429  #start_status #final_status
     
    451467
    452468lemma trace_compute_paid_trace_cl_call:
    453   ∀code_memory' : (BitVectorTrie Byte 16).
     469  ∀prog: labelled_object_code.
     470  let code_memory' ≝ load_code_memory (oc prog) in
    454471  ∀program_counter' : Word.
    455   ∀cost_labels : BitVectorTrie costlabel 16.
    456472  ∀program_size' : ℕ.
    457473  ∀ticks : ℕ.
     
    462478  ∀final_status : (Status code_memory').
    463479  ∀trace_ends_flag : trace_ends_with_ret.
    464   ∀the_trace : trace_any_label (OC_abstract_status … cost_labels) trace_ends_flag start_status final_status.
     480  ∀the_trace : trace_any_label (OC_abstract_status prog) trace_ends_flag start_status final_status.
    465481  ∀program_counter_refl : (program_counter' = program_counter … start_status).
    466482  ∀size_invariant : trace_any_label_length … the_trace ≤S program_size'.
    467483  ∀classify_assm: ASM_classify0 instruction = cl_call.
    468484  (∀pi1:ℕ
    469   .if match lookup_opt costlabel 16 program_counter'' cost_labels with 
     485  .if match lookup_opt costlabel 16 program_counter'' (costlabels prog) with 
    470486      [None ⇒ true | Some _ ⇒ false] 
    471487   then (∀start_status0:Status code_memory'
     
    473489              .∀trace_ends_flag0:trace_ends_with_ret
    474490               .∀the_trace0:trace_any_label
    475                                         (OC_abstract_status … cost_labels)
     491                                        (OC_abstract_status prog)
    476492                                        trace_ends_flag0 start_status0 final_status0.
    477493                trace_any_label_length … the_trace0
     
    484500   → ticks+pi1
    485501     =compute_paid_trace_any_label … the_trace).
    486   #code_memory' #program_counter' #cost_labels #program_size'
     502  #prog letin code_memory' ≝ (load_code_memory ?) #program_counter' #program_size'
    487503  #ticks #instruction #program_counter'' #FETCH
    488504  #start_status #final_status #trace_ends_flag
     
    510526    whd in costed_assm;
    511527    generalize in match costed_assm;
    512     generalize in match (refl … (lookup_opt … (program_counter … status_final) cost_labels));
     528    generalize in match (refl … (lookup_opt … (program_counter … status_final) (costlabels prog)));
    513529    whd in match (as_label ??);
    514     generalize in match (lookup_opt … (program_counter … status_final) cost_labels)
     530    generalize in match (lookup_opt … (program_counter … status_final) ?)
    515531      in ⊢ (??%? → % → ?);
    516532    #lookup_assm cases lookup_assm
     
    552568    whd in costed_assm:(?%);
    553569    generalize in match costed_assm;
    554     generalize in match (refl … (lookup_opt … (program_counter … status_after_fun_call) cost_labels));
     570    generalize in match (refl … (lookup_opt … (program_counter … status_after_fun_call) (costlabels ?)));
    555571    whd in match (as_label ??);
    556     generalize in match (lookup_opt … (program_counter … status_after_fun_call) cost_labels)
     572    generalize in match (lookup_opt … (program_counter … status_after_fun_call) (costlabels prog))
    557573      in ⊢ (??%? → % → ?);
    558574    #lookup_assm cases lookup_assm
     
    590606
    591607lemma trace_compute_paid_trace_cl_return:
    592   ∀code_memory' : (BitVectorTrie Byte 16).
     608  ∀prog: labelled_object_code.
     609  let code_memory' ≝ load_code_memory (oc prog) in
    593610  ∀program_counter' : Word.
    594   ∀cost_labels : BitVectorTrie costlabel 16.
    595611  ∀program_size' : ℕ.
    596612  ∀ticks : ℕ.
     
    601617  ∀final_status : (Status code_memory').
    602618  ∀trace_ends_flag : trace_ends_with_ret.
    603   ∀the_trace : trace_any_label (OC_abstract_status … cost_labels) trace_ends_flag start_status final_status.
     619  ∀the_trace : trace_any_label (OC_abstract_status prog) trace_ends_flag start_status final_status.
    604620  ∀program_counter_refl : (program_counter' = program_counter … start_status).
    605621  ∀classify_assm: ASM_classify0 instruction = cl_return.
    606622    ticks
    607623     =compute_paid_trace_any_label … the_trace.
    608   #code_memory' #program_counter' #cost_labels #program_size'
     624  #prog letin code_memory' ≝ (load_code_memory ?) #program_counter' #program_size'
    609625  #ticks #instruction #program_counter'' #FETCH
    610626  #start_status #final_status #trace_ends_flag
     
    658674
    659675lemma trace_any_label_length_leq_0_to_False:
    660   ∀code_memory: BitVectorTrie Byte 16.
    661   ∀cost_labels: BitVectorTrie costlabel 16.
     676  ∀prog: labelled_object_code.
     677  let code_memory ≝ load_code_memory (oc prog) in
    662678  ∀trace_ends_flag: trace_ends_with_ret.
    663679  ∀start_status: Status code_memory.
    664680  ∀final_status: Status code_memory.
    665   ∀the_trace: trace_any_label (OC_abstract_status … cost_labels) trace_ends_flag start_status final_status.
     681  ∀the_trace: trace_any_label (OC_abstract_status prog) trace_ends_flag start_status final_status.
    666682   trace_any_label_length … the_trace ≤ 0 → False.
    667   #code_memory #cost_labels #trace_ends_flag #start_status #final_status
    668   #the_trace
    669   cases the_trace /2/
     683  #prog #trace_ends_flag #start_status #final_status #the_trace
     684  cases the_trace /2 by absurd/
    670685qed.
    671686     
    672687let rec block_cost'
    673   (code_memory': BitVectorTrie Byte 16) (program_counter': Word)
    674     (program_size: nat) (cost_labels: BitVectorTrie costlabel 16)
     688 (prog: labelled_object_code) (program_counter': Word)
     689    (program_size: nat)
    675690      (first_time_around: bool)
    676691        on program_size:
    677692          Σcost_of_block: nat.
    678           if (match lookup_opt … program_counter' cost_labels with [ None ⇒ true | _ ⇒ first_time_around ]) then
    679             ∀start_status: Status code_memory'.
    680             ∀final_status: Status code_memory'.
     693          if (match lookup_opt … program_counter' (costlabels prog) with [ None ⇒ true | _ ⇒ first_time_around ]) then
     694            ∀start_status,final_status: Status (load_code_memory (oc prog)).
    681695            ∀trace_ends_flag.
    682             ∀the_trace: trace_any_label (OC_abstract_status … cost_labels) trace_ends_flag start_status final_status.
     696            ∀the_trace: trace_any_label (OC_abstract_status prog) trace_ends_flag start_status final_status.
    683697              trace_any_label_length … the_trace ≤ program_size →
    684698              program_counter' = program_counter … start_status →
     
    686700          else
    687701            (cost_of_block = 0) ≝
     702  let code_memory' ≝ load_code_memory (oc prog) in
    688703  match program_size return λx. x = program_size → ? with
    689704  [ O ⇒ λbase_case. 0 (* XXX: dummy to be inserted here *)
    690705  | S program_size' ⇒ λstep_case.
    691     let 〈instruction, program_counter'', ticks〉 as FETCH ≝ fetch code_memory' program_counter' in
     706    let 〈instruction, program_counter'', ticks〉 as FETCH ≝ fetch (load_code_memory (oc prog)) program_counter' in
    692707    let to_continue ≝
    693       match lookup_opt … program_counter' cost_labels with
     708      match lookup_opt … program_counter' (costlabels prog) with
    694709      [ None ⇒ true
    695710      | Some _ ⇒ first_time_around
     
    701716          match real_instruction return λx. x = real_instruction →
    702717          Σcost_of_block: nat.
    703             ∀start_status: Status code_memory'.
    704             ∀final_status: Status code_memory'.
     718            ∀start_status,final_status: Status code_memory'.
    705719            ∀trace_ends_flag.
    706             ∀the_trace: trace_any_label (OC_abstract_status code_memory' cost_labels) trace_ends_flag start_status final_status.
     720            ∀the_trace: trace_any_label (OC_abstract_status prog) trace_ends_flag start_status final_status.
    707721              trace_any_label_length … the_trace ≤ S program_size' →
    708722              program_counter' = program_counter … start_status →
     
    720734          | DJNZ src_trgt relative ⇒ λinstr. ticks
    721735          | JMP   addr             ⇒ λinstr. (* XXX: actually a call due to use with fptrs *)
    722               ticks + block_cost' code_memory' program_counter'' program_size' cost_labels false
     736              ticks + block_cost' prog program_counter'' program_size' false
    723737          | _                      ⇒ λinstr.
    724               ticks + block_cost' code_memory' program_counter'' program_size' cost_labels false
     738              ticks + block_cost' prog program_counter'' program_size' false
    725739          ] (refl …)
    726740        | ACALL addr     ⇒ λinstr.
    727             ticks + block_cost' code_memory' program_counter'' program_size' cost_labels false
     741            ticks + block_cost' prog program_counter'' program_size' false
    728742        | AJMP  addr     ⇒ λinstr.
    729743          let jump_target ≝ compute_target_of_unconditional_jump program_counter'' instruction in
    730             ticks + block_cost' code_memory' jump_target program_size' cost_labels false
     744            ticks + block_cost' prog jump_target program_size' false
    731745        | LCALL addr     ⇒ λinstr.
    732             ticks + block_cost' code_memory' program_counter'' program_size' cost_labels false
     746            ticks + block_cost' prog program_counter'' program_size' false
    733747        | LJMP  addr     ⇒ λinstr.
    734748          let jump_target ≝ compute_target_of_unconditional_jump program_counter'' instruction in
    735             ticks + block_cost' code_memory' jump_target program_size' cost_labels false
     749            ticks + block_cost' prog jump_target program_size' false
    736750        | SJMP  addr     ⇒ λinstr.
    737751          let jump_target ≝ compute_target_of_unconditional_jump program_counter'' instruction in
    738             ticks + block_cost' code_memory' jump_target program_size' cost_labels false
     752            ticks + block_cost' prog jump_target program_size' false
    739753        | MOVC  src trgt ⇒ λinstr.
    740             ticks + block_cost' code_memory' program_counter'' program_size' cost_labels false
     754            ticks + block_cost' prog program_counter'' program_size' false
    741755        ] (refl …))
    742756      else
    743757        0)
    744758      : Σcost_of_block: nat.
    745           match (match lookup_opt … program_counter' cost_labels with [ None ⇒ true | _ ⇒ first_time_around ]) with
     759          match (match lookup_opt … program_counter' (costlabels prog) with [ None ⇒ true | _ ⇒ first_time_around ]) with
    746760          [ true ⇒
    747761            ∀start_status: Status code_memory'.
    748762            ∀final_status: Status code_memory'.
    749763            ∀trace_ends_flag.
    750             ∀the_trace: trace_any_label (OC_abstract_status … cost_labels) trace_ends_flag start_status final_status.
     764            ∀the_trace: trace_any_label (OC_abstract_status prog) trace_ends_flag start_status final_status.
    751765              trace_any_label_length … the_trace ≤ S program_size' →
    752766              program_counter' = program_counter … start_status →
     
    781795  |4,46,47:
    782796    #start_status #final_status #trace_ends_flag #the_trace #size_invariant #program_counter_refl
    783     cases(block_cost' ?????) -block_cost'
     797    cases(block_cost' ???) -block_cost'
    784798    @(trace_compute_paid_trace_cl_call … program_size' … FETCH … the_trace program_counter_refl size_invariant)
    785799    destruct %
    786800  |43,44,45: (* XXX: unconditional jumps *)
    787801    #start_status #final_status #trace_ends_flag #the_trace #size_invariant #program_counter_refl
    788     cases (block_cost' ?????) -block_cost'
     802    cases (block_cost' ???) -block_cost'
    789803    lapply (trace_compute_paid_trace_cl_other … program_size' … FETCH … the_trace program_counter_refl size_invariant)
    790804    whd in match (program_counter_after_other ??); normalize nodelta destruct
    791805    whd in match (is_unconditional_jump ?); normalize nodelta #assm @assm %
    792806  |25,26,27,28,29,30,31,32,33:
    793     #start_status #final_status #trace_ends_flag #the_trace #size_invariant #program_counter_refl 
    794     @(trace_compute_paid_trace_cl_jump … first_time_around program_size' … FETCH … the_trace program_counter_refl)
    795     destruct %
     807    #start_status #final_status #trace_ends_flag #the_trace #size_invariant #program_counter_refl
     808    @(trace_compute_paid_trace_cl_jump prog … first_time_around program_size' … FETCH … the_trace program_counter_refl)
     809   destruct %
    796810  |4,33:
    797811  |*:
    798812    #start_status #final_status #trace_ends_flag #the_trace #size_invariant #program_counter_refl
    799     cases(block_cost' ?????) -block_cost'
     813    cases(block_cost' ???) -block_cost'
    800814    lapply (trace_compute_paid_trace_cl_other … program_size' … FETCH … the_trace program_counter_refl size_invariant)     
    801815    destruct #assm @assm %
     
    804818
    805819definition block_cost:
    806     ∀code_memory': BitVectorTrie Byte 16.
     820    ∀prog: labelled_object_code.
    807821    ∀program_counter': Word.
    808     ∀cost_labels: BitVectorTrie costlabel 16.
    809822      Σcost_of_block: nat.
    810         ∀start_status: Status code_memory'.
    811         ∀final_status: Status code_memory'.
     823        ∀start_status: Status (load_code_memory (oc prog)).
     824        ∀final_status: Status (load_code_memory (oc prog)).
    812825        ∀trace_ends_flag.
    813         ∀the_trace: trace_any_label (OC_abstract_status … cost_labels) trace_ends_flag start_status final_status.
     826        ∀the_trace: trace_any_label (OC_abstract_status prog) trace_ends_flag start_status final_status.
    814827        ∀unrepeating_witness: tal_unrepeating … the_trace.
    815828          program_counter' = program_counter … start_status →
    816             cost_of_block = compute_paid_trace_any_label … the_trace ≝
    817   λcode_memory: BitVectorTrie Byte 16.
    818   λprogram_counter: Word.
    819   λcost_labels: BitVectorTrie costlabel 16. ?.
    820   cases(block_cost' code_memory program_counter (2^16) cost_labels true)
     829            cost_of_block = compute_paid_trace_any_label … the_trace.
     830  #prog #program_counter
     831  cases(block_cost' prog program_counter (2^16) true)
    821832  #cost_of_block #block_cost_hyp
    822833  %{cost_of_block}
    823   cases(lookup_opt … cost_labels) in block_cost_hyp;
     834  cases(lookup_opt … (costlabels prog)) in block_cost_hyp;
    824835  [2: #cost_label] normalize nodelta
    825836  #hyp #start_status #final_status #trace_ends_flag #the_trace #unrepeating_witness
Note: See TracChangeset for help on using the changeset viewer.