| 1 | |
|---|
| 2 | include "compiler.ma". |
|---|
| 3 | |
|---|
| 4 | include "common/SmallstepExec.ma". |
|---|
| 5 | include "Clight/Cexec.ma". |
|---|
| 6 | include "ASM/Interpret2.ma". |
|---|
| 7 | |
|---|
| 8 | (* TODO |
|---|
| 9 | |
|---|
| 10 | ∀input_program. |
|---|
| 11 | ! 〈object_code,costlabel_map,labelled,cost_map〉 ← compile input_program |
|---|
| 12 | |
|---|
| 13 | exec_inf … clight_fullexec input_program ≃l exec_inf … clight_fullexec labelled |
|---|
| 14 | |
|---|
| 15 | ∧ |
|---|
| 16 | |
|---|
| 17 | exec_inf … clight_fullexec labelled ≈ exec_inf … ASM_fullexec object_code |
|---|
| 18 | (* Should we be lifting labels in some way here? *) |
|---|
| 19 | |
|---|
| 20 | ∧ |
|---|
| 21 | |
|---|
| 22 | |
|---|
| 23 | ∀i,f : clight_status. [i,f labelled, at same level] |
|---|
| 24 | i clight~> f → |
|---|
| 25 | ∃!i',f'. i ≃ i' ∧ f ≃ f' ∧ i' 8051~> f' ∧ |
|---|
| 26 | clock f - clock i = clock f' - clock i'. |
|---|
| 27 | |
|---|
| 28 | |
|---|
| 29 | ∀s,flat. |
|---|
| 30 | let ge ≝ (globalenvs … labelled) in |
|---|
| 31 | subtrace_of (exec_inf … RTLabs_fullexec labelled) flat → |
|---|
| 32 | RTLabs_cost s = true → |
|---|
| 33 | ∀WR : will_return ge 0 s flat. |
|---|
| 34 | let structured_trace_rtlabs ≝ make_label_return' ge 0 s flat ??? WR in |
|---|
| 35 | let labels_rtlabs ≝ flat_label_trace … flat WR in |
|---|
| 36 | ∃!initial,final,structured_trace_asm. |
|---|
| 37 | structured_trace_rtlabs ≈ structured_trace_asm ∧ |
|---|
| 38 | clock … code_memory … final = clock … code_memory … initial + |
|---|
| 39 | (Σ_{i < |labels_rtlabs|} (cost_map (match nth i labels_rtlabs with [ Some k ⇒ k | None ⇒ 0 ])). |
|---|
| 40 | |
|---|
| 41 | |
|---|
| 42 | |
|---|
| 43 | What is ≃l? Must show that "labelled" does everything that |
|---|
| 44 | "input_program" does, without getting lost in some |
|---|
| 45 | non-terminating loop part way. |
|---|
| 46 | |
|---|
| 47 | *) |
|---|
| 48 | |
|---|
