Changeset 1906


Ignore:
Timestamp:
Apr 26, 2012, 5:20:06 PM (7 years ago)
Author:
mulligan
Message:

Statements simplified in block_cost and dependencies

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/ASMCosts.ma

    r1904 r1906  
    545545      ∀the_trace0:trace_any_label (ASM_abstract_status code_memory' cost_labels) trace_ends_flag0 start_status0 final_status0.
    546546        program_counter'' = program_counter (BitVectorTrie Byte 16) code_memory' start_status0 →
    547         (* (∃n:ℕ.
    548             trace_any_label_length code_memory' cost_labels
    549               trace_ends_flag0 start_status0 final_status0 the_trace0
    550                 + S n
    551                   = total_program_size) *) True ∧
    552547                  pi1
    553548                    =compute_paid_trace_any_label code_memory' cost_labels
    554549                     trace_ends_flag0 start_status0 final_status0 the_trace0
    555550    else (pi1=O) )
    556    → (* (∃n:ℕ.
    557      trace_any_label_length code_memory' cost_labels trace_ends_flag
    558       start_status final_status the_trace
    559       +S n
    560       =total_program_size)
    561     *) True ∧ticks+pi1
     551   → ticks+pi1
    562552     =compute_paid_trace_any_label code_memory' cost_labels trace_ends_flag
    563553      start_status final_status the_trace.
     
    598588          cases(new_recursive_assm (execute_1 code_memory' status_pre) status_end
    599589            end_flag trace_any_label ?) try %
    600           #exists_assm #recursive_block_cost_assm %
     590          whd in match (current_instruction_cost … status_pre);
     591          cut(ticks = \snd (fetch code_memory'
     592             (program_counter (BitVectorTrie Byte 16) code_memory' status_pre)))
    601593          [1:
    602             cases exists_assm (* #exists_n #total_program_size_refl
    603             <total_program_size_refl
    604             %{(exists_n - (nat_of_bitvector 16
    605                 (program_counter (BitVectorTrie Byte 16) code_memory'
    606                   (execute_1 code_memory' status_pre))
    607                 - nat_of_bitvector 16
    608                   (program_counter (BitVectorTrie Byte 16) code_memory' status_pre)))}
    609             <plus_n_Sm <plus_n_Sm @eq_f >commutative_plus
    610             cases daemon *) @I
     594            <FETCH %
    611595          |2:
    612             >recursive_block_cost_assm
    613             whd in match (current_instruction_cost … status_pre);
    614             cut(ticks = \snd (fetch code_memory'
    615                (program_counter (BitVectorTrie Byte 16) code_memory' status_pre)))
    616             [1:
    617               <FETCH %
    618             |2:
    619               #ticks_refl_assm >ticks_refl_assm %
    620             ]
     596            #ticks_refl_assm >ticks_refl_assm %
    621597          ]
    622598        ]
     
    670646        |2:
    671647          #program_counter_assm >program_counter_assm <Some_lookup_opt_assm
    672           normalize nodelta #new_recursive_assm >new_recursive_assm %
     648          normalize nodelta #new_recursive_assm >new_recursive_assm
     649          cut(ticks = \snd (fetch code_memory'
     650             (program_counter (BitVectorTrie Byte 16) code_memory' status_start)))
    673651          [1:
    674           (*
    675             %{(pred total_program_size)} whd in ⊢ (??%?);
    676             @S_pred
    677             @(reachable_program_counter_to_0_lt_total_program_size … reachable_program_counter_witness) *) @I
     652            <FETCH %
    678653          |2:
    679             cut(ticks = \snd (fetch code_memory'
    680                (program_counter (BitVectorTrie Byte 16) code_memory' status_start)))
    681             [1:
    682               <FETCH %
    683             |2:
    684               #ticks_refl_assm >ticks_refl_assm
    685               <plus_n_O %
    686             ]
     654            #ticks_refl_assm >ticks_refl_assm
     655            <plus_n_O %
    687656          ]
    688657        ]
     
    728697  ∀program_counter_refl: (program_counter' = program_counter (BitVectorTrie Byte 16) code_memory' start_status).
    729698  ∀classify_assm: ASM_classify0 instruction = cl_jump.
    730    (* (∃n:ℕ
    731      .trace_any_label_length code_memory' cost_labels trace_ends_flag
    732       start_status final_status the_trace
    733       +S n
    734       =total_program_size)
    735     *) True ∧ ticks
     699    ticks
    736700     =compute_paid_trace_any_label code_memory' cost_labels trace_ends_flag
    737701      start_status final_status the_trace.
     
    751715    destruct
    752716    whd in match (trace_any_label_length … (tal_base_not_return …));
    753     whd in match (compute_paid_trace_any_label … (tal_base_not_return …)); %
    754     [1: (*
    755       %{(pred total_program_size)} whd in ⊢ (??%?);
    756       @S_pred
    757       @(reachable_program_counter_to_0_lt_total_program_size … reachable_program_counter_witness) *)
    758       @I
    759     |2:
    760       <FETCH %
    761     ]
     717    whd in match (compute_paid_trace_any_label … (tal_base_not_return …));
     718    <FETCH %
    762719  |2:
    763720    #start_status' #final_status' #execute_assm #classifier_assm #trace_ends_assm
     
    810767                .program_counter''
    811768                 =program_counter (BitVectorTrie Byte 16) code_memory' start_status0
    812                  →True (*(∃n:ℕ
    813                    .trace_any_label_length code_memory' cost_labels trace_ends_flag0
    814                     start_status0 final_status0 the_trace0
    815                     +S n
    816                     =total_program_size) *)
    817                   ∧pi1
     769                 → pi1
    818770                   =compute_paid_trace_any_label code_memory' cost_labels
    819771                    trace_ends_flag0 start_status0 final_status0 the_trace0) 
    820772   else (pi1=O) 
    821    →True (*(∃n:ℕ
    822      .trace_any_label_length code_memory' cost_labels trace_ends_flag
    823       start_status final_status the_trace
    824       +S n
    825       =total_program_size) *)
    826     ∧ticks+pi1
     773   → ticks+pi1
    827774     =compute_paid_trace_any_label code_memory' cost_labels trace_ends_flag
    828775      start_status final_status the_trace).
     
    868815      |2:
    869816        #program_counter_assm >program_counter_assm <Some_lookup_opt
    870         normalize nodelta #new_recursive_assm >new_recursive_assm %
    871         [1: (*
    872           %{(pred total_program_size)} whd in ⊢ (??%?);
    873           @S_pred
    874           @(reachable_program_counter_to_0_lt_total_program_size … reachable_program_counter_witness) *) @I
     817        normalize nodelta #new_recursive_assm >new_recursive_assm
     818        cut(ticks = \snd (fetch code_memory' (program_counter (BitVectorTrie Byte 16) code_memory' status_pre_fun_call)))
     819        [1:
     820          <FETCH %
    875821        |2:
    876           cut(ticks = \snd (fetch code_memory' (program_counter (BitVectorTrie Byte 16) code_memory' status_pre_fun_call)))
    877           [1:
    878             <FETCH %
    879           |2:
    880             #ticks_refl_assm >ticks_refl_assm
    881             <plus_n_O %
    882           ]
     822          #ticks_refl_assm >ticks_refl_assm
     823          <plus_n_O %
    883824        ]
    884825      ]
     
    907848      |2:
    908849        #program_counter_refl >program_counter_refl <None_lookup_opt_assm
    909         normalize nodelta #new_recursive_assm %
     850        normalize nodelta #new_recursive_assm
    910851        cases (new_recursive_assm … trace_any_label ?)
    911         [1,3:
    912           #exists_assm #recursive_block_cost_assm
    913           [2:
    914             >recursive_block_cost_assm
    915             @plus_right_monotone
    916             whd in ⊢ (???%); <FETCH %
    917           |1: (*
    918             cases exists_assm #exists_n #trace_total_program_size_assm
    919             generalize in match execute_assm; destruct #execute_assm
    920             %{(exists_n - ((nat_of_bitvector … (program_counter … status_after_fun_call)
    921                 - nat_of_bitvector … (program_counter … status_pre_fun_call))))}
    922             >commutative_plus in ⊢ (??(?%?)?);
    923             <plus_n_Sm <plus_n_Sm @eq_f >associative_plus in ⊢ (??%?);
    924             @plus_left_monotone @sym_eq <commutative_plus in ⊢ (???%);
    925             @plus_minus_m_m
    926             cases daemon (* XXX: !!! *) *) @I
    927           ]
    928         |2,4:
     852        [1:
     853          @plus_right_monotone whd in ⊢ (???%); <FETCH %
     854        |2:
    929855          %
    930856        ]
     
    962888  ∀program_counter_refl : (program_counter' = program_counter (BitVectorTrie Byte 16) code_memory' start_status).
    963889  ∀classify_assm: ASM_classify0 instruction = cl_return.
    964     (* (∃n:ℕ
    965      .trace_any_label_length code_memory' cost_labels trace_ends_flag
    966       start_status final_status the_trace
    967       +S n
    968       =total_program_size) *) True
    969     ∧ticks
     890    ticks
    970891     =compute_paid_trace_any_label code_memory' cost_labels trace_ends_flag
    971892      start_status final_status the_trace.
     
    984905    #start_status_refl #final_status_refl #the_trace_refl destruct
    985906    whd in match (trace_any_label_length … (tal_base_return …));
    986     whd in match (compute_paid_trace_any_label … (tal_base_return …)); %
    987     [1: (*
    988       %{(pred total_program_size)} whd in ⊢ (??%?);
    989       @S_pred
    990       @(reachable_program_counter_to_0_lt_total_program_size … reachable_program_counter_witness) *)
    991       @I
    992     |2:
    993       <FETCH %
    994     ]
     907    whd in match (compute_paid_trace_any_label … (tal_base_return …));
     908    <FETCH %
    995909  |3:
    996910    #status_pre_fun_call #status_start_fun_call #status_final #execute_assm
     
    1033947            ∀the_trace: trace_any_label (ASM_abstract_status … cost_labels) trace_ends_flag start_status final_status.
    1034948              program_counter' = program_counter … start_status →
    1035                 (* (∃n: nat. trace_any_label_length … the_trace + (S n) = total_program_size) *) True ∧
    1036                   cost_of_block = compute_paid_trace_any_label code_memory' cost_labels trace_ends_flag start_status final_status the_trace
     949                cost_of_block = compute_paid_trace_any_label code_memory' cost_labels trace_ends_flag start_status final_status the_trace
    1037950          else
    1038951            (cost_of_block = 0) ≝
     
    1057970            ∀the_trace: trace_any_label (ASM_abstract_status code_memory' cost_labels) trace_ends_flag start_status final_status.
    1058971              program_counter' = program_counter … start_status →
    1059                 (* (∃n: nat. trace_any_label_length … the_trace + (S n) = total_program_size) *) True ∧
    1060                   cost_of_block = compute_paid_trace_any_label code_memory' cost_labels trace_ends_flag start_status final_status the_trace with
     972                cost_of_block = compute_paid_trace_any_label code_memory' cost_labels trace_ends_flag start_status final_status the_trace with
    1061973          [ RET                    ⇒ λinstr. ticks
    1062974          | RETI                   ⇒ λinstr. ticks
     
    10961008            ∀the_trace: trace_any_label (ASM_abstract_status … cost_labels) trace_ends_flag start_status final_status.
    10971009              program_counter' = program_counter … start_status →
    1098                 (* (∃n: nat. trace_any_label_length … the_trace + (S n) = total_program_size) *) True ∧
    1099                   cost_of_block = compute_paid_trace_any_label code_memory' cost_labels trace_ends_flag start_status final_status the_trace
     1010                cost_of_block = compute_paid_trace_any_label code_memory' cost_labels trace_ends_flag start_status final_status the_trace
    11001011          | false ⇒
    11011012            (cost_of_block = 0)
     
    12751186        ∀the_trace: trace_any_label (ASM_abstract_status … cost_labels) trace_ends_flag start_status final_status.
    12761187          program_counter' = program_counter … start_status →
    1277             (* (∃n: nat. trace_any_label_length … the_trace + (S n) = total_program_size) *) True ∧
    1278               cost_of_block = compute_paid_trace_any_label code_memory' cost_labels trace_ends_flag start_status final_status the_trace ≝
     1188            cost_of_block = compute_paid_trace_any_label code_memory' cost_labels trace_ends_flag start_status final_status the_trace ≝
    12791189  λcode_memory: BitVectorTrie Byte 16.
    12801190  λprogram_counter: Word.
Note: See TracChangeset for help on using the changeset viewer.