Library AnalysersSign

This file contains some extractable analysers and their correctness proofs relative to the abstract semantics.

Set Implicit Arguments.
Require Export Analysers AbstractSign.
Require Export LibList.
Require Export Shared.

Notation " [ ] " := nil : list_scope.
Notation " [ x ] " := (cons x nil) : list_scope.
Notation " [ x ; .. ; y ] " := (cons x .. (cons y nil) ..) : list_scope.

Section General.

Let analyser_result := analyser_result sign_asem.
Coercion sign_analyser_found := analyser_found sign_asem : sign_ares → analyser_result.
Let analyser_correct_modulo := analyser_correct_modulo (asem := sign_asem).
Let analyser_correct := analyser_correct (asem := sign_asem) _ _.
Let correct_analyser_result := correct_analyser_result (asem := sign_asem) _ _.

Definition analyser_match (ar : analyser_result) A (found : sign_ares → A)
    (failed : list (prog × sign_ast) → list (prog × sign_ast × sign_ares) → A) : A :=
  match ar with
  | analyser_found r ⇒ found r
  | analyser_failed lf lo ⇒ failed lf lo
  end.

Instanting the general analyses from Analysers.

The analysers from Analysers are generic and can be used under any semantics, under some minor conditions. Here follows the instantiation of each of these generic analysers and the proof of their respective conditions.

Global Instance abort_ares_decidable : ∀ r,
    Decidable (abort_ares r).
  introv. applys decidable_make
    (decide (sign_ares_expr (⊥♯, ⊤♯) ⊑♯ r ∨ sign_ares_stat (⊥♯, ⊤♯) ⊑♯ r)).
  rewrite decide_spec. apply eq_isTrue. iff A.
   inverts A as A; constructor (exact A).
   inverts× A.
Defined.

Global Instance abort_ast_decidable : ∀ sigma,
    Decidable (abort_ast sigma).
  destruct sigma as [aE|aE ar|aE ar|aE ar|ar|aE ar|ar|aE ar| |];
  try solve [ applys decidable_make false; fold_bool; rew_refl; intro A; inverts A ];
  applys decidable_make (decide (abort_ares ar));
  rewrite decide_spec; apply eq_isTrue; iff A; try solve [ constructors¬ ]; inverts× A.
Defined.

Global Instance sign_acond_Decidable : ∀ n sigma,
    Decidable (sign_acond n sigma).
  destruct n; destruct sigma; typeclass.
Defined.

This function returns the applicable rule names for a given term.

Definition sign_applicable_names (t : prog) (sigma : sign_ast) :=
  'let f := fun n ⇒ decide (sign_acond n sigma) in
  option_map (filter f)
    match t with
    | expr_cst c ⇒
        Some ([ name_cst c ])
    | expr_var x ⇒
        Some ([ name_var x; name_varUndef x ])
    | expr_add e1 e2 ⇒
        Some ([ name_add e1 e2 ])
    | expr_add_1 e2 ⇒
        Some ([ name_add_1 e2; name_abort_ext_expr (expr_add_1 e2) ])
    | expr_add_2 ⇒
        Some ([ name_add_2 ; name_abort_ext_expr expr_add_2 ])
    | stat_skip ⇒
        Some ([ name_skip ])
    | stat_throw ⇒
        Some ([ name_throw ])
    | stat_asgn x e ⇒
        Some ([ name_asgn x e ])
    | stat_asgn_1 x ⇒
        Some ([ name_asgn_1 x; name_abort_ext_stat (stat_asgn_1 x) ])
    | stat_seq s1 s2 ⇒
        Some ([ name_seq s1 s2 ])
    | stat_seq_1 s2 ⇒
        Some ([ name_seq_1 s2; name_abort_ext_stat (stat_seq_1 s2) ])
    | stat_if e s1 s2 ⇒
        Some ([ name_if e s1 s2 ])
    | stat_if_1 s1 s2 ⇒
        Some ([ name_if_1_true s1 s2; name_if_1_false s1 s2;
                name_abort_ext_stat (stat_if_1 s1 s2) ])
    | stat_while e s ⇒
        Some ([ name_while e s ])
    | stat_while_1 e s ⇒
        Some ([ name_while_1 e s; name_abort_ext_stat (stat_while_1 e s) ])
    | stat_while_2 e s ⇒
        Some ([ name_while_2_true e s; name_while_2_false e s;
                name_abort_ext_stat (stat_while_2 e s) ])
    end.

Lemma sign_applicable_names_correct : ∀ l t sigma n,
  sign_applicable_names t sigma = Some l →
  (sign_left n = t ∧ sign_acond n sigma ) ↔ List.In n l.
