Wiki Agenda Contact Version française

A challenge related to the Esterel Compiler

This is a challenge given by Gérard Berry, extracted from the Esterel compiler. The technique used for reasoning about bit-vectors is described in Specification and proof of high-level functional properties of bit-level programs.


Authors: Claude Marché / Clément Fumex

Topics: Bitwise operations

Tools: Why3

References: ProofInUse joint laboratory

see also the index (by topic, by tool, by reference, by year)



Challenge about the Esterel Compiler

This is a challenge given by Gérard Berry, extracted from Esterel compiler.

1. Each instruction returns an integer code between 1 and N. Parallel execution returns the maximum of codes of its branches.

2. Return codes are implemented as bitvectors.

3. During static analysis, each instruction P may return a set of codes C(P) instead of one code only. Hence P||Q must return {max(p,q) | p in C(p), q in C(q), to be computed on bitvectors.

4. A method given by Georges Gonthier is to write the result under the form { x in P U Q | x >= max (min(P), min(Q) } that can be encoded as bitvector operation (P|Q)&(P|-P)&(Q|-Q).

module Esterel

  use import int.Int
  use import int.MinMax
  use import set.Fsetint
  use import bv.BV64

  type s = {
          bv : BV64.t;  (* a 64-bit bitvector *)
    ghost mdl: set int; (* its interpretation as a set *)
  }
  invariant {
    forall i: int. (0 <= i < size /\ nth self.bv i) <-> mem i self.mdl
  }

  let union (a b: s) : s  (* operator [a|b] *)
    ensures  { result.mdl = union b.mdl a.mdl }
  = { bv = bw_or a.bv b.bv;
      mdl = union b.mdl a.mdl }

  let intersection (a b : s) : s (* operator [a&b] *)
    ensures { result.mdl = inter a.mdl b.mdl }
  = { bv = bw_and a.bv b.bv;
      mdl = inter a.mdl b.mdl }

  let aboveMin (a : s) : s (* operator [a|-a] *)
    requires { not is_empty a.mdl }
    ensures { result.mdl = interval (min_elt a.mdl) size }
  = let ghost p = min_elt a.mdl in
    let ghost p_bv = of_int p in
    assert { eq_sub_bv a.bv zeros zeros p_bv };
    let res = bw_or a.bv (neg a.bv) in
    assert { eq_sub_bv res zeros zeros p_bv };
    assert { eq_sub_bv res ones p_bv (sub size_bv p_bv) };
    { bv = res;
      mdl = interval p size }

  let maxUnion (a b : s) : s  (* operator [(a|b)&(a|-a)&(b|-b)] *)
    requires { not is_empty a.mdl /\ not is_empty b.mdl }
    ensures { forall x. mem x result.mdl <->
                (mem x (union a.mdl b.mdl) /\
                 x >= max (min_elt a.mdl) (min_elt b.mdl)) }
    ensures { forall x. mem x result.mdl <->
                exists y z. mem y a.mdl /\ mem z b.mdl /\ x = max y z }
  = let res =
      intersection (union a b) (intersection (aboveMin a) (aboveMin b))
    in
    assert {
      forall x. mem x res.mdl ->
        let (y,z) =
          if mem x a.mdl then (x,min_elt b.mdl) else (min_elt a.mdl,x)
        in
          mem y a.mdl /\ mem z b.mdl /\ x = max y z };
    res

end

download ZIP archive

Why3 Proof Results for Project "esterel"

Theory "esterel.Esterel": fully verified in 4.25 s

ObligationsAlt-Ergo (1.01)CVC4 (1.4)Z3 (4.5.0)
VC for union0.16------
VC for intersection0.18------
VC for aboveMin---------
split_goal_wp
  assertion0.15------
assertion---0.220.28
assertion---0.42---
type invariant0.30------
postcondition0.020.030.01
VC for maxUnion---------
split_goal_wp
  precondition0.010.050.01
precondition0.020.050.02
assertion---0.130.33
postcondition1.270.14---
postcondition---------
split_goal_wp
  postcondition---0.06---
postcondition0.230.16---