Changeset 1912


Ignore:
Timestamp:
May 3, 2012, 4:11:36 PM (7 years ago)
Author:
mulligan
Message:

Patches to get block_cost' and dependencies working again after change to termination argument. Six goals remain, currently closed by daemons, corresponding to two goals for each unconditional jump.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/ASMCosts.ma

    r1911 r1912  
    282282  ∀good_program_witness : (good_program code_memory' total_program_size).
    283283  ∀program_size' : ℕ.
    284   ∀recursive_case : (total_program_size≤S program_size'+nat_of_bitvector 16 program_counter').
    285284  ∀ticks : ℕ.
    286285  ∀instruction : instruction.
     
    293292  ∀the_trace : (trace_any_label (ASM_abstract_status code_memory' cost_labels) trace_ends_flag start_status final_status).
    294293  ∀program_counter_refl : (program_counter' = program_counter (BitVectorTrie Byte 16) code_memory' start_status).
     294  ∀size_invariant : trace_any_label_length' code_memory' cost_labels trace_ends_flag start_status final_status the_trace ≤S program_size'.
    295295  ∀classify_assm: ASM_classify0 instruction = cl_other.
    296296  ∀pi1 : ℕ.
     
    304304      ∀trace_ends_flag0:trace_ends_with_ret.
    305305      ∀the_trace0:trace_any_label (ASM_abstract_status code_memory' cost_labels) trace_ends_flag0 start_status0 final_status0.
     306        trace_any_label_length' code_memory' cost_labels trace_ends_flag0
     307          start_status0 final_status0 the_trace0 ≤ program_size' →
    306308        program_counter''' = program_counter (BitVectorTrie Byte 16) code_memory' start_status0 →
    307309                  pi1
     
    314316  #code_memory' #program_counter' #total_program_size #cost_labels
    315317  #reachable_program_counter_witness #good_program_witness
    316   #program_size' #recursive_case #ticks #instruction #program_counter'' #FETCH
     318  #program_size' #ticks #instruction #program_counter'' #FETCH
    317319  #start_status #final_status
    318   #trace_ends_flag #the_trace #program_counter_refl #classify_assm #recursive_block_cost
     320  #trace_ends_flag #the_trace #program_counter_refl #size_invariant #classify_assm #recursive_block_cost
    319321  #recursive_assm
    320322  @(trace_any_label_inv_ind … the_trace)
     
    340342        normalize nodelta #new_recursive_assm
    341343        cases(new_recursive_assm (execute_1 code_memory' status_pre) status_end
    342           end_flag trace_any_label ?) try %
     344          end_flag trace_any_label ? ?) try %
    343345        whd in match (current_instruction_cost … status_pre);
    344346        cut(ticks = \snd (fetch code_memory'
    345347           (program_counter (BitVectorTrie Byte 16) code_memory' status_pre)))
    346         [1,3:
     348        [1,3,5:
    347349          <FETCH %
    348350        |2:
    349           #ticks_refl_assm >ticks_refl_assm %
     351          #ticks_refl_assm
     352          >ticks_refl_assm %
    350353        |4:
    351354          #ticks_refl_assm
    352           >rewrite_assm %
     355          change with (S ? ≤ S ?) in size_invariant;
     356          lapply (le_S_S_to_le … size_invariant) #assm
     357          assumption
     358        |6:
     359          #ticks_refl_assm
     360          <rewrite_assm %
    353361        ]
    354362      |2:
     
    434442  ∀first_time_around: bool.
    435443  ∀program_size': ℕ.
    436   ∀recursive_case: total_program_size ≤ S program_size'+nat_of_bitvector 16 program_counter'.
    437444  ∀ticks: ℕ.
    438445  ∀instruction: instruction.
     
    450457  #code_memory' #program_counter' #total_program_size #cost_labels
    451458  #reachable_program_counter_witness #good_program_witness #first_time_around
    452   #program_size' #recursive_case #ticks #instruction #program_counter'' #FETCH
     459  #program_size' #ticks #instruction #program_counter'' #FETCH
    453460  #start_status #final_status
    454461  #trace_ends_flag #the_trace #program_counter_refl #classify_assm
     
    493500  ∀good_program_witness : (good_program code_memory' total_program_size).
    494501  ∀program_size' : ℕ.
    495   ∀recursive_case : (total_program_size≤S program_size'+nat_of_bitvector 16 program_counter').
    496502  ∀ticks : ℕ.
    497503  ∀instruction : instruction.
     
    503509  ∀the_trace : (trace_any_label (ASM_abstract_status code_memory' cost_labels) trace_ends_flag start_status final_status).
    504510  ∀program_counter_refl : (program_counter' = program_counter (BitVectorTrie Byte 16) code_memory' start_status).
     511  ∀size_invariant : trace_any_label_length' code_memory' cost_labels trace_ends_flag start_status final_status the_trace ≤S program_size'.
    505512  ∀classify_assm: ASM_classify0 instruction = cl_call.
    506513  (∀pi1:ℕ
     
    512519               .∀the_trace0:trace_any_label
    513520                                        (ASM_abstract_status code_memory' cost_labels)
    514                                         trace_ends_flag0 start_status0 final_status0
    515                 .program_counter''
     521                                        trace_ends_flag0 start_status0 final_status0.
     522                trace_any_label_length' code_memory' cost_labels trace_ends_flag0
     523                  start_status0 final_status0 the_trace0
     524                   ≤ program_size' →
     525                program_counter''
    516526                 =program_counter (BitVectorTrie Byte 16) code_memory' start_status0
    517527                 → pi1
     
    524534  #code_memory' #program_counter' #total_program_size #cost_labels
    525535  #reachable_program_counter_witness #good_program_witness #program_size'
    526   #recursive_case #ticks #instruction #program_counter'' #FETCH
     536  #ticks #instruction #program_counter'' #FETCH
    527537  #start_status #final_status #trace_ends_flag
    528   #the_trace #program_counter_refl #classify_assm #recursive_block_cost #recursive_assm
     538  #the_trace #program_counter_refl #size_invariant #classify_assm
     539  #recursive_block_cost #recursive_assm
    529540  @(trace_any_label_inv_ind … the_trace)
    530541  [5:
     
    597608        #program_counter_refl >program_counter_refl <None_lookup_opt_assm
    598609        normalize nodelta #new_recursive_assm
    599         cases (new_recursive_assm … trace_any_label ?)
     610        cases (new_recursive_assm … trace_any_label ? ?)
    600611        [1:
    601612          @plus_right_monotone whd in ⊢ (???%); <FETCH %
    602613        |2:
     614          normalize in size_invariant;
     615          lapply (le_S_S_to_le … size_invariant)
     616          #assm assumption
     617        |3:
    603618          %
    604619        ]
     
    625640  ∀good_program_witness : (good_program code_memory' total_program_size).
    626641  ∀program_size' : ℕ.
    627   ∀recursive_case : (total_program_size≤S program_size'+nat_of_bitvector 16 program_counter').
    628642  ∀ticks : ℕ.
    629643  ∀instruction : instruction.
     
    641655  #code_memory' #program_counter' #total_program_size #cost_labels
    642656  #reachable_program_counter_witness #good_program_witness #program_size'
    643   #recursive_case #ticks #instruction #program_counter'' #FETCH
     657  #ticks #instruction #program_counter'' #FETCH
    644658  #start_status #final_status #trace_ends_flag
    645659  #the_trace #program_counter_refl #classify_assm
     
    679693  cases absurd
    680694  #absurd destruct(absurd)
     695qed.
     696
     697lemma trace_any_label_length_leq_0_to_False:
     698  ∀code_memory: BitVectorTrie Byte 16.
     699  ∀cost_labels: BitVectorTrie costlabel 16.
     700  ∀trace_ends_flag: trace_ends_with_ret.
     701  ∀start_status: Status code_memory.
     702  ∀final_status: Status code_memory.
     703  ∀the_trace.
     704  trace_any_label_length' code_memory cost_labels trace_ends_flag start_status
     705    final_status the_trace ≤ 0 → False.
     706  #code_memory #cost_labels #trace_ends_flag #start_status #final_status
     707  #the_trace
     708  cases the_trace /2/
    681709qed.
    682710     
     
    774802  |1:
    775803    destruct
    776     cases (lookup_opt ? ? ? ?) normalize nodelta
     804    cases (lookup_opt ????) normalize nodelta
    777805    [1:
     806      #start_status #final_status #trace_ends_flag #the_trace
     807      #absurd
     808      cases (trace_any_label_length_leq_0_to_False … absurd)
    778809    |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       ]
     810      #cost cases first_time_around normalize nodelta try %
     811      #start_status #final_status #trace_ends_flag #the_trace #absurd
     812      cases (trace_any_label_length_leq_0_to_False … absurd)
    786813    ]
    787814  |3:
    788815    change with (if to_continue then ? else (0 = 0))
    789816    >p normalize nodelta %
    790   |7,8:
    791     #start_status #final_status #trace_ends_flag #the_trace #program_counter_refl
    792     @(trace_compute_paid_trace_cl_return … reachable_program_counter_witness good_program_witness … recursive_case … FETCH … the_trace program_counter_refl)
     817  |6,7:
     818    #start_status #final_status #trace_ends_flag #the_trace #size_invariant #program_counter_refl
     819    @(trace_compute_paid_trace_cl_return … reachable_program_counter_witness good_program_witness program_size' … FETCH … the_trace program_counter_refl)
    793820    destruct %
    794   |96,108,111:
    795     #start_status #final_status #trace_ends_flag #the_trace #program_counter_refl
    796     cases(block_cost' ??????????) -block_cost'
    797     @(trace_compute_paid_trace_cl_call … reachable_program_counter_witness good_program_witness … recursive_case … FETCH … program_counter_refl)
     821  |69,77,79:
     822    #start_status #final_status #trace_ends_flag #the_trace #size_invariant #program_counter_refl
     823    cases(block_cost' ????????) -block_cost'
     824    @(trace_compute_paid_trace_cl_call … reachable_program_counter_witness good_program_witness program_size' … FETCH … the_trace program_counter_refl size_invariant)
    798825    destruct %
    799   |4,9,12,15,18,21,24,27,30,33,36,39,42,45,48,51,54,57,69,72,75,78,81,84,87,
    800    90,93,99,102,105:
    801     #start_status #final_status #trace_ends_flag #the_trace #program_counter_refl
    802     cases(block_cost' ??????????) -block_cost'
    803     lapply (trace_compute_paid_trace_cl_other ???? reachable_program_counter_witness good_program_witness ? recursive_case ??? FETCH ??? the_trace program_counter_refl)
    804     normalize nodelta destruct #assm @assm %
    805   |60,61,62,63,64,65,66,67,68:
    806     #start_status #final_status #trace_ends_flag #the_trace #program_counter_refl
    807     @(trace_compute_paid_trace_cl_jump … reachable_program_counter_witness good_program_witness … recursive_case … FETCH … the_trace program_counter_refl)
     826  |4,8,10,12,14,16,18,20,22,24,26,28,30,32,34,36,38,40,51,53,55,57,59,61,63,65,
     827    67:
     828    #start_status #final_status #trace_ends_flag #the_trace #size_invariant #program_counter_refl
     829    cases(block_cost' ????????) -block_cost'
     830    lapply (trace_compute_paid_trace_cl_other … reachable_program_counter_witness good_program_witness program_size' … FETCH … the_trace program_counter_refl size_invariant)     
     831    destruct #assm @assm %
     832  |42,43,44,45,46,47,48,49,50:
     833    #start_status #final_status #trace_ends_flag #the_trace #size_invariant #program_counter_refl
     834    @(trace_compute_paid_trace_cl_jump … reachable_program_counter_witness good_program_witness … FETCH … the_trace program_counter_refl)
    808835    destruct %
     836  |71,73,75: (* XXX: unconditional jumps *)
     837    #start_status #final_status #trace_ends_flag #the_trace #size_invariant #program_counter_refl
     838    cases (block_cost' ????????) -block_cost'
     839    cases daemon
    809840  ]
    810841  -block_cost'
    811   [63:
     842  [32:
    812843    cases reachable_program_counter_witness * #n #fetch_n_hyp #lt_hyp
    813844    lapply(good_program_witness program_counter' reachable_program_counter_witness)
     
    824855      assumption
    825856    ]
    826   |64:
    827     cases reachable_program_counter_witness * #n #fetch_n_hyp #lt_hyp
    828     lapply(good_program_witness program_counter' reachable_program_counter_witness)
    829     <FETCH normalize nodelta <instr normalize nodelta
    830     @(subaddressing_mode_elim … [[addr16]] … [[addr16]]) [1: // ] #new_addr
    831     * * * * #n'
    832     #_ #_ #program_counter_lt' #program_counter_lt_tps'
    833     @(transitive_le
    834       total_program_size
    835       ((S program_size') + nat_of_bitvector … program_counter')
    836       (program_size' + nat_of_bitvector … program_counter'') recursive_case)
    837     normalize in match (S program_size' + nat_of_bitvector … program_counter');
    838     >plus_n_Sm
    839     @monotonic_le_plus_r
    840     change with (
    841       nat_of_bitvector … program_counter' <
    842         nat_of_bitvector … program_counter'')
    843     assumption
    844   |65:
     857  |33:
    845858    cases reachable_program_counter_witness * #n #fetch_n_hyp #lt_hyp
    846859    lapply(good_program_witness program_counter' reachable_program_counter_witness)
     
    859872      assumption
    860873    ]
    861   |66:
    862     cases reachable_program_counter_witness * #n #fetch_n_hyp #lt_hyp
    863     lapply(good_program_witness program_counter' reachable_program_counter_witness)
    864     <FETCH normalize nodelta <instr normalize nodelta
    865     @(subaddressing_mode_elim … [[addr11]] … [[addr11]]) [1: // ] #new_addr
    866     cases (split … 8 8 program_counter'') #pc_bu #pc_bl normalize nodelta
    867     cases (split … 3 8 new_addr) #thr #eig normalize nodelta
    868     cases (split … 5 3 pc_bu) #fiv #thr' normalize nodelta * * * * #n'
    869     #_ #_ #program_counter_lt' #program_counter_lt_tps'
    870     @(transitive_le
    871       total_program_size
    872       ((S program_size') + nat_of_bitvector … program_counter')
    873       (program_size' + nat_of_bitvector … program_counter'') recursive_case)
    874     normalize in match (S program_size' + nat_of_bitvector … program_counter');
    875     >plus_n_Sm
    876     @monotonic_le_plus_r
    877     change with (
    878       nat_of_bitvector … program_counter' <
    879         nat_of_bitvector … program_counter'')
    880     assumption
    881   |53,55:
     874  |27,28:
    882875    cases reachable_program_counter_witness * #n #fetch_n_hyp #lt_hyp
    883876    lapply(good_program_witness program_counter' reachable_program_counter_witness)
     
    891884      assumption
    892885    ]
    893   |54,56:
    894     cases reachable_program_counter_witness * #n #fetch_n_hyp #lt_hyp
    895     lapply(good_program_witness program_counter' reachable_program_counter_witness)
    896     <FETCH normalize nodelta <instr normalize nodelta
    897     try(<real_instruction_refl <instr normalize nodelta) *
    898     #pc_pc_lt_hyp' #pc_tps_lt_hyp'
    899     @(transitive_le
    900       total_program_size
    901       ((S program_size') + nat_of_bitvector … program_counter')
    902       (program_size' + nat_of_bitvector … program_counter'') recursive_case)
    903     normalize in match (S program_size' + nat_of_bitvector … program_counter');
    904     >plus_n_Sm
    905     @monotonic_le_plus_r
    906     change with (
    907       nat_of_bitvector … program_counter' <
    908         nat_of_bitvector … program_counter'')
    909     assumption
    910   |1,3,5,7,9,11,13,15,17,19,21,23,25,27,29,31,33,35,37,39,41,43,45,47,49,51,53,
    911    55:
     886  |1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23,24,25,26:
    912887    cases reachable_program_counter_witness * #n #fetch_n_hyp #lt_hyp
    913888    lapply(good_program_witness program_counter' reachable_program_counter_witness)
     
    918893    <FETCH normalize nodelta whd in match ltb; normalize nodelta
    919894    >(le_to_leb_true … program_counter_lt') %
    920   |2,4,6,8,10,12,14,16,18,20,22,24,26,28,30,32,34,36,38,40,42,44,46,48,50,52,54,
    921    56:
    922     cases reachable_program_counter_witness * #n #fetch_n_hyp #lt_hyp
    923     lapply(good_program_witness program_counter' reachable_program_counter_witness)
    924     <FETCH normalize nodelta
    925     <real_instruction_refl <instr normalize nodelta *
    926     #pc_pc_lt_hyp' #pc_tps_lt_hyp'
    927     @(transitive_le
    928       total_program_size
    929       ((S program_size') + nat_of_bitvector … program_counter')
    930       (program_size' + nat_of_bitvector … program_counter'') recursive_case)
    931     normalize in match (S program_size' + nat_of_bitvector … program_counter');
    932     >plus_n_Sm
    933     @monotonic_le_plus_r
    934     change with (
    935       nat_of_bitvector … program_counter' <
    936         nat_of_bitvector … program_counter'')
    937     assumption
    938   |*:
    939     normalize nodelta
    940     cases daemon (* XXX: new goals using jump_target *)
     895  |*: (* XXX: unconditional jumps *)
     896    cases daemon
    941897  ]
    942898qed.
Note: See TracChangeset for help on using the changeset viewer.