Changeset 2575


Ignore:
Timestamp:
Jan 9, 2013, 8:51:17 PM (7 years ago)
Author:
mckinna
Message:

temporary commit

localised the source of trouble in the proof of

trace_compute_paid_trace_cl_other:

the case split on instruction in the left branch of the disjunction in ...
... the *first* case arising from inversion by

@(trace_any_label_inv_ind … the_trace)

now there are many branches left unclosed
(by contrast with the r2531 version before structured traces changed)

-matita runs out of memory/dumps core if you try to examine them all
-a problem with having too many tabs open?

how to fix this?
is this problem arising as a consequence of
the cost of the_trace not being defined in the tailcall case?

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/ASMCosts.ma

    r2573 r2575  
    66(*include "common/StructuredTraces.ma". (* already included by ASM/AbstractStatus.ma *) *)
    77
    8 (* should this definition be moved to ASM/AbstractStatus.ma ??? *)
     8(* could this definition be moved to ASM/AbstractStatus.ma ???
     9   no: requires ASM/Interpret/execute_1 *)
    910
    1011definition ASM_abstract_status: ∀code_memory. BitVectorTrie costlabel 16 → abstract_status ≝
     
    1718      (program_counter …)
    1819      (λs. Some ? (ASM_classify … s))
    19       (λpc.lookup_opt ?? pc cost_labels)
     20      (λpc.lookup_opt pc cost_labels)
    2021      (next_instruction_properly_relates_program_counters code_memory)
    2122      ? (* (λs.False) *)
     
    3536  λstart_status: Status code_memory.
    3637  λfinal_status: Status code_memory.
    37   λthe_trace: trace_any_label (ASM_abstract_status code_memory cost_labels) trace_ends_flag start_status final_status.
     38  λthe_trace: trace_any_label (ASM_abstract_status cost_labels) trace_ends_flag start_status final_status.
    3839    as_trace_any_label_length' … the_trace.
    3940
     
    140141  ∀code_memory: BitVectorTrie Byte 16.
    141142  ∀start_status: Status code_memory.
    142     ASM_classify code_memory start_status = cl_other →
     143    ASM_classify start_status = cl_other →
    143144      let 〈instruction, pc, ticks〉 ≝ fetch code_memory (program_counter … start_status) in
    144145        program_counter ? ? (execute_1 … start_status) =
     
    178179  ∀start, final: Status code_memory.
    179180  ∀trace_ends_flag.
    180   ∀the_trace: trace_any_label (ASM_abstract_status code_memory cost_labels) trace_ends_flag start final.
     181  ∀the_trace: trace_any_label (ASM_abstract_status cost_labels) trace_ends_flag start final.
    181182    sublist ? (tal_pc_list … the_trace) (all_program_counter_list (2^16)).
    182183  #code_memory #cost_labels #start #final #trace_ends_flag #the_trace
     
    191192  ∀start, final: Status code_memory.
    192193  ∀trace_ends_flag.
    193   ∀the_trace: trace_any_label (ASM_abstract_status code_memory cost_labels) trace_ends_flag start final.
    194   ∀unrepeating_witness: tal_unrepeating (ASM_abstract_status code_memory cost_labels) trace_ends_flag start final the_trace.
     194  ∀the_trace: trace_any_label (ASM_abstract_status cost_labels) trace_ends_flag start final.
     195  ∀unrepeating_witness: tal_unrepeating the_trace.
    195196    |tal_pc_list … the_trace| ≤ 2^16.
    196197  #code_memory #cost_labels #start #final #trace_ends_flag #the_trace #unrepeating_witness
     
    210211    (trace_ends_flag: trace_ends_with_ret) (start_status: Status code_memory)
    211212      (final_status: Status code_memory)
    212         (the_trace: trace_any_label (ASM_abstract_status code_memory cost_labels) trace_ends_flag start_status final_status)
     213        (the_trace: trace_any_label (ASM_abstract_status cost_labels) trace_ends_flag start_status final_status)
    213214       on the_trace: nat ≝
    214215  match the_trace with
     
    239240  λstart_status: Status code_memory.
    240241  λfinal_status: Status code_memory.
    241   λthe_trace: trace_label_label (ASM_abstract_status … cost_labels) trace_ends_flag start_status final_status.
     242  λthe_trace: (trace_label_label (ASM_abstract_status … cost_labels) trace_ends_flag start_status final_status).
    242243  match the_trace with
    243244  [ tll_base ends_flag initial final given_trace labelled_proof ⇒
     
    258259  ∀final_status : (Status code_memory').
    259260  ∀trace_ends_flag : trace_ends_with_ret.
    260   ∀the_trace : (trace_any_label (ASM_abstract_status code_memory' cost_labels) trace_ends_flag start_status final_status).
     261  ∀the_trace : (trace_any_label (ASM_abstract_status cost_labels) trace_ends_flag start_status final_status).
    261262  ∀program_counter_refl : (program_counter' = program_counter … start_status).
    262   ∀size_invariant : trace_any_label_length code_memory' cost_labels trace_ends_flag start_status final_status the_trace ≤S program_size'.
     263  ∀size_invariant : trace_any_label_length the_trace ≤S program_size'.
    263264  ∀classify_assm: ASM_classify0 instruction = cl_other.
    264265  ∀pi1 : ℕ.
     
    271272      ∀final_status0:Status code_memory'.
    272273      ∀trace_ends_flag0:trace_ends_with_ret.
    273       ∀the_trace0:trace_any_label (ASM_abstract_status code_memory' cost_labels) trace_ends_flag0 start_status0 final_status0.
    274         trace_any_label_length code_memory' cost_labels trace_ends_flag0
    275           start_status0 final_status0 the_trace0 ≤ program_size' →
     274      ∀the_trace0:trace_any_label (ASM_abstract_status … cost_labels) trace_ends_flag0 start_status0 final_status0.
     275        trace_any_label_length … the_trace0 ≤ program_size' →
    276276        program_counter''' = program_counter … start_status0 →
    277277                  pi1
    278                     =compute_paid_trace_any_label code_memory' cost_labels
    279                      trace_ends_flag0 start_status0 final_status0 the_trace0
     278                    =compute_paid_trace_any_label … the_trace0
    280279    else (pi1=O) )
    281280   → ticks+pi1
    282      =compute_paid_trace_any_label code_memory' cost_labels trace_ends_flag
    283       start_status final_status the_trace.
     281     =compute_paid_trace_any_label … the_trace.
    284282  #code_memory' #program_counter' #cost_labels #program_size' #ticks #instruction
    285283  #program_counter'' #FETCH #start_status #final_status #trace_ends_flag #the_trace
     
    287285  #recursive_assm
    288286  @(trace_any_label_inv_ind … the_trace)
    289     [6:
     287    [2:
     288      #start_status' #final_status' #execute_assm #classifier_assm #trace_ends_assm
     289      #start_status_refl #final_status_refl #the_trace_assm destruct @⊥
     290    |3:
     291      #status_pre_fun_call #status_start_fun_call #status_final #execute_assm
     292      #classifier_assm #after_return_assm #trace_label_return #costed_assm
     293      #ends_flag_refl #start_status_refl #final_status_refl #the_trace_refl
     294      destruct @⊥
     295    |4: (* XXX *)
     296      cases daemon
     297    |5:
     298      #end_flag #status_pre_fun_call #status_start_fun_call #status_after_fun_call
     299      #status_final #execute_assm #classifier_assm #after_return_assm #trace_label_return
     300      #costed_assm #trace_any_label #trace_ends_flag_refl #start_status_refl
     301      #final_status_refl #the_trace_refl destruct @⊥
     302    |6:
    290303      #end_flag #status_pre #status_init #status_end #execute_assm #trace_any_label
    291304      #classifier_assm #costed_assm #trace_ends_refl #start_status_refl #final_status_refl
     
    340353      generalize in match (refl … (lookup_opt … (program_counter … (execute_1 … status_start)) cost_labels));
    341354      whd in match (as_label ??);
    342       generalize in match (lookup_opt … (program_counter … (execute_1 code_memory' status_start)) cost_labels)
     355      generalize in match (lookup_opt … (program_counter … (execute_1 status_start)) cost_labels)
    343356        in ⊢ (??%? → % → ?);
    344357      #lookup_assm cases lookup_assm
     
    350363        generalize in match recursive_assm;
    351364        cases classifier_assm
    352         [1:
     365        [2:
     366          -classifier_assm #classifier_assm
     367          lapply (execute_1_and_program_counter_after_other_in_lockstep … classifier_assm)
     368          <FETCH normalize nodelta #rewrite_assm >rewrite_assm in Some_lookup_opt_assm;
     369          #Some_lookup_opt_assm <Some_lookup_opt_assm
     370          normalize nodelta #new_recursive_assm >new_recursive_assm
     371          cut(ticks = \snd (fetch code_memory'
     372             (program_counter … status_start)))
     373          [1:
     374            <FETCH %
     375          |2:
     376            #ticks_refl_assm >ticks_refl_assm
     377            <plus_n_O %
     378          ]
     379        |1:
    353380          whd in ⊢ (% → ?);
    354381          whd in ⊢ (??%? → ?);
     
    364391          try(#addr normalize nodelta #ignore #absurd destruct(absurd))
    365392          normalize in ignore; destruct(ignore)
    366         |2:
    367           -classifier_assm #classifier_assm
    368           lapply (execute_1_and_program_counter_after_other_in_lockstep … classifier_assm)
    369           <FETCH normalize nodelta #rewrite_assm >rewrite_assm in Some_lookup_opt_assm;
    370           #Some_lookup_opt_assm <Some_lookup_opt_assm
    371           normalize nodelta #new_recursive_assm >new_recursive_assm
    372           cut(ticks = \snd (fetch code_memory'
    373              (program_counter … status_start)))
    374           [1:
    375             <FETCH %
    376           |2:
    377             #ticks_refl_assm >ticks_refl_assm
    378             <plus_n_O %
    379           ]
    380         ]
    381       ]
    382     |2:
    383       #start_status' #final_status' #execute_assm #classifier_assm #trace_ends_assm
    384       #start_status_refl #final_status_refl #the_trace_assm destruct @⊥
    385     |3:
    386       #status_pre_fun_call #status_start_fun_call #status_final #execute_assm
    387       #classifier_assm #after_return_assm #trace_label_return #costed_assm
    388       #ends_flag_refl #start_status_refl #final_status_refl #the_trace_refl
    389       destruct @⊥
    390     |4: (* XXX *)
    391       cases daemon
    392     |5:
    393       #end_flag #status_pre_fun_call #status_start_fun_call #status_after_fun_call
    394       #status_final #execute_assm #classifier_assm #after_return_assm #trace_label_return
    395       #costed_assm #trace_any_label #trace_ends_flag_refl #start_status_refl
    396       #final_status_refl #the_trace_refl destruct @⊥
    397     ]
     393          (* JHM: at this point previously, all the instruction-case-split-induced goals were discharged, but now... they are left outstanding? *)
     394          cases daemon (* XXX *)
    398395  (* NTactic error: unify
    399396     NCicUnification failure: Can't unify Or with eq
     
    407404  <FETCH in classifier_assm; >classify_assm #absurd destruct(absurd)
    408405  *)
    409   cases daemon
     406        ]
     407      ]
     408    ]
     409  change with (Some ? (ASM_classify0 ?) = ?) in classifier_assm;
     410  whd in match current_instruction in classifier_assm; normalize nodelta in classifier_assm;
     411  whd in match current_instruction0 in classifier_assm; normalize nodelta in classifier_assm;
     412  <FETCH in classifier_assm; >classify_assm #absurd destruct(absurd)
     413 
    410414qed.
    411415
     
    423427  ∀final_status: (Status code_memory').
    424428  ∀trace_ends_flag: trace_ends_with_ret.
    425   ∀the_trace: (trace_any_label (ASM_abstract_status code_memory' cost_labels) trace_ends_flag start_status final_status).
     429  ∀the_trace: (trace_any_label (ASM_abstract_status cost_labels) trace_ends_flag start_status final_status).
    426430  ∀program_counter_refl: (program_counter' = program_counter … start_status).
    427431  ∀classify_assm: ASM_classify0 instruction = cl_jump.
    428432    ticks
    429      =compute_paid_trace_any_label code_memory' cost_labels trace_ends_flag
    430       start_status final_status the_trace.
     433     =compute_paid_trace_any_label … the_trace.
    431434  #code_memory' #program_counter' #cost_labels #first_time_around
    432435  #program_size' #ticks #instruction #program_counter'' #FETCH
     
    479482  ∀final_status : (Status code_memory').
    480483  ∀trace_ends_flag : trace_ends_with_ret.
    481   ∀the_trace : (trace_any_label (ASM_abstract_status code_memory' cost_labels) trace_ends_flag start_status final_status).
     484  ∀the_trace : trace_any_label (ASM_abstract_status … cost_labels) trace_ends_flag start_status final_status.
    482485  ∀program_counter_refl : (program_counter' = program_counter … start_status).
    483   ∀size_invariant : trace_any_label_length code_memory' cost_labels trace_ends_flag start_status final_status the_trace ≤S program_size'.
     486  ∀size_invariant : trace_any_label_length the_trace ≤S program_size'.
    484487  ∀classify_assm: ASM_classify0 instruction = cl_call.
    485488  (∀pi1:ℕ
     
    490493              .∀trace_ends_flag0:trace_ends_with_ret
    491494               .∀the_trace0:trace_any_label
    492                                         (ASM_abstract_status code_memory' cost_labels)
     495                                        (ASM_abstract_status cost_labels)
    493496                                        trace_ends_flag0 start_status0 final_status0.
    494                 trace_any_label_length code_memory' cost_labels trace_ends_flag0
    495                   start_status0 final_status0 the_trace0
     497                trace_any_label_length … the_trace0
    496498                   ≤ program_size' →
    497499                program_counter''
    498500                 =program_counter … start_status0
    499501                 → pi1
    500                    =compute_paid_trace_any_label code_memory' cost_labels
    501                     trace_ends_flag0 start_status0 final_status0 the_trace0) 
     502                   =compute_paid_trace_any_label … the_trace0) 
    502503   else (pi1=O) 
    503504   → ticks+pi1
    504      =compute_paid_trace_any_label code_memory' cost_labels trace_ends_flag
    505       start_status final_status the_trace).
     505     =compute_paid_trace_any_label … the_trace).
    506506  #code_memory' #program_counter' #cost_labels #program_size'
    507507  #ticks #instruction #program_counter'' #FETCH
     
    618618  ∀final_status : (Status code_memory').
    619619  ∀trace_ends_flag : trace_ends_with_ret.
    620   ∀the_trace : (trace_any_label (ASM_abstract_status code_memory' cost_labels) trace_ends_flag start_status final_status).
     620  ∀the_trace : trace_any_label (ASM_abstract_status … cost_labels) trace_ends_flag start_status final_status.
    621621  ∀program_counter_refl : (program_counter' = program_counter … start_status).
    622622  ∀classify_assm: ASM_classify0 instruction = cl_return.
    623623    ticks
    624      =compute_paid_trace_any_label code_memory' cost_labels trace_ends_flag
    625       start_status final_status the_trace.
     624     =compute_paid_trace_any_label … the_trace.
    626625  #code_memory' #program_counter' #cost_labels #program_size'
    627626  #ticks #instruction #program_counter'' #FETCH
     
    677676  ∀start_status: Status code_memory.
    678677  ∀final_status: Status code_memory.
    679   ∀the_trace.
    680   trace_any_label_length code_memory cost_labels trace_ends_flag start_status
    681     final_status the_trace ≤ 0 → False.
     678  ∀the_trace: trace_any_label (ASM_abstract_status … cost_labels) trace_ends_flag start_status final_status.
     679   trace_any_label_length … the_trace ≤ 0 → False.
    682680  #code_memory #cost_labels #trace_ends_flag #start_status #final_status
    683681  #the_trace
     
    698696              trace_any_label_length … the_trace ≤ program_size →
    699697              program_counter' = program_counter … start_status →
    700                 cost_of_block = compute_paid_trace_any_label code_memory' cost_labels trace_ends_flag start_status final_status the_trace
     698                cost_of_block = compute_paid_trace_any_label the_trace
    701699          else
    702700            (cost_of_block = 0) ≝
     
    722720              trace_any_label_length … the_trace ≤ S program_size' →
    723721              program_counter' = program_counter … start_status →
    724                 cost_of_block = compute_paid_trace_any_label code_memory' cost_labels trace_ends_flag start_status final_status the_trace with
     722                cost_of_block = compute_paid_trace_any_label the_trace with
    725723          [ RET                    ⇒ λinstr. ticks
    726724          | RETI                   ⇒ λinstr. ticks
     
    766764              trace_any_label_length … the_trace ≤ S program_size' →
    767765              program_counter' = program_counter … start_status →
    768                 cost_of_block = compute_paid_trace_any_label code_memory' cost_labels trace_ends_flag start_status final_status the_trace
     766                cost_of_block = compute_paid_trace_any_label the_trace
    769767          | false ⇒
    770768            (cost_of_block = 0)
     
    828826        ∀unrepeating_witness: tal_unrepeating … the_trace.
    829827          program_counter' = program_counter … start_status →
    830             cost_of_block = compute_paid_trace_any_label code_memory' cost_labels trace_ends_flag start_status final_status the_trace ≝
     828            cost_of_block = compute_paid_trace_any_label the_trace ≝
    831829  λcode_memory: BitVectorTrie Byte 16.
    832830  λprogram_counter: Word.
Note: See TracChangeset for help on using the changeset viewer.