Changeset 1591 for src/ASM/ASMCosts.ma


Ignore:
Timestamp:
Dec 6, 2011, 5:24:45 PM (8 years ago)
Author:
mulligan
Message:

work from today

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/ASMCosts.ma

    r1587 r1591  
    7272  mk_abstract_status
    7373   Status
    74    (λs,s'. eject … (execute_1 s) = s')
     74   (λs,s'. (execute_1 s) = s')
    7575   (λs,class. ASM_classify s = class)
    7676   (current_instruction_is_labelled cost_labels)
     
    9191  //
    9292qed.
    93 
    94 axiom size:
    95   ∀a: Type[0].
    96   ∀n: nat.
    97     BitVectorTrie Byte 16 → nat.
    98 
    99 (* XXX: need some precondition about pc not being too "big" to avoid overflow *)
    100 axiom fetch_pc_lt_new_pc:
    101   ∀mem: BitVectorTrie Byte 16.
    102   ∀pc: Word.
    103   ∀proof: nat_of_bitvector … pc < size Byte 16 mem.
    104     nat_of_bitvector … pc < nat_of_bitvector … (\snd (\fst (fetch … mem pc))).
    10593 
    10694axiom minus_m_n_le_minus_m_So_to_Sm_minus_n_le_minus_m_o:
     
    10896    m - n ≤ m - S o → S m - n ≤ m - o.
    10997
    110 axiom strengthened_invariant:
     98lemma strengthened_invariant:
    11199  ∀code_memory: BitVectorTrie Byte 16.
    112   ∀program_size: nat.
    113   ∀code_memory_size: nat.
     100  ∀total_program_size: nat.
    114101  ∀new_program_counter: Word.
    115102  ∀program_counter: Word.
    116     code_memory_size ≤ size Byte 16 code_memory →
    117     program_size < code_memory_size →
    118       let end_instr ≝ \fst (\fst (fetch … code_memory (bitvector_of_nat … program_size))) in
     103    total_program_size ≤ code_memory_size →
     104      let end_instr ≝ \fst (\fst (fetch … code_memory (bitvector_of_nat … total_program_size))) in
    119105        Or (ASM_classify0 end_instr = cl_jump) (ASM_classify0 end_instr = cl_return) →
    120106          new_program_counter = \snd (\fst (fetch … code_memory program_counter)) →
    121             nat_of_bitvector … program_counter < program_size →
    122               nat_of_bitvector … new_program_counter < program_size.
     107            nat_of_bitvector … program_counter ≤ total_program_size →
     108              nat_of_bitvector … new_program_counter ≤ total_program_size.
     109  #code_memory #total_program_size #new_program_counter #program_counter
     110  #relation_total_program_code_memory_size #end_instruction_is_ok
     111  #new_program_counter_from_fetch #program_counter_within_program
     112  >new_program_counter_from_fetch
     113  lapply (sig2 ? ? (fetch code_memory program_counter)) #assm
     114   
    123115       
    124116(* XXX: use memoisation here in the future *)
    125117let rec block_cost
    126118  (code_memory: BitVectorTrie Byte 16) (cost_labels: BitVectorTrie costlabel 16)
    127     (program_counter: Word) (program_size: nat) (code_memory_size: nat)
    128       (size_invariant: code_memory_size ≤ size Byte 16 code_memory)
    129         (pc_invariant: nat_of_bitvector … program_counter < code_memory_size)
     119    (program_counter: Word) (program_size: nat) (total_program_size: nat)
     120      (size_invariant: total_program_size ≤ code_memory_size)
     121        (pc_invariant: nat_of_bitvector … program_counter < total_program_size)
    130122          (final_instr_invariant:
    131             let instr ≝ \fst (\fst (fetch … code_memory (bitvector_of_nat … initial_program_size))) in
     123            let instr ≝ \fst (\fst (fetch … code_memory (bitvector_of_nat … total_program_size))) in
    132124              Or (ASM_classify0 instr = cl_jump) (ASM_classify0 instr = cl_return))
    133                 on program_size: initial_program_size - nat_of_bitvector … program_counter < program_size → nat ≝
    134   match program_size return λprogram_size: nat. initial_program_size - nat_of_bitvector … program_counter < program_size → nat with
     125                on program_size: total_program_size - nat_of_bitvector … program_counter < program_size → nat ≝
     126  match program_size return λprogram_size: nat. total_program_size - nat_of_bitvector … program_counter < program_size → nat with
    135127  [ O ⇒ λabsurd. ⊥
    136128  | S program_size ⇒ λrecursive_case.
    137     let ticks ≝ \snd (fetch … code_memory pc) in
    138     let instr ≝ \fst (\fst (fetch … mem pc)) in
    139     let newpc ≝ \snd (\fst (fetch … mem pc)) in
     129    let ticks ≝ \snd (fetch … code_memory program_counter) in
     130    let instr ≝ \fst (\fst (fetch … code_memory program_counter)) in
     131    let newpc ≝ \snd (\fst (fetch … code_memory program_counter)) in
    140132    match lookup_opt … newpc cost_labels return λx: option costlabel. nat with
    141133    [ None ⇒
     
    143135        match classify return λx. ∀classify_refl: x = classify. nat with
    144136        [ cl_jump ⇒ λclassify_refl. ticks
    145         | cl_call ⇒ λclassify_refl. ticks + (block_cost mem cost_labels newpc program_size initial_program_size size_invariant ? final_instr_invariant ?)
     137        | cl_call ⇒ λclassify_refl. ticks + (block_cost code_memory cost_labels newpc program_size total_program_size size_invariant ? final_instr_invariant ?)
    146138        | cl_return ⇒ λclassify_refl. ticks
    147         | cl_other ⇒ λclassify_refl. ticks + (block_cost mem cost_labels newpc program_size initial_program_size size_invariant ? final_instr_invariant ?)
     139        | cl_other ⇒ λclassify_refl. ticks + (block_cost code_memory cost_labels newpc program_size total_program_size size_invariant ? final_instr_invariant ?)
    148140        ] (refl … classify)
    149141    | Some _ ⇒ ticks
     
    153145    cases(lt_to_not_zero … absurd)
    154146  |2,4:
    155     cut(nat_of_bitvector … pc < nat_of_bitvector … newpc)
     147    cut(nat_of_bitvector … program_counter < nat_of_bitvector … newpc)
    156148    [1,3:
    157       @fetch_pc_lt_new_pc
     149      @fetch_pc_lt_new_pc (* XXX: now @sig2 from fetch's russell type *)
    158150      lapply(transitive_lt
    159151        (nat_of_bitvector 16 pc)
Note: See TracChangeset for help on using the changeset viewer.