Changeset 1500 for src/ASM/CostsProof.ma


Ignore:
Timestamp:
Nov 8, 2011, 1:34:22 PM (8 years ago)
Author:
sacerdot
Message:

Proof sketch for one of the two main proofs.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/CostsProof.ma

    r1499 r1500  
    33include "ASM/Status.ma".
    44
     5inductive trace_lab_ret: Type[0] ≝
     6   sing: ∀p. trace_lab_lab true p → structured_trace
     7 | cons:
     8    ∀p. trace_lab_lab false p → ∀tr:trace_lab_ret.
     9     execute 1 (last p) = hd tr →
     10      structured_trace
     11
     12with trace_lab_lab0: bool → Type[0] ≝ (* true = ends with ret *)
     13   final:
     14    ∀hd.
     15     fetch hd ≠ Ret … →
     16     fetch (execute 1 hd) = Cost … →
     17      trace_lab_lab0 false
     18 | final_ret:
     19    ∀hd.
     20     fetch hd = Ret … → trace_lab_lab0 true
     21 | call:
     22    ∀b.∀bf.∀trace:trace_lab_ret.∀af,tl.
     23     trace_lab_lab0 b tl →
     24     fetch bf = Call … →
     25     pc af = pc bf + 2 →
     26      execute 1 bf = hd trace →
     27      execute 1 (last trace) = af →
     28       trace_lab_lab
     29 | other:
     30    ∀b.∀hd,tl.
     31     trace_lab_lab0 b tl →
     32     fetch hd ≠ Call … →
     33     fetch (execute 1 hd) ≠ Cost … →
     34     fetch hd ≠ Ret … →
     35      simple_path_0
     36
     37with trace_lab_lab: bool → Type[0] ≝
     38 mk_trace_lab_lab: ∀b.∀p:trace_lab_lab0 b → is_labelled (hd p) → trace_lab_lab b.
     39
     40definition compute_simple_path0 (s:Status) (is_labelled s) (well_balanced s): trace_lab_ret ≝ ….
     41
     42lemma simple_path_ok:
     43 ∀st: Status.∀H.
     44 let p ≝ compute_simple_path0 st H in
     45   ∀n.
     46    nth_path n p = execute n st ∧
     47     (execute' (path_length p) st = 〈st',τ〉 →
     48      τ = cost_trace p)
     49  ].
     50
     51let rec trace_lab_rec_cost (p: trace_lab_ret) : nat. COUNTS EVERYTHING
     52
     53lemma trace_lab_rec_cost_ok:
     54 ∀p: trace_lab_rec.
     55  trace_lab_rec_cost p = Timer (last p) - Timer (first p).
     56
     57let rec trace_lab_lab_cost_nocall (p: trace_lab_lab) : nat ≝
     58 match p with
     59 [ call ⇒ DO NOT ADD ANYTHING
     60 | _ ⇒ DO ADD ].
     61
     62let rec trace_lab_rec_cost' (p: trace_lab_ret) : nat.
     63 | (call b bf tr af tl) as self ⇒
     64    trace_lab_lab_cost_nocall self + trace_lab_ret_cost' tr +
     65    trace_lab_rec_cost' tl
     66
     67theorem main_lemma:
     68 ∀p. trace_lab_rec_cost p = trace_lab_rec_cost' p.
     69
     70axiom lemma1:
     71 ∀p: simple_path.
     72  traverse_cost_internal (pc (hd p)) … = trace_lab_lab_cost_nocall p.
     73
     74axiom lemma2:
     75 ∀s,l,cost_map.
     76  is_labelled l s →
     77   traverse_cost_internal s = cost_map l.
     78
    579axiom main_statement:
    6   ∀s: Status.
    7   ∀cost_labels: BitVectorTrie Byte 16.
    8     let program_counter ≝ program_counter … s in
    9       ∀cost_label: Byte.
    10       ∀s': Status.
    11       ∀n: nat.
    12         (lookup_opt … program_counter cost_labels) = (Some … cost_label) ∧
    13         s' = (execute n s) → ?.
    14        
     80 ∀s.
     81 ∀cost_map.
     82 let p ≝ compute_simple_path0 s in
     83 ∑ (cost_trace p) cost_map = trace_lab_rec_cost' p.
     84
     85axiom main_statement:
     86 ∀s.
     87 ∀cost_map.
     88 let p ≝ compute_simple_path0 s in
     89  execute' (path_length p) s = 〈s',τ〉 →
     90   Timer s' - Timer s = ∑ τ cost_map.
Note: See TracChangeset for help on using the changeset viewer.