Changeset 2573 for src/ASM


Ignore:
Timestamp:
Jan 9, 2013, 6:15:31 PM (7 years ago)
Author:
mckinna
Message:

temporary fixes to ensure {compiler,correctness}.ma recompile
after paolo's recent (r2553) changes to StructuredTraces?.ma

a number of lemmas could be made a bit more abstract
I've been quite aggressive in use of ldots to suppress verbosity;
more should be possible

previous proofs now break, either

arising from missing cases or
renumbering of cases arising from the changes to trace_* constructors

arguably, much more refactoring would be helpful here
e.g. some dependencies simplified; but more possible

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/ASMCosts.ma

    r2531 r2573  
    22include "ASM/Arithmetic.ma".
    33include "ASM/Fetch.ma".
    4 include "ASM/Interpret.ma".
    5 include "common/StructuredTraces.ma".
    6 
    7 (* moved to Fetch.ma *)
    8 (* definition costlabel_map ≝ BitVectorTrie costlabel 16.   *)
     4include "ASM/Interpret.ma". (* includes ASM/AbstractStatus.ma *)
     5
     6(*include "common/StructuredTraces.ma". (* already included by ASM/AbstractStatus.ma *) *)
     7
     8(* should this definition be moved to ASM/AbstractStatus.ma ??? *)
    99
    1010definition ASM_abstract_status: ∀code_memory. BitVectorTrie costlabel 16 → abstract_status ≝
     
    1616      word_deqset
    1717      (program_counter …)
    18       (λs. ASM_classify … s)
     18      (λs. Some ? (ASM_classify … s))
    1919      (λpc.lookup_opt ?? pc cost_labels)
    2020      (next_instruction_properly_relates_program_counters code_memory)
    2121      ? (* (λs.False) *)
     22      ?
    2223      ?.
    23   cases daemon (* XXX: is final predicate, call ident function *)
    24 qed.
     24  cases daemon (* XXX: is_final predicate, (tail)call_ident function *)
     25qed.
     26
     27lemma Some_inv : ∀A.∀a,b. Some A a = Some A b → a = b.
     28  #A#a #b #eq destruct //
     29  qed.
    2530
    2631definition trace_any_label_length ≝
     
    118123include alias "arithmetics/nat.ma".
    119124
    120 lemma execute_1_and_program_counter_after_other_in_lockstep:
     125lemma execute_1_and_program_counter_after_other_in_lockstep00:
     126  ∀code_memory: BitVectorTrie Byte 16.
     127  ∀start_status: Status code_memory.
     128      let 〈instruction, pc, ticks〉 ≝ fetch code_memory (program_counter … start_status) in
     129    ASM_classify0 instruction = cl_other →
     130        program_counter ? ? (execute_1 … start_status) =
     131          program_counter_after_other pc instruction.
     132  #code_memory #start_status
     133  whd in match execute_1; normalize nodelta 
     134  cases (execute_1' code_memory start_status) #the_status; * #_
     135  cases (fetch ? ?); * #instruction #pc #ticks
     136  #classify_assm #classify_assm0 @classify_assm assumption
     137qed.
     138
     139lemma execute_1_and_program_counter_after_other_in_lockstep0:
    121140  ∀code_memory: BitVectorTrie Byte 16.
    122141  ∀start_status: Status code_memory.
     
    132151  #classify_assm #classify_assm' @classify_assm' assumption
    133152qed.
     153
     154lemma execute_1_and_program_counter_after_other_in_lockstep:
     155  ∀code_memory: BitVectorTrie Byte 16.
     156  ∀cost_labels: BitVectorTrie costlabel 16.
     157  ∀start_status: Status code_memory.
     158    as_classifier (ASM_abstract_status code_memory cost_labels) start_status cl_other →
     159      let 〈instruction, pc, ticks〉 ≝ fetch code_memory (program_counter … start_status) in
     160        program_counter ? ? (execute_1 … start_status) =
     161          program_counter_after_other pc instruction.
     162  #code_memory #cost_labels #start_status #classify_assm
     163  change with (Some ? (ASM_classify0 ?) = ?) in classify_assm;
     164  destruct (classify_assm)
     165  @execute_1_and_program_counter_after_other_in_lockstep0 assumption.
     166qed. 
    134167
    135168lemma nat_of_bitvector_lt_bound:
     
    195228      in
    196229        current_instruction_cost + tail_trace_cost
    197   ].
     230  | _ ⇒ ? (* XXX *)
     231  ].
     232  cases daemon
     233  qed.
    198234
    199235definition compute_paid_trace_label_label ≝
     
    223259  ∀trace_ends_flag : trace_ends_with_ret.
    224260  ∀the_trace : (trace_any_label (ASM_abstract_status code_memory' cost_labels) trace_ends_flag start_status final_status).
    225   ∀program_counter_refl : (program_counter' = program_counter (BitVectorTrie Byte 16) code_memory' start_status).
     261  ∀program_counter_refl : (program_counter' = program_counter start_status).
    226262  ∀size_invariant : trace_any_label_length code_memory' cost_labels trace_ends_flag start_status final_status the_trace ≤S program_size'.
    227263  ∀classify_assm: ASM_classify0 instruction = cl_other.
     
    238274        trace_any_label_length code_memory' cost_labels trace_ends_flag0
    239275          start_status0 final_status0 the_trace0 ≤ program_size' →
    240         program_counter''' = program_counter (BitVectorTrie Byte 16) code_memory' start_status0 →
     276        program_counter''' = program_counter start_status0 →
    241277                  pi1
    242278                    =compute_paid_trace_any_label code_memory' cost_labels
     
    251287  #recursive_assm
    252288  @(trace_any_label_inv_ind … the_trace)
    253     [5:
     289    [6:
    254290      #end_flag #status_pre #status_init #status_end #execute_assm #trace_any_label
    255291      #classifier_assm #costed_assm #trace_ends_refl #start_status_refl #final_status_refl
     
    268304        #None_lookup_opt_assm normalize nodelta #_
    269305        generalize in match recursive_assm;
    270         lapply (execute_1_and_program_counter_after_other_in_lockstep code_memory' ? classifier_assm)
     306        (*lapply (execute_1_and_program_counter_after_other_in_lockstep0 code_memory' ? (Some_inv … classifier_assm))*)
     307        lapply (execute_1_and_program_counter_after_other_in_lockstep … classifier_assm)
    271308        <FETCH normalize nodelta #rewrite_assm >rewrite_assm in None_lookup_opt_assm;
    272309        #None_lookup_opt_assm <None_lookup_opt_assm
     
    276313        whd in match (current_instruction_cost … status_pre);
    277314        cut(ticks = \snd (fetch code_memory'
    278            (program_counter (BitVectorTrie Byte 16) code_memory' status_pre)))
     315           (program_counter status_pre)))
    279316        [1,3:
    280317          <FETCH %
     
    329366        |2:
    330367          -classifier_assm #classifier_assm
    331           lapply (execute_1_and_program_counter_after_other_in_lockstep code_memory' ? classifier_assm)
     368          lapply (execute_1_and_program_counter_after_other_in_lockstep classifier_assm)
    332369          <FETCH normalize nodelta #rewrite_assm >rewrite_assm in Some_lookup_opt_assm;
    333370          #Some_lookup_opt_assm <Some_lookup_opt_assm
    334371          normalize nodelta #new_recursive_assm >new_recursive_assm
    335372          cut(ticks = \snd (fetch code_memory'
    336              (program_counter (BitVectorTrie Byte 16) code_memory' status_start)))
     373             (program_counter status_start)))
    337374          [1:
    338375            <FETCH %
     
    351388      #ends_flag_refl #start_status_refl #final_status_refl #the_trace_refl
    352389      destruct @⊥
    353     |4:
     390    |4: (* XXX *)
     391      cases daemon
     392    |5:
    354393      #end_flag #status_pre_fun_call #status_start_fun_call #status_after_fun_call
    355394      #status_final #execute_assm #classifier_assm #after_return_assm #trace_label_return
     
    357396      #final_status_refl #the_trace_refl destruct @⊥
    358397    ]
    359   change with (ASM_classify0 ? = ?) in classifier_assm;
     398  (* NTactic error: unify
     399     NCicUnification failure: Can't unify Or with eq
     400     in response to
     401     
     402  change with (Some ? (ASM_classify0 ?) = ? ∨ Some ? (ASM_classify0 ?) = ?) in classifier_assm;
     403
     404  (*change with (ASM_classify0 ? = ?) in classifier_assm;*)
    360405  whd in match current_instruction in classifier_assm; normalize nodelta in classifier_assm;
    361406  whd in match current_instruction0 in classifier_assm; normalize nodelta in classifier_assm;
    362407  <FETCH in classifier_assm; >classify_assm #absurd destruct(absurd)
     408  *)
     409  cases daemon
    363410qed.
    364411
     
    377424  ∀trace_ends_flag: trace_ends_with_ret.
    378425  ∀the_trace: (trace_any_label (ASM_abstract_status code_memory' cost_labels) trace_ends_flag start_status final_status).
    379   ∀program_counter_refl: (program_counter' = program_counter (BitVectorTrie Byte 16) code_memory' start_status).
     426  ∀program_counter_refl: (program_counter' = program_counter start_status).
    380427  ∀classify_assm: ASM_classify0 instruction = cl_jump.
    381428    ticks
     
    387434  #trace_ends_flag #the_trace #program_counter_refl #classify_assm
    388435  @(trace_any_label_inv_ind … the_trace)
    389   [5:
     436  [6:
    390437    #end_flag #status_pre #status_init #status_end #execute_assm #trace_any_label
    391438    #classifier_assm #costed_assm #trace_ends_refl #start_status_refl #final_status_refl
     
    406453    #ends_flag_refl #start_status_refl #final_status_refl #the_trace_refl
    407454    destruct @⊥
    408   |4:
     455  |4: (* XXX *)
     456    cases daemon
     457  |5:
    409458    #end_flag #status_pre_fun_call #status_start_fun_call #status_after_fun_call
    410459    #status_final #execute_assm #classifier_assm #after_return_assm #trace_label_return
     
    412461    #final_status_refl #the_trace_refl destruct @⊥
    413462  ]
    414   change with (ASM_classify0 ? = ?) in classifier_assm;
     463  change with (Some ? (ASM_classify0 ?) = ?) in classifier_assm;
    415464  whd in match current_instruction in classifier_assm; normalize nodelta in classifier_assm;
    416465  whd in match current_instruction0 in classifier_assm; normalize nodelta in classifier_assm;
     
    431480  ∀trace_ends_flag : trace_ends_with_ret.
    432481  ∀the_trace : (trace_any_label (ASM_abstract_status code_memory' cost_labels) trace_ends_flag start_status final_status).
    433   ∀program_counter_refl : (program_counter' = program_counter (BitVectorTrie Byte 16) code_memory' start_status).
     482  ∀program_counter_refl : (program_counter' = program_counter start_status).
    434483  ∀size_invariant : trace_any_label_length code_memory' cost_labels trace_ends_flag start_status final_status the_trace ≤S program_size'.
    435484  ∀classify_assm: ASM_classify0 instruction = cl_call.
     
    447496                   ≤ program_size' →
    448497                program_counter''
    449                  =program_counter (BitVectorTrie Byte 16) code_memory' start_status0
     498                 =program_counter start_status0
    450499                 → pi1
    451500                   =compute_paid_trace_any_label code_memory' cost_labels
     
    461510  #recursive_block_cost #recursive_assm
    462511  @(trace_any_label_inv_ind … the_trace)
    463   [5:
     512  [6:
    464513    #end_flag #status_pre #status_init #status_end #execute_assm #trace_any_label
    465514    #classifier_assm #costed_assm #trace_ends_refl #start_status_refl #final_status_refl
     
    492541      #costlabel #Some_lookup_opt normalize nodelta #ignore
    493542      generalize in match recursive_assm;
    494       cut(program_counter'' = (program_counter (BitVectorTrie Byte 16) code_memory' status_final))
     543      cut(program_counter'' = (program_counter status_final))
    495544      [1:
    496545        generalize in match after_return_assm;
     
    499548        #program_counter_assm >program_counter_assm <Some_lookup_opt
    500549        normalize nodelta #new_recursive_assm >new_recursive_assm
    501         cut(ticks = \snd (fetch code_memory' (program_counter (BitVectorTrie Byte 16) code_memory' status_pre_fun_call)))
     550        cut(ticks = \snd (fetch code_memory' (program_counter status_pre_fun_call)))
    502551        [1:
    503552          <FETCH %
     
    508557      ]
    509558    ]
    510   |4:
     559  |4: (* XXX *)
     560    cases daemon
     561  |5:
    511562    #end_flag #status_pre_fun_call #status_start_fun_call #status_after_fun_call
    512563    #status_final #execute_assm #classifier_assm #after_return_assm #trace_label_return
     
    547598    ]
    548599  ]
    549   try (change with (ASM_classify0 ? = ? ∨ ASM_classify0 ? = ?) in classifier_assm;)
    550   try (change with (ASM_classify0 ? = ?) in classifier_assm;)
     600  try (change with (Some ? (ASM_classify0 ?) = ? ∨ Some ? (ASM_classify0 ?) = ?) in classifier_assm;)
     601  try (change with (Some ? (ASM_classify0 ?) = ?) in classifier_assm;)
    551602  whd in match current_instruction in classifier_assm; normalize nodelta in classifier_assm;
    552603  whd in match current_instruction0 in classifier_assm; normalize nodelta in classifier_assm;
     
    568619  ∀trace_ends_flag : trace_ends_with_ret.
    569620  ∀the_trace : (trace_any_label (ASM_abstract_status code_memory' cost_labels) trace_ends_flag start_status final_status).
    570   ∀program_counter_refl : (program_counter' = program_counter (BitVectorTrie Byte 16) code_memory' start_status).
     621  ∀program_counter_refl : (program_counter' = program_counter start_status).
    571622  ∀classify_assm: ASM_classify0 instruction = cl_return.
    572623    ticks
     
    593644    #trace_ends_flag_refl #start_status_refl #final_status_refl #the_trace_refl
    594645    destruct @⊥
    595   |4:
     646  |4: (* XXX *)
     647    cases daemon
     648  |5:
    596649    #end_flag #status_pre_fun_call #status_start_fun_call #status_after_fun_call
    597650    #status_final #execute_assm #classifier_assm #after_return_assm #trace_label_return
     
    599652    #final_status_refl #the_trace_refl
    600653    destruct @⊥
    601   |5:
     654  |6:
    602655    #end_flag #status_pre #status_init #status_end #execute_assm #trace_any_label
    603656    #classifier_assm #costed_assm #trace_ends_flag_refl #start_status_refl
    604657    #final_status_refl #the_trace_refl destruct @⊥
    605658  ]
     659  try (change with (Some ? (ASM_classify0 ?) = ? ∨ Some ? (ASM_classify0 ?) = ?) in classifier_assm;)
     660  try (change with (Some ? (ASM_classify0 ?) = ?) in classifier_assm;)
     661  (*
    606662  try (change with (ASM_classify0 ? = ? ∨ ASM_classify0 ? = ?) in classifier_assm;)
    607663  try (change with (ASM_classify0 ? = ?) in classifier_assm;)
     664  *)
    608665  whd in match current_instruction in classifier_assm; normalize nodelta in classifier_assm;
    609666  whd in match current_instruction0 in classifier_assm; normalize nodelta in classifier_assm;
     
    769826        ∀trace_ends_flag.
    770827        ∀the_trace: trace_any_label (ASM_abstract_status … cost_labels) trace_ends_flag start_status final_status.
    771         ∀unrepeating_witness: tal_unrepeating (ASM_abstract_status code_memory' cost_labels) trace_ends_flag start_status final_status the_trace.
     828        ∀unrepeating_witness: tal_unrepeating the_trace.
    772829          program_counter' = program_counter … start_status →
    773830            cost_of_block = compute_paid_trace_any_label code_memory' cost_labels trace_ends_flag start_status final_status the_trace ≝
Note: See TracChangeset for help on using the changeset viewer.