source: src/ERTLptr/ERTLtoERTLptrOK.ma @ 2592

Last change on this file since 2592 was 2592, checked in by piccolo, 8 years ago

main lemma of ERTLptr in place

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