1 | |
---|
2 | include "compiler.ma". |
---|
3 | |
---|
4 | include "common/SmallstepExec.ma". |
---|
5 | include "Clight/Cexec.ma". |
---|
6 | include "ASM/Interpret2.ma". |
---|
7 | |
---|
8 | include "Clight/labelSimulation.ma". |
---|
9 | |
---|
10 | theorem 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 |
---|
26 | cases (bind_inversion ????? COMPILE) -COMPILE * * #init_cost #labelled' #rtlabs_program * #FRONTEND #COMPILE |
---|
27 | cases (bind_inversion ????? COMPILE) -COMPILE * #object_code' #costlabel_map' * #ASSEMBLER #COMPILE |
---|
28 | whd in COMPILE:(??%%); destruct |
---|
29 | cases (bind_inversion ????? FRONTEND) -FRONTEND #cminor_program * #CMINOR #FRONTEND |
---|
30 | whd 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 | |
---|
42 | exec_inf … clight_fullexec input_program ≃l exec_inf … clight_fullexec labelled |
---|
43 | |
---|
44 | ∧ |
---|
45 | |
---|
46 | exec_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] |
---|
53 | i 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. |
---|
59 | let ge ≝ (globalenvs … labelled) in |
---|
60 | subtrace_of (exec_inf … RTLabs_fullexec labelled) flat → |
---|
61 | RTLabs_cost s = true → |
---|
62 | ∀WR : will_return ge 0 s flat. |
---|
63 | let structured_trace_rtlabs ≝ make_label_return' ge 0 s flat ??? WR in |
---|
64 | let 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 | |
---|
72 | What is ≃l? Must show that "labelled" does everything that |
---|
73 | "input_program" does, without getting lost in some |
---|
74 | non-terminating loop part way. |
---|
75 | |
---|
76 | *) |
---|
77 | |
---|