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

Obligations | Alt-Ergo (1.01) | CVC4 (1.4) | Z3 (4.5.0) | ||

VC for union | 0.16 | --- | --- | ||

VC for intersection | 0.18 | --- | --- | ||

VC for aboveMin | --- | --- | --- | ||

split_goal_wp | |||||

assertion | 0.15 | --- | --- | ||

assertion | --- | 0.22 | 0.28 | ||

assertion | --- | 0.42 | --- | ||

type invariant | 0.30 | --- | --- | ||

postcondition | 0.02 | 0.03 | 0.01 | ||

VC for maxUnion | --- | --- | --- | ||

split_goal_wp | |||||

precondition | 0.01 | 0.05 | 0.01 | ||

precondition | 0.02 | 0.05 | 0.02 | ||

assertion | --- | 0.13 | 0.33 | ||

postcondition | 1.27 | 0.14 | --- | ||

postcondition | --- | --- | --- | ||

split_goal_wp | |||||

postcondition | --- | 0.06 | --- | ||

postcondition | 0.23 | 0.16 | --- |