Changeset 2774 for src/correctness.ma


Ignore:
Timestamp:
Mar 5, 2013, 6:15:06 PM (7 years ago)
Author:
sacerdot
Message:
  1. the compiler now outputs both the stack cost model and the max stack available
  2. hypothesis on initial status not failing removed from correctness.ma by using the low level definition
File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/correctness.ma

    r2766 r2774  
    77
    88theorem correct :
    9   ∀input_program
    10   ∀lobject_code,labelled,cost_map.
    11   compile input_program = OK ? 〈lobject_code,❬labelled,cost_map❭〉
     9  ∀input_program,output.
     10(*  ∀lobject_code,labelled,cost_map. *)
     11  compile input_program = OK ? output
    1212
    1313  not_wrong … (exec_inf … clight_fullexec input_program) →
    1414 
    15   sim_with_labels (exec_inf … clight_fullexec input_program) (exec_inf … clight_fullexec labelled)
     15  sim_with_labels
     16   (exec_inf … clight_fullexec input_program)
     17   (exec_inf … clight_fullexec (c_labelled_clight … output))
    1618  ∧
    1719  True (* TODO *).
    1820
    19 #input_program
    20 #object_code #labelled #cost_map
     21#input_program #output
    2122#COMPILE
    2223#NOT_WRONG
     
    3738include "Clight/Clight_abstract.ma".
    3839include "common/Measurable.ma".
    39 
    40 (* We could restrict this function to identifiers that are function names in the
    41    program and lift it (like the lift_cost_map_back_to_front function), but
    42    let's go with the easier notion of having a total map and ignore all the
    43    extra stuff. *)
    44 definition stack_cost_T ≝ ident → nat.
    4540
    4641definition Clight_stack_ident :
     
    117112qed.
    118113
     114include "common/AssocList.ma".
     115
     116definition lookup_stack_cost : stack_cost_model → ident → nat ≝
     117 λstack_cost,id.
     118  match assoc_list_lookup ?? id (eq_identifier …) stack_cost with
     119  [ None ⇒ 0 | Some n ⇒ n ].
     120
    119121definition simulates ≝
    120   λstack_cost : stack_cost_T.  λ stack_bound, labelled, object_code, cost_map, initial_status.
    121   return initial_status = make_initial_state ?? (OC_preclassified_system object_code) it →
    122   ∀m1,m2. measurable Clight_pcs labelled m1 m2 stack_cost stack_bound →
    123   ∀c1,c2. clight_clock_after labelled m1 cost_map = Some ? c1 → clight_clock_after labelled m2 cost_map = Some ? c2 →
    124   ∃n1,n2. observables Clight_pcs labelled m1 m2 = observables (OC_preclassified_system object_code) it n1 n2 ∧
     122  λp: compiler_output.
     123  let initial_status ≝ initialise_status … (load_code_memory (oc (c_labelled_object_code … p))) in
     124  ∀m1,m2.
     125   measurable Clight_pcs (c_labelled_clight … p) m1 m2
     126    (lookup_stack_cost (c_stack_cost … p)) (c_max_stack … p) →
     127  ∀c1,c2.
     128   clight_clock_after (c_labelled_clight … p) m1 (c_clight_cost_map … p) = Some ? c1 →
     129   clight_clock_after (c_labelled_clight … p) m2 (c_clight_cost_map … p) = Some ? c2 →
     130  ∃n1,n2.
     131   observables Clight_pcs (c_labelled_clight … p) m1 m2 =
     132   observables (OC_preclassified_system (c_labelled_object_code … p)) it n1 n2
     133  ∧
    125134   minus c2 c1 = clock … (execute n2 ? initial_status) - clock … (execute n1 ? initial_status).
    126135
    127136theorem correct' :
    128   ∀input_program. 
    129   ∀lobject_code,labelled,cost_map,stack_cost,stack_bound,initial_status.
    130   compile input_program = OK ? 〈lobject_code,❬labelled,cost_map❭〉 →
    131 
     137  ∀input_program,output.
     138  ∀initial_status.
     139  compile input_program = OK ? output →
    132140  not_wrong … (exec_inf … clight_fullexec input_program) →
    133  
    134   return initial_status = make_initial_state ?? (OC_preclassified_system lobject_code) it →
    135  
    136   sim_with_labels (exec_inf … clight_fullexec input_program) (exec_inf … clight_fullexec labelled)
     141  sim_with_labels
     142   (exec_inf … clight_fullexec input_program)
     143   (exec_inf … clight_fullexec (c_labelled_clight … output))
    137144  ∧
    138   simulates stack_cost stack_bound labelled lobject_code cost_map initial_status.
    139  
    140 
     145  simulates output.
    141146 
    142147(* start of old simulates 
Note: See TracChangeset for help on using the changeset viewer.