## 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  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
```