source: src/ERTLptr/ERTLtoERTLptrOK.ma @ 2645

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