Changeset 3566

Timestamp:

Jun 17, 2015, 4:23:08 PM (6 years ago)

Author:

piccolo

Message:

 

Location:

LTS

Files:

• mono_stack.ma (added)
• stack.ma (modified) (4 diffs)
• variable.ma (modified) (3 diffs)
• variable_stack_pass.ma (modified) (4 diffs)

LTS/stack.ma

@@ -81 +81 @@
 @hide_prf ** % // qed.
 
+definition stack_env_params ≝ mk_env_params ℕ.
+
 definition stack_state_params:state_params≝
-mk_state_params stack_instr_params frame_env_params flat_labels frame_store_t (*DeqEnv*).
+mk_state_params stack_instr_params stack_env_params flat_labels frame_store_t (*DeqEnv*).
 
 definition push : (store_type stack_state_params) → DeqNat → option (store_type stack_state_params) ≝ 
@@ -125 +127 @@
 
 
+let rec list_n (A :Type[0]) (a : A) (n :ℕ) on n : list A ≝
+match n with
+[ O ⇒ nil ?
+| S m ⇒ a :: list_n … a m
+].
+
 definition stack_eval_call:(signature stack_state_params stack_state_params)→ act_params_type stack_state_params → 
 frame_store_t → (option frame_store_t)≝
-λsgn,var,st.
-  match sgn with 
-  [ mk_signature fun fpt rt ⇒
-    !〈n,st1〉 ← pop st;
-    frame_assign_var 〈(〈(nil ?),var〉::(\fst st1)),(\snd st1)〉 O n
-  ].
+λsgn.λvar,st.
+    !〈n,st1〉 ← pop st;  
+    frame_assign_var 〈(〈list_n … O (pred (to_shift + (f_pars … sgn))),var〉::(\fst st1)),(\snd st1)〉 to_shift n.
 
 definition stack_return_call:frame_store_t→ (option frame_store_t)≝
@@ -142 +147 @@
 ].
  
+definition stack_init_store ≝ λn : ℕ.〈[〈list_n … O (to_shift + n),O〉],〈O,O〉〉.
 
 
-definition stack_sem_state_params : sem_state_params stack_state_params ≝ mk_sem_state_params stack_state_params stack_eval_seq frame_eval_io
-(λ_.stack_eval_cond_cond (nil ?)) stack_eval_cond_cond stack_eval_call (λ_.stack_return_call) frame_init_store.
+definition stack_sem_state_params : ℕ → sem_state_params stack_state_params ≝ 
+λn.mk_sem_state_params stack_state_params stack_eval_seq frame_eval_io
+(λ_.stack_eval_cond_cond (nil ?)) stack_eval_cond_cond stack_eval_call (λ_.stack_return_call) (stack_init_store n).
 
   (* Abitare tipo Instructions *)
@@ -154 +161 @@
 
 
-definition stack_envitem≝ (env_item frame_env_params stack_instr_params flat_labels).
+definition stack_envitem≝ (env_item stack_env_params stack_instr_params flat_labels).

LTS/variable.ma

@@ -52 +52 @@
 
 
-definition frame_store_t≝ DeqProd (DeqSet_List (DeqProd activation_frame variable)) (DeqProd DeqNat DeqNat). (*frame_pointer e stack_pointer*)
+definition frame_store_t≝ DeqProd (DeqSet_List activation_frame) (DeqProd DeqNat DeqNat). (*frame_pointer e return register*)
 
 definition frame_env_params ≝ mk_env_params unit.
 
