Audience

• Thibaut Balabonski
• Yakoub Nemouchi
• Safouan Taha
• Frédéric Tuong
• Burkhart Wolff
• Lina Ye

Project : Modélisation de Lustre en Isabelle

Bu

Lustre

Lustre est un modèle de langage pour la programmation synchrone. Les objets sont des flux (streams) de données représentant des signaux, sur lesquels les blocs (nodes) effectuent des transformations (opérateurs logiques, retard (pre), ...). Les flux sont typés, tous les types ayant une valeur nil indiquant que la valeur du flux n'est pas déterminée ; les opérateurs sont stricts (le résultat vaut nil dès qu'un des arguments vaut nil).

Formalisation Isabelle

Les types des flux sont représentés par 'a::null, où null est une classe de type ajoutant nil à chaque type 'a. Dans cette classe, on définit une operation is_def(X); il est true sess X est différent de nil

Les flux sont eux-mêmes représentés par des fonctions de nat dans 'a, les opérateurs étant restreints à des types 'a::null (pour des raisons techniques en Isabelle). Cette construction permet une opération de transformation d'une paire de flux en un flux de paires, afin que les blocs aient une seule entrée et une seule sortie_: des n-uplets de flux. Cette isomorphisme peut être donné du support syntaxique analogiquement des pairs en HOL comme:

   (λ⟦x, y, z⟧. P x y z) 

