Changeset 3448 for LTS/Vm.ma


Ignore:
Timestamp:
Feb 19, 2014, 6:45:55 PM (6 years ago)
Author:
piccolo
Message:
 
File:
1 edited

Legend:

Unmodified
Added
Removed
  • LTS/Vm.ma

    r3379 r3448  
    1 include "Common.ma".
    2 
    3 inductive instr: Type[0] :=
    4 | Iconst: nat → instr
    5 | Ivar: option ident → instr
    6 | Isetvar: option ident → instr
    7 | Iadd: instr
    8 | Isub: instr
    9 | Ijmp: nat → instr
    10 | Ibne: nat → instr
    11 | Ibge: nat → instr
    12 | Ihalt: instr
    13 | Iio: instr
    14 | Icall: fname → instr
    15 | Iret: fname → instr.
    16 
    17 definition programT ≝ fname → list instr.
    18 
    19 definition fetch: list instr → nat → option instr ≝ λl,n. nth_opt ? n l.
    20 
    21 definition stackT: Type[0] ≝ list nat.
    22 
    23 definition vmstate ≝ λS:storeT. (list instr) × nat × (stackT × S).
    24 
    25 definition pc: ∀S. vmstate S → nat ≝ λS,s. \snd (\fst s).
    26 
    27 inductive vmstep (p: programT) (S: storeT) : vmstate S → vmstate S → Prop :=
    28 | vmstep_const: ∀c,pc,stk,s,n. fetch c pc = Some … (Iconst n) →
    29    vmstep …
    30     〈c, pc,     stk,      s〉
    31     〈c, 1 + pc, n :: stk, s〉
    32 | vmstep_var: ∀c,pc,stk,s,x. fetch c pc = Some … (Ivar x) →
    33    vmstep …
    34     〈c, pc,     stk,              s〉
    35     〈c, 1 + pc, get … s x :: stk, s〉
    36 | vmstep_setvar: ∀c,pc,stk,s,x,n. fetch c pc = Some … (Isetvar x) →
    37    vmstep …
    38     〈c, pc,     n :: stk, s〉
    39     〈c, 1 + pc, stk,      set … s x n〉
    40 | vmstep_add: ∀c,pc,stk,s,n1,n2. fetch c pc = Some … Iadd →
    41    vmstep …
    42     〈c, pc,     n2 :: n1 :: stk,  s〉
    43     〈c, 1 + pc, (n1 + n2) :: stk, s〉
    44 | vmstep_sub: ∀c,pc,stk,s,n1,n2. fetch c pc = Some … Isub →
    45    vmstep …
    46     〈c, pc,     n2 :: n1 :: stk,  s〉
    47     〈c, 1 + pc, (n1 - n2) :: stk, s〉
    48 | vmstep_bne: ∀c,pc,stk,s,ofs,n1,n2. fetch c pc = Some … (Ibne ofs) →
    49    let pc' ≝ if eqb n1 n2 then 1 + pc else 1 + pc + ofs in
    50    vmstep …
    51     〈c, pc,  n2 :: n1 :: stk, s〉
    52     〈c, pc', stk,             s〉
    53 | vmstep_bge: ∀c,pc,stk,s,ofs,n1,n2. fetch c pc = Some … (Ibge ofs) →
    54    let pc' ≝ if ltb n1 n2 then 1 + pc else 1 + pc + ofs in
    55    vmstep …
    56     〈c, pc,  n2 :: n1 :: stk, s〉
    57     〈c, pc', stk,             s〉
    58 | vmstep_branch: ∀c,pc,stk,s,ofs. fetch c pc = Some … (Ijmp ofs) →
    59    let pc' ≝ 1 + pc + ofs in
    60    vmstep …
    61     〈c,           pc, stk, s〉
    62     〈c, 1 + pc + ofs, stk, s〉
    63 | vmstep_io: ∀c,pc,stk,s. fetch c pc = Some … Iio →
    64    vmstep …
    65     〈c,     pc, stk, s〉
    66     〈c, 1 + pc, stk, s〉.
    67 
    68 definition emitterT ≝ nat → nat → option label.
    69 
    70 definition vmlstep: ∀p: programT. ∀S: storeT. ∀emit: emitterT.
    71  vmstate S → vmstate S → list label → Prop ≝
    72 λp,S,emitter,s1,s2,ll. ∀l.
    73  vmstep p S s1 s2 ∧ ll = [l] ∧ emitter (pc … s1) (pc … s2) = Some … l.
    74 
    75 (*
    76 Definition star_vm (lbl: Type) (c: code (instr_vm lbl)) := star (trans_vm lbl c).
    77 
    78 Definition term_vm_lbl (lbl: Type) (c: code (instr_vm lbl)) (s_init s_fin: store) (trace: list lbl) :=
    79         exists pc,
    80         code_at c pc = Some (Ihalt lbl) /\
    81         star_vm lbl c (0, nil, s_init) (pc, nil, s_fin) trace.
    82 
    83 Definition term_vm (c: code_vm) (s_init s_fin: store):=
    84         exists pc,
    85         code_at c pc = Some (Ihalt False) /\
    86         star_vm False c (0, nil, s_init) (pc, nil, s_fin) nil.
    87 
    88 Definition term_vml (c: code_vml) (s_init s_fin: store) (trace: list label) :=
    89         exists pc,
    90         code_at c pc = Some (Ihalt label) /\
    91         star_vm label c (0, nil, s_init) (pc, nil, s_fin) trace.
    92 *)
     1include "Traces.ma".
     2include "basics/lists/list.ma".
     3include "../src/utilities/option.ma".
     4include "basics/jmeq.ma".
     5
     6record monoid: Type[1] ≝
     7 { carrier :> Type[0]
     8 ; op: carrier → carrier → carrier
     9 ; e: carrier
     10 ; neutral: ∀x. op … x e = x
     11 ; is_associative: ∀x,y,z. op … (op … x y) z = op … x (op … y z)
     12 }.
     13
     14record assembler_params : Type[1] ≝
     15{ seq_instr : Type[0]
     16; jump_condition : Type[0]
     17; io_instr : Type[0]
     18; entry_of_function : FunctionName → ℕ
     19; call_label_fun : list (ℕ × CallCostLabel)
     20; return_label_fun : list (ℕ × ReturnPostCostLabel)
     21}.
     22
     23inductive AssemblerInstr (p : assembler_params) : Type[0] ≝
     24| Seq : seq_instr p → option (NonFunctionalLabel) →  AssemblerInstr p
     25| Ijmp: ℕ → AssemblerInstr p
     26| CJump : jump_condition p → ℕ → NonFunctionalLabel → NonFunctionalLabel → AssemblerInstr p
     27| Iio : NonFunctionalLabel → io_instr p → NonFunctionalLabel → AssemblerInstr p
     28| Icall: FunctionName → AssemblerInstr p
     29| Iret: AssemblerInstr p.
     30
     31definition AssemblerProgram ≝λp.list (AssemblerInstr p) × ℕ.
     32
     33definition fetch: ∀p.AssemblerProgram p → ℕ → option (AssemblerInstr p) ≝
     34 λp,l,n. nth_opt ? n (\fst l).
     35
     36definition stackT: Type[0] ≝ list (nat).
     37
     38record sem_params (p : assembler_params) : Type[1] ≝
     39{ m : monoid
     40; asm_store_type : Type[0]
     41; eval_asm_seq : seq_instr p → asm_store_type → option asm_store_type
     42; eval_asm_cond : jump_condition p → asm_store_type → option bool
     43; eval_asm_io : io_instr p → asm_store_type → option asm_store_type
     44; cost_of_io : io_instr p → asm_store_type → m
     45; cost_of : AssemblerInstr p → m
     46}.
     47
     48record vm_state (p : assembler_params) (p' : sem_params p) : Type[0] ≝
     49{ pc : ℕ
     50; asm_stack : stackT
     51; asm_store : asm_store_type … p'
     52; asm_is_io : bool
     53; cost : m … p'
     54}.
     55
     56definition label_of_pc ≝ λL.λl.λpc.find …
     57   (λp.let 〈x,y〉 ≝ p in if eqb x pc then Some L y else None ? ) l.
     58
     59
     60inductive vmstep (p : assembler_params) (p' : sem_params p)
     61   (prog : AssemblerProgram p)  :
     62      ActionLabel → relation (vm_state p p') ≝
     63| vm_seq : ∀st1,st2 : vm_state p p'.∀i,l.
     64           fetch … prog (pc … st1) = return (Seq p i l) →
     65           asm_is_io … st1 = false →
     66           eval_asm_seq p p' i (asm_store … st1) = return asm_store … st2 → 
     67           asm_stack … st1 = asm_stack … st2 →
     68           asm_is_io … st1 = asm_is_io … st2 →
     69           S (pc … st1) = pc … st2 →
     70           op … (cost … st1) (cost_of p p' (Seq p i l)) = cost … st2 →
     71           vmstep … (cost_act l) st1 st2
     72| vm_ijump : ∀st1,st2 : vm_state p p'.∀new_pc : ℕ.
     73           fetch … prog (pc … st1) = return (Ijmp p new_pc) →
     74           asm_is_io … st1 = false →
     75           asm_store … st1 = asm_store … st2 →
     76           asm_stack … st1 = asm_stack … st2 →
     77           asm_is_io … st1 = asm_is_io … st2 →
     78           new_pc = pc … st2 →
     79           op … (cost … st1) (cost_of p p' (Ijmp … new_pc)) = cost … st2 →
     80           vmstep … (cost_act (None ?)) st1 st2
     81| vm_cjump_true :
     82           ∀st1,st2 : vm_state p p'.∀cond,new_pc,ltrue,lfalse.
     83           eval_asm_cond p p' cond (asm_store … st1) = return true→
     84           fetch … prog (pc … st1) = return (CJump p cond new_pc ltrue lfalse) →
     85           asm_is_io … st1 = false →
     86           asm_store … st1 = asm_store … st2 →
     87           asm_stack … st1 = asm_stack … st2 →
     88           asm_is_io … st1 = asm_is_io … st2 →
     89           pc … st2 = new_pc →
     90           op … (cost … st1) (cost_of p p' (CJump p cond new_pc ltrue lfalse)) = cost … st2 →
     91           vmstep … (cost_act (Some ? ltrue)) st1 st2
     92| vm_cjump_false :
     93           ∀st1,st2 : vm_state p p'.∀cond,new_pc,ltrue,lfalse.
     94           eval_asm_cond p p' cond (asm_store … st1) = return false→
     95           fetch … prog (pc … st1) = return (CJump p cond new_pc ltrue lfalse) →
     96           asm_is_io … st1 = false →
     97           asm_store … st1 = asm_store … st2 →
     98           asm_stack … st1 = asm_stack … st2 →
     99           asm_is_io … st1 = asm_is_io … st2 →
     100           S (pc … st1) = pc … st2 →
     101           op … (cost … st1) (cost_of p p' (CJump … cond new_pc ltrue lfalse)) = cost … st2 →
     102           vmstep … (cost_act (Some ? lfalse)) st1 st2
     103| vm_io_in : 
     104           ∀st1,st2 : vm_state p p'.∀lin,io,lout.
     105           fetch … prog (pc … st1) = return (Iio p lin io lout) →
     106           asm_is_io … st1 = false →
     107           asm_store … st1 = asm_store … st2 →
     108           asm_stack … st1 = asm_stack … st2 →
     109           true = asm_is_io … st2 →
     110           pc … st1 = pc … st2 →
     111           cost … st1 = cost … st2 →
     112           vmstep … (cost_act (Some ? lin)) st1 st2
     113| vm_io_out :
     114           ∀st1,st2 : vm_state p p'.∀lin,io,lout.
     115           fetch … prog (pc … st1) = return (Iio p lin io lout) →
     116           asm_is_io … st1 = true →
     117           eval_asm_io … io (asm_store … st1) = return asm_store … st2 →
     118           asm_stack … st1 = asm_stack … st2 →
     119           false = asm_is_io … st2 →
     120           S (pc … st1) = pc … st2 →
     121           op … (cost … st1) (cost_of_io p p' io (asm_store … st1)) = cost … st2 →
     122           vmstep … (cost_act (Some ? lout)) st1 st2
     123| vm_call :
     124           ∀st1,st2 : vm_state p p'.∀f,lbl.
     125           fetch … prog (pc … st1) = return (Icall p f) →
     126           asm_is_io … st1 = false →
     127           asm_store … st1 = asm_store … st2 →
     128           S (pc … st1) ::  asm_stack … st1 = asm_stack … st2 →
     129           asm_is_io … st1 = asm_is_io … st2 →
     130           entry_of_function p  f = pc … st2 →
     131           op … (cost … st1) (cost_of p p' (Icall p f)) = cost … st2 →
     132           label_of_pc ? (call_label_fun p) (entry_of_function p f) = return lbl →
     133           vmstep … (call_act f lbl) st1 st2
     134| vm_ret :
     135          ∀st1,st2 : vm_state p p'.∀newpc,lbl.
     136           fetch … prog (pc … st1) = return (Iret p) →
     137           asm_is_io … st1 = false →
     138           asm_store … st1 = asm_store … st2 →
     139           asm_stack … st1 = newpc ::  asm_stack … st2  →
     140           asm_is_io … st1 = asm_is_io … st2 →
     141           newpc = pc … st2 →
     142           label_of_pc ? (return_label_fun p) newpc = return lbl →
     143           op … (cost … st1) (cost_of p p' (Iret p)) = cost … st2 →
     144           vmstep … (ret_act (Some ? lbl)) st1 st2.
     145           
     146include "../src/utilities/hide.ma".
     147
     148discriminator option.
     149
     150definition asm_operational_semantics : ∀p.sem_params p → AssemblerProgram p →  abstract_status ≝
     151λp,p',prog.mk_abstract_status
     152                (vm_state p p')
     153                (λl.λst1,st2 : vm_state p p'.(eqb (pc ?? st1) (\snd prog)) = false ∧
     154                               vmstep p p' prog l st1 st2)
     155                (λ_.λ_.True)
     156                (λs.match fetch … prog (pc … s) with
     157                    [ Some i ⇒ match i with
     158                               [ Seq _ _ ⇒ cl_other
     159                               | Ijmp _ ⇒ cl_other
     160                               | CJump _ _ _ _ ⇒ cl_jump
     161                               | Iio _ _ _ ⇒ if asm_is_io … s then cl_io else cl_other
     162                               | Icall _ ⇒ cl_other
     163                               | Iret ⇒ cl_other
     164                               ]
     165                    | None ⇒ cl_other
     166                    ]
     167                )
     168                (λ_.true)
     169                (λs.eqb (pc ?? s) O)
     170                (λs.eqb (pc … s) (\snd prog))
     171                ???.
     172@hide_prf cases daemon (*
     173[ #s1 #s2 #l inversion(fetch ???) normalize nodelta
     174  [ #_ #EQ destruct] * normalize nodelta
     175  [ #seq #lbl #_
     176  | #n #_
     177  | #cond #newpc #ltrue #lfalse #EQfetch
     178  | #lin #io #lout #_ cases (asm_is_io ??) normalize nodelta
     179  | #f #_
     180  | #_
     181  ]
     182  #EQ destruct * #_ #H inversion H in ⊢ ?;
     183  [ #st1 #st2 #i #lbl #EQ #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 #H9 #H10 #H11
     184  | #st1 #st2 #new_pc #EQ #H13 #H14 #H15 #H16 #H17 #H18 #H19 #H20 #H21 #H22 #H23
     185  | #st1 #st2 #cond1 #new_pc1 #ltrue1 #lfalse1 #ev_c #EQ #H25 #H26 #H27 #H28 #H29 #H30 #H31 #H32 #H33 #H34 #H35
     186  | #st1 #st2 #cond1 #new_pc1 #ltrue1 #lfalse1 #ev_c #EQ #H37 #H38 #H39 #H40 #H41 #H42 #H43 #H44 #H45 #H46 #H47
     187  | #st1 #st2 #lin #io #lout #EQ #H49 #H50 #H51 #H52 #H53 #H54 #H55 #H56 #H57 #H58 #H59
     188  | #st1 #st2 #lin #io #lout #EQ #H61 #H62 #H63 #H64 #H65 #H66 #H67 #H68 #H69 #H70 #H71
     189  | #st1 #st2 #f #EQ #H73 #H74 #H75 #H76 #H77 #H78 #H79 #H80 #H81 #H82 #H83
     190  | #st1 #st2 #new_pc #EQ #H85 #H86 #H87 #H88 #H89 #H90 #H91 #H92 #H93 #H94 #H95
     191  ]   
     192  destruct >EQfetch in EQ; whd in ⊢ (??%% → ?); #EQ
     193  lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct % //
     194| #s1 #s2 #l inversion(fetch ???) normalize nodelta
     195  [ #_ #EQ destruct] * normalize nodelta
     196  [ #seq #lbl #_
     197  | #n #_
     198  | #cond #newpc #ltrue #lfalse #_
     199  | #lin #io #lout #EQfetch inversion (asm_is_io ??) #EQio normalize nodelta
     200  | #f #_
     201  | #_
     202  ]
     203  #EQ destruct * #_ #H inversion H in ⊢ ?;
     204  [ #st1 #st2 #i #lbl #EQf #EQio1 #H2 #H3 #H4 #EQio2 #H6 #H7 #H8 #H9 #H10 #H11
     205  | #st1 #st2 #new_pc #EQf #EQio1 #H13 #H14 #H15 #EQio2 #H17 #H18 #H19 #H20 #H21 #H22
     206  | #st1 #st2 #cond1 #new_pc1 #ltrue1 #lfalse1 #ev_c #EQf #EQio1 #H26 #H27 #H28 #EQio2 #H30 #H31 #H32 #H33 #H34 #H35
     207  | #st1 #st2 #cond1 #new_pc1 #ltrue1 #lfalse1 #ev_c #EQf #EQio1 #H38 #H39 #H40 #EQio2 #H42 #H43 #H44 #H45 #H46 #H47
     208  | #st1 #st2 #lin #io #lout #EQf #EQio1 #H50 #H51 #H52 #EQio2 #H54 #H55 #H56 #H57 #H58 #H59
     209  | #st1 #st2 #lin #io #lout #EQf #EQio1 #H61 #H62 #H63 #EQio2 #H65 #H66 #H67 #H68 #H69 #H70
     210  | #st1 #st2 #f #EQf #EQio1 #H74 #H75 #H76 #EQio2 #H78 #H79 #H80 #H81 #H82 #H83
     211  | #st1 #st2 #new_pc #EQf #EQio1 #H86 #H87 #H88 #EQio2 #H90 #H91 #H92 #H93 #H94 #H95
     212  ]   
     213  destruct >EQio in EQio2; >EQio1 #EQ destruct %{lin} //
     214|  #s1 #s2 #l inversion(fetch ???) normalize nodelta
     215  [ #_ #EQ destruct] * normalize nodelta
     216  [ #seq #lbl #_
     217  | #n #_
     218  | #cond #newpc #ltrue #lfalse #EQfetch
     219  | #lin #io #lout #EQfetch cases (asm_is_io ??) normalize nodelta
     220  | #f #_
     221  | #_
     222  ]
     223  #EQ destruct * #_ #H inversion H in ⊢ ?;
     224  [ #st1 #st2 #i #lbl #EQ #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 #H9 #H10 #H11
     225  | #st1 #st2 #new_pc #EQ #H13 #H14 #H15 #H16 #H17 #H18 #H19 #H20 #H21 #H22 #H23
     226  | #st1 #st2 #cond1 #new_pc1 #ltrue1 #lfalse1 #ev_c #EQ #H25 #H26 #H27 #H28 #H29 #H30 #H31 #H32 #H33 #H34 #H35
     227  | #st1 #st2 #cond1 #new_pc1 #ltrue1 #lfalse1 #ev_c #EQ #H37 #H38 #H39 #H40 #H41 #H42 #H43 #H44 #H45 #H46 #H47
     228  | #st1 #st2 #lin1 #io1 #lout1 #EQ #H49 #H50 #H51 #H52 #H53 #H54 #H55 #H56 #H57 #H58 #H59
     229  | #st1 #st2 #lin1 #io1 #lout1 #EQ #H61 #H62 #H63 #H64 #H65 #H66 #H67 #H68 #H69 #H70 #H71
     230  | #st1 #st2 #f #EQ #H73 #H74 #H75 #H76 #H77 #H78 #H79 #H80 #H81 #H82 #H83
     231  | #st1 #st2 #new_pc #EQ #H85 #H86 #H87 #H88 #H89 #H90 #H91 #H92 #H93 #H94 #H95
     232  ]   
     233  destruct >EQfetch in EQ; whd in ⊢ (??%% → ?); #EQ
     234  lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct % //
     235]*)
     236qed.
     237
     238definition emits_labels ≝
     239λp.λinstr : AssemblerInstr p.match instr with
     240        [ Seq _ opt_l ⇒ match opt_l with
     241                        [ None ⇒ Some ? (λpc.S pc)
     242                        | Some _ ⇒ None ?
     243                        ]
     244        | Ijmp newpc ⇒ Some ? (λ_.newpc)
     245        | _ ⇒ None ?
     246        ].
     247
     248
     249let rec block_cost (p : assembler_params) (p' : sem_params p)
     250 (prog: AssemblerProgram p) (program_counter: ℕ)
     251    (program_size: ℕ)
     252        on program_size: option (m … p') ≝
     253match program_size with
     254  [ O ⇒ None ?
     255  | S program_size' ⇒
     256    if eqb program_counter (\snd prog) then
     257       return e … (m … p')
     258    else
     259    ! instr ← fetch … prog program_counter;
     260    ! n ← (match emits_labels … instr with
     261          [ Some f ⇒ block_cost … prog (f program_counter) program_size'
     262          | None ⇒ return e …
     263          ]);
     264    return (op … (m … p') (cost_of p p' instr) n)
     265  ].
     266 
     267axiom initial_act : CostLabel.
     268 
     269record cost_map_T (dom : DeqSet) (codom : Type[0]) : Type[1] ≝
     270{ map_type :> Type[0]
     271; empty_map : map_type
     272; get_map : map_type → dom → option codom
     273; set_map : map_type → dom → codom → map_type
     274; get_set_hit : ∀k,v,m.get_map (set_map m k v) k = return v
     275; get_set_miss : ∀k1,k2,v,m.(k1 == k2) = false → get_map (set_map m k1 v) k2 = get_map m k2
     276}.
     277
     278let rec labels_pc (p : assembler_params)
     279(prog : list (AssemblerInstr p)) (program_counter : ℕ) on prog : list (CostLabel × ℕ) ≝
     280match prog with
     281[ nil ⇒ [〈initial_act,O〉] @
     282        map … (λx.let〈y,z〉 ≝ x in 〈a_call z,y〉) (call_label_fun … p) @
     283        map … (λx.let〈y,z〉 ≝ x in 〈a_return_post z,y〉) (return_label_fun … p)
     284| cons i is ⇒
     285  match i with
     286  [ Seq _ opt_l ⇒ match opt_l with
     287                  [ Some lbl ⇒ [〈a_non_functional_label lbl,S program_counter〉]
     288                  | None ⇒ [ ]
     289                  ]
     290  | Ijmp _ ⇒ [ ]
     291  | CJump _ newpc ltrue lfalse ⇒ [〈a_non_functional_label ltrue,newpc〉;〈a_non_functional_label lfalse,S program_counter〉]
     292  | Iio lin _ lout ⇒ [〈a_non_functional_label lout,S program_counter〉]
     293  | Icall f ⇒ [ ]
     294  | Iret ⇒ [ ]
     295  ] @ labels_pc p is (S program_counter)             
     296].
     297
     298definition static_analisys : ∀p : assembler_params.∀ p' : sem_params p.
     299∀mT : cost_map_T DEQCostLabel (m … p').AssemblerProgram p → option mT ≝
     300λp,p',mT,prog.
     301let 〈instrs,final〉 ≝ prog in
     302let prog_size ≝ S (|instrs|) in
     303m_fold Option ?? (λx,m.let 〈z,w〉≝ x in ! k ← block_cost … prog w prog_size; 
     304                               return set_map … m z k) (labels_pc … instrs O)
     305      (empty_map ?? mT).
     306
     307(*falso: necessita di no_duplicates*)
     308axiom static_analisys_ok : ∀p,p',mT,prog,lbl,pc,map.
     309static_analisys p p' mT prog = return map →
     310mem … 〈lbl,pc〉 (labels_pc … (\fst prog) O) →
     311get_map … map lbl = block_cost … prog pc (S (|(\fst prog)|)). 
     312
     313include "Simulation.ma".
     314
     315record terminated_trace (S : abstract_status) (L_s1,R_s2) (trace: raw_trace S L_s1 R_s2)
     316 : Prop ≝
     317 { R_label : option ActionLabel
     318 ; R_post_state : option S
     319 ; R_fin_ok : match R_label with
     320               [ None ⇒ bool_to_Prop (as_final … R_s2) ∧ R_post_state = None ?
     321               | Some l ⇒ (is_costlabelled_act l ∨ is_unlabelled_ret_act l) ∧
     322                          (is_call_act l → bool_to_Prop (is_call_post_label … R_s2)) ∧
     323                          ∃ s'.R_post_state = Some ? s' ∧ as_execute … l R_s2 s'
     324               ]
     325 }.
     326 
     327lemma bind_inversion : ∀A,B : Type[0].∀m : option A.
     328∀f : A → option B.∀y : B.
     329! x ← m; f x = return y →
     330∃ x.(m = return x) ∧ (f x = return y).
     331#A #B * [| #a] #f #y normalize #EQ [destruct]
     332%{a} %{(refl …)} //
     333qed.
     334
     335lemma static_dynamic : ∀p,p',prog,k,mT,map.
     336static_analisys p p' mT prog = return map →
     337∀st1,st2 : vm_state p p'.∀t : raw_trace (asm_operational_semantics p p' prog) … st1 st2.
     338pre_measurable_trace … t → terminated_trace … t →
     339block_cost … prog (pc … st1) (S (|(\fst prog)|)) = return k →
     340op … (m … p') (cost … st1)
     341 (foldr ?? (λlbl,k1.op … (opt_safe … (get_map … map lbl) ?) k1)
     342     k (get_costlabels_of_trace … t)) = cost … st2.
     343[2: cases daemon]
     344#p #p' #prog #k #mT #map #EQmap #st1 #st2 #t elim t
     345[ #st #_ ** [|#r_lab] normalize nodelta #opt_r_state
     346  [ * whd in ⊢ (?% → ?); #final_st #_ whd in ⊢ (??%? → ?); >final_st
     347    normalize nodelta whd in ⊢ (??%% → ?); #EQ destruct(EQ)
     348    >neutral %
     349  | ** #H1 #H2 * #post_st * #EQ destruct * #H3 #H4 whd in ⊢ (??%? → ?);
     350    >H3 normalize nodelta #H cases(bind_inversion ????? H) -H
     351    #i * #EQi #H cases(bind_inversion ????? H) -H #el
     352    inversion H4
     353    [ #s1 #s2 #i1 * [| #lbl] #EQfetch #no_io #EQstore #EQstack #EQio #EQpc
     354      #EQcost #EQ1 #EQ2 #EQ3 #EQ4 destruct >EQi in EQfetch; whd in ⊢ (??%% → ?);
     355      #EQ destruct whd in match emits_labels; normalize nodelta
     356      [ cases H1 whd in ⊢ (% → ?); [ * |  #EQ destruct]]
     357      * whd in ⊢ (??%% → ?); #EQ destruct >neutral whd in ⊢ (??%% → ?);
     358      #EQ destruct whd in match (foldr ?????);
     359
     360
     361
     362
Note: See TracChangeset for help on using the changeset viewer.