+inductive frame_seq_i : Type[0] ≝ 
+| Seq_i : seq_i → frame_seq_i
+| PopReg : variable → frame_seq_i.
+
+definition eq_frame_seq_i : frame_seq_i → frame_seq_i → bool ≝ 
+λx,y.
+match x with
+[ Seq_i s ⇒ match y with [Seq_i s' ⇒ seq_i_eq s s' | _ ⇒ false ]
+| PopReg v ⇒ match y with [PopReg v' ⇒ eqb v v' | _ ⇒ false]
+].
+
+definition DeqFrameSeqI ≝ mk_DeqSet frame_seq_i eq_frame_seq_i ?.
+@hide_prf cases daemon qed.
+
+definition frame_instr_params : instr_params ≝ 
+mk_instr_params ? ? ? ? ? ?.
+[ @DeqFrameSeqI
+|@(mk_DeqSet io_i io_i_eq io_i_eq_equality)
+|@(mk_DeqSet cond_i cond_i_eq cond_i_eq_equality)
+|@(mk_DeqSet loop_i loop_i_eq loop_i_eq_equality)
+|@(DeqProd variable DeqExpr)
+|@DeqExpr].qed.
+
 definition frame_state_params:state_params≝
-mk_state_params imp_instr_params frame_env_params flat_labels frame_store_t (*DeqEnv*).
+mk_state_params frame_instr_params frame_env_params flat_labels frame_store_t (*DeqEnv*).
 
-definition frame_current_env:store_type frame_state_params→ option ?≝λs.!hd ← option_hd … (\fst s); return \fst hd.
+definition frame_current_env:store_type frame_state_params→ option ?≝λs.!hd ← option_hd … (\fst s); return hd.
 
 definition frame_assign_var ≝ λenv:frame_store_t.λv:variable.λn:DeqNat.
 match \fst env with
 [ nil ⇒ None ?
-| cons hd tl ⇒ let 〈e,var〉 ≝ hd in return 〈(〈assign_frame e v (\fst (\snd env)) n,var〉 :: tl),\snd env〉
+| cons hd tl ⇒ return 〈(assign_frame hd v (\fst (\snd env)) n :: tl),\snd env〉
 ].
 
 definition frame_eval_seq:(seq_instr frame_state_params)→(store_type frame_state_params)→ option (store_type frame_state_params)≝
 λi,s.match i with
