source: src/ERTLptr/ERTLtoERTLptrOK.ma @ 2601

Last change on this file since 2601 was 2601, checked in by sacerdot, 8 years ago

Extraction to ocaml is now working, with a couple of bugs left.
One limitation is that it is not possible to have two files with the
same name in different directories. Therefore this commit renames files
to avoid this situation.

The extracted directory contains:

  1. a snapshot of the .ml(i) files extracted from CerCo? by running ocamlc.opt -extract_ocaml compiler.ma The files have been patched by hand to implement all strings and fix the bugs.
  2. a file PROBLEMS that describes the remaining problems, i.e. bugs and axioms to be implemented

To obtain the compiler, run ocamlbuild compiler.byte.
At the moment it fails because of the three remaining axioms.

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/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.