source: src/ERTLptr/ERTLtoERTLptrOK.ma @ 2663

(**************************************************************************)
(*       ___                                                              *)
(*      ||M||                                                             *)
(*      ||A||       A project by Andrea Asperti                           *)
(*      ||T||                                                             *)
(*      ||I||       Developers:                                           *)
(*      ||T||         The HELM team.                                      *)
(*      ||A||         http://helm.cs.unibo.it                             *)
(*      \   /                                                             *)
(*       \ /        This file is distributed under the terms of the       *)
(*        v         GNU General Public License Version 2                  *)
(*                                                                        *)
(**************************************************************************)

include "ERTLptr/ERTLtoERTLptr.ma".
include "common/StatusSimulation.ma".   
include "joint/Traces.ma".
include "ERTLptr/ERTLptr_semantics.ma".
include "common/ExtraMonads.ma".

definition ERTL_status ≝ 
λprog : ertl_program.λstack_sizes.
joint_abstract_status (mk_prog_params ERTL_semantics prog stack_sizes).

definition ERTLptr_status ≝ 
λprog : ertlptr_program.λstack_sizes.
joint_abstract_status (mk_prog_params ERTLptr_semantics prog stack_sizes).

definition sigma_map ≝ λ prog : ertl_program.
joint_closed_internal_function ERTL (prog_var_names … prog) → label → option label.


definition sigma_pc_opt : 
∀ prog : ertl_program.
sigma_map prog → program_counter → option program_counter ≝
λprog,sigma,pc.
  let ge ≝ globalenv_noinit … prog in
  if eqZb       (block_id (pc_block pc)) (-1) then (* check for dummy exit pc *)
    return pc
  else 
    ! 〈i, fd〉 ← res_to_opt … (fetch_internal_function … ge (pc_block pc)) ;
    ! ertl_ptr_point ← sigma fd (point_of_pc ERTL_semantics pc) ;
    return pc_of_point 
    ERTLptr_semantics (pc_block pc) ertl_ptr_point.

definition sigma_stored_pc ≝ 
λprog,sigma,pc. match sigma_pc_opt prog sigma pc with
      [None ⇒ null_pc (pc_offset … pc) | Some x ⇒ x].
      
      
definition sigma_beval :
 ∀prog : ertl_program.
  sigma_map prog →
  beval → beval ≝
λprog,sigma,bv.
match bv with
[ BVpc pc prt ⇒ match sigma_pc_opt prog sigma pc with 
                 [None ⇒ BVundef | Some x ⇒ BVpc x prt]
| _ ⇒ bv
].

(*
definition sigma_beval :
 ∀prog,sigma,bv.
 sigma_beval_opt prog sigma bv ≠ None ? → beval ≝
 λprog,sigma,bv.opt_safe ….
*)
definition sigma_is :
 ∀prog : ertl_program.
  sigma_map prog →
  internal_stack → internal_stack ≝
λprog,sigma,is.
match is with
[ empty_is ⇒ empty_is
| one_is bv ⇒ one_is (sigma_beval prog sigma bv)
| both_is bv1 bv2 ⇒
  both_is (sigma_beval prog sigma bv1) (sigma_beval prog sigma bv2)
].

lemma sigma_is_empty : ∀prog,sigma.
  sigma_is prog sigma empty_is = empty_is.
#prog #sigma %
qed.

definition sigma_mem :
 ∀prog : ertl_program . sigma_map prog → bemem → bemem ≝
 λprog,sigma,m.
 mk_mem
  (λb.
    If Zltb (block_id b) (nextblock m) then with prf' do    
      let l ≝ low_bound m b in
      let h ≝ high_bound m b in
      mk_block_contents l h
      (λz.If Zleb l z ∧ Zltb z h then with prf'' do
        sigma_beval prog sigma (contents (blocks m b) z)
      else BVundef)
    else empty_block OZ OZ)
  (nextblock m)
  (nextblock_pos m).

(*DOPPIONE ASSIOMA IN LINEARISE_PROOF.MA *)
axiom mem_ext_eq :
  ∀m1,m2 : mem.
  (∀b.let bc1 ≝ blocks m1 b in
      let bc2 ≝ blocks m2 b in
      low bc1 = low bc2 ∧ high bc1 = high bc2 ∧
      ∀z.contents bc1 z = contents bc2 z) →
  nextblock m1 = nextblock m2 → m1 = m2.



inductive id_is_in (A : Type[0]) : Pos →  positive_map A → Prop ≝ 
| is_in_root : ∀l,r,opt_a. id_is_in A (one) (pm_node … opt_a l r)
| is_in_left : ∀l,r,opt_a,x. id_is_in A x l → 
                                    id_is_in A (p0 x) (pm_node … opt_a l r)
| is_in_right : ∀l,r,opt_a,x. id_is_in A x r → 
                                    id_is_in A (p1 x) (pm_node … opt_a l r).

definition id_is_in : ∀A : Type[0]. ∀tag : identifierTag. 
identifier_map tag A → identifier tag → Prop ≝ 
λA,tag,m,id.match id with 
     [an_identifier x ⇒ match m with 
                              [an_id_map p ⇒ id_is_in A x p]
     ].
     
lemma lookup_eq : ∀ A : Type[0].
∀m,m' : positive_map A.
(∀id. lookup_opt A id m = lookup_opt A id m'
      ∧ (id_is_in A id m ↔ id_is_in A id m')) → m=m'.
#A #m elim m 
[ * [#_ %] #opt_a #l #r #H lapply(H one) normalize * #EQ >EQ * #_ #H1 lapply(H1 ?) [%]
  -H1 -H <EQ -EQ #H inversion H #l1 #r1 #opt_a1
  [ #_ #EQ  lapply(jmeq_to_eq ??? EQ) -EQ #EQ destruct(EQ)
  |*: #pos #H1 #_ #_ #EQ  lapply(jmeq_to_eq ??? EQ) -EQ #EQ destruct(EQ)
  ]
| #opt_a #l #r #Hl #Hr *
  [ #H lapply(H one) normalize * #EQ >EQ * #H1 #_ lapply(H1 ?) [%]
  -H1 -H -EQ #H inversion H #l1 #r1 #opt_a1
    [ #_ #EQ  lapply(jmeq_to_eq ??? EQ) -EQ #EQ destruct(EQ)
    |*: #pos #H1 #_ #_ #EQ  lapply(jmeq_to_eq ??? EQ) -EQ #EQ destruct(EQ)
    ]
  | #opt_a1 #l1 #r1 #H lapply(H one) normalize * #EQ >EQ -EQ #_ @eq_f2 [@Hl|@Hr]
    #id [ lapply(H (p0 id)) | lapply(H (p1 id))] normalize * #H1 * #H2 #H3 %
    [1,3: assumption] % #H4 [1,3: lapply(H2 ?) |*: lapply(H3 ?)]
    try %2 try %3 try assumption #H5 inversion H5 #l2 #r2 #opt_a2
    [1,4,7,10: #EQ lapply(jmeq_to_eq ??? EQ) -EQ #EQ @⊥
               [1,3: cut(p0 id ≠ one) [1,3: @(pos_elim … id) /3/]
               |*:   cut(p1 id ≠ one) [1,3: @(pos_elim … id) /3/]
               ] * #H @H assumption
    |*: #pos #H6 #_ #EQ lapply(jmeq_to_eq ??? EQ) -EQ #EQ destruct(EQ)
        #EQ lapply(jmeq_to_eq ??? EQ) -EQ #EQ destruct(EQ) #_ assumption
    ]
  ]
]
qed.

include alias "common/Identifiers.ma".
include alias "common/PositiveMap.ma".


lemma p0_neq_one : ∀x: Pos. p0 x ≠ one.
#x /3/
qed.

lemma p1_neq_one : ∀x: Pos. p1 x ≠ one.
#x /3/
qed.

lemma lookup_ok_to_update : ∀ A : Type[0].
∀ tag : identifierTag.
∀m,m' : identifier_map tag A. ∀id,a.
(lookup tag A m' id = Some ? a)  → lookup tag A m id ≠ None ? → 
(∀ id'. id ≠ id' → (lookup tag A m id' = lookup tag A m' id') ∧ 
     (id_is_in A tag m id' ↔ id_is_in A tag m' id')) → 
update tag A m id a = return m'.
#A #tag * #m * #m' * #id #a 
normalize in ⊢ (%→%→?); lapply id -id lapply m' -m' elim m 
    [ #m' #id #m_spec' normalize in ⊢ (% → ?); * #EQ @⊥ @EQ %] #opt_a #l #r #Hl #Hr 
    #m' * [|*: #x] normalize in ⊢ (%→%→?); #m_spec'
    [ cases opt_a -opt_a [* #H @⊥ @H %] #a1 #_ #H normalize @eq_f @eq_f
      lapply H -H lapply m_spec'; -m_spec' lapply a -a cases m'
      [#a normalize #EQ destruct] #opt_a1 #l1 #r1 #a 
      normalize in ⊢ (%→?); #EQ >EQ #H @eq_f2 @lookup_eq #id'
      [ lapply (H (an_identifier tag (p0 id')) ?) 
      | lapply (H (an_identifier tag (p1 id')) ?)
      ]
      [1,3:% @(pos_elim … id') [1,3:#H destruct|*: #n #IP #H destruct]]
      * normalize #H1 * #H2 #H3 % [1,3: >H1 %] % #H4 
      [1,3: lapply(H2 ?) |*: lapply(H3 ?)] try %2 try %3 try assumption
      #H5 inversion H5 #l2 #r2 #opt_a2
        [1,4,7,10: #EQ lapply(jmeq_to_eq ??? EQ) -EQ #EQ @⊥ 
                   [1,3: cut(p0 id' ≠ one) [1,3: /3/]
                   |*: cut(p1 id' ≠ one) [1,3: /3/]
                   ] >EQ * #H @H %
        |*: #pos #H6 #_ #EQ1 lapply(jmeq_to_eq ??? EQ1) -EQ1 #EQ1 destruct(EQ1)
            #EQ1 lapply(jmeq_to_eq ??? EQ1) -EQ1 #EQ1 destruct(EQ1) #_ assumption
        ]
    |*: #H lapply m_spec' -m_spec' cases m' -m' [1,3: normalize #EQ destruct] 
        #opt_a1 #l1 #r1 normalize in ⊢ (% → ?); #H1 #H2
        [ lapply(Hr ?? H1 H ?) | lapply(Hl ?? H1 H ?)] 
          [1,3: * #y * #y_spec 
            [lapply(H2 (an_identifier tag (p1 y)) ?) | lapply(H2 (an_identifier tag (p0 y)) ?)]
            [1,3: % #EQ destruct @y_spec %] * normalize #H3 * #H4 #H5 % // % #H6
            [1,3: lapply(H4 ?) |*: lapply (H5 ?)] try %2 try %3 try assumption
            #H7 inversion H7 #l2 #r2 #opt_a2
              [1,4,7,10: #EQ lapply(jmeq_to_eq ??? EQ) -EQ #EQ @⊥ 
                   [1,3: cut(p1 y ≠ one) [1,3: /3/]
                   |*: cut(p0 y ≠ one) [1,3: /3/]
                   ] >EQ * #H @H %
              |*: #pos #H6 #_ #EQ1 lapply(jmeq_to_eq ??? EQ1) -EQ1 #EQ1 
                 destruct(EQ1) #EQ1 lapply(jmeq_to_eq ??? EQ1) -EQ1 #EQ1 
                 destruct(EQ1) #_ assumption
              ]
          |2,4: normalize cases(update A x a ?) normalize [2,4: #pos_map] 
               #EQ destruct @eq_f @eq_f lapply(H2 (an_identifier tag one) ?)
               [1,3: % #EQ destruct] * normalize #EQ >EQ #_ @eq_f2 [2,3: %]
               @lookup_eq #id'
               [lapply (H2 (an_identifier tag (p0 id')) ?) | 
                                   lapply (H2 (an_identifier tag (p1 id')) ?) ]
               [1,3: % #EQ1 destruct] * normalize #H3 * #H4 #H5 % // % #H6
               [1,3: lapply(H4 ?) |*: lapply(H5 ?)] try %2 try %3 try assumption
               #H7 inversion H7 #l2 #r2 #opt_a2
                  [1,4,7,10: #EQ lapply(jmeq_to_eq ??? EQ) -EQ #EQ @⊥ 
                    [1,3: cut(p0 id' ≠ one) [1,3: /3/]
                    |*: cut(p1 id' ≠ one) [1,3: /3/]
                   ] >EQ * #H @H %
                  |*: #pos #H6 #_ #EQ1 lapply(jmeq_to_eq ??? EQ1) -EQ1 #EQ1 
                      destruct(EQ1) #EQ1 lapply(jmeq_to_eq ??? EQ1) -EQ1 #EQ1 
                      destruct(EQ1) #_ assumption
                  ]
            ]
      ] 
qed.

lemma update_ok_to_lookup : ∀ A : Type[0].
∀ tag : identifierTag.
∀m,m' : identifier_map tag A. ∀id,a.
update tag A m id a = return m' → 
(lookup tag A m' id = Some ? a) ∧ lookup tag A m id ≠ None ? ∧
(∀ id'. id ≠ id' → (lookup tag A m id' = lookup tag A m' id') ∧ 
     (id_is_in A tag m id' ↔ id_is_in A tag m' id')).
#A #tag * #m * #m' * #id #a 
whd in ⊢ (??%% →  ?); inversion(update A ???) normalize nodelta [#_ #ABS destruct]
    #m1 #m1_spec #EQ destruct % [%] 
    [  normalize @(update_lookup_opt_same … m1_spec)
    |3: * #id' * #id_spec' normalize %
        [@(update_lookup_opt_other … m1_spec ??) % #EQ @id_spec' >EQ %]
        lapply id_spec' lapply m1_spec -id_spec' -m1_spec 
        (*cases id [|*:#x] -id normalize*) lapply m' -m' lapply id lapply id' -id -id'
        elim m [#id' #id #m' cases id [|*: #x] normalize #EQ destruct] 
        #opt_a #l #r #Hl #Hr #id' #id #m' cases id [|*:#x] -id normalize 
        [ cases opt_a [2:#a] normalize #EQ destruct cases id' [#H @⊥ @H %] 
          #x #_ normalize % #H [1,2: %3 |*: %2]
          inversion H #l1 #r1 #opt_a1 
          [1,4,7,10: #EQ lapply(jmeq_to_eq ??? EQ) #EQ1 @⊥ 
                     [1,2: cut(p1 x ≠ one) [1,3: @(pos_elim … x) /3/]
                     |*:   cut(p0 x ≠ one) [1,3: @(pos_elim … x) /3/]
                     ] 
                     * #H @H >EQ1 //   
          |*:        #pos #H1 #_ #EQ lapply(jmeq_to_eq ??? EQ) #EQ1 destruct(EQ1)
                     #EQ lapply(jmeq_to_eq ??? EQ) #EQ1 destruct(EQ1) #_ assumption
          ]
        |*: inversion(update A x a ?) normalize [1,3: #_ #EQ destruct] #pos_map
            #pos_map_spec #EQ destruct #id_spec' % #H
            inversion H #l1 #l2 #opt_a1
            [1,4,7,10: #EQ lapply(jmeq_to_eq ??? EQ) -EQ #EQ 
                       #EQ1 lapply(jmeq_to_eq ??? EQ1) -EQ1 #EQ1 destruct(EQ1)
                       #H1 %
            |*: #pos #H1 #_ #EQ lapply(jmeq_to_eq ??? EQ) -EQ #EQ 
                #EQ1 lapply(jmeq_to_eq ??? EQ1) -EQ1 #EQ1 destruct(EQ1)
                #H2 try %2 try %3 try assumption
                [ @(proj1 … (Hr ? ? pos_map pos_map_spec ?)) [#EQ1 destruct @id_spec' %]
                | @(proj2 … (Hr ? ? l2 pos_map_spec ?)) [#EQ1 destruct @id_spec' %]
                | @(proj1 … (Hl ? ? pos_map pos_map_spec ?)) [#EQ1 destruct @id_spec' %]
                | @(proj2 … (Hl ? ? l1 pos_map_spec ?)) [#EQ1 destruct @id_spec' %]
                ]
                assumption
            ]
         ]      
    | % normalize lapply m1_spec lapply id lapply m' -id -m' elim m
      [#m' * [|*: #x] normalize #EQ destruct] #opt_a #l #r #Hl #Hr #m' * [|*: #x] 
      normalize [ cases opt_a [2:#a] normalize #EQ1 #EQ2 destruct]
      inversion (update A x a ?) [1,3: #_ normalize #EQ destruct]
      #pos_map #EQpos_map normalize #EQ destruct [@Hr|@Hl] assumption
    ]
qed.


(*
               
lemma update_lookup_after : ∀ A : Type[0].
∀ tag : identifierTag.
∀m,m' : identifier_map tag A. ∀id,a.
update tag A m id a = return m' → 
lookup tag A m' id = Some ? a.
#A #B #tag * #m1 * #id #a whd in ⊢ (??%% → ?); inversion(update A ???) 
normalize nodelta [#_ #EQ destruct] #pos_map #pos_map_spec #EQ destruct
@(update_lookup_opt_same … pos_map_spec)
qed.

lemma p0_neq_one : ∀x: Pos. p0 x ≠ one.
#x /3/
qed.

lemma p1_neq_one : ∀x: Pos. p1 x ≠ one.
#x /3/
qed.

lemma id_is_in_map : ∀ A,B : Type[0]. ∀tag : identifierTag.
∀m : identifier_map tag A. 
∀ F : (∀a:A.(Σid. lookup tag A m id = Some A a) → B). 
∀id. id_is_in A tag m id ↔ id_is_in B tag (map_inf1 A B tag m F) id.
#A #B #tag * #m elim m
[ #F * #id % normalize #H inversion H #l #r #opt_a
  [1,4: #_ #EQ lapply(jmeq_to_eq ??? EQ) -EQ #EQ destruct
  |*: #pos #H1 #_ #_ #EQ lapply(jmeq_to_eq ??? EQ) -EQ #EQ destruct
  ]
| * [2:#a] #l #r #Hl #Hr #F ** [1,4: |*:#x] normalize % #H try % try %2 try %3
  [1,2,5,6: cases(Hr ? (an_identifier tag x)) |*: cases (Hl ? (an_identifier tag x))]
  [2,4,6,8,10,12,14,16: #a1 ** #id1 #prf1 @F try(@a1)
                        try(%{(an_identifier tag (p1 id1))} assumption) 
                        try(%{(an_identifier tag (p0 id1))} assumption) ] 
  try(#H1 #_ @H1) try(#_ #H1 @H1) -H1 -Hl -Hr inversion H #l1 #r1 #opt_a1
  [1,4,7,10,13,16,19,22: #EQ lapply(jmeq_to_eq ??? EQ) -EQ #EQ @⊥
             [1,2,3,4: lapply(p1_neq_one x)
             |*:       lapply(p0_neq_one x)
             ] * #H @H >EQ %
  |*: #pos #H1 #_ #EQ lapply(jmeq_to_eq ??? EQ) -EQ #EQ destruct
      #EQ lapply(jmeq_to_eq ??? EQ) -EQ #EQ destruct #_ assumption
  ]
]
qed.

lemma map_update_commute : ∀ A, B : Type[0].
∀tag : identifierTag.
∀m1,m2 : identifier_map tag A.
∀id,a.
update tag A m1 id a = return m2 →
∀ F : (∀a:A.(Σid. lookup tag A m1 id = Some A a) → B).
∀ F': (∀a:A.(Σid. lookup tag A m2 id = Some A a) → B).  
(∀a',id',prf,prf'. F a' «id',prf» = F' a' «id',prf'») → ∃prf.
update tag B (map_inf1 A B tag m1 F) id (F' a «id,prf») = 
return map_inf1 A B tag m2 F'.
#A #B #tag #m1 #m2 #id #a #m2_spec #F #F' #eqFF' %
[ @hide_prf cases(update_lookup_previous A tag m1 m2 id a) #H1 #_ cases (H1 m2_spec) 
  * #H1 #H2 #H3 assumption
| cases(update_lookup_previous B tag (map_inf1 A B tag m1 F) 
                             (map_inf1 A B tag m2 F') id (F' a «id,?»))
  [ #_ #H @H |] cases(update_lookup_previous A tag m1 m2 id a) #H2 #INUTILE
cases(H2 m2_spec) * #H3 #H4 #H5 % [%] 
[ >(lookup_map … H3) %
| elim H4 -H4 #H4 % #H5 @H4 lapply H5 cases m1 in F; -m1 #m1 cases id -id 
  elim m1 [ #id #F normalize * %] #a1 #l #r #Hl #Hr * [|*:#x] #F normalize
  [ cases a1 in F; [2: #a2] #F normalize [2: * %] #EQ destruct
  |*: #H 
    [@(Hr x ??) | @(Hl x ??)]
    [1,3:#a ** #id1 #prf1 @F [1,3: @a] 
         [%{(an_identifier tag (p1 id1))}|%{(an_identifier tag (p0 id1))}] 
         normalize assumption
    |*: normalize @H
    ]
  ]
| #id' #id_spec' lapply(H5 id' id_spec') * #H6 * #H7 #H8 %
  [ lapply H6 inversion (lookup tag A m2 id') 
    [2: #w] #w_spec #EQ >(lookup_map … EQ) normalize nodelta
    >(lookup_map … w_spec) normalize nodelta [2: %] @eq_f @eqFF'
  | cases(id_is_in_map A B tag m1 F id') cases(id_is_in_map A B tag m2 F' id')
   #H9 #H10 #H11 #H12 % #H13 [ @H9 @H7 @H12 assumption | @H11 @H8 @H10 assumption]
  ]
]
qed.

(*
definition well_formed_register_env :
∀prog : ertl_program .∀sigma : (sigma_map prog).
register_env beval → Prop ≝
λprog,sigma,psd_reg.∀id,bv. lookup ?? psd_reg id = Some ? bv → 
sigma_beval_opt prog sigma bv ≠ None ?.
*)
*)

definition map : ∀tag,A,B. identifier_map tag A → (A → B) → identifier_map tag B ≝ 
λtag,A,B,m,f.match m with
[an_id_map p ⇒ an_id_map … (map ?? f p)].

lemma lookup_map : ∀A,B : Type[0].
  ∀tag : identifierTag.
  ∀m : identifier_map tag A.
  ∀ f:A → B.
  ∀ id. 
lookup tag B (map tag A B m f) id = 
! a ← lookup tag A m id; return f a.
#A #B #tag * #m #f * #id normalize >lookup_opt_map %
qed.

lemma update_leaf_fail: ∀tag,A,i,v.
 update tag A (empty_map ??) i v = Error ? [MSG MissingId; CTX … i].
#ta #A ** [|*: #x] #v normalize %
qed.

lemma update_def : ∀tag,A,m,i,v.
  update tag A m i v =
  match lookup tag A m i with
  [ Some _ ⇒ OK ? (add tag A m i v)
  | None ⇒ Error ? [MSG MissingId; CTX … i]
  ].
#tag #A #m #i #v inversion(update tag A m i v)
[ #m' #EQm' cases(update_ok_to_lookup ?????? EQm') * #_
 #H #_ elim H cases(lookup tag A m i) [#H @⊥ @H %]
 #x #_ normalize <EQm' lapply EQm' cases i cases m cases m' -m -m' -i 
 normalize #m' #m #i inversion(update A i v m) normalize [#_ #ABS destruct]
 #m'' #EQm'' #EQ destruct(EQ) @eq_f @eq_f lapply EQm'' -EQm'' lapply i -i
 lapply m' -m' elim m [#m' * [2,3: #z] normalize #EQ destruct]
 #opt_a #l #r #Hl #Hr #m' * [2,3: #z] normalize
 [3: cases opt_a normalize [2: #y] #EQ destruct %
 |*: inversion(update A z v ?) [2,4: #m'']  #EQm'' normalize #EQ destruct
     [<(Hr … EQm'') | <(Hl … EQm'')] % 
 ]
| #err cases m -m cases i -i #i #m normalize inversion(update A i v m) [2:#m'] 
  #EQerr normalize #EQ destruct lapply EQerr lapply i elim m
  [ normalize #x #_ %] #opt_a #l #r #Hl #Hr * [2,3:#z] normalize
 [3: cases opt_a [2:#w] normalize #EQ destruct %
 |*: inversion(update A z v ?) [2,4: #m'] #EQm' normalize #EQ destruct
     [lapply(Hr … EQm') | lapply(Hl … EQm')] cases(lookup_opt A z ?) [2,4: #a] 
     normalize #EQ destruct %
 ]
]
qed.

lemma map_add : ∀tag : identifierTag.∀A,B : Type[0].∀ f: A → B.∀m,id,v.
map tag A B (add tag A m id v) f = add tag B (map tag A B m f) id (f v).
#tag #A #B #f * #m * #id #v normalize @eq_f lapply v -v lapply id -id elim m
[ #id elim id [#v %] #x #IH #id normalize >IH normalize inversion(pm_set ? ? ? ?) 
  normalize // cases x normalize [2,3,5,6: #y] #EQ destruct
| #opt_a #l #r #Hl #Hr * [2,3: #x| #v normalize cases opt_a normalize [2: #a %]
  cases (map_opt ? ? ? l) normalize [2: //] cases (map_opt ? ? ? r) normalize 
  //] #v normalize cases opt_a [2,4: #a] normalize // 
  [ cases(map_opt ? ? ? l) normalize // >Hr cases(map_opt ? ? ? r) normalize
    [2: #opt_b #lb #rb] inversion(pm_set B x ? ?) normalize // cases x [2,3,5,6: #y]
    normalize #EQ destruct
  | >Hl cases(map_opt ? ? ? l) normalize [2: #opt_b #lb #rb] 
    inversion (pm_set B x ? ?) normalize // 
    [1,2: cases x [2,3,5,6: #y] normalize #EQ destruct]
    #opt_b' #lb' #rb' #_ normalize #_ #EQ cases(map_opt ? ? ? r) 
    normalize nodelta [%] #opt_b'' #lb'' #rb'' >EQ %
]
qed.


definition restrict : ∀tag.∀A,B.
identifier_map tag A → identifier_map tag B → identifier_map tag A ≝ 
λtag,A,B,m1,m2.an_id_map … 
           (merge A B A (λo,o'.match o' with [None ⇒ None ? | Some _ ⇒ o])
                  (match m1 with [an_id_map p1 ⇒ p1])
                  (match m2 with [an_id_map p2 ⇒ p2])).

interpretation "identifier map restriction" 'intersects a b = (restrict ??? a b).

unification hint 0 ≔ tag ; R ≟ identifier tag ⊢ list R ≡ list (identifier tag).
 
lemma map_update_commute : ∀tag : identifierTag.∀A,B : Type[0].∀f : A → B. ∀m,id,v. 
update tag B (map tag A B m f) id (f v) = 
!m' ← update tag A m id v; return map tag A B m' f.
#tag #A #B #f #m #id #v >update_def >update_def >lookup_map
cases (lookup tag A m id) [%] #a >m_return_bind >m_return_bind normalize nodelta
whd in ⊢ (???%); @eq_f @sym_eq @map_add
qed.

definition is_leaf ≝ λA.λpm : positive_map A.
match pm with [ pm_leaf ⇒ true | _ ⇒ false ].
(*
let rec pm_clean A (pm : positive_map A) on pm : positive_map A ≝
match pm with
[ pm_leaf ⇒ pm_leaf ?
| pm_node o l r ⇒
  let l' ≝ pm_clean … l in
  let r' ≝ pm_clean … r in
  match o with
  [ Some _ ⇒ pm_node … o l' r'
  | None ⇒
    if is_leaf … l' ∧ is_leaf … r' then pm_leaf ? else
    pm_node … o l' r'
  ]
]. 
 
definition clean ≝ λtag,A.λm : identifier_map tag A.
  match m with [ an_id_map pm ⇒ an_id_map tag A (pm_clean … pm) ].
*)

definition sigma_register_env :
∀prog : ertl_program.∀sigma : (sigma_map prog).
register_env beval → list register →  register_env beval ≝
λprog,sigma,psd_env,ids.
let m' ≝  map ??? psd_env (λbv.sigma_beval prog sigma bv) in
m' ∖ ids.

(*
definition well_formed_ertl_psd_env :
∀prog : ertl_program. ∀sigma : (sigma_map prog).
ertl_psd_env → Prop≝ 
λprog,sigma,psd_env.well_formed_register_env prog sigma (psd_regs psd_env).
*)
(*
let rec well_formed_frames 
(prog : ertl_program) (sigma : (sigma_map prog)) 
(l : list ertl_psd_env) on l : Prop ≝ 
match l with 
  [nil ⇒ True 
  | cons a tl ⇒ well_formed_ertl_psd_env prog sigma a ∧
               well_formed_frames prog sigma tl
  ].                            
*)


lemma lookup_restrict : ∀tag,A,B.∀a : identifier_map tag A.∀b : identifier_map tag B.
∀i.lookup ?? (a ∩ b) i = if i ∈ b then lookup … a i else None ?.
#tag #A #B * #a * #b * #i normalize >lookup_opt_merge [2: %] cases (lookup_opt B i b)
[2: #b] normalize % qed.


lemma lookup_set_minus : ∀tag,A,B. ∀a : identifier_map tag A. ∀b : identifier_map tag B.
∀i. lookup ?? (a ∖ b) i = if i ∈ b then None ? else lookup … a i.
#tag #A #B * #a * #b * #i normalize >lookup_opt_merge [2: %] cases(lookup_opt B i b)
[2: #b] % qed.

(*
lemma clean_add : ∀tag,A,m,i,v.clean … (add tag A m i v) = add tag A (clean … m) i v.
#tag #A * #m * #i #v normalize @eq_f
lapply m -m
elim i -i
[ * [%]
  * [2: #x] #l #r [%] normalize
  cases (pm_clean A l) normalize // cases (pm_clean A r) //
|*: #i #IH * normalize
  [1,3: >IH cases i // ]
  * [2,4: #x] #l #r normalize
  [1,2: >IH % ]
  >IH cases i cases (pm_clean A l) cases (pm_clean A r) normalize //
]
qed.

lemma clean_lookup : ∀tag,A,m,i.lookup … (clean tag A m) i = lookup … m i.
#tag #A * #m * #i normalize lapply i -i elim m
[#i %] * [2: #a] #l #r #Hl #Hr * [2,3,5,6: #x] normalize in ⊢ (???%);
[1,3:<Hr|2,4:<Hl] normalize try % [3: @if_elim #_ %] 
cases(pm_clean A l) in Hl; normalize 
[2: #opt_a1 #l1 #r1 #_ %
|3: #H cases(pm_clean A r) normalize //
| #H cases(pm_clean A r) in Hr; normalize //
| #opt_a1 #l1 #r1 #H cases x normalize //
]
qed.   

 
lemma clean_update : ∀tag,A,m,i,v.
! m' ← update tag A m i v; return clean … m' =
update tag A (clean … m) i v.
#tag #A #m #i #v
>update_def >update_def >clean_lookup cases (lookup tag A m i)
[ % ]
#m' >m_return_bind normalize nodelta >clean_add %
qed.
*)
lemma lookup_eq_id_map : ∀tag : identifierTag. ∀ A : Type[0].
∀m,m' : identifier_map tag A.
(∀id. lookup … m id = lookup … m' id
      ∧ (id_is_in A tag m id ↔ id_is_in A tag m' id)) → m=m'.
#tag #A * #m * #m' #H @eq_f @lookup_eq #id lapply(H (an_identifier tag id))
* #H1 #H2 % // assumption
qed.

(*
lemma clean_leaf : ∀tag : identifierTag . ∀ A : Type[0].
∀m : identifier_map tag A. (∀ id. lookup … m id = None ?) → 
clean ?? m = empty_map ??.
#tag #A * #m elim m [#_ %] #opt_a #l #r #Hl #Hr #H normalize @eq_f 
lapply(H (an_identifier tag one)) normalize #EQ >EQ -EQ normalize
lapply(Hl ?) [2: lapply(Hr ?)] 
  [1,3: * #id [lapply(H (an_identifier tag (p1 id))) | lapply(H (an_identifier tag (p0 id)))]
       #H assumption
  | normalize #EQ #EQ1 destruct >e0 >e1 normalize %
  ]
qed.
*)
lemma id_is_in_lookup : ∀tag,A,m,id,v.
 lookup tag A m id = Some ? v → id_is_in A tag m id.
#tag #A * #m * #id #a normalize lapply m -m elim id
[|*: #x #IH] * normalize [1,3,5: #EQ destruct] #opt_a #l #r [ #_ %] #H [%3 |%2]
@IH assumption
qed.
(*
lemma pm_clean_leaf : ∀ A : Type[0].
∀m : positive_map A. (∀ id. lookup_opt … id m = None ?) → 
pm_clean ? m = pm_leaf ….
#A #m elim m [ #id %] #opt_a #l #r #Hl #Hr #H normalize lapply(H one) normalize 
#EQ >EQ normalize >Hl [normalize >Hr [ %]] #id [@(H (p1 id))|@(H (p0 id))]
qed.


lemma pm_clean_canonic : ∀A,m,n.(∀i.lookup_opt A i m = lookup_opt A i n) →
  pm_clean ? m = pm_clean ? n.
#A #m #n lapply m -m elim n
[ @pm_clean_leaf ]
* [2: #x] #l #r #IHl #IHr *
  [1,3: #H @sym_eq @pm_clean_leaf #id @sym_eq @H ] #opt #l' #r' #H
 lapply (H one) normalize in ⊢ (%→?); #EQ destruct
 whd in ⊢ (??%%);
 >(IHl l') [1,3: >(IHr r') [1,3 : % ]] #i
 [1,2: @(H (p1 i)) |*: @(H (p0 i)) ] qed.


lemma clean_canonic : ∀tag,A,m,n.(∀i.lookup tag A m i = lookup tag A n i) →
  clean ?? m = clean ?? n.
#tag #A * #m * #n #H normalize @eq_f @pm_clean_canonic #i 
lapply(H (an_identifier tag i))
normalize //
qed.
*)
lemma update_fail_lookup : ∀tag,A,m,i,v,e.update tag A m i v = Error … e →  
  e = [MSG MissingId; CTX … i] ∧ lookup … m i = None ?.
#tag #A #m #i #v #errmsg >update_def cases(lookup tag A m i) [2: #a] normalize
#EQ destruct % //
qed.

lemma lookup_hit_update : ∀tag,A,m,i,v.i ∈ m →  
  ∃m'.update tag A m i v = OK ? m'.
#tag #A #m #i #v #H % [2: >update_def lapply(in_map_domain … m i) >H * #v #EQ >EQ
normalize %|]
qed.

lemma lookup_miss_update : ∀tag,A,m,i,v.lookup tag A m i = None ? →  
  update … m i v = Error … [MSG MissingId; CTX … i].
#tag #A #m #i #v #EQ >update_def >EQ normalize %
qed.

lemma update_ok_old_lookup : ∀tag,A,m,i,v,m'.update tag A m i v = OK ? m' →
  i ∈ m.
#tag #A #m #i #v #m' >update_def inversion(lookup tag A m i) [2: #a] #EQ normalize
#EQ destruct >EQ normalize @I
qed.

lemma lookup_update_ok : ∀tag,A,m,i,v,m',i'.update tag A m i v = OK ? m' →
  lookup … m' i' = if eq_identifier ? i' i then Some ? v else lookup … m i'.
#tag #A #m #i #v #m' #i' >update_def inversion(lookup tag A m i) [2: #a] #EQ
normalize nodelta #EQ1 destruct @eq_identifier_elim 
[ #H normalize nodelta >H @lookup_add_hit
| #H normalize nodelta @lookup_add_miss assumption
]
qed.

lemma mem_set_restrict : ∀tag,A,B.∀a : identifier_map tag A.∀b : identifier_map tag B.
∀i.i ∈ a ∩ b = (i ∈ a ∧ i ∈ b).
#tag #A #B * #a * #b  * #i normalize >lookup_opt_merge [2: %] cases(lookup_opt B i b)
[2: #a1] normalize [2: @if_elim #_ %] cases(lookup_opt A i a) [2: #a2] normalize %
qed.
(*
lemma merge_eq : ∀A.∀p : positive_map A.∀choice. merge 
*)
(*
lemma add_restrict : ∀tag,A,B.∀a : identifier_map tag A. ∀b : identifier_map tag B.
∀i,v.i∈b → add tag A (a ∩ b) i v = (add tag A a i v) ∩ b.
#tag #A #B * #a * #b * #i #v normalize inversion(lookup_opt B i b) normalize [#_ *]
#v1 #EQv1 * @eq_f lapply EQv1 lapply v1 lapply a lapply b -a -b -v1 elim i normalize
[ * normalize [#b #v #EQ destruct] #opt_a #l #r *
  [#v #EQ destruct normalize %] #opt_b #l1 #r1 #v #EQ destruct normalize cases opt_b
  normalize [2: #x %] cases(merge A B A ? l1 l) normalize [2: #opt_a2 #l2 #r2 %]
  cases(merge A B A ? r1 r) //
|*: #x #IH * [2,4: #opt_b #l1 #r1] #p1 normalize [3,4: #i #EQ destruct] cases p1 -p1
    [2,4: #opt_a #l2 #r2] normalize #v #H cases opt_b [2,4,6,8: #b] normalize 
    [1,2,5,6: <IH try assumption [1,2: cases opt_a [2,4: #a] normalize try %]
     cases(merge A B A ? l2 l1) normalize // lapply H [1,4: cases r1 |*: cases l1]
     normalize [1,3,5,7,9,11: #EQ destruct] #opt_b4 #l4 #r4 cases x normalize
     [1,4,7,10,13,16: #EQ destruct normalize // cases(merge A B A ? ? ?) normalize //] 
     #x #H normalize cases(merge A B A ? ? ?) normalize //
    |*: <IH try assumption 
       [1,3: cases(map_opt ? ? ? l1) normalize // lapply H cases r1 normalize 
            [1,3: #EQ destruct] #opt_b2 #l2 #r2 cases x [1,4: //] #x normalize //
       |*: lapply H cases x normalize [2,3,5,6: #y] cases l1 normalize 
          [1,3,5,7,9,11: #EQ destruct] #opt_b2 #l2 #r2 #H //
       ]
   ]
]
qed.

lemma update_restrict : ∀tag,A,B.∀a : identifier_map tag A.∀b : identifier_map tag B.
∀i,v.i ∈ b → update ?? (a ∩ b) i v = 
  ! a' ← update ?? a i v ; return a' ∩ b.
#tag #A #B #a #b #id #v #H
lapply (in_map_domain … b id) >H * #ignore #EQ_lookup_b
(*<clean_update*)
inversion (update tag A a id v)
[2: #e #EQ cases (update_fail_lookup ?????? EQ) #EQ1 #EQ2 destruct
  >lookup_miss_update [%]
  >lookup_restrict >H assumption ]
#m' #EQ >m_return_bind
cases (lookup_hit_update ?? (a∩b) id v ?)
[2: >mem_set_restrict >H >(update_ok_old_lookup ?????? EQ) % ]
#m'' >update_def >update_def in EQ; >lookup_restrict >H normalize nodelta 
cases(lookup tag A a id) normalize nodelta [#ABS destruct] #v1 #EQ #EQ'' destruct
whd in ⊢ (??%%); @eq_f @add_restrict assumption
qed.
*)
lemma add_set_minus  : ∀tag,A,B.∀a : identifier_map tag A.∀b : identifier_map tag B.
∀i,v.¬(i ∈ b) → add tag A (a ∖ b) i v = (add tag A a i v) ∖ b.
#tag #A #B * #a * #b * #i #v @notb_elim @if_elim normalize [#_ *] 
@if_elim [2: #_ *] @if_elim [#_ *] inversion(lookup_opt B i b) normalize [2: #x #_ *]
#H * * * * @eq_f lapply H -H lapply v -v lapply b -b lapply a -a elim i
[  * 
  [ * [2: #opt_b #l #r] #v normalize in ⊢ (% → ?); #EQ destruct [2: %]
  normalize in ⊢ (??%%); cases (map_opt ??? l) // normalize cases(map_opt ??? r)
  normalize //
  | * [2: #a] #l #r * [2,4: #opt_b #l1 #r1] #v normalize in ⊢ (% → ?); #EQ destruct
    normalize [3: % |1,2: cases(merge ???? l l1) // cases(merge ???? r r1) //]
    cases(map_opt ??? l) normalize // cases(map_opt ??? r) //
  ]
|2,3: #x #IH * [2,4: #opt_a #l #r] * [2,4,6,8: #opt_b #l1 #r1] #v 
      normalize in ⊢ (% → ?); #H whd in match (pm_set ????) in ⊢ (???%); 
      whd in match (merge ??????) in ⊢ (???%); 
      [1,2,3,4: <IH try assumption whd in match (pm_set ????) in ⊢ (??%?);
                whd in match (merge ??????) in ⊢ (??%?); cases opt_b normalize
                [2,4,6,8: #b] [5,6: cases opt_a normalize //]
                [1,2,3,4: cases (merge ???? l l1) normalize [2,4,6,8: #opt_a2 #l2 #r2] 
                          // cases (merge ???? r r1) normalize 
                          [2,4,6,8,10,12: #opt_a3 #l3 #r3] inversion(pm_set ????)
                          normalize // cases x 
                          [2,3,5,6,8,9,11,12,14,15,17,18,20,21,23,24 : #y]
                          normalize #EQ destruct
                |*: cases(map_opt ??? l1) normalize [2,4,6,8: #opt_a2 #l2 #r2] //
                    cases(map_opt ??? r1) normalize [2,4,6,8,10,12: #opt_a3 #l3 #r3]
                    inversion(pm_set ????) normalize // cases x 
                    [2,3,5,6,8,9,11,12,14,15,17,18,20,21,23,24 : #y]
                    normalize #EQ destruct
                ]
     |*: whd in match (pm_set ????) in ⊢ (??%?); 
         whd in match (merge ??????) in ⊢ (??%?); [1,2: cases opt_a [2,4: #a]] 
         normalize 
         [1,2: @eq_f2 [1,4:%] | cases(map_opt ??? l) [2: #opt_a1 #l1 #r1] normalize 
         | cases(map_opt ??? r) [2: #opt_a1 #l1 #r1] normalize]       
         [1,3,4: lapply(map_add tag A A (λx.x) (an_id_map … r) (an_identifier ? x) v)
         |2,5,6: lapply(map_add tag A A (λx.x) (an_id_map … l) (an_identifier ? x) v)
         |*: lapply(map_add tag A A (λx.x) (an_id_map … (pm_leaf ?)) (an_identifier ? x) v)
         ] normalize #EQ destruct >e0 try % [4,5: cases x [2,3,5,6: #y] normalize %]
           cases(map_opt ????) [2,4,6: #opt_a1 #l1 #r1] normalize
           inversion(pm_set ????) normalize // cases x [2,3,5,6,8,9,11,12: #y]
           normalize #EQ1 destruct 
     ]
]
qed.     

lemma update_set_minus : ∀tag,A,B.∀a : identifier_map tag A.∀b : identifier_map tag B.
∀i,v.¬(i ∈ b) → update ?? (a ∖ b) i v = 
  ! a' ← update ?? a i v ; return a' ∖ b.
#tag #A #B #a #b #id #v #H >update_def >lookup_set_minus @if_elim 
[ #H1 @⊥ lapply H1 lapply H @notb_elim >H1 normalize *] #_ >update_def
cases (lookup tag A a id) normalize [ %] #a @eq_f @add_set_minus assumption
qed.


record good_state_transformation 
(prog : ertl_program)
(def_in : joint_closed_internal_function ERTL (prog_var_names ?? prog)) :
Type[0] ≝ 
{ f_lbls : label → option (list label) 
; f_regs : label → option (list register)
; part_partition_f_lbls : partial_partition … f_lbls
; part_partion_f_regs : partial_partition … f_regs
; freshness_lab : let def_out ≝ translate_internal … def_in in 
     (∀l.opt_All … (All …
    (λlbl.¬fresh_for_univ … lbl (joint_if_luniverse … def_in) ∧
           fresh_for_univ … lbl (joint_if_luniverse … def_out))) (f_lbls l))
; freshness_regs : let def_out ≝ translate_internal … def_in in 
  (∀l.opt_All … (All …
    (λreg.¬fresh_for_univ … reg (joint_if_runiverse … def_in) ∧
           fresh_for_univ … reg (joint_if_runiverse … def_out))) (f_regs l))
; multi_fetch_ok : let def_out ≝ translate_internal … def_in in 
  let f_step ≝ translate_step ? in
  let f_fin ≝  translate_fin_step ? in
  ∀l,s.stmt_at … (joint_if_code … def_in) l = Some ? s →
  ∃lbls,regs.f_lbls l = Some ? lbls ∧ f_regs l = Some ? regs ∧
  match s with
  [ sequential s' nxt ⇒
    l ~❨f_step l s', lbls, regs❩~> nxt in joint_if_code … def_out
  | final s' ⇒
    l ~❨f_fin l s', lbls, regs❩~> it in joint_if_code … def_out
  | FCOND abs _ _ _ ⇒ Ⓧabs
  ]
}.

definition get_internal_function_from_ident : 
∀ p: sem_params. ∀ globals : list ident . ∀ge : genv_t (joint_function p globals).
ident → option (joint_closed_internal_function p globals) ≝ 
λp,globals,ge,id.
! bl  ← (find_symbol (joint_function p globals) ge id);
! bl' ← (code_block_of_block bl);
! 〈f,fn〉 ← res_to_opt … (fetch_internal_function ? ge bl');
return fn. 

definition get_sigma_from_good_state : 
∀prog : ertl_program. 
(∀ fn : joint_closed_internal_function ERTL (prog_var_names ?? prog).
good_state_transformation prog fn) → sigma_map prog ≝ 
λprog,good,fn,searched.
!〈res,s〉 ← find ?? (joint_if_code … fn) 
                (λlbl.λ_. match (f_lbls … (good fn)) lbl with
                          [None ⇒ false
                          |Some lbls ⇒ 
                             match lbls with
                                [nil ⇒ eq_identifier … searched lbl
                                |cons hd tl ⇒ let last ≝ last_ne … «hd::tl,I» in
                                          eq_identifier … searched last
                                ]
                          ]);
return res.


definition sigma_frames : ∀prog : ertl_program. 
(∀fn.good_state_transformation prog fn) → 
list (register_env beval × ident) → (list (register_env beval × ident)) ≝ 
λprog,good,frms. 
let sigma ≝ get_sigma_from_good_state … good in
foldr ?? 
(λx,tl.let 〈reg_env,id〉 ≝ x in 
       match get_internal_function_from_ident 
                  ERTL_semantics (prog_var_names … prog)
                  (globalenv_noinit … prog) id with
       [Some fn ⇒ 
  〈(sigma_register_env prog sigma reg_env 
       (added_registers … fn (f_regs … (good fn)))),id〉 :: tl
       |None ⇒ [ ]
       ]) ([ ]) frms.


(*
lemma sigma_empty_frames_commute :
∀prog : ertl_program. ∀ sigma : (sigma_map prog).
∃prf.
sigma_frames prog sigma [] prf = [].
#p #s % normalize %
qed.


let rec sigma_bit_vector_trie_opt (prog : ertl_program) 
(sigma : (sigma_map prog)) (n : nat) (t : BitVectorTrie beval n) 
on t : option … (BitVectorTrie beval n) ≝ 
match t with
  [Leaf bv ⇒ ! bv' ← (sigma_beval_opt prog sigma bv);
                   return Leaf … bv'
  |Node n1 b1 b2 ⇒ ! b1' ← (sigma_bit_vector_trie_opt prog sigma n1 b1);
                   ! b2' ← (sigma_bit_vector_trie_opt prog sigma n1 b2);
                   return Node … n1 b1' b2' 
  |Stub n1 ⇒  return Stub … n1
  ].


definition well_formed_hw_register_env : 
∀ prog : ertl_program. ∀ sigma : (sigma_map prog).
hw_register_env → Prop ≝
λprog,sigma,regs.sigma_bit_vector_trie_opt prog sigma 6 (reg_env … regs) ≠ None ?.
*)


include "common/BitVectorTrieMap.ma".

definition sigma_hw_register_env :
∀prog: ertl_program. ∀sigma : (sigma_map prog).
hw_register_env → hw_register_env ≝ 
λprog,sigma,h_reg.mk_hw_register_env
(map ? ? (sigma_beval prog sigma) 6 (reg_env … h_reg)) (other_bit … h_reg).


definition sigma_regs :
∀prog : ertl_program. ∀sigma : (sigma_map prog).
(register_env beval)×hw_register_env→ list register → 
(register_env beval)×hw_register_env ≝ 
λprog,sigma,regs,ids.let 〈x,y〉≝ regs in
      〈sigma_register_env prog sigma x ids,
       sigma_hw_register_env prog sigma y〉.
(*
lemma sigma_empty_regsT_commute :
∀prog : ertl_program. ∀sigma : (sigma_map prog).
∀ptr.∃ prf.
  empty_regsT ERTLptr_semantics ptr =
  sigma_regs prog sigma (empty_regsT ERTL_semantics ptr) prf.
#prog #sigma #ptr % 
[ @hide_prf whd in match well_formed_regs; normalize nodelta %
 [whd in match well_formed_ertl_psd_env; normalize nodelta #id #bv
  normalize in ⊢ (%→?); #EQ destruct
 | normalize % #EQ destruct
 ]
| % ]
qed.

axiom sigma_load_sp_commute : 
∀prog : ertl_program.∀sigma : (sigma_map prog).
∀regs,ptr.
load_sp ERTL_semantics regs = return ptr
→ ∃prf.
load_sp ERTLptr_semantics (sigma_regs prog sigma regs prf) = return ptr.

axiom sigma_save_sp_commute :
∀prog : ertl_program. ∀sigma : (sigma_map prog).
∀reg,ptr,prf1. ∃prf2.
save_sp ERTLptr_semantics (sigma_regs prog sigma reg prf1) ptr = 
sigma_regs prog sigma (save_sp ERTL_semantics reg ptr) prf2.

definition well_formed_state :
∀prog : ertl_program. ∀sigma : sigma_map prog.
state ERTL_semantics → Prop ≝ 
λprog,sigma,st.
well_formed_frames prog sigma (st_frms … st) ∧
sigma_is_opt prog sigma (istack … st) ≠ None ? ∧
well_formed_regs prog sigma (regs … st) ∧
well_formed_mem prog sigma (m … st).
*)

definition sigma_state : ∀prog : ertl_program. 
(∀fn.good_state_transformation prog fn) → 
 state ERTLptr_semantics → list register → 
 state ERTL_semantics ≝
λprog,good,st,ids.
let sigma ≝ get_sigma_from_good_state … good in
mk_state ?
  (sigma_frames prog good (st_frms ERTLptr_semantics st))
  (sigma_is ? sigma (istack … st))
  (carry … st)
  (sigma_regs ? sigma (regs … st) ids)
  (sigma_mem ? sigma (m … st)).


definition dummy_state : state ERTL_semantics ≝ 
mk_state ERTL_semantics
   [ ] empty_is BBundef 〈empty_map ? ?,mk_hw_register_env … (Stub …) BBundef〉 empty.
   
definition dummy_state_pc : state_pc ERTL_semantics ≝ 
mk_state_pc ? dummy_state (null_pc one) (null_pc one).

definition sigma_state_pc : 
∀prog : ertl_program. 
(∀fn.good_state_transformation prog fn) → 
state_pc ERTLptr_semantics → 
 state_pc ERTL_semantics ≝ 
λprog,good,st.
  let sigma ≝ get_sigma_from_good_state … good in
  let ge ≝ globalenv_noinit … prog in 
  if eqZb       (block_id (pc_block (pc … st))) (-1) then (* check for dummy pc *)
    dummy_state_pc
  else 
  match (fetch_internal_function (joint_closed_internal_function ERTL
         (prog_var_names (joint_function ERTL) ℕ prog)) ge (pc_block (pc … st))) with
   [OK x ⇒ let 〈i,fd〉 ≝ x in 
      mk_state_pc ? 
       (sigma_state prog good st (added_registers … fd (f_regs … (good fd))))
       (pc … st) (sigma_stored_pc prog sigma (last_pop … st))
   |Error msg ⇒ dummy_state_pc].


definition ERTLptrStatusSimulation :
∀ prog : ertl_program.
let trans_prog ≝ ertl_to_ertlptr prog in
∀stack_sizes.(∀fn.good_state_transformation prog fn) → 
status_rel (ERTL_status prog stack_sizes) (ERTLptr_status trans_prog stack_sizes) ≝ 
λprog,stack_sizes,good.
  let trans_prog ≝ ertl_to_ertlptr prog in 
    mk_status_rel ??
    (* sem_rel ≝ *) (λs1:ERTL_status prog stack_sizes
       .λs2:ERTLptr_status trans_prog stack_sizes
        .s1=sigma_state_pc prog good s2)
    (* call_rel ≝ *)  
          (λs1:Σs:ERTL_status prog stack_sizes
               .as_classifier (ERTL_status prog stack_sizes) s cl_call
       .λs2:Σs:ERTLptr_status trans_prog stack_sizes
                .as_classifier (ERTLptr_status trans_prog stack_sizes) s cl_call
        .let sigma ≝ get_sigma_from_good_state … good in 
        pc (mk_prog_params ERTL_semantics prog stack_sizes) s1
         =sigma_stored_pc prog sigma
          (pc
           (mk_prog_params ERTLptr_semantics (ertl_to_ertlptr prog) stack_sizes)
           s2)) 
    (* sim_final ≝ *) ?.
cases daemon
qed.

lemma fetch_function_no_minus_one :
  ∀F,V,i,p,bl.
  block_id (pi1 … bl) = -1 →
  fetch_function … (globalenv (λvars.fundef (F vars)) V i p)
    bl = Error … [MSG BadFunction].
 #F#V#i#p ** #r #id #EQ1 destruct
  whd in match fetch_function; normalize nodelta
  >globalenv_no_minus_one
  cases (symbol_for_block ???) normalize //
qed.
  
lemma fetch_function_no_zero :
 ∀F,V,i,p,bl.
  block_id (pi1 … bl) = 0 →
  fetch_function … (globalenv (λvars.fundef (F vars)) V i p)
    bl = Error … [MSG BadFunction].
 #F#V#i#p ** #r #id #EQ1 destruct
  whd in match fetch_function; normalize nodelta
  >globalenv_no_zero
  cases (symbol_for_block ???) normalize //
qed.

(*DOPPIONI dei LEMMI in LINEARISE_PROOF*)
lemma symbol_for_block_match:
    ∀M:matching.∀initV,initW.
     (∀v,w. match_var_entry M v w →
      size_init_data_list (initV (\snd v)) = size_init_data_list (initW (\snd w))) →
    ∀p: program (m_A M) (m_V M). ∀p': program (m_B M) (m_W M).
    ∀MATCH:match_program … M p p'.
    ∀b: block.
    symbol_for_block … (globalenv … initW p') b =
    symbol_for_block … (globalenv … initV p) b.
* #A #B #V #W #match_fn #match_var #initV #initW #H
#p #p' * #Mvars #Mfn #Mmain
#b
whd in match symbol_for_block; normalize nodelta
whd in match globalenv in ⊢ (???%); normalize nodelta
whd in match (globalenv_allocmem ????);
change with (add_globals ?????) in match (foldl ?????);
>(proj1 … (add_globals_match … initW … Mvars))
[ % |*:]
[ * #idr #v * #idr' #w #MVE %
  [ inversion MVE
    #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 destruct %
  | @(H … MVE)
  ]
| @(matching_fns_get_same_blocks … Mfn) 
  #f #g @match_funct_entry_id
]
qed.

lemma symbol_for_block_transf :
 ∀A,B,V,init.∀prog_in : program A V.
 ∀trans : ∀vars.A vars → B vars.
 let prog_out ≝ transform_program … prog_in trans in
 ∀bl.
 symbol_for_block … (globalenv … init prog_out) bl =
 symbol_for_block … (globalenv … init prog_in) bl.
#A #B #V #iV #p #tf @(symbol_for_block_match … (transform_program_match … tf ?))
#v0 #w0 * //
qed.

lemma fetch_function_transf :
 ∀A,B,V,init.∀prog_in : program A V.
 ∀trans : ∀vars.A vars → B vars.
 let prog_out ≝ transform_program … prog_in trans in
 ∀bl,i,f.
 fetch_function … (globalenv … init prog_in) bl = 
  return 〈i, f〉
→ fetch_function … (globalenv … init prog_out) bl =
  return 〈i, trans … f〉.
#A #B #V #init #prog_in #trans #bl #i #f
 whd in match fetch_function; normalize nodelta
 #H lapply (opt_eq_from_res ???? H) -H
 #H @('bind_inversion H) -H #id #eq_symbol_for_block
 #H @('bind_inversion H) -H #fd #eq_find_funct
 whd in ⊢ (??%?→?); #EQ destruct(EQ)
 >(symbol_for_block_transf … trans) >eq_symbol_for_block >m_return_bind
 >(find_funct_ptr_transf A B …  eq_find_funct) %
qed.


lemma fetch_internal_function_transf :
 ∀A,B.∀prog_in : program (λvars.fundef (A vars)) ℕ.
 ∀trans : ∀vars.A vars → B vars.
 let prog_out ≝ transform_program … prog_in (λvars.transf_fundef … (trans vars)) in
 ∀bl,i,f.
 fetch_internal_function … (globalenv_noinit … prog_in) bl = 
  return 〈i, f〉
→ fetch_internal_function … (globalenv_noinit … prog_out) bl =
  return 〈i, trans … f〉.
#A #B #prog #trans #bl #i #f
 whd in match fetch_internal_function; normalize nodelta
 #H @('bind_inversion H) * #id * #fd normalize nodelta #EQfetch
 whd in ⊢ (??%%→?); #EQ destruct(EQ)
 >(fetch_function_transf … EQfetch) %
qed.

(*
definition good_local_sigma :
  ∀globals.
  ∀g:codeT ERTLptr globals.
  (Σl.bool_to_Prop (code_has_label … g l)) →
  codeT ERTL globals →
  (label → option label) → Prop ≝
  λglobals,g,c,sigma.
    ∀l,l'.sigma l = Some ? l' →
      ∃s. stmt_at … g l = Some ? s ∧
          All ? (λl.sigma l ≠ None ?) (stmt_labels … s) ∧
          (match s with
           [ sequential s' nxt ⇒
             match s' with
             [ step_seq _ ⇒
               (stmt_at … c n = Some ? (sequential … s' it)) ∧
                  ((sigma nxt = Some ? (S n)) ∨
                   (stmt_at … c (S n) = Some ? (GOTO … nxt)))
             | COND a ltrue ⇒
               (stmt_at … c n = Some ? (sequential … s' it) ∧ sigma nxt = Some ? (S n)) ∨
               (stmt_at … c n = Some ? (FCOND … I a ltrue nxt))
             ]
           | final s' ⇒
             stmt_at … c n = Some ? (final … s')
           | FCOND abs _ _ _ ⇒ Ⓧabs
           ]).
 
*)

lemma ps_reg_retrieve_ok :  ∀prog : ertl_program. 
∀sigma : sigma_map prog. ∀r,restr.
preserving1 ?? res_preserve1 …
     (λregs.sigma_regs prog sigma regs restr)
     (sigma_beval prog sigma)
     (λregs.ps_reg_retrieve regs r)
     (λregs.ps_reg_retrieve regs r).
#prog #sigma #r #restr * #psd_r #hw_r whd in match ps_reg_retrieve; 
whd in match reg_retrieve; normalize nodelta @opt_to_res_preserve1
whd in match sigma_regs; whd in match sigma_register_env; normalize nodelta
>lookup_set_minus @if_elim [ #_ @opt_preserve_none1] #id_r_not_in
>(lookup_map ?? RegisterTag ???) #bv #H @('bind_inversion H) -H #bv1
#bv1_spec whd in ⊢ (??%? → ?); #EQ destruct %{bv1} % // >bv1_spec %
qed.

lemma hw_reg_retrieve_ok : ∀prog : ertl_program.
∀sigma : sigma_map prog. ∀r,restr.
preserving1 ?? res_preserve1 …
    (λregs.sigma_regs prog sigma regs restr)
    (sigma_beval prog sigma)
    (λregs.hw_reg_retrieve regs r)
    (λregs.hw_reg_retrieve regs r).
#prog #sigma #r #restr * #psd_r * #hw_r #b whd in match hw_reg_retrieve;
whd in match hwreg_retrieve; normalize nodelta whd in match sigma_regs;
whd in match sigma_hw_register_env; normalize nodelta
change with (sigma_beval prog sigma BVundef) in ⊢ (???????(??(?????%))?);
#bv >lookup_map whd in ⊢ (???% → ?); #EQ destruct 
%{(lookup beval 6 (bitvector_of_register r) hw_r BVundef)}
% //
qed.


lemma ps_reg_store_ok : ∀prog : ertl_program.
∀sigma : sigma_map prog. ∀r,restr.
preserving21 ?? res_preserve1 … 
   (sigma_beval prog sigma)
   (λregs.sigma_regs prog sigma regs restr)
   (λregs.sigma_regs prog sigma regs restr)
   (ps_reg_store r)
   (ps_reg_store r).
#prog #sigma #r #restr whd in match ps_reg_store; normalize nodelta
#bv * #psd_r #hw_r @mfr_bind1 
[ @(λr.sigma_register_env prog sigma r restr)
| whd in match reg_store; whd in match sigma_regs; normalize nodelta
  #x #x_spec lapply(update_ok_to_lookup ?????? x_spec) * * #_ #EQpsd #_ 
  lapply x_spec -x_spec lapply EQpsd -EQpsd whd in match sigma_register_env;
  normalize nodelta >lookup_set_minus @if_elim [ #_ * #H @⊥ @H %]
  #id_not_in #_ >update_set_minus [2: assumption] #H @('bind_inversion H) -H
  #x0 >map_update_commute #H @('bind_inversion H) -H #x1 #x1_spec
  whd in ⊢ (??%% → ??%% → ?); #EQ1 #EQ2 destruct %{x1} % //
| #x * #psd_r' #hw_r' whd in match sigma_regs; normalize nodelta
  whd in ⊢ (???% → ?); #EQ destruct %{〈x,hw_r〉} % //
]
qed.


lemma hw_reg_store_ok : ∀prog : ertl_program.
∀sigma : sigma_map prog. ∀r,restr.
preserving21 ?? res_preserve1 …
   (sigma_beval prog sigma)
   (λregs.sigma_regs prog sigma regs restr)
   (λregs.sigma_regs prog sigma regs restr)
   (hw_reg_store r)
   (hw_reg_store r).
#prog #sigma #r #restr whd in match hw_reg_store; normalize nodelta
#bv * #psd_r * #hw_r #b whd in match hwreg_store; whd in match sigma_regs; normalize nodelta
whd in match sigma_hw_register_env; normalize nodelta <insert_map * #psd_r' 
* #hw_r' #b' whd in ⊢ (???% → ?); #EQ destruct % [2: % [%] % |]
qed.


lemma ertl_eval_move_ok : ∀prog : ertl_program. 
∀sigma : sigma_map prog. ∀ restr,pm.
preserving1 ?? res_preserve1 …
     (λregs.sigma_regs prog sigma regs restr)
     (λregs.sigma_regs prog sigma regs restr)
     (λregs.ertl_eval_move regs pm)
     (λregs.ertl_eval_move regs pm).
#prog #sigma #restr * #mv_dst #arg_dst #pm whd in match ertl_eval_move; 
normalize nodelta @mfr_bind1 [@(sigma_beval prog sigma)
| cases arg_dst normalize nodelta 
  [2: #b change with (return sigma_beval prog sigma (BVByte b)) in ⊢ (???????%?);
      @mfr_return1]
  * #r normalize nodelta [@ps_reg_retrieve_ok| @hw_reg_retrieve_ok]
| #bv cases mv_dst #r normalize nodelta [@ps_reg_store_ok | @hw_reg_store_ok]
]
qed.

lemma ps_arg_retrieve_ok : ∀prog : ertl_program.
∀sigma : sigma_map prog. ∀a,restr.
preserving1 ?? res_preserve1 …
    (λregs.sigma_regs prog sigma regs restr)
    (sigma_beval prog sigma)
    (λregs.ps_arg_retrieve regs a)
    (λregs.ps_arg_retrieve regs a).
#prog #sigma #a #restr whd in match ps_arg_retrieve; normalize nodelta cases a -a
normalize nodelta [#r | #b ] #regs 
[ @ps_reg_retrieve_ok
| change with (return sigma_beval prog sigma (BVByte b)) in ⊢ (???????%?);
  @mfr_return1
]
qed.

lemma pop_ok :
∀prog : ertl_program.
∀good : (∀fn.good_state_transformation prog fn).
∀restr.
preserving1 ?? res_preserve1 ????
   (λst.sigma_state prog good st restr)
   (λx.let 〈bv,st〉 ≝ x in 
      〈let sigma ≝ get_sigma_from_good_state … good in
       sigma_beval prog sigma bv,
       sigma_state prog good st restr〉)
   (pop ERTL_semantics)
   (pop ERTLptr_semantics).
#prog #good #restr whd in match pop; normalize nodelta #st @mfr_bind1
[@(λx.let 〈bv,is〉 ≝ x in
      let sigma ≝ get_sigma_from_good_state … good in
     〈sigma_beval prog sigma bv,
      sigma_is prog sigma is 〉)
| whd in match is_pop; normalize nodelta whd in match sigma_state; normalize nodelta
  cases(istack ? st) normalize nodelta
  [@res_preserve_error1
  |2,3: #bv1 [2: #bv2] * #bv3 #is1 whd in ⊢ (??%% → ?); #EQ destruct
        % [2,4: % [1,3: %|*: %] |*:]
  ]
| * #bv #is * #bv1 #st whd in ⊢ (??%% → ?); #EQ destruct % [2: % [%] %|]
]
qed.

lemma push_ok : 
∀prog : ertl_program.
∀good : (∀fn.good_state_transformation prog fn).
∀restr.
preserving21 ?? res_preserve1 …
     (λst.sigma_state prog good st restr)
     (let sigma ≝ get_sigma_from_good_state … good in sigma_beval prog sigma)
     (λst.sigma_state prog good st restr)
     (push ERTL_semantics)
     (push ERTLptr_semantics).
#prog #good #restr whd in match push; normalize nodelta #st #bv @mfr_bind1
[ @(let sigma ≝ get_sigma_from_good_state … good in sigma_is ? sigma)
| whd in match is_push; normalize nodelta whd in match sigma_state; normalize nodelta
 cases (istack ? st) [2,3: #bv [2: #bv']]  whd in match sigma_is in ⊢ (???????%?);
 normalize nodelta [@res_preserve_error1] @mfr_return_eq1 %
| #is @mfr_return_eq1 %
]
qed.

lemma be_opaccs_ok : 
∀prog : ertl_program. ∀sigma : sigma_map prog.
∀ op.
preserving21 ?? res_preserve1 ??????
    (sigma_beval prog sigma)
    (sigma_beval prog sigma)
    (λx.let 〈bv1,bv2〉 ≝ x in
           〈sigma_beval prog sigma bv1,
            sigma_beval prog sigma bv2〉)
    (be_opaccs op)
    (be_opaccs op).
#prog #sigma #op #bv #bv1
whd in match be_opaccs; normalize nodelta @mfr_bind1
[ @(λx.x)
| cases bv
  [ | | #ptr1 #ptr2 #p | #by | #p | #ptr #p | #pc1 #p1]
  whd in match Byte_of_val; normalize nodelta
  try @res_preserve_error1 [ #x whd in ⊢ (???% → ?); #EQ destruct %{x} % //]
  whd in match sigma_beval; normalize nodelta cases (sigma_pc_opt ? ? ?)
  normalize nodelta [2: #pc] @res_preserve_error1
| #by @mfr_bind1
  [ @(λx.x)
  | cases bv1
    [ | | #ptr1 #ptr2 #p | #by | #p | #ptr #p | #pc1 #p1]
    whd in match Byte_of_val; normalize nodelta
    try @res_preserve_error1 [ #x whd in ⊢ (???% → ?); #EQ destruct %{x} % //]
    whd in match sigma_beval; normalize nodelta cases (sigma_pc_opt ? ? ?)
    normalize nodelta [2: #pc] @res_preserve_error1
 | #by1 * #bv2 #bv3 cases(opaccs eval op by by1) #by' #by1' normalize nodelta
   whd in ⊢ (??%% → ?); #EQ destruct % [2: % [%] % |]
qed.

lemma be_op1_ok : ∀prog : ertl_program. ∀sigma : sigma_map prog.
∀ op.
preserving1 ?? res_preserve1 …
     (sigma_beval prog sigma)
     (sigma_beval prog sigma)
     (be_op1 op)
     (be_op1 op).
#prog #sigma #o #bv whd in match be_op1; normalize nodelta @mfr_bind1
[ @(λx.x)
| cases bv 
  [ | | #ptr1 #ptr2 #p | #by | #p | #ptr #p | #pc1 #p1]
  whd in match Byte_of_val; whd in match sigma_beval; normalize nodelta
  try @res_preserve_error1 [ @mfr_return_eq1 %]
  cases(sigma_pc_opt prog sigma pc1) [2: #pc2] normalize nodelta
  @res_preserve_error1
| #by @mfr_return_eq1 %
]
qed.

lemma res_preserve_error11 : ∀X,Y,F,e,n. (∃e'.n = Error … e') → 
res_preserve1 X Y F n (Error … e).
#X #Y #F #e #n * #e' #n_spec >n_spec @res_preserve_error1
qed. 


lemma be_op2_ok : ∀prog : ertl_program. ∀sigma : sigma_map prog.
∀ b,op.
preserving21 ?? res_preserve1 …
     (sigma_beval prog sigma)
     (sigma_beval prog sigma)
     (λx.let 〈bv,b〉≝ x in 〈sigma_beval prog sigma bv,b〉)
     (be_op2 b op)
     (be_op2 b op).
#prog #sigma #b #op #bv #bv1 whd in match be_op2; normalize nodelta
cases bv
[ | | #ptr1 #ptr2 #p | #by | #p | #ptr #p | #pc1 #p1]
normalize nodelta [@res_preserve_error1] whd in match sigma_beval;
normalize nodelta
cases bv1
[1,2,8,9,15,16,22,23,29,30,36,37:
|3,10,17,24,31,38: #ptr1' #ptr2' #p' 
|4,11,18,25,32,39: #by' 
|5,12,19,26,33,40: #p' 
|6,13,20,27,34,41: #ptr' #p' 
|7,14,21,28,35,42: #pc1' #p1'
]
normalize nodelta try @res_preserve_error1
[4,5,8,13,16,20,21,22,23,24,25,26 : @res_preserve_error11 % 
   [2,4,6,8,10,12,14,16,18,20,22,24: cases(sigma_pc_opt ???) try % #pc2 %
   |*:]
|*: cases op normalize nodelta
    try @res_preserve_error1 try( @mfr_return_eq1 %) 
    [1,2,12,13,16,17,18: @if_elim #_ try @res_preserve_error1 
                         try( @mfr_return_eq1 %) 
                         [ @if_elim #_ @mfr_return_eq1 %
                         | cases(ptype ptr) normalize nodelta 
                           [2: @res_preserve_error1] @mfr_bind1
                           [ @(λx.x)
                           | whd in match Bit_of_val; normalize nodelta
                             cases b [#bo|| #bo #ptr'' #p'' #bit_v]
                             normalize nodelta [2,3: @res_preserve_error1]
                             @mfr_return_eq1 %
                           | #bi cases(op2 ?????) #by #bi1 normalize nodelta
                             @mfr_return_eq1 %
                           ]
                         | cases(ptype ptr) normalize nodelta @res_preserve_error1
                         ]
    |3,4,5,6,7,8: @mfr_bind1
        [1,4,7,10,13,16: @(λx.x)
        |2,5,8,11,14,17: whd in match Bit_of_val; normalize nodelta
                         cases b [1,4,7,10,13,16: #bo|
                                 |2,5,8,11,14,17:
                                 |3,6,9,12,15,18: #bo #ptr'' #p'' #bit_v
                                 ] normalize nodelta try @res_preserve_error1
                                 @mfr_return_eq1 %
       |3,6,9,12,15,18: #bi cases(op2 ?????) #by #bi1 normalize nodelta
                        @mfr_return_eq1 %
       ]
    |*: whd in match be_add_sub_byte; normalize nodelta
        [1,2,3: cases(ptype ptr) normalize nodelta [2,4,6: @res_preserve_error1]
                cases p * [2,4,6: #p_no] #prf normalize nodelta
                [@res_preserve_error1
                |2,3: cases b [1,4: #bo|2,5: |3,6:  #bo #ptr'' #p'' #bit_v]
                      normalize nodelta [1,2,3,4: @res_preserve_error1]
                      @if_elim #_ [2,4: @res_preserve_error1]
                      @If_elim #INUTILE [2,4: @res_preserve_error1]
                      @pair_elim #a1 #a2 #_ normalize nodelta
                      @mfr_return_eq1 %
                |*: @mfr_bind1
                  [1,4,7: @(λx.x)
                  |2,5,8: whd in match Bit_of_val; normalize nodelta
                          [@mfr_return_eq1 %] cases b
                          [1,4: #bo|2,5: |3,6:  #bo #ptr'' #p'' #bit_v]
                          normalize nodelta [3,4,5,6: @res_preserve_error1]
                          @mfr_return_eq1 %
                  |3,6,9: * normalize nodelta [1,3,5: @res_preserve_error1]
                          cases(op2 ?????) #a1 #a2 normalize nodelta
                          @mfr_return_eq1 %
                  ]
               ]
         |*: cases(ptype ptr') normalize nodelta [2,4: @res_preserve_error1]
             cases p' * [2,4: #part_no] #prf normalize nodelta 
             [ @res_preserve_error1
             | cases b [#bo|| #bo #ptr'' #p'' #bit_v]
               normalize nodelta [1,2: @res_preserve_error1] @if_elim #_
               [2: @res_preserve_error1] @If_elim #INUTILE [2: @res_preserve_error1]
               @pair_elim #a1 #a2 #_ normalize nodelta @mfr_return_eq1 %
             |*: @mfr_bind1
                [1,4: @(λx.x)
                |2,5: whd in match Bit_of_val; normalize nodelta [ @mfr_return_eq1 %]
                      cases b [#bo|| #bo #ptr'' #p'' #bit_v] normalize nodelta
                      [2,3: @res_preserve_error1] @mfr_return_eq1 %
                |3,6: * normalize nodelta [1,3: @res_preserve_error1]   
                      cases(op2 ?????) #a1 #a2 normalize nodelta
                      @mfr_return_eq1 %
                ]
              ]
          ]
      ]
]
qed.

lemma pointer_of_address_ok : ∀prog : ertl_program. ∀sigma : sigma_map prog.
preserving1 … res_preserve1 …
     (λx.let 〈bv1,bv2〉 ≝ x in〈sigma_beval prog sigma bv1,
           sigma_beval prog sigma bv2〉)
     (λx.x)
     pointer_of_address pointer_of_address.
#prog #sigma * #bv1 #bv2 whd in match pointer_of_address;
whd in match pointer_of_bevals; normalize nodelta
cases bv1 normalize nodelta
[ | | #ptr1 #ptr2 #p | #by | #p | #ptr #p | #pc1 #p1]
try @res_preserve_error1
[ cases bv2 [ | | #ptr1' #ptr2' #p' | #by' | #p' | #ptr' #p' | #pc1' #p1']
  normalize nodelta 
  [1,2,3,4,5: @res_preserve_error1 
  | @if_elim #_ [ @mfr_return_eq1 % | @res_preserve_error1]
  ]
] whd in match sigma_beval; normalize nodelta cases(sigma_pc_opt ???)
  [2,4: #pc4] normalize nodelta @res_preserve_error1
qed.

lemma beloadv_ok : ∀prog : ertl_program. ∀sigma : sigma_map prog.
∀ptr.
preserving1 … opt_preserve1 …
     (sigma_mem prog sigma)
     (sigma_beval prog sigma)
     (λm.beloadv m ptr)
     (λm.beloadv m ptr).
#prog #sigma #ptr #mem whd in match beloadv; whd in match do_if_in_bounds; 
normalize nodelta @if_elim [2: #_ @opt_preserve_none1]
whd in match sigma_mem in ⊢ (% → ?); normalize nodelta #Hzlb
@if_elim [2: #_ @opt_preserve_none1] whd in match sigma_mem in ⊢ (% → ?);
normalize nodelta @If_elim [2: >Hzlb * #H @⊥ @H %] #_ @andb_elim @if_elim 
[2: #_ *] #Hzleb #Hzlb' >Hzlb normalize nodelta >Hzlb' normalize nodelta
@mfr_return_eq1 whd in match sigma_mem; normalize nodelta >Hzlb
@If_elim [2: * #H @⊥ @H %] * >Hzleb >Hzlb' @If_elim [2: * #H @⊥ @H %]
* %
qed.

lemma bestorev_ok : ∀prog : ertl_program.∀sigma : sigma_map prog.
∀ptr.
preserving21 … opt_preserve1 …
    (sigma_mem prog sigma)
    (sigma_beval prog sigma)
    (sigma_mem prog sigma)
    (λm.bestorev m ptr)
    (λm.bestorev m ptr).
#prog #sigma #ptr #mem #bv whd in match bestorev; whd in match do_if_in_bounds;
normalize nodelta @if_elim [2: #_ @opt_preserve_none1]
whd in match sigma_mem in ⊢ (% → ?); normalize nodelta #Hzlb
@if_elim [2: #_ @opt_preserve_none1] @andb_elim @if_elim [2: #_ *]
whd in match sigma_mem in ⊢ (% → % → ?); normalize nodelta >Hzlb
@If_elim [2: * #H @⊥ @H %] * #Hzleb #Hzlb' normalize nodelta >Hzleb
>Hzlb' normalize nodelta @mfr_return_eq1 whd in ⊢ (???%); @eq_f @mem_ext_eq
[ #bl normalize nodelta % [%]
  [ whd in match sigma_mem; normalize nodelta >Hzlb @If_elim [2: * #H @⊥ @H %] *
    whd in match update_block; normalize nodelta @if_elim
    [ @eq_block_elim [2: #_ *] #EQbl * >EQbl >Hzlb @If_elim [2: * #H @⊥ @H %]
      * whd in match low_bound; normalize nodelta @if_elim [ #_ %]
      @eq_block_elim #_ * %
    | @eq_block_elim [#_ *] * #Hbl * @If_elim 
      [ #Hzlb'' >Hzlb'' @If_elim [2: * #H @⊥ @H %] * whd in match low_bound; 
        normalize nodelta @if_elim [2: #_ %] @eq_block_elim [2: #_ *] #H @⊥ @Hbl 
        assumption
      | #Hzlb'' >Hzlb'' @If_elim [*] #_ %
      ]
   ]
 | whd in match update_block; whd in match sigma_mem; normalize nodelta
   @if_elim @eq_block_elim [2,3: #_ * |4: *] #Hbl #_ @If_elim
   [3,4: >Hbl >Hzlb * [2: #H @⊥ @H %] @If_elim [2: * #H @⊥ @H %] *
        whd in match high_bound; normalize nodelta @if_elim [#_ %]
        @eq_block_elim [ #_ *] * #H @⊥ @H %
   | #Hzlb'' >Hzlb'' @If_elim [2: * #H @⊥ @H %] * whd in match high_bound;
     normalize nodelta @if_elim [2: #_ %] @eq_block_elim [2: #_ *]
     #H @⊥ @Hbl assumption
  | #Hzlb'' >Hzlb'' @If_elim [*] #_ %
  ]
 | #z whd in match update_block; whd in match sigma_mem; normalize nodelta
   @if_elim @eq_block_elim [2,3: #_ * |4: *] #Hbl #_
   [ @If_elim #Hzlb'' >Hzlb'' [2: @If_elim * #_ %] @If_elim @andb_elim
     @if_elim [2: #_ *] #Hzleb' #Hzlb'''
     [ @If_elim [2: * #H @⊥ @H %] * whd in match low_bound; normalize nodelta
       @If_elim @andb_elim @if_elim [2: #_ *] @if_elim
       [1,3,5: @eq_block_elim [2,4,6: #_ *] #H @⊥ @Hbl assumption] #_ >Hzleb' *
       whd in match high_bound; normalize nodelta @if_elim
       [1,3: @eq_block_elim [2,4: #_ *] #H @⊥ @Hbl assumption] #_ >Hzlb''' 
       [ * %] * #H @⊥ @H %
     | @If_elim * [2: #H @⊥ @H %] whd in match low_bound; normalize nodelta
       @if_elim [@eq_block_elim [2: #_ *] #H @⊥ @Hbl assumption] #_
       >Hzleb' whd in match high_bound; normalize nodelta @if_elim
       [@eq_block_elim [2: #_ *] #H @⊥ @Hbl assumption] #_ >Hzlb'''
       @If_elim [2: #_ %] *
     | @If_elim [2: * #H @⊥ @H %] whd in match low_bound; normalize nodelta @if_elim
       [@eq_block_elim [2: #_ *] #H @⊥ @Hbl assumption] #_ #_ 
       whd in match low_bound in Hzleb'; normalize nodelta in Hzleb';
       whd in match high_bound; normalize nodelta @if_elim
       [@eq_block_elim [2: #_ *] #H @⊥ @Hbl assumption] #_ @If_elim [2: #_ %]
       @andb_elim @if_elim [2: #_ *] #H >H in Hzleb'; *
     ]
   | whd in ⊢ (??%?); @if_elim @eqZb_elim [2,3: #_ * |4: *] #Hz * 
       [ >Hzlb @If_elim [2: * #H @⊥ @H %] * @If_elim @andb_elim @if_elim
          [2: #_ *] #Hzleb' #Hzlb'' >Hbl >Hzlb @If_elim [2,4,6: * #H @⊥ @H %] #_
          whd in match low_bound; normalize nodelta @eq_block_elim
          [2,4,6: * #H @⊥ @H %] #_ normalize nodelta whd in match high_bound;
          normalize nodelta @eq_block_elim [2,4,6: * #H @⊥ @H %]
          #_ normalize nodelta 
          [1,2: >Hzleb' >Hzlb'' @If_elim [2,3: * #H @⊥ @H %]
                #_ [2: %] whd in ⊢ (???(???%)); @if_elim [2: #_ %] 
                @eqZb_elim [2: #_ *] #H @⊥ @Hz assumption
          | @If_elim [2: #_ %] @andb_elim @if_elim [2: #_ *] #H >H in Hzleb'; *
          ]
       | >Hbl >Hzlb @If_elim [2: * #H @⊥ @H %] * whd in match low_bound;
         normalize nodelta @eq_block_elim [2: * #H @⊥ @H %] #_ normalize nodelta
         whd in match high_bound; normalize nodelta @eq_block_elim [2: * #H @⊥ @H %]
         normalize nodelta >Hz >Hzleb >Hzlb' @If_elim [2: * #H @⊥ @H %] #_ #_
         whd in ⊢ (???(???%)); @eqZb_elim [2: * #H @⊥ @H %] #_ %
       ]
    ]
 ]
| %
]
qed.

lemma match_reg_elim : ∀ A : Type[0]. ∀ P : A → Prop. ∀ r : region.
∀f : (r = XData) → A. ∀g : (r = Code) → A. (∀ prf : r = XData.P (f prf)) → 
(∀ prf : r = Code.P (g prf)) → 
P ((match r return λx.(r = x → ?) with
    [XData ⇒ f | Code ⇒ g])(refl ? r)).
#A #P * #f #g #H1 #H2 normalize nodelta [ @H1 | @H2]
qed. 


lemma sp_ok : ∀prog : ertl_program.
∀good : (∀fn.good_state_transformation prog fn).
∀restr.
   preserving1 … res_preserve1 …
      (λst.sigma_state prog good st restr)
      (λx.x)
      (sp ERTL_semantics)
      (sp ERTLptr_semantics).
#prog #good #restr #st whd in match sp; normalize nodelta 
whd in match (load_sp ??); whd in match (load_sp ??); whd in match sigma_state;
normalize nodelta whd in match sigma_regs; normalize nodelta 
cases(regs ? st) #psd_r #hw_r normalize nodelta 
inversion(pointer_of_address ?) normalize nodelta [2: #e #_ @res_preserve_error1]
#pt #EQ lapply(jmeq_to_eq ??? EQ) -EQ whd in match hwreg_retrieve; normalize nodelta
whd in match sigma_hw_register_env; normalize nodelta 
change with (sigma_beval ? (get_sigma_from_good_state … good) BVundef) in ⊢ (??(?(???(?????%)(?????%)))? → ?);
>lookup_map >lookup_map 
cases(lookup beval 6 (bitvector_of_register RegisterSPL) (reg_env hw_r) BVundef)
[ | | #ptr1 #ptr2 #p | #by | #p | #ptr #p | #pc1 #p1]
whd in match pointer_of_address; whd in match pointer_of_bevals; normalize nodelta
[1,2,3,4,5: #ABS destruct 
| cases(lookup beval 6 (bitvector_of_register RegisterSPH) (reg_env hw_r) BVundef)
  [ | | #ptr1' #ptr2' #p' | #by' | #p' | #ptr' #p' | #pc1' #p1']
  whd in match sigma_beval; normalize nodelta
  [1,2,3,4,5: #ABS destruct
  | @if_elim [2: #_ #ABS destruct] #H whd in ⊢ (??%? → ?); #EQ destruct 
    normalize nodelta @match_reg_elim #INUTILE 
    [ @mfr_return_eq1 % | @res_preserve_error1 ] 
  | cases (sigma_pc_opt ? ? ?) normalize nodelta [2: #x] #EQ destruct
  ]
| whd in match sigma_beval; normalize nodelta cases(sigma_pc_opt ? ? ?)
 normalize nodelta [2: #x] #EQ destruct
]
qed.

lemma set_sp_ok :  ∀prog : ertl_program.
∀good : (∀fn.good_state_transformation prog fn).
∀restr.∀ptr,st.
set_sp ? ptr (sigma_state prog good st restr) =
sigma_state prog good (set_sp ? ptr st) restr.
#prog #good #restr #ptr #st whd in match set_sp; whd in match sigma_state;
normalize nodelta @eq_f2 [2: %] whd in match (save_sp ???); 
whd in match (save_sp ???); whd in match sigma_regs; normalize nodelta
cases(regs ? st) #psd_env #hw_regs normalize nodelta @eq_f
whd in match hwreg_store_sp; normalize nodelta whd in match sigma_hw_register_env;
normalize nodelta whd in match hwreg_store; normalize nodelta @eq_f2 [2: %]
>insert_map @eq_f >insert_map %
qed.

lemma eval_seq_no_pc_no_call_ok :
∀prog : ertl_program.
let trans_prog ≝ (ertl_to_ertlptr prog) in
∀good : (∀fn.good_state_transformation prog fn).
∀stack_size. ∀id. ∀fn : (joint_closed_internal_function ??) .∀seq.
   preserving1 ?? res_preserve1 ????
      (λst.sigma_state prog good st (added_registers … fn (f_regs … (good fn))))
      (λst.sigma_state prog good st (added_registers … fn (f_regs … (good fn))))
      (eval_seq_no_pc ERTL_semantics
             (globals (mk_prog_params ERTL_semantics prog stack_size))
             (ev_genv (mk_prog_params ERTL_semantics prog stack_size)) id fn seq)
      (eval_seq_no_pc ERTLptr_semantics
  (globals (mk_prog_params ERTLptr_semantics trans_prog stack_size))
  (ev_genv (mk_prog_params ERTLptr_semantics trans_prog stack_size)) id (translate_internal … fn) (seq_embed … seq)).
#prog #good #stack_size #f #fn *
whd in match eval_seq_no_pc; normalize nodelta
[ #c #st @mfr_return1
| #c #st @mfr_return1 
| #pm #st whd in match pair_reg_move; normalize nodelta 
  @mfr_bind1 
  [ 2: change with (ertl_eval_move ??) in ⊢ (???????%%); @ertl_eval_move_ok
  | | #regs  @mfr_return_eq1 % 
  ]
| #r #st @mfr_bind1
  [2:  @pop_ok |
  | * #bv #st whd in match acca_store; normalize nodelta @mfr_bind1
    [2: @ps_reg_store_ok |
    | #regs  @mfr_return_eq1 % 
    ]
  ]
| #r #st @mfr_bind1
  [2: whd in match acca_arg_retrieve; normalize nodelta @ps_arg_retrieve_ok |
  | #bv @push_ok
  ] 
| #i 
  #i_spec
  change with ((dpl_reg ERTL) → ?) 
  #dpl
  change with ((dph_reg ERTL) → ?) 
  #dph #st @mfr_bind1
  [ @(λst.sigma_state prog good st (added_registers … fn (f_regs … (good fn))))
  | whd in match dpl_store; normalize nodelta @mfr_bind1
    [2: @opt_safe_elim #bl #EQbl
       @opt_safe_elim #bl'
       >(find_symbol_transf …
          (λvars.transf_fundef … (λfn.(translate_internal … fn))) prog i) in ⊢ (%→?);
       >EQbl #EQ destruct whd in match sigma_state; normalize nodelta        
       change with (sigma_beval prog (get_sigma_from_good_state … good) (BVptr …)) 
                                               in ⊢ (???????(?????%?)?); 
       @ps_reg_store_ok |
    | #regs  @mfr_return_eq1 %
    ]
  | #st1 @opt_safe_elim #bl #EQbl @opt_safe_elim #bl'   
    >(find_symbol_transf …
          (λvars.transf_fundef … (λfn.(translate_internal … fn))) prog i) in ⊢ (%→?);
    >EQbl #EQ destruct whd in match dph_store; normalize nodelta @mfr_bind1
    [2: whd in match sigma_state; normalize nodelta        
       change with (sigma_beval prog (get_sigma_from_good_state … good) (BVptr …)) 
                                               in ⊢ (???????(?????%?)?); 
      @ps_reg_store_ok |
    | #regs  @mfr_return_eq1 % 
    ]
  ] 
| #op #a #b #arg1 #arg2 #st @mfr_bind1
  [2: whd in match acca_arg_retrieve; whd in match sigma_state; normalize nodelta
     @ps_arg_retrieve_ok |
  | #bv1 @mfr_bind1
   [2: whd in match accb_arg_retrieve; whd in match sigma_state; normalize nodelta
      @ps_arg_retrieve_ok |
   | #bv2 @mfr_bind1
     [2: @be_opaccs_ok |
     | * #bv3 #bv4 normalize nodelta @mfr_bind1
       [ @(λst.sigma_state prog good st (added_registers … fn (f_regs … (good fn))))
       | whd in match acca_store; normalize nodelta @mfr_bind1
         [2: @ps_reg_store_ok |
         | #regs  @mfr_return_eq1 % 
         ]
       | #st1 whd in match accb_store; normalize nodelta @mfr_bind1
         [2: whd in match sigma_state; normalize nodelta
            @ps_reg_store_ok |
         | #regs  @mfr_return_eq1 %
         ]         
       ]
     ]
   ]
  ]  
| #op #r1 #r2 #st @mfr_bind1
  [ @(sigma_beval prog (get_sigma_from_good_state … good))
  | whd in match acca_retrieve; normalize nodelta @ps_reg_retrieve_ok
  | #bv1 @mfr_bind1
    [ @(sigma_beval prog (get_sigma_from_good_state … good))
    | @be_op1_ok
    | #bv2 whd in match acca_store; normalize nodelta @mfr_bind1
      [2: whd in match sigma_state; normalize nodelta @ps_reg_store_ok |
      | #regs  @mfr_return_eq1 %
      ]
    ]
  ]
| #op2 #r1 #r2 #arg #st @mfr_bind1
  [2: whd in match acca_arg_retrieve; normalize nodelta @ps_arg_retrieve_ok |
  | #bv @mfr_bind1
    [2: whd in match snd_arg_retrieve; normalize nodelta @ps_arg_retrieve_ok |
    | #bv1 @mfr_bind1
      [2: @be_op2_ok |
      | * #bv2 #b @mfr_bind1
        [ @(λst.sigma_state prog good st (added_registers … fn (f_regs … (good fn))))
        | whd in match acca_store; normalize nodelta @mfr_bind1
          [2: whd in match sigma_state; normalize nodelta @ps_reg_store_ok |
          | #regs  @mfr_return_eq1 %
          ]
        | #st1 @mfr_return_eq1 %
        ]
      ]
    ]
  ]
| #st  @mfr_return_eq1 %
| #st  @mfr_return_eq1 % 
| #r1 #dpl #dph #st @mfr_bind1
  [2: whd in match dph_arg_retrieve; normalize nodelta @ps_arg_retrieve_ok |
  | #bv @mfr_bind1
    [2: whd in match dpl_arg_retrieve; normalize nodelta @ps_arg_retrieve_ok |
    | #bv1 @mfr_bind1
      [ @(λx.x) 
      | @(pointer_of_address_ok ? ? 〈bv1,bv〉)
      | #ptr @mfr_bind1
        [2: @opt_to_res_preserve1 @beloadv_ok |
        | #bv2 whd in match acca_store; normalize nodelta @mfr_bind1
          [2: whd in match sigma_state; normalize nodelta @ps_reg_store_ok |
          | #regs  @mfr_return_eq1 %
          ]
        ]  
      ]
    ]
  ]  
| #dpl #dph #r #st @mfr_bind1
  [2: whd in match dph_arg_retrieve; normalize nodelta @ps_arg_retrieve_ok |
  | #bv @mfr_bind1
    [2: whd in match dpl_arg_retrieve; normalize nodelta @ps_arg_retrieve_ok |
    | #bv1 @mfr_bind1
      [ @(λx.x)
      |  @(pointer_of_address_ok ? ? 〈bv1,bv〉)
      | #ptr @mfr_bind1
        [2: whd in match acca_arg_retrieve; normalize nodelta @ps_arg_retrieve_ok |
        | #bv2 @mfr_bind1
          [2: @opt_to_res_preserve1 @bestorev_ok |
          | #m @mfr_return_eq1 %
          ]
        ]
      ]
    ]
  ]
| #ext #st whd in ⊢ (???????%%); whd in match (stack_sizes ????); cases (stack_size f)
  normalize nodelta
  [ @res_preserve_error1
  | #n cases ext normalize nodelta
    [1,2: @mfr_bind1
      [1,4: @(λx.x)
      |2,5: @sp_ok
      |3,6: #ptr @mfr_return_eq1 >set_sp_ok %
      ]
    | #r whd in match ps_reg_store_status; normalize nodelta @mfr_bind1
      [2: whd in match sigma_state; normalize nodelta
          change with (sigma_beval ? (get_sigma_from_good_state … good) (BVByte ?)) 
               in ⊢ (???????(??%?)?);
          @ps_reg_store_ok
      |
      | #regs @mfr_return_eq1 %
      ]
    ]
  ]      
]
qed.

lemma partial_inj_sigma : ∀ prog : ertl_program.
∀good : (∀fn.good_state_transformation prog fn). 
let sigma ≝ (get_sigma_from_good_state … good) in
∀fn,lbl1,lbl2. sigma fn lbl1 ≠ None ? → sigma fn lbl1 = sigma fn lbl2 → lbl1 = lbl2.
#prog #good #fn #lbl1 #lbl2 inversion(get_sigma_from_good_state … lbl1) 
[#_ * #H @⊥ @H %] #lbl1' whd in match get_sigma_from_good_state; normalize nodelta
#H @('bind_inversion H) -H * #lbl1'' #stmt1 #H1 whd in ⊢ (??%? → ?); #EQ destruct
#_ #H lapply(sym_eq ??? H) -H #H @('bind_inversion H) -H * #lbl2' #stmt2 #H2
whd in ⊢ (??%? → ?); #EQ destruct lapply(find_predicate ?????? H1)
lapply(find_predicate ?????? H2) cases(f_lbls ????) normalize nodelta [*] 
* normalize nodelta 
[@eq_identifier_elim #EQ1 * @eq_identifier_elim #EQ2 * >EQ1 >EQ2 % ] 
#lb #tl @eq_identifier_elim #EQ1 * @eq_identifier_elim #EQ2 * >EQ1 >EQ2 %
qed.

lemma pc_of_label_eq :
  ∀p,p'.let pars ≝ make_sem_graph_params p p' in 
  ∀globals,ge,bl,i_fn,lbl.
  fetch_internal_function ? ge bl = return i_fn →
  pc_of_label pars globals ge bl lbl =
    OK ? (pc_of_point ERTL_semantics bl lbl). 
#p #p' #globals #ge #bl #i_fn #lbl #EQf 
whd in match pc_of_label;
normalize nodelta >EQf >m_return_bind %
qed.

lemma pop_ra_ok : 
∀prog : ertl_program.
∀good : (∀fn.good_state_transformation prog fn). 
∀restr.
preserving1 … res_preserve1 …
     (λst.sigma_state prog good st restr)
     (λx.let 〈st,pc〉 ≝ x in 
         let sigma ≝ (get_sigma_from_good_state … good) in
       〈sigma_state prog good st restr,
        sigma_stored_pc ? sigma pc〉)
     (pop_ra ERTL_semantics)
     (pop_ra ERTLptr_semantics).
#prog #good #restr #st whd in match pop_ra; normalize nodelta @mfr_bind1
[ | @pop_ok ] * #bv #st1 @mfr_bind1 [ | @pop_ok] * #bv1 #st2 @mfr_bind1
[ @(sigma_stored_pc ? (get_sigma_from_good_state … good)) 
| whd in match pc_of_bevals; normalize nodelta 
  cases bv [ | | #ptr1 #ptr2 #p | #by | #p | #ptr #p | #pc #p]
  whd in match sigma_beval; normalize nodelta try @res_preserve_error1
  inversion(sigma_pc_opt ? ? ?) normalize nodelta [ #_ @res_preserve_error1]
  #sigma_pc #sigma_pc_spec normalize nodelta cases bv1
  [ | | #ptr1 #ptr2 #p | #by | #p | #ptr #p | #pc1 #p1]
  normalize nodelta try @res_preserve_error1 
  inversion(sigma_pc_opt ? ? ?) normalize nodelta [#_ @res_preserve_error1]
  #sigma_pc1 #sigma_pc1_spec @if_elim [2: #_ @res_preserve_error1]
  @andb_elim @if_elim [2: #_ *] @andb_elim @if_elim [2: #_ *]
  #_ #H >H @eq_program_counter_elim [2: #_ *]
  #EQspc * @eq_program_counter_elim 
  [#_ normalize nodelta @mfr_return_eq1 whd in match sigma_stored_pc; normalize nodelta
   >sigma_pc1_spec %] * #H1 @⊥ @H1 >EQspc in sigma_pc_spec; <sigma_pc1_spec
   whd in match sigma_pc_opt; normalize nodelta @if_elim
  [ #H2 #EQ lapply(sym_eq ??? EQ) -EQ @if_elim [#_  whd in ⊢ (??%% → ?); #EQ destruct %]
    #H3 #H @('bind_inversion H) -H #x #_ #H @('bind_inversion H) -H #y #_
    cases sigma_pc1 in H2; #bl_pc1 #z #H2 whd in ⊢ (??%? → ?); #EQ destruct >H2 in H3; *
  | #H2 @if_elim 
    [ #H3 #H @('bind_inversion H) -H #x1 #_ #H @('bind_inversion H) -H #lbl1 #_
      cases pc in H2; #bl #z #H2 whd in match pc_of_point; normalize nodelta whd in ⊢ (??%? → ?);
      #EQ destruct >H3 in H2; *
    | #H3 lapply sigma_pc1_spec; whd in match sigma_pc_opt; normalize nodelta @if_elim
     [#H >H in H3; *] #_ #EQ >EQ @('bind_inversion EQ) -EQ #x #x_spec 
     lapply(res_eq_from_opt ??? x_spec) -x_spec #x_spec #H @('bind_inversion H) * #lbl 
     #lbl_spec whd in match pc_of_point; normalize nodelta cases sigma_pc1 #bl1 #lbl1
     whd in match (offset_of_point ??); whd in ⊢ (??%? → ?); #EQ destruct cases pc #bl2 #p2 
     #H @('bind_inversion H) -H #x1 #x1_spec lapply(res_eq_from_opt ??? x1_spec) -x1_spec #x1_spec
     #H @('bind_inversion H) -H * #lbl2 #lbl2_spec
     whd in match (offset_of_point ??); whd in ⊢ (??%? → ?); #EQ destruct
     <lbl_spec in lbl2_spec; #EQsig >x_spec in x1_spec; whd in ⊢ (??%% → ?); #EQ destruct
     lapply(partial_inj_sigma … EQsig)
     [>EQsig >lbl_spec % #ABS destruct] whd in match point_of_pc; normalize nodelta
     whd in match (point_of_offset ??); whd in match (point_of_offset ??);
     #EQ destruct cases pc1 #bl #p %
    ]
  ]
| #pc @mfr_return_eq1 %
]
qed. 

lemma pc_block_eq : ∀prog : ertl_program.
∀sigma : sigma_map prog.
∀pc,id,fn.
fetch_internal_function (joint_closed_internal_function ERTL
  (prog_var_names (joint_function ERTL) ℕ prog))
  (globalenv_noinit (joint_function ERTL) prog) (pc_block … pc) 
  = return 〈id,fn〉→ 
sigma fn (point_of_pc ERTL_semantics pc) ≠ None ? → 
 pc_block … pc = pc_block … (sigma_stored_pc prog sigma pc).
#prog #sigma * #bl #pos #id #fn #EQfn #EQlbl whd in match sigma_stored_pc; 
normalize nodelta whd in match sigma_pc_opt; normalize nodelta @if_elim [ #_ %]
#_ >EQfn >m_return_bind >(opt_to_opt_safe … EQlbl) >m_return_bind %
qed.

inductive ex_Type1 (A:Type[1]) (P:A → Prop) : Prop ≝
    ex1_intro: ∀ x:A. P x →  ex_Type1 A P.
(*interpretation "exists in Type[1]" 'exists x = (ex_Type1 ? x).*)

include "joint/semantics_blocks.ma".

lemma fetch_internal_function_no_zero :
∀F,V,i,p,bl.
  block_id (pi1 … bl) = 0 →
  fetch_internal_function ?
  
  (globalenv (λvars.fundef (F vars)) V i p) bl = 
  Error ? [MSG BadFunction].
#F #V #i #p #bl #EQbl whd in match fetch_internal_function; 
normalize nodelta >fetch_function_no_zero [2: assumption] %
qed.

lemma fetch_statement_no_zero : 
∀pars,prog,stack_size,pc.
block_id(pi1 … (pc_block pc)) = 0 →
fetch_statement pars (prog_var_names … prog) 
(ev_genv (mk_prog_params pars prog stack_size)) pc = 
Error ? [MSG BadFunction].
#pars #vars #ge #pc #EQpc whd in match fetch_statement; normalize nodelta
>fetch_internal_function_no_zero [2: assumption] %
qed.

lemma foo :
 ∀P1_unser,P2_unser: unserialized_params.
 ∀P1_sem_unser,P2_sem_unser.
 let P1_sem ≝ make_sem_graph_params P1_unser P1_sem_unser in
 let P2_sem ≝ make_sem_graph_params P2_unser P2_sem_unser in
 ∀init,translate_step.
 ∀translate_fin_step.
 ∀closed_graph_translate.
 let translate_internal :
  ∀globals.
   joint_closed_internal_function P1_sem globals →
   joint_closed_internal_function P2_sem globals
  ≝
  λglobals,fun.
   «b_graph_translate (mk_graph_params P1_sem) (mk_graph_params P2_sem) globals
    (init globals)
    (translate_step globals)
    (translate_fin_step globals)
    (pi1 … fun), closed_graph_translate globals fun» in
 ∀prog.
 let trans_prog ≝ transform_program ??? prog (λvarnames. transf_fundef ?? (translate_internal varnames)) in
 ∀stack_size.
 ∀sigma_state_pc.
 (∀s. pc_block (pc … (sigma_state_pc s)) = pc_block … (pc … s)) →
 ∀st : state_pc P2_sem. 
 ∀st' : state_pc P1_sem. 
 ∀f.
 ∀fn: joint_closed_internal_function P1_sem (globals (mk_prog_params P1_sem prog stack_size)).
 luniverse_ok … fn → 
 ∀stmt,nxt.
 (∀pre_Instrs',last_Instrs',dst.
   ∃st''.∃st'''.∃st''''.
    repeat_eval_seq_no_pc (mk_prog_params P2_sem trans_prog stack_size)
     f (translate_internal ? fn) (map_eval ?? pre_Instrs' dst) st = return st''' ∧
    eval_seq_no_pc ? (prog_var_names … trans_prog) (ev_genv … (mk_prog_params P2_sem trans_prog stack_size))
                      f (translate_internal … fn) (last_Instrs' dst) st''' = return st'''' ∧
    st'' = (mk_state_pc (mk_prog_params P2_sem trans_prog stack_size)
     st'''' (pc_of_point P2_sem (pc_block (pc … (sigma_state_pc st))) dst) (last_pop … st)) ∧ 
    st' = sigma_state_pc st'' ∧
    let P2_prog_params ≝ mk_prog_params P2_sem trans_prog stack_size in
    let P2_globals ≝ globals P2_prog_params in 
     All
      (joint_seq … P2_globals)
      (no_cost_label … P2_globals)
      (map_eval (code_point P2_sem) (joint_seq … P2_globals) pre_Instrs' dst)) →
 fetch_statement … 
  (prog_var_names (joint_function P1_sem) ℕ prog)
  (ev_genv (mk_prog_params P1_sem prog stack_size)) 
  (pc … (sigma_state_pc st)) =
    return 〈f, fn,  sequential … (step_seq P1_sem … stmt) nxt〉 →
 eval_state …
 (prog_var_names (joint_function P1_sem) ℕ prog) 
 (ev_genv … (mk_prog_params P1_sem prog stack_size)) 
 (sigma_state_pc st) = return st' → 
 ∃st''. (*CSC: this needs to be linked back again st' = sigma_state_pc ? good st'' ∧*)
 ∃taf : trace_any_any_free (joint_abstract_status (mk_prog_params P2_sem trans_prog stack_size)) st st''.
 True (* the length of taf is the same of the length of ??? *).
#P1_unser #P2_unser #P1_sem_unser #P2_sem_unser
letin P1_sem ≝ (make_sem_graph_params P1_unser P1_sem_unser)
letin P2_sem ≝ (make_sem_graph_params P2_unser P2_sem_unser)
#init #translate_step #translate_fin_step #closed_graph_translate.
letin translate_internal ≝
 (λglobals,fun.
   «b_graph_translate (mk_graph_params P1_sem) (mk_graph_params P2_sem) globals
    (init globals)
    (translate_step globals)
    (translate_fin_step globals)
    (pi1 … fun), closed_graph_translate globals fun»)
#prog
letin trans_prog ≝ (transform_program ??? prog (λvarnames. transf_fundef ?? (translate_internal varnames)))
#stack_size #sigma_state_pc #sigma_state_pc_ok #st #st' #f #fn #fn_universe_ok #stmt #nxt #Hpass 
#EQfetch lapply(fetch_statement_inv … EQfetch) * #EQfn #EQstmt
cases
 (b_graph_translate_ok … (init …) (translate_step …) (translate_fin_step …) … fn_universe_ok)
#_ * #MK_fresh_labels * #MK_fresh_registers **** #_ #_ #_ #_ (*CSC: useful things thrown out here *)
#MULTI_FETCH_OK cases (MULTI_FETCH_OK … EQstmt)
#list_b_last * #fresh_registers ** #EQlist_b_last #EQfresh_registers
normalize nodelta * #Instrs * #fresh_registers_spec whd in ⊢ (% → ?);
@pair_elim #pre_Instrs #last_Instrs #EQInstrs * #dst * #Multi_fetch #STEP_in_code
#EQeval
cut((list
   (code_point P2_sem
    →joint_seq P2_sem (prog_var_names (joint_function P1_sem) ℕ prog)))) [ cases daemon (*Paolo should fix the lemma*)]
#pre_Instrs'
cut((code_point P2_sem
   →joint_seq P2_sem (prog_var_names (joint_function P1_sem) ℕ prog))) [ cases daemon (*Paolo should fix the lemma*)]
#last_Instrs'
cases (Hpass pre_Instrs' last_Instrs' dst (* MANY MORE HERE *))
#st'' * #st''' * #st'''' **** #REPEAT #EVAL_NO_PC_Last #EQst'' #EQst' #NO_COSTED
lapply(produce_trace_any_any_free … NO_COSTED … REPEAT)
[ cases daemon (* should be @Multi_fetch *)
| <sigma_state_pc_ok @(fetch_internal_function_transf … (λvars.translate_internal vars))
  assumption
| @dst
| @list_b_last (*wrong, should dst be destination or the last of list_b_last *)
] #TAAF
lapply
  (produce_step_trace (mk_prog_params P2_sem trans_prog stack_size)
    (mk_state_pc (mk_prog_params P2_sem trans_prog stack_size)
       st''' (pc_of_point P2_sem (pc_block (pc … st)) dst) (last_pop … st))
    f (translate_internal ? fn) (last_Instrs' dst) nxt st'''' … EVAL_NO_PC_Last)
[ cases daemon (* should be @STEP_In_code *)
| <sigma_state_pc_ok
  @(fetch_internal_function_transf … (λvars. translate_internal vars) … EQfn) ]
#LAST_STEP
cases daemon
qed.

lemma eval_seq_no_call_ok :
 ∀prog.
 let trans_prog ≝ ertl_to_ertlptr prog in
 ∀good : (∀fn.good_state_transformation prog fn).     
 ∀stack_sizes. 
 (*? →*) 
 ∀st : state_pc ERTLptr_semantics. 
 ∀st' : state_pc ERTL_semantics. 
 ∀f,fn,stmt,nxt.
   fetch_statement ERTL_semantics 
     (prog_var_names (joint_function ERTL_semantics) ℕ prog)
    (ev_genv (mk_prog_params ERTL_semantics prog stack_sizes)) 
    (pc … (sigma_state_pc ? good st)) =
      return 〈f, fn,  sequential … (step_seq ERTL … stmt) nxt〉 →
   eval_state ERTL_semantics
   (prog_var_names (joint_function ERTL_semantics) ℕ prog) 
   (ev_genv … (mk_prog_params ERTL_semantics prog stack_sizes)) 
   (sigma_state_pc ? good st) =
    return st' → 
 ∃st''. st' = sigma_state_pc ? good st'' ∧
 ∃taf : trace_any_any_free (ERTLptr_status trans_prog stack_sizes)
  st
  st''.
 bool_to_Prop (taaf_non_empty … taf).
#prog #good #stack_size #st #st' #f #fn #stmt #nxt #EQfetch #EQeval
cases (foo … translate_step translate_fin_step … EQfetch EQeval)
[2,3: cases daemon (* first one, take out init definition from ERTLtoERTLptr;
                      second one to be taken from somewhere *)
|4: #x cases daemon (* TO BE DONE, EASY *)
|5: cases daemon (* to be taken in input *) ]
[2: cases daemon
| #st'' * #taaf #_ %{st''}
  change with ERTL_uns in match (mk_unserialized_params ???????????????);
  change with ERTLptr_uns in match (mk_unserialized_params ???????????????);
  change with ERTL_semantics in match (make_sem_graph_params ??);
  change with ERTLptr_semantics in match (make_sem_graph_params ??);


#H1 #H2 #H3 *

 ∀P1_unser,P2_unser: unserialized_params.
 ∀P1_sem_unser,P2_sem_unser.
 ∀init,translate_step.
 ∀translate_fin_step.
 ∀closed_graph_translate.
 ∀prog.
 ∀stack_size.
 ∀sigma_state_pc.
 (∀s. pc_block (pc … (sigma_state_pc s)) = pc_block … (pc … s)) →
 ∀st : state_pc P2_sem. 
 ∀st' : state_pc P1_sem. 
 ∀f.
 ∀fn: joint_closed_internal_function P1_sem (globals (mk_prog_params P1_sem prog stack_size)).
 luniverse_ok … fn → 
 ∀stmt,nxt.
 (∀pre_Instrs',last_Instrs',dst.
   ∃st''.∃st'''.∃st''''.
    repeat_eval_seq_no_pc (mk_prog_params P2_sem trans_prog stack_size)
     f (translate_internal ? fn) (map_eval ?? pre_Instrs' dst) st = return st''' ∧
    eval_seq_no_pc ? (prog_var_names … trans_prog) (ev_genv … (mk_prog_params P2_sem trans_prog stack_size))
                      f (translate_internal … fn) (last_Instrs' dst) st''' = return st'''' ∧
    st'' = (mk_state_pc (mk_prog_params P2_sem trans_prog stack_size)
     st'''' (pc_of_point P2_sem (pc_block (pc … (sigma_state_pc st))) dst) (last_pop … st)) ∧ 
    st' = sigma_state_pc st'' ∧
    let P2_prog_params ≝ mk_prog_params P2_sem trans_prog stack_size in
    let P2_globals ≝ globals P2_prog_params in 
     All
      (joint_seq … P2_globals)
      (no_cost_label … P2_globals)
      (map_eval (code_point P2_sem) (joint_seq … P2_globals) pre_Instrs' dst)) →


 
whd in match sigma_state_pc in ⊢ (% → ?); normalize nodelta @if_elim
[ #_ >fetch_statement_no_zero [2,4: %] whd in ⊢ (???% → ?); #ABS destruct]
#EQbl inversion(fetch_internal_function ?? (pc_block (pc ? st))) normalize nodelta
[2: #err #_ >fetch_statement_no_zero [2,4: %] whd in ⊢ (???% → ?); #ABS destruct]
* #id1 #fn1 #EQfn normalize nodelta #EQfetch lapply(fetch_statement_inv … EQfetch)
* >EQfn #EQ destruct normalize nodelta #EQstmt
cases(multi_fetch_ok … (good fn) ?? EQstmt)
#list_b_last * #fresh_registers ** #EQlist_b_last #EQfresh_registers
normalize nodelta * #Instrs * #fresh_registers_spec whd in ⊢ (% → ?);
@pair_elim #pre_Instrs #last_Instrs #EQInstrs * #dst * #Multi_fetch #STEP_in_code
#EQeval
cut((list
   (code_point ERTLptr
    →joint_seq ERTLptr (prog_var_names (joint_function ERTL) ℕ prog)))) [ cases daemon (*Paolo should fix the lemma*)]
#pre_Instrs'
cut((code_point ERTLptr
   →joint_seq ERTLptr (prog_var_names (joint_function ERTL) ℕ prog))) [ cases daemon (*Paolo should fix the lemma*)]
#last_Instrs'
letin list_map ≝ cic:/matita/basics/lists/list/map.fix(0,3,1)
cut(∃st''.∃st'''.∃st''''.
    repeat_eval_seq_no_pc (mk_prog_params ERTLptr_semantics (ertl_to_ertlptr prog) stack_size)
     f (translate_internal ? fn) (map_eval ?? pre_Instrs' dst) st = return st''' ∧
    eval_seq_no_pc ? (prog_var_names … (ertl_to_ertlptr prog)) (ev_genv … (mk_prog_params ERTLptr_semantics (ertl_to_ertlptr prog) stack_size))
                      f (translate_internal … fn) (last_Instrs' dst) st''' = return st'''' ∧
    st'' = (mk_state_pc (mk_prog_params ERTLptr_semantics (ertl_to_ertlptr prog) stack_size)
     st'''' (pc_of_point ERTLptr_semantics (pc_block (pc … st)) dst) 
                                 (last_pop … st)) ∧ 
    st' = sigma_state_pc ? good st'')
     [ cases daemon (*to be generalized and TO be moved into an other lemma *)]
* #st'' * #st''' * #st'''' *** #REPEAT #EVAL_NO_PC_Last #EQst'' #EQst' %{st''} % [assumption]
lapply(produce_trace_any_any_free … REPEAT)
[ cases daemon (* Pass dependent *)
| cases daemon (* should be @Multi_fetch *)
| @(fetch_internal_function_transf … (λvars. translate_internal …) … EQfn)
| @dst
| @list_b_last (*wrong, should dst be destination or the last of list_b_last *)
] #TAAF
lapply(produce_step_trace (mk_prog_params ERTLptr_semantics (ertl_to_ertlptr prog) stack_size)
       (mk_state_pc (mk_prog_params ERTLptr_semantics (ertl_to_ertlptr prog) stack_size)
     st''' (pc_of_point ERTLptr_semantics (pc_block (pc … st)) dst) 
                                 (last_pop … st)) f (translate_internal ? fn) (last_Instrs' dst) nxt st'''' (fetch_internal_function_transf … (λvars. translate_internal …) … EQfn) 
       ? EVAL_NO_PC_Last) [cases daemon (* should be @STEP_in_code *)]
#LAST_STEP
letin taaf_last ≝ (taaf_step ???? TAAF LAST_STEP)

        cut(dst = (point_of_pc
                           (mk_prog_params ERTLptr_semantics (ertl_to_ertlptr prog) stack_size)
                           (pc … st))) [cases daemon (*TODO it is true since pre_Instr is empty *)]
                #EQ <EQ whd in match step_in_code; normalize nodelta
                cases STEP_in_code #x * #x_spec #x_spec' %{x} % 
                [ >x_spec in ⊢ (??%?); @eq_f @eq_f2 [2: %] cases daemon (*should be % *) |
                 [<EVAL_NO_PC_Last in ⊢ (???%); @eq_f %



whd in match eval_state; normalize nodelta >EQfetch >m_return_bind
lapply EQfetch -EQfetch whd in match sigma_state_pc in ⊢ (% → ?); 
normalize nodelta @if_elim
[ #_ >fetch_statement_no_zero [2,4: %] whd in ⊢ (???% → ?); #ABS destruct]
#EQbl inversion(fetch_internal_function ?? (pc_block (pc ? st))) normalize nodelta
[2: #err #_ >fetch_statement_no_zero [2,4: %] whd in ⊢ (???% → ?); #ABS destruct]
* #id1 #fn1 #EQfn normalize nodelta #EQfetch lapply(fetch_statement_inv … EQfetch)
* >EQfn #EQ destruct normalize nodelta #EQstmt
whd in match sigma_state_pc in ⊢ (% → ?); normalize nodelta @if_elim
[#H >H in EQbl; *] #_ >EQfn normalize nodelta whd in match eval_statement_no_pc; 
normalize nodelta #H @('bind_inversion H) -H #ex_st_nopc
#H lapply (err_eq_from_io ????? H) -H #EQnopc whd in match eval_statement_advance;
normalize nodelta whd in match set_no_pc; normalize nodelta
whd in ⊢ (??%% → ?); #EQ destruct cases(eval_seq_no_pc_no_call_ok … EQnopc)
#sigma_st_nopc * #EQsigma_st_nopc #sem_rel %
[ % [@sigma_st_nopc
    | @(succ_pc ERTL_semantics (pc ERTLptr_semantics st) nxt)
    | @(last_pop … st)
    ]
] % whd in match sigma_state_pc;



qed.

lemma ertl_to_ertlptr_ok:
∀prog.
let trans_prog ≝ ertl_to_ertlptr prog in
∀good : (∀fn.good_state_transformation prog fn).     
∀stack_sizes. 
   ex_Type1 … (λR.
   status_simulation
    (ERTL_status prog stack_sizes) (ERTLptr_status trans_prog stack_sizes) R).
#prog #good #stack_size % [@ERTLptrStatusSimulation assumption]
whd in match status_simulation; normalize nodelta
whd in match ERTL_status; whd in match ERTLptr_status; normalize nodelta
whd in ⊢ (% → % → % → % → ?); #st1 #st1' #st2
change with
  (eval_state ERTL_semantics (prog_var_names ???) ?? = ? → ?)  
#EQeval @('bind_inversion EQeval)
** #id #fn #stmt #H lapply (err_eq_from_io ????? H) -H #EQfetch
#_  whd in match ERTLptrStatusSimulation; normalize nodelta #EQst2 destruct
cases stmt in EQfetch; -stmt
[ * [ #called_id #args #dest| #reg #lbl | #seq] #nxt | #fin_step | *] #EQfetch
change with (joint_classify ??) in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ? ]);
[ (*CALL*) cases daemon
| (*COND*) cases daemon
| (*seq*) whd in match joint_classify; normalize nodelta >EQfetch >m_return_bind
          normalize nodelta cases (eval_seq_no_call_ok ?????????  EQfetch EQeval)
  #st3 * #EQ destruct *  #taf #tafne %{st3} %{taf} >tafne normalize nodelta
  % [% //] whd >as_label_ok [2:assumption] %


lapply(produce_trace_any_any_free 
      (mk_prog_params ERTLptr_semantics (ertl_to_ertlptr prog) stack_size)
      st2 id (translate_internal ? fn)) #PRODUCE_TAAF
cases stmt in EQfetch; -stmt
[ * [ #called_id #args #dest| #reg #lbl | #seq] #nxt | #fin_step | *] #EQfetch
normalize nodelta

      
lapply EQfetch -EQfetch whd in match sigma_state_pc in ⊢ (% → ?);
normalize nodelta @if_elim 
[ #_ >fetch_statement_no_zero [2,4: %] whd in ⊢ (???% → ?); #ABS destruct]
#EQbl inversion(fetch_internal_function ?? (pc_block (pc ? st2))) normalize nodelta
[2: #err #_ >fetch_statement_no_zero [2,4: %] whd in ⊢ (???% → ?); #ABS destruct]
* #id1 #fn1 #EQfn normalize nodelta #EQfetch lapply(fetch_statement_inv … EQfetch)
* >EQfn #EQ destruct normalize nodelta #EQstmt      
      
      ? ? ?? ? ???) 



cases stmt in EQfetch; -stmt
[ * [ #called_id #args #dest| #reg #lbl | #seq] #nxt | #fin_step | *] #EQstmt
change with (joint_classify ??) in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ? ]);
whd in match joint_classify; normalize nodelta >EQstmt >m_return_bind
normalize nodelta lapply(fetch_statement_inv … EQstmt) * #fn_spec
#stmt_spec
cases(multi_fetch_ok … (good fn) ?? stmt_spec) #f_labs * #f_regs ** #f_labs_spec
#f_regs_spec normalize nodelta * #list_instr * #b_new_f_regs
whd in ⊢ (% → ?); normalize nodelta 
[1,2,3: @pair_elim #list_instr1 #rgt #last_ne_spec * #last_lab * 
       #list_instr1_spec #last_step 
       lapply(fetch_internal_function_transf … 
                                       (λvars. translate_internal …) … fn_spec)
       change with ((fetch_internal_function 
                    (joint_closed_internal_function ? (prog_var_names … (ertl_to_ertlptr prog)))
                    (globalenv_noinit … (ertl_to_ertlptr prog)) ?) = ?  → ?)
       #EQtrans_fn
       check prog_params
       lapply(produce_trace_any_any_free 
       (mk_prog_params ERTLptr_semantics (ertl_to_ertlptr prog) stack_size)
        ? id (translate_internal ? fn) ? ? ?? EQtrans_fn ???) [2: @EQtrans_fn





lapply EQstmt whd in match sigma_state_pc in ⊢ (% → ?);
normalize nodelta @if_elim 
[1,3: #_ >fetch_statement_no_zero [2,4: %] whd in ⊢ (???% → ?); #ABS destruct]
#EQbl inversion(fetch_internal_function ?? (pc_block (pc ? st2))) normalize nodelta
[2,4: #err #_ >fetch_statement_no_zero [2,4: %] whd in ⊢ (???% → ?); #ABS destruct]
* #id1 #fn1 #EQfn1 normalize nodelta #EQstmt1 lapply(fetch_statement_inv … EQstmt1)
* >EQfn1 #EQ destruct normalize nodelta #EQstmtat




[ (*CALL*)
  cases daemon (*TODO*) 
| whd in match joint_classify; normalize nodelta
 >EQfetch in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ? ]);
  normalize nodelta
 #n_cost 
 cases (eval_cond_ok … EQfetch EQeval n_cost)
 #st3 * #EQ destruct * #taf #tafne %{st3} %{taf} 
 % [ % [2: %] >tafne normalize nodelta @I] whd >as_label_ok %
| whd in match joint_classify; normalize nodelta
 >EQfetch in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ? ]);
  normalize nodelta
  cases (eval_seq_no_call_ok ?????????  EQfetch EQeval)
  #st3 * #EQ destruct *  #taf #tafne %{st3} %{taf} >tafne normalize nodelta
  % [% //] whd >as_label_ok [2:assumption] %
| (*FIN*) 
  cases fin_step in EQfetch;
  [ (*GOTO*) #lbl #EQfetch  whd in match joint_classify; normalize nodelta
  >EQfetch in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ? ]); normalize nodelta
    cases (eval_goto_ok … EQfetch EQeval)
    #st3 * #EQ destruct * #taf #tarne %{st3} %{taf} >tarne normalize nodelta
    % [% //] whd >as_label_ok [2:assumption] %
  | (*RETURN*) #EQfetch
     whd in match joint_classify; normalize nodelta
    >EQfetch in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ? ]); normalize nodelta
    cases (eval_return_ok … EQfetch EQeval) #is_ret
    * #st3 * #EQ destruct * #after_ret * #taf ** #taf_prf #EQeval' #ret_prf
    % [2: % [2: % [2: %{(taa_base …)} %{taf}] |*: ] |*:]
    % [2: whd >as_label_ok %] % [2: assumption] % [2: %] % [2: assumption]
    % assumption
  | (*TAILCALL*) #fl #called #args #EQfetch 
    cases (eval_tailcall_ok … EQfetch EQeval) #st3 * #EQ destruct * #is_tailcall 
    * #is_tailcall' *  #eq_call #EQeval' >is_tailcall normalize nodelta
    #prf  %{«?, is_tailcall'»} %{eq_call}
    % [2: % [2: %{(taa_base …)} %{(taa_base …)}  % [ %{EQeval'} % |] | ] | ]
    whd >as_label_ok %
  ]
]
qed.

@('bind_inversion EQfetch) * #id1 #fn1 #EQfn #H @('bind_inversion H) -H
#stmt1 #H lapply(opt_eq_from_res ???? H) -H #EQstmt whd in ⊢ (??%% → ?);
#EQ destruct

(*
lemma push_ra_ok : ∀prog : ertl_program.
∀good :  (∀fn.good_state_transformation prog fn).∀restr.
preserving21 … res_preserve1 …
     (sigma_state_pc prog good)
     (\l
     (λst.sigma_state prog good st restr)
     (push_ra ERTL_semantics)
     (push_ra ERTLptr_semantics).
#prog #good #restr #st #pc whd in match push_ra; normalize nodelta @mfr_bind1
[2: whd in match sigma_stored_pc; normalize nodelta 

[2: #x


lemma ertlptr_save_frame_ok : ∀prog : ertl_program.
∀good : (∀fn.good_state_transformation prog fn). 
∀id.
    preserving1 … res_preserve1 …
        (sigma_state_pc prog good)
        (λst. match get_internal_function_from_ident 
                  ERTL_semantics (prog_var_names … prog)
                  (globalenv_noinit … prog) id with
             [None ⇒ dummy_state
             |Some fd ⇒ 
                sigma_state prog good st (added_registers … fd (f_regs … (good fd)))
             ])
        (ertl_save_frame ID it id)
        (ertlptr_save_frame ID it id).
#prog #good #id #st whd in match ertl_save_frame; whd in match ertlptr_save_frame;
normalize nodelta @mfr_bind1
[2: whd in match push_ra; normalize nodelta @mfr_bind1
xxxxxxxxxxxx



lemma fetch_statement_commute :
∀prog : ertl_program.
let trans_prog ≝ (ertl_to_ertlptr prog) in
∀sigma : sigma_map trans_prog.
∀stack_sizes,id,fn,stmt,pc.
fetch_statement ERTL_semantics 
(globals (mk_prog_params ERTL_semantics prog stack_sizes))
(ev_genv (mk_prog_params ERTL_semantics prog stack_sizes))
pc = return 〈id,fn,stmt〉 → 
match stmt with 
[ sequential seq nxt ⇒
    match seq with
    [ CALL ids args dest ⇒
        match ids with
        [ inl i ⇒ 
          fetch_statement ERTLptr_semantics 
          (globals (mk_prog_params ERTLptr_semantics trans_prog stack_sizes))
          (ev_genv (mk_prog_params ERTLptr_semantics trans_prog stack_sizes))
          pc = 
          return 〈id,
          translate_internal … fn,
          sequential ?? (CALL ERTLptr ? (inl ?? i) args dest) nxt〉
        | inr p ⇒ ?(*
          ∃reg,lbl.
          fetch_statement ERTLptr_semantics 
          (globals (mk_prog_params ERTLptr_semantics trans_prog stack_sizes))
          (ev_genv (mk_prog_params ERTLptr_semantics trans_prog stack_sizes))
           pc = return 〈id,translate_internal … fn,sequential ?? (extension_seq ERTLptr ? (LOW_ADDRESS reg lbl)) nxt〉
           ∧ ∃ nxt'.
           ! pc' ← get_pc_from_label ? ? (ev_genv (mk_prog_params ERTLptr_semantics trans_prog stack_sizes))
                 id nxt;
           fetch_statement ERTLptr_semantics 
          (globals (mk_prog_params ERTLptr_semantics trans_prog stack_sizes))
          (ev_genv (mk_prog_params ERTLptr_semantics trans_prog stack_sizes))
           pc' = return 〈id,translate_internal … fn,sequential ?? (step_seq ERTLptr ? (PUSH … (Reg … reg))) nxt'〉
           ∧ ∃ nxt''.
           ! pc' ← get_pc_from_label ? ? (ev_genv (mk_prog_params ERTLptr_semantics trans_prog stack_sizes))
                 id nxt';
           fetch_statement ERTLptr_semantics 
          (globals (mk_prog_params ERTLptr_semantics trans_prog stack_sizes))
          (ev_genv (mk_prog_params ERTLptr_semantics trans_prog stack_sizes))
           pc' = return 〈id,translate_internal … fn,sequential ?? (extension_seq ERTLptr ? (HIGH_ADDRESS reg lbl)) nxt''〉
           ∧ ∃ nxt'''.
           ! pc' ← get_pc_from_label ? ? (ev_genv (mk_prog_params ERTLptr_semantics trans_prog stack_sizes))
                 id nxt'';
           fetch_statement ERTLptr_semantics 
          (globals (mk_prog_params ERTLptr_semantics trans_prog stack_sizes))
          (ev_genv (mk_prog_params ERTLptr_semantics trans_prog stack_sizes))
           pc' = return 〈id,translate_internal … fn,sequential ?? (step_seq ERTLptr ? (PUSH … (Reg … reg))) nxt'''〉
           ∧ ∃ nxt''''.
           ! pc' ← get_pc_from_label ? ? (ev_genv (mk_prog_params ERTLptr_semantics trans_prog stack_sizes))
                 id nxt''';
           fetch_statement ERTLptr_semantics 
          (globals (mk_prog_params ERTLptr_semantics trans_prog stack_sizes))
          (ev_genv (mk_prog_params ERTLptr_semantics trans_prog stack_sizes))
           pc' = return 〈id,translate_internal … fn,sequential ?? (CALL ERTLptr ? (inr ?? p) args dest) nxt''''〉
           ∧ sigma (translate_internal … fn) nxt''' =  return point_of_pc ERTL_semantics pc *)
        ]
    | COND r lbl ⇒ 
          fetch_statement ERTLptr_semantics 
          (globals (mk_prog_params ERTLptr_semantics trans_prog stack_sizes))
          (ev_genv (mk_prog_params ERTLptr_semantics trans_prog stack_sizes))
          pc = 
          return 〈id,
          translate_internal … fn,
          sequential ?? (COND ERTLptr ? r lbl) nxt〉
    | step_seq s ⇒ 
          fetch_statement ERTLptr_semantics 
          (globals (mk_prog_params ERTLptr_semantics trans_prog stack_sizes))
          (ev_genv (mk_prog_params ERTLptr_semantics trans_prog stack_sizes))
          pc = 
          return 〈id,
          translate_internal … fn,
          sequential ?? (step_seq ERTLptr … (translate_step_seq ? s)) nxt〉
    ]                   
| final fin ⇒ 
     fetch_statement ERTLptr_semantics 
     (globals (mk_prog_params ERTLptr_semantics trans_prog stack_sizes))
     (ev_genv (mk_prog_params ERTLptr_semantics trans_prog stack_sizes))
     pc = return 〈id,(translate_internal … fn),final … (joint_fin_step_id fin)〉
| FCOND abs _ _ _ ⇒ Ⓧabs
].
cases daemon
qed.

lemma eval_seq_no_call_ok :
 ∀prog.
 let trans_prog ≝ ertl_to_ertlptr prog in
 ∀sigma : sigma_map trans_prog.∀stack_sizes.
 (*? →*) 
 ∀st,st',f,fn,stmt,nxt.
   fetch_statement ERTL_semantics 
     (prog_var_names (joint_function ERTL_semantics) ℕ prog)
    (ev_genv (mk_prog_params ERTL_semantics prog stack_sizes)) 
    (pc … (sigma_state_pc ? sigma st)) =
      return 〈f, fn,  sequential … (step_seq ERTL … stmt) nxt〉 →
   eval_state ERTL_semantics
   (prog_var_names (joint_function ERTL_semantics) ℕ prog) 
   (ev_genv … (mk_prog_params ERTL_semantics prog stack_sizes)) 
   (sigma_state_pc ? sigma st) =
    return st' → 
 ∃st''. st' = sigma_state_pc ? sigma st'' ∧
 ∃taf : trace_any_any_free (ERTLptr_status trans_prog stack_sizes)
  st
  st''.
 bool_to_Prop (taaf_non_empty … taf).
#prog #sigma #stack_size #st1 #st2 #f #fn #stmt #nxt #EQf whd in match eval_state;
normalize nodelta >EQf >m_return_bind whd in match eval_statement_advance; 
whd in match eval_statement_no_pc; normalize nodelta
 #H @('bind_inversion H) -H #st_no_pc #EQ lapply(err_eq_from_io ????? EQ) -EQ 
#EQeval whd in ⊢ (??%% → ?); #EQ destruct lapply EQf 
whd in match sigma_state_pc in ⊢ (% → ?); normalize nodelta @if_elim
[ #EQbl
| #pc_st1_spec inversion(fetch_internal_function ???) [2: #e #_]
]
[1,2: whd in match dummy_state_pc; whd in match null_pc; 
  whd in match fetch_statement; normalize nodelta whd in match fetch_internal_function;
  normalize nodelta lapply(fetch_function_no_zero ??????) 
  [2,9: @( «mk_block Code OZ,refl region Code»)
    |1,8: % |3,10: @prog |7,14: #EQ >EQ |*:]  whd in ⊢ (??%% → ?); #EQ destruct]
* #f1 #fn1 #EQ lapply(jmeq_to_eq ??? EQ) -EQ #fn1_spec normalize nodelta
whd in match fetch_statement; normalize nodelta >fn1_spec
>m_return_bind #H @('bind_inversion H) -H #stmt1 #EQ 
lapply(opt_eq_from_res ???? EQ) -EQ #stmt1_spec whd in ⊢ (??%% → ?); #EQ destruct
lapply EQeval -EQeval whd in match sigma_state_pc in ⊢ (% → ?);
normalize nodelta @if_elim [#H >H in pc_st1_spec; *] #_ >fn1_spec
normalize nodelta #EQeval cases(eval_seq_no_pc_no_call_ok ???????? EQeval)
#st_no_pc' * #EQeval' #EQst_no_pc' 
whd in match set_no_pc; normalize nodelta 
% [ % [@st_no_pc'|@(succ_pc ERTL_semantics (pc ERTL_semantics (sigma_state_pc prog sigma st1))
   nxt)| @(last_pop ? st1)]]
% [ whd in match sigma_state_pc; normalize nodelta
    @if_elim [#H >H in pc_st1_spec; *] #_ >fn1_spec normalize nodelta 
    @if_elim [#H >H in pc_st1_spec; *] #_ >fn1_spec normalize nodelta
    >EQst_no_pc' %]
%{(taaf_step … (taa_base …) …)} 
[3: //] lapply(fetch_statement_commute ? sigma ????? EQf) normalize nodelta
whd in match sigma_state_pc; normalize nodelta
@if_elim [1,3:#H >H in pc_st1_spec; *] #_ >fn1_spec normalize nodelta
#EQf1
[ whd in match as_classifier; normalize nodelta whd in match (as_classify ??);
  >EQf1 normalize nodelta %
| whd in match (as_execute ???); whd in match eval_state; normalize nodelta
  >EQf1 >m_return_bind whd in match eval_statement_no_pc; normalize nodelta
  >EQeval' >m_return_bind %
]
qed.


lemma eval_goto_ok :
 ∀prog : ertl_program.
 let trans_prog ≝ ertl_to_ertlptr prog in
 ∀stack_sizes.
 ∀sigma : sigma_map trans_prog.
 ∀st,st',f,fn,nxt.
   fetch_statement ERTL_semantics …
    (globalenv_noinit ? prog) (pc … (sigma_state_pc ? sigma st)) =
      return 〈f, fn,  final … (GOTO ERTL … nxt)〉 → 
   eval_state ERTL_semantics
   (prog_var_names (joint_function ERTL_semantics) ℕ prog) 
   (ev_genv … (mk_prog_params ERTL_semantics prog stack_sizes)) 
   (sigma_state_pc ? sigma st) =
    return st' → 
    ∃ st''. st' = sigma_state_pc ? sigma st'' ∧
 ∃taf : trace_any_any_free (ERTLptr_status trans_prog stack_sizes)
  st
  st''.
 bool_to_Prop (taaf_non_empty … taf).
#prog #stack_sizes #sigma #st #st' #f #fn #nxt
whd in match sigma_state_pc in ⊢ (% → ?); normalize nodelta
@if_elim 
[ #EQbl whd in match dummy_state_pc; whd in match null_pc;
  whd in match fetch_statement; whd in match fetch_internal_function;
  normalize nodelta lapply(fetch_function_no_zero ??????) 
  [2: @( «mk_block Code OZ,refl region Code»)
    | % | @prog |7: #EQ >EQ |*:]  whd in ⊢ (??%% → ?); #EQ destruct]
#Hbl inversion(fetch_internal_function ???)
[2: #e #_ normalize nodelta whd in match dummy_state_pc; whd in match null_pc;
   whd in match fetch_statement; whd in match fetch_internal_function;
  normalize nodelta lapply(fetch_function_no_zero ??????) 
  [2: @( «mk_block Code OZ,refl region Code»)
    | % | @prog |7: #EQ >EQ |*:]  whd in ⊢ (??%% → ?); #EQ destruct]
* #f1 #fn1 #EQ lapply(jmeq_to_eq ??? EQ) -EQ #fn1_spec normalize nodelta
#EQf lapply EQf whd in match fetch_statement; normalize nodelta >fn1_spec
>m_return_bind #H @('bind_inversion H) -H #stmt' #_ whd in ⊢ (??%% → ?);
#EQ destruct whd in match sigma_state_pc in ⊢ (% → ?); normalize nodelta
@if_elim [#H >H in Hbl; *] #_ >fn1_spec normalize nodelta whd in match eval_state;
normalize nodelta >EQf >m_return_bind whd in match eval_statement_advance; 
whd in match eval_statement_no_pc; normalize nodelta >m_return_bind
whd in match goto; normalize nodelta #H lapply (err_eq_from_io ????? H) -H
#H @('bind_inversion H) -H #pc' whd in match set_no_pc; normalize nodelta
>(pc_of_label_eq … fn1_spec) whd in ⊢ (???% → ?); #EQ whd in ⊢ (??%% → ?); #EQ1 
destruct lapply (fetch_statement_commute … sigma … stack_sizes … EQf)
normalize nodelta #EQf' % 
[ % [ @st 
    | @(mk_program_counter 
         (pc_block (pc ERTLptr_semantics st))
         (offset_of_point ERTL_semantics nxt)) 
    | @(last_pop … st)
    ]
] % 
[ whd in match sigma_state_pc; normalize nodelta @if_elim [#H >H in Hbl; *]
  >fn1_spec normalize nodelta #_ % ] 
%{(taaf_step … (taa_base …) …)}
[ whd in match as_classifier; normalize nodelta whd in match (as_classify ??);
  >EQf' normalize nodelta %
| whd in match (as_execute ???); whd in match eval_state; normalize nodelta
  >EQf' >m_return_bind whd in match eval_statement_no_pc; 
  whd in match eval_statement_advance; normalize nodelta >m_return_bind
  whd in match goto; normalize nodelta whd in match pc_of_label; normalize nodelta
  lapply(fetch_internal_function_transf ??????? fn1_spec)
  [ #vars @translate_internal |] #EQ >EQ >m_return_bind %
| %
]
qed.
*)


                        

 
lemma eval_return_ok :
∀prog : ertl_program.
let trans_prog ≝ ertl_to_ertlptr prog in
∀stack_sizes.
∀sigma : sigma_map trans_prog.
∀st,st',f,fn.
 fetch_statement ERTL_semantics …
  (globalenv_noinit ? prog) (pc … (sigma_state_pc ? sigma st)) =
    return 〈f, fn,  final … (RETURN ERTL … )〉 → 
 eval_state ERTL_semantics
   (prog_var_names (joint_function ERTL_semantics) ℕ prog) 
   (ev_genv … (mk_prog_params ERTL_semantics prog stack_sizes)) 
   (sigma_state_pc ? sigma st) =
  return st' →
joint_classify (mk_prog_params ERTLptr_semantics trans_prog stack_sizes)
  st = Some ? cl_return ∧
∃ st''. st' = sigma_state_pc ? sigma st'' ∧
∃st2_after_ret.
∃taf : trace_any_any_free (ERTLptr_status trans_prog stack_sizes)
st2_after_ret
st''.
(if taaf_non_empty … taf then
  ¬as_costed (ERTLptr_status trans_prog stack_sizes)
    st2_after_ret
 else True) ∧
eval_state … (ev_genv …  (mk_prog_params ERTLptr_semantics trans_prog stack_sizes)) st =
return st2_after_ret ∧ 
ret_rel ?? (ERTLptrStatusSimulation prog stack_sizes sigma) st' st2_after_ret.
#prog #stack_size #sigma #st #st' #f #fn
whd in match sigma_state_pc in ⊢ (% → ?); normalize nodelta
@if_elim 
[ #EQbl whd in match dummy_state_pc; whd in match null_pc;
  whd in match fetch_statement; whd in match fetch_internal_function;
  normalize nodelta >(fetch_function_no_zero ??????) [2: %] 
  whd in ⊢ (??%% → ?); #EQ destruct ]
#Hbl inversion(fetch_internal_function ???)
[2: #e #_ normalize nodelta whd in match dummy_state_pc; whd in match null_pc;
   whd in match fetch_statement; whd in match fetch_internal_function;
  normalize nodelta lapply(fetch_function_no_zero ??????) 
  [2: @( «mk_block Code OZ,refl region Code»)
    | % | @prog |7: #EQ >EQ |*:]  whd in ⊢ (??%% → ?); #EQ destruct]
* #f1 #fn1 #EQ lapply(jmeq_to_eq ??? EQ) -EQ #fn1_spec normalize nodelta
#EQf lapply EQf whd in match fetch_statement; normalize nodelta >fn1_spec
>m_return_bind #H @('bind_inversion H) -H #stmt' #_ whd in ⊢ (??%% → ?);
#EQ destruct whd in match sigma_state_pc in ⊢ (% → ?); normalize nodelta
@if_elim [#H >H in Hbl; *] #_ >fn1_spec normalize nodelta
whd in match eval_state; normalize nodelta >EQf >m_return_bind
whd in match eval_statement_no_pc; whd in match eval_statement_advance;
normalize nodelta >m_return_bind
#H lapply (err_eq_from_io ????? H) -H #H @('bind_inversion H) -H 
* #st1 #pc1 #EQpop whd in match next_of_call_pc; normalize nodelta
>m_bind_bind #H @('bind_inversion H) -H ** #f1 #fn1 * normalize nodelta
[ * [ #c_id #args #dest | #r #lbl | #seq ] #nxt | #fin | * ]
#EQf1 normalize nodelta [2,3,4: whd in ⊢ (??%% → ?); #EQ destruct]
>m_return_bind whd in ⊢ (??%% → ?); #EQ destruct
lapply (fetch_statement_commute prog sigma stack_size … EQf)
normalize nodelta #EQf'
% [ whd in match joint_classify; normalize nodelta >EQf' >m_return_bind %]
change with (pop_ra ?? = ?) in EQpop; whd in match set_no_pc in EQpop;
normalize nodelta in EQpop;
cases(pop_ra_ok ? sigma  stack_size fn ?? EQpop) * #st3 #pc3 * #st3_spec
normalize nodelta #EQ destruct whd in match set_last_pop; whd in match succ_pc; 
normalize nodelta whd in match (point_of_succ ???);
 % [ % [ @st3 | @(pc_of_point ERTL_semantics (pc_block … pc3) nxt) | @pc3] ] 
 % [  @('bind_inversion EQf1) * #f3 #fn3 whd in match sigma_stored_pc;
      normalize nodelta inversion(sigma_pc_opt ???) normalize nodelta
      [ #_ #H @('bind_inversion H) -H #x whd in match null_pc; normalize nodelta
        >fetch_function_no_zero [2: %] whd in ⊢ (???% → ?); #EQ destruct
      | #pc4 whd in match sigma_pc_opt; normalize nodelta @if_elim
        [ #bl3_spec @('bind_inversion EQf1) #x #H @('bind_inversion H) -H
          #x1 >fetch_function_no_minus_one [ whd in ⊢ (???% → ?); #EQ destruct] 
          lapply bl3_spec @eqZb_elim #EQ * whd in match sigma_stored_pc;
          normalize nodelta whd in match sigma_pc_opt; normalize nodelta
           >bl3_spec normalize nodelta assumption
        | #bl3_spec #H @('bind_inversion H) -H * #id4 #fn4 
          #H lapply(res_eq_from_opt ??? H) -H #fn4_spec
          #H @('bind_inversion H) -H #lbl4 #lbl4_spec whd in ⊢ (??%? → ?); #EQ
          destruct #fn3_spec #H @('bind_inversion H) -H #stmt1 #_ 
          whd in ⊢ (??%% → ?); #EQ destruct 
          >(fetch_internal_function_transf … fn3_spec) in fn4_spec; 
          whd in ⊢ (??%% → ?); #EQ destruct
        ]
      ]
      whd in match sigma_state_pc; normalize nodelta @if_elim
      [ >(pc_block_eq prog sigma ????) in bl3_spec; 
       [2: >lbl4_spec % #ABS destruct 
       |3: >(fetch_internal_function_transf … fn3_spec) % |*:]
       #bl3_spec whd in match pc_of_point; normalize nodelta #EQ >EQ in bl3_spec; *
      | #_ cases daemon
      ]
  ] cases daemon
qed.

(*
lemma ertl_allocate_local_ok : ∀ prog : ertl_program.
let trans_prog ≝ ertl_to_ertlptr prog in
∀sigma : sigma_map.
∀stack_size.
∀id,regs.
ertl_allocate_local id (sigma_regs ? sigma getLocalsFromId(
*)

lemma eval_tailcall_ok :
∀prog.
let trans_prog ≝ ertl_to_ertlptr prog in
∀stack_sizes.
∀sigma : sigma_map trans_prog.
∀st,st',f,fn,fl,called,args.
 fetch_statement ERTL_semantics …
  (globalenv_noinit ? prog) (pc … (sigma_state_pc ? sigma st)) =
    return 〈f, fn,  final … (TAILCALL ERTL … fl called args)〉 → 
 eval_state ERTL_semantics
   (prog_var_names (joint_function ERTL_semantics) ℕ prog) 
   (ev_genv … (mk_prog_params ERTL_semantics prog stack_sizes)) 
   (sigma_state_pc ? sigma st) =
  return st' →
  ∃ st''. st' = sigma_state_pc ? sigma st'' ∧
  ∃is_tailcall, is_tailcall'.
  joint_tailcall_ident (mk_prog_params ERTLptr_semantics trans_prog stack_sizes) «st, is_tailcall'» =
  joint_tailcall_ident (mk_prog_params ERTL_semantics prog stack_sizes) «(sigma_state_pc ? sigma st), is_tailcall» ∧
  eval_state … (ev_genv … (mk_prog_params ERTLptr_semantics trans_prog stack_sizes))
    st = return st''.
#prog #stack_size #sigma #st #st' #f #fn #fl #called #args
whd in match sigma_state_pc in ⊢ (% → ?); normalize nodelta
@if_elim 
[ #EQbl whd in match dummy_state_pc; whd in match null_pc;
  whd in match fetch_statement; whd in match fetch_internal_function;
  normalize nodelta >(fetch_function_no_zero ??????) [2: %] 
  whd in ⊢ (??%% → ?); #EQ destruct ]
#Hbl inversion(fetch_internal_function ???)
[2: #e #_ normalize nodelta whd in match dummy_state_pc; whd in match null_pc;
   whd in match fetch_statement; whd in match fetch_internal_function;
  normalize nodelta lapply(fetch_function_no_zero ??????) 
  [2: @( «mk_block Code OZ,refl region Code»)
    | % | @prog |7: #EQ >EQ |*:]  whd in ⊢ (??%% → ?); #EQ destruct]
* #f1 #fn1 #EQ lapply(jmeq_to_eq ??? EQ) -EQ #fn1_spec normalize nodelta
#EQf lapply EQf whd in match fetch_statement; normalize nodelta >fn1_spec
>m_return_bind #H @('bind_inversion H) -H #stmt' #_ whd in ⊢ (??%% → ?);
#EQ destruct  whd in match sigma_state_pc in ⊢ (% → ?); normalize nodelta
@if_elim [#H >H in Hbl; *] #_ >fn1_spec normalize nodelta
whd in match eval_state; normalize nodelta >EQf >m_return_bind
whd in match eval_statement_no_pc; whd in match eval_statement_advance;
normalize nodelta >m_return_bind whd in match eval_tailcall;
normalize nodelta #H @('bind_inversion H) -H #bl whd in match set_no_pc;
normalize nodelta #bl_spec #H @('bind_inversion H) -H * #id1 * [#int_f | #ext_f]  
#H lapply(err_eq_from_io ????? H) -H #id1_spec normalize nodelta 
[2: #H @('bind_inversion H) -H #st1 whd in match eval_external_call; normalize nodelta
    #H @('bind_inversion H) -H #l_val #_ #H @('bind_inversion H) -H #le #_
    #H @('bind_inversion H) -H #x whd in match do_io; normalize nodelta
    whd in ⊢ (???% → ?); #EQ destruct ]
#H lapply(err_eq_from_io ????? H) -H  #H @('bind_inversion H) -H #st1
whd in match eval_internal_call; normalize nodelta whd in match (stack_sizes ????);
#H @('bind_inversion H) -H #n #H lapply(opt_eq_from_res ???? H) -H #n_spec
whd in match(setup_call ???????); >m_return_bind
whd in ⊢ (??%% → ?); #EQ destruct whd in match sigma_state in ⊢ (% → ?); 
normalize  nodelta whd in ⊢ (??%% → ?); #EQ destruct
% [ % 
    [ % 
      [ @(st_frms ERTLptr_semantics st)
      | @(istack ERTLptr_semantics st)
      | @(carry ERTLptr_semantics st)
      | cases daemon
      | @(m ERTLptr_semantics st)
      ]
    | @(mk_program_counter bl
            (offset_of_point ERTL_semantics
              (joint_if_entry ERTL_semantics
                  (prog_var_names (joint_function ERTL_semantics) ℕ prog) int_f)))
    | @(last_pop ERTLptr_semantics st)
    ]
  ]
% [ whd in match sigma_state_pc; normalize nodelta @if_elim whd in match pc_of_point;
    normalize nodelta 
    [ #Hbl >fetch_function_no_minus_one in id1_spec; 
       [2: lapply Hbl @eqZb_elim -Hbl #Hbl * @Hbl] whd in ⊢ (???% → ?); 
       #EQ destruct(EQ)
    ] #_ whd in match fetch_internal_function; normalize nodelta >id1_spec 
      >m_return_bind normalize nodelta cases daemon (*TO BE COmpleted *)
  ] cases daemon (*TO BE COMPLETED*)
qed.
    
    
    
    
lemma as_label_ok : ∀ prog : ertl_program.
let trans_prog ≝ ertl_to_ertlptr prog in
∀ sigma : sigma_map trans_prog.
∀stack_sizes.
∀ st.
as_label (ERTLptr_status trans_prog stack_sizes) st = as_label 
(ERTL_status prog stack_sizes) (sigma_state_pc prog sigma st).
#prog #sigma #stack_size * #st #pc #lp
whd in match as_label; normalize nodelta whd in match (as_pc_of ??) in ⊢ (??%%);
whd in match (as_label_of_pc ??) in ⊢ (??%%); 


(*

whd in match fetch_statement; normalize nodelta
whd in match sigma_state_pc; normalize nodelta @if_elim
[ #EQbl whd in match fetch_internal_function; normalize nodelta >m_bind_bind
 lapply(fetch_function_no_minus_one ??????) [2: @(pc_block pc) | lapply EQbl
 @eqZb_elim #H * @H| @(ertl_to_ertlptr prog) |7: #EQ >EQ |*:] normalize nodelta
 whd in match dummy_state_pc; whd in match (as_label_of_pc ??); whd in match null_pc;
 whd in match fetch_statement; normalize nodelta whd in match fetch_internal_function;
 normalize nodelta >m_bind_bind 
 lapply(fetch_function_no_zero ??????) [2: @( «mk_block Code OZ,refl region Code»)
 | % | @prog |7: #EQ >EQ |*:] %
| inversion ( fetch_internal_function
     (joint_closed_internal_function ERTL
      (prog_var_names (joint_function ERTL) ℕ prog))
     (globalenv_noinit (joint_function ERTL) prog) (pc_block pc))
 [ * #id #fn #fn_spec #_ lapply(fetch_internal_function_transf ??????? fn_spec)
   [ @(λvars,fn.translate_internal … fn) |] #EQ >EQ >m_return_bind normalize nodelta
     whd in match (as_label_of_pc ??);
     whd in match fetch_statement; normalize nodelta >fn_spec >m_return_bind
     cases daemon (*serve specifica su sigma TODO*)
   | #err #EQ lapply(jmeq_to_eq ??? EQ) -EQ #fetch_err #_ normalize nodelta 
     whd in match dummy_state_pc; 
     whd in match (as_label_of_pc ??); whd in match null_pc;
     whd in match fetch_statement; normalize nodelta 
     whd in match fetch_internal_function in ⊢ (???%);
     normalize nodelta 
     lapply(fetch_function_no_zero ??????) [2: @( «mk_block Code OZ,refl region Code»)
     | % | @prog |7: #EQ >EQ in ⊢ (???%); |*:] normalize nodelta -EQ
     lapply fetch_err -fetch_err whd in match fetch_internal_function; normalize nodelta
     inversion(fetch_function ???) 
     [* #id * #fn #fn_spec >m_return_bind normalize nodelta [whd in ⊢ (??%? → ?); #EQ destruct]
     #EQ destruct  lapply(jmeq_to_eq ??? fn_spec) -fn_spec #fn_spec 
     lapply(fetch_function_transf ????????? fn_spec) [ #v  @transf_fundef [2:@translate_internal |]|]
     #EQ >EQ >m_return_bind %
   | #err1 #EQ lapply(jmeq_to_eq ??? EQ) -EQ #EQfetch whd in ⊢ (??%? → ?); #EQ destruct 
     normalize nodelta lapply EQfetch -EQfetch whd in match fetch_function;
     normalize nodelta check joint_function
      lapply(symbol_for_block_transf  ? ? ? ? prog (λvars.?)  (pc_block pc))
      [@transf_fundef [2: @translate_internal|] |4: #EQ >EQ in ⊢ (? → %); |*:]  
     cases(symbol_for_block ???) [ whd in ⊢ (??%% → ?); #EQ destruct %]
     #id >m_return_bind inversion(find_funct_ptr ???)
     [2: #fn1 #_ >m_return_bind whd in ⊢ (??%? → ?); #EQ destruct] 
     #EQf whd in ⊢ (??%? → ?); #EQ destruct 
     lapply(find_funct_ptr_none ??????? EQf) (*forse e' falso*)
     [#vars @transf_fundef [2: @translate_internal|]|]
     #EQ >EQ %
     ]
  ]
]*)
cases daemon
qed.

lemma bool_of_beval_ok : ∀prog : ertlptr_program.
∀sigma : sigma_map prog.
preserving1 … res_preserve1 …
    (sigma_beval prog sigma)
    (λx.x)
    (bool_of_beval)
    (bool_of_beval).
#prog #sigma whd in match bool_of_beval; normalize nodelta
* normalize nodelta
 [ | | #ptr1 #ptr2 #p | #by | #p | #ptr #p | #pc #p]
try @res_preserve_error1 #x 
[1,2,3,4: whd in ⊢ (???% → ?); #EQ destruct 
          [1,4: %{true} % //
          |3: %{false} % //
          | %{(eq_bv 8 (zero 8) by)} % //
          ]
| whd in match sigma_beval; normalize nodelta cases(sigma_pc_opt ? ? ?) 
  normalize nodelta [2: #pc1] whd in ⊢ (???% → ?); #EQ destruct 
]
qed.

lemma eval_cond_ok :
∀prog.
let trans_prog ≝ ertl_to_ertlptr prog in
∀stack_sizes.
∀sigma : sigma_map trans_prog.
∀st,st',f,fn,a,ltrue,lfalse.
 fetch_statement ERTL_semantics …
  (globalenv_noinit ? prog) (pc … (sigma_state_pc ? sigma st)) =
    return 〈f, fn,  sequential … (COND ERTL … a ltrue) lfalse〉 →
 eval_state ERTL_semantics
   (prog_var_names (joint_function ERTL_semantics) ℕ prog) 
   (ev_genv … (mk_prog_params ERTL_semantics prog stack_sizes)) 
   (sigma_state_pc ? sigma st) =
  return st' → 
as_costed (ERTL_status prog stack_sizes)
  st' → 
∃ st''. st' = sigma_state_pc ? sigma st'' ∧
∃taf : trace_any_any_free (ERTLptr_status trans_prog stack_sizes)
st st''.
bool_to_Prop (taaf_non_empty … taf).
#prog #stack_size #sigma #st #st' #f #fn #a #lb_t #lb_f 
whd in match sigma_state_pc in ⊢ (% → ?); normalize nodelta
@if_elim 
[ #EQbl whd in match dummy_state_pc; whd in match null_pc;
  whd in match fetch_statement; whd in match fetch_internal_function;
  normalize nodelta >(fetch_function_no_zero ??????) [2: %] 
  whd in ⊢ (??%% → ?); #EQ destruct ]
#Hbl inversion(fetch_internal_function ???)
[2: #e #_ normalize nodelta whd in match dummy_state_pc; whd in match null_pc;
   whd in match fetch_statement; whd in match fetch_internal_function;
  normalize nodelta >(fetch_function_no_zero ??????) [2: %]
 whd in ⊢ (??%% → ?); #EQ destruct]
* #f1 #fn1 #EQ lapply(jmeq_to_eq ??? EQ) -EQ #fn1_spec normalize nodelta
#EQf lapply EQf whd in match fetch_statement; normalize nodelta >fn1_spec
>m_return_bind #H @('bind_inversion H) -H #stmt' #_ whd in ⊢ (??%% → ?);
#EQ destruct whd in match eval_state; whd in match eval_statement_no_pc;
whd in match eval_statement_advance; whd in match sigma_state_pc in ⊢ (% → ?); 
normalize nodelta @if_elim [#H >H in Hbl; *] #_ >fn1_spec normalize nodelta
>EQf >m_return_bind normalize nodelta >m_return_bind 
#H lapply(err_eq_from_io ????? H) -H #H @('bind_inversion H) -H #bv
change with (ps_reg_retrieve ?? = ? → ?) whd in match set_no_pc;
whd in match sigma_state in ⊢ (??(?%?)? → ?); normalize nodelta #bv_spec
#H @('bind_inversion H) -H * #EQbv normalize nodelta
[ whd in match goto; normalize nodelta >pc_of_label_eq [2: assumption |3:]
  >m_return_bind whd in match pc_of_point; normalize nodelta whd in ⊢ (??%% → ?);
  whd in match set_pc; normalize nodelta #EQ destruct
| whd in match next; whd in match set_pc; normalize nodelta whd in match (succ_pc ???);
  whd in match (point_of_succ ???); whd in ⊢ (??%% → ?); #EQ destruct 
]
whd in match as_costed; normalize nodelta * #n_cost % 
[1,3: % [1,4: @st 
        |2,5: @(mk_program_counter 
                  (pc_block (pc ERTLptr_semantics st))
                  (offset_of_point ERTL_semantics ?)) [ @lb_t | @lb_f]
        |3,6: @(last_pop ? st)
        ] 
]
% [1,3: whd in match sigma_state_pc; normalize nodelta @if_elim 
       [1,3: #EQ >EQ in Hbl; *] #_ >fn1_spec %] 
%{(taaf_step_jump … (taa_base …) …) I}
lapply (fetch_statement_commute prog sigma … stack_size … EQf)
normalize nodelta #EQf' 
[1,4: whd in match as_costed; normalize nodelta >as_label_ok [2,4: @sigma] 
      % #H @n_cost <H whd in match sigma_state_pc; normalize nodelta 
      @if_elim [1,3: #EQ >EQ in Hbl; *] #_ >fn1_spec %
|2,5: whd in match as_classifier; normalize nodelta  whd in match (as_classify ??);
      normalize nodelta >EQf' %
|*:  whd in match (as_execute ???); whd in match eval_state; normalize nodelta
     >EQf' >m_return_bind whd in match eval_statement_no_pc; normalize nodelta
     >m_return_bind whd in match eval_statement_advance; normalize nodelta  
     change with (ps_reg_retrieve ??) in ⊢ (??(????(????%?))?);
     cases(ps_reg_retrieve_ok ????? ? bv_spec) #bv' * #bv_spec' #bv_bv'
     >bv_spec' >m_return_bind >bv_bv' in EQbv; #EQbv
     cases(bool_of_beval_ok ? sigma ? ? EQbv) #b1 * #b1_spec #EQ destruct
     >b1_spec >m_return_bind normalize nodelta [2: %] whd in match goto;
     normalize nodelta whd in match set_no_pc; normalize nodelta 
     >pc_of_label_eq 
     [ % 
     | lapply(fetch_internal_function_transf ????????) 
       [3: @f |2: @fn | whd in ⊢ (???%); <fn1_spec in ⊢ (???%); % 
       | | #vars @translate_internal |9: #EQ >EQ in ⊢ (??%?); % |*:]
       |
     ]
]
qed.
       

lemma
  find_funct_ptr_none:
    ∀A,B,V,iV. ∀p: program A V. ∀transf: (∀vs. A vs → B vs).
    ∀b: block.
    find_funct_ptr ? (globalenv … iV p) b = None ? →
    find_funct_ptr ? (globalenv … iV (transform_program … p transf)) b = None ?.
#A #B #V #i #p #transf #b 
whd in match find_funct_ptr; normalize nodelta
cases b -b * normalize nodelta [#x #_ %] * normalize nodelta 
[1,2: [2: #x] #_ %] #x whd in match globalenv; normalize nodelta
whd in match globalenv_allocmem; normalize nodelta
cases daemon (*forse e' falso *)
qed.