Changeset 3549 for LTS/Vm.ma


Ignore:
Timestamp:
Apr 2, 2015, 3:44:19 PM (5 years ago)
Author:
piccolo
Message:

added paolo's trick

File:
1 edited

Legend:

Unmodified
Added
Removed
  • LTS/Vm.ma

    r3535 r3549  
    1717; io_instr : Type[0] }.
    1818
    19 inductive AssemblerInstr (p : assembler_params) : Type[0] ≝
    20 | Seq : seq_instr p → option (NonFunctionalLabel) →  AssemblerInstr p
    21 | Ijmp: ℕ → AssemblerInstr p
    22 | CJump : jump_condition p → ℕ → NonFunctionalLabel → NonFunctionalLabel → AssemblerInstr p
    23 | Iio : NonFunctionalLabel → io_instr p → NonFunctionalLabel → AssemblerInstr p
    24 | Icall: FunctionName → AssemblerInstr p
    25 | Iret: AssemblerInstr p.
    26 
    27 definition labels_pc_of_instr : ∀p.AssemblerInstr p → ℕ → list (CostLabel × ℕ) ≝
    28 λp,i,program_counter.
     19inductive AssemblerInstr (p : assembler_params) (l_p : label_params) : Type[0] ≝
     20| Seq : seq_instr p → option (NonFunctionalLabel l_p) →  AssemblerInstr p l_p
     21| Ijmp: ℕ → AssemblerInstr p l_p
     22| CJump : jump_condition p → ℕ → NonFunctionalLabel l_p → NonFunctionalLabel l_p → AssemblerInstr p l_p
     23| Iio : NonFunctionalLabel l_p → io_instr p → NonFunctionalLabel l_p → AssemblerInstr p l_p
     24| Icall: FunctionName → AssemblerInstr p l_p
     25| Iret: AssemblerInstr p l_p.
     26
     27definition labels_pc_of_instr : ∀p,l_p.AssemblerInstr p l_p → ℕ → list (CostLabel l_p × ℕ) ≝
     28λp,l_p,i,program_counter.
    2929match i with
    3030  [ Seq _ opt_l ⇒ match opt_l with
    31                   [ Some lbl ⇒ [〈(a_non_functional_label lbl),S program_counter〉]
     31                  [ Some lbl ⇒ [〈(a_non_functional_label lbl),S program_counter〉]
    3232                  | None ⇒ [ ]
    3333                  ]
    3434  | Ijmp _ ⇒ [ ]
    35   | CJump _ newpc ltrue lfalse ⇒ [〈(a_non_functional_label ltrue),newpc〉;
    36                                   〈(a_non_functional_label lfalse),S program_counter〉]
    37   | Iio lin _ lout ⇒ [〈(a_non_functional_label lin),program_counter〉;
    38                       〈(a_non_functional_label lout),S program_counter〉]
     35  | CJump _ newpc ltrue lfalse ⇒ [〈(a_non_functional_label ltrue),newpc〉;
     36                                  〈(a_non_functional_label lfalse),S program_counter〉]
     37  | Iio lin _ lout ⇒ [〈(a_non_functional_label lin),program_counter〉;
     38                      〈(a_non_functional_label lout),S program_counter〉]
    3939  | Icall f ⇒ [ ]
    4040  | Iret ⇒ [ ]
    4141  ].
    4242
    43 let rec labels_pc (p : assembler_params)
    44 (prog : list (AssemblerInstr p)) (call_label_fun : list (ℕ × CallCostLabel))
    45               (return_label_fun : list (ℕ × ReturnPostCostLabel)) (i_act : NonFunctionalLabel)
    46               (program_counter : ℕ) on prog : list (CostLabel × ℕ) ≝
     43let rec labels_pc (p : assembler_params) (l_p : label_params)
     44(prog : list (AssemblerInstr p l_p)) (call_label_fun : list (ℕ × (CallCostLabel l_p)))
     45              (return_label_fun : list (ℕ × (ReturnPostCostLabel l_p))) (i_act : NonFunctionalLabel l_p)
     46              (program_counter : ℕ) on prog : list ((CostLabel l_p) × ℕ) ≝
    4747match prog with
    48 [ nil ⇒ [〈a_non_functional_label (i_act),O〉] @
    49         map … (λx.let〈y,z〉 ≝ x in 〈(a_call z),y〉) (call_label_fun) @
    50         map … (λx.let〈y,z〉 ≝ x in 〈(a_return_post z),y〉) (return_label_fun)
    51 | cons i is ⇒ (labels_pc_of_instr … i program_counter)@labels_pc p is call_label_fun return_label_fun i_act (S program_counter)
     48[ nil ⇒ [〈a_non_functional_label (i_act),O〉] @
     49        map … (λx.let〈y,z〉 ≝ x in 〈(a_call z),y〉) (call_label_fun) @
     50        map … (λx.let〈y,z〉 ≝ x in 〈(a_return_post z),y〉) (return_label_fun)
     51| cons i is ⇒ (labels_pc_of_instr … i program_counter)@labels_pc p l_p is call_label_fun return_label_fun i_act (S program_counter)
    5252].
    5353
    5454include "basics/lists/listb.ma".
    5555
    56 (*doppione da mettere a posto*)
    57 let rec no_duplicates (A : DeqSet) (l : list A) on l : Prop ≝
    58 match l with
    59 [ nil ⇒ True
    60 | cons x xs ⇒ ¬ (bool_to_Prop (x ∈ xs)) ∧ no_duplicates … xs
    61 ].
    62 
    63 
    64 record AssemblerProgram (p : assembler_params) : Type[0] ≝
    65 { instructions : list (AssemblerInstr p)
     56
     57record AssemblerProgram (p : assembler_params) (l_p : label_params) : Type[0] ≝
     58{ instructions : list (AssemblerInstr p l_p)
    6659; endmain : ℕ
    6760; endmain_ok : endmain < |instructions|
    6861; entry_of_function : FunctionName → ℕ
    69 ; call_label_fun : list (ℕ × CallCostLabel)
    70 ; return_label_fun : list (ℕ × ReturnPostCostLabel)
    71 ; in_act : NonFunctionalLabel
     62; call_label_fun : list (ℕ × (CallCostLabel l_p))
     63; return_label_fun : list (ℕ × (ReturnPostCostLabel l_p))
     64; in_act : NonFunctionalLabel l_p
    7265; asm_no_duplicates : no_duplicates … (map ?? \fst … (labels_pc … instructions call_label_fun return_label_fun in_act O))
    7366}.
    7467
    7568
    76 definition fetch: ∀p.AssemblerProgram p → ℕ → option (AssemblerInstr p) ≝
    77  λp,l,n. nth_opt ? n (instructions … l).
     69definition fetch: ∀p,l_p.AssemblerProgram p l_p → ℕ → option (AssemblerInstr p l_p) ≝
     70 λp,l_p,l,n. nth_opt ? n (instructions … l).
    7871
    7972definition stackT: Type[0] ≝ list (nat).
     
    10295
    10396
    104 inductive vmstep (p : assembler_params) (p' : sem_params p)
    105    (prog : AssemblerProgram p)  :
    106       ActionLabel → relation (vm_state p p') ≝
     97inductive vmstep (p : assembler_params) (p' : sem_params p) (l_p : label_params)
     98   (prog : AssemblerProgram p l_p)  :
     99      ActionLabel l_p → relation (vm_state p p') ≝
    107100| vm_seq : ∀st1,st2 : vm_state p p'.∀i,l.
    108            fetch … prog (pc … st1) = return (Seq p i l) →
     101           fetch … prog (pc … st1) = return (Seq p l_p i l) →
    109102           asm_is_io … st1 = false →
    110103           eval_asm_seq p p' i (asm_store … st1) = return asm_store … st2 → 
     
    112105           asm_is_io … st1 = asm_is_io … st2 →
    113106           S (pc … st1) = pc … st2 →
    114            vmstep … (cost_act l) st1 st2
     107           vmstep … (cost_act l) st1 st2
    115108| vm_ijump : ∀st1,st2 : vm_state p p'.∀new_pc : ℕ.
    116            fetch … prog (pc … st1) = return (Ijmp p new_pc) →
     109           fetch … prog (pc … st1) = return (Ijmp p l_p new_pc) →
    117110           asm_is_io … st1 = false →
    118111           asm_store … st1 = asm_store … st2 →
     
    120113           asm_is_io … st1 = asm_is_io … st2 →
    121114           new_pc = pc … st2 →
    122            vmstep … (cost_act (None ?)) st1 st2
     115           vmstep … (cost_act (None ?)) st1 st2
    123116| vm_cjump_true :
    124117           ∀st1,st2 : vm_state p p'.∀cond,new_pc,ltrue,lfalse.
    125118           eval_asm_cond p p' cond (asm_store … st1) = return true→
    126            fetch … prog (pc … st1) = return (CJump p cond new_pc ltrue lfalse) →
     119           fetch … prog (pc … st1) = return (CJump p l_p cond new_pc ltrue lfalse) →
    127120           asm_is_io … st1 = false →
    128121           asm_store … st1 = asm_store … st2 →
     
    130123           asm_is_io … st1 = asm_is_io … st2 →
    131124           pc … st2 = new_pc →
    132            vmstep … (cost_act (Some ? ltrue)) st1 st2
     125           vmstep … (cost_act (Some ? ltrue)) st1 st2
    133126| vm_cjump_false :
    134127           ∀st1,st2 : vm_state p p'.∀cond,new_pc,ltrue,lfalse.
    135128           eval_asm_cond p p' cond (asm_store … st1) = return false→
    136            fetch … prog (pc … st1) = return (CJump p cond new_pc ltrue lfalse) →
     129           fetch … prog (pc … st1) = return (CJump p l_p cond new_pc ltrue lfalse) →
    137130           asm_is_io … st1 = false →
    138131           asm_store … st1 = asm_store … st2 →
     
    140133           asm_is_io … st1 = asm_is_io … st2 →
    141134           S (pc … st1) = pc … st2 →
    142            vmstep … (cost_act (Some ? lfalse)) st1 st2
     135           vmstep … (cost_act (Some ? lfalse)) st1 st2
    143136| vm_io_in : 
    144137           ∀st1,st2 : vm_state p p'.∀lin,io,lout.
    145            fetch … prog (pc … st1) = return (Iio p lin io lout) →
     138           fetch … prog (pc … st1) = return (Iio p l_p lin io lout) →
    146139           asm_is_io … st1 = false →
    147140           asm_store … st1 = asm_store … st2 →
     
    149142           true = asm_is_io … st2 →
    150143           pc … st1 = pc … st2 →
    151            vmstep … (cost_act (Some ? lin)) st1 st2
     144           vmstep … (cost_act (Some ? lin)) st1 st2
    152145| vm_io_out :
    153146           ∀st1,st2 : vm_state p p'.∀lin,io,lout.
    154            fetch … prog (pc … st1) = return (Iio p lin io lout) →
     147           fetch … prog (pc … st1) = return (Iio p l_p lin io lout) →
    155148           asm_is_io … st1 = true →
    156149           eval_asm_io … io (asm_store … st1) = return asm_store … st2 →
     
    158151           false = asm_is_io … st2 →
    159152           S (pc … st1) = pc … st2 →
    160            vmstep … (cost_act (Some ? lout)) st1 st2
     153           vmstep … (cost_act (Some ? lout)) st1 st2
    161154| vm_call :
    162155           ∀st1,st2 : vm_state p p'.∀f,lbl.
    163            fetch … prog (pc … st1) = return (Icall p f) →
     156           fetch … prog (pc … st1) = return (Icall p l_p f) →
    164157           asm_is_io … st1 = false →
    165158           asm_store … st1 = asm_store … st2 →
     
    167160           asm_is_io … st1 = asm_is_io … st2 →
    168161           entry_of_function … prog f = pc … st2 →
    169            label_of_pc ? (call_label_fun … prog) (entry_of_function … prog f) = return lbl →
    170            vmstep … (call_act f lbl) st1 st2
     162           label_of_pc (call_label_fun … prog) (entry_of_function … prog f) = return lbl →
     163           vmstep … (call_act f lbl) st1 st2
    171164| vm_ret :
    172165          ∀st1,st2 : vm_state p p'.∀newpc,lbl.
    173            fetch … prog (pc … st1) = return (Iret p) →
     166           fetch … prog (pc … st1) = return (Iret p l_p) →
    174167           asm_is_io … st1 = false →
    175168           asm_store … st1 = asm_store … st2 →
     
    177170           asm_is_io … st1 = asm_is_io … st2 →
    178171           newpc = pc … st2 →
    179            label_of_pc ? (return_label_fun … prog) newpc = return lbl →
    180            vmstep … (ret_act (Some ? lbl)) st1 st2.
    181 
    182 definition eval_vmstate : ∀p : assembler_params.∀p' : sem_params p. 
    183 AssemblerProgram p → vm_state p p' → option (ActionLabel × (vm_state p p')) ≝
    184 λp,p',prog,st.
     172           label_of_pc (return_label_fun … prog) newpc = return lbl →
     173           vmstep … (ret_act (Some ? lbl)) st1 st2.
     174
     175definition eval_vmstate : ∀p : assembler_params.∀p' : sem_params p.∀l_p : label_params.
     176AssemblerProgram p l_p → vm_state p p' → option ((ActionLabel l_p) × (vm_state p p')) ≝
     177λp,p',l_p,prog,st.
    185178! i ← fetch … prog (pc … st);
    186179match i with
     
    190183   else
    191184     ! new_store ← eval_asm_seq p p' x (asm_store … st);
    192      return 〈cost_act opt_l,
     185     return 〈cost_act opt_l,
    193186             mk_vm_state ?? (S (pc … st)) (asm_stack … st) new_store false〉
    194187| Ijmp newpc ⇒
     
    196189     None ?
    197190   else
    198      return 〈cost_act (None ?),
     191     return 〈cost_act (None ?),
    199192             mk_vm_state ?? newpc (asm_stack … st) (asm_store … st) false〉
    200193| CJump cond newpc ltrue lfalse ⇒
     
    204197     ! b ← eval_asm_cond p p' cond (asm_store … st);
    205198     if b then
    206        return 〈cost_act (Some ? ltrue),
     199       return 〈cost_act (Some ? ltrue),
    207200               mk_vm_state ?? newpc (asm_stack … st) (asm_store … st) false〉
    208201     else
    209        return 〈cost_act (Some ? lfalse),
     202       return 〈cost_act (Some ? lfalse),
    210203               mk_vm_state ?? (S (pc … st)) (asm_stack … st) (asm_store … st) false〉
    211204| Iio lin io lout ⇒
    212205              if asm_is_io … st then
    213206                 ! new_store ← eval_asm_io … io (asm_store … st);
    214                  return 〈cost_act (Some ? lout),
     207                 return 〈cost_act (Some ? lout),
    215208                         mk_vm_state ?? (S (pc … st)) (asm_stack … st)
    216209                         new_store false〉   
    217210              else
    218                 return 〈cost_act (Some ? lin),
     211                return 〈cost_act (Some ? lin),
    219212                        mk_vm_state ?? (pc … st) (asm_stack … st) (asm_store … st)
    220213                                    true〉
     
    224217    else
    225218      ! lbl ← label_of_pc ? (call_label_fun … prog) (entry_of_function … prog f);
    226       return 〈call_act f lbl,
     219      return 〈call_act f lbl,
    227220              mk_vm_state ?? (entry_of_function … prog f)
    228221                             ((S (pc … st)) :: (asm_stack … st))
     
    233226            ! 〈newpc,tl〉 ← option_pop … (asm_stack … st);
    234227            ! lbl ← label_of_pc ? (return_label_fun … prog) newpc;
    235             return 〈ret_act (Some ? lbl),
     228            return 〈ret_act (Some ? lbl),
    236229                    mk_vm_state ?? newpc tl (asm_store … st) false〉
    237230].
    238231
    239 lemma eval_vmstate_to_Prop : ∀p,p',prog,st1,st2,l.
    240 eval_vmstate p p' prog st1 = return 〈l,st2〉 → vmstep … prog l st1 st2.
    241 #p #p' #prog #st1 #st2 #l whd in match eval_vmstate; normalize nodelta
     232lemma eval_vmstate_to_Prop : ∀p,p',l_p,prog,st1,st2,l.
     233eval_vmstate p p' l_p prog st1 = return 〈l,st2〉 → vmstep … prog l st1 st2.
     234#p #p' #l_p #prog #st1 #st2 #l whd in match eval_vmstate; normalize nodelta
    242235#H cases(bind_inversion ????? H) -H * normalize nodelta
    243236[ #seq #opt_l * #EQfetch inversion(asm_is_io ???) normalize nodelta
     
    269262
    270263 
    271 lemma vm_step_to_eval : ∀p,p',prog,st1,st2,l.vmstep … prog l st1 st2 →
    272 eval_vmstate p p' prog st1 = return 〈l,st2〉.
    273 #p #p' #prog * #pc1 #stack1 #store1 #io1
     264lemma vm_step_to_eval : ∀p,p',l_p,prog,st1,st2,l.vmstep … prog l st1 st2 →
     265eval_vmstate p p' l_p prog st1 = return 〈l,st2〉.
     266#p #p' #l_p #prog * #pc1 #stack1 #store1 #io1
    274267* #pc2 #stack2 #store2 #io2 #l #H inversion H
    275268[ #s1 #s2 #i #opt_l #EQfetch #EQio #EQstore #EQstack #EQio1 #EQpc
     
    316309
    317310definition ass_vmstep ≝
    318  λp,p',prog.
     311 λp,p',l_p,prog.
    319312  λl.λs1,s2 : vm_ass_state p p'.
    320313                    match s1 with
     
    322315                        match s2 with
    323316                        [ STATE st2 ⇒ 
    324                             (eqb (pc ?? st1) (endmain … prog)) = false ∧ vmstep p p' prog l st1 st2
     317                            (eqb (pc ?? st1) (endmain … prog)) = false ∧ vmstep p p' l_p prog l st1 st2
    325318                        | INITIAL ⇒ False
    326319                        | FINAL ⇒ eqb (pc … st1) (endmain … prog) = true ∧
    327                            l = cost_act (Some … (in_act … prog))
     320                           l = cost_act (Some … (in_act … prog))
    328321                        ]
    329322                    | INITIAL ⇒ match s2 with
    330323                                [ STATE st2 ⇒ eqb (pc … st2) O = true ∧
    331                                    l = cost_act (Some … (in_act … prog))
     324                                   l = cost_act (Some … (in_act … prog))
    332325                                | _ ⇒ False
    333326                                ]
     
    335328                    ].
    336329
    337 definition asm_operational_semantics : ∀p.sem_params p → AssemblerProgram p →  abstract_status
    338 λp,p',prog.let init_act ≝ cost_act (Some ? (in_act … prog)) in
    339            let end_act ≝ cost_act (Some ? (in_act … prog)) in
    340     mk_abstract_status
     330definition asm_operational_semantics : ∀p,l_p.sem_params p → AssemblerProgram p l_p →  abstract_status l_p
     331λp,l_p,p',prog.let init_act ≝ cost_act … (Some ? (in_act … prog)) in
     332           let end_act ≝ cost_act (Some ? (in_act … prog)) in
     333    mk_abstract_status
    341334                (vm_ass_state p p')
    342335                (ass_vmstep … prog)
     
    427420
    428421definition asm_concrete_trans_sys ≝
    429 λp,p',prog.mk_concrete_transition_sys …
    430              (asm_operational_semantics p p' prog).
     422λp,p',l_p,prog.mk_concrete_transition_sys …
     423             (asm_operational_semantics p p' l_p prog).
    431424             
    432425         
    433426definition emits_labels ≝
    434 λp.λinstr : AssemblerInstr p.match instr with
     427λp,l_p.λinstr : AssemblerInstr p l_p.match instr with
    435428        [ Seq _ opt_l ⇒ match opt_l with
    436429                        [ None ⇒ Some ? (λpc.S pc)
     
    441434        ].
    442435
    443 definition fetch_state : ∀p,p'.AssemblerProgram p → vm_state p p' → option (AssemblerInstr p) ≝
    444 λp,p',prog,st.fetch … prog (pc … st).
    445 
    446 record asm_galois_connection (p: assembler_params) (p': sem_params p) (prog: AssemblerProgram p) : Type[2] ≝
     436definition fetch_state : ∀p,p',l_p.AssemblerProgram p l_p → vm_state p p' → option (AssemblerInstr p l_p) ≝
     437λp,p',l_p,prog,st.fetch … prog (pc … st).
     438
     439record asm_galois_connection (p: assembler_params) (p': sem_params p) (l_p : label_params) (prog: AssemblerProgram p l_p) : Type[2] ≝
    447440{ aabs_d : abstract_transition_sys
    448 ; agalois_rel:> galois_rel (asm_concrete_trans_sys p p' prog) aabs_d
     441; agalois_rel:> galois_rel … (asm_concrete_trans_sys p l_p p' prog) aabs_d
    449442}.
    450443
    451444definition galois_connection_of_asm_galois_connection:
    452  ∀p,p',prog. asm_galois_connection p p' prog → galois_connection
    453  λp,p',prog,agc.
    454   mk_galois_connection
    455    (asm_concrete_trans_sys p p' prog)
     445 ∀p,p',l_p,prog. asm_galois_connection p p' l_p prog → galois_connection l_p
     446 λp,p',l_p,prog,agc.
     447  mk_galois_connection …
     448   (asm_concrete_trans_sys p l_p p' prog)
    456449   (aabs_d … agc)
    457450   (agalois_rel … agc).
     
    460453
    461454definition ass_fetch ≝
    462  λp,p',prog.
    463     λs.match s with [ STATE st ⇒ if eqb (pc … st) (endmain prog) then
     455 λp,p',l_p,prog.
     456    λs.match s with [ STATE st ⇒ if eqb (pc … st) (endmain p l_p prog) then
    464457                                   Some ? (None ?)
    465                                else ! x ← fetch_state p p' prog st; Some ? (Some ? x)
     458                               else ! x ← fetch_state p p' l_p prog st; Some ? (Some ? x)
    466459                    | INITIAL ⇒ Some ? (None ?)
    467460                    | FINAL  ⇒ None ? ].
    468461
    469462definition ass_instr_map ≝
    470  λp,p',prog.λasm_galois_conn: asm_galois_connection p p' prog.
    471   λinstr_map: AssemblerInstr p → (*option*) (abs_instr … (abs_d asm_galois_conn)).
     463 λp,p',l_p,prog.λasm_galois_conn: asm_galois_connection p p' l_p prog.
     464  λinstr_map: AssemblerInstr p l_p → (*option*) (abs_instr … (abs_d … asm_galois_conn)).
    472465  (λi.match i with [None ⇒ (*Some …*) (e …) |Some x ⇒ instr_map … x]).
    473466
    474 record asm_abstract_interpretation (p: assembler_params) (p': sem_params p) (prog: AssemblerProgram p) : Type[2] ≝
    475 { asm_galois_conn: asm_galois_connection p p' prog
    476 ; instr_map : AssemblerInstr p → (*option*) (abs_instr … (abs_d asm_galois_conn))
     467record asm_abstract_interpretation (p: assembler_params) (p': sem_params p) (l_p : label_params) (prog: AssemblerProgram p l_p) : Type[2] ≝
     468{ asm_galois_conn: asm_galois_connection p p' l_p prog
     469; instr_map : AssemblerInstr p l_p → (*option*) (abs_instr … (abs_d … asm_galois_conn))
    477470; instr_map_ok :
    478471   ∀s,s': concr … asm_galois_conn. ∀a: abs_d … asm_galois_conn.∀l,i.
     
    484477
    485478definition abstract_interpretation_of_asm_abstract_interpretation:
    486  ∀p,p',prog. asm_abstract_interpretation p p' prog → abstract_interpretation
     479 ∀p,p',l_p,prog. asm_abstract_interpretation p p' l_p prog → abstract_interpretation l_p
    487480
    488 λp,p',prog,aai.
    489  mk_abstract_interpretation
    490   (asm_galois_conn … aai) (option (AssemblerInstr p)) (ass_fetch p p' prog)
     481λp,p',l_p,prog,aai.
     482 mk_abstract_interpretation …
     483  (asm_galois_conn … aai) (option (AssemblerInstr p l_p)) (ass_fetch p p' l_p prog)
    491484   (ass_instr_map … prog … (instr_map … aai)) (instr_map_ok … aai).
    492485
     
    496489λA,l.match l with [ nil ⇒ false | _ ⇒  true ].
    497490
    498 let rec block_cost (p : assembler_params)
    499  (prog: AssemblerProgram p) (abs_t : monoid)
    500  (instr_m : AssemblerInstr p → abs_t)
     491let rec block_cost (p : assembler_params) (l_p : label_params)
     492 (prog: AssemblerProgram p l_p) (abs_t : monoid)
     493 (instr_m : AssemblerInstr p l_p → abs_t)
    501494 (prog_c: option ℕ)
    502495    (program_size: ℕ)
     
    532525
    533526
    534 lemma labels_pc_ok : ∀p,prog,l1,l2,i_act,i,lbl,pc,m.
     527lemma labels_pc_ok : ∀p,l_p,prog,l1,l2,i_act,i,lbl,pc,m.
    535528nth_opt ? pc prog = return i →
    536529mem ? lbl (labels_pc_of_instr … i (m+pc)) →
    537 mem ? lbl (labels_pc p prog l1 l2 i_act m).
    538 #p #instrs #l1 #l2 #iact #i #lbl #pc
     530mem ? lbl (labels_pc p l_p prog l1 l2 i_act m).
     531#p #l_p #instrs #l1 #l2 #iact #i #lbl #pc
    539532whd in match fetch; normalize nodelta lapply pc -pc
    540533elim instrs
     
    547540qed.
    548541
    549 lemma labels_pf_in_act: ∀p,prog,pc.
    550   mem CostLabel (in_act p prog)
    551   (map (CostLabel×ℕ) CostLabel \fst
    552    (labels_pc p (instructions p prog) (call_label_fun p prog)
    553     (return_label_fun p prog) (in_act p prog) pc)).
    554  #p #prog elim (instructions p prog) normalize /2/
    555 qed.
    556 
    557 lemma labels_pc_return: ∀p,prog,l1,l2,iact,x1,x2.
    558  label_of_pc ReturnPostCostLabel l2 x1=return x2 →
     542lemma labels_pf_in_act: ∀p,l_p,prog,pc.
     543  mem (CostLabel l_p) (in_act p l_p prog)
     544  (map ((CostLabel l_p)×ℕ) (CostLabel l_p) \fst
     545   (labels_pc p … (instructions p …  prog) (call_label_fun p … prog)
     546    (return_label_fun p …  prog) (in_act p … prog) pc)).
     547 #p #l_p #prog elim (instructions … prog) normalize /2/
     548qed.
     549
     550lemma labels_pc_return: ∀p,l_p,prog,l1,l2,iact,x1,x2.
     551 label_of_pc (ReturnPostCostLabel l_p) l2 x1=return x2 →
    559552 ∀m.
    560    mem … 〈(a_return_post x2),x1〉 (labels_pc p prog l1 l2 iact m).
    561  #p #l #l1 #l2 #iact whd in match (labels_pc ???); #x1 #x2 #H elim l
     553   mem … 〈(a_return_post … x2),x1〉 (labels_pc p l_p prog l1 l2 iact m).
     554 #p #l_p #l #l1 #l2 #iact whd in match (labels_pc ???); #x1 #x2 #H elim l
    562555[ #m @mem_append_l2 @mem_append_l2 whd in H:(??%?);
    563556  elim l2 in H; [ whd in ⊢ (??%% → ?); #EQ destruct]
     
    569562qed.
    570563
    571 lemma labels_pc_call: ∀p,prog,l1,l2,iact,x1,x2.
    572  label_of_pc CallCostLabel l1 x1=return x2 →
     564lemma labels_pc_call: ∀p,l_p,prog,l1,l2,iact,x1,x2.
     565 label_of_pc (CallCostLabel l_p) l1 x1=return x2 →
    573566 ∀m.
    574    mem … 〈(a_call x2),x1〉 (labels_pc p prog l1 l2 iact m).
    575  #p #l #l1 #l2 #iact whd in match (labels_pc ???); #x1 #x2 #H elim l
     567   mem … 〈(a_call l_p x2),x1〉 (labels_pc p l_p prog l1 l2 iact m).
     568 #p #l_p #l #l1 #l2 #iact whd in match (labels_pc ???); #x1 #x2 #H elim l
    576569[ #m @mem_append_l2 @mem_append_l1 whd in H:(??%?);
    577570  elim l1 in H; [ whd in ⊢ (??%% → ?); #EQ destruct]
     
    609602].
    610603
    611 definition static_analisys : ∀p : assembler_params.∀abs_t : monoid.(AssemblerInstr p → abs_t) →
    612 ∀mT : cost_map_T DEQCostLabel abs_t.AssemblerProgram p → option mT ≝
    613 λp,abs_t,instr_m,mT,prog.
     604definition static_analisys : ∀p : assembler_params.∀l_p : label_params.∀abs_t : monoid.(AssemblerInstr p l_p → abs_t …) →
     605∀mT : cost_map_T (DEQCostLabel l_p) (abs_t …).AssemblerProgram p l_p → option mT ≝
     606λp,l_p,abs_t,instr_m,mT,prog.
    614607let prog_size ≝ S (|instructions … prog|) in
    615 m_foldr Option ?? (λx,m.let 〈z,w〉≝ x in ! k ← block_cost p prog abs_t instr_m (Some ? w) prog_size; 
     608m_foldr Option ?? (λx,m.let 〈z,w〉≝ x in ! k ← block_cost p l_p prog abs_t instr_m (Some ? w) prog_size; 
    616609                               return set_map … m z k) (labels_pc … (instructions … prog)
    617610                                         (call_label_fun … prog) (return_label_fun … prog) (in_act … prog) O)
    618611      (empty_map ?? mT).
    619612     
    620 
    621 (*falso: necessita di no_duplicates*)
    622613
    623614definition eq_deq_prod : ∀D1,D2 : DeqSet.D1 × D2 → D1 × D2 → bool ≝
     
    658649qed.
    659650
    660 lemma static_analisys_ok : ∀p,abs_t,instr_m,mT,prog,lbl,pc,map.
    661 static_analisys p abs_t instr_m mT prog = return map →
     651lemma static_analisys_ok : ∀p,l_p,abs_t,instr_m,mT,prog,lbl,pc,map.
     652static_analisys p l_p abs_t instr_m mT prog = return map →
    662653mem … 〈lbl,pc〉 (labels_pc … (instructions … prog) (call_label_fun … prog)
    663654                   (return_label_fun … prog) (in_act … prog) O) →
     
    665656block_cost … prog abs_t instr_m (Some ? pc) (S (|(instructions … prog)|)) ∧
    666657block_cost … prog abs_t instr_m (Some ? pc) (S (|(instructions … prog)|)) ≠ None ?.
    667 #p #abs_t #instr_m #mT * #prog whd in match static_analisys; normalize nodelta
     658#p #l_p #abs_t #instr_m #mT * #prog whd in match static_analisys; normalize nodelta
    668659#endmain #Hendmain #entry_fun #call_label_fun #return_label_fun #inact
    669660#nodup generalize in match nodup in ⊢ (∀_.∀_.∀_. (??(????%??)?) → %); #Hnodup lapply nodup -nodup
    670 lapply (labels_pc ??????) #l elim l [ #x #y #z #w #h * ]
     661lapply (labels_pc ???????) #l elim l [ #x #y #z #w #h * ]
    671662* #hd1 #hd2 #tl #IH * #H1 #H2 #lbl #pc #map #H
    672663cases(bind_inversion ????? H) -H #map1 * #EQmap1 normalize nodelta #H
     
    683674qed.
    684675
    685 definition terminated_trace : ∀S : abstract_status.∀s1,s3 : S.raw_trace … s1 s3 → Prop ≝
    686 λS,s1,s3,t.∃s2: S.∃t1 : raw_trace … s1 s2.∃ l,prf.t = t1 @ (t_ind ? s2 s3 s3 l prf … (t_base … s3))
    687 ∧ is_costlabelled_act l ∧ pre_measurable_trace … t1.
     676definition terminated_trace : ∀p : label_params.∀S : abstract_status p.∀s1,s3 : S.raw_trace … s1 s3 → Prop ≝
     677λp,S,s1,s3,t.∃s2: S.∃t1 : raw_trace … s1 s2.∃ l,prf.t = t1 @ (t_ind p ? s2 s3 s3 l prf … (t_base … s3))
     678∧ is_costlabelled_act l ∧ pre_measurable_trace … t1.
    688679
    689680definition big_op: ∀M: monoid. list M → M ≝
     
    716707qed.
    717708
    718 lemma monotonicity_of_block_cost : ∀p,prog,abs_t,instr_m,pc,size,k.
    719 block_cost p prog abs_t instr_m (Some ? pc) size = return k →
     709lemma monotonicity_of_block_cost : ∀p,l_p,prog,abs_t,instr_m,pc,size,k.
     710block_cost p l_p prog abs_t instr_m (Some ? pc) size = return k →
    720711∀size'.size ≤ size' →
    721 block_cost p prog abs_t instr_m (Some ? pc) size' = return k.
    722 #p #prog #abs_t #instr_m #pc #size lapply pc elim size
     712block_cost p l_p prog abs_t instr_m (Some ? pc) size' = return k.
     713#p #l_p #prog #abs_t #instr_m #pc #size lapply pc elim size
    723714[ #pc #k whd in ⊢ (??%% → ?); #EQ destruct]
    724715#n #IH #pc #k whd in ⊢ (??%% → ?); @eqb_elim
     
    741732qed.
    742733
    743 lemma step_emit : ∀p,p',prog,st1,st2,l,i.
    744 fetch p prog (pc … st1) = return i →
     734lemma step_emit : ∀p,p',l_p,prog,st1,st2,l,i.
     735fetch p l_p prog (pc … st1) = return i →
    745736eval_vmstate p p' … prog st1 = return 〈l,st2〉 → 
    746737emits_labels … i = None ? → ∃x.
    747 match l in ActionLabel return λ_:ActionLabel.(list CostLabel) with 
    748 [call_act f c ⇒ [a_call c]
     738match l in ActionLabel return λ_: (ActionLabel l_p).(list (CostLabel l_p)) with 
     739[call_act f c ⇒ [a_call c]
    749740|ret_act x ⇒
    750    match x with [None⇒[]|Some c⇒[a_return_post c]]
     741   match x with [None⇒[]|Some c⇒[a_return_post c]]
    751742|cost_act x ⇒
    752    match x with [None⇒[]|Some c⇒[a_non_functional_label c]]
     743   match x with [None⇒[]|Some c⇒[a_non_functional_label c]]
    753744] = [x] ∧
    754  (mem … 〈x,pc … st2〉 (labels_pc p (instructions … prog) (call_label_fun … prog) (return_label_fun … prog) (in_act … prog) O)).
    755 #p #p' #prog #st1 #st2 #l #i #EQi whd in match eval_vmstate; normalize nodelta
     745 (mem … 〈x,pc … st2〉 (labels_pc p l_p (instructions … prog) (call_label_fun … prog) (return_label_fun … prog) (in_act … prog) O)).
     746#p #p' #l_p #prog #st1 #st2 #l #i #EQi whd in match eval_vmstate; normalize nodelta
    756747>EQi >m_return_bind normalize nodelta cases i in EQi; -i normalize nodelta
    757748[ #seq * [|#lab]
     
    775766qed.
    776767
    777 lemma step_non_emit : ∀p,p',prog,st1,st2,l,i,f.
    778 fetch p prog (pc … st1) = return i →
     768lemma step_non_emit : ∀p,p',l_p,prog,st1,st2,l,i,f.
     769fetch p l_p prog (pc … st1) = return i →
    779770eval_vmstate p p' … prog st1 = return 〈l,st2〉 → 
    780771emits_labels … i = Some ? f →
    781 match l in ActionLabel return λ_:ActionLabel.(list CostLabel) with 
    782 [call_act f c ⇒ [a_call c]
     772match l in ActionLabel return λ_: (ActionLabel l_p).(list (CostLabel l_p)) with 
     773[call_act f c ⇒ [a_call c]
    783774|ret_act x ⇒
    784    match x with [None⇒[]|Some c⇒[a_return_post c]]
     775   match x with [None⇒[]|Some c⇒[a_return_post c]]
    785776|cost_act x ⇒
    786    match x with [None⇒[]|Some c⇒[a_non_functional_label c]]
     777   match x with [None⇒[]|Some c⇒[a_non_functional_label c]]
    787778] = [ ] ∧ pc … st2 = f (pc … st1).
    788 #p #p' #prog #st1 #st2 #l #i #f #EQi whd in match eval_vmstate; normalize nodelta
     779#p #p' #l_p #prog #st1 #st2 #l #i #f #EQi whd in match eval_vmstate; normalize nodelta
    789780>EQi >m_return_bind normalize nodelta cases i in EQi; -i normalize nodelta
    790781[ #seq * [|#lab]
     
    807798
    808799lemma labels_of_trace_are_in_code :
    809 ∀p,p',prog.∀st1,st2 : vm_ass_state p p'.∀t : raw_trace (asm_operational_semantics p p' prog) … st1 st2.
     800∀p,p',l_p,prog.∀st1,st2 : vm_ass_state p p'.∀t : raw_trace … (asm_operational_semantics p l_p p' prog) … st1 st2.
    810801∀lbl.
    811802mem … lbl (get_costlabels_of_trace … t) →
    812 mem … lbl (map … \fst … (labels_pc … (instructions p prog) (call_label_fun … prog) (return_label_fun … prog) (in_act … prog) O)).
    813 #p #p' #prog #st1 #st2 #t elim t
     803mem … lbl (map … \fst … (labels_pc … (instructions p prog) (call_label_fun … prog) (return_label_fun … prog) (in_act … prog) O)).
     804#p #p' #l_p #prog #st1 #st2 #t elim t
    814805[ #st #lbl *
    815806| #st1 #st2 #st3 #l whd in ⊢ (% → ?);
     
    862853
    863854
    864 lemma tbase_tind_append : ∀S : abstract_status.∀st1,st2,st3.∀t : raw_trace … st1 st2.
     855lemma tbase_tind_append : ∀p : label_params.∀S : abstract_status p.∀st1,st2,st3 : S.∀t : raw_trace … st1 st2.
    865856∀l,prf.∀t'.
    866 t_base … st1 = t @ t_ind S st2 st3 st1 l prf t' → False.
    867 #S #st1 #st2 #st3 *
     857t_base … st1 = t @ t_ind S st2 st3 st1 l prf t' → False.
     858#p #S #st1 #st2 #st3 *
    868859[ #st #l #prf  #t' normalize #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct ]
    869860#s1 #s2 #s3 #l1 #prf1 #t2 #l2 #prf2 #t3 normalize #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct
     
    893884*)
    894885
    895 lemma get_cost_label_of_trace_tind : ∀S : abstract_status.
     886lemma get_cost_label_of_trace_tind : ∀p. ∀S : abstract_status p.
    896887∀st1,st2,st3 : S.∀l,prf,t.
    897888get_costlabels_of_trace … (t_ind … st1 st2 st3 l prf t) =
    898 actionlabel_to_costlabel l @ get_costlabels_of_trace … t.
    899 #S #st1 #st2 #st3 * // qed.
     889actionlabel_to_costlabel l @ get_costlabels_of_trace … t.
     890#p #S #st1 #st2 #st3 * // qed.
    900891
    901892lemma actionlabel_ok :
    902  ∀l : ActionLabel.
    903   is_costlabelled_act l → ∃c.actionlabel_to_costlabel l = [c].
    904 * /2/ * /2/ *
    905 qed.
    906 
    907 lemma i_act_in_map :  ∀p,prog,iact,l1,l2.
    908 mem ? 〈a_non_functional_label iact,O〉 (labels_pc p prog l1 l2 iact O).
    909 #p #instr #iact #l1 #l2 generalize in match O in ⊢ (???%); elim instr
     893 ∀p.∀l : ActionLabel p.
     894  is_costlabelled_act … l → ∃c.actionlabel_to_costlabel … l = [c].
     895#p * /2/ * /2/ *
     896qed.
     897
     898lemma i_act_in_map :  ∀p,l_p,prog,iact,l1,l2.
     899mem ? 〈a_non_functional_label l_p iact,O〉 (labels_pc p l_p prog l1 l2 iact O).
     900#p #l_p #instr #iact #l1 #l2 generalize in match O in ⊢ (???%); elim instr
    910901[ normalize /2/] #i #xs #IH #m whd in match (labels_pc ???);
    911902@mem_append_l2 @IH
     
    916907lemma static_dynamic_inv :
    917908(* Given an assembly program *)
    918 ∀p,p',prog.
     909∀p,p',l_p,prog.
    919910
    920911(* Given an abstraction interpretation framework for the program *)
    921 ∀R: asm_abstract_interpretation p p' prog.
     912∀R: asm_abstract_interpretation p p' l_p prog.
    922913
    923914(* If the static analysis does not fail *)
     
    925916
    926917(* For every pre_measurable, terminated trace *)
    927 ∀st1,st2. ∀t: raw_trace (asm_operational_semantics … prog) … st1 st2.
     918∀st1,st2. ∀t: raw_trace l_p (asm_operational_semantics … prog) … st1 st2.
    928919 terminated_trace … t →
    929920
     
    933924(* Let k be the statically computed abstract action of the prefix of the trace
    934925   up to the first label *)
    935 ∀k.block_cost p prog … (instr_map … R) (get_pc … st1 (endmain … prog)) (S (|(instructions … prog)|)) = return k →
     926∀k.block_cost p prog … (instr_map … R) (get_pc … st1 (endmain … prog)) (S (|(instructions … prog)|)) = return k →
    936927
    937928(* Let abs_actions be the list of statically computed abstract actions
     
    954945    @(proj2 … (static_analisys_ok … EQmap … Hmem))
    955946]
    956 #p #p' #prog #R #mT #map1 #EQmap #st1 #st2 #t * #st3 * #t1 *
     947#p #p' #l_p #prog #R #mT #map1 #EQmap #st1 #st2 #t * #st3 * #t1 *
    957948#l1 * #prf1 ** #EQ destruct #Hlabelled
    958949>(rewrite_in_dependent_map ??? (get_costlabels_of_trace … t1))
     
    1002993    whd in match (dependent_map ????); #costs #EQ destruct #a1 #good_st_a1
    1003994    >neutral_r >act_neutral
    1004     lapply(instr_map_ok R … (refl …) good_st_a1)
     995    lapply(instr_map_ok … l_p … R … (refl …) good_st_a1)
    1005996    [1,7,13,19,25,31,37: whd in ⊢ (??%%); @eqb_elim normalize nodelta
    1006997      [1,3,5,7,9,11,13: #EQ cases(absurd ? EQ Hpc) ] #_ whd in match fetch_state;
     
    10091000        | >EQfetch in ⊢ (??%?); | >EQfetch in ⊢ (??%?); | >EQfetch in ⊢ (??%?);
    10101001        | >EQfetch in ⊢ (??%?); ] %
    1011       |3,9,15,21,27,33,39: skip |*: try assumption // ]]]
     1002      |3,9,15,21,27,33,39: skip |*: try assumption #H @H] ]]
    10121003| -st1 * [3: #st1] #st3 #st4 #l [3: *] cases st3 -st3
    10131004  [1,2,4,5: * #H1 #H2 #tl #_ #l1 #exe @⊥ lapply tl -tl lapply(refl ? (FINAL p p'))
     
    10401031  [2: cases(static_analisys_ok … c … (pc … st3) … EQmap) // #EQ #_ <EQ whd in match (big_op ??);
    10411032      >neutral_l assumption
    1042    |3,6: [ >neutral_r] lapply(instr_map_ok R … (refl …) good_a1)
     1033   |3,6: [ >neutral_r] lapply(instr_map_ok … l_p … R … (refl …) good_a1)
    10431034       [1,7: whd in ⊢ (??%?); @eqb_elim
    10441035         [1,3: #ABS cases(absurd ? ABS Hpc) ] #_ normalize nodelta whd in match fetch_state;
     
    10781069      [2: lapply EQpc_st3 @eqb_elim [2: #_ #EQ destruct] #EQ #_ >EQ @i_act_in_map ]
    10791070      #EQ #_ <EQ whd in match (big_op ??); >neutral_l assumption
    1080    |  lapply(instr_map_ok R … (refl …) good_a1)
     1071   |  lapply(instr_map_ok … l_p …  R … (refl …) good_a1)
    10811072     [1: % | assumption |*:] normalize in ⊢ (% → ?); #H @H
    10821073   ]
     
    10941085qed. *)
    10951086
    1096 lemma execute_mem_label_pc :∀p,p',prog.∀st0,st1 :vm_state p p'.∀l1,c1.
    1097 actionlabel_to_costlabel l1 = [c1] →
    1098 vmstep p p' prog l1 st0 st1 →
     1087lemma execute_mem_label_pc :∀p,p',l_p,prog.∀st0,st1 :vm_state p p'.∀l1,c1.
     1088actionlabel_to_costlabel l_p l1 = [c1] →
     1089vmstep p p' l_p prog l1 st0 st1 →
    10991090 mem … 〈c1,pc p p' st1〉
    11001091  (labels_pc … (instructions … prog) (call_label_fun … prog)
    11011092   (return_label_fun … prog) (in_act … prog) O).
    1102 #p #p' #prog #st0 #st1 #l1 #c1 #EQc1 #H lapply(vm_step_to_eval … H) -H
     1093#p #p' #l_p #prog #st0 #st1 #l1 #c1 #EQc1 #H lapply(vm_step_to_eval … H) -H
    11031094#H cases(bind_inversion ????? H); #i * #EQi #Hi cases(step_emit … EQi H)
    11041095[ #c2 whd in match actionlabel_to_costlabel in EQc1; normalize nodelta in EQc1;
     
    11241115include "Simulation.ma".
    11251116
    1126 lemma sub_trace_premeasurable_l1 : ∀p,p',prog.
    1127 ∀s1,s2,s3. ∀t1: raw_trace (asm_operational_semantics p p' prog) … s1 s2.
    1128 ∀t2 : raw_trace (asm_operational_semantics p p' prog) … s2 s3.
     1117lemma sub_trace_premeasurable_l1 : ∀p,p',l_p,prog.
     1118∀s1,s2,s3. ∀t1: raw_trace l_p (asm_operational_semantics p l_p p' prog) … s1 s2.
     1119∀t2 : raw_trace l_p (asm_operational_semantics p l_p p' prog) … s2 s3.
    11291120pre_measurable_trace … (t1 @ t2) →
    11301121pre_measurable_trace … t1.
    1131 #p #p' #prog #s1 #s2 #s3 #t1 lapply s3 -s3 elim t1
    1132 [ #st #st3 #t2 whd in ⊢ (????% → ?); #H %1 @(head_of_premeasurable_is_not_io … H) ]
     1122#p #p' #l_p #prog #s1 #s2 #s3 #t1 lapply s3 -s3 elim t1
     1123[ #st #st3 #t2 whd in ⊢ (?????% → ?); #H %1 @(head_of_premeasurable_is_not_io … H) ]
    11331124#st1 #st2 #st3 #l #exe #tl #IH #st4 #t2 #H inversion H in ⊢ ?;
    11341125[ #st #class #EQ1 #EQ2 #EQ3 #EQ4 destruct whd in EQ3 : (??%?%); destruct
     
    11441135qed.
    11451136
    1146 lemma sub_trace_premeasurable_l2 : ∀p,p',prog.
    1147 ∀s1,s2,s3. ∀t1: raw_trace (asm_operational_semantics p p' prog) … s1 s2.
    1148 ∀t2 : raw_trace (asm_operational_semantics p p' prog) … s2 s3.
     1137lemma sub_trace_premeasurable_l2 : ∀p,p',l_p,prog.
     1138∀s1,s2,s3. ∀t1: raw_trace l_p (asm_operational_semantics p l_p p' prog) … s1 s2.
     1139∀t2 : raw_trace l_p (asm_operational_semantics p l_p p' prog) … s2 s3.
    11491140pre_measurable_trace … (t1 @ t2) →
    11501141pre_measurable_trace … t2.
    1151 #p #p' #prog #s1 #s2 #s3 #t1 lapply s3 -s3 elim t1
    1152 [ #st #st3 #t2 whd in ⊢ (????% → ?); #H @H ]
     1142#p #p' #l_p #prog #s1 #s2 #s3 #t1 lapply s3 -s3 elim t1
     1143[ #st #st3 #t2 whd in ⊢ (?????% → ?); #H @H ]
    11531144#st1 #st2 #st3 #l #exe #tl #IH #st4 #t2 #H inversion H in ⊢ ?;
    11541145[ #st #class #EQ1 #EQ2 #EQ3 #EQ4 destruct whd in EQ3 : (??%?%); destruct
     
    11681159theorem static_dynamic :
    11691160(* Given an assembly program *)
    1170 ∀p,p',prog.
     1161∀p,p',l_p,prog.
    11711162
    11721163(* Given an abstraction interpretation framework for the program *)
    1173 ∀R: asm_abstract_interpretation p p' prog.
     1164∀R: asm_abstract_interpretation p p' l_p prog.
    11741165
    11751166(* If the static analysis does not fail *)
     
    11781169(* For every measurable trace whose second state is st1 or, equivalently,
    11791170   whose first state after the initial labelled transition is st1 *)
    1180 ∀si,s1,s2,sn. ∀t: raw_trace (asm_operational_semantics … prog) … si sn.
     1171∀si,s1,s2,sn. ∀t: raw_trace l_p (asm_operational_semantics … prog) … si sn.
    11811172 measurable … s1 s2 … t →
    11821173
     
    12031194    @(proj2 … (static_analisys_ok … EQmap … Hmem))
    12041195]
    1205 #p #p' #prog #R #mT #map1 #EQmap #si #s1 #s2 #sn #t #measurable
     1196#p #p' #l_p #prog #R #mT #map1 #EQmap #si #s1 #s2 #sn #t #measurable
    12061197cases measurable #s0 * #s3 * #ti0 * #t13 * #t2n* #l1 * #l2 * #prf1 * #prf2
    12071198******* #pre_t13 #EQ destruct #Hl1 #Hl2 #Hcall_l2 #sil_ti0 #sil_t2n #Hcall_l1
Note: See TracChangeset for help on using the changeset viewer.