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