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 int.Int
  use int.MinMax
  use set.Fsetint
  use 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 bv i) <-> mem i 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

ObligationsAlt-Ergo 2.0.0CVC4 1.5Eprover 2.0Z3 4.6.0
VC s------0.02---
VC union0.16---------
VC intersection0.06---------
VC aboveMin------------
split_goal_right
VC aboveMin.0---------0.01
VC aboveMin.10.15---------
VC aboveMin.2---0.04---0.31
VC aboveMin.3---0.19------
VC aboveMin.40.59---------
VC aboveMin.50.020.03---0.01
VC maxUnion------------
split_goal_right
VC maxUnion.00.020.05---0.02
VC maxUnion.10.010.05---0.01
VC maxUnion.2---0.25---0.40
VC maxUnion.30.42---------
VC maxUnion.4------------
split_goal_right
VC maxUnion.4.0---0.06------
VC maxUnion.4.10.280.06------