Changeset 2592


Ignore:
Timestamp:
Jan 29, 2013, 11:20:53 AM (6 years ago)
Author:
piccolo
Message:

main lemma of ERTLptr in place

Location:
src
Files:
3 edited

Legend:

Unmodified
Added
Removed
  • src/ERTLptr/ERTLtoERTLptr.ma

    r2570 r2592  
    1616include "ERTLptr/ERTLptr.ma".
    1717include "joint/TranslateUtils.ma".
    18 
     18 
    1919definition translate_step_seq :
    2020∀globals.(joint_seq ERTL globals) → (joint_seq ERTLptr globals) ≝
  • src/ERTLptr/ERTLtoERTLptrOK.ma

    r2590 r2592  
    4646    ERTLptr_semantics (pc_block pc) ertl_ptr_point.
    4747
    48 
    4948definition sigma_stored_pc ≝
    5049λprog,sigma,pc. match sigma_pc_opt prog sigma pc with
    51       [None ⇒ null_pc | Some x ⇒ x].
     50      [None ⇒ null_pc (pc_offset … pc) | Some x ⇒ x].
    5251     
    5352     
     
    10881087   
    10891088definition dummy_state_pc : state_pc ERTL_semantics ≝
    1090 mk_state_pc ? dummy_state null_pc null_pc.
     1089mk_state_pc ? dummy_state (null_pc one) (null_pc one).
    10911090
    10921091check fetch_internal_function
     
    16841683qed.
    16851684
     1685lemma sp_ok : ∀prog : ertl_program. ∀sigma : sigma_map (ertl_to_ertlptr prog).
     1686∀stack_size.
     1687∀fn : (joint_closed_internal_function ? (globals (mk_prog_params ERTL_semantics prog stack_size))).
     1688preserving1 … res_preserve1 …
     1689      (λst.sigma_state (ertl_to_ertlptr prog) sigma st (joint_if_locals ERTL ? fn))
     1690      (λx.x)
     1691      (sp ERTL_semantics)
     1692      (sp ERTLptr_semantics).
     1693cases daemon
     1694qed.
     1695
     1696lemma set_sp_ok :  ∀prog : ertl_program.
     1697let trans_prog ≝ ertl_to_ertlptr prog in
     1698∀sigma : sigma_map trans_prog.
     1699∀stack_size.
     1700∀fn : (joint_closed_internal_function ? (globals (mk_prog_params ERTL_semantics prog stack_size))).
     1701∀ptr,st.
     1702set_sp ? ptr (sigma_state trans_prog sigma st (joint_if_locals ERTL ? fn)) =
     1703sigma_state trans_prog sigma (set_sp ? ptr st) (joint_if_locals ERTL ? fn).
     1704cases daemon
     1705qed.
     1706
    16861707lemma eval_seq_no_pc_no_call_ok :
    16871708∀prog : ertl_program.
     
    16921713      (λst.sigma_state trans_prog sigma st (joint_if_locals ERTL ? fn))
    16931714      (λst.sigma_state trans_prog sigma st (joint_if_locals ERTL ? fn))
    1694       (eval_seq_no_pc (mk_prog_params ERTL_semantics prog stack_size)
     1715      (eval_seq_no_pc ERTL_semantics
    16951716             (globals (mk_prog_params ERTL_semantics prog stack_size))
    16961717             (ev_genv (mk_prog_params ERTL_semantics prog stack_size)) id fn seq)
    1697       (eval_seq_no_pc (mk_prog_params ERTLptr_semantics trans_prog stack_size)
     1718      (eval_seq_no_pc ERTLptr_semantics
    16981719  (globals (mk_prog_params ERTLptr_semantics trans_prog stack_size))
    16991720  (ev_genv (mk_prog_params ERTLptr_semantics trans_prog stack_size)) id (translate_internal … fn) (translate_step_seq … seq)).
     
    17061727  [ @(λregs.sigma_regs (ertl_to_ertlptr prog) sigma regs (joint_if_locals ERTL ? fn))
    17071728  | change with (ertl_eval_move ??) in ⊢ (???????%%); @ertl_eval_move_ok
    1708   | #regs #st whd in ⊢ (??%% → ?); #EQ destruct % [2: % [%] % |]
     1729  | #regs  @mfr_return_eq1 %
    17091730  ]
    17101731| #r #st @mfr_bind1
     
    17161737    [@(λregs.sigma_regs (ertl_to_ertlptr prog) sigma regs (joint_if_locals ERTL ? fn))
    17171738    | @ps_reg_store_ok
    1718     | #regs #x whd in ⊢ (??%% → ?); #EQ destruct % [2: % [%] % |]
     1739    | #regs  @mfr_return_eq1 %
    17191740    ]
    17201741  ]
     
    17421763                                               in ⊢ (???????(?????%?)?);
    17431764       @ps_reg_store_ok
    1744     | #regs #st1 whd in match set_regs; whd in match sigma_state; normalize nodelta;
    1745       whd in ⊢(??%% → ?); #EQ destruct % [2: % [%] %|]
     1765    | #regs  @mfr_return_eq1 %
    17461766    ]
    17471767  | #st1 @opt_safe_elim #bl #EQbl @opt_safe_elim #bl'   
     
    17541774                                               in ⊢ (???????(?????%?)?);
    17551775      @ps_reg_store_ok
    1756     | #regs #st1 whd in match set_regs; whd in match sigma_state; normalize nodelta;
    1757       whd in ⊢(??%% → ?); #EQ destruct % [2: % [%] %|]
     1776    | #regs  @mfr_return_eq1 %
    17581777    ]
    17591778  ]
     
    17761795         [  @(λregs.sigma_regs (ertl_to_ertlptr prog) sigma regs (joint_if_locals ERTL ? fn))
    17771796         | @ps_reg_store_ok
    1778          | #regs #st1 whd in match set_regs; whd in match sigma_state; normalize nodelta;
    1779             whd in ⊢(??%% → ?); #EQ destruct % [2: % [%] %|]
     1797         | #regs  @mfr_return_eq1 %
    17801798         ]
    17811799       | #st1 whd in match accb_store; normalize nodelta @mfr_bind1
     
    17831801         |  whd in match sigma_state; normalize nodelta
    17841802            @ps_reg_store_ok
    1785          | #regs #st1 whd in match set_regs; whd in match sigma_state; normalize nodelta;
    1786             whd in ⊢(??%% → ?); #EQ destruct % [2: % [%] %|]
    1787          ]
     1803         | #regs  @mfr_return_eq1 %         ]
    17881804       ]
    17891805     ]
     
    17991815      [ @(λregs.sigma_regs (ertl_to_ertlptr prog) sigma regs (joint_if_locals ERTL ? fn))
    18001816      | whd in match sigma_state; normalize nodelta @ps_reg_store_ok
    1801       | #regs #st1 whd in match set_regs; whd in match sigma_state; normalize nodelta;
    1802             whd in ⊢(??%% → ?); #EQ destruct % [2: % [%] %|]
     1817      | #regs  @mfr_return_eq1 %
    18031818      ]
    18041819    ]
     
    18181833          [  @(λregs.sigma_regs (ertl_to_ertlptr prog) sigma regs (joint_if_locals ERTL ? fn))
    18191834          | whd in match sigma_state; normalize nodelta @ps_reg_store_ok
    1820           | #regs #st1 whd in match set_regs; whd in match sigma_state; normalize nodelta;
    1821             whd in ⊢(??%% → ?); #EQ destruct % [2: % [%] %|]
     1835          | #regs  @mfr_return_eq1 %
    18221836          ]
    1823         | #st1 #st2 whd in match set_carry; whd in match sigma_state; normalize nodelta
    1824            whd in ⊢ (??%% → ?); #EQ destruct % [2: % [%] % |] 
     1837        | #st1 @mfr_return_eq1 %
    18251838        ]
    18261839      ]
    18271840    ]
    18281841  ]
    1829 | #st whd in match set_carry; whd in match sigma_state; normalize nodelta
    1830   #st1 whd in ⊢ (??%% → ?); #EQ destruct % [2: % [%] % |]
    1831 | #st #st1 whd in match set_carry; whd in match sigma_state; normalize nodelta
    1832    whd in ⊢ (??%% → ?); #EQ destruct % [2: % [%] % |]
     1842| #st  @mfr_return_eq1 %
     1843| #st  @mfr_return_eq1 %
    18331844| #r1 #dpl #dph #st @mfr_bind1
    18341845  [ @(sigma_beval (ertl_to_ertlptr prog) sigma)
     
    18461857          [ @(λregs.sigma_regs (ertl_to_ertlptr prog) sigma regs (joint_if_locals ERTL ? fn))
    18471858          |  whd in match sigma_state; normalize nodelta @ps_reg_store_ok
    1848           | #regs #st1 whd in match set_regs; whd in match sigma_state; normalize nodelta;
    1849             whd in ⊢(??%% → ?); #EQ destruct % [2: % [%] %|]
     1859          | #regs  @mfr_return_eq1 %
    18501860          ]
    18511861        ] 
     
    18681878          [ @(sigma_mem (ertl_to_ertlptr prog) sigma)
    18691879          | @opt_to_res_preserve1 @bestorev_ok
    1870           | #m #st1 whd in ⊢ (??%% → ?); whd in match set_m; whd in match sigma_state;
    1871             normalize nodelta #EQ destruct % [2: % [%] %|]
     1880          | #m @mfr_return_eq1 %
    18721881          ]
    18731882        ]
     
    18751884    ]
    18761885  ]
    1877 | #ext #st cases daemon
     1886| #ext #st whd in ⊢ (???????%%); whd in match (stack_sizes ????); cases (stack_size f)
     1887  normalize nodelta
     1888  [ @res_preserve_error1
     1889  | #n cases ext normalize nodelta
     1890    [1,2: @mfr_bind1
     1891      [1,4: @(λx.x)
     1892      |2,5: @sp_ok
     1893      |3,6: #ptr @mfr_return_eq1 >set_sp_ok %
     1894      ]
     1895    | #r whd in match ps_reg_store_status; normalize nodelta @mfr_bind1
     1896      [2: whd in match sigma_state; normalize nodelta
     1897          change with (sigma_beval ? sigma (BVByte ?)) in ⊢ (???????(??%?)?);
     1898          @ps_reg_store_ok
     1899      |
     1900      | #regs @mfr_return_eq1 %
     1901      ]
     1902    ]
     1903  ]     
    18781904]
    18791905qed.
     1906
     1907lemma fetch_statement_commute :
     1908∀prog : ertl_program.
     1909let trans_prog ≝ (ertl_to_ertlptr prog) in
     1910∀sigma : sigma_map trans_prog.
     1911∀stack_sizes,id,fn,stmt,pc.
     1912fetch_statement ERTL_semantics
     1913(globals (mk_prog_params ERTL_semantics prog stack_sizes))
     1914(ev_genv (mk_prog_params ERTL_semantics prog stack_sizes))
     1915pc = return 〈id,fn,stmt〉 →
     1916match stmt with
     1917[ sequential seq nxt ⇒
     1918    match seq with
     1919    [ CALL ids args dest ⇒
     1920        match ids with
     1921        [ inl i ⇒
     1922          fetch_statement ERTLptr_semantics
     1923          (globals (mk_prog_params ERTLptr_semantics trans_prog stack_sizes))
     1924          (ev_genv (mk_prog_params ERTLptr_semantics trans_prog stack_sizes))
     1925          pc =
     1926          return 〈id,
     1927          translate_internal … fn,
     1928          sequential ?? (CALL ERTLptr ? (inl ?? i) args dest) nxt〉
     1929        | inr p ⇒ ?(*
     1930          ∃reg,lbl.
     1931          fetch_statement ERTLptr_semantics
     1932          (globals (mk_prog_params ERTLptr_semantics trans_prog stack_sizes))
     1933          (ev_genv (mk_prog_params ERTLptr_semantics trans_prog stack_sizes))
     1934           pc = return 〈id,translate_internal … fn,sequential ?? (extension_seq ERTLptr ? (LOW_ADDRESS reg lbl)) nxt〉
     1935           ∧ ∃ nxt'.
     1936           ! pc' ← get_pc_from_label ? ? (ev_genv (mk_prog_params ERTLptr_semantics trans_prog stack_sizes))
     1937                 id nxt;
     1938           fetch_statement ERTLptr_semantics
     1939          (globals (mk_prog_params ERTLptr_semantics trans_prog stack_sizes))
     1940          (ev_genv (mk_prog_params ERTLptr_semantics trans_prog stack_sizes))
     1941           pc' = return 〈id,translate_internal … fn,sequential ?? (step_seq ERTLptr ? (PUSH … (Reg … reg))) nxt'〉
     1942           ∧ ∃ nxt''.
     1943           ! pc' ← get_pc_from_label ? ? (ev_genv (mk_prog_params ERTLptr_semantics trans_prog stack_sizes))
     1944                 id nxt';
     1945           fetch_statement ERTLptr_semantics
     1946          (globals (mk_prog_params ERTLptr_semantics trans_prog stack_sizes))
     1947          (ev_genv (mk_prog_params ERTLptr_semantics trans_prog stack_sizes))
     1948           pc' = return 〈id,translate_internal … fn,sequential ?? (extension_seq ERTLptr ? (HIGH_ADDRESS reg lbl)) nxt''〉
     1949           ∧ ∃ nxt'''.
     1950           ! pc' ← get_pc_from_label ? ? (ev_genv (mk_prog_params ERTLptr_semantics trans_prog stack_sizes))
     1951                 id nxt'';
     1952           fetch_statement ERTLptr_semantics
     1953          (globals (mk_prog_params ERTLptr_semantics trans_prog stack_sizes))
     1954          (ev_genv (mk_prog_params ERTLptr_semantics trans_prog stack_sizes))
     1955           pc' = return 〈id,translate_internal … fn,sequential ?? (step_seq ERTLptr ? (PUSH … (Reg … reg))) nxt'''〉
     1956           ∧ ∃ nxt''''.
     1957           ! pc' ← get_pc_from_label ? ? (ev_genv (mk_prog_params ERTLptr_semantics trans_prog stack_sizes))
     1958                 id nxt''';
     1959           fetch_statement ERTLptr_semantics
     1960          (globals (mk_prog_params ERTLptr_semantics trans_prog stack_sizes))
     1961          (ev_genv (mk_prog_params ERTLptr_semantics trans_prog stack_sizes))
     1962           pc' = return 〈id,translate_internal … fn,sequential ?? (CALL ERTLptr ? (inr ?? p) args dest) nxt''''〉
     1963           ∧ sigma (translate_internal … fn) nxt''' =  return point_of_pc ERTL_semantics pc *)
     1964        ]
     1965    | COND r lbl ⇒
     1966          fetch_statement ERTLptr_semantics
     1967          (globals (mk_prog_params ERTLptr_semantics trans_prog stack_sizes))
     1968          (ev_genv (mk_prog_params ERTLptr_semantics trans_prog stack_sizes))
     1969          pc =
     1970          return 〈id,
     1971          translate_internal … fn,
     1972          sequential ?? (COND ERTLptr ? r lbl) nxt〉
     1973    | step_seq s ⇒
     1974          fetch_statement ERTLptr_semantics
     1975          (globals (mk_prog_params ERTLptr_semantics trans_prog stack_sizes))
     1976          (ev_genv (mk_prog_params ERTLptr_semantics trans_prog stack_sizes))
     1977          pc =
     1978          return 〈id,
     1979          translate_internal … fn,
     1980          sequential ?? (step_seq ERTLptr … (translate_step_seq ? s)) nxt〉
     1981    ]                   
     1982| final fin ⇒
     1983     fetch_statement ERTLptr_semantics
     1984     (globals (mk_prog_params ERTLptr_semantics trans_prog stack_sizes))
     1985     (ev_genv (mk_prog_params ERTLptr_semantics trans_prog stack_sizes))
     1986     pc = return 〈id,(translate_internal … fn),final … (joint_fin_step_id fin)〉
     1987| FCOND abs _ _ _ ⇒ Ⓧabs
     1988].
     1989cases daemon
     1990qed.
     1991
     1992lemma eval_seq_no_call_ok :
     1993 ∀prog.
     1994 let trans_prog ≝ ertl_to_ertlptr prog in
     1995 ∀sigma : sigma_map trans_prog.∀stack_sizes.
     1996 (*? →*)
     1997 ∀st,st',f,fn,stmt,nxt.
     1998   fetch_statement ERTL_semantics
     1999     (prog_var_names (joint_function ERTL_semantics) ℕ prog)
     2000    (ev_genv (mk_prog_params ERTL_semantics prog stack_sizes))
     2001    (pc … (sigma_state_pc ? sigma st)) =
     2002      return 〈f, fn,  sequential … (step_seq ERTL … stmt) nxt〉 →
     2003   eval_state ERTL_semantics
     2004   (prog_var_names (joint_function ERTL_semantics) ℕ prog)
     2005   (ev_genv … (mk_prog_params ERTL_semantics prog stack_sizes))
     2006   (sigma_state_pc ? sigma st) =
     2007    return st' →
     2008 ∃st''. st' = sigma_state_pc ? sigma st'' ∧
     2009 ∃taf : trace_any_any_free (ERTLptr_status trans_prog stack_sizes)
     2010  st
     2011  st''.
     2012 bool_to_Prop (taaf_non_empty … taf).
     2013#prog #sigma #stack_size #st1 #st2 #f #fn #stmt #nxt #EQf whd in match eval_state;
     2014normalize nodelta >EQf >m_return_bind whd in match eval_statement_advance;
     2015whd in match eval_statement_no_pc; normalize nodelta
     2016 #H @('bind_inversion H) -H #st_no_pc #EQ lapply(err_eq_from_io ????? EQ) -EQ
     2017#EQeval whd in ⊢ (??%% → ?); #EQ destruct lapply EQf
     2018whd in match sigma_state_pc in ⊢ (% → ?); normalize nodelta @if_elim
     2019[ #EQbl
     2020| #pc_st1_spec inversion(fetch_internal_function ???) [2: #e #_]
     2021]
     2022[1,2: whd in match dummy_state_pc; whd in match null_pc;
     2023  whd in match fetch_statement; normalize nodelta whd in match fetch_internal_function;
     2024  normalize nodelta lapply(fetch_function_no_zero ??????)
     2025  [2,9: @( «mk_block Code OZ,refl region Code»)
     2026    |1,8: % |3,10: @prog |7,14: #EQ >EQ |*:]  whd in ⊢ (??%% → ?); #EQ destruct]
     2027* #f1 #fn1 #EQ lapply(jmeq_to_eq ??? EQ) -EQ #fn1_spec normalize nodelta
     2028whd in match fetch_statement; normalize nodelta >fn1_spec
     2029>m_return_bind #H @('bind_inversion H) -H #stmt1 #EQ
     2030lapply(opt_eq_from_res ???? EQ) -EQ #stmt1_spec whd in ⊢ (??%% → ?); #EQ destruct
     2031lapply EQeval -EQeval whd in match sigma_state_pc in ⊢ (% → ?);
     2032normalize nodelta @if_elim [#H >H in pc_st1_spec; *] #_ >fn1_spec
     2033normalize nodelta #EQeval cases(eval_seq_no_pc_no_call_ok ???????? EQeval)
     2034#st_no_pc' * #EQeval' #EQst_no_pc'
     2035whd in match set_no_pc; normalize nodelta
     2036% [ % [@st_no_pc'|@(succ_pc ERTL_semantics (pc ERTL_semantics (sigma_state_pc prog sigma st1))
     2037   nxt)| @(last_pop ? st1)]]
     2038% [ whd in match sigma_state_pc; normalize nodelta
     2039    @if_elim [#H >H in pc_st1_spec; *] #_ >fn1_spec normalize nodelta
     2040    @if_elim [#H >H in pc_st1_spec; *] #_ >fn1_spec normalize nodelta
     2041    >EQst_no_pc' %]
     2042%{(taaf_step … (taa_base …) …)}
     2043[3: //] lapply(fetch_statement_commute ? sigma ????? EQf) normalize nodelta
     2044whd in match sigma_state_pc; normalize nodelta
     2045@if_elim [1,3:#H >H in pc_st1_spec; *] #_ >fn1_spec normalize nodelta
     2046#EQf1
     2047[ whd in match as_classifier; normalize nodelta whd in match (as_classify ??);
     2048  >EQf1 normalize nodelta %
     2049| whd in match (as_execute ???); whd in match eval_state; normalize nodelta
     2050  >EQf1 >m_return_bind whd in match eval_statement_no_pc; normalize nodelta
     2051  >EQeval' >m_return_bind %
     2052]
     2053qed.
     2054
     2055lemma pc_of_label_eq :
     2056  ∀globals,ge,bl,i_fn,lbl.
     2057  fetch_internal_function ? ge bl = return i_fn →
     2058  pc_of_label ERTL_semantics globals ge bl lbl =
     2059    OK ? (pc_of_point ERTL_semantics bl lbl).
     2060#globals #ge #bl #i_fn #lbl #EQf whd in match pc_of_label;
     2061normalize nodelta >EQf %
     2062qed.
     2063
     2064lemma eval_goto_ok :
     2065 ∀prog : ertl_program.
     2066 let trans_prog ≝ ertl_to_ertlptr prog in
     2067 ∀stack_sizes.
     2068 ∀sigma : sigma_map trans_prog.
     2069 ∀st,st',f,fn,nxt.
     2070   fetch_statement ERTL_semantics …
     2071    (globalenv_noinit ? prog) (pc … (sigma_state_pc ? sigma st)) =
     2072      return 〈f, fn,  final … (GOTO ERTL … nxt)〉 →
     2073   eval_state ERTL_semantics
     2074   (prog_var_names (joint_function ERTL_semantics) ℕ prog)
     2075   (ev_genv … (mk_prog_params ERTL_semantics prog stack_sizes))
     2076   (sigma_state_pc ? sigma st) =
     2077    return st' →
     2078    ∃ st''. st' = sigma_state_pc ? sigma st'' ∧
     2079 ∃taf : trace_any_any_free (ERTLptr_status trans_prog stack_sizes)
     2080  st
     2081  st''.
     2082 bool_to_Prop (taaf_non_empty … taf).
     2083#prog #stack_sizes #sigma #st #st' #f #fn #nxt
     2084whd in match sigma_state_pc in ⊢ (% → ?); normalize nodelta
     2085@if_elim
     2086[ #EQbl whd in match dummy_state_pc; whd in match null_pc;
     2087  whd in match fetch_statement; whd in match fetch_internal_function;
     2088  normalize nodelta lapply(fetch_function_no_zero ??????)
     2089  [2: @( «mk_block Code OZ,refl region Code»)
     2090    | % | @prog |7: #EQ >EQ |*:]  whd in ⊢ (??%% → ?); #EQ destruct]
     2091#Hbl inversion(fetch_internal_function ???)
     2092[2: #e #_ normalize nodelta whd in match dummy_state_pc; whd in match null_pc;
     2093   whd in match fetch_statement; whd in match fetch_internal_function;
     2094  normalize nodelta lapply(fetch_function_no_zero ??????)
     2095  [2: @( «mk_block Code OZ,refl region Code»)
     2096    | % | @prog |7: #EQ >EQ |*:]  whd in ⊢ (??%% → ?); #EQ destruct]
     2097* #f1 #fn1 #EQ lapply(jmeq_to_eq ??? EQ) -EQ #fn1_spec normalize nodelta
     2098#EQf lapply EQf whd in match fetch_statement; normalize nodelta >fn1_spec
     2099>m_return_bind #H @('bind_inversion H) -H #stmt' #_ whd in ⊢ (??%% → ?);
     2100#EQ destruct whd in match sigma_state_pc in ⊢ (% → ?); normalize nodelta
     2101@if_elim [#H >H in Hbl; *] #_ >fn1_spec normalize nodelta whd in match eval_state;
     2102normalize nodelta >EQf >m_return_bind whd in match eval_statement_advance;
     2103whd in match eval_statement_no_pc; normalize nodelta >m_return_bind
     2104whd in match goto; normalize nodelta #H lapply (err_eq_from_io ????? H) -H
     2105#H @('bind_inversion H) -H #pc' whd in match set_no_pc; normalize nodelta
     2106>(pc_of_label_eq … fn1_spec) whd in ⊢ (???% → ?); #EQ whd in ⊢ (??%% → ?); #EQ1
     2107destruct lapply (fetch_statement_commute … sigma … stack_sizes … EQf)
     2108normalize nodelta #EQf' %
     2109[ % [ @st
     2110    | @(mk_program_counter
     2111         (pc_block (pc ERTLptr_semantics st))
     2112         (offset_of_point ERTL_semantics nxt))
     2113    | @(last_pop … st)
     2114    ]
     2115] %
     2116[ whd in match sigma_state_pc; normalize nodelta @if_elim [#H >H in Hbl; *]
     2117  >fn1_spec normalize nodelta #_ % ]
     2118%{(taaf_step … (taa_base …) …)}
     2119[ whd in match as_classifier; normalize nodelta whd in match (as_classify ??);
     2120  >EQf' normalize nodelta %
     2121| whd in match (as_execute ???); whd in match eval_state; normalize nodelta
     2122  >EQf' >m_return_bind whd in match eval_statement_no_pc;
     2123  whd in match eval_statement_advance; normalize nodelta >m_return_bind
     2124  whd in match goto; normalize nodelta whd in match pc_of_label; normalize nodelta
     2125  lapply(fetch_internal_function_transf ??????? fn1_spec)
     2126  [ #vars @translate_internal |] #EQ >EQ >m_return_bind %
     2127| %
     2128]
     2129qed.
     2130
     2131axiom partial_inj_sigma : ∀ prog : ertlptr_program.
     2132∀sigma :sigma_map prog.
     2133∀fn,lbl1,lbl2. sigma fn lbl1 ≠ None ? → sigma fn lbl1 = sigma fn lbl2 → lbl1 = lbl2.
     2134
     2135lemma pop_ra_ok :
     2136∀prog : ertl_program.
     2137let trans_prog ≝ ertl_to_ertlptr prog in
     2138∀sigma : sigma_map trans_prog.
     2139∀stack_size.
     2140∀fn : (joint_closed_internal_function ? (globals (mk_prog_params ERTL_semantics prog stack_size))).
     2141preserving1 … res_preserve1 …
     2142     (λst.sigma_state trans_prog sigma st (joint_if_locals ERTL ? fn))
     2143     (λx.let 〈st,pc〉 ≝ x in
     2144       〈sigma_state trans_prog sigma st (joint_if_locals ERTL ? fn),
     2145        sigma_stored_pc ? sigma pc〉)
     2146     (pop_ra ERTL_semantics)
     2147     (pop_ra ERTLptr_semantics).
     2148#prog #sigma #stack_size #fn #st whd in match pop_ra; normalize nodelta @mfr_bind1
     2149[ | @pop_ok ] * #bv #st1 @mfr_bind1 [ | @pop_ok] * #bv1 #st2 @mfr_bind1
     2150[ @(sigma_stored_pc ? sigma) | whd in match pc_of_bevals; normalize nodelta
     2151  cases bv [ | | #ptr1 #ptr2 #p | #by | #p | #ptr #p | #pc #p]
     2152  whd in match sigma_beval; normalize nodelta try @res_preserve_error1
     2153  inversion(sigma_pc_opt ? ? ?) normalize nodelta [ #_ @res_preserve_error1]
     2154  #sigma_pc #sigma_pc_spec normalize nodelta cases bv1
     2155  [ | | #ptr1 #ptr2 #p | #by | #p | #ptr #p | #pc1 #p1]
     2156  normalize nodelta try @res_preserve_error1
     2157  inversion(sigma_pc_opt ? ? ?) normalize nodelta [#_ @res_preserve_error1]
     2158  #sigma_pc1 #sigma_pc1_spec @if_elim [2: #_ @res_preserve_error1]
     2159  @andb_elim @if_elim [2: #_ *] @andb_elim @if_elim [2: #_ *]
     2160  #_ #H >H @eq_program_counter_elim [2: #_ *]
     2161  #EQspc * @eq_program_counter_elim
     2162  [#_ normalize nodelta @mfr_return_eq1 whd in match sigma_stored_pc; normalize nodelta
     2163   >sigma_pc1_spec %] * #H1 @⊥ @H1 >EQspc in sigma_pc_spec; <sigma_pc1_spec
     2164   whd in match sigma_pc_opt; normalize nodelta @if_elim
     2165  [ #H2 #EQ lapply(sym_eq ??? EQ) -EQ @if_elim [#_  whd in ⊢ (??%% → ?); #EQ destruct %]
     2166    #H3 #H @('bind_inversion H) -H #x #_ #H @('bind_inversion H) -H #y #_
     2167    cases sigma_pc1 in H2; #bl_pc1 #z #H2 whd in ⊢ (??%? → ?); #EQ destruct >H2 in H3; *
     2168  | #H2 @if_elim
     2169    [ #H3 #H @('bind_inversion H) -H #x1 #_ #H @('bind_inversion H) -H #lbl1 #_
     2170      cases pc in H2; #bl #z #H2 whd in match pc_of_point; normalize nodelta whd in ⊢ (??%? → ?);
     2171      #EQ destruct >H3 in H2; *
     2172    | #H3 lapply sigma_pc1_spec; whd in match sigma_pc_opt; normalize nodelta @if_elim
     2173     [#H >H in H3; *] #_ #EQ >EQ @('bind_inversion EQ) -EQ #x #x_spec
     2174     lapply(res_eq_from_opt ??? x_spec) -x_spec #x_spec #H @('bind_inversion H) * #lbl
     2175     #lbl_spec whd in match pc_of_point; normalize nodelta cases sigma_pc1 #bl1 #lbl1
     2176     whd in match (offset_of_point ??); whd in ⊢ (??%? → ?); #EQ destruct cases pc #bl2 #p2
     2177     #H @('bind_inversion H) -H #x1 #x1_spec lapply(res_eq_from_opt ??? x1_spec) -x1_spec #x1_spec
     2178     #H @('bind_inversion H) -H * #lbl2 #lbl2_spec
     2179     whd in match (offset_of_point ??); whd in ⊢ (??%? → ?); #EQ destruct
     2180     <lbl_spec in lbl2_spec; #EQsig >x_spec in x1_spec; whd in ⊢ (??%% → ?); #EQ destruct
     2181     lapply(partial_inj_sigma (ertl_to_ertlptr prog) sigma ???? EQsig)
     2182     [>EQsig >lbl_spec % #ABS destruct] whd in match point_of_pc; normalize nodelta
     2183     whd in match (point_of_offset ??); whd in match (point_of_offset ??);
     2184     #EQ destruct cases pc1 #bl #p %
     2185    ]
     2186  ]
     2187| #pc @mfr_return_eq1 %
     2188]
     2189qed.
     2190
     2191lemma pc_block_eq : ∀prog : ertl_program.
     2192let trans_prog ≝ ertl_to_ertlptr prog in
     2193∀sigma : sigma_map trans_prog.
     2194∀pc,id,fn.
     2195fetch_internal_function (joint_closed_internal_function ERTLptr
     2196  (prog_var_names (joint_function ERTLptr) ℕ trans_prog))
     2197  (globalenv_noinit (joint_function ERTLptr) trans_prog) (pc_block … pc) = return 〈id,fn〉→
     2198sigma fn (point_of_pc ERTL_semantics pc) ≠ None ? →
     2199 pc_block … pc = pc_block … (sigma_stored_pc trans_prog sigma pc).
     2200#prog #sigma * #bl #pos #id #fn #EQfn #EQlbl whd in match sigma_stored_pc;
     2201normalize nodelta whd in match sigma_pc_opt; normalize nodelta @if_elim [ #_ %]
     2202#_ >EQfn >m_return_bind >(opt_to_opt_safe … EQlbl) >m_return_bind %
     2203qed.
     2204                       
     2205
     2206 
     2207lemma eval_return_ok :
     2208∀prog : ertl_program.
     2209let trans_prog ≝ ertl_to_ertlptr prog in
     2210∀stack_sizes.
     2211∀sigma : sigma_map trans_prog.
     2212∀st,st',f,fn.
     2213 fetch_statement ERTL_semantics …
     2214  (globalenv_noinit ? prog) (pc … (sigma_state_pc ? sigma st)) =
     2215    return 〈f, fn,  final … (RETURN ERTL … )〉 →
     2216 eval_state ERTL_semantics
     2217   (prog_var_names (joint_function ERTL_semantics) ℕ prog)
     2218   (ev_genv … (mk_prog_params ERTL_semantics prog stack_sizes))
     2219   (sigma_state_pc ? sigma st) =
     2220  return st' →
     2221joint_classify (mk_prog_params ERTLptr_semantics trans_prog stack_sizes)
     2222  st = Some ? cl_return ∧
     2223∃ st''. st' = sigma_state_pc ? sigma st'' ∧
     2224∃st2_after_ret.
     2225∃taf : trace_any_any_free (ERTLptr_status trans_prog stack_sizes)
     2226st2_after_ret
     2227st''.
     2228(if taaf_non_empty … taf then
     2229  ¬as_costed (ERTLptr_status trans_prog stack_sizes)
     2230    st2_after_ret
     2231 else True) ∧
     2232eval_state … (ev_genv …  (mk_prog_params ERTLptr_semantics trans_prog stack_sizes)) st =
     2233return st2_after_ret ∧
     2234ret_rel ?? (ERTLptrStatusSimulation prog stack_sizes sigma) st' st2_after_ret.
     2235#prog #stack_size #sigma #st #st' #f #fn
     2236whd in match sigma_state_pc in ⊢ (% → ?); normalize nodelta
     2237@if_elim
     2238[ #EQbl whd in match dummy_state_pc; whd in match null_pc;
     2239  whd in match fetch_statement; whd in match fetch_internal_function;
     2240  normalize nodelta lapply(fetch_function_no_zero ??????)
     2241  [2: @( «mk_block Code OZ,refl region Code»)
     2242    | % | @prog |7: #EQ >EQ |*:]  whd in ⊢ (??%% → ?); #EQ destruct]
     2243#Hbl inversion(fetch_internal_function ???)
     2244[2: #e #_ normalize nodelta whd in match dummy_state_pc; whd in match null_pc;
     2245   whd in match fetch_statement; whd in match fetch_internal_function;
     2246  normalize nodelta lapply(fetch_function_no_zero ??????)
     2247  [2: @( «mk_block Code OZ,refl region Code»)
     2248    | % | @prog |7: #EQ >EQ |*:]  whd in ⊢ (??%% → ?); #EQ destruct]
     2249* #f1 #fn1 #EQ lapply(jmeq_to_eq ??? EQ) -EQ #fn1_spec normalize nodelta
     2250#EQf lapply EQf whd in match fetch_statement; normalize nodelta >fn1_spec
     2251>m_return_bind #H @('bind_inversion H) -H #stmt' #_ whd in ⊢ (??%% → ?);
     2252#EQ destruct whd in match sigma_state_pc in ⊢ (% → ?); normalize nodelta
     2253@if_elim [#H >H in Hbl; *] #_ >fn1_spec normalize nodelta
     2254whd in match eval_state; normalize nodelta >EQf >m_return_bind
     2255whd in match eval_statement_no_pc; whd in match eval_statement_advance;
     2256normalize nodelta >m_return_bind
     2257#H lapply (err_eq_from_io ????? H) -H #H @('bind_inversion H) -H
     2258* #st1 #pc1 #EQpop whd in match next_of_call_pc; normalize nodelta
     2259>m_bind_bind #H @('bind_inversion H) -H ** #f1 #fn2 * normalize nodelta
     2260[ * [ #c_id #args #dest | #r #lbl | #seq ] #nxt | #fin | * ]
     2261#EQf1 normalize nodelta [2,3,4: whd in ⊢ (??%% → ?); #EQ destruct]
     2262>m_return_bind whd in ⊢ (??%% → ?); #EQ destruct
     2263lapply (fetch_statement_commute prog sigma stack_size … EQf)
     2264normalize nodelta #EQf'
     2265% [ whd in match joint_classify; normalize nodelta >EQf' >m_return_bind %]
     2266cases(pop_ra_ok ? sigma  stack_size ??? EQpop) * #st3 #pc3 * #st3_spec
     2267normalize nodelta #EQ destruct whd in match set_last_pop; whd in match succ_pc;
     2268normalize nodelta whd in match (point_of_succ ???);
     2269 % [ % [ @st3 | @(pc_of_point ERTL_semantics (pc_block … pc3) nxt) | @pc3] ]
     2270 % [  @('bind_inversion EQf1) * #f3 #fn3 whd in match sigma_stored_pc;
     2271      normalize nodelta inversion(sigma_pc_opt ???) normalize nodelta
     2272      [ #_ #H @('bind_inversion H) -H #x whd in match null_pc; normalize nodelta
     2273        >fetch_function_no_zero [2: %] whd in ⊢ (???% → ?); #EQ destruct
     2274      | #pc4 whd in match sigma_pc_opt; normalize nodelta @if_elim
     2275        [ #bl3_spec @('bind_inversion EQf1) #x #H @('bind_inversion H) -H
     2276          #x1 >fetch_function_no_minus_one [ whd in ⊢ (???% → ?); #EQ destruct]
     2277          lapply bl3_spec @eqZb_elim #EQ * whd in match sigma_stored_pc;
     2278          normalize nodelta whd in match sigma_pc_opt; normalize nodelta
     2279           >bl3_spec normalize nodelta assumption
     2280        | #bl3_spec #H @('bind_inversion H) -H * #fn4 #id4
     2281          #H lapply(res_eq_from_opt ??? H) -H #fn4_spec
     2282          #H @('bind_inversion H) -H #lbl4 #lbl4_spec whd in ⊢ (??%? → ?); #EQ
     2283          destruct #fn3_spec #H @('bind_inversion H) -H #stmt1 #_
     2284          whd in ⊢ (??%% → ?); #EQ destruct
     2285          >(fetch_internal_function_transf … fn3_spec) in fn4_spec;
     2286          whd in ⊢ (??%% → ?); #EQ destruct
     2287        ]
     2288      ]
     2289      whd in match sigma_state_pc; normalize nodelta @if_elim
     2290      [ >(pc_block_eq prog sigma ????) in bl3_spec;
     2291       [2: >lbl4_spec % #ABS destruct
     2292       |3: >(fetch_internal_function_transf … fn3_spec) % |*:]
     2293       #bl3_spec whd in match pc_of_point; normalize nodelta #EQ >EQ in bl3_spec; *
     2294      | #_ inversion(fetch_internal_function ???) [#x #_ normalize nodelta % cases daemon (*serve lemma sul fetch della call *)
     2295        xxxxxxxxxxxxxxx
     2296            |
     2297 whd in match sigma_state_pc; normalize nodelta @if_elim
     2298   
     2299qed.
     2300
     2301lemma eval_tailcall_ok :
     2302∀prog.
     2303let trans_prog ≝ ertl_to_ertlptr prog in
     2304∀stack_sizes.
     2305∀sigma : sigma_map trans_prog.
     2306∀st,st',f,fn,fl,called,args.
     2307 fetch_statement ERTL_semantics …
     2308  (globalenv_noinit ? prog) (pc … (sigma_state_pc ? sigma st)) =
     2309    return 〈f, fn,  final … (TAILCALL ERTL … fl called args)〉 →
     2310 eval_state ERTL_semantics
     2311   (prog_var_names (joint_function ERTL_semantics) ℕ prog)
     2312   (ev_genv … (mk_prog_params ERTL_semantics prog stack_sizes))
     2313   (sigma_state_pc ? sigma st) =
     2314  return st' →
     2315  ∃ st''. st' = sigma_state_pc ? sigma st'' ∧
     2316  ∃is_tailcall, is_tailcall'.
     2317  joint_tailcall_ident (mk_prog_params ERTLptr_semantics trans_prog stack_sizes) «st, is_tailcall'» =
     2318  joint_tailcall_ident (mk_prog_params ERTL_semantics prog stack_sizes) «(sigma_state_pc ? sigma st), is_tailcall» ∧
     2319  eval_state … (ev_genv … (mk_prog_params ERTLptr_semantics trans_prog stack_sizes))
     2320    st = return st''.
     2321cases daemon
     2322qed.
     2323
     2324lemma eval_cond_ok :
     2325∀prog.
     2326let trans_prog ≝ ertl_to_ertlptr prog in
     2327∀stack_sizes.
     2328∀sigma : sigma_map trans_prog.
     2329∀st,st',f,fn,a,ltrue,lfalse.
     2330 fetch_statement ERTL_semantics …
     2331  (globalenv_noinit ? prog) (pc … (sigma_state_pc ? sigma st)) =
     2332    return 〈f, fn,  sequential … (COND ERTL … a ltrue) lfalse〉 →
     2333 eval_state ERTL_semantics
     2334   (prog_var_names (joint_function ERTL_semantics) ℕ prog)
     2335   (ev_genv … (mk_prog_params ERTL_semantics prog stack_sizes))
     2336   (sigma_state_pc ? sigma st) =
     2337  return st' →
     2338as_costed (ERTL_status prog stack_sizes)
     2339  st' →
     2340∃ st''. st' = sigma_state_pc ? sigma st'' ∧
     2341∃taf : trace_any_any_free (ERTLptr_status trans_prog stack_sizes)
     2342st st''.
     2343bool_to_Prop (taaf_non_empty … taf).
     2344cases daemon
     2345qed.
     2346 
    18802347       
    18812348inductive ex_Type1 (A:Type[1]) (P:A → Prop) : Prop ≝
     
    18832350(*interpretation "exists in Type[1]" 'exists x = (ex_Type1 ? x).*)
    18842351
    1885 lemma linearise_ok:
     2352lemma
     2353  find_funct_ptr_none:
     2354    ∀A,B,V,iV. ∀p: program A V. ∀transf: (∀vs. A vs → B vs).
     2355    ∀b: block.
     2356    find_funct_ptr ? (globalenv … iV p) b = None ? →
     2357    find_funct_ptr ? (globalenv … iV (transform_program … p transf)) b = None ?.
     2358#A #B #V #i #p #transf #b
     2359whd in match find_funct_ptr; normalize nodelta
     2360cases b -b * normalize nodelta [#x #_ %] * normalize nodelta
     2361[1,2: [2: #x] #_ %] #x whd in match globalenv; normalize nodelta
     2362whd in match globalenv_allocmem; normalize nodelta
     2363cases daemon (*forse e' falso *)
     2364qed.
     2365
     2366lemma as_label_ok : ∀ prog : ertl_program.
     2367let trans_prog ≝ ertl_to_ertlptr prog in
     2368∀ sigma : sigma_map trans_prog.
     2369∀stack_sizes.
     2370∀ st.
     2371as_label (ERTLptr_status trans_prog stack_sizes) st = as_label
     2372(ERTL_status prog stack_sizes) (sigma_state_pc prog sigma st).
     2373#prog #sigma #stack_size * #st #pc #lp
     2374whd in match as_label; normalize nodelta whd in match (as_pc_of ??) in ⊢ (??%%);
     2375whd in match (as_label_of_pc ??) in ⊢ (??%%);
     2376
     2377
     2378(*
     2379
     2380whd in match fetch_statement; normalize nodelta
     2381whd in match sigma_state_pc; normalize nodelta @if_elim
     2382[ #EQbl whd in match fetch_internal_function; normalize nodelta >m_bind_bind
     2383 lapply(fetch_function_no_minus_one ??????) [2: @(pc_block pc) | lapply EQbl
     2384 @eqZb_elim #H * @H| @(ertl_to_ertlptr prog) |7: #EQ >EQ |*:] normalize nodelta
     2385 whd in match dummy_state_pc; whd in match (as_label_of_pc ??); whd in match null_pc;
     2386 whd in match fetch_statement; normalize nodelta whd in match fetch_internal_function;
     2387 normalize nodelta >m_bind_bind
     2388 lapply(fetch_function_no_zero ??????) [2: @( «mk_block Code OZ,refl region Code»)
     2389 | % | @prog |7: #EQ >EQ |*:] %
     2390| inversion ( fetch_internal_function
     2391     (joint_closed_internal_function ERTL
     2392      (prog_var_names (joint_function ERTL) ℕ prog))
     2393     (globalenv_noinit (joint_function ERTL) prog) (pc_block pc))
     2394 [ * #id #fn #fn_spec #_ lapply(fetch_internal_function_transf ??????? fn_spec)
     2395   [ @(λvars,fn.translate_internal … fn) |] #EQ >EQ >m_return_bind normalize nodelta
     2396     whd in match (as_label_of_pc ??);
     2397     whd in match fetch_statement; normalize nodelta >fn_spec >m_return_bind
     2398     cases daemon (*serve specifica su sigma TODO*)
     2399   | #err #EQ lapply(jmeq_to_eq ??? EQ) -EQ #fetch_err #_ normalize nodelta
     2400     whd in match dummy_state_pc;
     2401     whd in match (as_label_of_pc ??); whd in match null_pc;
     2402     whd in match fetch_statement; normalize nodelta
     2403     whd in match fetch_internal_function in ⊢ (???%);
     2404     normalize nodelta
     2405     lapply(fetch_function_no_zero ??????) [2: @( «mk_block Code OZ,refl region Code»)
     2406     | % | @prog |7: #EQ >EQ in ⊢ (???%); |*:] normalize nodelta -EQ
     2407     lapply fetch_err -fetch_err whd in match fetch_internal_function; normalize nodelta
     2408     inversion(fetch_function ???)
     2409     [* #id * #fn #fn_spec >m_return_bind normalize nodelta [whd in ⊢ (??%? → ?); #EQ destruct]
     2410     #EQ destruct  lapply(jmeq_to_eq ??? fn_spec) -fn_spec #fn_spec
     2411     lapply(fetch_function_transf ????????? fn_spec) [ #v  @transf_fundef [2:@translate_internal |]|]
     2412     #EQ >EQ >m_return_bind %
     2413   | #err1 #EQ lapply(jmeq_to_eq ??? EQ) -EQ #EQfetch whd in ⊢ (??%? → ?); #EQ destruct
     2414     normalize nodelta lapply EQfetch -EQfetch whd in match fetch_function;
     2415     normalize nodelta check joint_function
     2416      lapply(symbol_for_block_transf  ? ? ? ? prog (λvars.?)  (pc_block pc))
     2417      [@transf_fundef [2: @translate_internal|] |4: #EQ >EQ in ⊢ (? → %); |*:] 
     2418     cases(symbol_for_block ???) [ whd in ⊢ (??%% → ?); #EQ destruct %]
     2419     #id >m_return_bind inversion(find_funct_ptr ???)
     2420     [2: #fn1 #_ >m_return_bind whd in ⊢ (??%? → ?); #EQ destruct]
     2421     #EQf whd in ⊢ (??%? → ?); #EQ destruct
     2422     lapply(find_funct_ptr_none ??????? EQf) (*forse e' falso*)
     2423     [#vars @transf_fundef [2: @translate_internal|]|]
     2424     #EQ >EQ %
     2425     ]
     2426  ]
     2427]*)
     2428cases daemon
     2429qed.
     2430
     2431
     2432lemma ertl_to_ertlptr_ok:
    18862433 ∀prog.
    18872434  let trans_prog ≝ ertl_to_ertlptr prog in
     
    18942441whd in match ERTL_status; whd in match ERTLptr_status; normalize nodelta
    18952442whd in ⊢ (% → % → % → % → ?); #st1 #st1' #st2
    1896 whd in match eval_state; normalize nodelta @('bind_inversion) ** #id #fn #stmt
    1897 #H lapply (err_eq_from_io ????? H) -H #EQfetch @('bind_inversion) #st #EQst
    1898 #EQst1' whd in match ERTLptrStatusSimulation; normalize nodelta
    1899 #EQsim whd in match joint_abstract_status in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ? ]);
    1900 normalize nodelta whd in match joint_classify; normalize nodelta >EQfetch
    1901 >m_return_bind cases stmt in EQst EQst1'; -stmt normalize nodelta
    1902 [ * [#called #c_arg #c_dest | #reg #lbl | #seq ] #succ_pc | #fin_step | (*FCOND absurd*) cases daemon]
    1903 [3: whd in match joint_classify_step; normalize nodelta whd in match eval_statement_no_pc;
    1904    normalize nodelta #H1 whd in match eval_statement_advance; normalize nodelta
    1905    whd in match set_no_pc; whd in match next; whd in match set_pc; normalize nodelta
    1906    #EQtobdest >EQsim in H1; #H1 cases(eval_seq_no_pc_no_call_ok ????????? H1)
    1907      [2: cases daemon (*TODO*)] #st' * #st_spec' #st_sim %
    1908          [% [ @st'| @(pc … st1') | @(last_pop … st1')]]
    1909          check taa_base
    1910          %{(taaf_step ???? (taa_base … st2) ? ?)}
    1911           [(*dalla commutazione del fetch TODO*) cases daemon
    1912           | whd in match (as_execute ???); whd in match eval_state; normalize nodelta
    1913            cases daemon (*dalla commutazione del fetch + st_spec' TODO *)
    1914           ] normalize nodelta % [% // cases daemon (*facile TODO *)] whd in match label_rel;
    1915            normalize nodelta (*specifica di sigma TODO *) cases daemon
    1916 |       
    1917    
    1918 
    1919 
    1920 >EQsim in EQfetch; whd in match sigma_state_pc in ⊢ (%→ ?);
    1921 whd in match fetch_statement; normalize nodelta #H @('bind_inversion H) -H
    1922 * #id1 #fn1 whd in match fetch_internal_function; normalize nodelta
    1923 #H @('bind_inversion H) -H * #id2 #fn2 @if_elim #block_st2_spec
    1924 [whd in match dummy_state_pc; whd in match null_pc; normalize nodelta
    1925  lapply(fetch_function_no_zero ??????)
    1926  [2: @(«mk_block Code OZ,refl region Code»)|%|@prog|7: #EQ >EQ |*:]
    1927  whd in ⊢ (???% → ?); #ABS destruct]
    1928  inversion(fetch_function
    1929           (fundef
    1930            (joint_closed_internal_function ERTLptr
    1931             (prog_var_names (joint_function ERTLptr) ℕ (ertl_to_ertlptr prog))))
    1932           (globalenv_noinit (joint_function ERTLptr) (ertl_to_ertlptr prog))
    1933           (pc_block (pc ERTLptr_semantics st2)))
    1934 [2: #err #_ normalize nodelta whd in match dummy_state_pc; whd in match null_pc; normalize nodelta
    1935  lapply(fetch_function_no_zero ??????)
    1936  [2: @(«mk_block Code OZ,refl region Code»)|%|@prog|7: #EQ >EQ |*:]
    1937  whd in ⊢ (???% → ?); #ABS destruct] * #id3 #fn3 #EQ  lapply(jmeq_to_eq ??? EQ) -EQ
    1938  #EQffst2 >m_return_bind cases fn3 in EQffst2; -fn3 [2: #ext #_ normalize nodelta
    1939  whd in match dummy_state_pc; whd in match null_pc; normalize nodelta
    1940  lapply(fetch_function_no_zero ??????)
    1941  [2: @(«mk_block Code OZ,refl region Code»)|%|@prog|7: #EQ >EQ |*:]
    1942  whd in ⊢ (???% → ?); #ABS destruct] #fn3 #fn3_spec normalize nodelta
    1943  #fn2_spec >(fetch_function_transf ??????????) in fn3_spec; [2: @fn2_spec|*:]
    1944  cases fn2 in fn2_spec; -fn2 #fn2 #fn2_spec whd in match transf_fundef;
    1945  normalize nodelta whd in ⊢ (??%? → ?); #EQ destruct whd in ⊢ (??%% → ?); #EQ destruct
    1946  #H @('bind_inversion H) -H #stmt1 #H lapply(opt_eq_from_res ???? H) -H #stmt1_spec
    1947  whd in ⊢ (??%% → ?); #EQ destruct cases stmt in stmt1_spec EQst1' EQst; -stmt
    1948  [* [#called #c_arg #c_dest | #reg #lbl | #seq ] #succ_pc | #fin_step | (*FCOND absurd*) cases daemon]
    1949  #stmt_spec whd in match eval_statement_advance; normalize nodelta whd in match eval_call;
    1950  normalize nodelta #EQst1' whd in match eval_statement_no_pc; normalize nodelta
    1951 [3: #H cases(eval_seq_no_pc_no_call_ok ????????? H) [2: whd in match fetch_internal_function;
    1952     normalize nodelta whd in match sigma_state_pc; normalize nodelta @if_elim
    1953     [ #H1 >H1 in block_st2_spec; *] #_ whd in match fetch_internal_function; normalize nodelta
    1954     >(fetch_function_transf ??????????) [2: @fn2_spec |*: ] whd in match transf_fundef;
    1955     normalize nodelta >fn2_spec >m_return_bind %] #st3 * #st3_spec #sem_rel
    1956     % [ % [ @st3 | @(pc … st1') | @(last_pop … st2)]] % [%2 [2: %1|1:|4: whd in match as_classifier; normalize nodelta whd in match (as_classify ??); normalize nodelta
    1957    
    1958     %{(taaf_step … (taa_base …) …) I}
    1959  
    1960  
    1961  [1,2,4: whd in ⊢ (??%% → ?); #EQ destruct
    1962  |3: whd in EQst1' : (??%%); whd in match set_no_pc in EQst1'; normalize nodelta in EQst1';
    1963     whd in match sigma_state_pc in EQst1'; normalize nodelta in EQst1';
    1964     >block_st2_spec in EQst1'; @if_elim [ #H >H in block_st2_spec; *] #_
    1965     whd in match fetch_internal_function; normalize nodelta >(fetch_function_transf ??????????) [2: @fn2_spec|*:]
    1966     >m_return_bind whd in match transf_fundef; normalize nodelta whd in match next;
    1967     normalize nodelta whd in match set_pc; normalize nodelta #EQ destruct #H
    1968 
    1969    
    1970 
    1971    
    1972     whd ;in match  in EQst1';
    1973     destruct #EQst
    1974  #EQst normalize nodelta
    1975  [ whd in match joint_classify_step; normalize nodelta
    1976  
    1977  
    1978  
    1979  lapply(fetch_function_no_zero ??????) [2: @(«mk_block Code OZ,refl region Code»)
    1980  |2: % | %|7: #EQ >EQ *: try assumption
    1981 
    1982  normalize in ⊢ (%→ ?);
    1983 normalize in as_ex;
    1984 
    1985 
    1986 
     2443change with
     2444  (eval_state ERTL_semantics (prog_var_names ???) ?? = ? → ?)
     2445#EQeval @('bind_inversion EQeval)
     2446** #id #fn #stmt #H lapply (err_eq_from_io ????? H) -H #EQfetch
     2447#_  whd in match ERTLptrStatusSimulation; normalize nodelta #EQst2 destruct
     2448cases stmt in EQfetch; -stmt
     2449[ * [#called #c_arg #c_dest | #reg #lbl | #seq ] #succ_pc | #fin_step | *]
     2450normalize nodelta #EQfetch
     2451change with (joint_classify ??) in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ? ]);
     2452[ (*CALL*)
     2453  cases daemon (*TODO*)
     2454| whd in match joint_classify; normalize nodelta
     2455 >EQfetch in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ? ]);
     2456  normalize nodelta
     2457 #n_cost
     2458 cases (eval_cond_ok … EQfetch EQeval n_cost)
     2459 #st3 * #EQ destruct * #taf #tafne %{st3} %{taf}
     2460 % [ % [2: %] >tafne normalize nodelta @I] whd >as_label_ok %
     2461| whd in match joint_classify; normalize nodelta
     2462 >EQfetch in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ? ]);
     2463  normalize nodelta
     2464  cases (eval_seq_no_call_ok ?????????  EQfetch EQeval)
     2465  #st3 * #EQ destruct *  #taf #tafne %{st3} %{taf} >tafne normalize nodelta
     2466  % [% //] whd >as_label_ok [2:assumption] %
     2467| (*FIN*)
     2468  cases fin_step in EQfetch;
     2469  [ (*GOTO*) #lbl #EQfetch  whd in match joint_classify; normalize nodelta
     2470  >EQfetch in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ? ]); normalize nodelta
     2471    cases (eval_goto_ok … EQfetch EQeval)
     2472    #st3 * #EQ destruct * #taf #tarne %{st3} %{taf} >tarne normalize nodelta
     2473    % [% //] whd >as_label_ok [2:assumption] %
     2474  | (*RETURN*) #EQfetch
     2475     whd in match joint_classify; normalize nodelta
     2476    >EQfetch in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ? ]); normalize nodelta
     2477    cases (eval_return_ok … EQfetch EQeval) #is_ret
     2478    * #st3 * #EQ destruct * #after_ret * #taf ** #taf_prf #EQeval' #ret_prf
     2479    % [2: % [2: % [2: %{(taa_base …)} %{taf}] |*: ] |*:]
     2480    % [2: whd >as_label_ok %] % [2: assumption] % [2: %] % [2: assumption]
     2481    % assumption
     2482  | (*TAILCALL*) #fl #called #args #EQfetch
     2483    cases (eval_tailcall_ok … EQfetch EQeval) #st3 * #EQ destruct * #is_tailcall
     2484    * #is_tailcall' *  #eq_call #EQeval' >is_tailcall normalize nodelta
     2485    #prf  %{«?, is_tailcall'»} %{eq_call}
     2486    % [2: % [2: %{(taa_base …)} %{(taa_base …)}  % [ %{EQeval'} % |] | ] | ]
     2487    whd >as_label_ok %
     2488  ]
     2489]
     2490qed.
     2491
     2492
     2493
  • src/joint/semantics.ma

    r2590 r2592  
    7777  mk_program_counter «mk_block Code (-1), refl …» one.
    7878
    79 definition null_pc : program_counter ≝
    80     mk_program_counter «mk_block Code OZ, refl …» one.
     79definition null_pc : Pos →  program_counter ≝ λpos.
     80    mk_program_counter «mk_block Code OZ, refl …» pos.
    8181
    8282definition set_m: ∀p. bemem → state p → state p ≝
Note: See TracChangeset for help on using the changeset viewer.