Changeset 2899 for src/ASM/ASMCosts.ma


Ignore:
Timestamp:
Mar 19, 2013, 12:33:13 AM (7 years ago)
Author:
sacerdot
Message:
  1. some renaming ASM_xxx to OC_xxx
  2. ASM_pre_classified_system implemented (up to the same missing cases as OC_pre_classified_system) Note: the invariant that the pc is always in the program cannot be maintained in case of function pointer calls and returns. To be dropped.
File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/ASMCosts.ma

    r2832 r2899  
    99(*include "common/StructuredTraces.ma". (* included by ASM/AbstractStatus.ma *) *)
    1010
    11 definition ASM_abstract_status: ∀code_memory. BitVectorTrie costlabel 16 → abstract_status ≝
     11definition OC_abstract_status: ∀code_memory. BitVectorTrie costlabel 16 → abstract_status ≝
    1212  λcode_memory.
    1313  λcost_labels.
     
    1717      word_deqset
    1818      (program_counter …)
    19       (ASM_classify …)
     19      (OC_classify …)
    2020      (λpc.lookup_opt … pc cost_labels)
    2121      (next_instruction_properly_relates_program_counters code_memory)
     
    3232  λstart_status: Status code_memory.
    3333  λfinal_status: Status code_memory.
    34   λthe_trace: trace_any_label (ASM_abstract_status … cost_labels) trace_ends_flag start_status final_status.
     34  λthe_trace: trace_any_label (OC_abstract_status … cost_labels) trace_ends_flag start_status final_status.
    3535    as_trace_any_label_length' … the_trace.
    3636
     
    137137  ∀code_memory: BitVectorTrie Byte 16.
    138138  ∀start_status: Status code_memory.
    139     ASM_classify … start_status = cl_other →
     139    OC_classify … start_status = cl_other →
    140140      let 〈instruction, pc, ticks〉 ≝ fetch code_memory (program_counter … start_status) in
    141141        program_counter ? ? (execute_1 … start_status) =
     
    153153  ∀cost_labels: BitVectorTrie costlabel 16.
    154154  ∀start_status: Status code_memory.
    155     as_classifier (ASM_abstract_status code_memory cost_labels) start_status cl_other →
     155    as_classifier (OC_abstract_status code_memory cost_labels) start_status cl_other →
    156156      let 〈instruction, pc, ticks〉 ≝ fetch code_memory (program_counter … start_status) in
    157157        program_counter ? ? (execute_1 … start_status) =
     
    168168  ∀start, final: Status code_memory.
    169169  ∀trace_ends_flag.
    170   ∀the_trace: trace_any_label (ASM_abstract_status … cost_labels) trace_ends_flag start final.
     170  ∀the_trace: trace_any_label (OC_abstract_status … cost_labels) trace_ends_flag start final.
    171171    sublist ? (tal_pc_list … the_trace) (all_program_counter_list (2^16)).
    172172  #code_memory #cost_labels #start #final #trace_ends_flag #the_trace
     
    181181  ∀start, final: Status code_memory.
    182182  ∀trace_ends_flag.
    183   ∀the_trace: trace_any_label (ASM_abstract_status … cost_labels) trace_ends_flag start final.
     183  ∀the_trace: trace_any_label (OC_abstract_status … cost_labels) trace_ends_flag start final.
    184184  ∀unrepeating_witness: tal_unrepeating … the_trace.
    185185    |tal_pc_list … the_trace| ≤ 2^16.
     
    200200    (trace_ends_flag: trace_ends_with_ret) (start_status: Status code_memory)
    201201      (final_status: Status code_memory)
    202         (the_trace: trace_any_label (ASM_abstract_status … cost_labels) trace_ends_flag start_status final_status)
     202        (the_trace: trace_any_label (OC_abstract_status … cost_labels) trace_ends_flag start_status final_status)
    203203       on the_trace: nat ≝
    204204  match the_trace with
     
    227227  λstart_status: Status code_memory.
    228228  λfinal_status: Status code_memory.
    229   λthe_trace: (trace_label_label (ASM_abstract_status … cost_labels) trace_ends_flag start_status final_status).
     229  λthe_trace: (trace_label_label (OC_abstract_status … cost_labels) trace_ends_flag start_status final_status).
    230230  match the_trace with
    231231  [ tll_base ends_flag initial final given_trace labelled_proof ⇒
     
    246246  ∀final_status : (Status code_memory').
    247247  ∀trace_ends_flag : trace_ends_with_ret.
    248   ∀the_trace : (trace_any_label (ASM_abstract_status … cost_labels) trace_ends_flag start_status final_status).
     248  ∀the_trace : (trace_any_label (OC_abstract_status … cost_labels) trace_ends_flag start_status final_status).
    249249  ∀program_counter_refl : (program_counter' = program_counter … start_status).
    250250  ∀size_invariant : trace_any_label_length … the_trace ≤S program_size'.
     
    259259      ∀final_status0:Status code_memory'.
    260260      ∀trace_ends_flag0:trace_ends_with_ret.
    261       ∀the_trace0:trace_any_label (ASM_abstract_status … cost_labels) trace_ends_flag0 start_status0 final_status0.
     261      ∀the_trace0:trace_any_label (OC_abstract_status … cost_labels) trace_ends_flag0 start_status0 final_status0.
    262262        trace_any_label_length … the_trace0 ≤ program_size' →
    263263        program_counter''' = program_counter … start_status0 →
     
    366366          ]
    367367        |1:
    368                 (* JHM: wicked failure because Some prevent previous unfolding of ASM_classify here *)
     368                (* JHM: wicked failure because Some prevent previous unfolding of OC_classify here *)
    369369                @⊥
    370370                (* *** (* previously: unnecessary case analysis on instruction *)
     
    404404  ∀final_status: (Status code_memory').
    405405  ∀trace_ends_flag: trace_ends_with_ret.
    406   ∀the_trace: (trace_any_label (ASM_abstract_status … cost_labels) trace_ends_flag start_status final_status).
     406  ∀the_trace: (trace_any_label (OC_abstract_status … cost_labels) trace_ends_flag start_status final_status).
    407407  ∀program_counter_refl: (program_counter' = program_counter … start_status).
    408408  ∀classify_assm: ASM_classify0 instruction = cl_jump.
     
    462462  ∀final_status : (Status code_memory').
    463463  ∀trace_ends_flag : trace_ends_with_ret.
    464   ∀the_trace : trace_any_label (ASM_abstract_status … cost_labels) trace_ends_flag start_status final_status.
     464  ∀the_trace : trace_any_label (OC_abstract_status … cost_labels) trace_ends_flag start_status final_status.
    465465  ∀program_counter_refl : (program_counter' = program_counter … start_status).
    466466  ∀size_invariant : trace_any_label_length … the_trace ≤S program_size'.
     
    473473              .∀trace_ends_flag0:trace_ends_with_ret
    474474               .∀the_trace0:trace_any_label
    475                                         (ASM_abstract_status … cost_labels)
     475                                        (OC_abstract_status … cost_labels)
    476476                                        trace_ends_flag0 start_status0 final_status0.
    477477                trace_any_label_length … the_trace0
     
    601601  ∀final_status : (Status code_memory').
    602602  ∀trace_ends_flag : trace_ends_with_ret.
    603   ∀the_trace : trace_any_label (ASM_abstract_status … cost_labels) trace_ends_flag start_status final_status.
     603  ∀the_trace : trace_any_label (OC_abstract_status … cost_labels) trace_ends_flag start_status final_status.
    604604  ∀program_counter_refl : (program_counter' = program_counter … start_status).
    605605  ∀classify_assm: ASM_classify0 instruction = cl_return.
     
    663663  ∀start_status: Status code_memory.
    664664  ∀final_status: Status code_memory.
    665   ∀the_trace: trace_any_label (ASM_abstract_status … cost_labels) trace_ends_flag start_status final_status.
     665  ∀the_trace: trace_any_label (OC_abstract_status … cost_labels) trace_ends_flag start_status final_status.
    666666   trace_any_label_length … the_trace ≤ 0 → False.
    667667  #code_memory #cost_labels #trace_ends_flag #start_status #final_status
     
    680680            ∀final_status: Status code_memory'.
    681681            ∀trace_ends_flag.
    682             ∀the_trace: trace_any_label (ASM_abstract_status … cost_labels) trace_ends_flag start_status final_status.
     682            ∀the_trace: trace_any_label (OC_abstract_status … cost_labels) trace_ends_flag start_status final_status.
    683683              trace_any_label_length … the_trace ≤ program_size →
    684684              program_counter' = program_counter … start_status →
     
    704704            ∀final_status: Status code_memory'.
    705705            ∀trace_ends_flag.
    706             ∀the_trace: trace_any_label (ASM_abstract_status code_memory' cost_labels) trace_ends_flag start_status final_status.
     706            ∀the_trace: trace_any_label (OC_abstract_status code_memory' cost_labels) trace_ends_flag start_status final_status.
    707707              trace_any_label_length … the_trace ≤ S program_size' →
    708708              program_counter' = program_counter … start_status →
     
    748748            ∀final_status: Status code_memory'.
    749749            ∀trace_ends_flag.
    750             ∀the_trace: trace_any_label (ASM_abstract_status … cost_labels) trace_ends_flag start_status final_status.
     750            ∀the_trace: trace_any_label (OC_abstract_status … cost_labels) trace_ends_flag start_status final_status.
    751751              trace_any_label_length … the_trace ≤ S program_size' →
    752752              program_counter' = program_counter … start_status →
     
    811811        ∀final_status: Status code_memory'.
    812812        ∀trace_ends_flag.
    813         ∀the_trace: trace_any_label (ASM_abstract_status … cost_labels) trace_ends_flag start_status final_status.
     813        ∀the_trace: trace_any_label (OC_abstract_status … cost_labels) trace_ends_flag start_status final_status.
    814814        ∀unrepeating_witness: tal_unrepeating … the_trace.
    815815          program_counter' = program_counter … start_status →
Note: See TracChangeset for help on using the changeset viewer.