Proof.
  introv E. unfolds in E. let_name. forwards (l0&E1&E2): option_map_out (rm E). iff I.
   lets (T&C): (rm I). subst l. apply filter_in. splits.
    destruct t as [()|()|()|()]; inverts E1; destruct n; simpls~; tryfalse;
      repeat inverts T; auto¬.
    substs. rewrite decide_spec. rew_refl¬.
   subst l. apply filter_in in I. lets (I0&C): (rm I). substs. splits.
    clear C. destruct t as [()|()|()|()]; inverts E1; destruct n; simpls~; tryfalse;
      repeat inverts I0 as I0; auto¬.
    rewrite decide_spec in C. rew_refl¬ in C.
Qed.

Definition sign_failing_analyser : prog → sign_ast → analyser_result :=
  failing_analyser sign_asem.

Lemma sign_failing_analyser_correct : analyser_correct sign_failing_analyser.
Proof. apply failing_analyser_correct. Qed.

Definition sign_trivial_analyser : prog → sign_ast → analyser_result :=
  trivial_analyser sign_asem _ _.

Lemma sign_trivial_analyser_correct : analyser_correct sign_trivial_analyser.
Proof. applys trivial_analyser_correct sign_arule_format_correct sign_asemantics_full. Qed.

Definition sign_analyse_step : (prog → sign_ast → analyser_result ) → prog → sign_ast → analyser_result :=
  analyse_step (asem := sign_asem) _ _ sign_applicable_names.

Lemma sign_analyse_step_correct : ∀ analyser,
  analyser_correct analyser →
  analyser_correct (sign_analyse_step analyser).
Proof.
  applys analyse_step_correct sign_arule_format_correct sign_asemantics_full sign_applicable_names_correct.
Qed.

Definition sign_analyse_fuel : (prog → sign_ast → analyser_result ) → nat
                             → prog → sign_ast → analyser_result :=
  analyse_fuel (asem := sign_asem) _ _ sign_applicable_names.

Lemma sign_analyse_fuel_correct : ∀ analyser fuel,
  analyser_correct analyser →
  analyser_correct (sign_analyse_fuel analyser fuel).
Proof.
  introv C.
  applys analyse_fuel_correct sign_arule_format_correct sign_asemantics_full sign_applicable_names_correct C.
Qed.

Inductive is_looping_branch : prog → prog → Prop :=
  | is_looping_branch_while : ∀ e s,
    is_looping_branch (stat_while_1 e s) (stat_while_2 e s)
  .

Global Instance is_looping_branch_Decidable : ∀ p1 p2,
  Decidable (is_looping_branch p1 p2).
Proof.
  introv. destruct p1 as [()|()|()|()]; destruct p2 as [()|()|()|()];
    try solve [ applys decidable_make false; fold_bool; rew_refl; intro A; inverts A ].
   applys decidable_make (decide (e = e0 ∧ s = s0)). rewrite decide_def.
   cases_if as I; fold_bool; rew_refl.
    destruct I. substs. constructors.
    intro A. inverts× A.
Qed.

The following lemma basically states that we can iterate on these terms.

A Analyser Matching Types

This analyser always returns ⊤♯, but of the right type. As this is highly dependent on the semantics we are working on, this analyse is not present in Analysers.

Definition sign_type_analyse (p : prog) (sigma : sign_ast) : analyser_result :=
  match p return sign_ares with
  | prog_expr _ | prog_ext_expr _ ⇒ sign_ares_expr (⊤♯)
  | prog_stat _ | prog_ext_stat _ ⇒ sign_ares_stat (⊤♯)
  end.

Lemma sign_type_analyse_correct : analyser_correct sign_type_analyse.
Proof.
  introv E. substs. constructors.
    gen t sigma. cofix D. constructors. introv Eq C. substs.
    destruct n; simpls; (constructors; [apply TopDec.prop| |
      first [
         solve [ eapply aapply_step_Ax; reflexivity ]
       | solve [ eapply aapply_step_R1; try reflexivity; apply D; reflexivity ]
       | eapply aapply_step_R2; try reflexivity; [ apply D; reflexivity | apply D; reflexivity ] ] ]);
    let t :=
        first [
           solve [ constructors ]
         | solve [ simpl; rew_refl× ] ] in t || (split; t) || idtac.
Qed.

End Typed.

Definition sign_analyse_fuel_fail :=
  sign_analyse_fuel (failing_analyser sign_asem).

Lemma sign_analyse_fuel_fail_correct : ∀ fuel,
  analyser_correct (sign_analyse_fuel_fail fuel).
Proof. introv. apply sign_analyse_fuel_correct. apply failing_analyser_correct. Qed.

Definition sign_analyse_fuel_type :=
  sign_analyse_fuel sign_type_analyse.

Lemma sign_analyse_fuel_type_correct : ∀ fuel,
  analyser_correct (sign_analyse_fuel_type fuel).
