source: src/ERTLptr/ERTLptrToLTLProof.ma @ 2930

Last change on this file since 2930 was 2930, checked in by sacerdot, 9 years ago

More progress. Some useless parameters have been removed from the axioms.
Axiom's parameters fixed (they were not inhabited before).

File size: 36.6 KB
Line 
1include "ERTLptr/ERTLptrToLTL.ma".
2include "ERTLptr/ERTLptr_semantics.ma".
3include "LTL/LTL_semantics.ma".
4include "joint/Traces.ma".
5include "common/StatusSimulation.ma".
6include "common/AssocList.ma".
7
8
9
10(* Inefficient, replace with Trie lookup *)
11definition lookup_stack_cost ≝
12 λp.λid : ident.
13  assoc_list_lookup ? ℕ id (eq_identifier …) p.
14
15(*TO BE MOVED*)
16definition ERTLptr_status ≝
17λprog : ertlptr_program.λstack_sizes.
18joint_abstract_status (mk_prog_params ERTLptr_semantics prog stack_sizes).
19
20definition LTL_status ≝
21λprog : ltl_program.λstack_sizes.
22joint_abstract_status (mk_prog_params LTL_semantics prog stack_sizes).
23
24definition local_clear_sb_type ≝ decision → bool.
25definition clear_sb_type ≝ label → local_clear_sb_type.
26 
27axiom to_be_cleared_sb : 
28∀after : valuation register_lattice. coloured_graph after → clear_sb_type.
29
30definition local_clear_fb_type ≝ vertex → bool.
31definition clear_fb_type ≝ label → local_clear_fb_type.
32
33axiom to_be_cleared_fb :
34∀after : valuation register_lattice.clear_fb_type.
35
36axiom sigma_fb_state:
37 ertlptr_program → local_clear_fb_type →
38  state ERTLptr_semantics → state ERTLptr_semantics.
39
40axiom acc_is_dead : ∀fix_comp.∀prog : ertlptr_program.
41∀fn : joint_closed_internal_function ERTLptr (prog_var_names … prog).
42∀l.
43let after ≝ (analyse_liveness fix_comp (prog_var_names … prog) fn) in
44¬ lives (inr ? ? RegisterA) (livebefore  … fn l after).
45
46axiom dead_registers_in_dead :
47 ∀fix_comp.∀build : coloured_graph_computer.
48 ∀prog : ertlptr_program.
49 ∀fn : joint_closed_internal_function ERTLptr (prog_var_names … prog).
50 ∀l.
51 let after ≝ (analyse_liveness fix_comp (prog_var_names … prog) fn) in
52 let coloured_graph ≝ build … fn after in
53 ∀R : Register.
54  ¬ lives (inr ? ? R) (livebefore  … fn l after) →
55   to_be_cleared_sb after coloured_graph l R.
56
57axiom sigma_sb_state:
58 ertlptr_program → local_clear_sb_type → state LTL_semantics → state ERTLptr_semantics.
59
60definition dummy_state : state ERTLptr_semantics ≝
61mk_state ERTL_semantics
62   (None ?) empty_is BBundef 〈empty_map ? ?,mk_hw_register_env … (Stub …) BBundef〉 empty.
63
64definition dummy_state_pc : state_pc ERTLptr_semantics ≝
65mk_state_pc ? dummy_state (null_pc one) (null_pc one).
66
67
68definition sigma_fb_state_pc :
69 fixpoint_computer → ertlptr_program →
70  state_pc ERTLptr_semantics → state_pc ERTLptr_semantics ≝
71 λfix_comp,prog,st.
72 let ge ≝ globalenv_noinit … prog in
73 let globals ≝ prog_var_names … prog in
74 match fetch_internal_function … ge (pc_block (pc … st)) with
75  [ OK y ⇒
76     let pt ≝ point_of_pc ERTLptr_semantics (pc ? st) in
77     let after ≝ (analyse_liveness fix_comp (prog_var_names … prog) (\snd y)) in
78     mk_state_pc ? (sigma_fb_state prog (to_be_cleared_fb after pt) st) (pc … st) 
79      (last_pop … st)
80  | Error e ⇒ dummy_state_pc
81  ].
82
83include "joint/StatusSimulationHelper.ma".
84
85definition sigma_sb_state_pc:
86 fixpoint_computer → coloured_graph_computer → 
87  ertlptr_program → lbl_funct → state_pc LTL_semantics → state_pc ERTLptr_semantics ≝
88 λfix_comp,build,prog,f_lbls,st.
89  let ge ≝ globalenv_noinit … prog in
90  let globals ≝ prog_var_names … prog in
91  match fetch_internal_function … ge (pc_block (pc … st)) with
92  [ OK y ⇒ 
93     let pt ≝ point_of_pc ERTLptr_semantics (pc ? st) in
94     let after ≝ (analyse_liveness fix_comp (prog_var_names … prog) (\snd y)) in
95     let coloured_graph ≝ build … (\snd y) after in
96     mk_state_pc ? (sigma_sb_state prog
97                       (to_be_cleared_sb after coloured_graph pt) st) (pc … st) 
98                   (sigma_stored_pc ERTLptr_semantics LTL_semantics
99                                    prog f_lbls (last_pop … st))
100  | Error e ⇒ dummy_state_pc
101  ].
102
103definition state_rel : fixpoint_computer → coloured_graph_computer →
104ertlptr_program → (Σb:block.block_region b = Code) → label →
105 state ERTL_state → state LTL_LIN_state → Prop ≝
106λfix_comp,build,prog,bl,pc,st1,st2.
107∃f,fn.fetch_internal_function ? (globalenv_noinit … prog) bl = return 〈f,fn〉 ∧
108let after ≝ (analyse_liveness fix_comp (prog_var_names … prog) fn) in
109let coloured_graph ≝ build … fn after in
110(sigma_fb_state prog (to_be_cleared_fb after pc) st1) =
111(sigma_sb_state prog (to_be_cleared_sb after coloured_graph pc) st2).
112
113axiom write_decision :
114 decision → beval → state LTL_LIN_state → state LTL_LIN_state.
115
116axiom read_arg_decision : arg_decision → state LTL_LIN_state → beval.
117
118axiom insensitive_to_be_cleared_sb :
119 ∀prog. ∀tb : local_clear_sb_type. ∀st : state LTL_LIN_state.
120  ∀d : decision.∀bv.tb d →
121   sigma_sb_state prog tb st =
122    sigma_sb_state prog tb (write_decision d bv st).
123
124
125definition ERTLptr_to_LTL_StatusSimulation :
126∀fix_comp : fixpoint_computer.
127∀colour : coloured_graph_computer.
128∀ prog : ertlptr_program.
129∀ f_lbls, f_regs. ∀f_bl_r.
130b_graph_transform_program_props ERTLptr_semantics LTL_semantics
131     (λglobals,fn.«translate_data fix_comp colour globals fn,(refl …)») prog f_bl_r f_lbls f_regs →
132let p_out ≝ (\fst (\fst (ertlptr_to_ltl fix_comp colour prog))) in
133let m ≝ (\snd (\fst (ertlptr_to_ltl fix_comp colour prog))) in
134let n ≝ \snd (ertlptr_to_ltl fix_comp colour prog) in
135let stacksizes ≝ lookup_stack_cost … m in 
136status_rel (ERTLptr_status prog stacksizes) (LTL_status p_out stacksizes) ≝
137λfix_comp,colour,prog,f_lbls,f_regs,f_bl_r.λgood.
138    mk_status_rel ??
139    (* sem_rel ≝ *)
140         (λs1:ERTLptr_status ? ?
141          .λs2:LTL_status ? ?
142           .sigma_fb_state_pc fix_comp prog s1
143            =sigma_sb_state_pc fix_comp colour prog f_lbls s2)
144    (* call_rel ≝ *) 
145       (λs1:Σs:ERTLptr_status ??.as_classifier ? s cl_call
146          .λs2:Σs:LTL_status ??.as_classifier ? s cl_call
147           .pc ? s1 =sigma_stored_pc ERTLptr_semantics LTL_semantics
148                                                          prog f_lbls (pc ? s2))
149    (* sim_final ≝ *) ?.
150cases daemon
151qed.
152
153axiom as_label_ok :
154∀fix_comp,colour.
155∀prog.∀f_lbls,f_regs. ∀f_bl_r.
156∀ good :b_graph_transform_program_props ERTLptr_semantics LTL_semantics
157     (λglobals,fn.«translate_data fix_comp colour globals fn,(refl …)») prog f_bl_r f_lbls f_regs.
158∀st1,st2,fn,id,stmt.
159let R ≝ sem_rel … (ERTLptr_to_LTL_StatusSimulation fix_comp colour prog … good) in
160R st1 st2 → 
161fetch_statement ERTLptr_semantics (prog_var_names … prog)
162      (globalenv_noinit … prog) (pc … st1) = return 〈id,fn,stmt〉 →
163as_label ? st2 = as_label ? st1.
164
165(*
166(* Copy the proof too from previous pass *)
167axiom fetch_stmt_ok_sigma_state_ok :
168∀prog : ertlptr_program.
169∀ f_lbls,f_regs,id,fn,stmt,st.
170fetch_statement ERTLptr_semantics (prog_var_names … prog)
171    (globalenv_noinit … prog) (pc ? (sigma_sb_state_pc prog f_lbls f_regs st)) =
172               return 〈id,fn,stmt〉 →
173let added ≝ (added_registers ERTLptr (prog_var_names … prog) fn
174                                               (f_regs (pc_block (pc … st)))) in
175st_no_pc … (sigma_sb_state_pc prog f_lbls f_regs st) =
176sigma_sb_state prog f_lbls f_regs added (st_no_pc … st).
177*)
178
179axiom pc_block_eq_sigma_commute : ∀fix_comp,colour.
180∀prog.∀ f_lbls,f_regs.∀f_bl_r.
181∀ good :b_graph_transform_program_props ERTLptr_semantics LTL_semantics
182     (λglobals,fn.«translate_data fix_comp colour globals fn,(refl …)») prog f_bl_r f_lbls f_regs.
183∀st1,st2.
184let R ≝ sem_rel … (ERTLptr_to_LTL_StatusSimulation fix_comp colour prog … good) in
185R st1 st2 →
186pc_block (pc … st1) = pc_block (pc … st2).
187
188axiom pc_eq_sigma_commute : ∀fix_comp,colour.
189∀prog.∀ f_lbls,f_regs.∀f_bl_r.
190∀ good :b_graph_transform_program_props ERTLptr_semantics LTL_semantics
191     (λglobals,fn.«translate_data fix_comp colour globals fn,(refl …)») prog f_bl_r f_lbls f_regs.
192∀st1,st2,f,fn.
193fetch_internal_function ? (globalenv_noinit … prog)
194                (pc_block (pc … st1)) = return 〈f,fn〉 →
195let R ≝ sem_rel … (ERTLptr_to_LTL_StatusSimulation fix_comp colour prog … good) in
196R st1 st2 →
197(pc … st1) = (pc … st2).
198
199(*
200axiom change_pc_sigma_commute : ∀fix_comp,colour.
201∀prog.∀ f_lbls,f_regs.∀f_bl_r.
202∀ good :b_graph_transform_program_props ERTLptr_semantics LTL_semantics
203     (λglobals,fn.«translate_data fix_comp colour globals fn,(refl …)») prog f_bl_r f_lbls f_regs.
204∀st1,st2.
205let R ≝ sem_rel … (ERTLptr_to_LTL_StatusSimulation fix_comp colour prog … good) in
206R st1 st2 →
207∀pc1,pc2.pc1 = pc2 →
208R (set_pc … pc1 st1) (set_pc … pc2 st2).
209
210axiom globals_commute : ∀fix_comp,colour.
211∀prog.
212∀p_out,m,n.
213∀EQp_out: ertlptr_to_ltl fix_comp colour prog = 〈p_out, m, n〉.
214prog_var_names … prog = prog_var_names … p_out.
215
216lemma appoggio : (∀A,B,C : Type[0]. ∀a1,b1 : A.∀a2,b2 : B. ∀a3,b3 : C.
217〈a1,a2,a3〉 = 〈b1,b2,b3〉 → a1 = b1 ∧ a2 = b2 ∧ a3 = b3).
218#H19 #H20 #H21 #H22 #H23 #H24 #H25 #H26 #H27 #H28 destruct % [%] //
219qed.*)
220
221include "joint/semantics_blocks.ma".
222include "ASM/Util.ma".
223
224axiom hw_reg_retrieve_write_decision_hit : ∀r : Register.∀bv : beval.
225∀st : state LTL_LIN_state.
226hw_reg_retrieve (regs … (write_decision r bv st)) r = return bv.
227
228axiom move_spec : ∀prog.∀stack_size.∀localss : nat.
229∀ carry_lives_after : bool.∀dest : decision.∀src : arg_decision.
230∀f : ident.
231∀s : state LTL_LIN_state.
232repeat_eval_seq_no_pc (mk_prog_params LTL_semantics prog stack_size) f
233   (move (prog_var_names … prog) localss carry_lives_after dest src) s =
234   return write_decision dest (read_arg_decision src s) s.
235
236axiom sigma_beval:
237 ertlptr_program → (block → label → list label) → beval → beval.
238 
239
240axiom ps_reg_retrieve_hw_reg_retrieve_commute :
241∀fix_comp,colour,prog.
242∀ f_lbls,f_regs.∀f_bl_r.
243∀ good :b_graph_transform_program_props ERTLptr_semantics LTL_semantics
244 (λglobals,fn.«translate_data fix_comp colour globals fn,(refl …)») prog f_bl_r f_lbls f_regs.
245∀fn : joint_closed_internal_function ERTLptr (prog_var_names … prog).
246let R ≝ sem_rel … (ERTLptr_to_LTL_StatusSimulation fix_comp colour prog … good) in
247let after ≝ (analyse_liveness fix_comp (prog_var_names … prog) fn) in
248∀st1 : state_pc ERTL_state.
249∀st2 : state_pc LTL_LIN_state.
250∀bv.
251∀r : register.R st1 st2 →
252lives (inl ? ? r) (livebefore  … fn (point_of_pc ERTLptr_semantics (pc … st1)) after) →
253ps_reg_retrieve (regs … st1) r = return bv →
254∃bv'.bv = sigma_beval prog f_lbls bv' ∧
255read_arg_decision (colouring after (colour (prog_var_names … prog) fn after)
256                                            (inl register Register r))
257                              st2 = bv'.
258                             
259axiom set_member_empty :∀A.∀DEC.∀a.¬set_member A DEC a (set_empty …).   
260axiom set_member_singl : ∀A,DEC,a.set_member A DEC a (set_singleton … a).
261axiom set_member_union1 : ∀A,DEC,x,y,a.set_member A DEC a x →
262set_member A DEC a (set_union … x y).
263axiom set_member_union2 : ∀A,DEC,x,y,a.set_member A DEC a y →
264set_member A DEC a (set_union … x y).
265axiom set_member_diff : ∀A,DEC,x,y,a.set_member A DEC a x →
266¬set_member A DEC a y →
267set_member A DEC a (set_diff … x y).
268
269lemma all_used_are_live_before :
270∀fix_comp.
271∀prog : ertlptr_program.
272∀fn : joint_closed_internal_function ERTLptr (prog_var_names … prog).
273∀l,stmt.
274stmt_at … (joint_if_code … fn) l = return stmt →
275∀r : register. set_member ? (eq_identifier …) r (\fst (used ? stmt)) →
276let after ≝ (analyse_liveness fix_comp (prog_var_names … prog) fn) in
277eliminable ? (after l) stmt = false →
278lives (inl ? ? r)  (livebefore  … fn l after).
279#fix_comp #prog #fn #l *
280[ * [#c|* [#c_id | #c_ptr] #args #dest | #a #lbl | *
281[ #str
282| * * [#r1 | #R1]  * [1,3: * [1,3: #r |2,4: #R] |2,4: #b]
283| #a
284| * [ #r | #b]
285| #i #i_spec #dpl #dph
286| #op #a #b * [#r | #by]  * [1,3: #r'|2,4: #by']
287| #op #a #a'
288| * #a #a' * [1,3,5,7,9,11: #r |2,4,6,8,10,12: #b]
289|
290|
291| #a #dpl #dph
292| #dpl #dph #a
293| * [ * [|| #r] | #r #lbl | #r #lbl ]
294]
295] #nxt| * [ #lbl | | *] |*]
296#EQstmt #r #H #H1 whd in match (lives ??); normalize  nodelta
297whd in match (livebefore ????); whd in EQstmt : (??%?); >EQstmt
298normalize nodelta -EQstmt whd in match (statement_semantics ???);
299whd in match(\fst ?); try( @(set_member_union2) assumption) >H1
300normalize nodelta whd in match(\fst ?); @(set_member_union2) assumption
301qed.
302
303axiom bool_of_beval_sigma_commute :
304∀prog.∀f_lbls.∀bv,b.
305bool_of_beval (sigma_beval prog f_lbls bv) = return b →
306bool_of_beval bv = return b.
307
308lemma map_eval_add_dummy_variance_id :
309∀X,Y.∀l,x.map_eval X Y (add_dummy_variance X Y l) x =l.
310#X #Y #l elim l [//] #hd #tl normalize #IH #x >IH %
311qed.
312
313lemma state_pc_eq : ∀p.∀st1,st2 : state_pc p.
314st1 = st2 → st_no_pc … st1 = st_no_pc … st2 ∧
315pc … st1 = pc … st2 ∧ last_pop … st1 = last_pop … st2.
316#p * #st1 #pc1 #lp1 * #st2 #pc2 #lp2 #EQ destruct(EQ)
317%{(refl …)} %{(refl …)} %
318qed.
319(*
320axiom dead_is_to_be_clear :
321*)
322
323(* Cut&paste da un altro file con nome split_on_last_append, unificare*)
324lemma split_on_last_append_singl : ∀A : Type[0]. ∀pre : list A.
325∀ last : A. split_on_last ? (pre@[last]) = return 〈pre,last〉.
326#A #pre elim pre [#last %] #a #tl #IH #last whd in ⊢ (??%?);lapply(IH last)
327whd in ⊢ (??%? → ?); #EQ >EQ %
328qed.
329
330lemma split_on_last_append : ∀A : Type[0]. ∀l1,l2: list A.
331 OptPred True (λres.
332  split_on_last ? (l1@l2) = return 〈l1 @ \fst res, \snd res〉)
333  (split_on_last … l2).
334#A #l1 #l2 lapply l1 -l1 @(list_elim_left … l2) //
335#hd #tl #IH #l1 whd >split_on_last_append_singl whd
336<associative_append @split_on_last_append_singl
337qed.
338
339lemma injective_OK: ∀A:Type[0].∀a,b:A. OK … a = OK … b → a=b.
340 #A #a #b #EQ destruct %
341qed.
342
343lemma eq_notb_true_to_eq_false:
344 ∀b. (¬b) = true → b = false.
345* // #abs normalize in abs; destruct
346qed.
347
348axiom sigma_fb_state_insensitive_to_dead_reg:
349 ∀fix_comp,prog,fn,bv. ∀st: state ERTLptr_semantics. ∀l:label.
350 ∀r: register.
351 let live ≝
352  analyse_liveness fix_comp (prog_var_names (joint_function ERTLptr) ℕ prog) fn in
353  set_member (identifier RegisterTag) (eq_identifier RegisterTag) r
354   (\fst  (live l)) = false →
355  sigma_fb_state prog
356   (to_be_cleared_fb live l)
357   (set_regs ERTLptr_semantics
358    〈reg_store r bv (\fst  (regs ERTLptr_semantics st)),
359    \snd  (regs ERTLptr_semantics st)〉 st)
360  = sigma_fb_state prog (to_be_cleared_fb live l) st.
361
362axiom sigma_fb_state_insensitive_to_dead_Reg:
363 ∀fix_comp,prog,fn,bv. ∀st: state ERTLptr_semantics. ∀l:label.
364 ∀r: Register.
365 let live ≝
366  analyse_liveness fix_comp (prog_var_names (joint_function ERTLptr) ℕ prog) fn
367 in
368  set_member Register eq_Register r (\snd  (live l)) = false →
369  sigma_fb_state prog
370   (to_be_cleared_fb live l)
371   (set_regs ERTLptr_semantics
372     〈\fst  (regs ERTLptr_semantics st),
373      hwreg_store r bv (\snd  (regs ERTLptr_semantics st))〉
374      st)
375  = sigma_fb_state prog (to_be_cleared_fb live l) st.
376
377axiom sigma_fb_state_insensitive_to_dead_carry:
378 ∀fix_comp,prog,fn,bv. ∀st: state ERTLptr_semantics. ∀l:label.
379 let live ≝
380  analyse_liveness fix_comp (prog_var_names (joint_function ERTLptr) ℕ prog) fn
381 in
382  set_member Register eq_Register RegisterCarry (\snd (live l)) = false →
383   sigma_fb_state prog (to_be_cleared_fb live l) (set_carry ERTLptr_semantics bv st) =
384   sigma_fb_state prog (to_be_cleared_fb live l) st.
385
386lemma split_orb_false: ∀a,b:bool. orb a b = false → a = false ∧ b = false.
387 ** normalize #abs destruct /2/
388qed.
389
390lemma sigma_fb_state_insensitive_to_eliminable:
391 ∀fix_comp: fixpoint_computer.
392 ∀colour: coloured_graph_computer.
393 ∀prog: ertlptr_program.
394 let p_in ≝
395   mk_prog_params ERTLptr_semantics prog
396   (lookup_stack_cost (\snd  (\fst  (ertlptr_to_ltl fix_comp colour prog)))) in
397 ∀f,fn.
398 ∀st1 : joint_abstract_status p_in.
399 let pt ≝ point_of_pc ERTLptr_semantics (pc ? st1) in
400 ∀st1_no_pc,stms.
401 ∀Heval_seq_no_pc:
402   eval_seq_no_pc ERTLptr_semantics
403   (prog_var_names (joint_function ERTLptr_semantics) ℕ prog)
404   (ev_genv
405    (mk_prog_params ERTLptr_semantics prog
406     (lookup_stack_cost (\snd  (\fst  (ertlptr_to_ltl fix_comp colour prog))))))
407   f stms (st_no_pc … st1)
408   =return st1_no_pc.
409 ∀Heliminable:
410   eliminable_step (globals p_in)
411   (analyse_liveness fix_comp (globals p_in) fn
412    (point_of_pc ERTLptr_semantics (pc p_in st1))) stms
413   =true.
414 (sigma_fb_state prog
415  (to_be_cleared_fb
416   (analyse_liveness fix_comp (prog_var_names (joint_function ERTLptr) ℕ prog)
417    fn) pt)
418  st1_no_pc
419  =sigma_fb_state prog
420   (to_be_cleared_fb
421    (analyse_liveness fix_comp (prog_var_names (joint_function ERTLptr) ℕ prog)
422     fn) pt)
423   (st_no_pc … st1)).
424#fix_comp #colour #prog letin p_in ≝ (mk_prog_params ???) #f #fn
425#st1 #st1' *
426try (#arg1 #arg2 #arg3 #arg4 #arg5 #Heval #Helim)
427try (#arg1 #arg2 #arg3 #arg4 #Heval #Helim)
428try (#arg1 #arg2 #arg3 #Heval #Helim) try (#arg1 #arg2 #Heval #Helim)
429try (#arg1 #Heval #Helim) try (#Heval #Helim)
430whd in Heval:(??%?);
431whd in Helim:(??%?); try (change with (false=true) in Helim; destruct (Helim))
432[7: inversion arg1 in Heval Helim; [ * [3: #arg2 ] |*: #arg2 #arg3 ] #Harg1
433    normalize nodelta ] try #Heval try #Helim whd in Heval:(??%?);
434    try (change with (false=true) in Helim; destruct (Helim))
435    [4,8: cases arg1 in Heval Helim; normalize nodelta
436      [ * normalize nodelta #arg10 #arg11] #Heval #Helim]
437lapply (eq_notb_true_to_eq_false ? Helim) -Helim #Helim
438[1,2: cases arg11 in Heval; [1,3: *] #arg12 whd in ⊢ (??%? → ?);
439  [1,3: whd in match (pair_reg_move_ ?????); normalize nodelta
440        inversion ps_reg_retrieve normalize nodelta
441        [2,4: #error #_ #abs whd in abs:(???%); destruct (abs) ]
442        #bv #EQbv ]
443|3,4,5,6,7,8,13: inversion (acca_arg_retrieve ERTLptr_semantics) in Heval;
444    [2,4,6,8,10,12,14: #error #_ #abs whd in abs:(??%%); destruct (abs) ]
445    #bv normalize nodelta #EQbv #X cases (bind_inversion ????? X) -X
446    #v1 * #Hv1 #X cases (bind_inversion ????? X) -X
447    #vres * #Hvres #X cases (bind_inversion ????? X) -X
448    #st1'' * #Hst1''
449|9: inversion (opt_to_res ???) in Heval;
450    [2: #error #_ #abs whd in abs:(??%%); destruct (abs) ]
451    #bv normalize nodelta #EQbv
452|10,11: inversion (get_pc_from_label ?????) in Heval;
453     [2,4: #error #_ #abs whd in abs:(??%%); destruct (abs) ]
454     #bv normalize nodelta #EQbv
455|12: lapply Heval -Heval
456|14: inversion (acca_retrieve ???) in Heval;
457    [2: #error #_ #abs whd in abs:(??%%); destruct (abs) ]
458    #bv normalize nodelta #EQbv #X cases (bind_inversion ????? X) -X
459    #v1 * #Hv1
460|15: inversion (dph_arg_retrieve ???) in Heval;
461    [2: #error #_ #abs whd in abs:(??%%); destruct (abs) ]
462    #bv normalize nodelta #EQbv #X cases (bind_inversion ????? X) -X
463    #v1 * #Hv1 #X cases (bind_inversion ????? X) -X
464    #vres * #Hvres #X cases (bind_inversion ????? X) -X
465    #v1 * #Hv2 ]
466whd in ⊢ (??%% → ?); #X <(injective_OK ??? X) -X
467try (cases (split_orb_false … Helim) -Helim #Helim1 #Helim2)
468try (@sigma_fb_state_insensitive_to_dead_reg assumption)
469try (@sigma_fb_state_insensitive_to_dead_Reg assumption)
470try (@sigma_fb_state_insensitive_to_dead_carry assumption)
471[1,2,3,4,5,6,7: <(injective_OK ??? Hst1'') ]
472[1,2,3:
473  >sigma_fb_state_insensitive_to_dead_carry try assumption
474  @sigma_fb_state_insensitive_to_dead_reg assumption
475|4,5,6: (* BUG! *)
476|7: >sigma_fb_state_insensitive_to_dead_reg try assumption
477
478lemma make_ERTLptr_To_LTL_good_state_relation :
479∀fix_comp,colour,prog.
480let p_out ≝ (\fst (\fst (ertlptr_to_ltl fix_comp colour prog))) in
481let m ≝ (\snd (\fst (ertlptr_to_ltl fix_comp colour prog))) in
482let n ≝ \snd (ertlptr_to_ltl fix_comp colour prog) in
483let stacksizes ≝ lookup_stack_cost … m in
484∃init_regs : block → list register.
485∃f_lbls : block → label → list label.
486∃f_regs : block → label → list register.
487∃good : b_graph_transform_program_props ERTLptr_semantics LTL_semantics
488        (λglobals,fn.«translate_data fix_comp colour globals fn,(refl …)»)
489        prog init_regs f_lbls f_regs.
490good_state_relation ERTLptr_semantics LTL_semantics prog stacksizes
491 (λglobals,fn.«translate_data fix_comp colour globals fn,(refl …)»)
492 init_regs f_lbls f_regs good (state_rel fix_comp colour prog f_lbls f_regs)
493 (sem_rel … (ERTLptr_to_LTL_StatusSimulation fix_comp colour prog … good)).
494#fix_comp #colour #prog
495cases(make_b_graph_transform_program_props ERTLptr_semantics LTL_semantics
496          (λglobals,fn.«translate_data fix_comp colour globals fn,(refl …)») prog)
497#init_regs * #f_lbls * #f_regs #good %{init_regs} %{f_lbls} %{f_regs} %{good}
498%
499[ #st1 #st2 #f #fn whd in ⊢ (% → ?); #REL lapply REL whd in match sigma_fb_state_pc;
500  whd in match sigma_sb_state_pc; normalize nodelta #EQ #EQfn >EQfn in EQ;
501  normalize nodelta <(pc_eq_sigma_commute  … good … EQfn REL) >EQfn
502  normalize nodelta #H cases(state_pc_eq … H) * #H1 #_ #_ whd %{f} %{fn} %{EQfn}
503  assumption
504| #st1 #st2 #f #fn #Rst1st2 #EQfetcn >(pc_eq_sigma_commute … good … EQfetcn Rst1st2) %
505| #st1 #st2 #f #fn whd in ⊢ (% → ?); #REL lapply REL whd in match sigma_fb_state_pc;
506  whd in match sigma_sb_state_pc; normalize nodelta #EQ #EQfn >EQfn in EQ;
507  normalize nodelta <(pc_eq_sigma_commute  … good … EQfn REL) >EQfn normalize nodelta
508   #H cases(state_pc_eq … H) * #_ #_ //
509| #st1 #st2 #pc #lp1 #lp2 #f #fn #EQfn * #f1 * #fn1 * >EQfn whd in ⊢ (??%% → ?);
510  #EQ destruct(EQ) normalize nodelta #state_rel #EQ destruct(EQ) whd
511  whd in match sigma_fb_state_pc; whd in match sigma_sb_state_pc; normalize nodelta
512  >EQfn >EQfn normalize nodelta //
513| #st1 #st2 #f #fn #stmt #EQstmt #Rst1St2 >(as_label_ok … good … Rst1St2 EQstmt) %
514| normalize nodelta whd in ⊢ (% → % → % → ?); #st1 #st1' #st2 #f #fn #a #ltrue #lfalse
515  #EQfetch whd in match eval_state in ⊢ (% → ?); whd in match eval_statement_no_pc;
516  normalize nodelta >EQfetch >m_return_bind normalize nodelta >m_return_bind
517  whd in match eval_statement_advance; normalize nodelta
518  change with (ps_reg_retrieve ??) in match (acca_retrieve ?????);
519  #H lapply(err_eq_from_io ????? H) -H #H @('bind_inversion H) -H
520  #bv >set_no_pc_eta #EQbv #H @('bind_inversion H) -H * #EQbool normalize nodelta
521  cases(fetch_statement_inv … EQfetch) #EQfn #EQstmt
522  [ whd in match goto; normalize nodelta >(pc_of_label_eq … EQfn)
523    >m_return_bind ] whd in ⊢ (??%% → ?); #EQ destruct(EQ) #Rst1st2
524  #t_fn1 #EQt_fn1 whd normalize nodelta
525  letin trans_prog ≝ (b_graph_transform_program ????)
526  letin stacksizes ≝ (lookup_stack_cost ?)
527  letin prog_pars_in ≝ (mk_prog_params ERTLptr_semantics ??)
528  letin prog_pars_out ≝ (mk_prog_params LTL_semantics ??) %{(refl …)}
529  #mid #EQmid
530  letin st2_pre_mid_no_pc ≝
531  (write_decision RegisterA
532          (read_arg_decision
533              (colouring
534                  (analyse_liveness fix_comp (globals prog_pars_in) fn)
535                  (colour (globals prog_pars_in) fn
536                  (analyse_liveness fix_comp (globals prog_pars_in) fn))
537              (inl register Register a)) st2) st2)
538  %{st2_pre_mid_no_pc}
539  %
540  [1,3: >map_eval_add_dummy_variance_id %
541       [1,3: %
542            [1,3: %
543                 [1,3: @move_spec
544                 |*: lapply Rst1st2 whd in ⊢ (% → ?); whd in match sigma_fb_state_pc;
545                     whd in match sigma_sb_state_pc; normalize nodelta >EQfn
546                     <(pc_eq_sigma_commute … good … EQfn Rst1st2) >EQfn
547                     normalize nodelta #EQ cases(state_pc_eq … EQ) *
548                     #EQst1st2 #_ #_ whd %{f} %{fn} %{EQfn}
549                     <(insensitive_to_be_cleared_sb … prog f_lbls f_regs … st2 …
550                                          (point_of_pc ERTLptr_semantics (pc … st2)))
551                     [2,4: @dead_registers_in_dead @acc_is_dead ]
552                     assumption
553                 ]
554            |*: %
555            ]
556       |*: %
557       ]
558  |*: change with (hw_reg_retrieve ??) in match (acca_retrieve ?????);
559      >hw_reg_retrieve_write_decision_hit >m_return_bind
560      cases(ps_reg_retrieve_hw_reg_retrieve_commute fix_comp colour prog …
561                                                        good fn … Rst1st2 … EQbv)
562        [2,4: @(all_used_are_live_before … EQstmt)
563            [1,3: @set_member_singl |*: % ] ] #bv' * #EQbv' #EQbv1
564        change with (prog_var_names … prog) in match (globals ?); >EQbv1
565        >EQbv' in EQbool; #EQbool
566        >(bool_of_beval_sigma_commute prog f_lbls … EQbool) >m_return_bind
567        normalize nodelta
568        [2: <(pc_eq_sigma_commute … good … EQfn Rst1st2) %]
569        whd in match goto; normalize nodelta
570        >(pc_of_label_eq … EQt_fn1) <(pc_eq_sigma_commute … good … EQfn Rst1st2) %
571  ]
572| letin p_in ≝ (mk_prog_params ERTLptr_semantics ??)
573  letin p_out ≝ (mk_prog_params LTL_semantics ??)
574  letin trans_prog ≝ (b_graph_transform_program ????)
575  #st1 #st1' #st2 #f #fn
576  #stms #nxt #EQfetch whd in match eval_state in ⊢ (% → ?);
577  normalize nodelta >EQfetch >m_return_bind #H @('bind_inversion H) -H
578  #st1_no_pc whd in match eval_statement_no_pc in ⊢ (% → ?); normalize nodelta
579  #Heval_seq_no_pc
580  whd in match eval_statement_advance; normalize nodelta
581  whd in ⊢ (??%% → ?); #EQ destruct(EQ)
582  whd in ⊢ (% → ?); #Rst1st2 #t_fn #EQt_fn
583  whd normalize nodelta
584  change with p_out in match p_out;
585  change with p_in in match p_in;
586  change with trans_prog in match trans_prog;
587  inversion eliminable_step #Heliminable normalize nodelta %
588  [ @([ ])
589  | % [%] % [2: % [%] | skip] whd
590    cases(fetch_statement_inv … EQfetch) #EQfn #EQstmt >EQfn
591    % [2: % [2: % [%] | skip] | skip]
592    (* CSC: BEGIN cut&paste from previous case: make lemma? *)
593    lapply Rst1st2 whd in ⊢ (% → ?); whd in match sigma_fb_state_pc;
594    whd in match sigma_sb_state_pc; normalize nodelta >EQfn
595    <(pc_eq_sigma_commute … good … EQfn Rst1st2) >EQfn
596    normalize nodelta #EQ cases(state_pc_eq … EQ) *
597    #EQst1st2 #_ #_
598    (* CSC: END *)
599    <EQst1st2 whd in EQst1_no_pc:(??%%); whd in match (st_no_pc ??);
600
601
602       
603       
604       
605        <(injective_OK ??? EQst1_no_pc)
606        change with (set_regs ???) in match (st_no_pc ??);
607 
608 
609  *
610  [7: #op1 #dest #src #nxt #EQfetch whd in match eval_state in ⊢ (% → ?);
611      normalize nodelta >EQfetch >m_return_bind #H @('bind_inversion H) -H
612      #st1_no_pc whd in match eval_statement_no_pc in ⊢ (% → ?); normalize nodelta
613      whd in match eval_seq_no_pc; normalize  nodelta
614      #H lapply(err_eq_from_io ????? H) -H #H @('bind_inversion H) -H
615      #bv #EQbv #H @('bind_inversion H) -H #bv_op1 #EQbv_op1 #EQst1_no_pc
616      whd in match eval_statement_advance; normalize nodelta
617      whd in ⊢ (??%% → ?); #EQ destruct(EQ)
618      whd in ⊢ (% → ?); #Rst1st2 #t_fn #EQt_fn
619      whd normalize nodelta whd in match translate_op1;
620      normalize nodelta
621      change with p_out in match p_out;
622      change with p_in in match p_in;
623      change with trans_prog in match trans_prog;
624      inversion eliminable_step #Heliminable normalize nodelta %
625      [ @([ ])
626      | % [%] % [2: % [%] | skip] whd
627        cases(fetch_statement_inv … EQfetch) #EQfn #EQstmt >EQfn
628        % [2: % [2: % [%] | skip] | skip]
629        (* CSC: BEGIN cut&paste from previous case: make lemma? *)
630        lapply Rst1st2 whd in ⊢ (% → ?); whd in match sigma_fb_state_pc;
631        whd in match sigma_sb_state_pc; normalize nodelta >EQfn
632        <(pc_eq_sigma_commute … good … EQfn Rst1st2) >EQfn
633        normalize nodelta #EQ cases(state_pc_eq … EQ) *
634        #EQst1st2 #_ #_
635        (* CSC: END *)
636        <EQst1st2 whd in EQst1_no_pc:(??%%); <(injective_OK ??? EQst1_no_pc)
637        change with (set_regs ???) in match (st_no_pc ??);
638
639       
640       
641       
642       
643       
644       
645       
646         destruct (EQst1_no_pc)
647       
648        <(insensitive_to_be_cleared_sb … prog f_lbls f_regs … st2 …
649          (point_of_pc ERTLptr_semantics (pc … st2)))
650                     [2,4: @dead_registers_in_dead @acc_is_dead ]
651                     assumption
652     
653      Rst1st2
654     
655      % [2: % [ % | ] | skip]
656qed.
657
658
659lemma eval_cond_ok :
660∀fix_comp,colour.
661∀prog.
662∀ f_lbls,f_regs.∀f_bl_r.
663∀ good :b_graph_transform_program_props ERTLptr_semantics LTL_semantics
664     (λglobals,fn.«translate_data fix_comp colour globals fn,(refl …)») prog f_bl_r f_lbls f_regs.
665∀st1,st2,st1',f,fn,a,ltrue,lfalse.
666let R ≝ sem_rel … (ERTLptr_to_LTL_StatusSimulation fix_comp colour prog … good) in
667R st1 st2 →
668 fetch_statement ERTLptr_semantics …
669  (globalenv_noinit ? prog) (pc … st1) =
670    return 〈f, fn,  sequential … (COND ERTLptr … a ltrue) lfalse〉 →
671let stacksizes ≝ lookup_stack_cost …
672                  (\snd (\fst (ertlptr_to_ltl fix_comp colour prog))) in 
673 eval_state ERTLptr_semantics
674   (prog_var_names … ℕ prog)
675   (ev_genv … (mk_prog_params ERTLptr_semantics prog stacksizes))
676   st1 = return st1' →
677as_costed (ERTLptr_status prog stacksizes) st1' →
678∃ st2'. R st1' st2' ∧
679∃taf : trace_any_any_free (LTL_status ? ?)
680st2 st2'.
681bool_to_Prop (taaf_non_empty … taf).
682#fix_comp #colour #prog #f_lbls #f_regs #f_bl_r #good #st1 #st2 #st1' #f #fn #a
683#ltrue #lfalse #Rst1st2 #EQfetch #EQeval
684letin R ≝ (sem_rel … (ERTLptr_to_LTL_StatusSimulation fix_comp colour prog … good))
685@(general_eval_cond_ok … good … Rst1st2 EQfetch EQeval)
686%
687[ #st1 #st2 #Rst1St2 >(pc_eq_sigma_commute … good … Rst1St2) %
688| #st1 #st2 #f #fn #stmt #EQstmt #Rst1St2 >(as_label_ok … good … Rst1St2 EQstmt) %
689|
690
691
692
693whd in match eval_state; normalize nodelta
694>EQfetch >m_return_bind
695whd in match eval_statement_no_pc; normalize nodelta >m_return_bind
696whd in match eval_statement_advance; normalize nodelta
697change with (ps_reg_retrieve ??) in match (acca_retrieve ?????);
698#H lapply(err_eq_from_io ????? H) -H #H @('bind_inversion H) -H
699#bv >set_no_pc_eta #EQbv #H @('bind_inversion H) -H * #EQbool normalize nodelta
700lapply(fetch_statement_inv … EQfetch) * #EQfn #_
701[ whd in match goto; normalize nodelta >(pc_of_label_eq ??????? EQfn) >m_return_bind
702| whd in match next; normalize nodelta
703]
704whd in ⊢ (??%% → ?); #EQ lapply(eq_OK_OK_to_eq ??? EQ) -EQ #EQst1' #n_cost
705cases(b_graph_transform_program_fetch_statement … good … EQfetch)
706#init_data * #t_fn1 ** #EQt_fn1 whd in ⊢ (% → ?); cases (f_bl_r ?) normalize nodelta
707[2,4: #r #tl *] #EQ >EQ -init_data >if_merge_right in ⊢ (% → ?); [2,4: %] * #labs **
708[2,4: #hd #tl ** #_ #_ *** #pre #inst #post * whd in ⊢ (%→?); *] ** #EQlabs #EQf_regs
709whd in match translate_step; normalize nodelta *** #blp #blm #bls *
710whd in ⊢ (% → ?); #EQbl
711whd in ⊢ (% → ?); * #l1 * #mid1 * #mid2 * #l2 *** #EQmid1 whd in ⊢ (% → ?);
712#seq_pre_l
713letin stacksizes ≝ (lookup_stack_cost …
714                  (\snd (\fst (ertlptr_to_ltl fix_comp colour prog))))
715letin p≝ (mk_prog_params LTL_semantics
716                         (\fst (\fst (ertlptr_to_ltl fix_comp colour prog)))
717                         stacksizes)
718cases(? : ∃st2'.repeat_eval_seq_no_pc p f (map_eval ?? blp mid1) (st_no_pc … st2) = return (st_no_pc … st2') ∧
719           pc … st2' = (pc_of_point LTL_semantics (pc_block (pc … st2)) mid1) ∧
720           last_pop … st2' = last_pop … st2)
721   [2,4: cases daemon (* THE EXTENSIONAL PROOF *) ]
722#st2_pre_mid ** #res_st2_pre_mid #EQpc_st2_pre_mid #EQlast_pop_st2_pre_mid
723>(pc_block_eq_sigma_commute … good … Rst1st2) in EQt_fn1; #EQt_fn1
724>(pc_eq_sigma_commute … good … Rst1st2) in seq_pre_l; #seq_pre_l
725whd in ⊢ (% → ?); * #nxt1 * #EQmid change with nxt1 in ⊢ (??%? → ?); #EQ
726>EQ in EQmid ⊢ %; -nxt1 #EQmid
727lapply(taaf_to_taa ???
728           (produce_trace_any_any_free p st2 f t_fn1 ??? st2_pre_mid EQt_fn1
729                                       seq_pre_l res_st2_pre_mid) ?)
730[1,3: @if_elim #_ [2,4: @I] % whd in match as_costed; normalize nodelta
731      whd in match (as_label ??); whd in match (as_pc_of ??);
732      whd in match fetch_statement; normalize nodelta * #H @H -H >EQt_fn1
733      >m_return_bind whd in match point_of_pc; normalize nodelta
734      >point_of_offset_of_point >EQmid >m_return_bind normalize nodelta
735      cases(appoggio ????????? EQbl) cases daemon (*PASSED DEPENDANT * #_ #EQ1 #_ >EQ1 % *) ]
736#taa_pre_mid whd in ⊢ (% → ?);
737cases(? : ∃st2_cond. eval_state LTL_semantics (globals p) (ev_genv … p) st2_pre_mid =
738                     return st2_cond )
739[2,4: cases daemon (*THE EXTENSIONAL PROOF *)]
740#st2_mid #EQst2_mid
741cut(bls = [ ] ∧ as_classify (joint_abstract_status p) st2_pre_mid = cl_jump)
742[1,3: cases daemon (*PASSED DEPENDANT *)] * #EQbls #CL_JUMP >EQbls whd in ⊢ (% → ?);
743* #EQ1 #EQ2 >EQ1 in EQmid1; #EQmid1 -l2 >EQ2 in seq_pre_l EQmid; -mid2 #seq_pre_l #EQmid
744letin R ≝ (sem_rel … (ERTLptr_to_LTL_StatusSimulation fix_comp colour prog … good))
745cut(R st1' st2_mid) [1,3: cases daemon (*PASSED DEPENDANT*)] #Rst1_st2_mid
746%{st2_mid} % [1,3: assumption ] %{(taaf_step_jump ? ??? taa_pre_mid ???) I}
747[1,4: whd >(as_label_ok … fix_comp colour … good … Rst1_st2_mid) [1,6: assumption]
748     cases daemon (*TODO see also ERTL_to_ERTLptrOK proof! *)
749|*: <EQpc_st2_pre_mid <EQlast_pop_st2_pre_mid assumption
750]
751qed.
752
753
754theorem ERTLptrToLTL_ok :
755∀fix_comp : fixpoint_computer.
756∀colour : coloured_graph_computer.
757∀p_in : ertlptr_program.
758let p_out ≝ (\fst (\fst (ertlptr_to_ltl fix_comp colour p_in))) in
759let m ≝ (\snd (\fst (ertlptr_to_ltl fix_comp colour p_in))) in
760let n ≝ \snd (ertlptr_to_ltl fix_comp colour p_in) in
761(* what should we do with n? *)
762let stacksizes ≝ lookup_stack_cost m in
763∃[1] R.
764  status_simulation
765    (joint_status ERTLptr_semantics p_in stacksizes)
766    (joint_status LTL_semantics p_out stacksizes)
767    R.
768#fix_comp #colour #p_in
769cases(make_b_graph_transform_program_props ERTLptr_semantics LTL_semantics
770          (λglobals,fn.«translate_data fix_comp colour globals fn,(refl …)») p_in)
771#fregs * #f_lbls * #f_bl_r #good
772%{(ERTLptr_to_LTL_StatusSimulation fix_comp colour p_in … good)}
773whd in match status_simulation; normalize nodelta
774whd in match ERTLptr_status; whd in match LTL_status; normalize nodelta
775whd in ⊢ (% → % → % → % → ?); #st1 #st1' #st2
776change with
777  (eval_state ERTLptr_semantics (prog_var_names ???) ?? = ? → ?) 
778#EQeval @('bind_inversion EQeval)
779** #id #fn #stmt #H lapply (err_eq_from_io ????? H) -H #EQfetch
780#_  whd in match ERTLptr_to_LTL_StatusSimulation; normalize nodelta #EQst2
781cases stmt in EQfetch; -stmt
782[ * [ #cost | #called_id #args #dest| #reg #lbl | #seq] #nxt | #fin_step | *]
783#EQfetch
784change with (joint_classify ??) in
785                     ⊢ (match % with [ _ ⇒ ? | _ ⇒ ? | _ ⇒ ? | _ ⇒ ? | _ ⇒ ? ]);
786[ (*COST*) whd in match joint_classify; normalize nodelta >EQfetch normalize nodelta
787  (* XXX
788  cases(eval_cost_ok … good … EQfetch EQeval) #st2' * #EQst2' * #taf #tafne
789  %{st2'} %{taf} >tafne normalize nodelta % [ % [@I | assumption]]
790  whd >EQst2' >(as_label_ok … good … st2') [%] cases daemon (* needs lemma see below!! *)
791  *) cases daemon
792| (*CALL*)  whd in match joint_classify; normalize nodelta >EQfetch
793          normalize nodelta #is_call_st1
794          (* XXX
795          cases(eval_call_ok … good … EQfetch EQeval) #is_call_st1'
796          * #st2_pre_call * #is_call_st2_pre_call * * #Hcall
797          #call_rel * #taa * #st2' * #sem_rel #eval_rel
798          %{(«st2_pre_call,is_call_st2_pre_call»)} % [ % assumption]
799          %{st2'} %{st2'} %{taa} %{(taa_base …)} % [ % assumption]
800          whd >sem_rel >(as_label_ok … good … st2') [%] cases daemon (*TODO*)
801          *) cases daemon
802| (*COND*) whd in match joint_classify; normalize nodelta >EQfetch
803          normalize nodelta #n_costed
804          cases(eval_cond_ok  … good … EQst2 … EQfetch EQeval … n_costed)
805          #st2' * #EQst2' * #taf #tafne %{st2'} %{taf} >tafne % [% [@I|assumption]]
806          whd >EQst2' >(as_label_ok fix_comp colour … good … EQst2') [%] cases daemon (*TODO*)
807| (*seq*) XXX whd in match joint_classify; normalize nodelta >EQfetch
808          normalize nodelta
809          cases (eval_seq_no_call_ok … good … EQfetch EQeval)
810          #st3 * #EQ destruct *  #taf #taf_spec %{st3} %{taf} 
811          % [% //] whd >(as_label_ok … good … st3) [%]
812          cases daemon (*needs lemma about preservation of fetch_statement *)
813|  cases fin_step in EQfetch;
814  [ (*GOTO*) #lbl #EQfetch  whd in match joint_classify; normalize nodelta
815     >EQfetch normalize nodelta
816    cases (eval_goto_ok … good  … EQfetch EQeval)
817    #st3 * #EQ destruct * #taf #tarne %{st3} %{taf} >tarne normalize nodelta
818    % [% //] whd >(as_label_ok … good … st3) [%]
819    cases daemon (*needs lemma about preservation of fetch_statement *)
820  | (*RETURN*) #EQfetch
821     whd in match joint_classify; normalize nodelta
822    >EQfetch  normalize nodelta
823    cases (eval_return_ok … good … EQfetch EQeval) #is_ret
824    * #st3 * #EQ destruct * #after_ret * #taf ** #taf_prf #EQeval' #ret_prf
825    % [2: % [2: % [2: %{(taa_base …)} %{taf}] |*: ] |*:]
826    % [2: whd >(as_label_ok … good … st3) [%] cases daemon (*needs lemma *)]
827    % [2: assumption] % [2: %] % [2: assumption] % assumption
828  | (*TAILCALL*) *
829  ]
830]
831
Note: See TracBrowser for help on using the repository browser.