Changeset 1587 for src/ASM/ASMCosts.ma


Ignore:
Timestamp:
Dec 5, 2011, 5:16:55 PM (8 years ago)
Author:
mulligan
Message:

changes from today, including removing indexing of problematic function in utilities/binary/positive.ma

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/ASMCosts.ma

    r1560 r1587  
    9292qed.
    9393
     94axiom 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 *)
     100axiom 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))).
     105 
     106axiom minus_m_n_le_minus_m_So_to_Sm_minus_n_le_minus_m_o:
     107  ∀m, n, o: nat.
     108    m - n ≤ m - S o → S m - n ≤ m - o.
     109
     110axiom strengthened_invariant:
     111  ∀code_memory: BitVectorTrie Byte 16.
     112  ∀program_size: nat.
     113  ∀code_memory_size: nat.
     114  ∀new_program_counter: Word.
     115  ∀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
     119        Or (ASM_classify0 end_instr = cl_jump) (ASM_classify0 end_instr = cl_return) →
     120          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.
     123       
     124(* XXX: use memoisation here in the future *)
    94125let rec block_cost
    95   (mem: BitVectorTrie Byte 16) (cost_labels: BitVectorTrie costlabel 16)
    96     (pc: Word) (program_size: nat) on program_size : nat ≝
    97   match program_size with
    98   [ O ⇒ 0
    99   | S program_size ⇒
    100     let 〈instr,newpc,ticks〉 ≝ fetch … mem pc in
    101     match lookup_opt … newpc cost_labels with
    102      [ None ⇒
    103         match ASM_classify0 instr with
    104          [ cl_jump ⇒ ticks
    105          | cl_call ⇒ ticks + block_cost mem cost_labels newpc program_size
    106          | cl_return ⇒ ticks
    107          | cl_other ⇒ ticks + block_cost mem cost_labels newpc program_size
    108          ]
    109      | Some _ ⇒ ticks ]].
     126  (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)
     130          (final_instr_invariant:
     131            let instr ≝ \fst (\fst (fetch … code_memory (bitvector_of_nat … initial_program_size))) in
     132              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
     135  [ O ⇒ λabsurd. ⊥
     136  | 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
     140    match lookup_opt … newpc cost_labels return λx: option costlabel. nat with
     141    [ None ⇒
     142        let classify ≝ ASM_classify0 instr in
     143        match classify return λx. ∀classify_refl: x = classify. nat with
     144        [ 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 ?)
     146        | 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 ?)
     148        ] (refl … classify)
     149    | Some _ ⇒ ticks
     150    ]
     151  ].
     152  [1:
     153    cases(lt_to_not_zero … absurd)
     154  |2,4:
     155    cut(nat_of_bitvector … pc < nat_of_bitvector … newpc)
     156    [1,3:
     157      @fetch_pc_lt_new_pc
     158      lapply(transitive_lt
     159        (nat_of_bitvector 16 pc)
     160        initial_program_size
     161        (size Byte 16 mem) ? ?)
     162      [1,2,4,5:
     163        assumption
     164      |3,6:
     165        #assm assumption
     166      ]
     167    |2,4:
     168      change with (
     169        S (nat_of_bitvector … 16 pc) ≤ nat_of_bitvector … newpc
     170      ) in ⊢ (% → ?);
     171      #first_le_assm
     172      normalize in recursive_case;
     173      change with (
     174        S (initial_program_size - nat_of_bitvector … newpc) ≤ program_size)
     175      lapply (le_S_S_to_le … recursive_case)
     176      change with (
     177        initial_program_size - (nat_of_bitvector … pc) ≤ program_size
     178      ) in ⊢ (% → ?);
     179      #second_le_assm
     180      @(transitive_le
     181        (S (initial_program_size-nat_of_bitvector 16 newpc))
     182        (initial_program_size-nat_of_bitvector_aux 16 O pc)
     183        program_size ? second_le_assm)
     184      change with (
     185        initial_program_size - nat_of_bitvector … pc
     186      ) in ⊢ (??%);
     187      lapply (minus_Sn_m (nat_of_bitvector … newpc) initial_program_size)
     188      #assm <assm in ⊢ (?%?);
     189      [1,3:
     190        @minus_m_n_le_minus_m_So_to_Sm_minus_n_le_minus_m_o
     191        @monotonic_le_minus_r
     192        assumption
     193      |2,4:
     194        @(strengthened_invariant mem initial_program_size newpc pc size_invariant final_instr_invariant)
     195        [1,3:
     196          %
     197        |2,4:
     198          assumption
     199        ]
     200      ]
     201    ]
     202  |3,5:
     203  ]
     204qed.
    110205
    111206let rec traverse_code_internal
     
    135230  λcost_labels: BitVectorTrie costlabel 16.
    136231  λhas_main: bool.
    137   let program_size ≝ |program| in
     232  let program_size ≝ |program| + 1 in
    138233  let memory ≝ load_code_memory program in
    139234   traverse_code program memory cost_labels program_size.
Note: See TracChangeset for help on using the changeset viewer.