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
Obligations | Alt-Ergo 2.1.0 | CVC4 1.5 | Eprover 2.0 | Z3 4.12.2 | ||
VC for s | --- | --- | 0.02 | --- | ||
VC for union | 0.16 | --- | --- | --- | ||
VC for intersection | 0.06 | --- | --- | --- | ||
VC for aboveMin | --- | --- | --- | --- | ||
split_goal_right | ||||||
assertion | 0.15 | --- | --- | --- | ||
assertion | --- | 0.05 | --- | --- | ||
assertion | --- | 1.59 | --- | --- | ||
precondition | 0.52 | --- | --- | --- | ||
postcondition | 0.02 | 0.03 | --- | 0.01 | ||
VC for maxUnion | --- | --- | --- | --- | ||
split_goal_right | ||||||
precondition | 0.02 | 0.05 | --- | 0.01 | ||
precondition | 0.01 | 0.05 | --- | 0.01 | ||
assertion | --- | 0.53 | --- | 1.25 | ||
postcondition | 0.69 | --- | --- | --- | ||
postcondition | --- | --- | --- | --- | ||
split_goal_right | ||||||
postcondition | --- | 0.06 | --- | --- | ||
postcondition | 0.22 | 0.17 | --- | --- |