Changeset 2150


Ignore:
Timestamp:
Jul 3, 2012, 11:30:37 AM (5 years ago)
Author:
campbell
Message:

Add labelling result to the correctness file.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/correctness.ma

    r2004 r2150  
    55include "Clight/Cexec.ma".
    66include "ASM/Interpret2.ma".
     7
     8include "Clight/labelSimulation.ma".
     9
     10theorem correct :
     11  ∀input_program.
     12
     13  not_wrong (exec_inf … clight_fullexec input_program) →
     14 
     15  ∀object_code,costlabel_map,labelled,cost_map.
     16  compile input_program = OK ? 〈〈object_code,costlabel_map〉,labelled,cost_map〉 →
     17 
     18  sim_with_labels (exec_inf … clight_fullexec input_program) (exec_inf … clight_fullexec labelled)
     19  ∧
     20  True (* TODO *).
     21
     22#input_program
     23#NOT_WRONG
     24#object_code #costlabel_map #labelled #cost_map
     25#COMPILE
     26cases (bind_inversion ????? COMPILE) -COMPILE * #labelled' #rtlabs_program * #FRONTEND #COMPILE
     27cases (bind_inversion ????? COMPILE) -COMPILE * #object_code' #costlabel_map' * #ASSEMBLER #COMPILE
     28whd in COMPILE:(??%%); destruct
     29cases (bind_inversion ????? FRONTEND) -FRONTEND #cminor_program * #CMINOR #FRONTEND
     30cases (bind_inversion ????? FRONTEND) -FRONTEND #rtlabs_program' * #RTLABS #FRONTEND
     31whd in FRONTEND:(??%%); destruct
     32
     33%
     34[ @labelling_sim @NOT_WRONG
     35| @I
     36] qed.
    737
    838(* TODO
Note: See TracChangeset for help on using the changeset viewer.