Commit 93645b72 authored by David Hauzar's avatar David Hauzar
Browse files

Merge branch 'master' into counter-examples

parents bf803f19 8b32d86b
......@@ -156,6 +156,9 @@ pvsbin/
/lib/isabelle/list/
/lib/isabelle/map/
/lib/isabelle/set/
/lib/isabelle/Tools/why3
/lib/isabelle/Why3_Number.thy
/lib/isabelle/why3.ML
/lib/isabelle/last_build
# /src/driver/
......@@ -211,7 +214,6 @@ pvsbin/
/examples/in_progress/wcet_hull/
/examples/in_progress/binary_search2/
/examples/in_progress/binary_search_c/
/examples/in_progress/next_digit_sum/
/examples/in_progress/vacid_0_red_black_trees_harness/
/examples/why3bench.html
/examples/why3regtests.err
......
* marks an incompatible change
provers
o support for Isabelle 2015 (released May 25, 2015)
Version 0.86.1, May 22, 2015
============================
......
......@@ -151,7 +151,7 @@ LIB_DRIVER = call_provers driver_ast driver_parser driver_lexer driver \
whyconf autodetection \
parse_smtv2_model_parser parse_smtv2_model_lexer parse_smtv2_model
LIB_MLW = ity expr dexpr
LIB_MLW = ity expr dexpr mdecl
LIB_PARSER = ptree glob parser typing lexer
......@@ -844,7 +844,7 @@ ifeq (@enable_coq_support@,yes)
ifeq (@enable_coq_libs@,yes)
COQLIBS_INT_FILES = Abs ComputerDivision Div2 EuclideanDivision Int MinMax Power
COQLIBS_INT_FILES = Abs ComputerDivision Div2 EuclideanDivision Int MinMax Power NumOf
COQLIBS_INT_ALL_FILES = Exponentiation $(COQLIBS_INT_FILES)
COQLIBS_INT = $(addprefix lib/coq/int/, $(COQLIBS_INT_ALL_FILES))
......@@ -872,13 +872,16 @@ COQLIBS_OPTION = $(addprefix lib/coq/option/, $(COQLIBS_OPTION_FILES))
COQLIBS_SEQ_FILES = Seq
COQLIBS_SEQ = $(addprefix lib/coq/seq/, $(COQLIBS_SEQ_FILES))
COQLIBS_BV_FILES = Pow2int BV_Gen
COQLIBS_BV = $(addprefix lib/coq/bv/, $(COQLIBS_BV_FILES))
ifeq (@enable_coq_fp_libs@,yes)
COQLIBS_FP_FILES = Rounding SingleFormat Single DoubleFormat Double
COQLIBS_FP_ALL_FILES = GenFloat $(COQLIBS_FP_FILES)
COQLIBS_FP = $(addprefix lib/coq/floating_point/, $(COQLIBS_FP_ALL_FILES))
endif
COQLIBS_FILES = lib/coq/BuiltIn lib/coq/HighOrd $(COQLIBS_INT) $(COQLIBS_BOOL) $(COQLIBS_REAL) $(COQLIBS_NUMBER) $(COQLIBS_SET) $(COQLIBS_MAP) $(COQLIBS_LIST) $(COQLIBS_OPTION) $(COQLIBS_SEQ) $(COQLIBS_FP)
COQLIBS_FILES = lib/coq/BuiltIn lib/coq/HighOrd $(COQLIBS_INT) $(COQLIBS_BOOL) $(COQLIBS_REAL) $(COQLIBS_NUMBER) $(COQLIBS_SET) $(COQLIBS_MAP) $(COQLIBS_LIST) $(COQLIBS_OPTION) $(COQLIBS_SEQ) $(COQLIBS_FP) $(COQLIBS_BV)
drivers/coq-realizations.aux: Makefile
$(if $(QUIET),@echo 'Generate $@' &&) \
......@@ -903,6 +906,8 @@ drivers/coq-realizations.aux: Makefile
echo 'theory option.'"$$f"' meta "realized_theory" "option.'"$$f"'", "" end'; done; \
for f in $(COQLIBS_SEQ_FILES); do \
echo 'theory seq.'"$$f"' meta "realized_theory" "seq.'"$$f"'", "" end'; done; \
for f in $(COQLIBS_BV_FILES); do \
echo 'theory bv.'"$$f"' meta "realized_theory" "bv.'"$$f"'", "" end'; done; \
for f in $(COQLIBS_FP_FILES); do \
echo 'theory floating_point.'"$$f"' meta "realized_theory" "floating_point.'"$$f"'", "" end'; done; \
) > $@
......@@ -928,6 +933,8 @@ install_no_local::
cp $(addsuffix .vo, $(COQLIBS_OPTION)) $(LIBDIR)/why3/coq/option/
mkdir -p $(LIBDIR)/why3/coq/seq
cp $(addsuffix .vo, $(COQLIBS_SEQ)) $(LIBDIR)/why3/coq/seq/
mkdir -p $(LIBDIR)/why3/coq/bv
cp $(addsuffix .vo, $(COQLIBS_BV)) $(LIBDIR)/why3/coq/bv/
ifeq (@enable_coq_fp_libs@,yes)
mkdir -p $(LIBDIR)/why3/coq/floating_point
cp $(addsuffix .vo, $(COQLIBS_FP)) $(LIBDIR)/why3/coq/floating_point/
......@@ -962,6 +969,9 @@ update-coq-option: bin/why3realize.@OCAMLBEST@ drivers/coq-realizations.aux theo
update-coq-seq: bin/why3realize.@OCAMLBEST@ drivers/coq-realizations.aux theories/seq.why
for f in $(COQLIBS_SEQ_FILES); do WHY3CONFIG="" bin/why3realize.@OCAMLBEST@ -L theories -D drivers/coq-realize.drv -T seq.$$f -o lib/coq/seq/; done
update-coq-bv: bin/why3realize.@OCAMLBEST@ drivers/coq-realizations.aux theories/bv.why
for f in $(COQLIBS_BV_FILES); do WHY3CONFIG="" bin/why3realize.@OCAMLBEST@ -L theories -D drivers/coq-realize.drv -T bv.$$f -o lib/coq/bv/; done
update-coq-fp: bin/why3realize.@OCAMLBEST@ drivers/coq-realizations.aux theories/floating_point.why
for f in $(COQLIBS_FP_FILES); do WHY3CONFIG="" bin/why3realize.@OCAMLBEST@ -L theories -D drivers/coq-realize.drv -T floating_point.$$f -o lib/coq/floating_point/; done
......@@ -1102,6 +1112,21 @@ clean::
ifeq (@enable_isabelle_libs@,yes)
ISABELLEVERSIONSPECIFIC=why3.ML Tools/why3 Why3_Number.thy
ISABELLEVERSIONSPECIFICTARGETS=$(addprefix lib/isabelle/, $(ISABELLEVERSIONSPECIFIC))
ISABELLEVERSIONSPECIFICSOURCES=$(addsuffix .@ISABELLEVERSION@, $(ISABELLEVERSIONSPECIFICTARGETS))
ISABELLEREALIZEDRV=drivers/isabelle@ISABELLEVERSION@-realize.drv
$(ISABELLEVERSIONSPECIFICTARGETS): $(ISABELLEVERSIONSPECIFICSOURCES)
for i in $(ISABELLEVERSIONSPECIFIC); do \
cp lib/isabelle/$$i.@ISABELLEVERSION@ lib/isabelle/$$i ; \
done
clean::
rm -f $(ISABELLEVERSIONSPECIFICTARGETS)
ISABELLELIBS_INT_FILES = Exponentiation Abs ComputerDivision Div2 EuclideanDivision Int MinMax Power
ISABELLELIBS_INT = $(addsuffix .xml, $(addprefix lib/isabelle/int/, $(ISABELLELIBS_INT_FILES)))
......@@ -1151,7 +1176,10 @@ else
ISABELLE_TARGET_DIR=$(LIBDIR)/why3/isabelle
endif
lib/isabelle/last_build: $(ISABELLELIBS_INT) $(ISABELLELIBS_BOOL) $(ISABELLELIBS_REAL) $(ISABELLELIBS_NUMBER) $(ISABELLELIBS_SET) $(ISABELLELIBS_MAP) $(ISABELLELIBS_LIST) $(ISABELLELIBS_OPTION)
lib/isabelle/last_build: $(ISABELLEVERSIONSPECIFICTARGETS) $(ISABELLELIBS_INT) $(ISABELLELIBS_BOOL) $(ISABELLELIBS_REAL) $(ISABELLELIBS_NUMBER) $(ISABELLELIBS_SET) $(ISABELLELIBS_MAP) $(ISABELLELIBS_LIST) $(ISABELLELIBS_OPTION)
ifneq (@enable_local@,yes)
cp -r lib/isabelle "$(LIBDIR)/why3"
endif
@(if isabelle components -l | grep -q "$(ISABELLE_TARGET_DIR)$$"; then \
echo "Building the Why3 heap for Isabelle/HOL:"; \
isabelle build -bc Why3; \
......@@ -1163,7 +1191,6 @@ lib/isabelle/last_build: $(ISABELLELIBS_INT) $(ISABELLELIBS_BOOL) $(ISABELLELIBS
fi)
install_no_local::
cp -r lib/isabelle "$(LIBDIR)/why3"
cp drivers/isabelle-realizations.aux "$(DATADIR)/why3/drivers/"
install_no_local:: lib/isabelle/last_build
......@@ -1173,44 +1200,44 @@ install_local:: lib/isabelle/last_build
update-isabelle: $(ISABELLELIBS_INT) $(ISABELLELIBS_BOOL) $(ISABELLELIBS_REAL) $(ISABELLELIBS_NUMBER) $(ISABELLELIBS_SET) $(ISABELLELIBS_MAP) $(ISABELLELIBS_LIST) $(ISABELLELIBS_OPTION)
$(ISABELLELIBS_INT): bin/why3realize.@OCAMLBEST@ drivers/isabelle-realizations.aux \
drivers/isabelle-realize.drv drivers/isabelle-common.gen theories/int.why
$(ISABELLEREALIZEDRV) drivers/isabelle-common.gen theories/int.why
mkdir -p lib/isabelle/int
WHY3CONFIG="" bin/why3realize.@OCAMLBEST@ -L theories -D drivers/isabelle-realize.drv -T int.$(notdir $(basename $@)) -o lib/isabelle/int/
WHY3CONFIG="" bin/why3realize.@OCAMLBEST@ -L theories -D $(ISABELLEREALIZEDRV) -T int.$(notdir $(basename $@)) -o lib/isabelle/int/
$(ISABELLELIBS_BOOL): bin/why3realize.@OCAMLBEST@ drivers/isabelle-realizations.aux \
drivers/isabelle-realize.drv drivers/isabelle-common.gen theories/bool.why
$(ISABELLEREALIZEDRV) drivers/isabelle-common.gen theories/bool.why
mkdir -p lib/isabelle/bool
WHY3CONFIG="" bin/why3realize.@OCAMLBEST@ -L theories -D drivers/isabelle-realize.drv -T bool.$(notdir $(basename $@)) -o lib/isabelle/bool/
WHY3CONFIG="" bin/why3realize.@OCAMLBEST@ -L theories -D $(ISABELLEREALIZEDRV) -T bool.$(notdir $(basename $@)) -o lib/isabelle/bool/
$(ISABELLELIBS_REAL): bin/why3realize.@OCAMLBEST@ drivers/isabelle-realizations.aux \
drivers/isabelle-realize.drv drivers/isabelle-common.gen theories/real.why
$(ISABELLEREALIZEDRV) drivers/isabelle-common.gen theories/real.why
mkdir -p lib/isabelle/real
WHY3CONFIG="" bin/why3realize.@OCAMLBEST@ -L theories -D drivers/isabelle-realize.drv -T real.$(notdir $(basename $@)) -o lib/isabelle/real/
WHY3CONFIG="" bin/why3realize.@OCAMLBEST@ -L theories -D $(ISABELLEREALIZEDRV) -T real.$(notdir $(basename $@)) -o lib/isabelle/real/
$(ISABELLELIBS_NUMBER): bin/why3realize.@OCAMLBEST@ drivers/isabelle-realizations.aux \
drivers/isabelle-realize.drv drivers/isabelle-common.gen theories/number.why
$(ISABELLEREALIZEDRV) drivers/isabelle-common.gen theories/number.why
mkdir -p lib/isabelle/number
WHY3CONFIG="" bin/why3realize.@OCAMLBEST@ -L theories -D drivers/isabelle-realize.drv -T number.$(notdir $(basename $@)) -o lib/isabelle/number/
WHY3CONFIG="" bin/why3realize.@OCAMLBEST@ -L theories -D $(ISABELLEREALIZEDRV) -T number.$(notdir $(basename $@)) -o lib/isabelle/number/
$(ISABELLELIBS_SET): bin/why3realize.@OCAMLBEST@ drivers/isabelle-realizations.aux \
drivers/isabelle-realize.drv drivers/isabelle-common.gen theories/set.why
$(ISABELLEREALIZEDRV) drivers/isabelle-common.gen theories/set.why
mkdir -p lib/isabelle/set
WHY3CONFIG="" bin/why3realize.@OCAMLBEST@ -L theories -D drivers/isabelle-realize.drv -T set.$(notdir $(basename $@)) -o lib/isabelle/set/
WHY3CONFIG="" bin/why3realize.@OCAMLBEST@ -L theories -D $(ISABELLEREALIZEDRV) -T set.$(notdir $(basename $@)) -o lib/isabelle/set/
$(ISABELLELIBS_MAP): bin/why3realize.@OCAMLBEST@ drivers/isabelle-realizations.aux \
drivers/isabelle-realize.drv drivers/isabelle-common.gen theories/map.why
$(ISABELLEREALIZEDRV) drivers/isabelle-common.gen theories/map.why
mkdir -p lib/isabelle/map
WHY3CONFIG="" bin/why3realize.@OCAMLBEST@ -L theories -D drivers/isabelle-realize.drv -T map.$(notdir $(basename $@)) -o lib/isabelle/map/
WHY3CONFIG="" bin/why3realize.@OCAMLBEST@ -L theories -D $(ISABELLEREALIZEDRV) -T map.$(notdir $(basename $@)) -o lib/isabelle/map/
$(ISABELLELIBS_LIST): bin/why3realize.@OCAMLBEST@ drivers/isabelle-realizations.aux \
drivers/isabelle-realize.drv drivers/isabelle-common.gen theories/list.why
$(ISABELLEREALIZEDRV) drivers/isabelle-common.gen theories/list.why
mkdir -p lib/isabelle/list
WHY3CONFIG="" bin/why3realize.@OCAMLBEST@ -L theories -D drivers/isabelle-realize.drv -T list.$(notdir $(basename $@)) -o lib/isabelle/list/
WHY3CONFIG="" bin/why3realize.@OCAMLBEST@ -L theories -D $(ISABELLEREALIZEDRV) -T list.$(notdir $(basename $@)) -o lib/isabelle/list/
$(ISABELLELIBS_OPTION): bin/why3realize.@OCAMLBEST@ drivers/isabelle-realizations.aux \
drivers/isabelle-realize.drv drivers/isabelle-common.gen theories/option.why
$(ISABELLEREALIZEDRV) drivers/isabelle-common.gen theories/option.why
mkdir -p lib/isabelle/option
WHY3CONFIG="" bin/why3realize.@OCAMLBEST@ -L theories -D drivers/isabelle-realize.drv -T option.$(notdir $(basename $@)) -o lib/isabelle/option/
WHY3CONFIG="" bin/why3realize.@OCAMLBEST@ -L theories -D $(ISABELLEREALIZEDRV) -T option.$(notdir $(basename $@)) -o lib/isabelle/option/
# do not update isabelle realizations systematically
# opt byte: update-isabelle
......@@ -1645,7 +1672,8 @@ STDLIBS = algebra \
real \
relations \
set \
sum
sum \
bv
# function ? tptp ?
STDMODS = array matrix hashtbl impset pqueue queue random ref stack string
......
......@@ -615,18 +615,24 @@ else
reason_isabelle_support=" (isabelle not found)"
else
AC_MSG_CHECKING(Isabelle version)
ISABELLEVERSION=`$ISABELLE version | sed -n -e 's|Isabelle\([[^:]]*\).*$|\1|p' `
ISABELLEDETECTEDVERSION=`$ISABELLE version | sed -n -e 's|Isabelle\([[^:]]*\).*$|\1|p' `
case $ISABELLEVERSION in
case $ISABELLEDETECTEDVERSION in
2014*)
enable_isabelle_support=yes
AC_MSG_RESULT($ISABELLEVERSION)
ISABELLEVERSION=2014
AC_MSG_RESULT($ISABELLEDETECTEDVERSION)
;;
2015*)
enable_isabelle_support=yes
ISABELLEVERSION=2015
AC_MSG_RESULT($ISABELLEDETECTEDVERSION)
;;
*)
AC_MSG_RESULT($ISABELLEVERSION)
AC_MSG_RESULT($ISABELLEDETECTEDVERSION)
enable_isabelle_support=no
AC_MSG_WARN(You need Isabelle2013-2; Isabelle discarded)
reason_isabelle_support=" (need version 2013-2)"
AC_MSG_WARN(You need Isabelle 2014 or 2015; Isabelle discarded)
reason_isabelle_support=" (need version >= 2014)"
;;
esac
fi
......@@ -864,7 +870,7 @@ if test "$enable_pvs_support" = yes ; then
fi
echo " Isabelle : $enable_isabelle_support$reason_isabelle_support"
if test "$enable_isabelle_support" = yes ; then
echo " Version : $ISABELLEVERSION"
echo " Version : $ISABELLEVERSION ($ISABELLEDETECTEDVERSION)"
echo " Realization support : $enable_isabelle_libs$reason_isabelle_libs"
fi
if test "$enable_local" = yes ; then
......
......@@ -11,7 +11,9 @@ using ``Edit'' action in \texttt{why3ide}.
\subsection{Installation}
You need version Isabelle2014. Former versions are not supported.
You need version Isabelle2014 or Isabelle2015. Former versions are not
supported. We assume below that your version is 2015, please replace
2015 by 2014 otherwise.
Isabelle must be installed before compiling \why. After compilation
and installation of \why, you must manually add the path
......@@ -20,7 +22,7 @@ and installation of \why, you must manually add the path
\end{verbatim}
into either the user file
\begin{verbatim}
.isabelle/Isabelle2014/etc/components
.isabelle/Isabelle2015/etc/components
\end{verbatim}
or the system-wide file
\begin{verbatim}
......
theory number.Parity
syntax predicate even "<app><const name=\"Parity.even_odd_class.even\"/>%1</app>"
syntax predicate odd "<app><const name=\"Parity.even_odd_class.odd\"/>%1</app>"
end
theory number.Parity
syntax predicate even "<app><const name=\"Parity.semiring_parity_class.even\"/>%1</app>"
syntax predicate odd "<app><const name=\"Parity.semiring_parity_class.odd\"/>%1</app>"
end
......@@ -146,11 +146,6 @@ theory set.Fset
syntax function cardinal "<app><const name=\"Nat.semiring_1_class.of_nat\"><fun><type name=\"Nat.nat\"/><type name=\"Int.int\"/></fun></const><app><const name=\"FSet.fcard\"/>%1</app></app>"
end
theory number.Parity
syntax predicate even "<app><const name=\"Parity.even_odd_class.even\"/>%1</app>"
syntax predicate odd "<app><const name=\"Parity.even_odd_class.odd\"/>%1</app>"
end
theory number.Divisibility
syntax predicate divides "<app><const name=\"Rings.dvd_class.dvd\"/>%1%2</app>"
end
......
......@@ -7,3 +7,4 @@ filename "%t.xml"
transformation "inline_trivial"
import "isabelle-common.gen"
import "isabelle-2014.gen"
......@@ -8,5 +8,7 @@ transformation "inline_trivial"
transformation "eliminate_builtin"
import "isabelle-common.gen"
import "isabelle-2014.gen"
transformation "simplify_trivial_quantification_in_goal"
(* driver for Isabelle/HOL *)
(* main author: Stefan Berghofer <stefan.berghofer@secunet.com> *)
printer "isabelle-realize"
filename "%t.xml"
transformation "inline_trivial"
import "isabelle-common.gen"
import "isabelle-2015.gen"
(* driver for Isabelle/HOL *)
(* main author: Stefan Berghofer <stefan.berghofer@secunet.com> *)
printer "isabelle"
filename "%f_%t_%g.xml"
transformation "inline_trivial"
transformation "eliminate_builtin"
import "isabelle-common.gen"
import "isabelle-2015.gen"
transformation "simplify_trivial_quantification_in_goal"
......@@ -136,13 +136,6 @@ theory bv.Pow2int
remove prop Power_1
remove prop Power_sum
remove prop pow2pos
remove prop Div_mult_inst
remove prop Div_double
remove prop Div_pow
remove prop Div_double_neg
remove prop Div_pow2
remove prop Div_div_pow
remove prop Mod_pow2_gen
remove prop pow2_0
remove prop pow2_1
remove prop pow2_2
......
This diff is collapsed.
......@@ -123,7 +123,8 @@ module InPlaceCountingSort
0 <= f < v -> numeq a f 0 !j = numeq (at a 'L) f 0 (length a) }
invariant { numeq a v 0 !j = i-1 }
a[!j] <- v;
incr j
incr j;
assert {forall f. 0 <= f < v -> numeq a f 0 !j = numeq a f 0 (!j - 1)}
done
done;
assert { !j = length a }
......
This diff is collapsed.
......@@ -2,9 +2,12 @@
*second edition *)
module Hackers_delight
use import int.Int
use import bool.Bool
(** {2 Utilitaries}
We introduce in this theory two functions that will help us
write properties on bit-manipulating procedures *)
theory Utils
use import bv.BV32
constant one : t = of_int 1
......@@ -14,19 +17,8 @@ module Hackers_delight
function max (x y : t) : t = (if ult x y then y else x)
function min (x y : t) : t = (if ult x y then x else y)
(** {2 ASCII cheksum }
In the beginning the encoding of an ascii character was done on 8
bits: the first 7 bits were used for the carracter itself while
the 8th bit was used as a cheksum: a mean to detect errors. The
cheksum value was the binary sum of the 7 other bits, allowing the
detections of any change of an odd number of bits in the initial
value. Let's prove it! *)
(** {6 Hamming distance } *)
(** In order to express these properties we start by introducing a
function that returns the number of 1-bit in a bitvector (p.82)
*)
(** We start by introducing a function that returns the number of
1-bit in a bitvector (p.82) *)
function count (bv : t) : t =
let x = sub bv (bw_and (lsr_bv bv one) (of_int 0x55555555)) in
......@@ -38,12 +30,34 @@ module Hackers_delight
let x = add x (lsr_bv x (of_int 16)) in
bw_and x (of_int 0x0000003F)
(** We can verify our definition by, first, checking that there are no
1-bits in the bitvector "zero": *)
(** We then define the associated notion of distance, namely
"Hamming distance", that counts the number of bits that differ
between two bitvectors. *)
function hammingD (a b : t) : t = count (bw_xor a b)
end
(** {2 Correctness of Utils}
Before using our two functions let's first check that they are correct !
*)
module Utils_Spec
use import int.Int
use import int.NumOf
use import bv.BV32
use import Utils
(** {6 count correctness } *)
(** Let's start by checking that there are no 1-bits in the
bitvector "zero": *)
lemma countZero: count zero = zero
(** And then, for b a bitvector with n 1-bits, checking that if its
lemma numOfZero: NumOf.numof (\i. nth zero i) 0 32 = 0
(** Now, for b a bitvector with n 1-bits, we check that if its
first bit is 0 then shifting b by one on the right doesn't
change the number of 1-bit. And if its first bit is one, then
there are n-1 1-bits in the shifting of b by one on the right. *)
......@@ -52,27 +66,101 @@ module Hackers_delight
(not (nth_bv b zero) <-> count (lsr_bv b one) = count b) /\
(nth_bv b zero <-> count (lsr_bv b one) = sub (count b) one)
(** We then define the associated notion of distance, namely
"Hamming distance", that counts the number of bits that differ
between two bitvectors. *)
function hammingD (a b : t) : t = count (bw_xor a b)
(** It is indeed a distance in the algebraic sense: *)
let rec lemma numof_shift (p q : int -> bool) (a b k: int) : unit
requires {forall i. q i = p (i + k)}
variant {b - a}
ensures {numof p (a+k) (b+k) = numof q a b}
=
if a < b then
numof_shift p q a (b-1) k
let rec lemma countSpec_Aux (bv : t) : unit
variant {bv with ult}
ensures {to_uint (count bv) = NumOf.numof (nth bv) 0 32}
=
if bv = zero then ()
else
begin
countSpec_Aux (lsr_bv bv one);
assert {
let x = (if nth_bv bv zero then 1 else 0) in
let f = nth bv in
let g = nth (lsr_bv bv one) in
let h = \i. nth bv (i+1) in
(forall i. 0 <= i < 31 -> g i = h i) &&
NumOf.numof f 0 32 - x = NumOf.numof f (0+1) 32 &&
NumOf.numof f (0+1) (31+1) = NumOf.numof h 0 31 &&
NumOf.numof g 0 (32-1) = NumOf.numof g 0 32
}
end
(** With these lemmas, we can now prove the correctness property of
count: *)
lemma countSpec: forall b. to_uint (count b) = NumOf.numof
(nth b) 0 32
(** {6 hammingD correctness } *)
use HighOrd as HO
predicate nth_diff (a b : t) (i : int) = nth a i <> nth b i
(** The correctness property can be express as the following: *)
let lemma hamming_spec (a b : t) : unit
ensures {to_uint (hammingD a b) = NumOf.numof (nth_diff a b) 0 32}
=
assert { forall i. 0 <= i < 32 -> nth (bw_xor a b) i <-> (nth_diff a b i) }
(** In addition we can prove that it is indeed a distance in the
algebraic sens: *)
lemma symmetric: forall a b. hammingD a b = hammingD b a
lemma separation: forall a b. hammingD a b = zero <-> a = b
lemma triangleInequality: forall a b c. (* not proved ! :-( *)
function fun_or (f g : HO.pred 'a) : HO.pred 'a = \x. f x \/ g x
let rec lemma numof_or (p q : int -> bool) (a b: int) : unit
variant {b - a}
ensures {numof (fun_or p q) a b <= numof p a b + numof q a b}
=
if a < b then
numof_or p q a (b-1)
let lemma triangleInequalityInt (a b c : t) : unit
ensures {to_uint (hammingD a b) + to_uint (hammingD b c) >= to_uint (hammingD a c)}
=
assert {numof (nth_diff a b) 0 32 + numof (nth_diff b c) 0 32 >=
numof (fun_or (nth_diff a b) (nth_diff b c)) 0 32 >=
numof (nth_diff a c) 0 32}
lemma triangleInequality: forall a b c.
uge (add (hammingD a b) (hammingD b c)) (hammingD a c)
end
module Hackers_delight
use import int.Int
use import int.NumOf
use import bool.Bool
use import bv.BV32
use import Utils
(** {2 ASCII cheksum }
In the beginning the encoding of an ascii character was done on 8
bits: the first 7 bits were used for the carracter itself while
the 8th bit was used as a cheksum: a mean to detect errors. The
cheksum value was the binary sum of the 7 other bits, allowing the
detections of any change of an odd number of bits in the initial
value. Let's prove it! *)
(** {6 Checksum computation and correctness } *)
(** A ascii character is valid if its number of bits is even.
(Remember that a binary number is odd if and only if its first
bit is 1) *)
predicate validAscii (b : t) = not (nth_bv (count b) zero)
predicate validAscii (b : t) = (nth_bv (count b) zero) = False
(** The ascii checksum aim is to make any character valid in the
sens that we just defined. One way to implement it is to count
......
......@@ -5,47 +5,141 @@
<prover id="0" name="Alt-Ergo" version="0.99.1" timelimit="5" memlimit="1000"/>
<prover id="1" name="CVC4" version="1.4" timelimit="5" memlimit="1000"/>
<prover id="2" name="Z3" version="4.3.2" timelimit="5" memlimit="1000"/>
<prover id="3" name="CVC3" version="2.4.1" timelimit="5" memlimit="1000"/>
<file name="../hackers-delight.mlw" expanded="true">
<theory name="Hackers_delight" sum="f0a189c908de4dca4a7d7f3ad4145727" expanded="true">
<theory name="Utils" sum="d41d8cd98f00b204e9800998ecf8427e" expanded="true">
</theory>
<theory name="Utils_Spec" sum="3967722ffb6389d883275ccf0879b34f" expanded="true">
<goal name="countZero" expanded="true">
<proof prover="1"><result status="valid" time="0.05"/></proof>
<proof prover="2"><result status="valid" time="0.09"/></proof>
<proof prover="1"><result status="valid" time="0.03"/></proof>
<proof prover="2"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="numOfZero" expanded="true">
<proof prover="0"><result status="valid" time="0.87" steps="228"/></proof>
<proof prover="3"><result status="valid" time="0.78"/></proof>
</goal>
<goal name="countStep" expanded="true">
<proof prover="1"><result status="valid" time="4.98"/></proof>
<proof prover="1" timelimit="30"><result status="valid" time="5.82"/></proof>
</goal>
<goal name="WP_parameter numof_shift" expl="VC for numof_shift" expanded="true">
<proof prover="1"><result status="valid" time="0.24"/></proof>
<proof prover="2"><result status="valid" time="0.04"/></proof>
<proof prover="3"><result status="valid" time="0.34"/></proof>
</goal>
<goal name="WP_parameter countSpec_Aux" expl="VC for countSpec_Aux" expanded="true">
<transf name="split_goal_wp" expanded="true">
<goal name="WP_parameter countSpec_Aux.1" expl="1. postcondition" expanded="true">
<proof prover="0"><result status="valid" time="0.89" steps="265"/></proof>
<proof prover="1"><result status="valid" time="0.04"/></proof>
<proof prover="3"><result status="valid" time="0.61"/></proof>
</goal>
<goal name="WP_parameter countSpec_Aux.2" expl="2. variant decrease" expanded="true">
<proof prover="1"><result status="valid" time="0.02"/></proof>
<proof prover="2"><result status="valid" time="0.02"/></proof>
<proof prover="3"><result status="valid" time="0.99"/></proof>
</goal>
<goal name="WP_parameter countSpec_Aux.3" expl="3. assertion" expanded="true">
<transf name="split_goal_wp" expanded="true">
<goal name="WP_parameter countSpec_Aux.3.1" expl="1. assertion" expanded="true">
<proof prover="3"><result status="valid" time="1.86"/></proof>
</goal>
<goal name="WP_parameter countSpec_Aux.3.2" expl="2. assertion" expanded="true">
<proof prover="3"><result status="valid" time="0.60"/></proof>
</goal>
<goal name="WP_parameter countSpec_Aux.3.3" expl="3. assertion" expanded="true">
<proof prover="0"><result status="valid" time="0.90" steps="158"/></proof>
</goal>
<goal name="WP_parameter countSpec_Aux.3.4" expl="4. assertion" expanded="true">
<proof prover="3" timelimit="15"><result status="valid" time="7.26"/></proof>
</goal>
</transf>
</goal>
<goal name="WP_parameter countSpec_Aux.4" expl="4. postcondition" expanded="true">
<proof prover="1"><result status="valid" time="0.57"/></proof>
</goal>
</transf>
</goal>
<goal name="countSpec" expanded="true">
<proof prover="0"><result status="valid" time="0.05" steps="72"/></proof>
<proof prover="1"><result status="valid" time="0.10"/></proof>
<proof prover="2"><result status="valid" time="0.00"/></proof>
<proof prover="3"><result status="valid" time="0.04"/></proof>
</goal>
<goal name="WP_parameter hamming_spec" expl="VC for hamming_spec" expanded="true">