Changeset 1911


Ignore:
Timestamp:
Apr 27, 2012, 6:45:29 PM (7 years ago)
Author:
mulligan
Message:

Changed statement of block_cost' to start on new termination argument

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/ASMCosts.ma

    r1910 r1911  
    164164      let pc_difference ≝ nat_of_bitvector … (program_counter … status_init) - nat_of_bitvector … (program_counter … status_pre) in
    165165        pc_difference + tail_length       
     166  ].
     167
     168let rec trace_any_label_length'
     169  (code_memory: BitVectorTrie Byte 16) (cost_labels: BitVectorTrie costlabel 16)
     170    (trace_ends_flag: trace_ends_with_ret) (start_status: Status code_memory)
     171      (final_status: Status code_memory)
     172      (the_trace: trace_any_label (ASM_abstract_status code_memory cost_labels) trace_ends_flag start_status final_status)
     173        on the_trace: nat ≝
     174  match the_trace with
     175  [ tal_base_not_return the_status _ _ _ _ ⇒ 1
     176  | tal_base_call pre_fun_call start_fun_call final _ _ _ _ call_trace ⇒ 1
     177  | tal_base_return the_status _ _ _ ⇒ 1
     178  | tal_step_call end_flag pre_fun_call start_fun_call after_fun_call final _ _ _ call_trace _ final_trace ⇒
     179      let tail_length ≝ trace_any_label_length' … final_trace in
     180        S tail_length
     181  | tal_step_default end_flag status_pre status_init status_end _ tail_trace _ _ ⇒
     182      let tail_length ≝ trace_any_label_length' … tail_trace in
     183        S tail_length       
    166184  ].
    167185
     
    664682     
    665683let rec block_cost'
    666   (code_memory': BitVectorTrie Byte 16) (program_counter': Word) (visited: list Word)
     684  (code_memory': BitVectorTrie Byte 16) (program_counter': Word)
    667685    (program_size: nat) (total_program_size: nat) (cost_labels: BitVectorTrie costlabel 16)
    668686      (reachable_program_counter_witness: reachable_program_counter code_memory' total_program_size program_counter')
    669687        (good_program_witness: good_program code_memory' total_program_size) (first_time_around: bool)
    670688          on program_size:
    671           total_program_size ≤ program_size + nat_of_bitvector … program_counter' →
    672689          Σcost_of_block: nat.
    673690          if (match lookup_opt … program_counter' cost_labels with [ None ⇒ true | _ ⇒ first_time_around ]) then
     
    676693            ∀trace_ends_flag.
    677694            ∀the_trace: trace_any_label (ASM_abstract_status … cost_labels) trace_ends_flag start_status final_status.
     695              trace_any_label_length' … the_trace ≤ program_size →
    678696              program_counter' = program_counter … start_status →
    679697                cost_of_block = compute_paid_trace_any_label code_memory' cost_labels trace_ends_flag start_status final_status the_trace
    680698          else
    681699            (cost_of_block = 0) ≝
    682   match program_size return λprogram_size: nat. total_program_size ≤ program_size + nat_of_bitvector … program_counter' → ? with
    683   [ O ⇒ λbase_case. (* XXX: dummy to be inserted here *)
    684   | S program_size' ⇒ λrecursive_case.
     700  match program_size return λx. x = program_size → ? with
     701  [ O ⇒ λbase_case. 0 (* XXX: dummy to be inserted here *)
     702  | S program_size' ⇒ λstep_case.
    685703    let 〈instruction, program_counter'', ticks〉 as FETCH ≝ fetch code_memory' program_counter' in
    686704    let to_continue ≝
     
    699717            ∀trace_ends_flag.
    700718            ∀the_trace: trace_any_label (ASM_abstract_status code_memory' cost_labels) trace_ends_flag start_status final_status.
     719              trace_any_label_length' … the_trace ≤ S program_size' →
    701720              program_counter' = program_counter … start_status →
    702721                cost_of_block = compute_paid_trace_any_label code_memory' cost_labels trace_ends_flag start_status final_status the_trace with
     
    713732          | DJNZ src_trgt relative ⇒ λinstr. ticks
    714733          | _                      ⇒ λinstr.
    715               ticks + block_cost' code_memory' program_counter'' (program_counter'::visited) program_size' total_program_size cost_labels ? good_program_witness false ?
     734              ticks + block_cost' code_memory' program_counter'' program_size' total_program_size cost_labels ? good_program_witness false
    716735          ] (refl …)
    717736        | ACALL addr     ⇒ λinstr.
    718             ticks + block_cost' code_memory' program_counter'' (program_counter'::visited) program_size' total_program_size cost_labels ? good_program_witness false ?
     737            ticks + block_cost' code_memory' program_counter'' program_size' total_program_size cost_labels ? good_program_witness false
    719738        | AJMP  addr     ⇒ λinstr.
    720739          let jump_target ≝ compute_target_of_unconditional_jump program_counter'' instruction in
    721             ticks + block_cost' code_memory' jump_target (program_counter'::visited) program_size' total_program_size cost_labels ? good_program_witness false ?
     740            ticks + block_cost' code_memory' jump_target program_size' total_program_size cost_labels ? good_program_witness false
    722741        | LCALL addr     ⇒ λinstr.
    723             ticks + block_cost' code_memory' program_counter'' (program_counter'::visited) program_size' total_program_size cost_labels ? good_program_witness false ?
     742            ticks + block_cost' code_memory' program_counter'' program_size' total_program_size cost_labels ? good_program_witness false
    724743        | LJMP  addr     ⇒ λinstr.
    725744          let jump_target ≝ compute_target_of_unconditional_jump program_counter'' instruction in
    726             ticks + block_cost' code_memory' jump_target (program_counter'::visited) program_size' total_program_size cost_labels ? good_program_witness false ?
     745            ticks + block_cost' code_memory' jump_target program_size' total_program_size cost_labels ? good_program_witness false
    727746        | SJMP  addr     ⇒ λinstr.
    728747          let jump_target ≝ compute_target_of_unconditional_jump program_counter'' instruction in
    729             ticks + block_cost' code_memory' jump_target (program_counter'::visited) program_size' total_program_size cost_labels ? good_program_witness false ?
     748            ticks + block_cost' code_memory' jump_target program_size' total_program_size cost_labels ? good_program_witness false
    730749        | JMP   addr     ⇒ λinstr. (* XXX: actually a call due to use with fptrs *)
    731             ticks + block_cost' code_memory' program_counter'' (program_counter'::visited) program_size' total_program_size cost_labels ? good_program_witness false ?
     750            ticks + block_cost' code_memory' program_counter'' program_size' total_program_size cost_labels ? good_program_witness false
    732751        | MOVC  src trgt ⇒ λinstr.
    733             ticks + block_cost' code_memory' program_counter'' (program_counter'::visited) program_size' total_program_size cost_labels ? good_program_witness false ?
     752            ticks + block_cost' code_memory' program_counter'' program_size' total_program_size cost_labels ? good_program_witness false
    734753        ] (refl …))
    735754      else
     
    742761            ∀trace_ends_flag.
    743762            ∀the_trace: trace_any_label (ASM_abstract_status … cost_labels) trace_ends_flag start_status final_status.
     763              trace_any_label_length' … the_trace ≤ S program_size' →
    744764              program_counter' = program_counter … start_status →
    745765                cost_of_block = compute_paid_trace_any_label code_memory' cost_labels trace_ends_flag start_status final_status the_trace
     
    747767            (cost_of_block = 0)
    748768          ])
    749   ].
     769  ] (refl …).
    750770  [2:
    751771    change with (if to_continue then ? else (? = 0))
     
    753773    @pi2
    754774  |1:
    755     cases reachable_program_counter_witness #_ #hyp
    756     @(absurd (total_program_size < total_program_size) … (not_le_Sn_n …))
    757     @(le_to_lt_to_lt … base_case hyp)
     775    destruct
     776    cases (lookup_opt ? ? ? ?) normalize nodelta
     777    [1:
     778    |2:
     779      #_ cases first_time_around normalize nodelta
     780      [1:
     781        #start_status #final_status #trace_ends_flag #the_trace
     782        #absurd
     783      |2:
     784        %
     785      ]
     786    ]
    758787  |3:
    759788    change with (if to_continue then ? else (0 = 0))
Note: See TracChangeset for help on using the changeset viewer.