| 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 | |
|---|
