source: src/correctness.ma @ 2125

Last change on this file since 2125 was 2004, checked in by campbell, 7 years ago

Minor edits from discussion.

File size: 1.3 KB
RevLine 
[1996]1
2include "compiler.ma".
3
4include "common/SmallstepExec.ma".
5include "Clight/Cexec.ma".
6include "ASM/Interpret2.ma".
7
8(* TODO
9
10∀input_program.
[2003]11! 〈object_code,costlabel_map,labelled,cost_map〉 ← compile input_program
[1996]12
[2001]13exec_inf … clight_fullexec input_program ≃l exec_inf … clight_fullexec labelled
[1996]14
15
16
[2004]17exec_inf … clight_fullexec labelled ≈ exec_inf … ASM_fullexec object_code
18(* Should we be lifting labels in some way here? *)
[1996]19
[2001]20
21
22
[2003]23∀i,f : clight_status.  [i,f labelled, at same level]
24i clight~> f →
[2004]25∃!i',f'. i ≃ i' ∧ f ≃ f' ∧ i' 8051~> f' ∧
[2003]26  clock f - clock i = clock f' - clock i'.
[1996]27
[2001]28
[2003]29∀s,flat.
30let ge ≝ (globalenvs … labelled) in
31subtrace_of (exec_inf … RTLabs_fullexec labelled) flat →
32RTLabs_cost s = true →
33∀WR : will_return ge 0 s flat.
34let structured_trace_rtlabs ≝ make_label_return' ge 0 s flat ??? WR in
35let 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 ])).
[2001]40
[2003]41
42
[2001]43What is ≃l?  Must show that "labelled" does everything that
44"input_program" does, without getting lost in some
45non-terminating loop part way.
46
[1996]47*)
48
Note: See TracBrowser for help on using the repository browser.