source: src/correctness.ma @ 2150

Last change on this file since 2150 was 2150, checked in by campbell, 7 years ago

Add labelling result to the correctness file.

File size: 2.3 KB
Line 
1
2include "compiler.ma".
3
4include "common/SmallstepExec.ma".
5include "Clight/Cexec.ma".
6include "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.
37
38(* TODO
39
40∀input_program.
41! 〈object_code,costlabel_map,labelled,cost_map〉 ← compile input_program
42
43exec_inf … clight_fullexec input_program ≃l exec_inf … clight_fullexec labelled
44
45
46
47exec_inf … clight_fullexec labelled ≈ exec_inf … ASM_fullexec object_code
48(* Should we be lifting labels in some way here? *)
49
50
51
52
53∀i,f : clight_status.  [i,f labelled, at same level]
54i clight~> f →
55∃!i',f'. i ≃ i' ∧ f ≃ f' ∧ i' 8051~> f' ∧
56  clock f - clock i = clock f' - clock i'.
57
58
59∀s,flat.
60let ge ≝ (globalenvs … labelled) in
61subtrace_of (exec_inf … RTLabs_fullexec labelled) flat →
62RTLabs_cost s = true →
63∀WR : will_return ge 0 s flat.
64let structured_trace_rtlabs ≝ make_label_return' ge 0 s flat ??? WR in
65let labels_rtlabs ≝ flat_label_trace … flat WR in
66∃!initial,final,structured_trace_asm.
67  structured_trace_rtlabs ≈ structured_trace_asm ∧ 
68  clock … code_memory … final = clock … code_memory … initial +
69     (Σ_{i < |labels_rtlabs|} (cost_map (match nth i labels_rtlabs with [ Some k ⇒ k | None ⇒ 0 ])).
70
71
72
73What is ≃l?  Must show that "labelled" does everything that
74"input_program" does, without getting lost in some
75non-terminating loop part way.
76
77*)
78
Note: See TracBrowser for help on using the repository browser.