source: src/correctness.ma @ 2320

Last change on this file since 2320 was 2320, checked in by campbell, 8 years ago

Update compiler and correctness with labelling changes.

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