-[sNop ⇒ Some ? s
-|sAss v e ⇒ !env ← frame_current_env … s;
-            ! n ← frame_sem_expr env e;
-            frame_assign_var s v n
+[ Seq_i instr ⇒ 
+   match instr with
+   [sNop ⇒ Some ? s
+   |sAss v e ⇒ !env ← frame_current_env … s;
+               ! n ← frame_sem_expr env e;
+               frame_assign_var s v n
+   ]
+| PopReg v ⇒ frame_assign_var s v (\snd (\snd s))
 ].
 
@@ -88 +115 @@
 frame_eval_cond_cond.
 
-definition frame_eval_call:(signature frame_state_params imp_state_params)→ act_params_type frame_state_params → frame_store_t → (option frame_store_t)≝
+definition frame_eval_call:(signature frame_state_params frame_state_params)→ act_params_type frame_state_params → frame_store_t → (option frame_store_t)≝
 λsgn,e,st.
     let 〈var,act_exp〉 ≝ e in
     !env ← frame_current_env … st;
     !n ← frame_sem_expr env act_exp;
-    frame_assign_var 〈(〈(nil ?),var〉::(\fst st)),(\snd st)〉 O n.
+    frame_assign_var 〈((nil ?)::(\fst st)),(\snd st)〉 to_shift n.
 
 definition frame_return_call:(return_type frame_state_params)→ frame_store_t→ (option frame_store_t)≝
 λr,s.match (\fst s) with 
 [nil⇒ None ?
-|cons hd tl⇒ let 〈env,v〉≝ hd in
-             !n ← frame_sem_expr env r;
-             frame_assign_var 〈tl,\snd s〉 v n
+|cons hd tl⇒ !n ← frame_sem_expr hd r;
+             return 〈tl,〈(\fst (\snd s)),n〉〉
 ].
  
-
-definition frame_init_store: (store_type frame_state_params)≝ 〈[〈(nil ?),O〉],〈O,O〉〉.
+definition frame_init_store: (store_type frame_state_params)≝ 〈[(nil ?)],〈O,O〉〉.
 
 
@@ -117 +142 @@
 
 
-definition frame_envitem≝ (env_item frame_env_params imp_instr_params flat_labels).
+definition frame_envitem≝ (env_item frame_env_params frame_instr_params flat_labels).

LTS/variable_stack_pass.ma

@@ -32 +32 @@
 λl,i.foldr … (λc,instr.SEQ stack_state_params flat_labels (push c) (None ?) instr) i l.
 
-let rec trans_var_instr (i : frame_Instructions) on i : stack_Instructions ≝ 
+let rec get_expr_bound (e : expr) on e : ℕ ≝ 
+match e with
+[ Var v ⇒ S v
+| Const n ⇒ O
+| Plus e1 e2 ⇒ max (get_expr_bound e1) (get_expr_bound e2)
+| Minus e1 e2 ⇒ max (get_expr_bound e1) (get_expr_bound e2)
+].
+
+let rec get_cond_bound (c : condition) on c : ℕ ≝ 
+match c with
+[Eq e1 e2 ⇒ max (get_expr_bound e1) (get_expr_bound e2)
+| Not c ⇒ get_cond_bound c
+].
+
+let rec trans_var_instr (i : frame_Instructions) on i : (stack_Instructions × ℕ) ≝ 
 match i with
-[ EMPTY ⇒ EMPTY …
-| RETURN exp ⇒ list_combinators_to_instructions (trans_expr exp) (RETURN … it)
+[ EMPTY ⇒ 〈EMPTY …,O〉
+| RETURN exp ⇒ 〈list_combinators_to_instructions (trans_expr exp) (RETURN … it),get_expr_bound exp〉
 | SEQ seq opt_l instr ⇒ 
+  let 〈t_instr,c_bound〉 ≝ trans_var_instr … instr in
   match seq with
-  [ sNop ⇒ trans_var_instr … instr
-  | sAss v e ⇒ list_combinators_to_instructions (trans_expr e) (SEQ … (pop_Ass v) opt_l (trans_var_instr … instr))
+  [ sNop ⇒ 〈t_instr,c_bound〉
+  | sAss v e ⇒ 〈list_combinators_to_instructions (trans_expr e) (SEQ … (pop_Ass v) opt_l t_instr),
+                max (get_expr_bound e) c_bound〉
   ]
-| COND cond ltrue i_true lfalse i_false instr ⇒ 
-     list_combinators_to_instructions (trans_cond cond) 
-      (COND … it ltrue (trans_var_instr … i_true) lfalse (trans_var_instr … i_false) (trans_var_instr … instr))
+| COND cond ltrue i_true lfalse i_false instr ⇒
+  let 〈t_i_true,i_true_bound〉 ≝ trans_var_instr … i_true in
+  let 〈t_i_false,i_false_bound〉 ≝ trans_var_instr … i_false in
+  let 〈t_instr,c_bound〉 ≝ trans_var_instr … instr in
+  〈list_combinators_to_instructions (trans_cond cond) (COND … it ltrue t_i_true lfalse t_i_false t_instr),
+   max (get_cond_bound cond) (max i_true_bound (max i_false_bound c_bound))〉
 | LOOP cond ltrue i_true lfalse instr ⇒ 
-     LOOP stack_state_params flat_labels (trans_cond … cond) ltrue (trans_var_instr … i_true) lfalse (trans_var_instr … instr)
+  let 〈t_i_true,i_true_bound〉 ≝ trans_var_instr … i_true in 
+  let 〈t_instr,c_bound〉 ≝ trans_var_instr … instr in
+  〈LOOP stack_state_params flat_labels (trans_cond … cond) ltrue t_i_true lfalse t_instr,
+   max (get_cond_bound cond) (max i_true_bound c_bound)〉
 | CALL f act_p opt_l instr ⇒ 
-     list_combinators_to_instructions (trans_expr (\snd act_p)) (CALL … f (\fst act_p) opt_l (trans_var_instr … instr))
+  let 〈t_instr,c_bound〉 ≝ trans_var_instr … instr in
+  〈list_combinators_to_instructions (trans_expr (\snd act_p)) (CALL … f (\fst act_p) opt_l t_instr),
+   max (get_expr_bound (\snd act_p)) c_bound〉
 | IO lin io lout instr ⇒ ?
 ].
@@ -54 +78 @@
 
 definition trans_var_prog : Program frame_env_params imp_instr_params flat_labels → 
-Program frame_env_params stack_instr_params flat_labels ≝ λprog.
-mk_Program …
-(foldr … (λx,tail.(mk_env_item … 
-   (mk_signature ? stack_instr_params (f_name … (f_sig … x)) (f_pars … (f_sig … x)) it) (f_lab … x) 
-        (trans_var_instr … (f_body … x)) ) :: tail) (nil ?) (env … prog))
-(trans_var_instr … (main … prog)).
+(Program stack_env_params stack_instr_params flat_labels × ℕ) ≝ 
+λprog.
+let 〈t_main,m_bound〉 ≝ trans_var_instr … (main … prog) in
+〈(mk_Program …
+  (foldr … 
+   (λx,tail.(let 〈t_body,bound〉 ≝ trans_var_instr … (f_body … x) in
+     mk_env_item …       
+     (mk_signature stack_env_params stack_instr_params (f_name … (f_sig … x)) bound it) (f_lab … x) t_body) :: tail) 
+   (nil ?) (env … prog))
+  t_main),m_bound〉.
 
 include "Simulation.ma".
 
-definition frame_variable_pass_rel ≝  
-λprog : Program frame_state_params frame_state_params frame_state_params.
-let t_prog ≝ trans_var_prog prog in
-mk_relations flat_labels (operational_semantics frame_state_params frame_sem_state_params prog)
- (operational_semantics stack_state_params stack_sem_state_params t_prog) 
- (λs1,s2.store … s1 = store … s2 ∧ code … s2 = trans_var_instr (code … s1) ∧
-         cont … s2 = foldr … (λx,tail. 〈(\fst x),trans_var_instr (\snd x)〉 :: tail) (nil ?) (cont … s1))
- (λ_.λ_.True).
+definition frame_variable_pass_rel : 
+∀prog : Program frame_state_params frame_state_params frame_state_params.
+∀t_prog : Program stack_env_params stack_instr_params flat_labels.
+∀bound : ℕ. 
+relations flat_labels (operational_semantics frame_state_params frame_sem_state_params prog)
+(operational_semantics stack_state_params (stack_sem_state_params bound) t_prog) ≝ 
+λprog,t_prog,bound.
+(mk_relations flat_labels (operational_semantics frame_state_params frame_sem_state_params prog)
+ (operational_semantics stack_state_params (stack_sem_state_params bound) t_prog)
+ (λs1,s2.store … s1 = store … s2 ∧ code … s2 = (\fst (trans_var_instr (code … s1))) ∧
+         cont … s2 = foldr … (λx,tail. 〈(\fst x),(\fst (trans_var_instr (\snd x)))〉 :: tail) (nil ?) (cont … s1))
+ (λ_.λ_.True)).
+
 
 let rec expr_fv (e : expr) on e : list variable ≝ 
@@ -81 +114 @@
 
 definition good_expr ≝  λbound : ℕ.λe : expr.All … (λv.v < bound) (expr_fv e).
+
+let rec cond_fv (c : condition) on c : list variable ≝ 
+match c with
+[ Eq e1 e2 ⇒ expr_fv e1 @ expr_fv e2
+| Not c1 ⇒ cond_fv c1
+].
+
+definition good_cond ≝ λbound : ℕ.λc : condition.All … (λv.v < bound) (cond_fv c).
 
 lemma good_expr_monotone : ∀n1,n2.∀e.n1 ≤ n2 → good_expr n1 e → 
@@ -155 +196 @@
 qed.
 
-
+lemma eval_cond_ok :  ∀st.∀env:activation_frame.∀c: condition.∀b.
+to_shift ≤ |env| → good_cond (|env| - to_shift) c → 
+frame_current_env … st = return env → 
+frame_sem_condition env c = return b →
+∃st'.m_fold Option … eval_combinators (trans_cond c) st = return st' ∧
+pop st' = Some ? 〈if b then 1 else O,st〉.
+** [| * #curr_env #var #rem] #sp_fp #env #c #b #H1 #H2 normalize in ⊢ (% → ?); #EQ destruct
+lapply b -b lapply H1 -H1 lapply H2 -H2 lapply env -env elim c
+[ #e1 #e2 #env #H #H1 #b change with (m_bind ?????) in ⊢ (??%? → ?); #H cases(bind_inversion ????? H) -H
+  #n * #EQn #H cases(bind_inversion ????? H) -H #m * #EQm whd in ⊢ (??%% → ?); #EQ destruct
+  %{(〈〈(if (eqb n m )then 1 else O) :: env,var〉::rem,sp_fp〉)} >m_fold_append
+  cases(eval_exp_ok … EQn) //
+  [2: @(〈〈env,var〉::rem,sp_fp〉) |3: cases(All_inv_append … H) // |4: %]
+  #st1 * #EQst1 #EQpop1 >EQst1 >m_return_bind % // >m_fold_append
+  cases st1 in EQst1 EQpop1; * [| * * [| #m' #env'] #var #rem'] #sp_fp' #EQst1 whd in ⊢ (??%% → ?);
+  #EQ destruct cases(eval_exp_ok … (frame_sem_exp_cons … EQm)) 
+  [2: @(〈〈n::env,var〉::rem,sp_fp〉) |5: % |3: @(transitive_le … H1) // 
+  |4: @(good_expr_monotone … (|env| - to_shift)) [ /2/ | cases(All_inv_append … H) //]
+  |6: cases(All_inv_append … H) // |7: // |8:]
+  #st2 * #EQst2 #EQpop2 >EQst2 >m_return_bind change with (m_bind ?????) in ⊢ (??%?);
+  whd in match eval_combinators; normalize nodelta >EQpop2 %
+| #c1 #IH #env #H1 #H2 #b change with (m_bind ?????) in ⊢ (??%? → ?);
+  #H cases(bind_inversion ????? H) -H #b1 * #EQb1 whd in ⊢ (??%% → ?); #EQ destruct
+  %{(〈〈(if (if b1 then false else true) then 1 else O) :: env,var〉::rem,sp_fp〉)} % //
+  >m_fold_append cases(IH … EQb1) // #st1 * #EQst1 #EQpop1 >EQst1 >m_return_bind
+  change with (m_bind ?????) in ⊢ (??%?); whd in match eval_combinators; normalize nodelta
+  >EQpop1 >m_return_bind whd in ⊢ (??%?); @eq_f @eq_f2 // cases b1 //
+]
+qed.
+
+(*
+let rec create_silent_trace_from_eval_combinators (st : (l : list guard_combinators)
+(prf: m_fold Option … eval_combinators l st = return st')
+*)
+
+definition simulation_imp_frame : 
+∀prog : Program frame_state_params frame_state_params frame_state_params.
+∀t_prog,bound.〈t_prog,bound〉 = trans_var_prog prog → 
+simulation_conditions … (frame_variable_pass_rel prog t_prog bound) ≝ 
+λprog,t_prog,bound,good_trans.
+mk_simulation_conditions ….
+cases daemon
+qed.
  
-definition simulation_imp_frame ≝ 
-λprog : Program frame_state_params frame_state_params frame_state_params.
-mk_simulation_conditions … (frame_variable_pass_rel prog) ???????????.
-cases daemon
-qed.
-