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'

        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 
            ⟦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])
        by(simp add: Lustre_types.is_def_pair plus_option_def)
   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)
      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)
      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)                    

Note: No state machine was harmed during this meeting.

Previous meeting -- Next meeting