source: src/correctness.ma @ 2565

Last change on this file since 2565 was 2513, checked in by mckinna, 7 years ago

Minor tweaks. Simplified dependencies again.

File size: 7.0 KB
Line 
1
2include "compiler.ma".
3
4include "ASM/Interpret2.ma".
5
6include "Clight/Cexec.ma".
7
8include "Clight/labelSimulation.ma".
9
10theorem correct :
11  ∀input_program.
12 
13  ∀object_code,costlabel_map,labelled,cost_map.
14  compile input_program = OK ? 〈〈object_code,costlabel_map〉,❬labelled,cost_map❭〉 →
15
16  not_wrong … (exec_inf … clight_fullexec input_program) →
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#object_code #costlabel_map #labelled #cost_map
24#COMPILE
25#NOT_WRONG
26cases (bind_inversion ????? COMPILE) -COMPILE * * #init_cost #labelled' #rtlabs_program * #FRONTEND #COMPILE
27cases (bind_inversion ????? COMPILE) -COMPILE * #object_code' #costlabel_map' * #ASSEMBLER #COMPILE
28whd in COMPILE:(??%%); destruct
29cases (bind_inversion ????? FRONTEND) -FRONTEND #cminor_program * #CMINOR #FRONTEND
30whd in FRONTEND:(??%%); destruct
31
32%
33[ (* Needs switch removal too, now
34     @labelling_sim @NOT_WRONG
35   *) cases daemon
36| @I
37] qed.
38
39
40include "Clight/abstract.ma".
41include "common/Measurable.ma".
42
43definition Clight_stack_T ≝ ∀s:Clight_state. match Clight_classify s with [ cl_call ⇒ True | cl_return ⇒ True | _ ⇒ False ] → nat.
44
45definition Clight_pcs : preclassified_system ≝
46mk_preclassified_system
47  clight_fullexec
48  (λ_.Clight_labelled)
49  (λ_.Clight_classify).
50
51(* From measurable on Clight, we will end up with an RTLabs flat trace where
52   we know that there are some m' and n' such that the prefix in Clight matches
53   the prefix in RTLabs given by m', the next n steps in Clight are equivalent
54   to the n' steps in RTLabs, and we have a suitable "will_return" for RTLabs
55   for those n' steps so that we can build a corresponding structured trace.
56   
57   "Equivalent" here means, in particular, that the observables will be the same,
58   and those observables will include the stack space costs.
59 *)
60
61axiom observables_8051 : object_code → nat → nat → option ((list trace) × (list trace)).
62
63definition in_execution_prefix : execution_prefix Clight_state → costlabel → Prop ≝
64λx,l. Exists … (λtrs. Exists … (λev. ev = EVcost l) (\fst trs)) x.
65
66let rec foldl_exists_aux (A,B:Type[0]) (l,l':list B) (f:A → ∀b:B. Exists … (λx.x=b) l → A) (a:A) on l' : (∀b. Exists … (λx.x=b) l' → Exists … (λx.x=b) l) → A ≝
67match l' return λl'. (∀b. Exists … (λx.x=b) l' → Exists … (λx.x=b) l) → A with
68[ nil ⇒ λ_. a
69| cons h t ⇒ λH. foldl_exists_aux A B l t f (f a h (H …)) ?
70].
71[ %1 %
72| #b #H' @H %2 @H'
73] qed.
74
75definition foldl_exists : ∀A,B:Type[0]. ∀l:list B. (A → ∀b:B. Exists … (λx. x = b ) l → A) → A → A ≝
76λA,B,l,f,a.  foldl_exists_aux A B l l f a (λb,H. H).
77
78lemma Exists_lift : ∀A,P,Q,l.
79  (∀x. P x → Q x) →
80  Exists A P l →
81  Exists A Q l.
82#A #P #Q #l elim l
83[ //
84| #h #t #IH #H * [ #H' %1 @H @H' | #H' %2 @IH /2/ ]
85] qed.
86
87definition measure_clock : ∀x:execution_prefix Clight_state. ((Σl:costlabel.in_execution_prefix x l)→ℕ) → nat ≝
88λx,costmap. foldl_exists … x
89 (λclock,trs,H.
90    foldl_exists … (\fst trs) (λclock,ev. match ev return λev. Exists … (λx. x=ev) ? → nat with [ EVcost l ⇒ λH'. clock + costmap «l,?» | _ ⇒ λ_. clock ]) clock)
91 0.
92whd @(Exists_lift … H) * #tr1 #s1 #E destruct @(Exists_lift … H') #ev1 #E @E
93qed.
94
95definition clight_clock_after : ∀p:clight_program. nat → ((Σl:costlabel.in_clight_program p l)→ℕ) → option nat ≝
96λp,n,costmap.
97  let x ≝ exec_inf … clight_fullexec p in
98  match split_trace … x n with
99  [ Some traces ⇒
100    Some ? (measure_clock (\fst traces) (λl.costmap «l,?»))
101  | None ⇒ None ?
102  ].
103cases daemon
104qed.
105
106axiom initial_8051_status : ∀oc. Status oc.
107
108definition simulates ≝
109  λstack_cost : Clight_stack_T.  λ stack_bound, labelled, object_code, cost_map.
110  let initial_status ≝ initial_8051_status (load_code_memory object_code) in
111  ∀m1,m2. measurable Clight_pcs labelled m1 m2 stack_cost stack_bound →
112  ∀c1,c2. clight_clock_after labelled m1 cost_map = Some ? c1 → clight_clock_after labelled m2 cost_map = Some ? c2 →
113  ∃n1,n2. observables clight_fullexec labelled m1 m2 = observables_8051 object_code n1 n2 ∧
114          c2 - c1 = clock … (execute n2 ? initial_status) - clock … (execute n1 ? initial_status).
115
116axiom compile' : clight_program → res (object_code × costlabel_map ×
117  (𝚺labelled:clight_program. ((Σl:costlabel.in_clight_program labelled l)→ℕ)) × Clight_stack_T × nat).
118
119theorem correct' :
120  ∀input_program.
121
122  not_wrong … (exec_inf … clight_fullexec input_program) →
123 
124  ∀object_code,costlabel_map,labelled,cost_map,stack_cost,stack_bound.
125  compile' input_program = OK ? 〈〈〈object_code,costlabel_map〉,❬labelled,cost_map❭〉,stack_cost,stack_bound〉 →
126 
127  sim_with_labels (exec_inf … clight_fullexec input_program) (exec_inf … clight_fullexec labelled)
128  ∧
129
130  simulates stack_cost stack_bound labelled object_code cost_map.
131 
132
133 
134(* start of old simulates 
135
136(* [nth_state_of_with_stack state stack_cost stack_bound exec n] returns [Some s] iff after
137   [n] steps of [exec] we have reached [s] without exceeding the [stack_bound]
138   according to the [stack_cost] function. *)
139axiom nth_state_of_with_stack : ∀state. (state → nat) → nat → execution state io_out io_in → nat → option state.
140axiom nth_state_of : ∀state. execution state io_out io_in → nat → option state.
141
142
143  let cl_trace ≝ exec_inf … clight_fullexec labelled in
144  let asm_trace ≝ exec_inf … ASM_fullexec object_code in
145  not_wrong ? cl_trace →
146  ∀n,s. nth_state_of_with_stack ? stack_cost stack_bound cl_trace n = Some ? s →
147  𝚺m,s'. nth_state_of ? asm_trace m = Some ? s' ∧ s ≃ s'
148
149*)
150
151(* TODO
152
153
154∀input_program.
155! 〈object_code,costlabel_map,labelled,cost_map〉 ← compile input_program
156
157exec_inf … clight_fullexec input_program ≃l exec_inf … clight_fullexec labelled
158
159
160
161exec_inf … clight_fullexec labelled ≈ exec_inf … ASM_fullexec object_code
162(* Should we be lifting labels in some way here? *)
163
164
165
166∀i,f : clight_status.
167  Clight_labelled i →
168  Clight_labelled f →
169∀mx,time.
170  let trace ≝ exec_inf_aux … clight_fullexec labelled i in
171  will_return O O mx time f trace →
172  mx < max_allowed_stack →
173∃!i',f'. i ≃ i' ∧ f ≃ f' ∧ i' 8051~> f' ∧
174  time = clock f' - clock i'.
175
176
177∀s,flat.
178let ge ≝ (globalenvs … labelled) in
179subtrace_of (exec_inf … RTLabs_fullexec labelled) flat →
180RTLabs_cost s = true →
181∀WR : will_return ge 0 s flat.
182let structured_trace_rtlabs ≝ make_label_return' ge 0 s flat ??? WR in
183let labels_rtlabs ≝ flat_label_trace … flat WR in
184∃!initial,final,structured_trace_asm.
185  structured_trace_rtlabs ≈ structured_trace_asm ∧ 
186  clock … code_memory … final = clock … code_memory … initial +
187     (Σ_{i < |labels_rtlabs|} (cost_map (match nth i labels_rtlabs with [ Some k ⇒ k | None ⇒ 0 ])).
188
189
190
191What is ≃l?  Must show that "labelled" does everything that
192"input_program" does, without getting lost in some
193non-terminating loop part way.
194
195*)
196
Note: See TracBrowser for help on using the repository browser.