LRI Équipe MODHEL Bât 650 Ada Lovelace, Université Paris Sud Rue Noetzlin, 91190 Gif-sur-Yvette, France
Isabelle club meeting on June 22 2016

Personnes présentes

• Frédéric Boulanger
• Hai Nguyen Van
• Safouan Taha
• Frédéric Tuong
• Benoît Valiron
• Burkhart Wolff
• Lina Ye

A state machine free model of Lustre

Burkhart presents a model of the synchronous programming language Lustre. It is based on a shallow embedding, representing "blocks" with potential feed-backs as stream-processing functions (assuming that streams are typed).

The shallow embedding provides basic operations for arithmetic and logic which assume a null-element for non-existing values; with one exception (the test isNull) all operations of the Lustre language are assumed to be strict extensions.

The resulting shallow-embedding called HOL/Lustre allows finally to write typical examples:

fun    COUNTER⇩b⇩o⇩d⇩y::"(COUNTER⇩i⇩n stream × COUNTER⇩o⇩u⇩t stream) ⇒ COUNTER⇩o⇩u⇩t stream"
where "COUNTER⇩b⇩o⇩d⇩y (inp, out) =
(let ⟦init, incr, X, reset⟧ = inp;
⟦PC, C⟧ = out;

PC' = init -> pre (C);                       (* construction of state variables *)
C'  = if reset then init                     (* construction of output variables *)
else if X then PC' + incr
else PC'
endif
endif

in ⟦PC',C'⟧)"

definition  COUNTER :: "COUNTER⇩i⇩n stream ⇒ COUNTER⇩o⇩u⇩t stream"
where      "COUNTER ≡ (loop COUNTER⇩b⇩o⇩d⇩y)" (* block with feedback *)


as well as

fun    SPEED⇩b⇩o⇩d⇩y::"(SPEED⇩i⇩n stream × SPEED⇩o⇩u⇩t stream) ⇒ SPEED⇩o⇩u⇩t stream"
where "SPEED⇩b⇩o⇩d⇩y (inp,out) =
(let ⟦beacon, second⟧          = inp;
⟦diff, incr, late, early⟧ = out;
incr'                    = if beacon and (not second)
then 1
else if second and (not beacon)
then -1
else 0
endif
endif;
⟦diff',_⟧                 = COUNTER  ⟦0, incr', beacon or second, false⟧;
early'                   = false -> (if pre early then diff' >s 0 else diff' >=s M endif);
late'                    = false -> (if pre late then diff' <s 0 else diff' <=s -M endif)
in  ⟦diff', incr', late', early'⟧)"

definition  SPEED :: "SPEED⇩i⇩n stream ⇒ SPEED⇩o⇩u⇩t stream" where "SPEED ≡ (loop SPEED⇩b⇩o⇩d⇩y)"


which gives a classical example of a speed-controller with latency. Our encoding would be able to cope with float-variables.

Wrt. to the semantic construction of the operators of HOL/Lustre, the proceeding is as follows: First, a null class is defined to represent datatypes with a null value, and 'a option is shown to instantiate this class. Then pairing via cartesian products as well as streams itself are proven to live inside this class. The streams in Lustre are modeled as streams (nat => 'a) of with 'ainstances of the null class. The null value represents a hole in a stream. Thus, Lustre can be seen as a language to define behaviors by composing operators on infinite streams of values. These streams may have holes in them, i.e. samples with no defined value.

In order to achieve compositionality of streams, the projection and weaving of streams are defined so that a pair ('a stream, 'b stream) is isomorphic to a stream of pairs ('a×'b) stream.

A key concept for proving properties with feedback ("recursive blocks") is Computational Consistency; it Computational consistency of a process P is defined as : if for all n, two streams a and b are identical up to the nth sample, then P(a) = P(b) at n. This means that P depends only on the past of the stream. This is the major weapon to prove via a kind of specialised induction properties on blocks with feedback, as long as they only consider the past in their input and feedback streams.

Strict computational consistency of a process P is defined as : for all n, if the nth sample of a is identical to the nth sample of b, then P(a) = P(b) at n. This means that P depends only on the current sample of the stream (it has no memory).

Compositionality of streams and computational consistency allow the definition of the semantics of networks of operators with feedback (an output stream is fed back to the input of an operator).

Then a Hoare-style semantics is defined, and a proof is made on a simple example of a counter, which is an adder fed back with its own output. For example:

theorem MySecondThm:
"COUNTER  ⇘{⟦0, 1+1, true, true -> false⟧}⇙⊩ ( (λ ⟦_,C⟧. (C mod (1+1) =s 0)))"
unfolding   assert''_def  COUNTER_def
proof(auto simp: Lustre_basics.is_def_stream )
text{* The proof comes in two major stages: first, we have to establish
that the program observables are pointwise defined. We proceed by: *}
fix input n
show "is_def (loop COUNTER⇩b⇩o⇩d⇩y ⟦0, 1 + 1, true, true -> false⟧⟦n⟧)"
apply(rule COUNTER_def_preserve_pointwise[simplified COUNTER_def])
next
show "snd⇩s⇩t⇩r⇩e⇩a⇩m (loop COUNTER⇩b⇩o⇩d⇩y ⟦0, 1 + 1, true, true -> false⟧) mod (1 + 1) ≐ 0 = true"
(is "snd⇩s⇩t⇩r⇩e⇩a⇩m (?H) mod (1 + 1) ≐ 0 = true")
proof(rule observer_induct)
text{* This induction in itself boils down to three parts. *}
text{* First, our invariant must be strongly computationally consistent. *}
show "!⟨λa. ((snd⇩s⇩t⇩r⇩e⇩a⇩m a) mod (1 + 1)) ≐ (0::Integer stream)⟩"  by(simp)
next
text{* Second, our invariant must be true at the initial state.  *}
show "snd⇩s⇩t⇩r⇩e⇩a⇩m (COUNTER⇩b⇩o⇩d⇩y (⟦0, 1 + 1, true, true -> false⟧, nil)) mod (1 + 1) ≐ 0⟦0⟧ = true⟦0⟧"
by(auto simp:  sel_simps true_simp Let_def plus_option_def split: if_splits)
next
text{* Third, our invariant must be preserved.  *}
fix n fix σ::"(Integer × Integer) stream"
assume       "((snd⇩s⇩t⇩r⇩e⇩a⇩m σ) mod (1+1) ≐ 0)⟦n⟧ = (true⟦n⟧)"
then show    "(snd⇩s⇩t⇩r⇩e⇩a⇩m (COUNTER⇩b⇩o⇩d⇩y(⟦0, 1+1, true, true->false⟧,σ)) mod (1+1) ≐ 0)⟦Suc n⟧ =
(true⟦Suc n⟧)"
(* und schlachtefatz *)
by(auto simp: sel_simps true_simp Let_def false_simp plus_profile.nonstrict_compute
split:option.split_asm split_if_asm)
qed
qed


Note: No state machine was harmed during this meeting.