source: src/ERTLptr/ERTLtoERTLptrOK.ma @ 2638

Last change on this file since 2638 was 2638, checked in by piccolo, 7 years ago

Back-end fixes for last Garnier's commit that removes the regions from
the blocks. Only part of the back-end has been fixed.

File size: 116.7 KB
Line 
1
2(**************************************************************************)
3(*       ___                                                              *)
4(*      ||M||                                                             *)
5(*      ||A||       A project by Andrea Asperti                           *)
6(*      ||T||                                                             *)
7(*      ||I||       Developers:                                           *)
8(*      ||T||         The HELM team.                                      *)
9(*      ||A||         http://helm.cs.unibo.it                             *)
10(*      \   /                                                             *)
11(*       \ /        This file is distributed under the terms of the       *)
12(*        v         GNU General Public License Version 2                  *)
13(*                                                                        *)
14(**************************************************************************)
15
16include "ERTLptr/ERTLtoERTLptr.ma".
17include "common/StatusSimulation.ma".   
18include "joint/Traces.ma".
19include "ERTLptr/ERTLptr_semantics.ma".
20include "common/ExtraMonads.ma".
21
22definition ERTL_status ≝
23λprog : ertl_program.λstack_sizes.
24joint_abstract_status (mk_prog_params ERTL_semantics prog stack_sizes).
25
26definition ERTLptr_status ≝
27λprog : ertlptr_program.λstack_sizes.
28joint_abstract_status (mk_prog_params ERTLptr_semantics prog stack_sizes).
29
30definition sigma_map ≝ λ prog : ertl_program.
31joint_closed_internal_function ERTL (prog_var_names … prog) → label → option label.
32
33
34definition sigma_pc_opt :
35∀ prog : ertl_program.
36sigma_map prog → program_counter → option program_counter ≝
37λprog,sigma,pc.
38  let ge ≝ globalenv_noinit … prog in
39  if eqZb       (block_id (pc_block pc)) (-1) then (* check for dummy exit pc *)
40    return pc
41  else
42    ! 〈i, fd〉 ← res_to_opt … (fetch_internal_function … ge (pc_block pc)) ;
43    ! ertl_ptr_point ← sigma fd (point_of_pc ERTL_semantics pc) ;
44    return pc_of_point
45    ERTLptr_semantics (pc_block pc) ertl_ptr_point.
46
47definition sigma_stored_pc ≝
48λprog,sigma,pc. match sigma_pc_opt prog sigma pc with
49      [None ⇒ null_pc (pc_offset … pc) | Some x ⇒ x].
50     
51     
52definition sigma_beval :
53 ∀prog : ertl_program.
54  sigma_map prog →
55  beval → beval ≝
56λprog,sigma,bv.
57match bv with
58[ BVpc pc prt ⇒ match sigma_pc_opt prog sigma pc with
59                 [None ⇒ BVundef | Some x ⇒ BVpc x prt]
60| _ ⇒ bv
61].
62
63(*
64definition sigma_beval :
65 ∀prog,sigma,bv.
66 sigma_beval_opt prog sigma bv ≠ None ? → beval ≝
67 λprog,sigma,bv.opt_safe ….
68*)
69definition sigma_is :
70 ∀prog : ertl_program.
71  sigma_map prog →
72  internal_stack → internal_stack ≝
73λprog,sigma,is.
74match is with
75[ empty_is ⇒ empty_is
76| one_is bv ⇒ one_is (sigma_beval prog sigma bv)
77| both_is bv1 bv2 ⇒
78  both_is (sigma_beval prog sigma bv1) (sigma_beval prog sigma bv2)
79].
80
81lemma sigma_is_empty : ∀prog,sigma.
82  sigma_is prog sigma empty_is = empty_is.
83#prog #sigma %
84qed.
85
86(*
87lemma sigma_is_pop_commute :
88 ∀prog,sigma,is,bv,is'.
89 is_pop (sigma_is prog sigma is) =
90       return 〈sigma_beval prog sigma bv,sigma_is prog sigma is'〉 →
91 is_pop is = return 〈bv,is'〉.
92 
93 
94 ∀prf : sigma_is_opt prog sigma is ≠ None ?.
95 res_preserve …
96  (λpr.sigma_beval_opt prog sigma (\fst pr) ≠ None ? ∧
97       sigma_is_opt prog sigma (\snd pr) ≠ None ?)
98  (λpr,prf.〈sigma_beval … (proj1 … prf), sigma_is … (proj2 … prf)〉)
99  (is_pop is) (is_pop (sigma_is … prf)).
100#prog #sigma * [|#bv1|#bv1 #bv2] #prf
101[ @res_preserve_error
102|*:
103 whd in match sigma_is in ⊢ (?????????%); normalize nodelta
104 @opt_safe_elim #is'
105  #H @('bind_inversion H) -H #bv1' #EQ1
106  [2: #H @('bind_inversion H) -H #bv2' #EQ2 ]
107 whd in ⊢ (??%%→?); #EQ destruct(EQ)
108 @mfr_return_eq
109 [1,3: @hide_prf %%
110 |*: whd in match sigma_beval; whd in match sigma_is;
111  normalize nodelta @opt_safe_elim #bv1'' @opt_safe_elim #is''
112 ]
113 [2,4,5,6: whd in match sigma_is_opt; normalize nodelta [1,3: >EQ1 ]
114  whd in ⊢ (??%%→?); #EQ destruct(EQ) ]
115 [1,3: >EQ2 |*: >EQ1 ] #EQ' destruct(EQ') %
116]
117qed.
118
119definition well_formed_mem :
120 ∀prog : ertl_program.
121  sigma_map prog →
122 bemem → Prop ≝
123λprog,sigma,m.
124∀b,z.block_id b < nextblock m → low_bound m b ≤ z → z < high_bound m b →
125  sigma_beval_opt prog sigma (contents (blocks m b) z) ≠ None ?.
126*)
127
128
129definition sigma_mem :
130 ∀prog : ertl_program . sigma_map prog → bemem → bemem ≝
131 λprog,sigma,m.
132 mk_mem
133  (λb.
134    If Zltb (block_id b) (nextblock m) then with prf' do   
135      let l ≝ low_bound m b in
136      let h ≝ high_bound m b in
137      mk_block_contents l h
138      (λz.If Zleb l z ∧ Zltb z h then with prf'' do
139        sigma_beval prog sigma (contents (blocks m b) z)
140      else BVundef)
141    else empty_block OZ OZ)
142  (nextblock m)
143  (nextblock_pos m).
144(*
145@hide_prf
146lapply prf'' lapply prf' -prf' -prf''
147@Zltb_elim_Type0 [2: #_ * ]
148#bid_ok *
149@Zleb_elim_Type0 [2: #_ * ]
150@Zltb_elim_Type0 [2: #_ #_ * ]
151#zh #zl * @(prf … bid_ok zl zh)
152qed.
153*)
154
155(*DOPPIONI DEI CORRISPONDENTI LEMMI IN LINEARISE_PROOF.MA *)
156(*lemma andb_false : ∀b1,b2.andb b1 b2 = false → b1 = false ∨ b2 = false.
157** /2 by or_introl, or_intror/ normalize #ABS destruct(ABS) qed.
158*)
159
160axiom mem_ext_eq :
161  ∀m1,m2 : mem.
162  (∀b.let bc1 ≝ blocks m1 b in
163      let bc2 ≝ blocks m2 b in
164      low bc1 = low bc2 ∧ high bc1 = high bc2 ∧
165      ∀z.contents bc1 z = contents bc2 z) →
166  nextblock m1 = nextblock m2 → m1 = m2.
167
168(*
169
170lemma beloadv_sigma_commute:
171∀prog,sigma,ptr.
172preserving … opt_preserve …
173 (sigma_mem prog sigma)
174 (sigma_beval prog sigma)
175 (λm.beloadv m ptr)
176 (λm.beloadv m ptr).
177#prog  #sigma #ptr #m #prf #bv
178whd in match beloadv;
179whd in match do_if_in_bounds;
180whd in match sigma_mem;
181normalize nodelta
182@If_elim #block_ok >block_ok normalize nodelta
183[2: whd in ⊢ (???%→?); #ABS destruct(ABS) ]
184@If_elim #H
185[ elim (andb_true … H)
186  #H1 #H2
187  whd in match sigma_beval; normalize nodelta
188  @opt_safe_elim #bv' #EQ_bv' >H1 >H2 normalize nodelta
189  whd in ⊢ (???%→?); #EQ' destruct
190  >EQ_bv' % [ % #ABS destruct(ABS) ] @opt_to_opt_safe
191| elim (andb_false … H) -H #H >H
192  [2: >commutative_andb ] normalize nodelta
193  whd in ⊢ (???%→?); #ABS destruct(ABS)
194]
195qed.
196
197include alias "common/GenMem.ma".
198
199lemma bestorev_sigma_commute :
200∀prog,sigma,ptr.
201preserving2 ?? opt_preserve …
202  (sigma_mem prog sigma)
203  (sigma_beval prog sigma)
204  (sigma_mem prog sigma)
205  (λm.bestorev m ptr)
206  (λm.bestorev m ptr).
207#prog #sigma #ptr #m #bv #prf1 #prf2 #m'
208whd in match bestorev;
209whd in match do_if_in_bounds;
210whd in match sigma_mem;
211whd in match update_block;
212 normalize nodelta
213@If_elim #block_ok >block_ok normalize nodelta
214[2: whd in ⊢ ((???%) → ?); #ABS destruct(ABS)]
215@Zleb_elim_Type0 #H1
216[ @Zltb_elim_Type0 #H2 ]
217[2,3: #ABS normalize in ABS; destruct(ABS) ]
218normalize nodelta whd in ⊢ (???%→?); #EQ destruct(EQ)
219%
220[2: whd in ⊢ (???%);
221  @eq_f
222  @mem_ext_eq [2: % ]
223  #b @if_elim
224  [2: #B
225    @If_elim #prf1 @If_elim #prf2
226    [2,3: @⊥ >prf1 in prf2; * /2 by I/ ] [2: % [%%] #z % ]
227    whd in match low_bound; whd in match high_bound;
228    normalize nodelta
229    cut (Not (bool_to_Prop (eq_block b (pblock ptr))))
230    [ % #ABS >ABS in B; * ]
231    -B #B % [ >B %% ] #z
232    @If_elim #prf3 
233    @If_elim #prf4
234    [2,3: @⊥ >B in prf4; normalize nodelta >prf3 * /2 by I/ |4: % ]
235    whd in match sigma_beval in ⊢ (??%%); normalize nodelta
236    @opt_safe_elim @opt_safe_elim #bv1 #EQ1 #bv2 #EQ2 >B in EQ1;
237    >EQ2 #EQ destruct(EQ) %
238  | #B cut (b = pblock ptr) [ lapply B @eq_block_elim // #_ * ]
239    #EQ destruct(EQ)
240    @If_elim whd in match low_bound; whd in match high_bound;
241    normalize nodelta
242    [2: >block_ok * #ABS elim (ABS I) ]
243    #prf3 % [ >B %% ]
244    #z whd in match update; normalize nodelta
245    @eqZb_elim normalize nodelta #prf4
246    [2: @If_elim #prf5 @If_elim #prf6
247      [2,3: @⊥ >B in prf6; >prf5 * /2 by I/ |4: % ]
248      whd in match sigma_beval in ⊢ (??%%); normalize nodelta
249      @opt_safe_elim @opt_safe_elim #bv1 #EQ1 #bv2 #EQ2 >B in EQ1;
250      normalize nodelta >(eqZb_false … prf4) >EQ2
251      #EQ destruct(EQ) %
252    | @If_elim #prf5
253      [2: >B in prf5; normalize nodelta
254        >prf4 >(Zle_to_Zleb_true … H1) >(Zlt_to_Zltb_true … H2) * #ABS elim (ABS I) ]
255      whd in match sigma_beval in ⊢ (??%%); normalize nodelta
256      @opt_safe_elim @opt_safe_elim #bv1 #EQ1 #bv2 #EQ2 >B in EQ1;
257      normalize nodelta >prf4 >eqZb_z_z >EQ2 #EQ destruct(EQ) %
258    ]
259  ]
260| whd #b #z #h1 whd in match low_bound; whd in match high_bound; normalize nodelta
261  @eq_block_elim #H normalize nodelta destruct
262  #h2 #h3 whd in match update; normalize nodelta
263  [ @eqZb_elim #H destruct normalize nodelta [ assumption ]]
264  @prf1 assumption
265]
266qed.
267
268include alias "common/Identifiers.ma".
269include alias "common/PositiveMap.ma".
270
271let rec map_inf A B (b : positive_map A) on b :
272        (∀a : A.(Σp:Pos. lookup_opt A p b = Some ? a) → B) →  positive_map B ≝
273λf.       
274(match b return λx.x=b → ? with
275[ pm_leaf ⇒ λ_.pm_leaf ?
276| pm_node a l r ⇒ λprf.pm_node ?
277((match a return λx.a=x→? with
278        [Some x ⇒ λprf1.return f x «one,?» 
279        |None ⇒ λ_.None ?
280        ]) (refl ? a))
281    (map_inf ?? l (λa1,prf1.f a1 «p0 ?,?»))
282    (map_inf ?? r (λa1,prf1.f a1 «p1 ?,?»))
283]) (refl ? b).
284[ @hide_prf <prf normalize assumption
285|*: [1,3: @hide_prf] cases prf1 #tl #H [4,3 : @tl] <prf assumption
286] qed.
287
288
289definition map_inf1 :  ∀A, B: Type[0].
290  ∀tag: String.
291  ∀m:identifier_map tag A.
292   (∀a:A.(Σid. lookup tag A m id = Some A a) → B) →
293  identifier_map tag B ≝
294λA,B,tag,m.
295(match m return λx.(∀a:A.(Σid. lookup tag A x id = Some A a) → B) → ? with
296  [an_id_map b ⇒ λF.an_id_map …
297       (map_inf A B b (λa,prf.F a «an_identifier tag ?,?»))]).
298[@hide_prf] cases prf #pos #H assumption
299qed.
300
301lemma ext_map_inf_eq : ∀A , B : Type[0].
302  ∀ m : positive_map A.
303  ∀ F, F' :  (∀a:A.(Σp:Pos. lookup_opt A p m = Some ? a) → B).
304  (∀a',id',id'',prf,prf'. F a' «id',prf» = F' a' «id'',prf'») →
305  map_inf A B m F = map_inf A B m F'.
306#A #B #m elim m [#F #F' #eqFF' %] * [2:#a] normalize nodelta #l #r #Hl #Hr #F #F'
307#eqFF' normalize [>(eqFF' a one one (refl ? (Some A a)) (refl ? (Some A a)))]
308@eq_f2 [1,3: @Hl |*: @Hr] #a' #id' #id'' #prf' #prf'' @eqFF'
309qed.
310 
311
312lemma map_inf_add : ∀ A, B : Type[0].
313  ∀tag : String.
314  ∀m: identifier_map tag A.
315  ∀F :(∀a:A.(Σid. lookup tag A m id = Some A a) → B).
316  ∀a,id.
317  let m' ≝ (add tag A m id a) in
318  ∀F' :(∀a:A.(Σid. lookup tag A m' id = Some A a) → B).
319  (∀a',id',id'',prf,prf'. F a' «id',prf» = F' a' «id'',prf'») →
320  ∃ prf.
321  map_inf1 A B tag m' F' =
322  add tag B (map_inf1 A B tag m F) id (F' a «id,prf»).
323#A #B #tag #m #F #a #id normalize nodelta #F' #eqFF' %
324[@hide_prf @(lookup_add_hit tag A m ? ?)]
325lapply eqFF' -eqFF' lapply F' -F' lapply id -id lapply a -a lapply F -F
326cases m -m #m elim m
327[ #F #a * #id elim id [#F' #eqFF' %] #x #Hx #F' #eqFF' whd in ⊢ (??%%);
328  normalize nodelta @eq_f whd in match insert; normalize nodelta
329  whd in ⊢ (??%%); normalize nodelta @eq_f2 try %
330  lapply(Hx ??)
331    [2,5: #a1 ** #id1 #prf1 @F' [1,3: @a1]
332          [%{(an_identifier tag (p1 id1))} |%{(an_identifier tag (p0 id1))}] @prf1
333    |1,4: #a' * #id' * #id'' #prf #prf' normalize nodelta @eqFF'
334    |*: normalize nodelta whd in ⊢ (??%% → ?); normalize nodelta #EQ destruct(EQ)
335      lapply e0 -e0 whd in ⊢ (??%% → ?); normalize nodelta normalize in ⊢ (??(???%?)? → ?);
336      #EQ <EQ %
337    ]
338|  #opt_a #l1 #r1 #Hl1 #Hr1 #F #a ** [|*: #x] #F' #eqFF'
339  [ normalize @eq_f @eq_f2 @ext_map_inf_eq #a' #id' #id'' #prf' #prf'' >eqFF' [1,4:%|*:]
340  |*: normalize @eq_f lapply eqFF' -eqFF' lapply F' -F' lapply F -F cases opt_a
341      [2,4: #a1] normalize nodelta #F #F' #eqFF'
342      [3,4: @eq_f2|*: >(eqFF' a1 (an_identifier tag one) (an_identifier tag one)
343                     (refl (option A) (Some A a1)) (refl (option A) (Some A a1)))
344                    @eq_f2]
345          [1,4,5,8: @ext_map_inf_eq #a' #id' #id'' #prf' #prf'' >eqFF' [1,4,7,10:%|*:]
346          |2,6: lapply (Hr1 ? a (an_identifier tag x) ? ?)
347          |*: lapply (Hl1 ? a (an_identifier tag x) ? ?)
348          ]
349          [2,3,6,7,10,11,14,15: #a ** #id #prf [2,4,6,8: @F |*: @F'] try @a %
350                   [1,3,9,11: % @(p1 id) |5,7,13,15: % @(p0 id) |*: @hide_prf <prf %]
351          |1,5,9,13: #a * #id' * #id'' #prf #prf' normalize nodelta @eqFF'
352          |*: normalize in ⊢ (%→ ?); #EQ destruct(EQ) >e0 %
353          ]
354  ]
355]
356qed.
357*)
358
359
360inductive id_is_in (A : Type[0]) : Pos →  positive_map A → Prop ≝
361| is_in_root : ∀l,r,opt_a. id_is_in A (one) (pm_node … opt_a l r)
362| is_in_left : ∀l,r,opt_a,x. id_is_in A x l →
363                                    id_is_in A (p0 x) (pm_node … opt_a l r)
364| is_in_right : ∀l,r,opt_a,x. id_is_in A x r →
365                                    id_is_in A (p1 x) (pm_node … opt_a l r).
366
367definition id_is_in : ∀A : Type[0]. ∀tag : String.
368identifier_map tag A → identifier tag → Prop ≝
369λA,tag,m,id.match id with
370     [an_identifier x ⇒ match m with
371                              [an_id_map p ⇒ id_is_in A x p]
372     ].
373(*
374lemma lookup_map : ∀A,B : Type[0].
375  ∀tag : String.
376  ∀m : identifier_map tag A.
377  ∀ F : (∀a:A.(Σid. lookup tag A m id = Some A a) → B).
378  ∀ id,opt_a. lookup tag A m id =opt_a →
379lookup tag B (map_inf1 A B tag m F) id =
380(match opt_a return λx.opt_a = x→ ? with
381[Some a ⇒ λprf.Some ? (F a «id,?»)
382|None ⇒ λ_.None ?
383])(refl ? (opt_a)).
384[2: @hide_prf //]
385#A #B #tag * #m elim m [2: * [2: #a] #l #r #Hl #Hr] #F ** [1,4,7: |*: #x]
386* [2,4,6,8,10,12,14,16,18: #a1] normalize in ⊢ (% → ?); [1,2,3,8,9,10: #EQ destruct]
387// normalize nodelta
388#EQ
389[1,3: lapply(Hr ? (an_identifier tag x) (Some ? a1) EQ)
390  [1,3: #a2 * * #id2 #id2_spec @F [1,3: @a2 |*: %{(an_identifier tag (p1 id2))} <id2_spec %]]
391|2,4: lapply(Hl ? (an_identifier tag x) (Some ? a1) EQ)
392  [1,3: #a2 * * #id2 #id2_spec @F [1,3:  @a2 |*: %{(an_identifier tag (p0 id2))} <id2_spec %]]
393|5,7:  lapply(Hr ? (an_identifier tag x) (None ?) EQ)
394  [1,3: #a2 * * #id2 #id2_spec @F [1,3: @a2 |*: %{(an_identifier tag (p1 id2))} <id2_spec %]]
395|6,8: lapply(Hl ? (an_identifier tag x) (None ?) EQ)
396  [1,3: #a2 * * #id2 #id2_spec @F [1,3:  @a2 |*: %{(an_identifier tag (p0 id2))} <id2_spec %]]
397] normalize #EQ1 <EQ1 %
398qed.
399
400(*
401lemma lookup_map_weak : ∀ A,B : Type[0].
402  ∀tag : String.
403  ∀m : identifier_map tag A.
404  ∀ F : (∀a:A.(Σid. lookup tag A m id = Some A a) → B).
405  ∀ id,a,prf.
406 lookup tag B (map_inf1 A B tag m F) id = Some ? (F a «id,prf»).
407#A #B #tag #m #F #id #a #prf >(lookup_map … prf) normalize %
408qed.
409
410
411lemma lookup_map_fail : ∀A,B : Type[0].
412∀tag : String.
413  ∀m : identifier_map tag A.
414  ∀ F : (∀a:A.(Σid. lookup tag A m id = Some A a) → B).
415  ∀ id. lookup tag A m id = None ? →
416  lookup tag B (map_inf1 A B tag m F) id = None ?.
417cases daemon
418qed.*)
419
420*)
421
422lemma lookup_eq : ∀ A : Type[0].
423∀m,m' : positive_map A.
424(∀id. lookup_opt A id m = lookup_opt A id m'
425      ∧ (id_is_in A id m ↔ id_is_in A id m')) → m=m'.
426#A #m elim m
427[ * [#_ %] #opt_a #l #r #H lapply(H one) normalize * #EQ >EQ * #_ #H1 lapply(H1 ?) [%]
428  -H1 -H <EQ -EQ #H inversion H #l1 #r1 #opt_a1
429  [ #_ #EQ  lapply(jmeq_to_eq ??? EQ) -EQ #EQ destruct(EQ)
430  |*: #pos #H1 #_ #_ #EQ  lapply(jmeq_to_eq ??? EQ) -EQ #EQ destruct(EQ)
431  ]
432| #opt_a #l #r #Hl #Hr *
433  [ #H lapply(H one) normalize * #EQ >EQ * #H1 #_ lapply(H1 ?) [%]
434  -H1 -H -EQ #H inversion H #l1 #r1 #opt_a1
435    [ #_ #EQ  lapply(jmeq_to_eq ??? EQ) -EQ #EQ destruct(EQ)
436    |*: #pos #H1 #_ #_ #EQ  lapply(jmeq_to_eq ??? EQ) -EQ #EQ destruct(EQ)
437    ]
438  | #opt_a1 #l1 #r1 #H lapply(H one) normalize * #EQ >EQ -EQ #_ @eq_f2 [@Hl|@Hr]
439    #id [ lapply(H (p0 id)) | lapply(H (p1 id))] normalize * #H1 * #H2 #H3 %
440    [1,3: assumption] % #H4 [1,3: lapply(H2 ?) |*: lapply(H3 ?)]
441    try %2 try %3 try assumption #H5 inversion H5 #l2 #r2 #opt_a2
442    [1,4,7,10: #EQ lapply(jmeq_to_eq ??? EQ) -EQ #EQ @⊥
443               [1,3: cut(p0 id ≠ one) [1,3: @(pos_elim … id) /3/]
444               |*:   cut(p1 id ≠ one) [1,3: @(pos_elim … id) /3/]
445               ] * #H @H assumption
446    |*: #pos #H6 #_ #EQ lapply(jmeq_to_eq ??? EQ) -EQ #EQ destruct(EQ)
447        #EQ lapply(jmeq_to_eq ??? EQ) -EQ #EQ destruct(EQ) #_ assumption
448    ]
449  ]
450]
451qed.
452
453include alias "common/Identifiers.ma".
454include alias "common/PositiveMap.ma".
455
456
457lemma p0_neq_one : ∀x: Pos. p0 x ≠ one.
458#x /3/
459qed.
460
461lemma p1_neq_one : ∀x: Pos. p1 x ≠ one.
462#x /3/
463qed.
464
465lemma lookup_ok_to_update : ∀ A : Type[0].
466∀ tag : String.
467∀m,m' : identifier_map tag A. ∀id,a.
468(lookup tag A m' id = Some ? a)  → lookup tag A m id ≠ None ? →
469(∀ id'. id ≠ id' → (lookup tag A m id' = lookup tag A m' id') ∧
470     (id_is_in A tag m id' ↔ id_is_in A tag m' id')) →
471update tag A m id a = return m'.
472#A #tag * #m * #m' * #id #a
473normalize in ⊢ (%→%→?); lapply id -id lapply m' -m' elim m
474    [ #m' #id #m_spec' normalize in ⊢ (% → ?); * #EQ @⊥ @EQ %] #opt_a #l #r #Hl #Hr
475    #m' * [|*: #x] normalize in ⊢ (%→%→?); #m_spec'
476    [ cases opt_a -opt_a [* #H @⊥ @H %] #a1 #_ #H normalize @eq_f @eq_f
477      lapply H -H lapply m_spec'; -m_spec' lapply a -a cases m'
478      [#a normalize #EQ destruct] #opt_a1 #l1 #r1 #a
479      normalize in ⊢ (%→?); #EQ >EQ #H @eq_f2 @lookup_eq #id'
480      [ lapply (H (an_identifier tag (p0 id')) ?)
481      | lapply (H (an_identifier tag (p1 id')) ?)
482      ]
483      [1,3:% @(pos_elim … id') [1,3:#H destruct|*: #n #IP #H destruct]]
484      * normalize #H1 * #H2 #H3 % [1,3: >H1 %] % #H4
485      [1,3: lapply(H2 ?) |*: lapply(H3 ?)] try %2 try %3 try assumption
486      #H5 inversion H5 #l2 #r2 #opt_a2
487        [1,4,7,10: #EQ lapply(jmeq_to_eq ??? EQ) -EQ #EQ @⊥
488                   [1,3: cut(p0 id' ≠ one) [1,3: /3/]
489                   |*: cut(p1 id' ≠ one) [1,3: /3/]
490                   ] >EQ * #H @H %
491        |*: #pos #H6 #_ #EQ1 lapply(jmeq_to_eq ??? EQ1) -EQ1 #EQ1 destruct(EQ1)
492            #EQ1 lapply(jmeq_to_eq ??? EQ1) -EQ1 #EQ1 destruct(EQ1) #_ assumption
493        ]
494    |*: #H lapply m_spec' -m_spec' cases m' -m' [1,3: normalize #EQ destruct]
495        #opt_a1 #l1 #r1 normalize in ⊢ (% → ?); #H1 #H2
496        [ lapply(Hr ?? H1 H ?) | lapply(Hl ?? H1 H ?)]
497          [1,3: * #y * #y_spec
498            [lapply(H2 (an_identifier tag (p1 y)) ?) | lapply(H2 (an_identifier tag (p0 y)) ?)]
499            [1,3: % #EQ destruct @y_spec %] * normalize #H3 * #H4 #H5 % // % #H6
500            [1,3: lapply(H4 ?) |*: lapply (H5 ?)] try %2 try %3 try assumption
501            #H7 inversion H7 #l2 #r2 #opt_a2
502              [1,4,7,10: #EQ lapply(jmeq_to_eq ??? EQ) -EQ #EQ @⊥
503                   [1,3: cut(p1 y ≠ one) [1,3: /3/]
504                   |*: cut(p0 y ≠ one) [1,3: /3/]
505                   ] >EQ * #H @H %
506              |*: #pos #H6 #_ #EQ1 lapply(jmeq_to_eq ??? EQ1) -EQ1 #EQ1
507                 destruct(EQ1) #EQ1 lapply(jmeq_to_eq ??? EQ1) -EQ1 #EQ1
508                 destruct(EQ1) #_ assumption
509              ]
510          |2,4: normalize cases(update A x a ?) normalize [2,4: #pos_map]
511               #EQ destruct @eq_f @eq_f lapply(H2 (an_identifier tag one) ?)
512               [1,3: % #EQ destruct] * normalize #EQ >EQ #_ @eq_f2 [2,3: %]
513               @lookup_eq #id'
514               [lapply (H2 (an_identifier tag (p0 id')) ?) |
515                                   lapply (H2 (an_identifier tag (p1 id')) ?) ]
516               [1,3: % #EQ1 destruct] * normalize #H3 * #H4 #H5 % // % #H6
517               [1,3: lapply(H4 ?) |*: lapply(H5 ?)] try %2 try %3 try assumption
518               #H7 inversion H7 #l2 #r2 #opt_a2
519                  [1,4,7,10: #EQ lapply(jmeq_to_eq ??? EQ) -EQ #EQ @⊥
520                    [1,3: cut(p0 id' ≠ one) [1,3: /3/]
521                    |*: cut(p1 id' ≠ one) [1,3: /3/]
522                   ] >EQ * #H @H %
523                  |*: #pos #H6 #_ #EQ1 lapply(jmeq_to_eq ??? EQ1) -EQ1 #EQ1
524                      destruct(EQ1) #EQ1 lapply(jmeq_to_eq ??? EQ1) -EQ1 #EQ1
525                      destruct(EQ1) #_ assumption
526                  ]
527            ]
528      ]
529qed.
530
531
532lemma update_ok_to_lookup : ∀ A : Type[0].
533∀ tag : String.
534∀m,m' : identifier_map tag A. ∀id,a.
535update tag A m id a = return m' →
536(lookup tag A m' id = Some ? a) ∧ lookup tag A m id ≠ None ? ∧
537(∀ id'. id ≠ id' → (lookup tag A m id' = lookup tag A m' id') ∧
538     (id_is_in A tag m id' ↔ id_is_in A tag m' id')).
539#A #tag * #m * #m' * #id #a
540whd in ⊢ (??%% →  ?); inversion(update A ???) normalize nodelta [#_ #ABS destruct]
541    #m1 #m1_spec #EQ destruct % [%]
542    [  normalize @(update_lookup_opt_same … m1_spec)
543    |3: * #id' * #id_spec' normalize %
544        [@(update_lookup_opt_other … m1_spec ??) % #EQ @id_spec' >EQ %]
545        lapply id_spec' lapply m1_spec -id_spec' -m1_spec
546        (*cases id [|*:#x] -id normalize*) lapply m' -m' lapply id lapply id' -id -id'
547        elim m [#id' #id #m' cases id [|*: #x] normalize #EQ destruct]
548        #opt_a #l #r #Hl #Hr #id' #id #m' cases id [|*:#x] -id normalize
549        [ cases opt_a [2:#a] normalize #EQ destruct cases id' [#H @⊥ @H %]
550          #x #_ normalize % #H [1,2: %3 |*: %2]
551          inversion H #l1 #r1 #opt_a1
552          [1,4,7,10: #EQ lapply(jmeq_to_eq ??? EQ) #EQ1 @⊥
553                     [1,2: cut(p1 x ≠ one) [1,3: @(pos_elim … x) /3/]
554                     |*:   cut(p0 x ≠ one) [1,3: @(pos_elim … x) /3/]
555                     ]
556                     * #H @H >EQ1 //   
557          |*:        #pos #H1 #_ #EQ lapply(jmeq_to_eq ??? EQ) #EQ1 destruct(EQ1)
558                     #EQ lapply(jmeq_to_eq ??? EQ) #EQ1 destruct(EQ1) #_ assumption
559          ]
560        |*: inversion(update A x a ?) normalize [1,3: #_ #EQ destruct] #pos_map
561            #pos_map_spec #EQ destruct #id_spec' % #H
562            inversion H #l1 #l2 #opt_a1
563            [1,4,7,10: #EQ lapply(jmeq_to_eq ??? EQ) -EQ #EQ
564                       #EQ1 lapply(jmeq_to_eq ??? EQ1) -EQ1 #EQ1 destruct(EQ1)
565                       #H1 %
566            |*: #pos #H1 #_ #EQ lapply(jmeq_to_eq ??? EQ) -EQ #EQ
567                #EQ1 lapply(jmeq_to_eq ??? EQ1) -EQ1 #EQ1 destruct(EQ1)
568                #H2 try %2 try %3 try assumption
569                [ @(proj1 … (Hr ? ? pos_map pos_map_spec ?)) [#EQ1 destruct @id_spec' %]
570                | @(proj2 … (Hr ? ? l2 pos_map_spec ?)) [#EQ1 destruct @id_spec' %]
571                | @(proj1 … (Hl ? ? pos_map pos_map_spec ?)) [#EQ1 destruct @id_spec' %]
572                | @(proj2 … (Hl ? ? l1 pos_map_spec ?)) [#EQ1 destruct @id_spec' %]
573                ]
574                assumption
575            ]
576         ]     
577    | % normalize lapply m1_spec lapply id lapply m' -id -m' elim m
578      [#m' * [|*: #x] normalize #EQ destruct] #opt_a #l #r #Hl #Hr #m' * [|*: #x]
579      normalize [ cases opt_a [2:#a] normalize #EQ1 #EQ2 destruct]
580      inversion (update A x a ?) [1,3: #_ normalize #EQ destruct]
581      #pos_map #EQpos_map normalize #EQ destruct [@Hr|@Hl] assumption
582    ]
583qed.
584(*
585               
586lemma update_lookup_after : ∀ A : Type[0].
587∀ tag : String.
588∀m,m' : identifier_map tag A. ∀id,a.
589update tag A m id a = return m' →
590lookup tag A m' id = Some ? a.
591#A #B #tag * #m1 * #id #a whd in ⊢ (??%% → ?); inversion(update A ???)
592normalize nodelta [#_ #EQ destruct] #pos_map #pos_map_spec #EQ destruct
593@(update_lookup_opt_same … pos_map_spec)
594qed.
595
596lemma p0_neq_one : ∀x: Pos. p0 x ≠ one.
597#x /3/
598qed.
599
600lemma p1_neq_one : ∀x: Pos. p1 x ≠ one.
601#x /3/
602qed.
603
604lemma id_is_in_map : ∀ A,B : Type[0]. ∀tag : String.
605∀m : identifier_map tag A.
606∀ F : (∀a:A.(Σid. lookup tag A m id = Some A a) → B).
607∀id. id_is_in A tag m id ↔ id_is_in B tag (map_inf1 A B tag m F) id.
608#A #B #tag * #m elim m
609[ #F * #id % normalize #H inversion H #l #r #opt_a
610  [1,4: #_ #EQ lapply(jmeq_to_eq ??? EQ) -EQ #EQ destruct
611  |*: #pos #H1 #_ #_ #EQ lapply(jmeq_to_eq ??? EQ) -EQ #EQ destruct
612  ]
613| * [2:#a] #l #r #Hl #Hr #F ** [1,4: |*:#x] normalize % #H try % try %2 try %3
614  [1,2,5,6: cases(Hr ? (an_identifier tag x)) |*: cases (Hl ? (an_identifier tag x))]
615  [2,4,6,8,10,12,14,16: #a1 ** #id1 #prf1 @F try(@a1)
616                        try(%{(an_identifier tag (p1 id1))} assumption)
617                        try(%{(an_identifier tag (p0 id1))} assumption) ]
618  try(#H1 #_ @H1) try(#_ #H1 @H1) -H1 -Hl -Hr inversion H #l1 #r1 #opt_a1
619  [1,4,7,10,13,16,19,22: #EQ lapply(jmeq_to_eq ??? EQ) -EQ #EQ @⊥
620             [1,2,3,4: lapply(p1_neq_one x)
621             |*:       lapply(p0_neq_one x)
622             ] * #H @H >EQ %
623  |*: #pos #H1 #_ #EQ lapply(jmeq_to_eq ??? EQ) -EQ #EQ destruct
624      #EQ lapply(jmeq_to_eq ??? EQ) -EQ #EQ destruct #_ assumption
625  ]
626]
627qed.
628
629lemma map_update_commute : ∀ A, B : Type[0].
630∀tag : String.
631∀m1,m2 : identifier_map tag A.
632∀id,a.
633update tag A m1 id a = return m2 →
634∀ F : (∀a:A.(Σid. lookup tag A m1 id = Some A a) → B).
635∀ F': (∀a:A.(Σid. lookup tag A m2 id = Some A a) → B). 
636(∀a',id',prf,prf'. F a' «id',prf» = F' a' «id',prf'») → ∃prf.
637update tag B (map_inf1 A B tag m1 F) id (F' a «id,prf») =
638return map_inf1 A B tag m2 F'.
639#A #B #tag #m1 #m2 #id #a #m2_spec #F #F' #eqFF' %
640[ @hide_prf cases(update_lookup_previous A tag m1 m2 id a) #H1 #_ cases (H1 m2_spec)
641  * #H1 #H2 #H3 assumption
642| cases(update_lookup_previous B tag (map_inf1 A B tag m1 F)
643                             (map_inf1 A B tag m2 F') id (F' a «id,?»))
644  [ #_ #H @H |] cases(update_lookup_previous A tag m1 m2 id a) #H2 #INUTILE
645cases(H2 m2_spec) * #H3 #H4 #H5 % [%]
646[ >(lookup_map … H3) %
647| elim H4 -H4 #H4 % #H5 @H4 lapply H5 cases m1 in F; -m1 #m1 cases id -id
648  elim m1 [ #id #F normalize * %] #a1 #l #r #Hl #Hr * [|*:#x] #F normalize
649  [ cases a1 in F; [2: #a2] #F normalize [2: * %] #EQ destruct
650  |*: #H
651    [@(Hr x ??) | @(Hl x ??)]
652    [1,3:#a ** #id1 #prf1 @F [1,3: @a]
653         [%{(an_identifier tag (p1 id1))}|%{(an_identifier tag (p0 id1))}]
654         normalize assumption
655    |*: normalize @H
656    ]
657  ]
658| #id' #id_spec' lapply(H5 id' id_spec') * #H6 * #H7 #H8 %
659  [ lapply H6 inversion (lookup tag A m2 id')
660    [2: #w] #w_spec #EQ >(lookup_map … EQ) normalize nodelta
661    >(lookup_map … w_spec) normalize nodelta [2: %] @eq_f @eqFF'
662  | cases(id_is_in_map A B tag m1 F id') cases(id_is_in_map A B tag m2 F' id')
663   #H9 #H10 #H11 #H12 % #H13 [ @H9 @H7 @H12 assumption | @H11 @H8 @H10 assumption]
664  ]
665]
666qed.
667
668(*
669definition well_formed_register_env :
670∀prog : ertl_program .∀sigma : (sigma_map prog).
671register_env beval → Prop ≝
672λprog,sigma,psd_reg.∀id,bv. lookup ?? psd_reg id = Some ? bv →
673sigma_beval_opt prog sigma bv ≠ None ?.
674*)
675*)
676
677definition map : ∀tag,A,B. identifier_map tag A → (A → B) → identifier_map tag B ≝
678λtag,A,B,m,f.match m with
679[an_id_map p ⇒ an_id_map … (map ?? f p)].
680
681lemma lookup_map : ∀A,B : Type[0].
682  ∀tag : String.
683  ∀m : identifier_map tag A.
684  ∀ f:A → B.
685  ∀ id.
686lookup tag B (map tag A B m f) id =
687! a ← lookup tag A m id; return f a.
688#A #B #tag * #m #f * #id normalize >lookup_opt_map %
689qed.
690
691lemma update_leaf_fail: ∀tag,A,i,v.
692 update tag A (empty_map ??) i v = Error ? [MSG MissingId; CTX … i].
693#ta #A ** [|*: #x] #v normalize %
694qed.
695
696lemma update_def : ∀tag,A,m,i,v.
697  update tag A m i v =
698  match lookup tag A m i with
699  [ Some _ ⇒ OK ? (add tag A m i v)
700  | None ⇒ Error ? [MSG MissingId; CTX … i]
701  ].
702#tag #A #m #i #v inversion(update tag A m i v)
703[ #m' #EQm' cases(update_ok_to_lookup ?????? EQm') * #_
704 #H #_ elim H cases(lookup tag A m i) [#H @⊥ @H %]
705 #x #_ normalize <EQm' lapply EQm' cases i cases m cases m' -m -m' -i
706 normalize #m' #m #i inversion(update A i v m) normalize [#_ #ABS destruct]
707 #m'' #EQm'' #EQ destruct(EQ) @eq_f @eq_f lapply EQm'' -EQm'' lapply i -i
708 lapply m' -m' elim m [#m' * [2,3: #z] normalize #EQ destruct]
709 #opt_a #l #r #Hl #Hr #m' * [2,3: #z] normalize
710 [3: cases opt_a normalize [2: #y] #EQ destruct %
711 |*: inversion(update A z v ?) [2,4: #m'']  #EQm'' normalize #EQ destruct
712     [<(Hr … EQm'') | <(Hl … EQm'')] %
713 ]
714| #err cases m -m cases i -i #i #m normalize inversion(update A i v m) [2:#m']
715  #EQerr normalize #EQ destruct lapply EQerr lapply i elim m
716  [ normalize #x #_ %] #opt_a #l #r #Hl #Hr * [2,3:#z] normalize
717 [3: cases opt_a [2:#w] normalize #EQ destruct %
718 |*: inversion(update A z v ?) [2,4: #m'] #EQm' normalize #EQ destruct
719     [lapply(Hr … EQm') | lapply(Hl … EQm')] cases(lookup_opt A z ?) [2,4: #a]
720     normalize #EQ destruct %
721 ]
722]
723qed.
724
725lemma map_add : ∀tag : String.∀A,B : Type[0].∀ f: A → B.∀m,id,v.
726map tag A B (add tag A m id v) f = add tag B (map tag A B m f) id (f v).
727#tag #A #B #f * #m * #id #v normalize @eq_f lapply v -v lapply id -id elim m
728[ #id elim id [#v %] #x #IH #id normalize >IH normalize inversion(pm_set ? ? ? ?)
729  normalize // cases x normalize [2,3,5,6: #y] #EQ destruct
730| #opt_a #l #r #Hl #Hr * [2,3: #x| #v normalize cases opt_a normalize [2: #a %]
731  cases (map_opt ? ? ? l) normalize [2: //] cases (map_opt ? ? ? r) normalize
732  //] #v normalize cases opt_a [2,4: #a] normalize //
733  [ cases(map_opt ? ? ? l) normalize // >Hr cases(map_opt ? ? ? r) normalize
734    [2: #opt_b #lb #rb] inversion(pm_set B x ? ?) normalize // cases x [2,3,5,6: #y]
735    normalize #EQ destruct
736  | >Hl cases(map_opt ? ? ? l) normalize [2: #opt_b #lb #rb]
737    inversion (pm_set B x ? ?) normalize //
738    [1,2: cases x [2,3,5,6: #y] normalize #EQ destruct]
739    #opt_b' #lb' #rb' #_ normalize #_ #EQ cases(map_opt ? ? ? r)
740    normalize nodelta [%] #opt_b'' #lb'' #rb'' >EQ %
741]
742qed.
743
744
745definition restrict : ∀tag.∀A,B.
746identifier_map tag A → identifier_map tag B → identifier_map tag A ≝
747λtag,A,B,m1,m2.an_id_map …
748           (merge A B A (λo,o'.match o' with [None ⇒ None ? | Some _ ⇒ o])
749                  (match m1 with [an_id_map p1 ⇒ p1])
750                  (match m2 with [an_id_map p2 ⇒ p2])).
751
752interpretation "identifier map restriction" 'intersects a b = (restrict ??? a b).
753
754unification hint 0 ≔ tag ; R ≟ identifier tag ⊢ list R ≡ list (identifier tag).
755 
756lemma map_update_commute : ∀tag : String.∀A,B : Type[0].∀f : A → B. ∀m,id,v.
757update tag B (map tag A B m f) id (f v) =
758!m' ← update tag A m id v; return map tag A B m' f.
759#tag #A #B #f #m #id #v >update_def >update_def >lookup_map
760cases (lookup tag A m id) [%] #a >m_return_bind >m_return_bind normalize nodelta
761whd in ⊢ (???%); @eq_f @sym_eq @map_add
762qed.
763
764definition is_leaf ≝ λA.λpm : positive_map A.
765match pm with [ pm_leaf ⇒ true | _ ⇒ false ].
766(*
767let rec pm_clean A (pm : positive_map A) on pm : positive_map A ≝
768match pm with
769[ pm_leaf ⇒ pm_leaf ?
770| pm_node o l r ⇒
771  let l' ≝ pm_clean … l in
772  let r' ≝ pm_clean … r in
773  match o with
774  [ Some _ ⇒ pm_node … o l' r'
775  | None ⇒
776    if is_leaf … l' ∧ is_leaf … r' then pm_leaf ? else
777    pm_node … o l' r'
778  ]
779].
780 
781definition clean ≝ λtag,A.λm : identifier_map tag A.
782  match m with [ an_id_map pm ⇒ an_id_map tag A (pm_clean … pm) ].
783*)
784
785definition sigma_register_env :
786∀prog : ertl_program.∀sigma : (sigma_map prog).
787register_env beval → list register →  register_env beval ≝
788λprog,sigma,psd_env,ids.
789let m' ≝  map ??? psd_env (λbv.sigma_beval prog sigma bv) in
790m' ∖ ids.
791
792(*
793definition well_formed_ertl_psd_env :
794∀prog : ertl_program. ∀sigma : (sigma_map prog).
795ertl_psd_env → Prop≝
796λprog,sigma,psd_env.well_formed_register_env prog sigma (psd_regs psd_env).
797*)
798(*
799let rec well_formed_frames
800(prog : ertl_program) (sigma : (sigma_map prog))
801(l : list ertl_psd_env) on l : Prop ≝
802match l with
803  [nil ⇒ True
804  | cons a tl ⇒ well_formed_ertl_psd_env prog sigma a ∧
805               well_formed_frames prog sigma tl
806  ].                           
807*)
808
809
810lemma lookup_restrict : ∀tag,A,B.∀a : identifier_map tag A.∀b : identifier_map tag B.
811∀i.lookup ?? (a ∩ b) i = if i ∈ b then lookup … a i else None ?.
812#tag #A #B * #a * #b * #i normalize >lookup_opt_merge [2: %] cases (lookup_opt B i b)
813[2: #b] normalize % qed.
814
815
816lemma lookup_set_minus : ∀tag,A,B. ∀a : identifier_map tag A. ∀b : identifier_map tag B.
817∀i. lookup ?? (a ∖ b) i = if i ∈ b then None ? else lookup … a i.
818#tag #A #B * #a * #b * #i normalize >lookup_opt_merge [2: %] cases(lookup_opt B i b)
819[2: #b] % qed.
820
821(*
822lemma clean_add : ∀tag,A,m,i,v.clean … (add tag A m i v) = add tag A (clean … m) i v.
823#tag #A * #m * #i #v normalize @eq_f
824lapply m -m
825elim i -i
826[ * [%]
827  * [2: #x] #l #r [%] normalize
828  cases (pm_clean A l) normalize // cases (pm_clean A r) //
829|*: #i #IH * normalize
830  [1,3: >IH cases i // ]
831  * [2,4: #x] #l #r normalize
832  [1,2: >IH % ]
833  >IH cases i cases (pm_clean A l) cases (pm_clean A r) normalize //
834]
835qed.
836
837lemma clean_lookup : ∀tag,A,m,i.lookup … (clean tag A m) i = lookup … m i.
838#tag #A * #m * #i normalize lapply i -i elim m
839[#i %] * [2: #a] #l #r #Hl #Hr * [2,3,5,6: #x] normalize in ⊢ (???%);
840[1,3:<Hr|2,4:<Hl] normalize try % [3: @if_elim #_ %]
841cases(pm_clean A l) in Hl; normalize
842[2: #opt_a1 #l1 #r1 #_ %
843|3: #H cases(pm_clean A r) normalize //
844| #H cases(pm_clean A r) in Hr; normalize //
845| #opt_a1 #l1 #r1 #H cases x normalize //
846]
847qed.   
848
849 
850lemma clean_update : ∀tag,A,m,i,v.
851! m' ← update tag A m i v; return clean … m' =
852update tag A (clean … m) i v.
853#tag #A #m #i #v
854>update_def >update_def >clean_lookup cases (lookup tag A m i)
855[ % ]
856#m' >m_return_bind normalize nodelta >clean_add %
857qed.
858*)
859lemma lookup_eq_id_map : ∀tag : String. ∀ A : Type[0].
860∀m,m' : identifier_map tag A.
861(∀id. lookup … m id = lookup … m' id
862      ∧ (id_is_in A tag m id ↔ id_is_in A tag m' id)) → m=m'.
863#tag #A * #m * #m' #H @eq_f @lookup_eq #id lapply(H (an_identifier tag id))
864* #H1 #H2 % // assumption
865qed.
866
867(*
868lemma clean_leaf : ∀tag : String . ∀ A : Type[0].
869∀m : identifier_map tag A. (∀ id. lookup … m id = None ?) →
870clean ?? m = empty_map ??.
871#tag #A * #m elim m [#_ %] #opt_a #l #r #Hl #Hr #H normalize @eq_f
872lapply(H (an_identifier tag one)) normalize #EQ >EQ -EQ normalize
873lapply(Hl ?) [2: lapply(Hr ?)]
874  [1,3: * #id [lapply(H (an_identifier tag (p1 id))) | lapply(H (an_identifier tag (p0 id)))]
875       #H assumption
876  | normalize #EQ #EQ1 destruct >e0 >e1 normalize %
877  ]
878qed.
879*)
880lemma id_is_in_lookup : ∀tag,A,m,id,v.
881 lookup tag A m id = Some ? v → id_is_in A tag m id.
882#tag #A * #m * #id #a normalize lapply m -m elim id
883[|*: #x #IH] * normalize [1,3,5: #EQ destruct] #opt_a #l #r [ #_ %] #H [%3 |%2]
884@IH assumption
885qed.
886(*
887lemma pm_clean_leaf : ∀ A : Type[0].
888∀m : positive_map A. (∀ id. lookup_opt … id m = None ?) →
889pm_clean ? m = pm_leaf ….
890#A #m elim m [ #id %] #opt_a #l #r #Hl #Hr #H normalize lapply(H one) normalize
891#EQ >EQ normalize >Hl [normalize >Hr [ %]] #id [@(H (p1 id))|@(H (p0 id))]
892qed.
893
894
895lemma pm_clean_canonic : ∀A,m,n.(∀i.lookup_opt A i m = lookup_opt A i n) →
896  pm_clean ? m = pm_clean ? n.
897#A #m #n lapply m -m elim n
898[ @pm_clean_leaf ]
899* [2: #x] #l #r #IHl #IHr *
900  [1,3: #H @sym_eq @pm_clean_leaf #id @sym_eq @H ] #opt #l' #r' #H
901 lapply (H one) normalize in ⊢ (%→?); #EQ destruct
902 whd in ⊢ (??%%);
903 >(IHl l') [1,3: >(IHr r') [1,3 : % ]] #i
904 [1,2: @(H (p1 i)) |*: @(H (p0 i)) ] qed.
905
906
907lemma clean_canonic : ∀tag,A,m,n.(∀i.lookup tag A m i = lookup tag A n i) →
908  clean ?? m = clean ?? n.
909#tag #A * #m * #n #H normalize @eq_f @pm_clean_canonic #i
910lapply(H (an_identifier tag i))
911normalize //
912qed.
913*)
914lemma update_fail_lookup : ∀tag,A,m,i,v,e.update tag A m i v = Error … e → 
915  e = [MSG MissingId; CTX … i] ∧ lookup … m i = None ?.
916#tag #A #m #i #v #errmsg >update_def cases(lookup tag A m i) [2: #a] normalize
917#EQ destruct % //
918qed.
919
920lemma lookup_hit_update : ∀tag,A,m,i,v.i ∈ m → 
921  ∃m'.update tag A m i v = OK ? m'.
922#tag #A #m #i #v #H % [2: >update_def lapply(in_map_domain … m i) >H * #v #EQ >EQ
923normalize %|]
924qed.
925
926lemma lookup_miss_update : ∀tag,A,m,i,v.lookup tag A m i = None ? → 
927  update … m i v = Error … [MSG MissingId; CTX … i].
928#tag #A #m #i #v #EQ >update_def >EQ normalize %
929qed.
930
931lemma update_ok_old_lookup : ∀tag,A,m,i,v,m'.update tag A m i v = OK ? m' →
932  i ∈ m.
933#tag #A #m #i #v #m' >update_def inversion(lookup tag A m i) [2: #a] #EQ normalize
934#EQ destruct >EQ normalize @I
935qed.
936
937lemma lookup_update_ok : ∀tag,A,m,i,v,m',i'.update tag A m i v = OK ? m' →
938  lookup … m' i' = if eq_identifier ? i' i then Some ? v else lookup … m i'.
939#tag #A #m #i #v #m' #i' >update_def inversion(lookup tag A m i) [2: #a] #EQ
940normalize nodelta #EQ1 destruct @eq_identifier_elim
941[ #H normalize nodelta >H @lookup_add_hit
942| #H normalize nodelta @lookup_add_miss assumption
943]
944qed.
945
946lemma mem_set_restrict : ∀tag,A,B.∀a : identifier_map tag A.∀b : identifier_map tag B.
947∀i.i ∈ a ∩ b = (i ∈ a ∧ i ∈ b).
948#tag #A #B * #a * #b  * #i normalize >lookup_opt_merge [2: %] cases(lookup_opt B i b)
949[2: #a1] normalize [2: @if_elim #_ %] cases(lookup_opt A i a) [2: #a2] normalize %
950qed.
951(*
952lemma merge_eq : ∀A.∀p : positive_map A.∀choice. merge
953*)
954(*
955lemma add_restrict : ∀tag,A,B.∀a : identifier_map tag A. ∀b : identifier_map tag B.
956∀i,v.i∈b → add tag A (a ∩ b) i v = (add tag A a i v) ∩ b.
957#tag #A #B * #a * #b * #i #v normalize inversion(lookup_opt B i b) normalize [#_ *]
958#v1 #EQv1 * @eq_f lapply EQv1 lapply v1 lapply a lapply b -a -b -v1 elim i normalize
959[ * normalize [#b #v #EQ destruct] #opt_a #l #r *
960  [#v #EQ destruct normalize %] #opt_b #l1 #r1 #v #EQ destruct normalize cases opt_b
961  normalize [2: #x %] cases(merge A B A ? l1 l) normalize [2: #opt_a2 #l2 #r2 %]
962  cases(merge A B A ? r1 r) //
963|*: #x #IH * [2,4: #opt_b #l1 #r1] #p1 normalize [3,4: #i #EQ destruct] cases p1 -p1
964    [2,4: #opt_a #l2 #r2] normalize #v #H cases opt_b [2,4,6,8: #b] normalize
965    [1,2,5,6: <IH try assumption [1,2: cases opt_a [2,4: #a] normalize try %]
966     cases(merge A B A ? l2 l1) normalize // lapply H [1,4: cases r1 |*: cases l1]
967     normalize [1,3,5,7,9,11: #EQ destruct] #opt_b4 #l4 #r4 cases x normalize
968     [1,4,7,10,13,16: #EQ destruct normalize // cases(merge A B A ? ? ?) normalize //]
969     #x #H normalize cases(merge A B A ? ? ?) normalize //
970    |*: <IH try assumption
971       [1,3: cases(map_opt ? ? ? l1) normalize // lapply H cases r1 normalize
972            [1,3: #EQ destruct] #opt_b2 #l2 #r2 cases x [1,4: //] #x normalize //
973       |*: lapply H cases x normalize [2,3,5,6: #y] cases l1 normalize
974          [1,3,5,7,9,11: #EQ destruct] #opt_b2 #l2 #r2 #H //
975       ]
976   ]
977]
978qed.
979
980lemma update_restrict : ∀tag,A,B.∀a : identifier_map tag A.∀b : identifier_map tag B.
981∀i,v.i ∈ b → update ?? (a ∩ b) i v =
982  ! a' ← update ?? a i v ; return a' ∩ b.
983#tag #A #B #a #b #id #v #H
984lapply (in_map_domain … b id) >H * #ignore #EQ_lookup_b
985(*<clean_update*)
986inversion (update tag A a id v)
987[2: #e #EQ cases (update_fail_lookup ?????? EQ) #EQ1 #EQ2 destruct
988  >lookup_miss_update [%]
989  >lookup_restrict >H assumption ]
990#m' #EQ >m_return_bind
991cases (lookup_hit_update ?? (a∩b) id v ?)
992[2: >mem_set_restrict >H >(update_ok_old_lookup ?????? EQ) % ]
993#m'' >update_def >update_def in EQ; >lookup_restrict >H normalize nodelta
994cases(lookup tag A a id) normalize nodelta [#ABS destruct] #v1 #EQ #EQ'' destruct
995whd in ⊢ (??%%); @eq_f @add_restrict assumption
996qed.
997*)
998lemma add_set_minus  : ∀tag,A,B.∀a : identifier_map tag A.∀b : identifier_map tag B.
999∀i,v.¬(i ∈ b) → add tag A (a ∖ b) i v = (add tag A a i v) ∖ b.
1000#tag #A #B * #a * #b * #i #v @notb_elim @if_elim normalize [#_ *]
1001@if_elim [2: #_ *] @if_elim [#_ *] inversion(lookup_opt B i b) normalize [2: #x #_ *]
1002#H * * * * @eq_f lapply H -H lapply v -v lapply b -b lapply a -a elim i
1003[  *
1004  [ * [2: #opt_b #l #r] #v normalize in ⊢ (% → ?); #EQ destruct [2: %]
1005  normalize in ⊢ (??%%); cases (map_opt ??? l) // normalize cases(map_opt ??? r)
1006  normalize //
1007  | * [2: #a] #l #r * [2,4: #opt_b #l1 #r1] #v normalize in ⊢ (% → ?); #EQ destruct
1008    normalize [3: % |1,2: cases(merge ???? l l1) // cases(merge ???? r r1) //]
1009    cases(map_opt ??? l) normalize // cases(map_opt ??? r) //
1010  ]
1011|2,3: #x #IH * [2,4: #opt_a #l #r] * [2,4,6,8: #opt_b #l1 #r1] #v
1012      normalize in ⊢ (% → ?); #H whd in match (pm_set ????) in ⊢ (???%);
1013      whd in match (merge ??????) in ⊢ (???%);
1014      [1,2,3,4: <IH try assumption whd in match (pm_set ????) in ⊢ (??%?);
1015                whd in match (merge ??????) in ⊢ (??%?); cases opt_b normalize
1016                [2,4,6,8: #b] [5,6: cases opt_a normalize //]
1017                [1,2,3,4: cases (merge ???? l l1) normalize [2,4,6,8: #opt_a2 #l2 #r2]
1018                          // cases (merge ???? r r1) normalize
1019                          [2,4,6,8,10,12: #opt_a3 #l3 #r3] inversion(pm_set ????)
1020                          normalize // cases x
1021                          [2,3,5,6,8,9,11,12,14,15,17,18,20,21,23,24 : #y]
1022                          normalize #EQ destruct
1023                |*: cases(map_opt ??? l1) normalize [2,4,6,8: #opt_a2 #l2 #r2] //
1024                    cases(map_opt ??? r1) normalize [2,4,6,8,10,12: #opt_a3 #l3 #r3]
1025                    inversion(pm_set ????) normalize // cases x
1026                    [2,3,5,6,8,9,11,12,14,15,17,18,20,21,23,24 : #y]
1027                    normalize #EQ destruct
1028                ]
1029     |*: whd in match (pm_set ????) in ⊢ (??%?);
1030         whd in match (merge ??????) in ⊢ (??%?); [1,2: cases opt_a [2,4: #a]]
1031         normalize
1032         [1,2: @eq_f2 [1,4:%] | cases(map_opt ??? l) [2: #opt_a1 #l1 #r1] normalize
1033         | cases(map_opt ??? r) [2: #opt_a1 #l1 #r1] normalize]       
1034         [1,3,4: lapply(map_add tag A A (λx.x) (an_id_map … r) (an_identifier ? x) v)
1035         |2,5,6: lapply(map_add tag A A (λx.x) (an_id_map … l) (an_identifier ? x) v)
1036         |*: lapply(map_add tag A A (λx.x) (an_id_map … (pm_leaf ?)) (an_identifier ? x) v)
1037         ] normalize #EQ destruct >e0 try % [4,5: cases x [2,3,5,6: #y] normalize %]
1038           cases(map_opt ????) [2,4,6: #opt_a1 #l1 #r1] normalize
1039           inversion(pm_set ????) normalize // cases x [2,3,5,6,8,9,11,12: #y]
1040           normalize #EQ1 destruct
1041     ]
1042]
1043qed.     
1044
1045lemma update_set_minus : ∀tag,A,B.∀a : identifier_map tag A.∀b : identifier_map tag B.
1046∀i,v.¬(i ∈ b) → update ?? (a ∖ b) i v =
1047  ! a' ← update ?? a i v ; return a' ∖ b.
1048#tag #A #B #a #b #id #v #H >update_def >lookup_set_minus @if_elim
1049[ #H1 @⊥ lapply H1 lapply H @notb_elim >H1 normalize *] #_ >update_def
1050cases (lookup tag A a id) normalize [ %] #a @eq_f @add_set_minus assumption
1051qed.
1052
1053
1054record good_state_transformation
1055(prog : ertl_program)
1056(def_in : joint_closed_internal_function ERTL (prog_var_names ?? prog)) :
1057Type[0] ≝
1058{ f_lbls : label → option (list label)
1059; f_regs : label → option (list register)
1060; part_partition_f_lbls : partial_partition … f_lbls
1061; part_partion_f_regs : partial_partition … f_regs
1062; freshness_lab : let def_out ≝ translate_internal … def_in in
1063     (∀l.opt_All … (All …
1064    (λlbl.¬fresh_for_univ … lbl (joint_if_luniverse … def_in) ∧
1065           fresh_for_univ … lbl (joint_if_luniverse … def_out))) (f_lbls l))
1066; freshness_regs : let def_out ≝ translate_internal … def_in in
1067  (∀l.opt_All … (All …
1068    (λreg.¬fresh_for_univ … reg (joint_if_runiverse … def_in) ∧
1069           fresh_for_univ … reg (joint_if_runiverse … def_out))) (f_regs l))
1070; multi_fetch_ok : let def_out ≝ translate_internal … def_in in
1071  ∀f_step,f_fin.∀l,s.stmt_at … (joint_if_code … def_in) l = Some ? s →
1072  ∃lbls,regs.f_lbls l = Some ? lbls ∧ f_regs l = Some ? regs ∧
1073  match s with
1074  [ sequential s' nxt ⇒
1075    l ~❨f_step l s', lbls, regs❩~> nxt in joint_if_code … def_out
1076  | final s' ⇒
1077    l ~❨f_fin l s', lbls, regs❩~> it in joint_if_code … def_out
1078  | FCOND abs _ _ _ ⇒ Ⓧabs
1079  ]
1080}.
1081
1082definition get_internal_function_from_ident :
1083∀ p: sem_params. ∀ globals : list ident . ∀ge : genv_t (joint_function p globals).
1084ident → option (joint_closed_internal_function p globals) ≝
1085λp,globals,ge,id.
1086! bl  ← (find_symbol (joint_function p globals) ge id);
1087! bl' ← (code_block_of_block bl);
1088! 〈f,fn〉 ← res_to_opt … (fetch_internal_function ? ge bl');
1089return fn.
1090
1091definition get_sigma_from_good_state :
1092∀prog : ertl_program.
1093(∀ fn : joint_closed_internal_function ERTL (prog_var_names ?? prog).
1094good_state_transformation prog fn) → sigma_map prog ≝
1095λprog,good,fn,searched.
1096!〈res,s〉 ← find ?? (joint_if_code … fn)
1097                (λlbl.λ_. match (f_lbls … (good fn)) lbl with
1098                          [None ⇒ false
1099                          |Some lbls ⇒
1100                             match lbls with
1101                                [nil ⇒ eq_identifier … searched lbl
1102                                |cons hd tl ⇒ let last ≝ last_ne … «hd::tl,I» in
1103                                          eq_identifier … searched last
1104                                ]
1105                          ]);
1106return res.
1107
1108
1109definition sigma_frames : ∀prog : ertl_program.
1110(∀fn.good_state_transformation prog fn) →
1111list (register_env beval × ident) → (list (register_env beval × ident)) ≝
1112λprog,good,frms.
1113let sigma ≝ get_sigma_from_good_state … good in
1114foldr ??
1115(λx,tl.let 〈reg_env,id〉 ≝ x in
1116       match get_internal_function_from_ident
1117                  ERTL_semantics (prog_var_names … prog)
1118                  (globalenv_noinit … prog) id with
1119       [Some fn ⇒
1120  〈(sigma_register_env prog sigma reg_env
1121       (added_registers … fn (f_regs … (good fn)))),id〉 :: tl
1122       |None ⇒ [ ]
1123       ]) ([ ]) frms.
1124
1125
1126(*
1127lemma sigma_empty_frames_commute :
1128∀prog : ertl_program. ∀ sigma : (sigma_map prog).
1129∃prf.
1130sigma_frames prog sigma [] prf = [].
1131#p #s % normalize %
1132qed.
1133
1134
1135let rec sigma_bit_vector_trie_opt (prog : ertl_program)
1136(sigma : (sigma_map prog)) (n : nat) (t : BitVectorTrie beval n)
1137on t : option … (BitVectorTrie beval n) ≝
1138match t with
1139  [Leaf bv ⇒ ! bv' ← (sigma_beval_opt prog sigma bv);
1140                   return Leaf … bv'
1141  |Node n1 b1 b2 ⇒ ! b1' ← (sigma_bit_vector_trie_opt prog sigma n1 b1);
1142                   ! b2' ← (sigma_bit_vector_trie_opt prog sigma n1 b2);
1143                   return Node … n1 b1' b2'
1144  |Stub n1 ⇒  return Stub … n1
1145  ].
1146
1147
1148definition well_formed_hw_register_env :
1149∀ prog : ertl_program. ∀ sigma : (sigma_map prog).
1150hw_register_env → Prop ≝
1151λprog,sigma,regs.sigma_bit_vector_trie_opt prog sigma 6 (reg_env … regs) ≠ None ?.
1152*)
1153
1154
1155include "common/BitVectorTrieMap.ma".
1156
1157definition sigma_hw_register_env :
1158∀prog: ertl_program. ∀sigma : (sigma_map prog).
1159hw_register_env → hw_register_env ≝
1160λprog,sigma,h_reg.mk_hw_register_env
1161(map ? ? (sigma_beval prog sigma) 6 (reg_env … h_reg)) (other_bit … h_reg).
1162
1163
1164definition sigma_regs :
1165∀prog : ertl_program. ∀sigma : (sigma_map prog).
1166(register_env beval)×hw_register_env→ list register →
1167(register_env beval)×hw_register_env ≝
1168λprog,sigma,regs,ids.let 〈x,y〉≝ regs in
1169      〈sigma_register_env prog sigma x ids,
1170       sigma_hw_register_env prog sigma y〉.
1171(*
1172lemma sigma_empty_regsT_commute :
1173∀prog : ertl_program. ∀sigma : (sigma_map prog).
1174∀ptr.∃ prf.
1175  empty_regsT ERTLptr_semantics ptr =
1176  sigma_regs prog sigma (empty_regsT ERTL_semantics ptr) prf.
1177#prog #sigma #ptr %
1178[ @hide_prf whd in match well_formed_regs; normalize nodelta %
1179 [whd in match well_formed_ertl_psd_env; normalize nodelta #id #bv
1180  normalize in ⊢ (%→?); #EQ destruct
1181 | normalize % #EQ destruct
1182 ]
1183| % ]
1184qed.
1185
1186axiom sigma_load_sp_commute :
1187∀prog : ertl_program.∀sigma : (sigma_map prog).
1188∀regs,ptr.
1189load_sp ERTL_semantics regs = return ptr
1190→ ∃prf.
1191load_sp ERTLptr_semantics (sigma_regs prog sigma regs prf) = return ptr.
1192
1193axiom sigma_save_sp_commute :
1194∀prog : ertl_program. ∀sigma : (sigma_map prog).
1195∀reg,ptr,prf1. ∃prf2.
1196save_sp ERTLptr_semantics (sigma_regs prog sigma reg prf1) ptr =
1197sigma_regs prog sigma (save_sp ERTL_semantics reg ptr) prf2.
1198
1199definition well_formed_state :
1200∀prog : ertl_program. ∀sigma : sigma_map prog.
1201state ERTL_semantics → Prop ≝
1202λprog,sigma,st.
1203well_formed_frames prog sigma (st_frms … st) ∧
1204sigma_is_opt prog sigma (istack … st) ≠ None ? ∧
1205well_formed_regs prog sigma (regs … st) ∧
1206well_formed_mem prog sigma (m … st).
1207*)
1208
1209definition sigma_state : ∀prog : ertl_program.
1210(∀fn.good_state_transformation prog fn) →
1211 state ERTLptr_semantics → list register →
1212 state ERTL_semantics ≝
1213λprog,good,st,ids.
1214let sigma ≝ get_sigma_from_good_state … good in
1215mk_state ?
1216  (sigma_frames prog good (st_frms ERTLptr_semantics st))
1217  (sigma_is ? sigma (istack … st))
1218  (carry … st)
1219  (sigma_regs ? sigma (regs … st) ids)
1220  (sigma_mem ? sigma (m … st)).
1221
1222
1223definition dummy_state : state ERTL_semantics ≝
1224mk_state ERTL_semantics
1225   [ ] empty_is BBundef 〈empty_map ? ?,mk_hw_register_env … (Stub …) BBundef〉 empty.
1226   
1227definition dummy_state_pc : state_pc ERTL_semantics ≝
1228mk_state_pc ? dummy_state (null_pc one) (null_pc one).
1229
1230definition sigma_state_pc :
1231∀prog : ertl_program.
1232(∀fn.good_state_transformation prog fn) →
1233state_pc ERTLptr_semantics →
1234 state_pc ERTL_semantics ≝
1235λprog,good,st.
1236  let sigma ≝ get_sigma_from_good_state … good in
1237  let ge ≝ globalenv_noinit … prog in
1238  if eqZb       (block_id (pc_block (pc … st))) (-1) then (* check for dummy pc *)
1239    dummy_state_pc
1240  else
1241  match (fetch_internal_function (joint_closed_internal_function ERTL
1242         (prog_var_names (joint_function ERTL) ℕ prog)) ge (pc_block (pc … st))) with
1243   [OK x ⇒ let 〈i,fd〉 ≝ x in
1244      mk_state_pc ?
1245       (sigma_state prog good st (added_registers … fd (f_regs … (good fd))))
1246       (pc … st) (sigma_stored_pc prog sigma (last_pop … st))
1247   |Error msg ⇒ dummy_state_pc].
1248
1249
1250definition ERTLptrStatusSimulation :
1251∀ prog : ertl_program.
1252let trans_prog ≝ ertl_to_ertlptr prog in
1253∀stack_sizes.(∀fn.good_state_transformation prog fn) →
1254status_rel (ERTL_status prog stack_sizes) (ERTLptr_status trans_prog stack_sizes) ≝
1255λprog,stack_sizes,good.
1256  let trans_prog ≝ ertl_to_ertlptr prog in
1257    mk_status_rel ??
1258    (* sem_rel ≝ *) (λs1:ERTL_status prog stack_sizes
1259       .λs2:ERTLptr_status trans_prog stack_sizes
1260        .s1=sigma_state_pc prog good s2)
1261    (* call_rel ≝ *) 
1262          (λs1:Σs:ERTL_status prog stack_sizes
1263               .as_classifier (ERTL_status prog stack_sizes) s cl_call
1264       .λs2:Σs:ERTLptr_status trans_prog stack_sizes
1265                .as_classifier (ERTLptr_status trans_prog stack_sizes) s cl_call
1266        .let sigma ≝ get_sigma_from_good_state … good in
1267        pc (mk_prog_params ERTL_semantics prog stack_sizes) s1
1268         =sigma_stored_pc prog sigma
1269          (pc
1270           (mk_prog_params ERTLptr_semantics (ertl_to_ertlptr prog) stack_sizes)
1271           s2))
1272    (* sim_final ≝ *) ?.
1273cases daemon
1274qed.
1275
1276lemma fetch_function_no_minus_one :
1277  ∀F,V,i,p,bl.
1278  block_id (pi1 … bl) = -1 →
1279  fetch_function … (globalenv (λvars.fundef (F vars)) V i p)
1280    bl = Error … [MSG BadFunction].
1281 #F#V#i#p ** #r #id #EQ1 destruct
1282  whd in match fetch_function; normalize nodelta
1283  >globalenv_no_minus_one
1284  cases (symbol_for_block ???) normalize //
1285qed.
1286 
1287lemma fetch_function_no_zero :
1288 ∀F,V,i,p,bl.
1289  block_id (pi1 … bl) = 0 →
1290  fetch_function … (globalenv (λvars.fundef (F vars)) V i p)
1291    bl = Error … [MSG BadFunction].
1292 #F#V#i#p ** #r #id #EQ1 destruct
1293  whd in match fetch_function; normalize nodelta
1294  >globalenv_no_zero
1295  cases (symbol_for_block ???) normalize //
1296qed.
1297
1298(*DOPPIONI dei LEMMI in LINEARISE_PROOF*)
1299lemma symbol_for_block_match:
1300    ∀M:matching.∀initV,initW.
1301     (∀v,w. match_var_entry M v w →
1302      size_init_data_list (initV (\snd v)) = size_init_data_list (initW (\snd w))) →
1303    ∀p: program (m_A M) (m_V M). ∀p': program (m_B M) (m_W M).
1304    ∀MATCH:match_program … M p p'.
1305    ∀b: block.
1306    symbol_for_block … (globalenv … initW p') b =
1307    symbol_for_block … (globalenv … initV p) b.
1308* #A #B #V #W #match_fn #match_var #initV #initW #H
1309#p #p' * #Mvars #Mfn #Mmain
1310#b
1311whd in match symbol_for_block; normalize nodelta
1312whd in match globalenv in ⊢ (???%); normalize nodelta
1313whd in match (globalenv_allocmem ????);
1314change with (add_globals ?????) in match (foldl ?????);
1315>(proj1 … (add_globals_match … initW … Mvars))
1316[ % |*:]
1317[ * #idr #v * #idr' #w #MVE %
1318  [ inversion MVE
1319    #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 destruct %
1320  | @(H … MVE)
1321  ]
1322| @(matching_fns_get_same_blocks … Mfn)
1323  #f #g @match_funct_entry_id
1324]
1325qed.
1326
1327lemma symbol_for_block_transf :
1328 ∀A,B,V,init.∀prog_in : program A V.
1329 ∀trans : ∀vars.A vars → B vars.
1330 let prog_out ≝ transform_program … prog_in trans in
1331 ∀bl.
1332 symbol_for_block … (globalenv … init prog_out) bl =
1333 symbol_for_block … (globalenv … init prog_in) bl.
1334#A #B #V #iV #p #tf @(symbol_for_block_match … (transform_program_match … tf ?))
1335#v0 #w0 * //
1336qed.
1337
1338lemma fetch_function_transf :
1339 ∀A,B,V,init.∀prog_in : program A V.
1340 ∀trans : ∀vars.A vars → B vars.
1341 let prog_out ≝ transform_program … prog_in trans in
1342 ∀bl,i,f.
1343 fetch_function … (globalenv … init prog_in) bl =
1344  return 〈i, f〉
1345→ fetch_function … (globalenv … init prog_out) bl =
1346  return 〈i, trans … f〉.
1347#A #B #V #init #prog_in #trans #bl #i #f
1348 whd in match fetch_function; normalize nodelta
1349 #H lapply (opt_eq_from_res ???? H) -H
1350 #H @('bind_inversion H) -H #id #eq_symbol_for_block
1351 #H @('bind_inversion H) -H #fd #eq_find_funct
1352 whd in ⊢ (??%?→?); #EQ destruct(EQ)
1353 >(symbol_for_block_transf … trans) >eq_symbol_for_block >m_return_bind
1354 >(find_funct_ptr_transf A B …  eq_find_funct) %
1355qed.
1356
1357
1358lemma fetch_internal_function_transf :
1359 ∀A,B.∀prog_in : program (λvars.fundef (A vars)) ℕ.
1360 ∀trans : ∀vars.A vars → B vars.
1361 let prog_out ≝ transform_program … prog_in (λvars.transf_fundef … (trans vars)) in
1362 ∀bl,i,f.
1363 fetch_internal_function … (globalenv_noinit … prog_in) bl =
1364  return 〈i, f〉
1365→ fetch_internal_function … (globalenv_noinit … prog_out) bl =
1366  return 〈i, trans … f〉.
1367#A #B #prog #trans #bl #i #f
1368 whd in match fetch_internal_function; normalize nodelta
1369 #H @('bind_inversion H) * #id * #fd normalize nodelta #EQfetch
1370 whd in ⊢ (??%%→?); #EQ destruct(EQ)
1371 >(fetch_function_transf … EQfetch) %
1372qed.
1373
1374(*
1375definition good_local_sigma :
1376  ∀globals.
1377  ∀g:codeT ERTLptr globals.
1378  (Σl.bool_to_Prop (code_has_label … g l)) →
1379  codeT ERTL globals →
1380  (label → option label) → Prop ≝
1381  λglobals,g,c,sigma.
1382    ∀l,l'.sigma l = Some ? l' →
1383      ∃s. stmt_at … g l = Some ? s ∧
1384          All ? (λl.sigma l ≠ None ?) (stmt_labels … s) ∧
1385          (match s with
1386           [ sequential s' nxt ⇒
1387             match s' with
1388             [ step_seq _ ⇒
1389               (stmt_at … c n = Some ? (sequential … s' it)) ∧
1390                  ((sigma nxt = Some ? (S n)) ∨
1391                   (stmt_at … c (S n) = Some ? (GOTO … nxt)))
1392             | COND a ltrue ⇒
1393               (stmt_at … c n = Some ? (sequential … s' it) ∧ sigma nxt = Some ? (S n)) ∨
1394               (stmt_at … c n = Some ? (FCOND … I a ltrue nxt))
1395             ]
1396           | final s' ⇒
1397             stmt_at … c n = Some ? (final … s')
1398           | FCOND abs _ _ _ ⇒ Ⓧabs
1399           ]).
1400 
1401*)
1402
1403lemma ps_reg_retrieve_ok :  ∀prog : ertl_program.
1404∀sigma : sigma_map prog. ∀r,restr.
1405preserving1 ?? res_preserve1 …
1406     (λregs.sigma_regs prog sigma regs restr)
1407     (sigma_beval prog sigma)
1408     (λregs.ps_reg_retrieve regs r)
1409     (λregs.ps_reg_retrieve regs r).
1410#prog #sigma #r #restr * #psd_r #hw_r whd in match ps_reg_retrieve;
1411whd in match reg_retrieve; normalize nodelta @opt_to_res_preserve1
1412whd in match sigma_regs; whd in match sigma_register_env; normalize nodelta
1413>lookup_set_minus @if_elim [ #_ @opt_preserve_none1] #id_r_not_in
1414>(lookup_map ?? RegisterTag ???) #bv #H @('bind_inversion H) -H #bv1
1415#bv1_spec whd in ⊢ (??%? → ?); #EQ destruct %{bv1} % // >bv1_spec %
1416qed.
1417
1418lemma hw_reg_retrieve_ok : ∀prog : ertl_program.
1419∀sigma : sigma_map prog. ∀r,restr.
1420preserving1 ?? res_preserve1 …
1421    (λregs.sigma_regs prog sigma regs restr)
1422    (sigma_beval prog sigma)
1423    (λregs.hw_reg_retrieve regs r)
1424    (λregs.hw_reg_retrieve regs r).
1425#prog #sigma #r #restr * #psd_r * #hw_r #b whd in match hw_reg_retrieve;
1426whd in match hwreg_retrieve; normalize nodelta whd in match sigma_regs;
1427whd in match sigma_hw_register_env; normalize nodelta
1428change with (sigma_beval prog sigma BVundef) in ⊢ (???????(??(?????%))?);
1429#bv >lookup_map whd in ⊢ (???% → ?); #EQ destruct
1430%{(lookup beval 6 (bitvector_of_register r) hw_r BVundef)}
1431% //
1432qed.
1433
1434
1435lemma ps_reg_store_ok : ∀prog : ertl_program.
1436∀sigma : sigma_map prog. ∀r,restr.
1437preserving21 ?? res_preserve1 …
1438   (sigma_beval prog sigma)
1439   (λregs.sigma_regs prog sigma regs restr)
1440   (λregs.sigma_regs prog sigma regs restr)
1441   (ps_reg_store r)
1442   (ps_reg_store r).
1443#prog #sigma #r #restr whd in match ps_reg_store; normalize nodelta
1444#bv * #psd_r #hw_r @mfr_bind1
1445[ @(λr.sigma_register_env prog sigma r restr)
1446| whd in match reg_store; whd in match sigma_regs; normalize nodelta
1447  #x #x_spec lapply(update_ok_to_lookup ?????? x_spec) * * #_ #EQpsd #_
1448  lapply x_spec -x_spec lapply EQpsd -EQpsd whd in match sigma_register_env;
1449  normalize nodelta >lookup_set_minus @if_elim [ #_ * #H @⊥ @H %]
1450  #id_not_in #_ >update_set_minus [2: assumption] #H @('bind_inversion H) -H
1451  #x0 >map_update_commute #H @('bind_inversion H) -H #x1 #x1_spec
1452  whd in ⊢ (??%% → ??%% → ?); #EQ1 #EQ2 destruct %{x1} % //
1453| #x * #psd_r' #hw_r' whd in match sigma_regs; normalize nodelta
1454  whd in ⊢ (???% → ?); #EQ destruct %{〈x,hw_r〉} % //
1455]
1456qed.
1457
1458
1459lemma hw_reg_store_ok : ∀prog : ertl_program.
1460∀sigma : sigma_map prog. ∀r,restr.
1461preserving21 ?? res_preserve1 …
1462   (sigma_beval prog sigma)
1463   (λregs.sigma_regs prog sigma regs restr)
1464   (λregs.sigma_regs prog sigma regs restr)
1465   (hw_reg_store r)
1466   (hw_reg_store r).
1467#prog #sigma #r #restr whd in match hw_reg_store; normalize nodelta
1468#bv * #psd_r * #hw_r #b whd in match hwreg_store; whd in match sigma_regs; normalize nodelta
1469whd in match sigma_hw_register_env; normalize nodelta <insert_map * #psd_r'
1470* #hw_r' #b' whd in ⊢ (???% → ?); #EQ destruct % [2: % [%] % |]
1471qed.
1472
1473
1474lemma ertl_eval_move_ok : ∀prog : ertl_program.
1475∀sigma : sigma_map prog. ∀ restr,pm.
1476preserving1 ?? res_preserve1 …
1477     (λregs.sigma_regs prog sigma regs restr)
1478     (λregs.sigma_regs prog sigma regs restr)
1479     (λregs.ertl_eval_move regs pm)
1480     (λregs.ertl_eval_move regs pm).
1481#prog #sigma #restr * #mv_dst #arg_dst #pm whd in match ertl_eval_move;
1482normalize nodelta @mfr_bind1 [@(sigma_beval prog sigma)
1483| cases arg_dst normalize nodelta
1484  [2: #b change with (return sigma_beval prog sigma (BVByte b)) in ⊢ (???????%?);
1485      @mfr_return1]
1486  * #r normalize nodelta [@ps_reg_retrieve_ok| @hw_reg_retrieve_ok]
1487| #bv cases mv_dst #r normalize nodelta [@ps_reg_store_ok | @hw_reg_store_ok]
1488]
1489qed.
1490
1491lemma ps_arg_retrieve_ok : ∀prog : ertl_program.
1492∀sigma : sigma_map prog. ∀a,restr.
1493preserving1 ?? res_preserve1 …
1494    (λregs.sigma_regs prog sigma regs restr)
1495    (sigma_beval prog sigma)
1496    (λregs.ps_arg_retrieve regs a)
1497    (λregs.ps_arg_retrieve regs a).
1498#prog #sigma #a #restr whd in match ps_arg_retrieve; normalize nodelta cases a -a
1499normalize nodelta [#r | #b ] #regs
1500[ @ps_reg_retrieve_ok
1501| change with (return sigma_beval prog sigma (BVByte b)) in ⊢ (???????%?);
1502  @mfr_return1
1503]
1504qed.
1505
1506lemma pop_ok :
1507∀prog : ertl_program.
1508∀good : (∀fn.good_state_transformation prog fn).
1509∀restr.
1510preserving1 ?? res_preserve1 ????
1511   (λst.sigma_state prog good st restr)
1512   (λx.let 〈bv,st〉 ≝ x in
1513      〈let sigma ≝ get_sigma_from_good_state … good in
1514       sigma_beval prog sigma bv,
1515       sigma_state prog good st restr〉)
1516   (pop ERTL_semantics)
1517   (pop ERTLptr_semantics).
1518#prog #good #restr whd in match pop; normalize nodelta #st @mfr_bind1
1519[@(λx.let 〈bv,is〉 ≝ x in
1520      let sigma ≝ get_sigma_from_good_state … good in
1521     〈sigma_beval prog sigma bv,
1522      sigma_is prog sigma is 〉)
1523| whd in match is_pop; normalize nodelta whd in match sigma_state; normalize nodelta
1524  cases(istack ? st) normalize nodelta
1525  [@res_preserve_error1
1526  |2,3: #bv1 [2: #bv2] * #bv3 #is1 whd in ⊢ (??%% → ?); #EQ destruct
1527        % [2,4: % [1,3: %|*: %] |*:]
1528  ]
1529| * #bv #is * #bv1 #st whd in ⊢ (??%% → ?); #EQ destruct % [2: % [%] %|]
1530]
1531qed.
1532
1533lemma push_ok :
1534∀prog : ertl_program.
1535∀good : (∀fn.good_state_transformation prog fn).
1536∀restr.
1537preserving21 ?? res_preserve1 …
1538     (λst.sigma_state prog good st restr)
1539     (let sigma ≝ get_sigma_from_good_state … good in sigma_beval prog sigma)
1540     (λst.sigma_state prog good st restr)
1541     (push ERTL_semantics)
1542     (push ERTLptr_semantics).
1543#prog #good #restr whd in match push; normalize nodelta #st #bv @mfr_bind1
1544[ @(let sigma ≝ get_sigma_from_good_state … good in sigma_is ? sigma)
1545| whd in match is_push; normalize nodelta whd in match sigma_state; normalize nodelta
1546 cases (istack ? st) [2,3: #bv [2: #bv']]  whd in match sigma_is in ⊢ (???????%?);
1547 normalize nodelta [@res_preserve_error1] @mfr_return_eq1 %
1548| #is @mfr_return_eq1 %
1549]
1550qed.
1551
1552lemma be_opaccs_ok :
1553∀prog : ertl_program. ∀sigma : sigma_map prog.
1554∀ op.
1555preserving21 ?? res_preserve1 ??????
1556    (sigma_beval prog sigma)
1557    (sigma_beval prog sigma)
1558    (λx.let 〈bv1,bv2〉 ≝ x in
1559           〈sigma_beval prog sigma bv1,
1560            sigma_beval prog sigma bv2〉)
1561    (be_opaccs op)
1562    (be_opaccs op).
1563#prog #sigma #op #bv #bv1
1564whd in match be_opaccs; normalize nodelta @mfr_bind1
1565[ @(λx.x)
1566| cases bv
1567  [ | | #ptr1 #ptr2 #p | #by | #p | #ptr #p | #pc1 #p1]
1568  whd in match Byte_of_val; normalize nodelta
1569  try @res_preserve_error1 [ #x whd in ⊢ (???% → ?); #EQ destruct %{x} % //]
1570  whd in match sigma_beval; normalize nodelta cases (sigma_pc_opt ? ? ?)
1571  normalize nodelta [2: #pc] @res_preserve_error1
1572| #by @mfr_bind1
1573  [ @(λx.x)
1574  | cases bv1
1575    [ | | #ptr1 #ptr2 #p | #by | #p | #ptr #p | #pc1 #p1]
1576    whd in match Byte_of_val; normalize nodelta
1577    try @res_preserve_error1 [ #x whd in ⊢ (???% → ?); #EQ destruct %{x} % //]
1578    whd in match sigma_beval; normalize nodelta cases (sigma_pc_opt ? ? ?)
1579    normalize nodelta [2: #pc] @res_preserve_error1
1580 | #by1 * #bv2 #bv3 cases(opaccs eval op by by1) #by' #by1' normalize nodelta
1581   whd in ⊢ (??%% → ?); #EQ destruct % [2: % [%] % |]
1582qed.
1583
1584lemma be_op1_ok : ∀prog : ertl_program. ∀sigma : sigma_map prog.
1585∀ op.
1586preserving1 ?? res_preserve1 …
1587     (sigma_beval prog sigma)
1588     (sigma_beval prog sigma)
1589     (be_op1 op)
1590     (be_op1 op).
1591#prog #sigma #o #bv whd in match be_op1; normalize nodelta @mfr_bind1
1592[ @(λx.x)
1593| cases bv
1594  [ | | #ptr1 #ptr2 #p | #by | #p | #ptr #p | #pc1 #p1]
1595  whd in match Byte_of_val; whd in match sigma_beval; normalize nodelta
1596  try @res_preserve_error1 [ @mfr_return_eq1 %]
1597  cases(sigma_pc_opt prog sigma pc1) [2: #pc2] normalize nodelta
1598  @res_preserve_error1
1599| #by @mfr_return_eq1 %
1600]
1601qed.
1602
1603lemma res_preserve_error11 : ∀X,Y,F,e,n. (∃e'.n = Error … e') →
1604res_preserve1 X Y F n (Error … e).
1605#X #Y #F #e #n * #e' #n_spec >n_spec @res_preserve_error1
1606qed.
1607
1608
1609lemma be_op2_ok : ∀prog : ertl_program. ∀sigma : sigma_map prog.
1610∀ b,op.
1611preserving21 ?? res_preserve1 …
1612     (sigma_beval prog sigma)
1613     (sigma_beval prog sigma)
1614     (λx.let 〈bv,b〉≝ x in 〈sigma_beval prog sigma bv,b〉)
1615     (be_op2 b op)
1616     (be_op2 b op).
1617#prog #sigma #b #op #bv #bv1 whd in match be_op2; normalize nodelta
1618cases bv
1619[ | | #ptr1 #ptr2 #p | #by | #p | #ptr #p | #pc1 #p1]
1620normalize nodelta [@res_preserve_error1] whd in match sigma_beval;
1621normalize nodelta
1622cases bv1
1623[1,2,8,9,15,16,22,23,29,30,36,37:
1624|3,10,17,24,31,38: #ptr1' #ptr2' #p'
1625|4,11,18,25,32,39: #by'
1626|5,12,19,26,33,40: #p'
1627|6,13,20,27,34,41: #ptr' #p'
1628|7,14,21,28,35,42: #pc1' #p1'
1629]
1630normalize nodelta try @res_preserve_error1
1631[4,5,8,13,16,20,21,22,23,24,25,26 : @res_preserve_error11 %
1632   [2,4,6,8,10,12,14,16,18,20,22,24: cases(sigma_pc_opt ???) try % #pc2 %
1633   |*:]
1634|*: cases op normalize nodelta
1635    try @res_preserve_error1 try( @mfr_return_eq1 %)
1636    [1,2,12,13,16,17,18: @if_elim #_ try @res_preserve_error1
1637                         try( @mfr_return_eq1 %)
1638                         [ @if_elim #_ @mfr_return_eq1 %
1639                         | cases(ptype ptr) normalize nodelta
1640                           [2: @res_preserve_error1] @mfr_bind1
1641                           [ @(λx.x)
1642                           | whd in match Bit_of_val; normalize nodelta
1643                             cases b [#bo|| #bo #ptr'' #p'' #bit_v]
1644                             normalize nodelta [2,3: @res_preserve_error1]
1645                             @mfr_return_eq1 %
1646                           | #bi cases(op2 ?????) #by #bi1 normalize nodelta
1647                             @mfr_return_eq1 %
1648                           ]
1649                         | cases(ptype ptr) normalize nodelta @res_preserve_error1
1650                         ]
1651    |3,4,5,6,7,8: @mfr_bind1
1652        [1,4,7,10,13,16: @(λx.x)
1653        |2,5,8,11,14,17: whd in match Bit_of_val; normalize nodelta
1654                         cases b [1,4,7,10,13,16: #bo|
1655                                 |2,5,8,11,14,17:
1656                                 |3,6,9,12,15,18: #bo #ptr'' #p'' #bit_v
1657                                 ] normalize nodelta try @res_preserve_error1
1658                                 @mfr_return_eq1 %
1659       |3,6,9,12,15,18: #bi cases(op2 ?????) #by #bi1 normalize nodelta
1660                        @mfr_return_eq1 %
1661       ]
1662    |*: whd in match be_add_sub_byte; normalize nodelta
1663        [1,2,3: cases(ptype ptr) normalize nodelta [2,4,6: @res_preserve_error1]
1664                cases p * [2,4,6: #p_no] #prf normalize nodelta
1665                [@res_preserve_error1
1666                |2,3: cases b [1,4: #bo|2,5: |3,6:  #bo #ptr'' #p'' #bit_v]
1667                      normalize nodelta [1,2,3,4: @res_preserve_error1]
1668                      @if_elim #_ [2,4: @res_preserve_error1]
1669                      @If_elim #INUTILE [2,4: @res_preserve_error1]
1670                      @pair_elim #a1 #a2 #_ normalize nodelta
1671                      @mfr_return_eq1 %
1672                |*: @mfr_bind1
1673                  [1,4,7: @(λx.x)
1674                  |2,5,8: whd in match Bit_of_val; normalize nodelta
1675                          [@mfr_return_eq1 %] cases b
1676                          [1,4: #bo|2,5: |3,6:  #bo #ptr'' #p'' #bit_v]
1677                          normalize nodelta [3,4,5,6: @res_preserve_error1]
1678                          @mfr_return_eq1 %
1679                  |3,6,9: * normalize nodelta [1,3,5: @res_preserve_error1]
1680                          cases(op2 ?????) #a1 #a2 normalize nodelta
1681                          @mfr_return_eq1 %
1682                  ]
1683               ]
1684         |*: cases(ptype ptr') normalize nodelta [2,4: @res_preserve_error1]
1685             cases p' * [2,4: #part_no] #prf normalize nodelta
1686             [ @res_preserve_error1
1687             | cases b [#bo|| #bo #ptr'' #p'' #bit_v]
1688               normalize nodelta [1,2: @res_preserve_error1] @if_elim #_
1689               [2: @res_preserve_error1] @If_elim #INUTILE [2: @res_preserve_error1]
1690               @pair_elim #a1 #a2 #_ normalize nodelta @mfr_return_eq1 %
1691             |*: @mfr_bind1
1692                [1,4: @(λx.x)
1693                |2,5: whd in match Bit_of_val; normalize nodelta [ @mfr_return_eq1 %]
1694                      cases b [#bo|| #bo #ptr'' #p'' #bit_v] normalize nodelta
1695                      [2,3: @res_preserve_error1] @mfr_return_eq1 %
1696                |3,6: * normalize nodelta [1,3: @res_preserve_error1]   
1697                      cases(op2 ?????) #a1 #a2 normalize nodelta
1698                      @mfr_return_eq1 %
1699                ]
1700              ]
1701          ]
1702      ]
1703]
1704qed.
1705
1706lemma pointer_of_address_ok : ∀prog : ertl_program. ∀sigma : sigma_map prog.
1707preserving1 … res_preserve1 …
1708     (λx.let 〈bv1,bv2〉 ≝ x in〈sigma_beval prog sigma bv1,
1709           sigma_beval prog sigma bv2〉)
1710     (λx.x)
1711     pointer_of_address pointer_of_address.
1712#prog #sigma * #bv1 #bv2 whd in match pointer_of_address;
1713whd in match pointer_of_bevals; normalize nodelta
1714cases bv1 normalize nodelta
1715[ | | #ptr1 #ptr2 #p | #by | #p | #ptr #p | #pc1 #p1]
1716try @res_preserve_error1
1717[ cases bv2 [ | | #ptr1' #ptr2' #p' | #by' | #p' | #ptr' #p' | #pc1' #p1']
1718  normalize nodelta
1719  [1,2,3,4,5: @res_preserve_error1
1720  | @if_elim #_ [ @mfr_return_eq1 % | @res_preserve_error1]
1721  ]
1722] whd in match sigma_beval; normalize nodelta cases(sigma_pc_opt ???)
1723  [2,4: #pc4] normalize nodelta @res_preserve_error1
1724qed.
1725
1726lemma beloadv_ok : ∀prog : ertl_program. ∀sigma : sigma_map prog.
1727∀ptr.
1728preserving1 … opt_preserve1 …
1729     (sigma_mem prog sigma)
1730     (sigma_beval prog sigma)
1731     (λm.beloadv m ptr)
1732     (λm.beloadv m ptr).
1733#prog #sigma #ptr #mem whd in match beloadv; whd in match do_if_in_bounds;
1734normalize nodelta @if_elim [2: #_ @opt_preserve_none1]
1735whd in match sigma_mem in ⊢ (% → ?); normalize nodelta #Hzlb
1736@if_elim [2: #_ @opt_preserve_none1] whd in match sigma_mem in ⊢ (% → ?);
1737normalize nodelta @If_elim [2: >Hzlb * #H @⊥ @H %] #_ @andb_elim @if_elim
1738[2: #_ *] #Hzleb #Hzlb' >Hzlb normalize nodelta >Hzlb' normalize nodelta
1739@mfr_return_eq1 whd in match sigma_mem; normalize nodelta >Hzlb
1740@If_elim [2: * #H @⊥ @H %] * >Hzleb >Hzlb' @If_elim [2: * #H @⊥ @H %]
1741* %
1742qed.
1743
1744lemma bestorev_ok : ∀prog : ertl_program.∀sigma : sigma_map prog.
1745∀ptr.
1746preserving21 … opt_preserve1 …
1747    (sigma_mem prog sigma)
1748    (sigma_beval prog sigma)
1749    (sigma_mem prog sigma)
1750    (λm.bestorev m ptr)
1751    (λm.bestorev m ptr).
1752#prog #sigma #ptr #mem #bv whd in match bestorev; whd in match do_if_in_bounds;
1753normalize nodelta @if_elim [2: #_ @opt_preserve_none1]
1754whd in match sigma_mem in ⊢ (% → ?); normalize nodelta #Hzlb
1755@if_elim [2: #_ @opt_preserve_none1] @andb_elim @if_elim [2: #_ *]
1756whd in match sigma_mem in ⊢ (% → % → ?); normalize nodelta >Hzlb
1757@If_elim [2: * #H @⊥ @H %] * #Hzleb #Hzlb' normalize nodelta >Hzleb
1758>Hzlb' normalize nodelta @mfr_return_eq1 whd in ⊢ (???%); @eq_f @mem_ext_eq
1759[ #bl normalize nodelta % [%]
1760  [ whd in match sigma_mem; normalize nodelta >Hzlb @If_elim [2: * #H @⊥ @H %] *
1761    whd in match update_block; normalize nodelta @if_elim
1762    [ @eq_block_elim [2: #_ *] #EQbl * >EQbl >Hzlb @If_elim [2: * #H @⊥ @H %]
1763      * whd in match low_bound; normalize nodelta @if_elim [ #_ %]
1764      @eq_block_elim #_ * %
1765    | @eq_block_elim [#_ *] * #Hbl * @If_elim
1766      [ #Hzlb'' >Hzlb'' @If_elim [2: * #H @⊥ @H %] * whd in match low_bound;
1767        normalize nodelta @if_elim [2: #_ %] @eq_block_elim [2: #_ *] #H @⊥ @Hbl
1768        assumption
1769      | #Hzlb'' >Hzlb'' @If_elim [*] #_ %
1770      ]
1771   ]
1772 | whd in match update_block; whd in match sigma_mem; normalize nodelta
1773   @if_elim @eq_block_elim [2,3: #_ * |4: *] #Hbl #_ @If_elim
1774   [3,4: >Hbl >Hzlb * [2: #H @⊥ @H %] @If_elim [2: * #H @⊥ @H %] *
1775        whd in match high_bound; normalize nodelta @if_elim [#_ %]
1776        @eq_block_elim [ #_ *] * #H @⊥ @H %
1777   | #Hzlb'' >Hzlb'' @If_elim [2: * #H @⊥ @H %] * whd in match high_bound;
1778     normalize nodelta @if_elim [2: #_ %] @eq_block_elim [2: #_ *]
1779     #H @⊥ @Hbl assumption
1780  | #Hzlb'' >Hzlb'' @If_elim [*] #_ %
1781  ]
1782 | #z whd in match update_block; whd in match sigma_mem; normalize nodelta
1783   @if_elim @eq_block_elim [2,3: #_ * |4: *] #Hbl #_
1784   [ @If_elim #Hzlb'' >Hzlb'' [2: @If_elim * #_ %] @If_elim @andb_elim
1785     @if_elim [2: #_ *] #Hzleb' #Hzlb'''
1786     [ @If_elim [2: * #H @⊥ @H %] * whd in match low_bound; normalize nodelta
1787       @If_elim @andb_elim @if_elim [2: #_ *] @if_elim
1788       [1,3,5: @eq_block_elim [2,4,6: #_ *] #H @⊥ @Hbl assumption] #_ >Hzleb' *
1789       whd in match high_bound; normalize nodelta @if_elim
1790       [1,3: @eq_block_elim [2,4: #_ *] #H @⊥ @Hbl assumption] #_ >Hzlb'''
1791       [ * %] * #H @⊥ @H %
1792     | @If_elim * [2: #H @⊥ @H %] whd in match low_bound; normalize nodelta
1793       @if_elim [@eq_block_elim [2: #_ *] #H @⊥ @Hbl assumption] #_
1794       >Hzleb' whd in match high_bound; normalize nodelta @if_elim
1795       [@eq_block_elim [2: #_ *] #H @⊥ @Hbl assumption] #_ >Hzlb'''
1796       @If_elim [2: #_ %] *
1797     | @If_elim [2: * #H @⊥ @H %] whd in match low_bound; normalize nodelta @if_elim
1798       [@eq_block_elim [2: #_ *] #H @⊥ @Hbl assumption] #_ #_
1799       whd in match low_bound in Hzleb'; normalize nodelta in Hzleb';
1800       whd in match high_bound; normalize nodelta @if_elim
1801       [@eq_block_elim [2: #_ *] #H @⊥ @Hbl assumption] #_ @If_elim [2: #_ %]
1802       @andb_elim @if_elim [2: #_ *] #H >H in Hzleb'; *
1803     ]
1804   | whd in ⊢ (??%?); @if_elim @eqZb_elim [2,3: #_ * |4: *] #Hz *
1805       [ >Hzlb @If_elim [2: * #H @⊥ @H %] * @If_elim @andb_elim @if_elim
1806          [2: #_ *] #Hzleb' #Hzlb'' >Hbl >Hzlb @If_elim [2,4,6: * #H @⊥ @H %] #_
1807          whd in match low_bound; normalize nodelta @eq_block_elim
1808          [2,4,6: * #H @⊥ @H %] #_ normalize nodelta whd in match high_bound;
1809          normalize nodelta @eq_block_elim [2,4,6: * #H @⊥ @H %]
1810          #_ normalize nodelta
1811          [1,2: >Hzleb' >Hzlb'' @If_elim [2,3: * #H @⊥ @H %]
1812                #_ [2: %] whd in ⊢ (???(???%)); @if_elim [2: #_ %]
1813                @eqZb_elim [2: #_ *] #H @⊥ @Hz assumption
1814          | @If_elim [2: #_ %] @andb_elim @if_elim [2: #_ *] #H >H in Hzleb'; *
1815          ]
1816       | >Hbl >Hzlb @If_elim [2: * #H @⊥ @H %] * whd in match low_bound;
1817         normalize nodelta @eq_block_elim [2: * #H @⊥ @H %] #_ normalize nodelta
1818         whd in match high_bound; normalize nodelta @eq_block_elim [2: * #H @⊥ @H %]
1819         normalize nodelta >Hz >Hzleb >Hzlb' @If_elim [2: * #H @⊥ @H %] #_ #_
1820         whd in ⊢ (???(???%)); @eqZb_elim [2: * #H @⊥ @H %] #_ %
1821       ]
1822    ]
1823 ]
1824| %
1825]
1826qed.
1827
1828lemma match_reg_elim : ∀ A : Type[0]. ∀ P : A → Prop. ∀ r : region.
1829∀f : (r = XData) → A. ∀g : (r = Code) → A. (∀ prf : r = XData.P (f prf)) →
1830(∀ prf : r = Code.P (g prf)) →
1831P ((match r return λx.(r = x → ?) with
1832    [XData ⇒ f | Code ⇒ g])(refl ? r)).
1833#A #P * #f #g #H1 #H2 normalize nodelta [ @H1 | @H2]
1834qed.
1835
1836
1837lemma sp_ok : ∀prog : ertl_program.
1838∀good : (∀fn.good_state_transformation prog fn).
1839∀restr.
1840   preserving1 … res_preserve1 …
1841      (λst.sigma_state prog good st restr)
1842      (λx.x)
1843      (sp ERTL_semantics)
1844      (sp ERTLptr_semantics).
1845#prog #good #restr #st whd in match sp; normalize nodelta
1846whd in match (load_sp ??); whd in match (load_sp ??); whd in match sigma_state;
1847normalize nodelta whd in match sigma_regs; normalize nodelta
1848cases(regs ? st) #psd_r #hw_r normalize nodelta
1849inversion(pointer_of_address ?) normalize nodelta [2: #e #_ @res_preserve_error1]
1850#pt #EQ lapply(jmeq_to_eq ??? EQ) -EQ whd in match hwreg_retrieve; normalize nodelta
1851whd in match sigma_hw_register_env; normalize nodelta
1852change with (sigma_beval ? (get_sigma_from_good_state … good) BVundef) in ⊢ (??(?(???(?????%)(?????%)))? → ?);
1853>lookup_map >lookup_map
1854cases(lookup beval 6 (bitvector_of_register RegisterSPL) (reg_env hw_r) BVundef)
1855[ | | #ptr1 #ptr2 #p | #by | #p | #ptr #p | #pc1 #p1]
1856whd in match pointer_of_address; whd in match pointer_of_bevals; normalize nodelta
1857[1,2,3,4,5: #ABS destruct
1858| cases(lookup beval 6 (bitvector_of_register RegisterSPH) (reg_env hw_r) BVundef)
1859  [ | | #ptr1' #ptr2' #p' | #by' | #p' | #ptr' #p' | #pc1' #p1']
1860  whd in match sigma_beval; normalize nodelta
1861  [1,2,3,4,5: #ABS destruct
1862  | @if_elim [2: #_ #ABS destruct] #H whd in ⊢ (??%? → ?); #EQ destruct
1863    normalize nodelta @match_reg_elim #INUTILE
1864    [ @mfr_return_eq1 % | @res_preserve_error1 ]
1865  | cases (sigma_pc_opt ? ? ?) normalize nodelta [2: #x] #EQ destruct
1866  ]
1867| whd in match sigma_beval; normalize nodelta cases(sigma_pc_opt ? ? ?)
1868 normalize nodelta [2: #x] #EQ destruct
1869]
1870qed.
1871
1872lemma set_sp_ok :  ∀prog : ertl_program.
1873∀good : (∀fn.good_state_transformation prog fn).
1874∀restr.∀ptr,st.
1875set_sp ? ptr (sigma_state prog good st restr) =
1876sigma_state prog good (set_sp ? ptr st) restr.
1877cases daemon
1878qed.
1879
1880lemma eval_seq_no_pc_no_call_ok :
1881∀prog : ertl_program.
1882let trans_prog ≝ (ertl_to_ertlptr prog) in
1883∀good : (∀fn.good_state_transformation prog fn).
1884∀stack_size. ∀id. ∀fn : (joint_closed_internal_function ??) .∀seq.
1885   preserving1 ?? res_preserve1 ????
1886      (λst.sigma_state prog good st (added_registers … fn (f_regs … (good fn))))
1887      (λst.sigma_state prog good st (added_registers … fn (f_regs … (good fn))))
1888      (eval_seq_no_pc ERTL_semantics
1889             (globals (mk_prog_params ERTL_semantics prog stack_size))
1890             (ev_genv (mk_prog_params ERTL_semantics prog stack_size)) id fn seq)
1891      (eval_seq_no_pc ERTLptr_semantics
1892  (globals (mk_prog_params ERTLptr_semantics trans_prog stack_size))
1893  (ev_genv (mk_prog_params ERTLptr_semantics trans_prog stack_size)) id (translate_internal … fn) (seq_embed … seq)).
1894#prog #good #stack_size #f #fn *
1895whd in match eval_seq_no_pc; normalize nodelta
1896[ #c #st @mfr_return1
1897| #c #st @mfr_return1
1898| #pm #st whd in match pair_reg_move; normalize nodelta
1899  @mfr_bind1
1900  [ 2: change with (ertl_eval_move ??) in ⊢ (???????%%); @ertl_eval_move_ok
1901  | | #regs  @mfr_return_eq1 %
1902  ]
1903| #r #st @mfr_bind1
1904  [2:  @pop_ok |
1905  | * #bv #st whd in match acca_store; normalize nodelta @mfr_bind1
1906    [2: @ps_reg_store_ok |
1907    | #regs  @mfr_return_eq1 %
1908    ]
1909  ]
1910| #r #st @mfr_bind1
1911  [2: whd in match acca_arg_retrieve; normalize nodelta @ps_arg_retrieve_ok |
1912  | #bv @push_ok
1913  ]
1914| #i
1915  change with (member ? ? ? (((prog_var_names (joint_function ERTL)) ℕ prog)) → ?)
1916  #i_spec
1917  change with ((dpl_reg ERTL) → ?)
1918  #dpl
1919  change with ((dph_reg ERTL) → ?)
1920  #dph #st @mfr_bind1
1921  [ @(λst.sigma_state prog good st (added_registers … fn (f_regs … (good fn))))
1922  | whd in match dpl_store; normalize nodelta @mfr_bind1
1923    [2: @opt_safe_elim #bl #EQbl
1924       @opt_safe_elim #bl'
1925       >(find_symbol_transf …
1926          (λvars.transf_fundef … (λfn.(translate_internal … fn))) prog i) in ⊢ (%→?);
1927       >EQbl #EQ destruct whd in match sigma_state; normalize nodelta       
1928       change with (sigma_beval prog (get_sigma_from_good_state … good) (BVptr …))
1929                                               in ⊢ (???????(?????%?)?);
1930       @ps_reg_store_ok |
1931    | #regs  @mfr_return_eq1 %
1932    ]
1933  | #st1 @opt_safe_elim #bl #EQbl @opt_safe_elim #bl'   
1934    >(find_symbol_transf …
1935          (λvars.transf_fundef … (λfn.(translate_internal … fn))) prog i) in ⊢ (%→?);
1936    >EQbl #EQ destruct whd in match dph_store; normalize nodelta @mfr_bind1
1937    [2: whd in match sigma_state; normalize nodelta       
1938       change with (sigma_beval prog (get_sigma_from_good_state … good) (BVptr …))
1939                                               in ⊢ (???????(?????%?)?);
1940      @ps_reg_store_ok |
1941    | #regs  @mfr_return_eq1 %
1942    ]
1943  ]
1944| #op #a #b #arg1 #arg2 #st @mfr_bind1
1945  [2: whd in match acca_arg_retrieve; whd in match sigma_state; normalize nodelta
1946     @ps_arg_retrieve_ok |
1947  | #bv1 @mfr_bind1
1948   [2: whd in match accb_arg_retrieve; whd in match sigma_state; normalize nodelta
1949      @ps_arg_retrieve_ok |
1950   | #bv2 @mfr_bind1
1951     [2: @be_opaccs_ok |
1952     | * #bv3 #bv4 normalize nodelta @mfr_bind1
1953       [ @(λst.sigma_state prog good st (added_registers … fn (f_regs … (good fn))))
1954       | whd in match acca_store; normalize nodelta @mfr_bind1
1955         [2: @ps_reg_store_ok |
1956         | #regs  @mfr_return_eq1 %
1957         ]
1958       | #st1 whd in match accb_store; normalize nodelta @mfr_bind1
1959         [2: whd in match sigma_state; normalize nodelta
1960            @ps_reg_store_ok |
1961         | #regs  @mfr_return_eq1 %
1962         ]         
1963       ]
1964     ]
1965   ]
1966  ] 
1967| #op #r1 #r2 #st @mfr_bind1
1968  [ @(sigma_beval prog (get_sigma_from_good_state … good))
1969  | whd in match acca_retrieve; normalize nodelta @ps_reg_retrieve_ok
1970  | #bv1 @mfr_bind1
1971    [ @(sigma_beval prog (get_sigma_from_good_state … good))
1972    | @be_op1_ok
1973    | #bv2 whd in match acca_store; normalize nodelta @mfr_bind1
1974      [2: whd in match sigma_state; normalize nodelta @ps_reg_store_ok |
1975      | #regs  @mfr_return_eq1 %
1976      ]
1977    ]
1978  ]
1979| #op2 #r1 #r2 #arg #st @mfr_bind1
1980  [2: whd in match acca_arg_retrieve; normalize nodelta @ps_arg_retrieve_ok |
1981  | #bv @mfr_bind1
1982    [2: whd in match snd_arg_retrieve; normalize nodelta @ps_arg_retrieve_ok |
1983    | #bv1 @mfr_bind1
1984      [2: @be_op2_ok |
1985      | * #bv2 #b @mfr_bind1
1986        [ @(λst.sigma_state prog good st (added_registers … fn (f_regs … (good fn))))
1987        | whd in match acca_store; normalize nodelta @mfr_bind1
1988          [2: whd in match sigma_state; normalize nodelta @ps_reg_store_ok |
1989          | #regs  @mfr_return_eq1 %
1990          ]
1991        | #st1 @mfr_return_eq1 %
1992        ]
1993      ]
1994    ]
1995  ]
1996| #st  @mfr_return_eq1 %
1997| #st  @mfr_return_eq1 %
1998| #r1 #dpl #dph #st @mfr_bind1
1999  [2: whd in match dph_arg_retrieve; normalize nodelta @ps_arg_retrieve_ok |
2000  | #bv @mfr_bind1
2001    [2: whd in match dpl_arg_retrieve; normalize nodelta @ps_arg_retrieve_ok |
2002    | #bv1 @mfr_bind1
2003      [ @(λx.x)
2004      | @(pointer_of_address_ok ? ? 〈bv1,bv〉)
2005      | #ptr @mfr_bind1
2006        [2: @opt_to_res_preserve1 @beloadv_ok |
2007        | #bv2 whd in match acca_store; normalize nodelta @mfr_bind1
2008          [2: whd in match sigma_state; normalize nodelta @ps_reg_store_ok |
2009          | #regs  @mfr_return_eq1 %
2010          ]
2011        ] 
2012      ]
2013    ]
2014  ] 
2015| #dpl #dph #r #st @mfr_bind1
2016  [2: whd in match dph_arg_retrieve; normalize nodelta @ps_arg_retrieve_ok |
2017  | #bv @mfr_bind1
2018    [2: whd in match dpl_arg_retrieve; normalize nodelta @ps_arg_retrieve_ok |
2019    | #bv1 @mfr_bind1
2020      [ @(λx.x)
2021      |  @(pointer_of_address_ok ? ? 〈bv1,bv〉)
2022      | #ptr @mfr_bind1
2023        [2: whd in match acca_arg_retrieve; normalize nodelta @ps_arg_retrieve_ok |
2024        | #bv2 @mfr_bind1
2025          [2: @opt_to_res_preserve1 @bestorev_ok |
2026          | #m @mfr_return_eq1 %
2027          ]
2028        ]
2029      ]
2030    ]
2031  ]
2032| #ext #st whd in ⊢ (???????%%); whd in match (stack_sizes ????); cases (stack_size f)
2033  normalize nodelta
2034  [ @res_preserve_error1
2035  | #n cases ext normalize nodelta
2036    [1,2: @mfr_bind1
2037      [1,4: @(λx.x)
2038      |2,5: @sp_ok
2039      |3,6: #ptr @mfr_return_eq1 >set_sp_ok %
2040      ]
2041    | #r whd in match ps_reg_store_status; normalize nodelta @mfr_bind1
2042      [2: whd in match sigma_state; normalize nodelta
2043          change with (sigma_beval ? (get_sigma_from_good_state … good) (BVByte ?))
2044               in ⊢ (???????(??%?)?);
2045          @ps_reg_store_ok
2046      |
2047      | #regs @mfr_return_eq1 %
2048      ]
2049    ]
2050  ]     
2051]
2052qed.
2053
2054
2055xxxxxxxxxxxxxxxxx
2056
2057lemma fetch_statement_commute :
2058∀prog : ertl_program.
2059let trans_prog ≝ (ertl_to_ertlptr prog) in
2060∀sigma : sigma_map trans_prog.
2061∀stack_sizes,id,fn,stmt,pc.
2062fetch_statement ERTL_semantics
2063(globals (mk_prog_params ERTL_semantics prog stack_sizes))
2064(ev_genv (mk_prog_params ERTL_semantics prog stack_sizes))
2065pc = return 〈id,fn,stmt〉 →
2066match stmt with
2067[ sequential seq nxt ⇒
2068    match seq with
2069    [ CALL ids args dest ⇒
2070        match ids with
2071        [ inl i ⇒
2072          fetch_statement ERTLptr_semantics
2073          (globals (mk_prog_params ERTLptr_semantics trans_prog stack_sizes))
2074          (ev_genv (mk_prog_params ERTLptr_semantics trans_prog stack_sizes))
2075          pc =
2076          return 〈id,
2077          translate_internal … fn,
2078          sequential ?? (CALL ERTLptr ? (inl ?? i) args dest) nxt〉
2079        | inr p ⇒ ?(*
2080          ∃reg,lbl.
2081          fetch_statement ERTLptr_semantics
2082          (globals (mk_prog_params ERTLptr_semantics trans_prog stack_sizes))
2083          (ev_genv (mk_prog_params ERTLptr_semantics trans_prog stack_sizes))
2084           pc = return 〈id,translate_internal … fn,sequential ?? (extension_seq ERTLptr ? (LOW_ADDRESS reg lbl)) nxt〉
2085           ∧ ∃ nxt'.
2086           ! pc' ← get_pc_from_label ? ? (ev_genv (mk_prog_params ERTLptr_semantics trans_prog stack_sizes))
2087                 id nxt;
2088           fetch_statement ERTLptr_semantics
2089          (globals (mk_prog_params ERTLptr_semantics trans_prog stack_sizes))
2090          (ev_genv (mk_prog_params ERTLptr_semantics trans_prog stack_sizes))
2091           pc' = return 〈id,translate_internal … fn,sequential ?? (step_seq ERTLptr ? (PUSH … (Reg … reg))) nxt'〉
2092           ∧ ∃ nxt''.
2093           ! pc' ← get_pc_from_label ? ? (ev_genv (mk_prog_params ERTLptr_semantics trans_prog stack_sizes))
2094                 id nxt';
2095           fetch_statement ERTLptr_semantics
2096          (globals (mk_prog_params ERTLptr_semantics trans_prog stack_sizes))
2097          (ev_genv (mk_prog_params ERTLptr_semantics trans_prog stack_sizes))
2098           pc' = return 〈id,translate_internal … fn,sequential ?? (extension_seq ERTLptr ? (HIGH_ADDRESS reg lbl)) nxt''〉
2099           ∧ ∃ nxt'''.
2100           ! pc' ← get_pc_from_label ? ? (ev_genv (mk_prog_params ERTLptr_semantics trans_prog stack_sizes))
2101                 id nxt'';
2102           fetch_statement ERTLptr_semantics
2103          (globals (mk_prog_params ERTLptr_semantics trans_prog stack_sizes))
2104          (ev_genv (mk_prog_params ERTLptr_semantics trans_prog stack_sizes))
2105           pc' = return 〈id,translate_internal … fn,sequential ?? (step_seq ERTLptr ? (PUSH … (Reg … reg))) nxt'''〉
2106           ∧ ∃ nxt''''.
2107           ! pc' ← get_pc_from_label ? ? (ev_genv (mk_prog_params ERTLptr_semantics trans_prog stack_sizes))
2108                 id nxt''';
2109           fetch_statement ERTLptr_semantics
2110          (globals (mk_prog_params ERTLptr_semantics trans_prog stack_sizes))
2111          (ev_genv (mk_prog_params ERTLptr_semantics trans_prog stack_sizes))
2112           pc' = return 〈id,translate_internal … fn,sequential ?? (CALL ERTLptr ? (inr ?? p) args dest) nxt''''〉
2113           ∧ sigma (translate_internal … fn) nxt''' =  return point_of_pc ERTL_semantics pc *)
2114        ]
2115    | COND r lbl ⇒
2116          fetch_statement ERTLptr_semantics
2117          (globals (mk_prog_params ERTLptr_semantics trans_prog stack_sizes))
2118          (ev_genv (mk_prog_params ERTLptr_semantics trans_prog stack_sizes))
2119          pc =
2120          return 〈id,
2121          translate_internal … fn,
2122          sequential ?? (COND ERTLptr ? r lbl) nxt〉
2123    | step_seq s ⇒
2124          fetch_statement ERTLptr_semantics
2125          (globals (mk_prog_params ERTLptr_semantics trans_prog stack_sizes))
2126          (ev_genv (mk_prog_params ERTLptr_semantics trans_prog stack_sizes))
2127          pc =
2128          return 〈id,
2129          translate_internal … fn,
2130          sequential ?? (step_seq ERTLptr … (translate_step_seq ? s)) nxt〉
2131    ]                   
2132| final fin ⇒
2133     fetch_statement ERTLptr_semantics
2134     (globals (mk_prog_params ERTLptr_semantics trans_prog stack_sizes))
2135     (ev_genv (mk_prog_params ERTLptr_semantics trans_prog stack_sizes))
2136     pc = return 〈id,(translate_internal … fn),final … (joint_fin_step_id fin)〉
2137| FCOND abs _ _ _ ⇒ Ⓧabs
2138].
2139cases daemon
2140qed.
2141
2142lemma eval_seq_no_call_ok :
2143 ∀prog.
2144 let trans_prog ≝ ertl_to_ertlptr prog in
2145 ∀sigma : sigma_map trans_prog.∀stack_sizes.
2146 (*? →*)
2147 ∀st,st',f,fn,stmt,nxt.
2148   fetch_statement ERTL_semantics
2149     (prog_var_names (joint_function ERTL_semantics) ℕ prog)
2150    (ev_genv (mk_prog_params ERTL_semantics prog stack_sizes))
2151    (pc … (sigma_state_pc ? sigma st)) =
2152      return 〈f, fn,  sequential … (step_seq ERTL … stmt) nxt〉 →
2153   eval_state ERTL_semantics
2154   (prog_var_names (joint_function ERTL_semantics) ℕ prog)
2155   (ev_genv … (mk_prog_params ERTL_semantics prog stack_sizes))
2156   (sigma_state_pc ? sigma st) =
2157    return st' →
2158 ∃st''. st' = sigma_state_pc ? sigma st'' ∧
2159 ∃taf : trace_any_any_free (ERTLptr_status trans_prog stack_sizes)
2160  st
2161  st''.
2162 bool_to_Prop (taaf_non_empty … taf).
2163#prog #sigma #stack_size #st1 #st2 #f #fn #stmt #nxt #EQf whd in match eval_state;
2164normalize nodelta >EQf >m_return_bind whd in match eval_statement_advance;
2165whd in match eval_statement_no_pc; normalize nodelta
2166 #H @('bind_inversion H) -H #st_no_pc #EQ lapply(err_eq_from_io ????? EQ) -EQ
2167#EQeval whd in ⊢ (??%% → ?); #EQ destruct lapply EQf
2168whd in match sigma_state_pc in ⊢ (% → ?); normalize nodelta @if_elim
2169[ #EQbl
2170| #pc_st1_spec inversion(fetch_internal_function ???) [2: #e #_]
2171]
2172[1,2: whd in match dummy_state_pc; whd in match null_pc;
2173  whd in match fetch_statement; normalize nodelta whd in match fetch_internal_function;
2174  normalize nodelta lapply(fetch_function_no_zero ??????)
2175  [2,9: @( «mk_block Code OZ,refl region Code»)
2176    |1,8: % |3,10: @prog |7,14: #EQ >EQ |*:]  whd in ⊢ (??%% → ?); #EQ destruct]
2177* #f1 #fn1 #EQ lapply(jmeq_to_eq ??? EQ) -EQ #fn1_spec normalize nodelta
2178whd in match fetch_statement; normalize nodelta >fn1_spec
2179>m_return_bind #H @('bind_inversion H) -H #stmt1 #EQ
2180lapply(opt_eq_from_res ???? EQ) -EQ #stmt1_spec whd in ⊢ (??%% → ?); #EQ destruct
2181lapply EQeval -EQeval whd in match sigma_state_pc in ⊢ (% → ?);
2182normalize nodelta @if_elim [#H >H in pc_st1_spec; *] #_ >fn1_spec
2183normalize nodelta #EQeval cases(eval_seq_no_pc_no_call_ok ???????? EQeval)
2184#st_no_pc' * #EQeval' #EQst_no_pc'
2185whd in match set_no_pc; normalize nodelta
2186% [ % [@st_no_pc'|@(succ_pc ERTL_semantics (pc ERTL_semantics (sigma_state_pc prog sigma st1))
2187   nxt)| @(last_pop ? st1)]]
2188% [ whd in match sigma_state_pc; normalize nodelta
2189    @if_elim [#H >H in pc_st1_spec; *] #_ >fn1_spec normalize nodelta
2190    @if_elim [#H >H in pc_st1_spec; *] #_ >fn1_spec normalize nodelta
2191    >EQst_no_pc' %]
2192%{(taaf_step … (taa_base …) …)}
2193[3: //] lapply(fetch_statement_commute ? sigma ????? EQf) normalize nodelta
2194whd in match sigma_state_pc; normalize nodelta
2195@if_elim [1,3:#H >H in pc_st1_spec; *] #_ >fn1_spec normalize nodelta
2196#EQf1
2197[ whd in match as_classifier; normalize nodelta whd in match (as_classify ??);
2198  >EQf1 normalize nodelta %
2199| whd in match (as_execute ???); whd in match eval_state; normalize nodelta
2200  >EQf1 >m_return_bind whd in match eval_statement_no_pc; normalize nodelta
2201  >EQeval' >m_return_bind %
2202]
2203qed.
2204
2205lemma pc_of_label_eq :
2206  ∀p,p'.let pars ≝ make_sem_graph_params p p' in
2207  ∀globals,ge,bl,i_fn,lbl.
2208  fetch_internal_function ? ge bl = return i_fn →
2209  pc_of_label pars globals ge bl lbl =
2210    OK ? (pc_of_point ERTL_semantics bl lbl).
2211#p #p' #globals #ge #bl #i_fn #lbl #EQf
2212whd in match pc_of_label;
2213normalize nodelta >EQf >m_return_bind %
2214qed.
2215
2216lemma eval_goto_ok :
2217 ∀prog : ertl_program.
2218 let trans_prog ≝ ertl_to_ertlptr prog in
2219 ∀stack_sizes.
2220 ∀sigma : sigma_map trans_prog.
2221 ∀st,st',f,fn,nxt.
2222   fetch_statement ERTL_semantics …
2223    (globalenv_noinit ? prog) (pc … (sigma_state_pc ? sigma st)) =
2224      return 〈f, fn,  final … (GOTO ERTL … nxt)〉 →
2225   eval_state ERTL_semantics
2226   (prog_var_names (joint_function ERTL_semantics) ℕ prog)
2227   (ev_genv … (mk_prog_params ERTL_semantics prog stack_sizes))
2228   (sigma_state_pc ? sigma st) =
2229    return st' →
2230    ∃ st''. st' = sigma_state_pc ? sigma st'' ∧
2231 ∃taf : trace_any_any_free (ERTLptr_status trans_prog stack_sizes)
2232  st
2233  st''.
2234 bool_to_Prop (taaf_non_empty … taf).
2235#prog #stack_sizes #sigma #st #st' #f #fn #nxt
2236whd in match sigma_state_pc in ⊢ (% → ?); normalize nodelta
2237@if_elim
2238[ #EQbl whd in match dummy_state_pc; whd in match null_pc;
2239  whd in match fetch_statement; whd in match fetch_internal_function;
2240  normalize nodelta lapply(fetch_function_no_zero ??????)
2241  [2: @( «mk_block Code OZ,refl region Code»)
2242    | % | @prog |7: #EQ >EQ |*:]  whd in ⊢ (??%% → ?); #EQ destruct]
2243#Hbl inversion(fetch_internal_function ???)
2244[2: #e #_ normalize nodelta whd in match dummy_state_pc; whd in match null_pc;
2245   whd in match fetch_statement; whd in match fetch_internal_function;
2246  normalize nodelta lapply(fetch_function_no_zero ??????)
2247  [2: @( «mk_block Code OZ,refl region Code»)
2248    | % | @prog |7: #EQ >EQ |*:]  whd in ⊢ (??%% → ?); #EQ destruct]
2249* #f1 #fn1 #EQ lapply(jmeq_to_eq ??? EQ) -EQ #fn1_spec normalize nodelta
2250#EQf lapply EQf whd in match fetch_statement; normalize nodelta >fn1_spec
2251>m_return_bind #H @('bind_inversion H) -H #stmt' #_ whd in ⊢ (??%% → ?);
2252#EQ destruct whd in match sigma_state_pc in ⊢ (% → ?); normalize nodelta
2253@if_elim [#H >H in Hbl; *] #_ >fn1_spec normalize nodelta whd in match eval_state;
2254normalize nodelta >EQf >m_return_bind whd in match eval_statement_advance;
2255whd in match eval_statement_no_pc; normalize nodelta >m_return_bind
2256whd in match goto; normalize nodelta #H lapply (err_eq_from_io ????? H) -H
2257#H @('bind_inversion H) -H #pc' whd in match set_no_pc; normalize nodelta
2258>(pc_of_label_eq … fn1_spec) whd in ⊢ (???% → ?); #EQ whd in ⊢ (??%% → ?); #EQ1
2259destruct lapply (fetch_statement_commute … sigma … stack_sizes … EQf)
2260normalize nodelta #EQf' %
2261[ % [ @st
2262    | @(mk_program_counter
2263         (pc_block (pc ERTLptr_semantics st))
2264         (offset_of_point ERTL_semantics nxt))
2265    | @(last_pop … st)
2266    ]
2267] %
2268[ whd in match sigma_state_pc; normalize nodelta @if_elim [#H >H in Hbl; *]
2269  >fn1_spec normalize nodelta #_ % ]
2270%{(taaf_step … (taa_base …) …)}
2271[ whd in match as_classifier; normalize nodelta whd in match (as_classify ??);
2272  >EQf' normalize nodelta %
2273| whd in match (as_execute ???); whd in match eval_state; normalize nodelta
2274  >EQf' >m_return_bind whd in match eval_statement_no_pc;
2275  whd in match eval_statement_advance; normalize nodelta >m_return_bind
2276  whd in match goto; normalize nodelta whd in match pc_of_label; normalize nodelta
2277  lapply(fetch_internal_function_transf ??????? fn1_spec)
2278  [ #vars @translate_internal |] #EQ >EQ >m_return_bind %
2279| %
2280]
2281qed.
2282
2283axiom partial_inj_sigma : ∀ prog : ertlptr_program.
2284∀sigma :sigma_map prog.
2285∀fn,lbl1,lbl2. sigma fn lbl1 ≠ None ? → sigma fn lbl1 = sigma fn lbl2 → lbl1 = lbl2.
2286
2287lemma pop_ra_ok :
2288∀prog : ertl_program.
2289let trans_prog ≝ ertl_to_ertlptr prog in
2290∀sigma : sigma_map trans_prog.
2291∀stack_size.
2292∀fn : (joint_closed_internal_function ? (globals (mk_prog_params ERTL_semantics prog stack_size))).
2293preserving1 … res_preserve1 …
2294     (λst.sigma_state trans_prog sigma st (joint_if_locals ERTL ? fn))
2295     (λx.let 〈st,pc〉 ≝ x in
2296       〈sigma_state trans_prog sigma st (joint_if_locals ERTL ? fn),
2297        sigma_stored_pc ? sigma pc〉)
2298     (pop_ra ERTL_semantics)
2299     (pop_ra ERTLptr_semantics).
2300#prog #sigma #stack_size #fn #st whd in match pop_ra; normalize nodelta @mfr_bind1
2301[ | @pop_ok ] * #bv #st1 @mfr_bind1 [ | @pop_ok] * #bv1 #st2 @mfr_bind1
2302[ @(sigma_stored_pc ? sigma) | whd in match pc_of_bevals; normalize nodelta
2303  cases bv [ | | #ptr1 #ptr2 #p | #by | #p | #ptr #p | #pc #p]
2304  whd in match sigma_beval; normalize nodelta try @res_preserve_error1
2305  inversion(sigma_pc_opt ? ? ?) normalize nodelta [ #_ @res_preserve_error1]
2306  #sigma_pc #sigma_pc_spec normalize nodelta cases bv1
2307  [ | | #ptr1 #ptr2 #p | #by | #p | #ptr #p | #pc1 #p1]
2308  normalize nodelta try @res_preserve_error1
2309  inversion(sigma_pc_opt ? ? ?) normalize nodelta [#_ @res_preserve_error1]
2310  #sigma_pc1 #sigma_pc1_spec @if_elim [2: #_ @res_preserve_error1]
2311  @andb_elim @if_elim [2: #_ *] @andb_elim @if_elim [2: #_ *]
2312  #_ #H >H @eq_program_counter_elim [2: #_ *]
2313  #EQspc * @eq_program_counter_elim
2314  [#_ normalize nodelta @mfr_return_eq1 whd in match sigma_stored_pc; normalize nodelta
2315   >sigma_pc1_spec %] * #H1 @⊥ @H1 >EQspc in sigma_pc_spec; <sigma_pc1_spec
2316   whd in match sigma_pc_opt; normalize nodelta @if_elim
2317  [ #H2 #EQ lapply(sym_eq ??? EQ) -EQ @if_elim [#_  whd in ⊢ (??%% → ?); #EQ destruct %]
2318    #H3 #H @('bind_inversion H) -H #x #_ #H @('bind_inversion H) -H #y #_
2319    cases sigma_pc1 in H2; #bl_pc1 #z #H2 whd in ⊢ (??%? → ?); #EQ destruct >H2 in H3; *
2320  | #H2 @if_elim
2321    [ #H3 #H @('bind_inversion H) -H #x1 #_ #H @('bind_inversion H) -H #lbl1 #_
2322      cases pc in H2; #bl #z #H2 whd in match pc_of_point; normalize nodelta whd in ⊢ (??%? → ?);
2323      #EQ destruct >H3 in H2; *
2324    | #H3 lapply sigma_pc1_spec; whd in match sigma_pc_opt; normalize nodelta @if_elim
2325     [#H >H in H3; *] #_ #EQ >EQ @('bind_inversion EQ) -EQ #x #x_spec
2326     lapply(res_eq_from_opt ??? x_spec) -x_spec #x_spec #H @('bind_inversion H) * #lbl
2327     #lbl_spec whd in match pc_of_point; normalize nodelta cases sigma_pc1 #bl1 #lbl1
2328     whd in match (offset_of_point ??); whd in ⊢ (??%? → ?); #EQ destruct cases pc #bl2 #p2
2329     #H @('bind_inversion H) -H #x1 #x1_spec lapply(res_eq_from_opt ??? x1_spec) -x1_spec #x1_spec
2330     #H @('bind_inversion H) -H * #lbl2 #lbl2_spec
2331     whd in match (offset_of_point ??); whd in ⊢ (??%? → ?); #EQ destruct
2332     <lbl_spec in lbl2_spec; #EQsig >x_spec in x1_spec; whd in ⊢ (??%% → ?); #EQ destruct
2333     lapply(partial_inj_sigma (ertl_to_ertlptr prog) sigma ???? EQsig)
2334     [>EQsig >lbl_spec % #ABS destruct] whd in match point_of_pc; normalize nodelta
2335     whd in match (point_of_offset ??); whd in match (point_of_offset ??);
2336     #EQ destruct cases pc1 #bl #p %
2337    ]
2338  ]
2339| #pc @mfr_return_eq1 %
2340]
2341qed.
2342
2343lemma pc_block_eq : ∀prog : ertl_program.
2344let trans_prog ≝ ertl_to_ertlptr prog in
2345∀sigma : sigma_map trans_prog.
2346∀pc,id,fn.
2347fetch_internal_function (joint_closed_internal_function ERTLptr
2348  (prog_var_names (joint_function ERTLptr) ℕ trans_prog))
2349  (globalenv_noinit (joint_function ERTLptr) trans_prog) (pc_block … pc) = return 〈id,fn〉→
2350sigma fn (point_of_pc ERTL_semantics pc) ≠ None ? →
2351 pc_block … pc = pc_block … (sigma_stored_pc trans_prog sigma pc).
2352#prog #sigma * #bl #pos #id #fn #EQfn #EQlbl whd in match sigma_stored_pc;
2353normalize nodelta whd in match sigma_pc_opt; normalize nodelta @if_elim [ #_ %]
2354#_ >EQfn >m_return_bind >(opt_to_opt_safe … EQlbl) >m_return_bind %
2355qed.
2356                       
2357
2358 
2359lemma eval_return_ok :
2360∀prog : ertl_program.
2361let trans_prog ≝ ertl_to_ertlptr prog in
2362∀stack_sizes.
2363∀sigma : sigma_map trans_prog.
2364∀st,st',f,fn.
2365 fetch_statement ERTL_semantics …
2366  (globalenv_noinit ? prog) (pc … (sigma_state_pc ? sigma st)) =
2367    return 〈f, fn,  final … (RETURN ERTL … )〉 →
2368 eval_state ERTL_semantics
2369   (prog_var_names (joint_function ERTL_semantics) ℕ prog)
2370   (ev_genv … (mk_prog_params ERTL_semantics prog stack_sizes))
2371   (sigma_state_pc ? sigma st) =
2372  return st' →
2373joint_classify (mk_prog_params ERTLptr_semantics trans_prog stack_sizes)
2374  st = Some ? cl_return ∧
2375∃ st''. st' = sigma_state_pc ? sigma st'' ∧
2376∃st2_after_ret.
2377∃taf : trace_any_any_free (ERTLptr_status trans_prog stack_sizes)
2378st2_after_ret
2379st''.
2380(if taaf_non_empty … taf then
2381  ¬as_costed (ERTLptr_status trans_prog stack_sizes)
2382    st2_after_ret
2383 else True) ∧
2384eval_state … (ev_genv …  (mk_prog_params ERTLptr_semantics trans_prog stack_sizes)) st =
2385return st2_after_ret ∧
2386ret_rel ?? (ERTLptrStatusSimulation prog stack_sizes sigma) st' st2_after_ret.
2387#prog #stack_size #sigma #st #st' #f #fn
2388whd in match sigma_state_pc in ⊢ (% → ?); normalize nodelta
2389@if_elim
2390[ #EQbl whd in match dummy_state_pc; whd in match null_pc;
2391  whd in match fetch_statement; whd in match fetch_internal_function;
2392  normalize nodelta >(fetch_function_no_zero ??????) [2: %]
2393  whd in ⊢ (??%% → ?); #EQ destruct ]
2394#Hbl inversion(fetch_internal_function ???)
2395[2: #e #_ normalize nodelta whd in match dummy_state_pc; whd in match null_pc;
2396   whd in match fetch_statement; whd in match fetch_internal_function;
2397  normalize nodelta lapply(fetch_function_no_zero ??????)
2398  [2: @( «mk_block Code OZ,refl region Code»)
2399    | % | @prog |7: #EQ >EQ |*:]  whd in ⊢ (??%% → ?); #EQ destruct]
2400* #f1 #fn1 #EQ lapply(jmeq_to_eq ??? EQ) -EQ #fn1_spec normalize nodelta
2401#EQf lapply EQf whd in match fetch_statement; normalize nodelta >fn1_spec
2402>m_return_bind #H @('bind_inversion H) -H #stmt' #_ whd in ⊢ (??%% → ?);
2403#EQ destruct whd in match sigma_state_pc in ⊢ (% → ?); normalize nodelta
2404@if_elim [#H >H in Hbl; *] #_ >fn1_spec normalize nodelta
2405whd in match eval_state; normalize nodelta >EQf >m_return_bind
2406whd in match eval_statement_no_pc; whd in match eval_statement_advance;
2407normalize nodelta >m_return_bind
2408#H lapply (err_eq_from_io ????? H) -H #H @('bind_inversion H) -H
2409* #st1 #pc1 #EQpop whd in match next_of_call_pc; normalize nodelta
2410>m_bind_bind #H @('bind_inversion H) -H ** #f1 #fn1 * normalize nodelta
2411[ * [ #c_id #args #dest | #r #lbl | #seq ] #nxt | #fin | * ]
2412#EQf1 normalize nodelta [2,3,4: whd in ⊢ (??%% → ?); #EQ destruct]
2413>m_return_bind whd in ⊢ (??%% → ?); #EQ destruct
2414lapply (fetch_statement_commute prog sigma stack_size … EQf)
2415normalize nodelta #EQf'
2416% [ whd in match joint_classify; normalize nodelta >EQf' >m_return_bind %]
2417change with (pop_ra ?? = ?) in EQpop; whd in match set_no_pc in EQpop;
2418normalize nodelta in EQpop;
2419cases(pop_ra_ok ? sigma  stack_size fn ?? EQpop) * #st3 #pc3 * #st3_spec
2420normalize nodelta #EQ destruct whd in match set_last_pop; whd in match succ_pc;
2421normalize nodelta whd in match (point_of_succ ???);
2422 % [ % [ @st3 | @(pc_of_point ERTL_semantics (pc_block … pc3) nxt) | @pc3] ]
2423 % [  @('bind_inversion EQf1) * #f3 #fn3 whd in match sigma_stored_pc;
2424      normalize nodelta inversion(sigma_pc_opt ???) normalize nodelta
2425      [ #_ #H @('bind_inversion H) -H #x whd in match null_pc; normalize nodelta
2426        >fetch_function_no_zero [2: %] whd in ⊢ (???% → ?); #EQ destruct
2427      | #pc4 whd in match sigma_pc_opt; normalize nodelta @if_elim
2428        [ #bl3_spec @('bind_inversion EQf1) #x #H @('bind_inversion H) -H
2429          #x1 >fetch_function_no_minus_one [ whd in ⊢ (???% → ?); #EQ destruct]
2430          lapply bl3_spec @eqZb_elim #EQ * whd in match sigma_stored_pc;
2431          normalize nodelta whd in match sigma_pc_opt; normalize nodelta
2432           >bl3_spec normalize nodelta assumption
2433        | #bl3_spec #H @('bind_inversion H) -H * #id4 #fn4
2434          #H lapply(res_eq_from_opt ??? H) -H #fn4_spec
2435          #H @('bind_inversion H) -H #lbl4 #lbl4_spec whd in ⊢ (??%? → ?); #EQ
2436          destruct #fn3_spec #H @('bind_inversion H) -H #stmt1 #_
2437          whd in ⊢ (??%% → ?); #EQ destruct
2438          >(fetch_internal_function_transf … fn3_spec) in fn4_spec;
2439          whd in ⊢ (??%% → ?); #EQ destruct
2440        ]
2441      ]
2442      whd in match sigma_state_pc; normalize nodelta @if_elim
2443      [ >(pc_block_eq prog sigma ????) in bl3_spec;
2444       [2: >lbl4_spec % #ABS destruct
2445       |3: >(fetch_internal_function_transf … fn3_spec) % |*:]
2446       #bl3_spec whd in match pc_of_point; normalize nodelta #EQ >EQ in bl3_spec; *
2447      | #_ cases daemon
2448      ]
2449  ] cases daemon
2450qed.
2451
2452(*
2453lemma ertl_allocate_local_ok : ∀ prog : ertl_program.
2454let trans_prog ≝ ertl_to_ertlptr prog in
2455∀sigma : sigma_map.
2456∀stack_size.
2457∀id,regs.
2458ertl_allocate_local id (sigma_regs ? sigma getLocalsFromId(
2459*)
2460
2461lemma eval_tailcall_ok :
2462∀prog.
2463let trans_prog ≝ ertl_to_ertlptr prog in
2464∀stack_sizes.
2465∀sigma : sigma_map trans_prog.
2466∀st,st',f,fn,fl,called,args.
2467 fetch_statement ERTL_semantics …
2468  (globalenv_noinit ? prog) (pc … (sigma_state_pc ? sigma st)) =
2469    return 〈f, fn,  final … (TAILCALL ERTL … fl called args)〉 →
2470 eval_state ERTL_semantics
2471   (prog_var_names (joint_function ERTL_semantics) ℕ prog)
2472   (ev_genv … (mk_prog_params ERTL_semantics prog stack_sizes))
2473   (sigma_state_pc ? sigma st) =
2474  return st' →
2475  ∃ st''. st' = sigma_state_pc ? sigma st'' ∧
2476  ∃is_tailcall, is_tailcall'.
2477  joint_tailcall_ident (mk_prog_params ERTLptr_semantics trans_prog stack_sizes) «st, is_tailcall'» =
2478  joint_tailcall_ident (mk_prog_params ERTL_semantics prog stack_sizes) «(sigma_state_pc ? sigma st), is_tailcall» ∧
2479  eval_state … (ev_genv … (mk_prog_params ERTLptr_semantics trans_prog stack_sizes))
2480    st = return st''.
2481#prog #stack_size #sigma #st #st' #f #fn #fl #called #args
2482whd in match sigma_state_pc in ⊢ (% → ?); normalize nodelta
2483@if_elim
2484[ #EQbl whd in match dummy_state_pc; whd in match null_pc;
2485  whd in match fetch_statement; whd in match fetch_internal_function;
2486  normalize nodelta >(fetch_function_no_zero ??????) [2: %]
2487  whd in ⊢ (??%% → ?); #EQ destruct ]
2488#Hbl inversion(fetch_internal_function ???)
2489[2: #e #_ normalize nodelta whd in match dummy_state_pc; whd in match null_pc;
2490   whd in match fetch_statement; whd in match fetch_internal_function;
2491  normalize nodelta lapply(fetch_function_no_zero ??????)
2492  [2: @( «mk_block Code OZ,refl region Code»)
2493    | % | @prog |7: #EQ >EQ |*:]  whd in ⊢ (??%% → ?); #EQ destruct]
2494* #f1 #fn1 #EQ lapply(jmeq_to_eq ??? EQ) -EQ #fn1_spec normalize nodelta
2495#EQf lapply EQf whd in match fetch_statement; normalize nodelta >fn1_spec
2496>m_return_bind #H @('bind_inversion H) -H #stmt' #_ whd in ⊢ (??%% → ?);
2497#EQ destruct  whd in match sigma_state_pc in ⊢ (% → ?); normalize nodelta
2498@if_elim [#H >H in Hbl; *] #_ >fn1_spec normalize nodelta
2499whd in match eval_state; normalize nodelta >EQf >m_return_bind
2500whd in match eval_statement_no_pc; whd in match eval_statement_advance;
2501normalize nodelta >m_return_bind whd in match eval_tailcall;
2502normalize nodelta #H @('bind_inversion H) -H #bl whd in match set_no_pc;
2503normalize nodelta #bl_spec #H @('bind_inversion H) -H * #id1 * [#int_f | #ext_f] 
2504#H lapply(err_eq_from_io ????? H) -H #id1_spec normalize nodelta
2505[2: #H @('bind_inversion H) -H #st1 whd in match eval_external_call; normalize nodelta
2506    #H @('bind_inversion H) -H #l_val #_ #H @('bind_inversion H) -H #le #_
2507    #H @('bind_inversion H) -H #x whd in match do_io; normalize nodelta
2508    whd in ⊢ (???% → ?); #EQ destruct ]
2509#H lapply(err_eq_from_io ????? H) -H  #H @('bind_inversion H) -H #st1
2510whd in match eval_internal_call; normalize nodelta whd in match (stack_sizes ????);
2511#H @('bind_inversion H) -H #n #H lapply(opt_eq_from_res ???? H) -H #n_spec
2512whd in match(setup_call ???????); >m_return_bind
2513whd in ⊢ (??%% → ?); #EQ destruct whd in match sigma_state in ⊢ (% → ?);
2514normalize  nodelta whd in ⊢ (??%% → ?); #EQ destruct
2515% [ %
2516    [ %
2517      [ @(st_frms ERTLptr_semantics st)
2518      | @(istack ERTLptr_semantics st)
2519      | @(carry ERTLptr_semantics st)
2520      | cases daemon
2521      | @(m ERTLptr_semantics st)
2522      ]
2523    | @(mk_program_counter bl
2524            (offset_of_point ERTL_semantics
2525              (joint_if_entry ERTL_semantics
2526                  (prog_var_names (joint_function ERTL_semantics) ℕ prog) int_f)))
2527    | @(last_pop ERTLptr_semantics st)
2528    ]
2529  ]
2530% [ whd in match sigma_state_pc; normalize nodelta @if_elim whd in match pc_of_point;
2531    normalize nodelta
2532    [ #Hbl >fetch_function_no_minus_one in id1_spec;
2533       [2: lapply Hbl @eqZb_elim -Hbl #Hbl * @Hbl] whd in ⊢ (???% → ?);
2534       #EQ destruct(EQ)
2535    ] #_ whd in match fetch_internal_function; normalize nodelta >id1_spec
2536      >m_return_bind normalize nodelta cases daemon (*TO BE COmpleted *)
2537  ] cases daemon (*TO BE COMPLETED*)
2538qed.
2539   
2540   
2541   
2542   
2543lemma as_label_ok : ∀ prog : ertl_program.
2544let trans_prog ≝ ertl_to_ertlptr prog in
2545∀ sigma : sigma_map trans_prog.
2546∀stack_sizes.
2547∀ st.
2548as_label (ERTLptr_status trans_prog stack_sizes) st = as_label
2549(ERTL_status prog stack_sizes) (sigma_state_pc prog sigma st).
2550#prog #sigma #stack_size * #st #pc #lp
2551whd in match as_label; normalize nodelta whd in match (as_pc_of ??) in ⊢ (??%%);
2552whd in match (as_label_of_pc ??) in ⊢ (??%%);
2553
2554
2555(*
2556
2557whd in match fetch_statement; normalize nodelta
2558whd in match sigma_state_pc; normalize nodelta @if_elim
2559[ #EQbl whd in match fetch_internal_function; normalize nodelta >m_bind_bind
2560 lapply(fetch_function_no_minus_one ??????) [2: @(pc_block pc) | lapply EQbl
2561 @eqZb_elim #H * @H| @(ertl_to_ertlptr prog) |7: #EQ >EQ |*:] normalize nodelta
2562 whd in match dummy_state_pc; whd in match (as_label_of_pc ??); whd in match null_pc;
2563 whd in match fetch_statement; normalize nodelta whd in match fetch_internal_function;
2564 normalize nodelta >m_bind_bind
2565 lapply(fetch_function_no_zero ??????) [2: @( «mk_block Code OZ,refl region Code»)
2566 | % | @prog |7: #EQ >EQ |*:] %
2567| inversion ( fetch_internal_function
2568     (joint_closed_internal_function ERTL
2569      (prog_var_names (joint_function ERTL) ℕ prog))
2570     (globalenv_noinit (joint_function ERTL) prog) (pc_block pc))
2571 [ * #id #fn #fn_spec #_ lapply(fetch_internal_function_transf ??????? fn_spec)
2572   [ @(λvars,fn.translate_internal … fn) |] #EQ >EQ >m_return_bind normalize nodelta
2573     whd in match (as_label_of_pc ??);
2574     whd in match fetch_statement; normalize nodelta >fn_spec >m_return_bind
2575     cases daemon (*serve specifica su sigma TODO*)
2576   | #err #EQ lapply(jmeq_to_eq ??? EQ) -EQ #fetch_err #_ normalize nodelta
2577     whd in match dummy_state_pc;
2578     whd in match (as_label_of_pc ??); whd in match null_pc;
2579     whd in match fetch_statement; normalize nodelta
2580     whd in match fetch_internal_function in ⊢ (???%);
2581     normalize nodelta
2582     lapply(fetch_function_no_zero ??????) [2: @( «mk_block Code OZ,refl region Code»)
2583     | % | @prog |7: #EQ >EQ in ⊢ (???%); |*:] normalize nodelta -EQ
2584     lapply fetch_err -fetch_err whd in match fetch_internal_function; normalize nodelta
2585     inversion(fetch_function ???)
2586     [* #id * #fn #fn_spec >m_return_bind normalize nodelta [whd in ⊢ (??%? → ?); #EQ destruct]
2587     #EQ destruct  lapply(jmeq_to_eq ??? fn_spec) -fn_spec #fn_spec
2588     lapply(fetch_function_transf ????????? fn_spec) [ #v  @transf_fundef [2:@translate_internal |]|]
2589     #EQ >EQ >m_return_bind %
2590   | #err1 #EQ lapply(jmeq_to_eq ??? EQ) -EQ #EQfetch whd in ⊢ (??%? → ?); #EQ destruct
2591     normalize nodelta lapply EQfetch -EQfetch whd in match fetch_function;
2592     normalize nodelta check joint_function
2593      lapply(symbol_for_block_transf  ? ? ? ? prog (λvars.?)  (pc_block pc))
2594      [@transf_fundef [2: @translate_internal|] |4: #EQ >EQ in ⊢ (? → %); |*:] 
2595     cases(symbol_for_block ???) [ whd in ⊢ (??%% → ?); #EQ destruct %]
2596     #id >m_return_bind inversion(find_funct_ptr ???)
2597     [2: #fn1 #_ >m_return_bind whd in ⊢ (??%? → ?); #EQ destruct]
2598     #EQf whd in ⊢ (??%? → ?); #EQ destruct
2599     lapply(find_funct_ptr_none ??????? EQf) (*forse e' falso*)
2600     [#vars @transf_fundef [2: @translate_internal|]|]
2601     #EQ >EQ %
2602     ]
2603  ]
2604]*)
2605cases daemon
2606qed.
2607
2608lemma bool_of_beval_ok : ∀prog : ertlptr_program.
2609∀sigma : sigma_map prog.
2610preserving1 … res_preserve1 …
2611    (sigma_beval prog sigma)
2612    (λx.x)
2613    (bool_of_beval)
2614    (bool_of_beval).
2615#prog #sigma whd in match bool_of_beval; normalize nodelta
2616* normalize nodelta
2617 [ | | #ptr1 #ptr2 #p | #by | #p | #ptr #p | #pc #p]
2618try @res_preserve_error1 #x
2619[1,2,3,4: whd in ⊢ (???% → ?); #EQ destruct
2620          [1,4: %{true} % //
2621          |3: %{false} % //
2622          | %{(eq_bv 8 (zero 8) by)} % //
2623          ]
2624| whd in match sigma_beval; normalize nodelta cases(sigma_pc_opt ? ? ?)
2625  normalize nodelta [2: #pc1] whd in ⊢ (???% → ?); #EQ destruct
2626]
2627qed.
2628
2629lemma eval_cond_ok :
2630∀prog.
2631let trans_prog ≝ ertl_to_ertlptr prog in
2632∀stack_sizes.
2633∀sigma : sigma_map trans_prog.
2634∀st,st',f,fn,a,ltrue,lfalse.
2635 fetch_statement ERTL_semantics …
2636  (globalenv_noinit ? prog) (pc … (sigma_state_pc ? sigma st)) =
2637    return 〈f, fn,  sequential … (COND ERTL … a ltrue) lfalse〉 →
2638 eval_state ERTL_semantics
2639   (prog_var_names (joint_function ERTL_semantics) ℕ prog)
2640   (ev_genv … (mk_prog_params ERTL_semantics prog stack_sizes))
2641   (sigma_state_pc ? sigma st) =
2642  return st' →
2643as_costed (ERTL_status prog stack_sizes)
2644  st' →
2645∃ st''. st' = sigma_state_pc ? sigma st'' ∧
2646∃taf : trace_any_any_free (ERTLptr_status trans_prog stack_sizes)
2647st st''.
2648bool_to_Prop (taaf_non_empty … taf).
2649#prog #stack_size #sigma #st #st' #f #fn #a #lb_t #lb_f
2650whd in match sigma_state_pc in ⊢ (% → ?); normalize nodelta
2651@if_elim
2652[ #EQbl whd in match dummy_state_pc; whd in match null_pc;
2653  whd in match fetch_statement; whd in match fetch_internal_function;
2654  normalize nodelta >(fetch_function_no_zero ??????) [2: %]
2655  whd in ⊢ (??%% → ?); #EQ destruct ]
2656#Hbl inversion(fetch_internal_function ???)
2657[2: #e #_ normalize nodelta whd in match dummy_state_pc; whd in match null_pc;
2658   whd in match fetch_statement; whd in match fetch_internal_function;
2659  normalize nodelta >(fetch_function_no_zero ??????) [2: %]
2660 whd in ⊢ (??%% → ?); #EQ destruct]
2661* #f1 #fn1 #EQ lapply(jmeq_to_eq ??? EQ) -EQ #fn1_spec normalize nodelta
2662#EQf lapply EQf whd in match fetch_statement; normalize nodelta >fn1_spec
2663>m_return_bind #H @('bind_inversion H) -H #stmt' #_ whd in ⊢ (??%% → ?);
2664#EQ destruct whd in match eval_state; whd in match eval_statement_no_pc;
2665whd in match eval_statement_advance; whd in match sigma_state_pc in ⊢ (% → ?);
2666normalize nodelta @if_elim [#H >H in Hbl; *] #_ >fn1_spec normalize nodelta
2667>EQf >m_return_bind normalize nodelta >m_return_bind
2668#H lapply(err_eq_from_io ????? H) -H #H @('bind_inversion H) -H #bv
2669change with (ps_reg_retrieve ?? = ? → ?) whd in match set_no_pc;
2670whd in match sigma_state in ⊢ (??(?%?)? → ?); normalize nodelta #bv_spec
2671#H @('bind_inversion H) -H * #EQbv normalize nodelta
2672[ whd in match goto; normalize nodelta >pc_of_label_eq [2: assumption |3:]
2673  >m_return_bind whd in match pc_of_point; normalize nodelta whd in ⊢ (??%% → ?);
2674  whd in match set_pc; normalize nodelta #EQ destruct
2675| whd in match next; whd in match set_pc; normalize nodelta whd in match (succ_pc ???);
2676  whd in match (point_of_succ ???); whd in ⊢ (??%% → ?); #EQ destruct
2677]
2678whd in match as_costed; normalize nodelta * #n_cost %
2679[1,3: % [1,4: @st
2680        |2,5: @(mk_program_counter
2681                  (pc_block (pc ERTLptr_semantics st))
2682                  (offset_of_point ERTL_semantics ?)) [ @lb_t | @lb_f]
2683        |3,6: @(last_pop ? st)
2684        ]
2685]
2686% [1,3: whd in match sigma_state_pc; normalize nodelta @if_elim
2687       [1,3: #EQ >EQ in Hbl; *] #_ >fn1_spec %]
2688%{(taaf_step_jump … (taa_base …) …) I}
2689lapply (fetch_statement_commute prog sigma … stack_size … EQf)
2690normalize nodelta #EQf'
2691[1,4: whd in match as_costed; normalize nodelta >as_label_ok [2,4: @sigma]
2692      % #H @n_cost <H whd in match sigma_state_pc; normalize nodelta
2693      @if_elim [1,3: #EQ >EQ in Hbl; *] #_ >fn1_spec %
2694|2,5: whd in match as_classifier; normalize nodelta  whd in match (as_classify ??);
2695      normalize nodelta >EQf' %
2696|*:  whd in match (as_execute ???); whd in match eval_state; normalize nodelta
2697     >EQf' >m_return_bind whd in match eval_statement_no_pc; normalize nodelta
2698     >m_return_bind whd in match eval_statement_advance; normalize nodelta 
2699     change with (ps_reg_retrieve ??) in ⊢ (??(????(????%?))?);
2700     cases(ps_reg_retrieve_ok ????? ? bv_spec) #bv' * #bv_spec' #bv_bv'
2701     >bv_spec' >m_return_bind >bv_bv' in EQbv; #EQbv
2702     cases(bool_of_beval_ok ? sigma ? ? EQbv) #b1 * #b1_spec #EQ destruct
2703     >b1_spec >m_return_bind normalize nodelta [2: %] whd in match goto;
2704     normalize nodelta whd in match set_no_pc; normalize nodelta
2705     >pc_of_label_eq
2706     [ %
2707     | lapply(fetch_internal_function_transf ????????)
2708       [3: @f |2: @fn | whd in ⊢ (???%); <fn1_spec in ⊢ (???%); %
2709       | | #vars @translate_internal |9: #EQ >EQ in ⊢ (??%?); % |*:]
2710       |
2711     ]
2712]
2713qed.
2714       
2715inductive ex_Type1 (A:Type[1]) (P:A → Prop) : Prop ≝
2716    ex1_intro: ∀ x:A. P x →  ex_Type1 A P.
2717(*interpretation "exists in Type[1]" 'exists x = (ex_Type1 ? x).*)
2718
2719lemma
2720  find_funct_ptr_none:
2721    ∀A,B,V,iV. ∀p: program A V. ∀transf: (∀vs. A vs → B vs).
2722    ∀b: block.
2723    find_funct_ptr ? (globalenv … iV p) b = None ? →
2724    find_funct_ptr ? (globalenv … iV (transform_program … p transf)) b = None ?.
2725#A #B #V #i #p #transf #b
2726whd in match find_funct_ptr; normalize nodelta
2727cases b -b * normalize nodelta [#x #_ %] * normalize nodelta
2728[1,2: [2: #x] #_ %] #x whd in match globalenv; normalize nodelta
2729whd in match globalenv_allocmem; normalize nodelta
2730cases daemon (*forse e' falso *)
2731qed.
2732
2733
2734
2735lemma ertl_to_ertlptr_ok:
2736 ∀prog.
2737  let trans_prog ≝ ertl_to_ertlptr prog in
2738 ∀stack_sizes. sigma_map trans_prog →
2739   ex_Type1 … (λR.
2740   status_simulation
2741    (ERTL_status prog stack_sizes) (ERTLptr_status trans_prog stack_sizes) R).
2742#prog #stack_size #sigma % [@ERTLptrStatusSimulation assumption]
2743whd in match status_simulation; normalize nodelta
2744whd in match ERTL_status; whd in match ERTLptr_status; normalize nodelta
2745whd in ⊢ (% → % → % → % → ?); #st1 #st1' #st2
2746change with
2747  (eval_state ERTL_semantics (prog_var_names ???) ?? = ? → ?)
2748#EQeval @('bind_inversion EQeval)
2749** #id #fn #stmt #H lapply (err_eq_from_io ????? H) -H #EQfetch
2750#_  whd in match ERTLptrStatusSimulation; normalize nodelta #EQst2 destruct
2751cases stmt in EQfetch; -stmt
2752[ * [#called #c_arg #c_dest | #reg #lbl | #seq ] #succ_pc | #fin_step | *]
2753normalize nodelta #EQfetch
2754change with (joint_classify ??) in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ? ]);
2755[ (*CALL*)
2756  cases daemon (*TODO*)
2757| whd in match joint_classify; normalize nodelta
2758 >EQfetch in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ? ]);
2759  normalize nodelta
2760 #n_cost
2761 cases (eval_cond_ok … EQfetch EQeval n_cost)
2762 #st3 * #EQ destruct * #taf #tafne %{st3} %{taf}
2763 % [ % [2: %] >tafne normalize nodelta @I] whd >as_label_ok %
2764| whd in match joint_classify; normalize nodelta
2765 >EQfetch in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ? ]);
2766  normalize nodelta
2767  cases (eval_seq_no_call_ok ?????????  EQfetch EQeval)
2768  #st3 * #EQ destruct *  #taf #tafne %{st3} %{taf} >tafne normalize nodelta
2769  % [% //] whd >as_label_ok [2:assumption] %
2770| (*FIN*)
2771  cases fin_step in EQfetch;
2772  [ (*GOTO*) #lbl #EQfetch  whd in match joint_classify; normalize nodelta
2773  >EQfetch in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ? ]); normalize nodelta
2774    cases (eval_goto_ok … EQfetch EQeval)
2775    #st3 * #EQ destruct * #taf #tarne %{st3} %{taf} >tarne normalize nodelta
2776    % [% //] whd >as_label_ok [2:assumption] %
2777  | (*RETURN*) #EQfetch
2778     whd in match joint_classify; normalize nodelta
2779    >EQfetch in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ? ]); normalize nodelta
2780    cases (eval_return_ok … EQfetch EQeval) #is_ret
2781    * #st3 * #EQ destruct * #after_ret * #taf ** #taf_prf #EQeval' #ret_prf
2782    % [2: % [2: % [2: %{(taa_base …)} %{taf}] |*: ] |*:]
2783    % [2: whd >as_label_ok %] % [2: assumption] % [2: %] % [2: assumption]
2784    % assumption
2785  | (*TAILCALL*) #fl #called #args #EQfetch
2786    cases (eval_tailcall_ok … EQfetch EQeval) #st3 * #EQ destruct * #is_tailcall
2787    * #is_tailcall' *  #eq_call #EQeval' >is_tailcall normalize nodelta
2788    #prf  %{«?, is_tailcall'»} %{eq_call}
2789    % [2: % [2: %{(taa_base …)} %{(taa_base …)}  % [ %{EQeval'} % |] | ] | ]
2790    whd >as_label_ok %
2791  ]
2792]
2793qed.
2794
2795
2796
Note: See TracBrowser for help on using the repository browser.