| [1996] | 1 | |
|---|
| 2 | include "compiler.ma". |
|---|
| 3 | |
|---|
| 4 | include "common/SmallstepExec.ma". |
|---|
| 5 | include "Clight/Cexec.ma". |
|---|
| 6 | include "ASM/Interpret2.ma". |
|---|
| 7 | |
|---|
| [2150] | 8 | include "Clight/labelSimulation.ma". |
|---|
| 9 | |
|---|
| 10 | theorem correct : |
|---|
| 11 | ∀input_program. |
|---|
| 12 | |
|---|
| [2205] | 13 | not_wrong … (exec_inf … clight_fullexec input_program) → |
|---|
| [2150] | 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 * #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 | cases (bind_inversion ????? FRONTEND) -FRONTEND #rtlabs_program' * #RTLABS #FRONTEND |
|---|
| 31 | whd in FRONTEND:(??%%); destruct |
|---|
| 32 | |
|---|
| 33 | % |
|---|
| 34 | [ @labelling_sim @NOT_WRONG |
|---|
| 35 | | @I |
|---|
| 36 | ] qed. |
|---|
| 37 | |
|---|
| [1996] | 38 | (* TODO |
|---|
| 39 | |
|---|
| 40 | ∀input_program. |
|---|
| [2003] | 41 | ! 〈object_code,costlabel_map,labelled,cost_map〉 ← compile input_program |
|---|
| [1996] | 42 | |
|---|
| [2001] | 43 | exec_inf … clight_fullexec input_program ≃l exec_inf … clight_fullexec labelled |
|---|
| [1996] | 44 | |
|---|
| 45 | ∧ |
|---|
| 46 | |
|---|
| [2004] | 47 | exec_inf … clight_fullexec labelled ≈ exec_inf … ASM_fullexec object_code |
|---|
| 48 | (* Should we be lifting labels in some way here? *) |
|---|
| [1996] | 49 | |
|---|
| [2001] | 50 | ∧ |
|---|
| 51 | |
|---|
| 52 | |
|---|
| [2003] | 53 | ∀i,f : clight_status. [i,f labelled, at same level] |
|---|
| 54 | i clight~> f → |
|---|
| [2004] | 55 | ∃!i',f'. i ≃ i' ∧ f ≃ f' ∧ i' 8051~> f' ∧ |
|---|
| [2003] | 56 | clock f - clock i = clock f' - clock i'. |
|---|
| [1996] | 57 | |
|---|
| [2001] | 58 | |
|---|
| [2003] | 59 | ∀s,flat. |
|---|
| 60 | let ge ≝ (globalenvs … labelled) in |
|---|
| 61 | subtrace_of (exec_inf … RTLabs_fullexec labelled) flat → |
|---|
| 62 | RTLabs_cost s = true → |
|---|
| 63 | ∀WR : will_return ge 0 s flat. |
|---|
| 64 | let structured_trace_rtlabs ≝ make_label_return' ge 0 s flat ??? WR in |
|---|
| 65 | let 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 ])). |
|---|
| [2001] | 70 | |
|---|
| [2003] | 71 | |
|---|
| 72 | |
|---|
| [2001] | 73 | What is ≃l? Must show that "labelled" does everything that |
|---|
| 74 | "input_program" does, without getting lost in some |
|---|
| 75 | non-terminating loop part way. |
|---|
| 76 | |
|---|
| [1996] | 77 | *) |
|---|
| 78 | |
|---|
