Changeset 3578


Ignore:
Timestamp:
Jul 1, 2015, 11:45:08 PM (4 years ago)
Author:
piccolo
Message:

baco

Location:
LTS
Files:
3 edited

Legend:

Unmodified
Added
Removed
  • LTS/imp.ma

    r3575 r3578  
    6060    expr ≡ carr X.
    6161
    62 (* ambigous input? why?
     62(*
    6363unification hint  0 ≔ p1,p2;
    6464    X ≟ DeqExpr
  • LTS/monostack_to_asm_pass.ma

    r3574 r3578  
    9494qed.
    9595
    96 
    97 
    9896let rec mono_asm_state_rel_aux (s_stack : list ((ActionLabel flat_labels) × mono_stack_Instructions)) (stack_t : stackT)
    9997(post_t : list asm_instructions) (t_code : list asm_instructions) (post_t_pc : ℕ) on s_stack :
     
    114112                         mono_asm_state_rel_aux tl stack_t post_pc t_code (post_t_pc + |ts_code|) (proj2 … prf))
    115113                     ∨
    116                      (∃new_pc.option_hd … post_t = return (Ijmp … new_pc) ∧
     114                     (∃new_pc.nth_opt … O post_t = return (Ijmp … new_pc) ∧
    117115                      ∃pre_pc,post_pc.t_code = pre_pc @ ts_code @post_pc ∧ (|pre_pc|) = new_pc ∧
    118116                      mono_asm_state_rel_aux tl stack_t post_pc t_code (new_pc + |ts_code|) (proj2 … prf))
     
    124122definition mono_asm_state_rel : ∀s_code : mono_stack_Instructions.
    125123∀s_stack : list ((ActionLabel flat_labels) × mono_stack_Instructions).
    126 ℕ → stackT → list asm_instructions → post_labelled_return_instr … s_code →
     124ℕ → stackT → list asm_instructions → ? → post_labelled_return_instr … s_code →
    127125All … (λx.post_labelled_return_instr … (\snd x)) s_stack → Prop ≝ 
    128 λs_code,s_stack,pc,t_stack,t_code,prf1,prf2.
     126λs_code,s_stack,pc,t_stack,t_code,init_act,prf1,prf2.
    129127let 〈ts_code,ret_label〉 ≝ trans_mono_stack_instr s_code pc prf1 in
    130128∃pre_pc,post_t.t_code = pre_pc @ ts_code @ post_t ∧ (|pre_pc|) = pc ∧
    131  (All … (λx.let 〈act,code〉 ≝ x in is_cost_label … act → (bool_to_Prop (is_silent_cost_act_b … act))) s_stack) ∧
     129∃chop_stack.s_stack = chop_stack @ [〈init_act,EMPTY …〉] ∧
     130 (All … (λx.let 〈act,code〉 ≝ x in is_cost_label … act → (bool_to_Prop (is_silent_cost_act_b … act))) chop_stack) ∧
    132131 mono_asm_state_rel_aux s_stack t_stack post_t t_code (pc + |ts_code|) prf2.
    133  
     132
    134133definition monostack_asm_pass_rel :
    135134∀prog : Program stack_env_params stack_instr_params flat_labels.
     
    144143(mk_relations flat_labels (operational_semantics mono_stack_state_params (mono_stack_sem_state_params bound) prog)
    145144 (asm_operational_semantics … (asm_sem_params) t_prog)
    146  (λs1,s2.∃s2'.s2 = STATE … s2' ∧ store … s1 = (\fst (asm_store … s2')) ∧ ∃prf1 : post_labelled_return_instr … (code … s1).
    147    ∃prf2 : All … (λx.post_labelled_return_instr … (\snd x)) (cont … s1).
    148    mono_asm_state_rel (code … s1) (cont … s1) (pc … s2') (asm_stack … s2') (instructions … t_prog) prf1 prf2
     145 (λs1,s2.
     146   match s2 with
     147   [ INITIAL ⇒ bool_to_Prop (lang_initial … (mono_stack_sem_state_params bound) prog s1)
     148   | FINAL ⇒ bool_to_Prop (lang_final … s1)
     149   | STATE s2' ⇒ store … s1 = (\fst (asm_store … s2')) ∧ ∃prf1 : post_labelled_return_instr … (code … s1).
     150                 ∃prf2 : All … (λx.post_labelled_return_instr … (\snd x)) (cont … s1).
     151                 mono_asm_state_rel (code … s1) (cont … s1) (pc … s2') (asm_stack … s2') (instructions … t_prog)
     152                   (cost_act … (Some ? (initial_act … prog))) prf1 prf2
     153   ]
    149154  )
    150155 (λ_.λ_.True)).
     
    158163[4: #s1 #s1' #s2 #H inversion H
    159164  [ #st1 #st2 * #act #instr #tl #EQcode_st1 #EQcont_st1 #EQ1 #EQ2 destruct #EQstore #Hio1 #Hio2
    160     #no_ret #EQ1 #EQ2 #EQ3 #EQ4 destruct whd in ⊢ (% → ?); * #st2' ** #EQ destruct #EQstore1
    161     * #post_label1 * #post_label2 whd in match mono_asm_state_rel; normalize nodelta lapply post_label1 >EQcode_st1
    162     * whd in match (trans_mono_stack_instr ???); normalize nodelta
    163     * #pre_pc * #post_t *** #EQinstructions #EQpc lapply post_label2
    164     -post_label2 >EQcont_st1 * #post_code_st2 #post_tail * #_ #Hcont_cost
    165     whd in match (mono_asm_state_rel_aux ??????); @pair_elim #t_code_st2 #t_ret_st2 whd in match (length ??);
    166     <plus_n_O #EQt_code_st2
     165    #no_ret #EQ1 #EQ2 #EQ3 #EQ4 destruct whd in ⊢ (% → ?); cases s1' -s1' normalize nodelta
     166    [ whd in match lang_initial; normalize nodelta #H cases(andb_Prop_true … H) -H
     167      #H cases(andb_Prop_true … H) -H #H cases(andb_Prop_true … H) -H #_ inversion(eqb_list ???) [2: #_ *]
     168      #ABS @⊥ >EQcont_st1 in ABS; normalize #EQ destruct
     169    | whd in match lang_final; normalize nodelta #H cases(andb_Prop_true … H) -H #_ >EQcont_st1 *
     170    ]
     171    #st2' * #EQstore1 * #post_label1 * #post_label2 whd in match mono_asm_state_rel; normalize nodelta lapply post_label1
     172    >EQcode_st1 * whd in match (trans_mono_stack_instr ???); normalize nodelta
     173    * #pre_pc * #post_t ** #EQinstructions #EQpc ** [|#chop_hd #chop_tail] **
     174    [ >EQcont_st1 in ⊢ (% → ?); | >EQcont_st1 in ⊢ (% → ?); ] whd in ⊢ (??%% → ?); #EQ destruct -EQ
     175    * #_ #Hchop_tail >EQcont_st1 in post_label2; * #post_code_st2 #post_tail
     176    whd in match (mono_asm_state_rel_aux ??????); @pair_elim #t_code_st2 #t_ret_st2
     177    whd in match (length ??); <plus_n_O #EQt_code_st2
    167178    *
    168179    [ * #post_pc1 * #EQ destruct #Haux #class1 #class2 %{(STATE … st2')} %{(t_base …)} % [2: %2 normalize % *]
    169       whd %{st2'} % [ %{(refl …)} <EQstore1 //] %{post_code_st2} %{post_tail} whd >EQt_code_st2
    170       normalize nodelta %{pre_pc} %{post_pc1} % [ % // % // >EQinstructions %] assumption
    171     | cases daemon
    172     ]
     180      whd  % [ <EQstore1 //] %{post_code_st2} %{post_tail} whd >EQt_code_st2
     181      normalize nodelta %{pre_pc} %{post_pc1} % [ % // >EQinstructions %] %{chop_tail} %
     182      [ % //] assumption
     183    | * #new_pc * #EQnew_pc * #pre_pc * #post_pc ** #EQinstructions1 #EQ destruct #Hcont #class1 #class2
     184      %{(STATE … (mk_vm_state … (|pre_pc|) (asm_stack … st2') (asm_store … st2') (asm_is_io … st2')))}
     185      %{(t_ind … (cost_act … (None ?)) … (t_base …))}
     186      [ whd <EQpc % [ cases daemon (* BOH!!! *) ] @(vm_ijump … (|pre_pc|)) // [2: cases daemon (* TODO ???*) ]
     187      whd in match fetch; normalize nodelta >EQinstructions >nth_second <EQpc [2: //] <minus_n_n assumption ]     
     188      % [2: %1 %2 cases daemon ] whd % [ <EQstore //] %{post_code_st2} %{post_tail} whd @pair_elim #p1 #p2
     189      <EQpc in EQt_code_st2; #EQt_code_st2
     190      cut (∀a,b,c,c'. trans_mono_stack_instr a b c = trans_mono_stack_instr a b c')
     191      [ #a #b #c #d % ] #KK >KK [ <EQt_code_st2
     192     
     193       #K lapply (trans_eq ???? (sym_eq … EQt_code_st2) K)
     194     
     195       >EQt_code_st2 in ⊢ (% → ?);
     196      normalize nodelta
    173197  |*: cases daemon
    174198  ]
  • LTS/variable_stack_pass.ma

    r3577 r3578  
    203203qed.
    204204
    205 (*
    206 let rec create_silent_trace_from_eval_combinators (st : (l : list guard_combinators)
    207 (prf: m_fold Option … eval_combinators l st = return st')
    208 *)
     205definition safe_cast : ∀A,B : Type[0].A = B → A → B ≝
     206λA,B,prf.match prf with [refl ⇒ λx : A.x].
     207
     208let rec create_silent_trace_from_eval_combinators (prog : Program stack_env_params stack_instr_params flat_labels)
     209(bound : ℕ) (st,st' : state stack_state_params) (l : list guard_combinators) 
     210on l :
     211 m_fold Option … eval_combinators l (store … st) = return (store … st') →
     212  code … st = list_combinators_to_instructions l (code … st') →
     213  cont … st = cont … st' → io_info … st = io_info … st' →
     214  raw_trace … (operational_semantics stack_state_params (stack_sem_state_params bound) prog) st st' ≝
     215match l return λx.(m_fold Option … eval_combinators x ? = ? → ? = list_combinators_to_instructions x ? → ?) with
     216[ nil ⇒ λprf1,prf2,prf3,prf4.safe_cast (raw_trace … (operational_semantics stack_state_params (stack_sem_state_params bound) prog) st st)
     217     (raw_trace … (operational_semantics stack_state_params (stack_sem_state_params bound) prog) st st') ? (t_base ?? st)
     218| cons x xs ⇒ λprf1,prf2,prf3,prf4.
     219   let next_store ≝ (opt_safe … (eval_combinators x (store … st)) ?) in
     220   let next_st ≝ mk_state stack_state_params (list_combinators_to_instructions xs (code … st')) (cont … st')
     221                   next_store (io_info … st') in
     222   let tail ≝ create_silent_trace_from_eval_combinators prog bound next_st st' xs ? (refl …) (refl …) (refl …) in
     223   t_ind … (cost_act … (None ?)) … tail
     224].
     225@hide_prf
     226[ cases st in prf1 prf2 prf3 prf4; cases st' #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 #H9 #H10 #H11 #H12 whd in H9 : (??%%);
     227  whd in H10 : (??%%); destruct %
     228|4: change with (m_bind ?????) in prf1 :(??%?); cases(bind_inversion ????? prf1) -prf1 #w * #EQw #_ >EQw %
     229   whd in ⊢ (??%% → ?); #EQ destruct
     230| whd @seq_sil
     231  [4: >prf2 in ⊢ (??%?); %
     232  |8: %
     233  |5: change with (eval_combinators ??) in ⊢ (??%?); normalize nodelta @opt_safe_elim #w #H assumption
     234  |6: %
     235  |7: assumption
     236  |9,10: cases daemon (*io*)
     237  |*:
     238  ]
     239| normalize nodelta @opt_safe_elim #w #EQw change with (m_bind ?????) in prf1 :(??%?); >EQw in prf1;
     240  >m_return_bind //
     241]
     242qed.
     243
     244lemma create_silent_trace_from_eval_combinators_ok : ∀prog,bound,st,st',l,prf1,prf2,prf3,prf4,t.
     245create_silent_trace_from_eval_combinators prog bound st st' l prf1 prf2 prf3 prf4 = t →
     246pre_silent_trace … t.
     247#prog #bound #st #st' #l lapply st -st lapply st' -st' elim l
     248[ * #code' #cont' #store' #io' * #code #cont #store #io whd in ⊢ (??%% → ??%% → ?); #EQ destruct #EQ1 #EQ2 #EQ3 destruct
     249  #t whd in ⊢ (??%% → ?); #EQ destruct % cases daemon (*io*)
     250| #x #xs #IH #st' #st #H cases(bind_inversion ????? H) #w * #EQw #EQstore_st'
     251  whd in ⊢ (???% → ?); change with (list_combinators_to_instructions ??) in match (foldr ?????);
     252  #prf2 #EQcont #EQio #t whd in ⊢ (??%? → ?); #EQ destruct %2 [cases daemon (* io *)] @IH [|*: %]
     253]
     254qed.
     255
     256(*  [ @opt_safe_elim #w' >EQw whd in ⊢ (??%% → ?); #EQ destruct assumption
     257  | %
     258  | % c'e' un baco????*)
    209259
    210260definition simulation_imp_frame :
Note: See TracChangeset for help on using the changeset viewer.