Changeset 3500

Timestamp:

Sep 25, 2014, 6:50:51 PM (5 years ago)

Author:

sacerdot

Message:

Nicer statements.

Location:

LTS

Files:

• Vm.ma (modified) (13 diffs)
• costs.ma (modified) (1 diff)

LTS/Vm.ma

@@ -335 +335 @@
 | STATE : vm_state p p' → vm_ass_state p p'.
 
-definition asm_operational_semantics : ∀p.sem_params p → AssemblerProgram p →  abstract_status ≝ 
-λp,p',prog.let init_act ≝ cost_act (Some ? (in_act … prog)) in
-           let end_act ≝ cost_act (Some ? (in_act … prog)) in
-    mk_abstract_status 
-                (vm_ass_state p p') 
-                (λl.λs1,s2 : vm_ass_state p p'.
+definition ass_vmstep ≝
+ λp,p',prog.
+  λl.λs1,s2 : vm_ass_state p p'.
                     match s1 with 
                     [ STATE st1 ⇒ 
@@ -347 +344 @@
                             (eqb (pc ?? st1) (endmain … prog)) = false ∧ vmstep p p' prog l st1 st2
                         | INITIAL ⇒ False
-                        | FINAL ⇒ eqb (pc … st1) (endmain … prog) = true ∧ l = end_act
+                        | FINAL ⇒ eqb (pc … st1) (endmain … prog) = true ∧
+                           l = cost_act (Some … (in_act … prog))
                         ]
                     | INITIAL ⇒ match s2 with
-                                [ STATE st2 ⇒ eqb (pc … st2) O = true ∧ l = init_act 
+                                [ STATE st2 ⇒ eqb (pc … st2) O = true ∧
+                                   l = cost_act (Some … (in_act … prog))
                                 | _ ⇒ False
                                 ]
                     | FINAL ⇒ False
-                    ])
+                    ].
+
+definition asm_operational_semantics : ∀p.sem_params p → AssemblerProgram p →  abstract_status ≝ 
+λp,p',prog.let init_act ≝ cost_act (Some ? (in_act … prog)) in
+           let end_act ≝ cost_act (Some ? (in_act … prog)) in
+    mk_abstract_status 
+                (vm_ass_state p p')
+                (ass_vmstep … prog)
                 (λ_.λ_.True)
                 (λst.match st with 
@@ -458 +464 @@
 λp,p',prog,st.fetch … prog (pc … st).
 
-definition asm_static_analisys_data ≝ λp,p',prog,abs_t,instr_m.
-mk_static_analysis_data (asm_concrete_trans_sys p p' prog) abs_t (option (AssemblerInstr p))
- (λs.match s with [ STATE st ⇒ if eqb (pc … st) (endmain … prog) then
+record asm_galois_connection (p: assembler_params) (p': sem_params p) (prog: AssemblerProgram p) : Type[2] ≝
+{ aabs_d : abstract_transition_sys (m … p')
+; agalois_rel:> galois_rel (asm_concrete_trans_sys p p' prog) aabs_d
+}.
+
+definition galois_connection_of_asm_galois_connection:
+ ∀p,p',prog. asm_galois_connection p p' prog → galois_connection ≝
+ λp,p',prog,agc.
+  mk_galois_connection
+   (asm_concrete_trans_sys p p' prog)
+   (aabs_d … agc)
+   (agalois_rel … agc).
+
+coercion galois_connection_of_asm_galois_connection.
+
+definition ass_fetch ≝
+ λp,p',prog.
+    λs.match s with [ STATE st ⇒ if eqb (pc … st) (endmain … prog) then
                                    Some ? (None ?) 
                                else ! x ← fetch_state p p' prog st; Some ? (Some ? x) 
-                  | INITIAL ⇒ Some ? (None ?)
-                  | FINAL  ⇒ None ? ]) instr_m.
+                    | INITIAL ⇒ Some ? (None ?)
+                    | FINAL  ⇒ None ? ].
+
+definition ass_instr_map ≝
+ λp,p',prog.λasm_galois_conn: asm_galois_connection p p' prog.
+  λinstr_map: AssemblerInstr p → (*option*) (abs_instr … (abs_d asm_galois_conn)).
+  (λi.match i with [None ⇒ (*Some …*) (e …) |Some x ⇒ instr_map … x]).
+
+record asm_abstract_interpretation (p: assembler_params) (p': sem_params p) (prog: AssemblerProgram p) : Type[2] ≝
+{ asm_galois_conn: asm_galois_connection p p' prog
+; instr_map : AssemblerInstr p → (*option*) (abs_instr … (abs_d asm_galois_conn))
+; instr_map_ok :
+   ∀s,s': concr … asm_galois_conn. ∀a: abs_d … asm_galois_conn.∀l,i.
+    as_execute … l s s' → 
+     ass_fetch … prog s = Some ? i →
+      ∀I. ass_instr_map … instr_map i = (*Some ?*) I →
+       asm_galois_conn s a → asm_galois_conn s' (〚I〛 a)
+}.
+
+definition abstract_interpretation_of_asm_abstract_interpretation:
+ ∀p,p',prog. asm_abstract_interpretation p p' prog → abstract_interpretation
+≝
+λp,p',prog,aai.
+ mk_abstract_interpretation
+  (asm_galois_conn … aai) (option (AssemblerInstr p)) (ass_fetch p p' prog)
+   (ass_instr_map … prog … (instr_map … aai)) (instr_map_ok … aai).
+
+coercion abstract_interpretation_of_asm_abstract_interpretation.
 
 definition non_empty_list : ∀A.list A → bool ≝ 
@@ -883 +930 @@
 qed.
 
-notation "〚 term 19 C 〛 term 90 A" with precedence 10 for @{ 'sem $C $A }.
-interpretation "act_abs" 'sem f x = (act ?? (act_abs ??) f x).
-
 coercion big_op : ∀M:monoid. ∀l: list M. M ≝ big_op on _l: list ? to ?.
 
@@ -893 +937 @@
 
 (* Given a Galois connection to an abstract transition system *)
-∀abs_t : abstract_transition_sys (m … p').
-∀instr_m : (AssemblerInstr p) → abs_instr … abs_t.
-∀R : static_galois … (asm_static_analisys_data … prog …
- (λi.match i with [None ⇒ e … 
-                  |Some x ⇒ instr_m x
-                  ])).
+∀R: asm_abstract_interpretation p p' prog.
 
 (* If the static analysis does not fail *)
-∀mT,map1. ∀EQmap : static_analisys … instr_m mT prog = return map1.
+∀mT,map1. ∀EQmap : static_analisys … (instr_map … R) mT prog = return map1.
 
 (* For every pre_measurable, terminated trace *)
@@ -912 +951 @@
 (* Let k be the statically computed abstract action of the prefix of the trace
    up to the first label *)
-∀k.block_cost p prog … instr_m (get_pc … st1 (endmain … prog)) (S (|(instructions … prog)|)) = return k →
+∀k.block_cost p prog … (instr_map … R) (get_pc … st1 (endmain … prog)) (S (|(instructions … prog)|)) = return k →
 
 (* Let abs_actions be the list of statically computed abstract actions
@@ -933 +972 @@
     @(proj2 … (static_analisys_ok … EQmap … Hmem))
 ]
-#p #p' #prog #abs_t #instr_m #good #mT #map1 #EQmap #st1 #st2 #t * #st3 * #t1 *
+#p #p' #prog #R #mT #map1 #EQmap #st1 #st2 #t * #st3 * #t1 *
 #l1 * #prf1 * #EQ destruct #Hlabelled
 >(rewrite_in_dependent_map ??? (get_costlabels_of_trace … t1))
@@ -943 +982 @@
   |2: whd in ⊢ (??%% → ?); #EQ destruct #labels whd in ⊢ (??%% → ?); #EQlabels
       #a1 #rel_fin
-      lapply(instr_map_ok … good … prf … rel_fin) [ %|] cases st2 in prf; -st2 [3: #st2] *
+      lapply(instr_map_ok … R … prf … (refl …) rel_fin) [ %|] cases st2 in prf; -st2 [3: #st2] *
       #EQpc #EQ destruct #H >act_neutral >act_neutral normalize in H;
       <(act_neutral … (act_abs …) a1) @H
@@ -951 +990 @@
       normalize nodelta * >EQpc @eqb_elim [2,4: * #ABS @⊥ @ABS %] #_ #EQ destruct
       #EQ destruct whd in EQc : (??%%); destruct
-      lapply(instr_map_ok …  good … good_st_a1)
-      [5: @(FINAL …) 
-      |2: whd % [ >EQpc @eqb_elim // * #ABS @⊥ @ABS %] %
-      | whd in ⊢ (??%%); @eqb_elim [2: * #ABS @⊥ @ABS assumption 
-      ]
-      #_ normalize nodelta % | | | whd in ⊢ (% → ?); >act_neutral // 
-      ]
+      lapply(instr_map_ok … R … (refl …) good_st_a1)
+      [5: @(FINAL …)
+      |2: whd % [2: % | // ]
+      | whd whd in ⊢ (??%%); @eqb_elim [2: * #ABS @⊥ @ABS assumption | #_ % ]
+      |3,4: skip]
+      whd in ⊢ (% → ?); >act_neutral #H @H
   | #Hpc lapply prf whd in ⊢ (% → ?); cases st2 in prf; -st2 [3: #st2] #prf
     normalize nodelta [2:* |3: * #ABS @⊥ lapply ABS -ABS @eqb_elim
@@ -982 +1020 @@
     whd in match (dependent_map ????); #costs #EQ destruct #a1 #good_st_a1
     >neutral_r >act_neutral
-    lapply(instr_map_ok … good … good_st_a1) 
+    lapply(instr_map_ok R … (refl …) good_st_a1)
     [1,7,13,19,25,31,37: whd in ⊢ (??%%); @eqb_elim normalize nodelta
       [1,3,5,7,9,11,13: #EQ cases(absurd ? EQ Hpc) ] #_ whd in match fetch_state;
@@ -989 +1027 @@
         | >EQfetch in ⊢ (??%?); | >EQfetch in ⊢ (??%?); | >EQfetch in ⊢ (??%?);
         | >EQfetch in ⊢ (??%?); ] %
-      |3,9,15,21,27,33,39: skip |*: try assumption // ]
-      ]
-    ]
+      |3,9,15,21,27,33,39: skip |*: try assumption // ]]]
 | -st1 * [3: #st1] #st3 #st4 #l [3: *] cases st3 -st3
   [1,2,4,5: * #H1 #H2 #tl #_ #l1 #exe @⊥ lapply tl -tl lapply(refl ? (FINAL p p'))
@@ -1022 +1058 @@
   [2: cases(static_analisys_ok … c … (pc … st3) … EQmap) // #EQ #_ <EQ whd in match (big_op ??);
       >neutral_l assumption
-   |3,6: [ >neutral_r] lapply(instr_map_ok … good … good_a1) 
+   |3,6: [ >neutral_r] lapply(instr_map_ok R … (refl …) good_a1) 
        [1,7: whd in ⊢ (??%?); @eqb_elim
          [1,3: #ABS cases(absurd ? ABS Hpc) ] #_ normalize nodelta whd in match fetch_state;
@@ -1060 +1096 @@
       [2: lapply EQpc_st3 @eqb_elim [2: #_ #EQ destruct] #EQ #_ >EQ @i_act_in_map ]
       #EQ #_ <EQ whd in match (big_op ??); >neutral_l assumption
-   |  lapply(instr_map_ok … good … good_a1) 
+   |  lapply(instr_map_ok R … (refl …) good_a1) 
      [1: % | assumption |*:] normalize in ⊢ (% → ?); #H @H
    ]

LTS/costs.ma

@@ -43 +43 @@
 }.
 
-record galois_conn (C : concrete_transition_sys) 
+notation "〚 term 19 C 〛 term 90 A" with precedence 10 for @{ 'sem $C $A }.
+interpretation "act_abs" 'sem f x = (act ?? (act_abs ??) f x).
+
+record galois_rel (C : concrete_transition_sys) 
                    (A : abstract_transition_sys (cost_mon C)) : Type[0] ≝ 
 { rel_galois :2> C → A → Prop
 ; rel_galois_cost : ∀s,a.rel_galois … s a → abs_cost … a = cost_of … s
-; rel_galois_prop : ∀s,s' : C.∀a : A.∀l.as_execute … l s s' → rel_galois … s a → 
-                    ∃i : abs_instr … A.∃a' : A.rel_galois … s' a' ∧
-                                               act_abs ?? i a = a'
 }.
 
-record static_analysis_data : Type[2] ≝ 
+record galois_connection : Type[2] ≝ 
 { concr : concrete_transition_sys
 ; abs_d : abstract_transition_sys (cost_mon concr)
-; instr_t : Type[0]
-; fetch : concr → option instr_t
-; instr_map : instr_t → abs_instr … abs_d
+; galois_rel:> galois_rel concr abs_d
 }.
 
-
-record static_galois (p : static_analysis_data) : Type[0] ≝ 
-{ good :> galois_conn (concr … p) (abs_d … p) 
-; instr_map_ok : ∀s,s' : (concr … p).∀a : (abs_d … p).∀l,i.as_execute … l s s' → 
-                fetch … p s = Some ? i → 
-                rel_galois … good s a → 
-                rel_galois … good s' (act_abs … (instr_map … p i) a)
+record abstract_interpretation : Type[2] ≝
+{ galois_conn:> galois_connection
+; instr_t : Type[0]
+; fetch : concr galois_conn → option instr_t
+; instr_map : instr_t → abs_instr … (abs_d galois_conn)
+; instr_map_ok :
+   ∀s,s': concr … galois_conn. ∀a: abs_d … galois_conn.∀l,i.
+    as_execute … l s s' → 
+     fetch … s = Some ? i →
+      ∀I. instr_map … i = I →
+       galois_conn s a → galois_conn s' (〚I〛 a)
 }.
-
-
-
-