Changeset 1587


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

Location:
src
Files:
4 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.
  • src/ASM/CostsProof.ma

    r1581 r1587  
    1 
    21include "ASM/ASMCosts.ma".
    32include "ASM/WellLabeled.ma".
    43include "ASM/Status.ma".
    54include "common/StructuredTraces.ma".
    6 
    7 (*
    8 definition next_instruction_is_labelled ≝
    9   λcost_labels: BitVectorTrie Byte 16.
    10   λs: Status.
    11   let pc ≝ program_counter … (execute_1 s) in
    12     match lookup_opt … pc cost_labels with
    13     [ None ⇒ False
    14     | _    ⇒ True
    15     ].
    16 
    17 definition current_instruction_cost ≝
    18   λs: Status. \snd (fetch (code_memory … s) (program_counter … s)).
    19 
    20 definition is_call_p ≝
    21   λs.
    22   match s with
    23   [ ACALL _ ⇒ True
    24   | LCALL _ ⇒ True
    25   | JMP ⇒ True (* XXX: is function pointer call *)
    26   | _ ⇒ False
    27   ].
    28 
    29 definition next_instruction ≝
    30   λs: Status.
    31   let 〈instruction, ignore, ignore〉 ≝ fetch (code_memory … s) (program_counter … s) in
    32     instruction.
    33 
    34 inductive trace_ends_with_ret: Type[0] ≝
    35   | ends_with_ret: trace_ends_with_ret
    36   | doesnt_end_with_ret: trace_ends_with_ret.
    37 
    38 definition next_instruction_is_labelled ≝
    39   λcost_labels: BitVectorTrie Byte 16.
    40   λs: Status.
    41   let pc ≝ program_counter … (execute 1 s) in
    42     match lookup_opt … pc cost_labels with
    43     [ None ⇒ False
    44     | _    ⇒ True
    45     ].
    46 
    47 definition next_instruction_properly_relates_program_counters ≝
    48   λbefore: Status.
    49   λafter : Status.
    50   let size ≝ current_instruction_cost before in
    51   let pc_before ≝ program_counter … before in
    52   let pc_after ≝ program_counter … after in
    53   let sum ≝ \snd (half_add … pc_before (bitvector_of_nat … size)) in
    54     sum = pc_after.
    55 
    56 definition current_instruction ≝
    57   λs: Status.
    58   let pc ≝ program_counter … s in
    59   \fst (\fst (fetch … (code_memory … s) pc)).
    60 
    61 definition current_instruction_is_labelled ≝
    62   λcost_labels: BitVectorTrie Byte 16.
    63   λs: Status.
    64   let pc ≝ program_counter … s in
    65     match lookup_opt … pc cost_labels with
    66     [ None ⇒ False
    67     | _    ⇒ True
    68     ].
    69 
    70 inductive trace_label_return (cost_labels: BitVectorTrie Byte 16): Status → Status → Type[0] ≝
    71   | tlr_base:
    72       ∀status_before: Status.
    73       ∀status_after: Status.
    74         trace_label_label cost_labels ends_with_ret status_before status_after →
    75         trace_label_return cost_labels status_before status_after
    76   | tlr_step:
    77       ∀status_initial: Status.
    78       ∀status_labelled: Status.
    79       ∀status_final: Status.
    80           trace_label_label cost_labels doesnt_end_with_ret status_initial status_labelled →
    81             trace_label_return cost_labels status_labelled status_final →
    82               trace_label_return cost_labels status_initial status_final
    83 with trace_label_label: trace_ends_with_ret → Status → Status → Type[0] ≝
    84   | tll_base:
    85       ∀ends_flag: trace_ends_with_ret.
    86       ∀start_status: Status.
    87       ∀end_status: Status.
    88         trace_label_label_pre cost_labels ends_flag start_status end_status →
    89         current_instruction_is_labelled cost_labels start_status →
    90         trace_label_label cost_labels ends_flag start_status end_status
    91 with trace_label_label_pre: trace_ends_with_ret → Status → Status → Type[0] ≝
    92   | tllp_base_not_return:
    93       ∀start_status: Status.
    94         let final_status ≝ execute 1 start_status in
    95         current_instruction start_status ≠ (RealInstruction … (RET [[relative]])) →
    96         ¬ (is_jump_p (current_instruction start_status)) →
    97         current_instruction_is_labelled cost_labels final_status →
    98           trace_label_label_pre cost_labels doesnt_end_with_ret start_status final_status
    99   | tllp_base_return:
    100       ∀start_status: Status.
    101         let final_status ≝ execute 1 start_status in
    102           current_instruction start_status = (RealInstruction … (RET [[relative]])) →
    103             trace_label_label_pre cost_labels ends_with_ret start_status final_status
    104   | tllp_base_jump:
    105       ∀start_status: Status.
    106         let final_status ≝ execute 1 start_status in
    107           is_jump_p (current_instruction start_status) →
    108             current_instruction_is_labelled cost_labels final_status →
    109               trace_label_label_pre cost_labels doesnt_end_with_ret start_status final_status
    110   | tllp_step_call:
    111       ∀end_flag: trace_ends_with_ret.
    112       ∀status_pre_fun_call: Status.
    113       ∀status_after_fun_call: Status.
    114       ∀status_final: Status.
    115         let status_start_fun_call ≝ execute 1 status_pre_fun_call in
    116           is_call_p (current_instruction status_pre_fun_call) →
    117           next_instruction_properly_relates_program_counters status_pre_fun_call status_after_fun_call →
    118           trace_label_return cost_labels status_start_fun_call status_after_fun_call →
    119           trace_label_label_pre cost_labels end_flag status_after_fun_call status_final →
    120             trace_label_label_pre cost_labels end_flag status_pre_fun_call status_final
    121   | tllp_step_default:
    122       ∀end_flag: trace_ends_with_ret.
    123       ∀status_pre: Status.
    124       ∀status_end: Status.
    125         let status_init ≝ execute 1 status_pre in
    126           trace_label_label_pre cost_labels end_flag status_init status_end →
    127           ¬ (is_call_p (current_instruction status_pre)) →
    128           ¬ (is_jump_p (current_instruction status_pre)) →
    129           (current_instruction status_pre) ≠ (RealInstruction … (RET [[relative]])) →
    130           ¬ (current_instruction_is_labelled cost_labels status_init) →
    131             trace_label_label_pre cost_labels end_flag status_pre status_end.
    132 *)
    133 
    134 (* XXX: not us
    135 definition compute_simple_path0 (s:Status) (is_labelled s) (well_balanced s) (labelled_p p): trace_lab_ret ≝ ….
    136 
    137 lemma simple_path_ok:
    138  ∀st: Status.∀H.
    139  let p ≝ compute_simple_path0 st H in
    140    ∀n.
    141     nth_path n p = execute n st ∧
    142      (execute' (path_length p) st = 〈st',τ〉 →
    143       τ = cost_trace p)
    144   ].
    145 *)
    1465
    1476let rec compute_max_trace_label_label_cost
     
    23089 /3 by lt_plus_to_minus_r, plus_minus/
    23190qed.
    232 *)
    23391
    23492lemma plus_minus_rearrangement_1:
     
    266124  #m #n #o /2 by /
    267125qed.
     126*)
    268127
    269128let rec compute_max_trace_label_label_cost_is_ok
     
    737596  i < |l1| →
    738597   tech_cost_of_label cost_labels cost_map codom_dom l2 i =
    739    tech_cost_of_label cost_labels cost_map codom_dom (l1@l2) (i+|l1|).
     598   tech_cost_of_label cost_labels cost_mnth_safe ? i ctrace H) ?ap codom_dom (l1@l2) (i+|l1|).
    740599 #cost_labels #cost_Map #codom_dom #l1 #l2 #i #H
    741600 cut (ltb i (|l2|) = ltb (i+|l1|) (|l1@l2|))
     
    794653  ]
    795654]
    796 
     655(*
    797656lemma
    798657 compute_max_trace_any_label_cost cost_label trace_ends_flag start_status
     
    873732 let p ≝ compute_simple_path0 s in
    874733  execute' (path_length p) s = 〈s',τ〉 →
    875    Timer s' - Timer s = ∑ τ cost_map.
     734   Timer s' - Timer s = ∑ τ cost_map. *)
  • src/ASM/Interpret.ma

    r1582 r1587  
    638638                 let s ≝ add_ticks2 s in
    639639                  s
    640         ]. (*15s*)
     640        ]. (*15s*) (*
    641641    try (cases(other))
    642642    try assumption (*20s*)
     
    659659    try (normalize nodelta >set_arg_1_ignores_clock >clock_set_clock %)
    660660    try (normalize nodelta >clock_set_clock >set_arg_16_ignores_clock >clock_set_clock %)
    661     try (normalize nodelta >set_arg_16_ignores_clock >clock_set_clock %)
     661    try (normalize nodelta >set_arg_16_ignores_clock >clock_set_clock %) *) (* XXX: for convenience *)
    662662    cases daemon
    663 qed.
    664 
    665 lemma write_at_stack_pointer_ignores_clock:
    666   ∀M.∀s: PreStatus M.
    667   ∀sp: Byte.
    668     clock … (write_at_stack_pointer … s sp) = clock … s.
    669   #M #s #sp
    670   change with (let 〈nu, nl〉 ≝ split bool 4 4 (get_8051_sfr … s SFR_SP) in ?)
    671    in match (write_at_stack_pointer ???);
    672   normalize nodelta
    673   cases(split bool 4 4 (get_8051_sfr … s SFR_SP))
    674   #nu #nl normalize nodelta;
    675   cases(get_index_v bool 4 nu O (le_S_S O 3 (le_O_n 3)))
    676   normalize nodelta; %
    677663qed.
    678664
  • src/utilities/binary/positive.ma

    r1528 r1587  
    852852
    853853theorem nat_succ_pos: ∀n. nat_of_pos (succ_pos_of_nat n) = S n.
    854 #n elim n; //; qed.
     854#n elim n; //; qed-.
    855855
    856856theorem minus_plus_m_m: ∀n,m:Pos.n = (n+m)-m.
Note: See TracChangeset for help on using the changeset viewer.