source: src/ERTLptr/ERTLtoERTLptrOK.ma @ 2590

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

added monad machineary for ERTL to ERTLptr translation
eval_seq_no_pc case in place in ERTLptr translation

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