Commit efbee659 authored by Martin Clochard's avatar Martin Clochard

Merge branch 'master' into byso

parents bc541ef4 72b7667e
......@@ -1203,8 +1203,8 @@ drivers/isabelle-realizations.aux: Makefile
echo 'theory list.'"$$f"' meta "realized_theory" "list.'"$$f"'", "" end'; done; \
for f in $(ISABELLELIBS_OPTION_FILES); do \
echo 'theory option.'"$$f"' meta "realized_theory" "option.'"$$f"'", "" end'; done; \
# for f in $(ISABELLELIBS_BV_FILES); do \
# echo 'theory bv.'"$$f"' meta "realized_theory" "bv.'"$$f"'", "" end'; done; \
for f in $(ISABELLELIBS_BV_FILES); do \
echo 'theory bv.'"$$f"' meta "realized_theory" "bv.'"$$f"'", "" end'; done; \
) > $@
ifeq (@enable_local@,yes)
......@@ -1213,8 +1213,7 @@ else
ISABELLE_TARGET_DIR=$(LIBDIR)/why3/isabelle
endif
lib/isabelle/last_build: $(ISABELLEVERSIONSPECIFICTARGETS) $(ISABELLELIBS_INT) $(ISABELLELIBS_BOOL) $(ISABELLELIBS_REAL) $(ISABELLELIBS_NUMBER) $(ISABELLELIBS_SET) $(ISABELLELIBS_MAP) $(ISABELLELIBS_LIST) $(ISABELLELIBS_OPTION)
# $(ISABELLELIBS_BV)
lib/isabelle/last_build: $(ISABELLEVERSIONSPECIFICTARGETS) $(ISABELLELIBS_INT) $(ISABELLELIBS_BOOL) $(ISABELLELIBS_REAL) $(ISABELLELIBS_NUMBER) $(ISABELLELIBS_SET) $(ISABELLELIBS_MAP) $(ISABELLELIBS_LIST) $(ISABELLELIBS_OPTION) $(ISABELLELIBS_BV)
ifneq (@enable_local@,yes)
cp -r lib/isabelle "$(LIBDIR)/why3"
endif
......
(** Why3 driver specific for checking BV theory consistency with CVC4 *)
prelude "(set-logic AUFBVDTNIRA)"
(*
A : Array
UF : Uninterpreted Function
BV : BitVectors
DT : Datatypes
NIRA : NonLinear Integer Reals Arithmetic
*)
(* prelude "(set-logic ALL_SUPPORTED)"
does not seem to include DT
*)
import "smt-libv2.drv"
import "smt-libv2-bv-realization.gen"
import "discrimination.gen"
transformation "inline_trivial"
transformation "eliminate_builtin"
transformation "detect_polymorphism"
transformation "eliminate_definition"
(* We could keep more definitions by using
transformation "eliminate_definition_if_poly"
instead, but some proofs are lost
(examples/logic/triangle_inequality.why)
*)
transformation "eliminate_inductive"
transformation "eliminate_algebraic_if_poly"
transformation "eliminate_epsilon"
transformation "simplify_formula"
(*transformation "simplify_trivial_quantification"*)
transformation "discriminate_if_poly"
transformation "encoding_smt_if_poly"
(** Error messages specific to CVC4 *)
outofmemory "(error \".*out of memory\")\\|Cannot allocate memory"
timeout "interrupted by timeout"
steps "smt::SmtEngine::resourceUnitsUsed, \\([0-9]+.?[0-9]*\\)" 1
(**
Unfortunately, there is no specific output message when CVC4 reaches its resource limit
steplimitexceeded "??"
*)
(** Extra theories supported by CVC4 *)
(* Disabled:
CVC4 seems less efficient with its built-in implementation than
with the axiomatic version
*)
(*
theory int.EuclideanDivision
syntax function div "(div %1 %2)"
syntax function mod "(mod %1 %2)"
remove prop Mod_bound
remove prop Div_mod
remove prop Mod_1
remove prop Div_1
end
*)
import "cvc4_bv.gen"
(* Why3 driver checking compatibility of BV theories with SMT-LIB2 *)
theory bv.BV_Gen
syntax function bw_and "(bvand %1 %2)"
syntax function bw_or "(bvor %1 %2)"
syntax function bw_xor "(bvxor %1 %2)"
syntax function bw_not "(bvnot %1)"
syntax function add "(bvadd %1 %2)"
syntax function sub "(bvsub %1 %2)"
syntax function neg "(bvneg %1)"
syntax function mul "(bvmul %1 %2)"
syntax function udiv "(bvudiv %1 %2)"
syntax function urem "(bvurem %1 %2)"
syntax function lsr_bv "(bvlshr %1 %2)"
syntax function lsl_bv "(bvshl %1 %2)"
syntax function asr_bv "(bvashr %1 %2)"
syntax predicate eq "(= %1 %2)"
syntax predicate ult "(bvult %1 %2)"
syntax predicate ule "(bvule %1 %2)"
syntax predicate ugt "(bvugt %1 %2)"
syntax predicate uge "(bvuge %1 %2)"
syntax predicate slt "(bvslt %1 %2)"
syntax predicate sle "(bvsle %1 %2)"
syntax predicate sgt "(bvsgt %1 %2)"
syntax predicate sge "(bvsge %1 %2)"
(** Removing the axioms that should be proved instead
the one that are commented out are instead kept
*)
remove prop size_pos
remove prop nth_out_of_bound
remove prop Nth_zero
remove prop Nth_ones
remove prop Nth_bw_and
remove prop Nth_bw_or
remove prop Nth_bw_xor
remove prop Nth_bw_not
remove prop Lsr_nth_low
remove prop Lsr_nth_high
remove prop lsr_zero
remove prop Asr_nth_low
remove prop Asr_nth_high
remove prop asr_zero
remove prop Lsl_nth_high
remove prop Lsl_nth_low
remove prop lsl_zero
remove prop Nth_rotate_right
remove prop Nth_rotate_left
(* Conversions from/to integers *)
remove prop two_power_size_val
remove prop max_int_val
remove prop to_uint_extensionality
remove prop to_int_extensionality
remove prop to_uint_bounds
remove prop to_uint_of_int
remove prop Of_int_zero
remove prop Of_int_ones
(** Arithmetic operators *)
remove prop to_uint_add
remove prop to_uint_add_bounded
remove prop to_uint_sub
remove prop to_uint_sub_bounded
remove prop to_uint_neg
remove prop to_uint_mul
remove prop to_uint_mul_bounded
remove prop to_uint_udiv
remove prop to_uint_urem
(* kept: Nth_bv_is_nth *)
(* kept: Nth_bv_is_nth2 *)
(* kept: lsr_bv_is_lsr *)
remove prop to_uint_lsr
(* kept: asr_bv_is_asr *)
(* kept: lsl_bv_is_lsl *)
remove prop to_uint_lsl
(* kept: rotate_left_bv_is_rotate_left *)
(* kept: rotate_right_bv_is_rotate_right *)
remove prop eq_sub_equiv
remove prop Extensionality
end
theory bv.BV64
syntax type t "(_ BitVec 64)"
syntax function zero "#x0000000000000000"
syntax function ones "#xFFFFFFFFFFFFFFFF"
syntax function nth_bv
"(not (= (bvand (bvlshr %1 %2) (_ bv1 64)) (_ bv0 64)))"
(* possible alternative definition :
"(= ((_ extract 0 0) (bvlshr %1 %2)) (_ bv1 1))"
*)
syntax function rotate_left_bv "(bvor (bvshl %1 (bvurem %2 (_ bv64 64))) (bvlshr %1 (bvsub (_ bv64 64) (bvurem %2 (_ bv64 64)))))"
syntax function rotate_right_bv "(bvor (bvlshr %1 (bvurem %2 (_ bv64 64))) (bvshl %1 (bvsub (_ bv64 64) (bvurem %2 (_ bv64 64)))))"
end
theory bv.BV32
syntax type t "(_ BitVec 32)"
syntax function zero "#x00000000"
syntax function ones "#xFFFFFFFF"
syntax function nth_bv
"(not (= (bvand (bvlshr %1 %2) (_ bv1 32)) (_ bv0 32)))"
syntax function rotate_left_bv "(bvor (bvshl %1 (bvurem %2 (_ bv32 32))) (bvlshr %1 (bvsub (_ bv32 32) (bvurem %2 (_ bv32 32)))))"
syntax function rotate_right_bv "(bvor (bvlshr %1 (bvurem %2 (_ bv32 32))) (bvshl %1 (bvsub (_ bv32 32) (bvurem %2 (_ bv32 32)))))"
end
theory bv.BV16
syntax type t "(_ BitVec 16)"
syntax function zero "#x0000"
syntax function ones "#xFFFF"
syntax function nth_bv
"(not (= (bvand (bvlshr %1 %2) (_ bv1 16)) (_ bv0 16)))"
syntax function rotate_left_bv "(bvor (bvshl %1 (bvurem %2 (_ bv16 16))) (bvlshr %1 (bvsub (_ bv16 16) (bvurem %2 (_ bv16 16)))))"
syntax function rotate_right_bv "(bvor (bvlshr %1 (bvurem %2 (_ bv16 16))) (bvshl %1 (bvsub (_ bv16 16) (bvurem %2 (_ bv16 16)))))"
end
theory bv.BV8
syntax type t "(_ BitVec 8)"
syntax function zero "#x00"
syntax function ones "#xFF"
syntax function nth_bv
"(not (= (bvand (bvlshr %1 %2) (_ bv1 8)) (_ bv0 8)))"
syntax function rotate_left_bv "(bvor (bvshl %1 (bvurem %2 (_ bv8 8))) (bvlshr %1 (bvsub (_ bv8 8) (bvurem %2 (_ bv8 8)))))"
syntax function rotate_right_bv "(bvor (bvlshr %1 (bvurem %2 (_ bv8 8))) (bvshl %1 (bvsub (_ bv8 8) (bvurem %2 (_ bv8 8)))))"
end
theory bv.BVConverter_Gen
remove allprops
end
theory bv.BVConverter_32_64
syntax function toBig "((_ zero_extend 32) %1)"
syntax function toSmall "((_ extract 31 0) %1)"
end
theory bv.BVConverter_16_64
syntax function toBig "((_ zero_extend 48) %1)"
syntax function toSmall "((_ extract 15 0) %1)"
end
theory bv.BVConverter_8_64
syntax function toBig "((_ zero_extend 56) %1)"
syntax function toSmall "((_ extract 7 0) %1)"
end
theory bv.BVConverter_16_32
syntax function toBig "((_ zero_extend 16) %1)"
syntax function toSmall "((_ extract 15 0) %1)"
end
theory bv.BVConverter_8_32
syntax function toBig "((_ zero_extend 24) %1)"
syntax function toSmall "((_ extract 7 0) %1)"
end
theory bv.BVConverter_8_16
syntax function toBig "((_ zero_extend 8) %1)"
syntax function toSmall "((_ extract 7 0) %1)"
end
theory bv.Pow2int
remove allprops
end
......@@ -22,6 +22,26 @@ theory bv.BV_Gen
(* Warning: we should NOT remove all the axioms using "allprops" *)
remove prop nth_out_of_bound
remove prop Nth_zero
remove prop Nth_ones
remove prop two_power_size_val
remove prop max_int_val
remove prop eq_sub_equiv
remove prop Nth_bw_or
remove prop Nth_bw_and
remove prop Nth_bw_xor
remove prop Nth_bw_not
remove prop Nth_rotate_left
remove prop Nth_rotate_right
remove prop to_uint_extensionality
remove prop to_uint_bounds
remove prop to_int_extensionality
remove prop Of_int_zero
remove prop Of_int_ones
remove prop to_uint_add
remove prop to_uint_add_bounded
remove prop to_uint_sub
......@@ -31,16 +51,9 @@ theory bv.BV_Gen
remove prop to_uint_mul_bounded
remove prop to_uint_udiv
remove prop to_uint_urem
remove prop Nth_bv_is_nth
remove prop Nth_bv_is_nth2
remove prop lsr_bv_is_lsr
remove prop to_uint_lsr
remove prop asr_bv_is_asr
remove prop lsl_bv_is_lsl
remove prop to_uint_lsl
remove prop rotate_left_bv_is_rotate_left
remove prop rotate_right_bv_is_rotate_right
remove prop Extensionality
syntax predicate ult "(bvult %1 %2)"
......
(** Why3 driver for Z3 >= 4.3.2 *)
(* Do not set any logic, let z3 choose by itself
prelude "(set-logic AUFNIRA)"
*)
(* Counterexamples: set model parser *)
model_parser "smtv2"
import "smt-libv2.drv"
import "smt-libv2-bv-realization.gen"
import "discrimination.gen"
transformation "inline_trivial"
transformation "eliminate_builtin"
transformation "detect_polymorphism"
transformation "eliminate_definition"
(* We could keep more definitions by using
transformation "eliminate_definition_if_poly"
instead, but some proofs are lost
(examples/logic/triangle_inequality.why)
*)
transformation "eliminate_inductive"
transformation "eliminate_algebraic_if_poly"
transformation "eliminate_epsilon"
transformation "simplify_formula"
(*transformation "simplify_trivial_quantification"*)
(* Prepare for counter-example query: get rid of some quantifiers (makes it
possible to query model values of the variables in premises) and introduce
counter-example projections *)
transformation "prepare_for_counterexmp"
transformation "discriminate_if_poly"
transformation "encoding_smt_if_poly"
(** Error messages specific to Z3 *)
outofmemory "(error \".*out of memory\")\\|Cannot allocate memory"
timeout "interrupted by timeout"
(** Extra theories supported by Z3 *)
(* div/mod of Z3 seems to be Euclidean Division *)
theory int.EuclideanDivision
syntax function div "(div %1 %2)"
syntax function mod "(mod %1 %2)"
remove prop Mod_bound
remove prop Div_mod
remove prop Mod_1
remove prop Div_1
end
theory real.FromInt
syntax function from_int "(to_real %1)"
remove prop Zero
remove prop One
remove prop Add
remove prop Sub
remove prop Mul
remove prop Neg
end
(* does not work: Z3 segfaults
theory real.Trigonometry
syntax function cos "(cos %1)"
syntax function sin "(sin %1)"
syntax function pi "pi"
syntax function tan "(tan %1)"
syntax function atan "(atan %1)"
end
*)
(* bitvector modules, is not in smt-libv2.drv since cvc4 and z3 don't
have the same name for the function to_uint *)
theory bv.BV64
syntax converter of_int "((_ int2bv 64) %1)"
syntax function to_uint "(bv2int %1)"
end
theory bv.BV32
syntax converter of_int "((_ int2bv 32) %1)"
syntax function to_uint "(bv2int %1)"
end
theory bv.BV16
syntax converter of_int "((_ int2bv 16) %1)"
syntax function to_uint "(bv2int %1)"
end
theory bv.BV8
syntax converter of_int "((_ int2bv 8) %1)"
syntax function to_uint "(bv2int %1)"
end
......@@ -82,19 +82,31 @@ end
theory bv.BV64
syntax converter of_int "((_ int2bv 64) %1)"
syntax function to_uint "(bv2int %1)"
remove prop Nth_bv_is_nth
remove prop Nth_bv_is_nth2
end
theory bv.BV32
syntax converter of_int "((_ int2bv 32) %1)"
syntax function to_uint "(bv2int %1)"
remove prop Nth_bv_is_nth
remove prop Nth_bv_is_nth2
end
theory bv.BV16
syntax converter of_int "((_ int2bv 16) %1)"
syntax function to_uint "(bv2int %1)"
remove prop Nth_bv_is_nth
remove prop Nth_bv_is_nth2
end
theory bv.BV8
syntax converter of_int "((_ int2bv 8) %1)"
syntax function to_uint "(bv2int %1)"
remove prop Nth_bv_is_nth
remove prop Nth_bv_is_nth2
end
......@@ -407,6 +407,8 @@ module AsciiCode
end
(*** unfinished
module GrayCode
use import int.Int
use import int.NumOf
......@@ -489,3 +491,5 @@ module GrayCode
nth_bv b zero <-> even (count_logic (toGray b))
end
*)
......@@ -5,11 +5,10 @@
<prover id="0" name="Alt-Ergo" version="0.99.1" timelimit="5" memlimit="1000"/>
<prover id="1" name="CVC3" version="2.4.1" timelimit="30" memlimit="1000"/>
<prover id="2" name="CVC4" version="1.4" timelimit="5" memlimit="1000"/>
<prover id="3" name="Z3" version="4.4.0" alternative="noBV" timelimit="5" memlimit="1000"/>
<prover id="4" name="Z3" version="4.4.0" timelimit="5" memlimit="1000"/>
<prover id="5" name="CVC4" version="1.4" alternative="noBV" timelimit="5" memlimit="1000"/>
<prover id="5" name="CVC4" version="1.4" alternative="noBV" timelimit="30" memlimit="1000"/>
<file name="../bitcount.mlw" expanded="true">
<theory name="BitCount8bit_fact" sum="5751fad0b4d740cb2042ca2423c25c5e">
<theory name="BitCount8bit_fact" sum="5751fad0b4d740cb2042ca2423c25c5e" expanded="true">
<goal name="nth_as_bv_is_int">
<proof prover="0"><result status="valid" time="0.18" steps="95"/></proof>
</goal>
......@@ -73,7 +72,7 @@
<proof prover="2"><result status="valid" time="0.07"/></proof>
</goal>
<goal name="WP_parameter step2.5.5" expl="5. assertion">
<proof prover="5" timelimit="30"><result status="valid" time="7.94"/></proof>
<proof prover="5"><result status="valid" time="7.94"/></proof>
</goal>
</transf>
</goal>
......@@ -138,7 +137,7 @@
</transf>
</goal>
</theory>
<theory name="BitCounting32" sum="9f25f7ff7a6a81cbcd2f8a85a25ec49b">
<theory name="BitCounting32" sum="9f25f7ff7a6a81cbcd2f8a85a25ec49b" expanded="true">
<goal name="WP_parameter proof0" expl="VC for proof0">
<transf name="split_goal_wp">
<goal name="WP_parameter proof0.1" expl="1. assertion">
......@@ -379,7 +378,7 @@
</transf>
</goal>
</theory>
<theory name="Hamming" sum="dfdc0f1acb686591cb859b028bb81cbe">
<theory name="Hamming" sum="dfdc0f1acb686591cb859b028bb81cbe" expanded="true">
<goal name="WP_parameter hammingD" expl="VC for hammingD">
<transf name="split_goal_wp">
<goal name="WP_parameter hammingD.1" expl="1. assertion">
......@@ -424,7 +423,7 @@
<proof prover="2"><result status="valid" time="0.04"/></proof>
</goal>
</theory>
<theory name="AsciiCode" sum="65a00d71812a6ba057f736c4159b37f1">
<theory name="AsciiCode" sum="65a00d71812a6ba057f736c4159b37f1" expanded="true">
<goal name="WP_parameter bv_even" expl="VC for bv_even">
<transf name="split_goal_wp">
<goal name="WP_parameter bv_even.1" expl="1. assertion">
......@@ -463,7 +462,7 @@
<proof prover="4"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="WP_parameter count_or.4" expl="4. assertion">
<proof prover="5"><result status="valid" time="2.21"/></proof>
<proof prover="5" timelimit="5"><result status="valid" time="2.21"/></proof>
</goal>
<goal name="WP_parameter count_or.5" expl="5. postcondition">
<proof prover="0"><result status="valid" time="0.06" steps="74"/></proof>
......@@ -540,43 +539,5 @@
<proof prover="2"><result status="valid" time="0.05"/></proof>
</goal>
</theory>
<theory name="GrayCode" sum="6a0d92707e1971d288ea37b644e08ee7" expanded="true">
<goal name="iso">
<proof prover="2"><result status="valid" time="0.46"/></proof>
</goal>
<goal name="WP_parameter grayIsGray" expl="VC for grayIsGray" expanded="true">
<transf name="split_goal_wp" expanded="true">
<goal name="WP_parameter grayIsGray.1" expl="1. assertion">
<proof prover="0"><result status="timeout" time="5.01"/></proof>
<proof prover="2"><result status="valid" time="0.07"/></proof>
</goal>
<goal name="WP_parameter grayIsGray.2" expl="2. assertion" expanded="true">
</goal>
<goal name="WP_parameter grayIsGray.3" expl="3. assertion" expanded="true">
</goal>
<goal name="WP_parameter grayIsGray.4" expl="4. assertion">
<proof prover="0"><result status="timeout" time="4.99"/></proof>
<proof prover="2"><result status="valid" time="0.06"/></proof>
<proof prover="3"><result status="timeout" time="5.01"/></proof>
<proof prover="4"><result status="valid" time="0.03"/></proof>
<proof prover="5"><result status="timeout" time="5.11"/></proof>
</goal>
<goal name="WP_parameter grayIsGray.5" expl="5. postcondition" expanded="true">
</goal>
</transf>
</goal>
<goal name="nthGray">
<proof prover="0"><result status="valid" time="1.38" steps="555"/></proof>
<proof prover="2"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="lastNthGray">
<proof prover="2"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="nthBinary" expanded="true">
</goal>
<goal name="evenOdd">
<proof prover="5"><result status="valid" time="0.68"/></proof>
</goal>
</theory>
</file>
</why3session>
......@@ -25,7 +25,7 @@
<proof prover="1"><result status="valid" time="0.16"/></proof>
</goal>
<goal name="WP_parameter nth_ultpre0.3" expl="3. postcondition">
<proof prover="0"><result status="valid" time="0.47" steps="210"/></proof>
<proof prover="0"><result status="valid" time="0.52" steps="210"/></proof>
<proof prover="6"><result status="valid" time="0.30"/></proof>
</goal>
</transf>
......@@ -61,7 +61,7 @@
</goal>
<goal name="WP_parameter poke_64bit_bv.9" expl="9. postcondition">
<proof prover="0"><result status="valid" time="0.34" steps="188"/></proof>
<proof prover="6"><result status="valid" time="0.08"/></proof>
<proof prover="6"><result status="valid" time="0.22"/></proof>
</goal>
<goal name="WP_parameter poke_64bit_bv.10" expl="10. postcondition">
<proof prover="0"><result status="valid" time="0.29" steps="163"/></proof>
......@@ -121,7 +121,7 @@
<proof prover="1"><result status="valid" time="0.09"/></proof>
</goal>
<goal name="WP_parameter peek_8bit_bv.6" expl="6. postcondition">
<proof prover="0"><result status="valid" time="1.46" steps="611"/></proof>
<proof prover="0"><result status="valid" time="1.56" steps="611"/></proof>
</goal>
</transf>
</goal>
......@@ -214,7 +214,7 @@
<proof prover="3"><result status="valid" time="0.05"/></proof>
</goal>
<goal name="WP_parameter peek.13" expl="13. precondition">
<proof prover="3"><result status="valid" time="0.67"/></proof>
<proof prover="3"><result status="valid" time="0.72"/></proof>
</goal>
<goal name="WP_parameter peek.14" expl="14. precondition">
<proof prover="0"><result status="valid" time="0.10" steps="96"/></proof>
......@@ -231,14 +231,14 @@
<proof prover="3"><result status="valid" time="0.12"/></proof>
</goal>
<goal name="WP_parameter peek.17" expl="17. loop invariant preservation">
<proof prover="4"><result status="valid" time="1.55" steps="458"/></proof>
<proof prover="4"><result status="valid" time="1.65" steps="458"/></proof>
</goal>
<goal name="WP_parameter peek.18" expl="18. loop invariant preservation">
<proof prover="5"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="WP_parameter peek.19" expl="19. loop invariant preservation">
<proof prover="5"><result status="valid" time="0.02"/></proof>
<proof prover="6"><result status="valid" time="0.11"/></proof>
<proof prover="6"><result status="valid" time="0.25"/></proof>
</goal>
<goal name="WP_parameter peek.20" expl="20. loop variant decrease">
<proof prover="0"><result status="valid" time="0.14" steps="104"/></proof>
......@@ -297,7 +297,7 @@
<goal name="WP_parameter poke_8bit.3" expl="3. precondition">
<proof prover="0"><result status="valid" time="0.10" steps="103"/></proof>
<proof prover="1"><result status="valid" time="0.10"/></proof>
<proof prover="3"><result status="valid" time="0.11"/></proof>
<proof prover="3"><result status="valid" time="0.12"/></proof>
</goal>
<goal name="WP_parameter poke_8bit.4" expl="4. precondition">
<proof prover="0"><result status="valid" time="0.02" steps="82"/></proof>
......@@ -317,10 +317,10 @@
<proof prover="1"><result status="valid" time="0.08"/></proof>
</goal>
<goal name="WP_parameter poke_8bit.9" expl="9. postcondition">
<proof prover="3"><result status="valid" time="2.02"/></proof>
<proof prover="3"><result status="valid" time="1.68"/></proof>
</goal>
<goal name="WP_parameter poke_8bit.10" expl="10. postcondition">
<proof prover="3"><result status="valid" time="1.26"/></proof>
<proof prover="3"><result status="valid" time="0.88"/></proof>
</goal>
</transf>
</goal>
......@@ -357,7 +357,7 @@
<goal name="WP_parameter poke_8bit_array.6" expl="6. precondition">
<proof prover="0"><result status="valid" time="0.34" steps="196"/></proof>
<proof prover="1"><result status="valid" time="0.08"/></proof>
<proof prover="3"><result status="valid" time="1.40"/></proof>
<proof prover="3"><result status="valid" time="1.52"/></proof>
<proof prover="5"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="WP_parameter poke_8bit_array.7" expl="7. index in array bounds">
......@@ -446,7 +446,7 @@
<proof prover="3"><result status="valid" time="0.05"/></proof>
</goal>
<goal name="WP_parameter poke.16" expl="16. precondition">
<proof prover="3"><result status="valid" time="0.86"/></proof>
<proof prover="3"><result status="valid" time="1.03"/></proof>
</goal>
<goal name="WP_parameter poke.17" expl="17. precondition">
<proof prover="3"><result status="valid" time="0.07"/></proof>
......@@ -508,14 +508,14 @@
<proof prover="0"><result status="valid" time="0.29" steps="129"/></proof>
</goal>
<goal name="WP_parameter poke.27" expl="27. loop invariant preservation">
<proof prover="0"><result status="valid" time="1.52" steps="125"/></proof>
<proof prover="0"><result status="valid" time="1.16" steps="125"/></proof>
</goal>
<goal name="WP_parameter poke.28" expl="28. loop invariant preservation">
<proof prover="0"><result status="valid" time="0.75" steps="119"/></proof>
<proof prover="0"><result status="valid" time="0.49" steps="119"/></proof>
</goal>
<goal name="WP_parameter poke.29" expl="29. loop variant decrease">
<proof prover="0"><result status="valid" time="0.20" steps="104"/></proof>
<proof prover="3"><result status="valid" time="0.80"/></proof>
<proof prover="3"><result status="valid" time="0.86"/></proof>
</goal>
<goal name="WP_parameter poke.30" expl="30. type invariant">
<proof prover="0"><result status="valid" time="0.05" steps="88"/></proof>
......@@ -592,7 +592,7 @@
<proof prover="5"><result status="valid" time="0.00"/></proof>
</goal>
<goal name="WP_parameter peekthenpoke.8" expl="8. assertion">
<proof prover="3"><result status="valid" time="0.71"/></proof>
<proof prover="3"><result status="valid" time="0.76"/></proof>
</goal>
<goal name="WP_parameter peekthenpoke.9" expl="9. postcondition">
<proof prover="0"><result status="valid" time="0.02" steps="86"/></proof>
......@@ -646,7 +646,7 @@
<proof prover="3"><result status="valid" time="0.08"/></proof>
</goal>
<goal name="WP_parameter pokethenpeek.9" expl="9. assertion">
<proof prover="0"><result status="valid" time="1.07" steps="364"/></proof>
<proof prover="0"><result status="valid" time="1.26" steps="364"/></proof>
</goal>
<goal name="WP_parameter pokethenpeek.10" expl="10. postcondition">
<proof prover="0"><result status="valid" time="0.18" steps="97"/></proof>
......
......@@ -129,13 +129,11 @@
</goal>
<goal name="g8aa" expanded="true">
<proof prover="0"><result status="timeout" time="5.00"/></proof>
<proof prover="2"><result status="unknown" time="0.01"/></proof>
<proof prover="2"><result status="timeout" time="5.02"/></proof>
<proof prover="4"><result status="timeout" time="4.99"/></proof>
</goal>
<goal name="g8bb" expanded="true">
<proof prover="0"><result status="timeout" time="5.01"/></proof>
<proof prover="2"><result status="unknown" time="0.01"/></proof>
<proof prover="4"><result status="timeout" time="5.00"/></proof>
<proof prover="2"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="gtt">
<proof prover="0"><result status="valid" time="0.13" steps="80"/></proof>
......
......@@ -57,7 +57,7 @@ module OptimalReplay
0 < d[k] = d[g[k]] + 1 /\
forall k': int. g[k] < k' < k -> d[g[k]] < d[k'] }
(* could be deduced from above, but avoids induction *)
invariant { forall k: int. 0 <= k < i -> path d[k] k }
invariant { forall k: int. 0 <= k < i -> distance d[k] k }
let j = ref (i-1) in
while g[!j] >= f i do
invariant { f i <= !j < i /\ !count + d[!j] <= i-1 }
......
(* This file is generated by Why3's Coq driver *)
(* Beware! Only edit allowed sections below *)
Require Import BuiltIn.
Require BuiltIn.
Require int.Int.
Require map.Map.
(* Why3 assumption *)
Definition unit := unit.