qui a le type:

   ('a::null × 'b::null × 'c::null) stream ⇒ 'd,

tandis que P a le type:

   'a stream ⇒ stream ⇒ 'c stream ⇒ 'd.

On peut ainsi définir les blocs de base et les blocs récursifs. L'égalité de deux flux est l'égalité extensionnelle des fonctions:

lemma stream_ext : "(s = t) = (∀n. s⟦n⟧ = t⟦n⟧)"

ou s⟦n⟧ est le valeur de s a la position n.

Raisonnement sur Lustre Processes

Afin d'énoncer des propriétés sur des programmes Lustre particuliers, on place un observateur sur le flux de sortie. Pour établir ces propriétés, l'idée est de raisonner :

• par égalité de deux flux jusqu'à un certain point ;
• par analyse de cas sur toutes les variables (pour gérer le cas nil).

Il y a maintenant plusieurs problèmes d'un raisonnement 'efficace' sur des processus Lustre, surtout avec l'égard d'égalité des processus (ce qui est primordial si on veut finalement prouver qu'un programme P composer avec un observateur O (encodant une propriété) résulte dans le process true:

• la logique est une weak-Kleene logic (donc trois valeurs).
• l'espace de tous les processus lustre de type 'a stream est trop grand pour représenter une relation d'égalité avec une substuitutivité standard; donc l'égalité standard pour lequel on a des procédures efficaces de rewriting comme simp en Isabelle.

Une solution consister que les operations sur les streams Lustre, par contre, sont clos sur un sous-espace pour lequel une égalité partielle est possible. Cette espace est nommé l'espace des fonctions qui sont "computational(ly) consistent", ce qui veut dire que pour chaque point n dans un stream, son calcul dépend seulement sur le passé de ses entrées. Il y a meme une notre propriété renforcé: "strong computational consistency" ou juste la position n d'un flux d'entree suffit pour calculé la sortie a la position n.

Il est intéressant a voir que ces concepts sont relativement facile a formaliser, et surtout a établir pour des expressions composer par les opérateurs Lustre.

Weak and strong computational consistency can be defined by a variant of substitutivity:

definition cc :: " ('a::null stream ⇒ 'b::null stream) ⇒ bool" ("⟨_⟩")
where     "⟨P⟩ ≡ ∀ n S T.  S ≜⇩⟦⇘n⇙⇩⟧ T ⟶ P(S) ≜⇩⟦⇘n⇙⇩⟧ P(T)" 

definition scc :: " ('a::null stream ⇒ 'b::null stream) ⇒  bool"  ("!⟨_⟩")
where     "!⟨P⟩ ≡ ∀ n S T. (S⟦n⟧) = (T⟦n⟧) ⟶ ((P S)⟦n⟧) = ((P T)⟦n⟧)" 

Establish cc et scc for an expression P can be done by a side-calculus:

lemma X: "!⟨P⟩ ⟹ ⟨P⟩"               (* strong implies weak computational consistency *)
lemma scc_const[simp] : "!⟨λ_. c⟩"   (* a constant expression is strong computational consistent *)
lemma scc_id[simp] :  "!⟨λX. X⟩"     (* The empty Term-context is strongly computational consistent *)
lemma cc_const[simp] : "⟨λ_. c⟩"
lemma cc_id[simp] :  "⟨λX. X⟩"

And now for any operator f : + * / ... we have a rule:

 ⟨?S⟩ ⟹ ⟨?T⟩ ⟹ ⟨λX. f (?S X) (?T X)⟩
 !⟨?S⟩ ⟹ !⟨?T⟩ ⟹ !⟨λX. f (?S X) (?T X)⟩

For some exceptional cases like pre we only have the former rule, of course (pre depends on the past).

Now, we can have "quasi substutivity rules" like:

lemma cc_subst2 :  "⟨P⟩ ⟹ ⟨Q⟩ ⟹ X≜⇩⟦⇘n⇙⇩⟧Y ⟹ (P Y)⟦n⟧ = (Q Y)⟦n⟧ ⟹  (P X)⟦n⟧ = (Q X)⟦n⟧"
(* for the weak consistent case, as for term contexts containing pre *)
lemma scc_subst2 : "!⟨P⟩ ⟹ !⟨Q⟩ ⟹  X⟦n⟧ = Y⟦n⟧⟹ (P Y)⟦n⟧ = (Q Y)⟦n⟧ ⟹  (P X)⟦n⟧ = (Q X)⟦n⟧"
(* for the strong consistent case *)

which allows for a REPLACEMENT of some sub term X by Y in term contexts P, Q provided that they are (weak/strong) computational consistent.

A variant of this allows for a unit-propagation like transportation of the fact that a variable is null:

lemma scc_subst2_rev : "X⟦n⟧ = null ⟹ !⟨P⟩ ⟹ !⟨Q⟩ ⟹ (P null)⟦n⟧ = (Q null)⟦n⟧ ⟹ (P X)⟦n⟧ = (Q X)⟦n⟧"

Since most operations are strict, rules like:

     f null X = null
     f X null = null

and its converse:

     is_def ((f X Y)⟦n⟧) = (is_def (X⟦n⟧) ∧ is_def (Y⟦n⟧))

can be schematically derived via a suitable locale.

This gives rise to a particular proof style, which is highly automatable:

lemma and_commute: "(X and Y) = (Y and X)"
proof(auto simp: stream_ext, rename_tac "n",case_tac "X⟦n⟧=null")
   fix    n  assume * :"X⟦n⟧ = null"    show  "X and Y⟦n⟧ = Y and X⟦n⟧"
                                        by(rule scc_subst2_rev[OF *], simp_all) 
next 
   fix    n  assume **:"is_def (X⟦n⟧)"  show  "(X and Y)⟦n⟧ = (Y and X)⟦n⟧"
      proof (case_tac "Y⟦n⟧=null")
             assume * :"Y⟦n⟧ = null"    show  "(X and Y)⟦n⟧ = (Y and X)⟦n⟧"
                                        by(rule scc_subst2_rev[OF *], simp_all)
      next   
             assume * :"is_def (Y⟦n⟧)"  show  "(X and Y)⟦n⟧ = (Y and X)⟦n⟧"
                                        apply(insert * **)
                                        by(insert * **, auto)
      qed
qed

The structure is:

• reduction via extensionality to point wise reasoning
• case distinction on definedness for all variables contained in the terms "(X and Y)" and "(Y and X)"; in case that one variable (point) is undefined, apply strictness rules,
• For the case where all variables are defined, apply a class of rules

  (established for each operator f):

  
   is_def X ⟹ is_def Y ⟹ is_def (Some (g (the X) (the Y)))

  For the case of the and above, the instance of the above rule is just:

  
   is_def (S⟦n⟧) ⟹ is_def (T⟦n⟧) ⟹ (S and T)⟦n⟧ = Some (the (S⟦n⟧) ∧ the (T⟦n⟧))

   which allows for a direct elimination of the Some/the wrappers and reduces the problem directly
   to the core of the problem: is ∧ commutative.

NOTE THAT THE NUMBER OF CASE-DISTINCTIONS IS LINEAR IN THE NUMBER OF VARIABLES IN THE TERM; A SIMPLE UNFOLDING/TERM-CASE-SPLIT STRATEGY RESULTS IN AN EXPONENTIAL GROWTH OF CASE-SPLITS IN GENERAL.

Liens

Tutoriel Lustre

Code Isabelle

Previous meeting -- Next meeting