Proof. introv. apply sign_analyse_fuel_correct. apply sign_type_analyse_correct. Qed.

Definition sign_analyse_deep_fuel_fail :=
  sign_analyse_deep_fuel (failing_analyser sign_asem).

Lemma sign_analyse_deep_fuel_fail_correct : ∀ fuel,
  analyser_correct (sign_analyse_deep_fuel_fail fuel).
Proof. introv. apply sign_analyse_deep_fuel_correct. apply failing_analyser_correct. Qed.

Definition sign_analyse_deep_fuel_type :=
  sign_analyse_deep_fuel sign_type_analyse.

Lemma sign_analyse_deep_fuel_type_correct : ∀ fuel,
  analyser_correct (sign_analyse_deep_fuel_type fuel).
Proof. introv. apply sign_analyse_deep_fuel_correct. apply sign_type_analyse_correct. Qed.

Definition sign_analyse_oracle_back_and_forth oracle_fuel unfold_fuel fuel :=
  sign_analyser_back_and_forth (sign_analyser_oracle_fuel oracle_fuel)
                               (sign_oracle_unfold unfold_fuel) fuel HeapList.empty.

Lemma sign_analyse_oracle_back_and_forth_correct : ∀ oracle_fuel unfold_fuel fuel,
  analyser_correct (sign_analyse_oracle_back_and_forth oracle_fuel unfold_fuel fuel).
Proof. introv. apply sign_analyser_back_and_forth_correct. introv. apply sign_analyser_oracle_fuel_correct. Qed.

Definition sign_analyse_oracle_back_and_forth_loop oracle_fuel unfold_fuel fuel :=
  sign_analyser_back_and_forth (sign_analyser_oracle_fuel oracle_fuel)
                               (sign_oracle_loop_unfold unfold_fuel) fuel HeapList.empty.

Lemma sign_analyse_oracle_back_and_forth_loop_correct : ∀ oracle_fuel unfold_fuel fuel,
  analyser_correct (sign_analyse_oracle_back_and_forth_loop oracle_fuel unfold_fuel fuel).
Proof. introv. apply sign_analyser_back_and_forth_correct. introv. apply sign_analyser_oracle_fuel_correct. Qed.

Definition sign_analyse_oracle_back_and_forth_deep deep_fuel oracle_fuel unfold_fuel fuel :=
  sign_analyser_back_and_forth (sign_analyser_oracle_deep_fuel deep_fuel oracle_fuel)
                               (sign_oracle_unfold unfold_fuel) fuel HeapList.empty.

Lemma sign_analyse_oracle_back_and_forth_deep_correct : ∀ deep_fuel oracle_fuel unfold_fuel fuel,
  analyser_correct (sign_analyse_oracle_back_and_forth_deep deep_fuel oracle_fuel unfold_fuel fuel).
Proof. introv. apply sign_analyser_back_and_forth_correct. introv. apply sign_deep_analyser_oracle_fuel_correct. Qed.

Definition sign_analyse_oracle_back_and_forth_deep_loop deep_fuel oracle_fuel unfold_fuel fuel :=
  sign_analyser_back_and_forth (sign_analyser_oracle_deep_fuel deep_fuel oracle_fuel)
                               (sign_oracle_loop_unfold unfold_fuel) fuel HeapList.empty.

Lemma sign_analyse_oracle_back_and_forth_deep_loop_correct : ∀ deep_fuel oracle_fuel unfold_fuel fuel,
  analyser_correct (sign_analyse_oracle_back_and_forth_deep_loop deep_fuel oracle_fuel unfold_fuel fuel).
Proof. introv. apply sign_analyser_back_and_forth_correct. introv. apply sign_deep_analyser_oracle_fuel_correct. Qed.

End General.

Extraction

Extraction Language Ocaml.

Require Import ExtrOcamlBasic.
Require Import ExtrOcamlNatInt.
Require Import ExtrOcamlZInt.
Require Import ExtrOcamlString.

Definition eq_aValVar (v1 v2 : aValVar) := decide (v1 =♯ v2).

Extraction Inline arbitrary.

Extraction "Abstract.ml"
  prog_test0 prog_test1 prog_test2 prog_test3
  prog_test4 prog_test5 prog_test6 prog_test7
  prog_test8 prog_test9 prog_test10 prog_test11
  prog_test12
  initial eq_aValVar analyser_match
  sign_trivial_analyser sign_failing_analyser sign_type_analyse
  sign_analyse_fuel_fail sign_analyse_fuel_type
  sign_analyse_deep_fuel_fail sign_analyse_deep_fuel_type
  sign_analyse_oracle_back_and_forth sign_analyse_oracle_back_and_forth_deep
  sign_analyse_oracle_back_and_forth_loop sign_analyse_oracle_back_and_forth_deep_loop.