Changeset 2845


Ignore:
Timestamp:
Mar 11, 2013, 6:50:48 PM (4 years ago)
Author:
piccolo
Message:

ERTLptr to LTL correctness proof started

Location:
src
Files:
4 edited

Legend:

Unmodified
Added
Removed
  • src/ERTL/ERTLtoERTLptrUtils.ma

    r2843 r2845  
    10261026qed.
    10271027
     1028
     1029(*TO BE MOVED : GENERAL!!!*)
    10281030lemma pc_of_label_eq :
    10291031  ∀p,p'.let pars ≝ mk_sem_graph_params p p' in
  • src/ERTLptr/ERTLptrToLTLProof.ma

    r2796 r2845  
    44include "joint/Traces.ma".
    55include "common/StatusSimulation.ma".
    6 
    7 definition stacksizes_from_model : stack_cost_model → (ident → option ℕ) ≝
    8 λm,id.find ??
    9   (λid_stack.let 〈id', stack〉 ≝ id_stack in
    10     if id' == id then Some ? stack else None ?) m.
    11 
    12 axiom ERTLptrToLTL_ok :
     6include "common/AssocList.ma".
     7
     8
     9
     10(* Inefficient, replace with Trie lookup *)
     11definition lookup_stack_cost ≝
     12 λp.λid : ident.
     13  assoc_list_lookup ? ℕ id (eq_identifier …) p.
     14
     15(*TO BE MOVED*)
     16definition ERTLptr_status ≝
     17λprog : ertlptr_program.λstack_sizes.
     18joint_abstract_status (mk_prog_params ERTLptr_semantics prog stack_sizes).
     19
     20definition LTL_status ≝
     21λprog : ltl_program.λstack_sizes.
     22joint_abstract_status (mk_prog_params LTL_semantics prog stack_sizes).
     23
     24axiom sigma_stored_pc : ertlptr_program → (block → label → list label) → 
     25program_counter → program_counter.
     26
     27axiom sigma_fb_state: ertlptr_program → (block → label → list label) →
     28 (block → label → list register) → list register →
     29  state ERTLptr_semantics → state ERTLptr_semantics.
     30
     31axiom sigma_sb_state: ertlptr_program → (block → label → list label) →
     32 (block → label → list register) → list register →
     33  state LTL_semantics → state ERTLptr_semantics.
     34
     35definition dummy_state : state ERTLptr_semantics ≝
     36mk_state ERTL_semantics
     37   (None ?) empty_is BBundef 〈empty_map ? ?,mk_hw_register_env … (Stub …) BBundef〉 empty.
     38
     39definition dummy_state_pc : state_pc ERTLptr_semantics ≝
     40mk_state_pc ? dummy_state (null_pc one) (null_pc one).
     41
     42
     43definition sigma_fb_state_pc : ertlptr_program → (block → label → list label) →
     44 (block → label → list register) →
     45 state_pc ERTLptr_semantics → state_pc ERTLptr_semantics ≝
     46λprog,f_lbls,f_regs,st.
     47let ge ≝ globalenv_noinit … prog in
     48let globals ≝ prog_var_names … prog in
     49match fetch_internal_function … ge (pc_block (pc … st)) with
     50  [ OK y ⇒ ?
     51  | Error e ⇒ dummy_state_pc
     52  ].
     53cases daemon qed.
     54
     55definition sigma_sb_state_pc : ertlptr_program → (block → label → list label) →
     56 (block → label → list register) → state_pc LTL_semantics → state_pc ERTLptr_semantics ≝
     57λprog,f_lbls,f_regs,st.
     58let ge ≝ globalenv_noinit … prog in
     59let globals ≝ prog_var_names … prog in
     60match fetch_internal_function … ge (pc_block (pc … st)) with
     61  [ OK y ⇒ ?
     62  | Error e ⇒ dummy_state_pc
     63  ].
     64cases daemon qed.
     65
     66
     67definition ERTLptr_to_LTL_StatusSimulation :
     68∀fix_comp : fixpoint_computer.
     69∀colour : coloured_graph_computer.
     70∀ prog : ertlptr_program.
     71∀ f_lbls. ∀ f_regs. ∀f_bl_r.
     72∀p_out,m,n.
     73ertlptr_to_ltl fix_comp colour prog = 〈p_out, m, n〉 →
     74let stacksizes ≝ lookup_stack_cost … m in
     75b_graph_transform_program_props ERTLptr_semantics LTL_semantics
     76     (λglobals,fn.«translate_data fix_comp colour globals fn,(refl …)») prog f_bl_r f_lbls f_regs →
     77status_rel (ERTLptr_status prog stacksizes) (LTL_status p_out stacksizes) ≝
     78λfix_comp,colour,prog,f_lbls,f_regs,f_bl_r,p_out,m,n,EQ.
     79λgood.
     80    mk_status_rel ??
     81    (* sem_rel ≝ *) (λs1:ERTLptr_status prog ?.
     82       λs2: LTL_status ? ?.
     83        sigma_fb_state_pc prog f_lbls f_regs s1 = sigma_sb_state_pc prog f_lbls f_regs s2)
     84    (* call_rel ≝ *) 
     85       (λs1:Σs.as_classifier … s cl_call.
     86        λs2:Σs.as_classifier … s cl_call.
     87         pc … s1 =sigma_stored_pc prog f_lbls (pc … s2))
     88    (* sim_final ≝ *) ?.
     89cases daemon
     90qed.
     91
     92axiom as_label_ok :
     93∀fix_comp,colour.
     94∀prog.
     95∀p_out,m,n.
     96∀EQp_out: ertlptr_to_ltl fix_comp colour prog = 〈p_out, m, n〉.
     97∀f_lbls,f_regs.
     98∀f_bl_r.
     99∀ good :b_graph_transform_program_props ERTLptr_semantics LTL_semantics
     100     (λglobals,fn.«translate_data fix_comp colour globals fn,(refl …)») prog f_bl_r f_lbls f_regs.
     101∀st1,st2,fn,id,stmt.
     102let stack_sizes ≝ lookup_stack_cost m in
     103let R ≝ sem_rel … (ERTLptr_to_LTL_StatusSimulation fix_comp colour … EQp_out … good) in
     104R st1 st2 →
     105fetch_statement ERTLptr_semantics (prog_var_names … prog)
     106      (globalenv_noinit … prog) (pc … st1) = return 〈id,fn,stmt〉 →
     107as_label (LTL_status p_out stack_sizes) st2 =
     108 as_label (ERTLptr_status prog stack_sizes) st1.
     109
     110
     111
     112(*
     113(* Copy the proof too from previous pass *)
     114axiom fetch_stmt_ok_sigma_state_ok :
     115∀prog : ertlptr_program.
     116∀ f_lbls,f_regs,id,fn,stmt,st.
     117fetch_statement ERTLptr_semantics (prog_var_names … prog)
     118    (globalenv_noinit … prog) (pc ? (sigma_sb_state_pc prog f_lbls f_regs st)) =
     119               return 〈id,fn,stmt〉 →
     120let added ≝ (added_registers ERTLptr (prog_var_names … prog) fn
     121                                               (f_regs (pc_block (pc … st)))) in
     122st_no_pc … (sigma_sb_state_pc prog f_lbls f_regs st) =
     123sigma_sb_state prog f_lbls f_regs added (st_no_pc … st).
     124*)
     125
     126lemma set_no_pc_eta:
     127 ∀P.∀st1: state_pc P. set_no_pc P st1 st1 = st1.
     128#P * //
     129qed.
     130
     131lemma pc_of_label_eq :
     132  ∀p,p'.let pars ≝ mk_sem_graph_params p p' in
     133  ∀globals,ge,bl,i_fn,lbl.
     134  fetch_internal_function ? ge bl = return i_fn →
     135  pc_of_label pars globals ge bl lbl =
     136    OK ? (pc_of_point ERTL_semantics bl lbl).
     137#p #p' #globals #ge #bl #i_fn #lbl #EQf
     138whd in match pc_of_label;
     139normalize nodelta >EQf >m_return_bind %
     140qed.
     141
     142lemma eq_OK_OK_to_eq: ∀T,x,y. OK T x = OK T y → x=y.
     143 #T #x #y #EQ destruct %
     144qed.
     145
     146
     147axiom pc_block_eq_sigma_commute : ∀fix_comp,colour.
     148∀prog.
     149∀p_out,m,n.
     150∀EQp_out: ertlptr_to_ltl fix_comp colour prog = 〈p_out, m, n〉.
     151∀ f_lbls,f_regs.
     152∀f_bl_r.
     153∀ good :b_graph_transform_program_props ERTLptr_semantics LTL_semantics
     154     (λglobals,fn.«translate_data fix_comp colour globals fn,(refl …)») prog f_bl_r f_lbls f_regs.
     155∀st1,st2.
     156let stack_sizes ≝ lookup_stack_cost m in
     157let R ≝ sem_rel … (ERTLptr_to_LTL_StatusSimulation fix_comp colour … EQp_out … good) in
     158R st1 st2 →
     159pc_block (pc … st1) = pc_block (pc … st2).
     160
     161axiom change_pc_sigma_commute : ∀fix_comp,colour.
     162∀prog.
     163∀p_out,m,n.
     164∀EQp_out: ertlptr_to_ltl fix_comp colour prog = 〈p_out, m, n〉.
     165∀ f_lbls,f_regs.
     166∀f_bl_r.
     167∀ good :b_graph_transform_program_props ERTLptr_semantics LTL_semantics
     168     (λglobals,fn.«translate_data fix_comp colour globals fn,(refl …)») prog f_bl_r f_lbls f_regs.
     169∀st1,st2.
     170let stack_sizes ≝ lookup_stack_cost m in
     171let R ≝ sem_rel … (ERTLptr_to_LTL_StatusSimulation fix_comp colour … EQp_out … good) in
     172R st1 st2 →
     173∀pc1,pc2.pc1 = pc2 →
     174R (set_pc … pc1 st1) (set_pc … pc2 st2).
     175
     176axiom globals_commute : ∀fix_comp,colour.
     177∀prog.
     178∀p_out,m,n.
     179∀EQp_out: ertlptr_to_ltl fix_comp colour prog = 〈p_out, m, n〉.
     180prog_var_names … prog = prog_var_names … p_out.
     181
     182include "joint/semantics_blocks.ma".
     183include "ASM/Util.ma".
     184
     185lemma eval_cond_ok :
     186∀fix_comp,colour.
     187∀prog.
     188∀p_out,m,n.
     189∀EQp_out: ertlptr_to_ltl fix_comp colour prog = 〈p_out, m, n〉.
     190∀ f_lbls,f_regs.
     191∀f_bl_r.
     192∀ good :b_graph_transform_program_props ERTLptr_semantics LTL_semantics
     193     (λglobals,fn.«translate_data fix_comp colour globals fn,(refl …)») prog f_bl_r f_lbls f_regs.
     194∀st1,st2,st1',f,fn,a,ltrue,lfalse.
     195let stack_sizes ≝ lookup_stack_cost m in
     196let R ≝ sem_rel … (ERTLptr_to_LTL_StatusSimulation fix_comp colour … EQp_out … good) in
     197R st1 st2 →
     198 fetch_statement ERTLptr_semantics …
     199  (globalenv_noinit ? prog) (pc … st1) =
     200    return 〈f, fn,  sequential … (COND ERTLptr … a ltrue) lfalse〉 →
     201 eval_state ERTLptr_semantics
     202   (prog_var_names … ℕ prog)
     203   (ev_genv … (mk_prog_params ERTLptr_semantics prog stack_sizes))
     204   st1 = return st1' →
     205as_costed (ERTLptr_status prog stack_sizes) st1' →
     206∃ st2'. R st1' st2' ∧
     207∃taf : trace_any_any_free (LTL_status p_out stack_sizes)
     208st2 st2'.
     209bool_to_Prop (taaf_non_empty … taf).
     210#fix_comp #colour #prog #transf_prog #stack_size #maxstack #EQtransf_prog
     211#f_lbls #f_regs #f_bl_r #good #st1 #st2 #st1' #f #fn #a #ltrue #lfalse
     212#Rst1st2
     213#EQfetch whd in match eval_state; normalize nodelta >EQfetch >m_return_bind
     214whd in match eval_statement_no_pc; normalize nodelta >m_return_bind
     215whd in match eval_statement_advance; normalize nodelta
     216change with (ps_reg_retrieve ??) in match (acca_retrieve ?????);
     217#H lapply(err_eq_from_io ????? H) -H #H @('bind_inversion H) -H
     218#bv >set_no_pc_eta
     219#EQbv #H @('bind_inversion H) -H * #EQbool normalize nodelta
     220 lapply(fetch_statement_inv … EQfetch) * #EQfn #_
     221[ whd in match goto; normalize nodelta >(pc_of_label_eq ??????? EQfn) >m_return_bind
     222| whd in match next; normalize nodelta
     223]
     224whd in ⊢ (??%% → ?); #EQ <(eq_OK_OK_to_eq ??? EQ) -EQ -st1'
     225#n_cost
     226cases(b_graph_transform_program_fetch_statement … good … EQfetch)
     227#init_data * #t_fn1 ** #EQt_fn1 whd in ⊢ (% → ?); cases (f_bl_r ?) normalize nodelta
     228[2,4: #r #tl *] #EQ >EQ -init_data >if_merge_right in ⊢ (% → ?); [2,4: %] * #labs **
     229[2,4: #hd #tl ** #_ #_ *** #pre #inst #post * whd in ⊢ (%→?); *] ** #EQlabs #EQf_regs
     230whd in match translate_step; normalize nodelta * #bl *
     231whd in ⊢ (% → ?); inversion (〈?,?〉) * #blp #blm #bls #EQ #EQbl >EQbl -bl
     232letin p≝ (mk_prog_params LTL_semantics (\fst (\fst (ertlptr_to_ltl fix_comp colour prog))) (lookup_stack_cost stack_size))
     233whd in ⊢ (% → ?); * #l1 * #mid1 * #mid2 * #l2 *** #EQmid1 whd in ⊢ (% → ?); #seq_pre_l
     234cases(? : ∃st2'.repeat_eval_seq_no_pc p f (map_eval ?? blp mid1) (st_no_pc … st2) = return (st_no_pc … st2') ∧
     235           pc … st2' = (pc_of_point ERTLptr_semantics (pc_block (pc … st2)) mid1) ∧
     236           last_pop … st2' = last_pop … st2)
     237   [2,4: cases daemon (* THE EXTENSIONAL PROOF *) ]
     238#st2_pre_cond ** #res_st2_pre_cond #EQpc_st2_pre_cond #EQlast_pop_st2_pre_cond
     239>(pc_block_eq_sigma_commute … EQtransf_prog … good … Rst1st2) in EQt_fn1; #EQt_fn1
     240
     241xxxxxxxxxxxxxxxxxxxxxxxxxxxx
     242
     243lapply(taaf_to_taa ???
     244    (produce_trace_any_any_free p st2 f t_fn1 ??? st2_pre_cond EQt_fn1 seq_pre_l res_st2_pre_cond) ?)
     245 
     246   @(map_eval ??? mid1) lapply blp whd in match p; normalize nodelta
     247   whd in match (globals ?); whd in match prog_var_names; normalize nodelta
     248   change with (prog_var_names ??) in match (globals ??);
     249
     250lapply(produce_trace_any_any_free p st2 ?????
     251
     252
     253%{(set_pc … (pc_of_point ERTLptr_semantics (pc_block (pc … st2)) ?) st2)}
     254[ @ltrue |3: @lfalse]
     255% [1,3: @(change_pc_sigma_commute … EQtransf_prog … good … Rst1st2)
     256        <(pc_block_eq_sigma_commute … EQtransf_prog … good … Rst1st2) %]
     257
     258
     259
     260 -bl whd in ⊢ (% → ?); * #l1 * #mid1 * #mid2 * #l2
     261*** #EQmid1 whd in ⊢ (% → ?); #seq_pre_l * #EQ1 #EQ2 destruct(EQ1 EQ2) whd in ⊢ (% → ?); *
     262#nxt1 * #EQcond #EQ destruct(EQ) whd in ⊢ (% → ?); * #EQ1 #EQ2 destruct(EQ1 EQ2)
     263whd in EQmid1 : (??%%); destruct(EQmid1)
     264%{(taaf_step_jump … (taa_base …) …) I}
     265[2,5: whd whd in ⊢ (??%?); whd in match fetch_statement; normalize nodelta 
     266      <(fetch_stmt_ok_sigma_pc_ok … EQfetch) >EQt_fn1 >m_return_bind
     267      >EQcond %
     268|3,6: whd whd in match eval_state; normalize nodelta whd in match eval_statement_no_pc;
     269      normalize nodelta whd in match fetch_statement; normalize nodelta
     270      <(fetch_stmt_ok_sigma_pc_ok … EQfetch) >EQt_fn1 >m_return_bind
     271      >EQcond >m_return_bind normalize nodelta >m_return_bind
     272      whd in match eval_statement_advance; normalize nodelta
     273      change with (ps_reg_retrieve ??) in match (acca_retrieve ?????);
     274      cases(ps_reg_retrieve_ok … EQbv) #bv1 * #EQbv1 #EQsem >EQbv1
     275      >m_return_bind >EQsem in EQbool; #EQbool cases(bool_of_beval_ok … EQbool)
     276      #bool1 * #EQbool1 #EQ destruct(EQ) >EQbool1 >m_return_bind normalize nodelta
     277      >(fetch_stmt_ok_sigma_pc_ok … EQfetch) [2: %] whd in match goto;
     278      normalize nodelta >(fetch_stmt_ok_sigma_pc_ok … EQfetch) in EQt_fn1; #EQt_fn1
     279      >(pc_of_label_eq … EQt_fn1) >m_return_bind %
     280|*: lapply n_cost whd in match as_costed; normalize nodelta
     281    [ cut((mk_state_pc ERTL_semantics
     282   (sigma_state prog f_lbls f_regs
     283    (added_registers ERTL (prog_var_names (joint_function ERTL) ℕ prog) fn
     284     (f_regs (pc_block (pc ERTLptr_semantics st2)))) st2)
     285   (pc_of_point ERTL_semantics (pc_block (pc ERTLptr_semantics st2)) ltrue)
     286   (sigma_stored_pc prog f_lbls (last_pop ERTLptr_semantics st2))) =
     287   sigma_state_pc prog f_lbls f_regs (mk_state_pc ERTLptr_semantics st2
     288    (pc_of_point ERTLptr_semantics (pc_block (pc ERTLptr_semantics st2)) ltrue)
     289    (last_pop ERTLptr_semantics st2))) [ whd in match sigma_state_pc; normalize  nodelta
     290    >(fetch_stmt_ok_sigma_pc_ok … EQfetch) in EQfn; #EQfn >EQfn %]
     291    #EQ >EQ >(as_label_ok … good … (mk_state_pc ERTLptr_semantics st2
     292    (pc_of_point ERTLptr_semantics (pc_block (pc ERTLptr_semantics st2)) ltrue)
     293    (last_pop ERTLptr_semantics st2))) [#H @H] cases daemon (*needs lemma see below *)
     294    | cut((mk_state_pc ERTL_semantics
     295   (sigma_state prog f_lbls f_regs
     296    (added_registers ERTL (prog_var_names (joint_function ERTL) ℕ prog) fn
     297     (f_regs (pc_block (pc ERTLptr_semantics st2)))) st2)
     298   (succ_pc ERTL_semantics (pc ERTLptr_semantics st2)
     299    (point_of_succ ERTLptr_semantics
     300     (point_of_pc ERTLptr_semantics
     301      (pc ERTL_semantics (sigma_state_pc prog f_lbls f_regs st2))) nxt1))
     302   (sigma_stored_pc prog f_lbls (last_pop ERTLptr_semantics st2))) =
     303   sigma_state_pc prog f_lbls f_regs (mk_state_pc ERTLptr_semantics st2
     304    (pc_of_point ERTLptr_semantics (pc_block (pc ERTLptr_semantics st2))
     305     (point_of_succ ERTLptr_semantics
     306      (point_of_pc ERTLptr_semantics
     307       (pc ERTL_semantics (sigma_state_pc prog f_lbls f_regs st2))) nxt1))
     308    (last_pop ERTLptr_semantics st2))) [ whd in match sigma_state_pc; normalize  nodelta
     309    >(fetch_stmt_ok_sigma_pc_ok … EQfetch) in EQfn; #EQfn >EQfn %] #EQ >EQ
     310    >(as_label_ok … good … (mk_state_pc ERTLptr_semantics st2
     311    (pc_of_point ERTLptr_semantics (pc_block (pc ERTLptr_semantics st2))
     312     (point_of_succ ERTLptr_semantics
     313      (point_of_pc ERTLptr_semantics
     314       (pc ERTL_semantics (sigma_state_pc prog f_lbls f_regs st2))) nxt1))
     315    (last_pop ERTLptr_semantics st2))) [#H @H] cases daemon (*needs lemma see below ! *)
     316]
     317qed.*)
     318
     319
     320theorem ERTLptrToLTL_ok :
    13321∀fix_comp : fixpoint_computer.
    14322∀colour : coloured_graph_computer.
     
    16324let 〈p_out, m, n〉 ≝ ertlptr_to_ltl fix_comp colour p_in in
    17325(* what should we do with n? *)
    18 let stacksizes ≝ stacksizes_from_model m in
     326let stacksizes ≝ lookup_stack_cost m in
    19327∃[1] R.
    20328  status_simulation
     
    22330    (joint_status LTL_semantics p_out stacksizes)
    23331    R.
     332#fix_comp #colour #p_in
     333@pair_elim * #p_out #m #n #EQp_out whd
     334cases(make_b_graph_transform_program_props ERTLptr_semantics LTL_semantics
     335          (λglobals,fn.«translate_data fix_comp colour globals fn,(refl …)») p_in)
     336#fregs * #f_lbls * #f_bl_r #good
     337%{(ERTLptr_to_LTL_StatusSimulation … EQp_out … good)}
     338whd in match status_simulation; normalize nodelta
     339whd in match ERTLptr_status; whd in match LTL_status; normalize nodelta
     340whd in ⊢ (% → % → % → % → ?); #st1 #st1' #st2
     341change with
     342  (eval_state ERTLptr_semantics (prog_var_names ???) ?? = ? → ?) 
     343#EQeval @('bind_inversion EQeval)
     344** #id #fn #stmt #H lapply (err_eq_from_io ????? H) -H #EQfetch
     345#_  whd in match ERTLptr_to_LTL_StatusSimulation; normalize nodelta #EQst2
     346cases stmt in EQfetch; -stmt
     347[ * [ #cost | #called_id #args #dest| #reg #lbl | #seq] #nxt | #fin_step | *]
     348#EQfetch
     349change with (joint_classify ??) in
     350                     ⊢ (match % with [ _ ⇒ ? | _ ⇒ ? | _ ⇒ ? | _ ⇒ ? | _ ⇒ ? ]);
     351[ (*COST*) whd in match joint_classify; normalize nodelta >EQfetch normalize nodelta
     352  (* XXX
     353  cases(eval_cost_ok … good … EQfetch EQeval) #st2' * #EQst2' * #taf #tafne
     354  %{st2'} %{taf} >tafne normalize nodelta % [ % [@I | assumption]]
     355  whd >EQst2' >(as_label_ok … good … st2') [%] cases daemon (* needs lemma see below!! *)
     356  *) cases daemon
     357| (*CALL*)  whd in match joint_classify; normalize nodelta >EQfetch
     358          normalize nodelta #is_call_st1
     359          (* XXX
     360          cases(eval_call_ok … good … EQfetch EQeval) #is_call_st1'
     361          * #st2_pre_call * #is_call_st2_pre_call * * #Hcall
     362          #call_rel * #taa * #st2' * #sem_rel #eval_rel
     363          %{(«st2_pre_call,is_call_st2_pre_call»)} % [ % assumption]
     364          %{st2'} %{st2'} %{taa} %{(taa_base …)} % [ % assumption]
     365          whd >sem_rel >(as_label_ok … good … st2') [%] cases daemon (*TODO*)
     366          *) cases daemon
     367| (*COND*) whd in match joint_classify; normalize nodelta >EQfetch
     368          normalize nodelta #n_costed
     369          cases(eval_cond_ok … EQp_out … good … EQst2 … EQfetch EQeval … n_costed)
     370          #st2' * #EQst2' * #taf #tafne %{st2'} %{taf} >tafne % [% [@I|assumption]]
     371          whd >EQst2' >(as_label_ok fix_comp colour … EQp_out … good … EQst2') [%] cases daemon (*TODO*)
     372| (*seq*) XXX whd in match joint_classify; normalize nodelta >EQfetch
     373          normalize nodelta
     374          cases (eval_seq_no_call_ok … good … EQfetch EQeval)
     375          #st3 * #EQ destruct *  #taf #taf_spec %{st3} %{taf} 
     376          % [% //] whd >(as_label_ok … good … st3) [%]
     377          cases daemon (*needs lemma about preservation of fetch_statement *)
     378|  cases fin_step in EQfetch;
     379  [ (*GOTO*) #lbl #EQfetch  whd in match joint_classify; normalize nodelta
     380     >EQfetch normalize nodelta
     381    cases (eval_goto_ok … good  … EQfetch EQeval)
     382    #st3 * #EQ destruct * #taf #tarne %{st3} %{taf} >tarne normalize nodelta
     383    % [% //] whd >(as_label_ok … good … st3) [%]
     384    cases daemon (*needs lemma about preservation of fetch_statement *)
     385  | (*RETURN*) #EQfetch
     386     whd in match joint_classify; normalize nodelta
     387    >EQfetch  normalize nodelta
     388    cases (eval_return_ok … good … EQfetch EQeval) #is_ret
     389    * #st3 * #EQ destruct * #after_ret * #taf ** #taf_prf #EQeval' #ret_prf
     390    % [2: % [2: % [2: %{(taa_base …)} %{taf}] |*: ] |*:]
     391    % [2: whd >(as_label_ok … good … st3) [%] cases daemon (*needs lemma *)]
     392    % [2: assumption] % [2: %] % [2: assumption] % assumption
     393  | (*TAILCALL*) *
     394  ]
     395]
     396
  • src/ERTLptr/Interference.ma

    r2739 r2845  
    1313{ colouring: vertex → decision
    1414; spilled_no: nat
    15 ; prop_colouring: ∀l. ∀v1, v2: vertex.
     15; prop_colouring: ∀l. ∀v1, v2: vertex.v1 ≠v2 →
    1616  lives v1 (after l) → lives v2 (after l) → colouring v1 ≠ colouring v2
    1717; prop_spilled_no: (*CSC: the exist-guarded premise is just to make the proof more general *)
  • src/LTL/LTL_semantics.ma

    r2783 r2845  
    22include "LTL/LTL.ma". (* CSC: syntax.ma in RTLabs *)
    33
    4 definition LTL_semantics : sem_params
     4definition LTL_semantics
    55  mk_sem_graph_params LTL LTL_LIN_semantics.
Note: See TracChangeset for help on using the changeset viewer.