Wiki Agenda Contact English version

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.


Auteurs: Claude Marché / Clément Fumex

Catégories: Bitwise operations

Outils: Why3

Références: 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: fset 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.1.0CVC4 1.5Eprover 2.0Z3 4.12.2
VC for s------0.02---
VC for union0.16---------
VC for intersection0.06---------
VC for aboveMin------------
split_goal_right
assertion0.15---------
assertion---0.05------
assertion---1.59------
precondition0.52---------
postcondition0.020.03---0.01
VC for maxUnion------------
split_goal_right
precondition0.020.05---0.01
precondition0.010.05---0.01
assertion---0.53---1.25
postcondition0.69---------
postcondition------------
split_goal_right
postcondition---0.06------
postcondition0.220.17------