Changeset 3500 for LTS


Ignore:
Timestamp:
Sep 25, 2014, 6:50:51 PM (5 years ago)
Author:
sacerdot
Message:

Nicer statements.

Location:
LTS
Files:
2 edited

Legend:

Unmodified
Added
Removed
  • LTS/Vm.ma

    r3499 r3500  
    335335| STATE : vm_state p p' → vm_ass_state p p'.
    336336
    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
    341                 (vm_ass_state p p')
    342                 (λl.λs1,s2 : vm_ass_state p p'.
     337definition ass_vmstep ≝
     338 λp,p',prog.
     339  λl.λs1,s2 : vm_ass_state p p'.
    343340                    match s1 with
    344341                    [ STATE st1 ⇒
     
    347344                            (eqb (pc ?? st1) (endmain … prog)) = false ∧ vmstep p p' prog l st1 st2
    348345                        | INITIAL ⇒ False
    349                         | FINAL ⇒ eqb (pc … st1) (endmain … prog) = true ∧ l = end_act
     346                        | FINAL ⇒ eqb (pc … st1) (endmain … prog) = true ∧
     347                           l = cost_act (Some … (in_act … prog))
    350348                        ]
    351349                    | INITIAL ⇒ match s2 with
    352                                 [ STATE st2 ⇒ eqb (pc … st2) O = true ∧ l = init_act
     350                                [ STATE st2 ⇒ eqb (pc … st2) O = true ∧
     351                                   l = cost_act (Some … (in_act … prog))
    353352                                | _ ⇒ False
    354353                                ]
    355354                    | FINAL ⇒ False
    356                     ])
     355                    ].
     356
     357definition asm_operational_semantics : ∀p.sem_params p → AssemblerProgram p →  abstract_status ≝
     358λp,p',prog.let init_act ≝ cost_act (Some ? (in_act … prog)) in
     359           let end_act ≝ cost_act (Some ? (in_act … prog)) in
     360    mk_abstract_status
     361                (vm_ass_state p p')
     362                (ass_vmstep … prog)
    357363                (λ_.λ_.True)
    358364                (λst.match st with
     
    458464λp,p',prog,st.fetch … prog (pc … st).
    459465
    460 definition asm_static_analisys_data ≝ λp,p',prog,abs_t,instr_m.
    461 mk_static_analysis_data (asm_concrete_trans_sys p p' prog) abs_t (option (AssemblerInstr p))
    462  (λs.match s with [ STATE st ⇒ if eqb (pc … st) (endmain … prog) then
     466record asm_galois_connection (p: assembler_params) (p': sem_params p) (prog: AssemblerProgram p) : Type[2] ≝
     467{ aabs_d : abstract_transition_sys (m … p')
     468; agalois_rel:> galois_rel (asm_concrete_trans_sys p p' prog) aabs_d
     469}.
     470
     471definition galois_connection_of_asm_galois_connection:
     472 ∀p,p',prog. asm_galois_connection p p' prog → galois_connection ≝
     473 λp,p',prog,agc.
     474  mk_galois_connection
     475   (asm_concrete_trans_sys p p' prog)
     476   (aabs_d … agc)
     477   (agalois_rel … agc).
     478
     479coercion galois_connection_of_asm_galois_connection.
     480
     481definition ass_fetch ≝
     482 λp,p',prog.
     483    λs.match s with [ STATE st ⇒ if eqb (pc … st) (endmain … prog) then
    463484                                   Some ? (None ?)
    464485                               else ! x ← fetch_state p p' prog st; Some ? (Some ? x)
    465                   | INITIAL ⇒ Some ? (None ?)
    466                   | FINAL  ⇒ None ? ]) instr_m.
     486                    | INITIAL ⇒ Some ? (None ?)
     487                    | FINAL  ⇒ None ? ].
     488
     489definition ass_instr_map ≝
     490 λp,p',prog.λasm_galois_conn: asm_galois_connection p p' prog.
     491  λinstr_map: AssemblerInstr p → (*option*) (abs_instr … (abs_d asm_galois_conn)).
     492  (λi.match i with [None ⇒ (*Some …*) (e …) |Some x ⇒ instr_map … x]).
     493
     494record asm_abstract_interpretation (p: assembler_params) (p': sem_params p) (prog: AssemblerProgram p) : Type[2] ≝
     495{ asm_galois_conn: asm_galois_connection p p' prog
     496; instr_map : AssemblerInstr p → (*option*) (abs_instr … (abs_d asm_galois_conn))
     497; instr_map_ok :
     498   ∀s,s': concr … asm_galois_conn. ∀a: abs_d … asm_galois_conn.∀l,i.
     499    as_execute … l s s' →
     500     ass_fetch … prog s = Some ? i →
     501      ∀I. ass_instr_map … instr_map i = (*Some ?*) I →
     502       asm_galois_conn s a → asm_galois_conn s' (〚I〛 a)
     503}.
     504
     505definition abstract_interpretation_of_asm_abstract_interpretation:
     506 ∀p,p',prog. asm_abstract_interpretation p p' prog → abstract_interpretation
     507
     508λp,p',prog,aai.
     509 mk_abstract_interpretation
     510  (asm_galois_conn … aai) (option (AssemblerInstr p)) (ass_fetch p p' prog)
     511   (ass_instr_map … prog … (instr_map … aai)) (instr_map_ok … aai).
     512
     513coercion abstract_interpretation_of_asm_abstract_interpretation.
    467514
    468515definition non_empty_list : ∀A.list A → bool ≝
     
    883930qed.
    884931
    885 notation "〚 term 19 C 〛 term 90 A" with precedence 10 for @{ 'sem $C $A }.
    886 interpretation "act_abs" 'sem f x = (act ?? (act_abs ??) f x).
    887 
    888932coercion big_op : ∀M:monoid. ∀l: list M. M ≝ big_op on _l: list ? to ?.
    889933
     
    893937
    894938(* Given a Galois connection to an abstract transition system *)
    895 ∀abs_t : abstract_transition_sys (m … p').
    896 ∀instr_m : (AssemblerInstr p) → abs_instr … abs_t.
    897 ∀R : static_galois … (asm_static_analisys_data … prog …
    898  (λi.match i with [None ⇒ e …
    899                   |Some x ⇒ instr_m x
    900                   ])).
     939∀R: asm_abstract_interpretation p p' prog.
    901940
    902941(* If the static analysis does not fail *)
    903 ∀mT,map1. ∀EQmap : static_analisys … instr_m mT prog = return map1.
     942∀mT,map1. ∀EQmap : static_analisys … (instr_map … R) mT prog = return map1.
    904943
    905944(* For every pre_measurable, terminated trace *)
     
    912951(* Let k be the statically computed abstract action of the prefix of the trace
    913952   up to the first label *)
    914 ∀k.block_cost p prog … instr_m (get_pc … st1 (endmain … prog)) (S (|(instructions … prog)|)) = return k →
     953∀k.block_cost p prog … (instr_map … R) (get_pc … st1 (endmain … prog)) (S (|(instructions … prog)|)) = return k →
    915954
    916955(* Let abs_actions be the list of statically computed abstract actions
     
    933972    @(proj2 … (static_analisys_ok … EQmap … Hmem))
    934973]
    935 #p #p' #prog #abs_t #instr_m #good #mT #map1 #EQmap #st1 #st2 #t * #st3 * #t1 *
     974#p #p' #prog #R #mT #map1 #EQmap #st1 #st2 #t * #st3 * #t1 *
    936975#l1 * #prf1 * #EQ destruct #Hlabelled
    937976>(rewrite_in_dependent_map ??? (get_costlabels_of_trace … t1))
     
    943982  |2: whd in ⊢ (??%% → ?); #EQ destruct #labels whd in ⊢ (??%% → ?); #EQlabels
    944983      #a1 #rel_fin
    945       lapply(instr_map_ok … good … prf … rel_fin) [ %|] cases st2 in prf; -st2 [3: #st2] *
     984      lapply(instr_map_ok … R … prf … (refl …) rel_fin) [ %|] cases st2 in prf; -st2 [3: #st2] *
    946985      #EQpc #EQ destruct #H >act_neutral >act_neutral normalize in H;
    947986      <(act_neutral … (act_abs …) a1) @H
     
    951990      normalize nodelta * >EQpc @eqb_elim [2,4: * #ABS @⊥ @ABS %] #_ #EQ destruct
    952991      #EQ destruct whd in EQc : (??%%); destruct
    953       lapply(instr_map_ok …  good … good_st_a1)
    954       [5: @(FINAL …)
    955       |2: whd % [ >EQpc @eqb_elim // * #ABS @⊥ @ABS %] %
    956       | whd in ⊢ (??%%); @eqb_elim [2: * #ABS @⊥ @ABS assumption
    957       ]
    958       #_ normalize nodelta % | | | whd in ⊢ (% → ?); >act_neutral //
    959       ]
     992      lapply(instr_map_ok … R … (refl …) good_st_a1)
     993      [5: @(FINAL …)
     994      |2: whd % [2: % | // ]
     995      | whd whd in ⊢ (??%%); @eqb_elim [2: * #ABS @⊥ @ABS assumption | #_ % ]
     996      |3,4: skip]
     997      whd in ⊢ (% → ?); >act_neutral #H @H
    960998  | #Hpc lapply prf whd in ⊢ (% → ?); cases st2 in prf; -st2 [3: #st2] #prf
    961999    normalize nodelta [2:* |3: * #ABS @⊥ lapply ABS -ABS @eqb_elim
     
    9821020    whd in match (dependent_map ????); #costs #EQ destruct #a1 #good_st_a1
    9831021    >neutral_r >act_neutral
    984     lapply(instr_map_ok … good … good_st_a1)
     1022    lapply(instr_map_ok R … (refl …) good_st_a1)
    9851023    [1,7,13,19,25,31,37: whd in ⊢ (??%%); @eqb_elim normalize nodelta
    9861024      [1,3,5,7,9,11,13: #EQ cases(absurd ? EQ Hpc) ] #_ whd in match fetch_state;
     
    9891027        | >EQfetch in ⊢ (??%?); | >EQfetch in ⊢ (??%?); | >EQfetch in ⊢ (??%?);
    9901028        | >EQfetch in ⊢ (??%?); ] %
    991       |3,9,15,21,27,33,39: skip |*: try assumption // ]
    992       ]
    993     ]
     1029      |3,9,15,21,27,33,39: skip |*: try assumption // ]]]
    9941030| -st1 * [3: #st1] #st3 #st4 #l [3: *] cases st3 -st3
    9951031  [1,2,4,5: * #H1 #H2 #tl #_ #l1 #exe @⊥ lapply tl -tl lapply(refl ? (FINAL p p'))
     
    10221058  [2: cases(static_analisys_ok … c … (pc … st3) … EQmap) // #EQ #_ <EQ whd in match (big_op ??);
    10231059      >neutral_l assumption
    1024    |3,6: [ >neutral_r] lapply(instr_map_ok … good … good_a1)
     1060   |3,6: [ >neutral_r] lapply(instr_map_ok R … (refl …) good_a1)
    10251061       [1,7: whd in ⊢ (??%?); @eqb_elim
    10261062         [1,3: #ABS cases(absurd ? ABS Hpc) ] #_ normalize nodelta whd in match fetch_state;
     
    10601096      [2: lapply EQpc_st3 @eqb_elim [2: #_ #EQ destruct] #EQ #_ >EQ @i_act_in_map ]
    10611097      #EQ #_ <EQ whd in match (big_op ??); >neutral_l assumption
    1062    |  lapply(instr_map_ok … good … good_a1)
     1098   |  lapply(instr_map_ok R … (refl …) good_a1)
    10631099     [1: % | assumption |*:] normalize in ⊢ (% → ?); #H @H
    10641100   ]
  • LTS/costs.ma

    r3458 r3500  
    4343}.
    4444
    45 record galois_conn (C : concrete_transition_sys)
     45notation "〚 term 19 C 〛 term 90 A" with precedence 10 for @{ 'sem $C $A }.
     46interpretation "act_abs" 'sem f x = (act ?? (act_abs ??) f x).
     47
     48record galois_rel (C : concrete_transition_sys)
    4649                   (A : abstract_transition_sys (cost_mon C)) : Type[0] ≝
    4750{ rel_galois :2> C → A → Prop
    4851; rel_galois_cost : ∀s,a.rel_galois … s a → abs_cost … a = cost_of … s
    49 ; rel_galois_prop : ∀s,s' : C.∀a : A.∀l.as_execute … l s s' → rel_galois … s a →
    50                     ∃i : abs_instr … A.∃a' : A.rel_galois … s' a' ∧
    51                                                act_abs ?? i a = a'
    5252}.
    5353
    54 record static_analysis_data : Type[2] ≝
     54record galois_connection : Type[2] ≝
    5555{ concr : concrete_transition_sys
    5656; abs_d : abstract_transition_sys (cost_mon concr)
    57 ; instr_t : Type[0]
    58 ; fetch : concr → option instr_t
    59 ; instr_map : instr_t → abs_instr … abs_d
     57; galois_rel:> galois_rel concr abs_d
    6058}.
    6159
    62 
    63 record static_galois (p : static_analysis_data) : Type[0] ≝
    64 { good :> galois_conn (concr … p) (abs_d … p)
    65 ; instr_map_ok : ∀s,s' : (concr … p).∀a : (abs_d … p).∀l,i.as_execute … l s s' →
    66                 fetch … p s = Some ? i →
    67                 rel_galois … good s a →
    68                 rel_galois … good s' (act_abs … (instr_map … p i) a)
     60record abstract_interpretation : Type[2] ≝
     61{ galois_conn:> galois_connection
     62; instr_t : Type[0]
     63; fetch : concr galois_conn → option instr_t
     64; instr_map : instr_t → abs_instr … (abs_d galois_conn)
     65; instr_map_ok :
     66   ∀s,s': concr … galois_conn. ∀a: abs_d … galois_conn.∀l,i.
     67    as_execute … l s s' →
     68     fetch … s = Some ? i →
     69      ∀I. instr_map … i = I →
     70       galois_conn s a → galois_conn s' (〚I〛 a)
    6971}.
    70 
    71 
    72 
    73 
Note: See TracChangeset for help on using the changeset viewer.