Changeset 2765


Ignore:
Timestamp:
Mar 3, 2013, 12:23:41 AM (7 years ago)
Author:
sacerdot
Message:
  1. correctness.ma repaired
  2. we used the OC_preclassified_system to make the theorem statement more uniform and close all the axioms

Notes:
a) the next step is to make the compiler return the stack cost too (easy)
b) the component of fullexec that returns the initial state returns a res.

Thus the final statement becomes uglier because program initialization
can fail. The one for the OC never does so, actually! I can call the
low level init function, but this breaks the preclassified_system
abstraction. Do we really need it to fail?

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/correctness.ma

    r2722 r2765  
    99
    1010theorem correct :
    11   ∀input_program.
    12  
    13   ∀object_code,costlabel_map,labelled,cost_map.
    14   compile input_program = OK ? 〈〈object_code,costlabel_map〉,❬labelled,cost_map❭〉 →
     11  ∀input_program. 
     12  ∀lobject_code,labelled,cost_map.
     13  compile input_program = OK ? 〈lobject_code,❬labelled,cost_map❭〉 →
    1514
    1615  not_wrong … (exec_inf … clight_fullexec input_program) →
     
    2120
    2221#input_program
    23 #object_code #costlabel_map #labelled #cost_map
     22#object_code #labelled #cost_map
    2423#COMPILE
    2524#NOT_WRONG
    2625cases (bind_inversion ????? COMPILE) -COMPILE * * #init_cost #labelled' #rtlabs_program * #FRONTEND #COMPILE
    27 cases (bind_inversion ????? COMPILE) -COMPILE * #object_code' #costlabel_map' * #ASSEMBLER #COMPILE
     26cases (bind_inversion ????? COMPILE) -COMPILE #lobject_code' * #ASSEMBLER #COMPILE
    2827whd in COMPILE:(??%%); destruct
    2928cases (bind_inversion ????? FRONTEND) -FRONTEND #cminor_program * #CMINOR #FRONTEND
     
    7776 *)
    7877
    79 axiom observables_8051 : object_code → nat → nat → res ((list intensional_event) × (list intensional_event)).
    80 
    8178definition in_execution_prefix : execution_prefix Clight_state → costlabel → Prop ≝
    8279λx,l. Exists … (λtrs. Exists … (λev. ev = EVcost l) (\fst trs)) x.
     
    122119qed.
    123120
    124 axiom initial_8051_status : ∀oc. Status oc.
    125 
    126121definition simulates ≝
    127   λstack_cost : stack_cost_T.  λ stack_bound, labelled, object_code, cost_map.
    128   let initial_status ≝ initial_8051_status (load_code_memory object_code) in
     122  λstack_cost : stack_cost_T.  λ stack_bound, labelled, object_code, cost_map, initial_status.
     123  return initial_status = make_initial_state ?? (OC_preclassified_system object_code) it →
    129124  ∀m1,m2. measurable Clight_pcs labelled m1 m2 stack_cost stack_bound →
    130125  ∀c1,c2. clight_clock_after labelled m1 cost_map = Some ? c1 → clight_clock_after labelled m2 cost_map = Some ? c2 →
    131   ∃n1,n2. observables Clight_pcs labelled m1 m2 = observables_8051 object_code n1 n2 ∧
    132           c2 - c1 = clock … (execute n2 ? initial_status) - clock … (execute n1 ? initial_status).
    133 
    134 axiom compile' : clight_program → res (object_code × costlabel_map ×
    135   (𝚺labelled:clight_program. ((Σl:costlabel.in_clight_program labelled l)→ℕ)) × stack_cost_T × nat).
     126  ∃n1,n2. observables Clight_pcs labelled m1 m2 = observables (OC_preclassified_system object_code) it n1 n2 ∧
     127   minus c2 c1 = clock … (execute n2 ? initial_status) - clock … (execute n1 ? initial_status).
    136128
    137129theorem correct' :
    138   ∀input_program.
     130  ∀input_program. 
     131  ∀lobject_code,labelled,cost_map,stack_cost,stack_bound,initial_status.
     132  compile input_program = OK ? 〈lobject_code,❬labelled,cost_map❭〉 →
    139133
    140134  not_wrong … (exec_inf … clight_fullexec input_program) →
    141135 
    142   ∀object_code,costlabel_map,labelled,cost_map,stack_cost,stack_bound.
    143   compile' input_program = OK ? 〈〈〈object_code,costlabel_map〉,❬labelled,cost_map❭〉,stack_cost,stack_bound〉 →
     136  return initial_status = make_initial_state ?? (OC_preclassified_system lobject_code) it →
    144137 
    145138  sim_with_labels (exec_inf … clight_fullexec input_program) (exec_inf … clight_fullexec labelled)
    146139  ∧
    147 
    148   simulates stack_cost stack_bound labelled object_code cost_map.
     140  simulates stack_cost stack_bound labelled lobject_code cost_map initial_status.
    149141 
    150142
Note: See TracChangeset for help on using the changeset viewer.