...
  View open merge request
Commits (7)
...@@ -998,7 +998,7 @@ COQLIBS_IEEEFLOAT_FILES = RoundingMode GenericFloat Float32 Float64 ...@@ -998,7 +998,7 @@ COQLIBS_IEEEFLOAT_FILES = RoundingMode GenericFloat Float32 Float64
COQLIBS_IEEEFLOAT = $(addprefix lib/coq/ieee_float/, $(COQLIBS_IEEEFLOAT_FILES)) COQLIBS_IEEEFLOAT = $(addprefix lib/coq/ieee_float/, $(COQLIBS_IEEEFLOAT_FILES))
endif endif
COQLIBS_FOR_DRIVERS_FILES = ComputerOfEuclideanDivision COQLIBS_FOR_DRIVERS_FILES =
COQLIBS_FOR_DRIVERS = $(addprefix lib/coq/for_drivers/, $(COQLIBS_FOR_DRIVERS_FILES)) COQLIBS_FOR_DRIVERS = $(addprefix lib/coq/for_drivers/, $(COQLIBS_FOR_DRIVERS_FILES))
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_FP) $(COQLIBS_BV) $(COQLIBS_IEEEFLOAT) $(COQLIBS_FOR_DRIVERS) 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_FP) $(COQLIBS_BV) $(COQLIBS_IEEEFLOAT) $(COQLIBS_FOR_DRIVERS)
......
...@@ -102,6 +102,13 @@ theory int.ComputerDivision ...@@ -102,6 +102,13 @@ theory int.ComputerDivision
end end
theory for_drivers.ComputerOfEuclideanDivision
remove prop cdiv_cases_0
remove prop cdiv_cases_1
end
theory real.Real theory real.Real
......
(** Why3 driver for Colibri (with floating point support) *)
prelude ";; produced by colibri.drv ;;"
prelude "(set-logic QF_NIRABVFP)"
prelude "(set-info :smt-lib-version 2.6)"
import "smt-libv2.gen"
printer "smtv2"
import "smt-libv2-bv.gen"
import "cvc4_bv.gen"
import "smt-libv2-floats.gen"
(* import "discrimination.gen" *)
theory BuiltIn
meta "select_inst_default" "all"
meta "select_lskept_default" "all"
meta "select_lsinst_default" "all"
meta "select_kept_default" "all"
end
transformation "inline_trivial"
transformation "eliminate_builtin"
(* transformation "detect_polymorphism" because eliminate algebraic
add polymorphism *)
transformation "eliminate_definition"
transformation "eliminate_inductive"
transformation "eliminate_algebraic"
transformation "eliminate_literal"
transformation "eliminate_epsilon"
transformation "simplify_formula"
(* 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. Note: does
nothing if meta get_counterexmp is not set *)
transformation "prepare_for_counterexmp"
transformation "introduce_premises"
transformation "instantiate_predicate"
transformation "abstract_quantifiers"
transformation "discriminate"
transformation "encoding_smt"
transformation "abstract_quantifiers"
(** Extra theories supported by COLIBRI *)
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 int.ComputerDivision
syntax function div "(colibri_cdiv %1 %2)"
syntax function mod "(colibri_crem %1 %2)"
remove prop Mod_bound
remove prop Div_mod
remove prop Mod_1
remove prop Div_1
end
theory real.Truncate
syntax function floor "(to_int %1)"
syntax function truncate "(to_int (colibri_truncate %1))"
syntax function ceil "(to_int (colibri_ceil %1))"
remove prop Floor_down
remove prop Floor_monotonic
end
theory real.FromInt
syntax function from_int "(to_real %1)"
end
theory real.Abs
syntax function abs "(colibri_abs_real %1)"
end
theory int.Abs
syntax function abs "(colibri_abs_int %1)"
end
theory real.PowerInt
syntax function power "(colibri_pow_real_int %1 %2)"
end
theory int.Power
syntax function power "(colibri_pow_int_int %1 %2)"
end
theory real.ExpLog
syntax function exp "(colibri_exp %1)"
(* syntax function log "(colibri_ln %1)" *)
end
theory real.MinMax
syntax function min "(colibri_min %1)"
syntax function max "(colibri_max %1)"
end
theory int.MinMax
syntax function min "(colibri_min %1)"
syntax function max "(colibri_max %1)"
end
(** TODO *)
(**
- colibri_floor
- colibri_abs_int
- colibri_abs_real
- colibri_truncate
- colibri_pow_real_int
- colibri_max
- colibri_min
- is_int
- to_int
- to_real
*)
This diff is collapsed.
(********************************************************************)
(* *)
(* The Why3 Verification Platform / The Why3 Development Team *)
(* Copyright 2010-2019 -- Inria - CNRS - Paris-Sud University *)
(* *)
(* This software is distributed under the terms of the GNU Lesser *)
(* General Public License version 2.1, with the special exception *)
(* on linking described in file LICENSE. *)
(* *)
(********************************************************************)
(* This file is generated by Why3's Coq-realize driver *)
(* Beware! Only edit allowed sections below *)
Require Import BuiltIn.
Require BuiltIn.
Require int.Int.
Require int.Abs.
Require int.EuclideanDivision.
Require int.ComputerDivision.
Lemma on_pos_euclidean_is_div:
forall n d, (int.EuclideanDivision.div n (Zpos d)) = Zdiv n (Zpos d).
intros n d.
unfold EuclideanDivision.div.
assert (0 < Z.pos d)%Z by reflexivity.
destruct (Z.mod_pos_bound n (Zpos d) H).
case (Z_le_dec 0 (n mod (Zpos d))); intros H2.
* reflexivity.
* destruct (H2 H0).
Qed.
(* Why3 goal *)
Lemma cdiv_cases :
forall (n:Numbers.BinNums.Z) (d:Numbers.BinNums.Z),
((0%Z <= n)%Z -> (0%Z < d)%Z ->
((ZArith.BinInt.Z.quot n d) = (int.EuclideanDivision.div n d))) /\
((n <= 0%Z)%Z -> (0%Z < d)%Z ->
((ZArith.BinInt.Z.quot n d) = (-(int.EuclideanDivision.div (-n)%Z d))%Z)) /\
((0%Z <= n)%Z -> (d < 0%Z)%Z ->
((ZArith.BinInt.Z.quot n d) = (-(int.EuclideanDivision.div n (-d)%Z))%Z)) /\
((n <= 0%Z)%Z -> (d < 0%Z)%Z ->
((ZArith.BinInt.Z.quot n d) = (int.EuclideanDivision.div (-n)%Z (-d)%Z))).
intros n d.
destruct d as [|d|d]; destruct n as [|n|n]; intuition (try contradiction; try discriminate; auto).
+ assert (NZ_d:((Zpos d) <> 0)%Z) by discriminate.
rewrite (Z.quot_div (Z.pos n) (Z.pos d) NZ_d).
rewrite on_pos_euclidean_is_div.
rewrite Z.mul_1_l.
reflexivity.
+ assert (NZ_d:((Zpos d) <> 0)%Z) by discriminate.
rewrite (Z.quot_div (Z.neg n) (Z.pos d) NZ_d).
rewrite on_pos_euclidean_is_div.
reflexivity.
+ assert (NZ_d:((Z.neg d) <> 0)%Z) by discriminate.
rewrite (Z.quot_div (Z.pos n) (Z.neg d) NZ_d).
simpl.
rewrite on_pos_euclidean_is_div.
reflexivity.
+ assert (NZ_d:((Z.neg d) <> 0)%Z) by discriminate.
rewrite (Z.quot_div (Z.neg n) (Z.neg d) NZ_d).
simpl.
rewrite on_pos_euclidean_is_div.
destruct (Z.pos n / Z.pos d)%Z;reflexivity.
Qed.
(* Why3 goal *)
Lemma cmod_cases :
forall (n:Numbers.BinNums.Z) (d:Numbers.BinNums.Z),
((0%Z <= n)%Z -> (0%Z < d)%Z ->
((ZArith.BinInt.Z.rem n d) = (int.EuclideanDivision.mod1 n d))) /\
((n <= 0%Z)%Z -> (0%Z < d)%Z ->
((ZArith.BinInt.Z.rem n d) = (-(int.EuclideanDivision.mod1 (-n)%Z d))%Z)) /\
((0%Z <= n)%Z -> (d < 0%Z)%Z ->
((ZArith.BinInt.Z.rem n d) = (int.EuclideanDivision.mod1 n (-d)%Z))) /\
((n <= 0%Z)%Z -> (d < 0%Z)%Z ->
((ZArith.BinInt.Z.rem n d) =
(-(int.EuclideanDivision.mod1 (-n)%Z (-d)%Z))%Z)).
intros n d.
unfold int.EuclideanDivision.mod1.
assert (Z.rem n d = n - (d * (Z.quot n d)))%Z.
assert (H:= Z.quot_rem' n d).
omega.
rewrite H.
assert (H2:=cdiv_cases n d).
intuition.
+ rewrite H1.
reflexivity.
+ rewrite H4.
rewrite Z.mul_opp_r.
omega.
+ rewrite H1.
rewrite Z.mul_opp_r.
rewrite Z.mul_opp_l.
reflexivity.
+ rewrite H4.
rewrite Z.mul_opp_l.
omega.
Qed.
...@@ -135,6 +135,29 @@ version_old = "1.0" ...@@ -135,6 +135,29 @@ version_old = "1.0"
driver = "cvc4" driver = "cvc4"
command = "%e --lang=smt2 %f" command = "%e --lang=smt2 %f"
# COLIBRI with counterexamples
[ATP colibri-ce]
name = "COLIBRI"
alternative = "counterexamples"
exec = "colibri"
version_switch = "--version"
version_regexp = "\\([^ \n\r]+\\)"
version_ok = "2137"
driver = "colibri"
command = "%e --memlimit %m %f"
# COLIBRI
[ATP colibri]
name = "COLIBRI"
exec = "colibri"
version_switch = "--version"
version_regexp = "\\([^ \n\r]+\\)"
version_ok = "2137"
driver = "colibri"
command = "%e --memlimit %m %f"
# Psyche version 2.x # Psyche version 2.x
[ATP psyche] [ATP psyche]
name = "Psyche" name = "Psyche"
......
...@@ -34,5 +34,5 @@ let elim_less (d:decl) = ...@@ -34,5 +34,5 @@ let elim_less (d:decl) =
let () = let () =
Trans.register_transform "abstract_quantifiers" (Trans.decl elim_less None) Trans.register_transform "abstract_quantifiers" (Trans.decl elim_less None)
~desc:"Abstract@ quantifiers@ in@ the@ axioms@ of@ the@ context \ ~desc:"Weaken quantifiers@ by replacing them by true or false in@ the@ axioms@ of@ the@ context \
and@ the@ goals." and@ the@ goals."
theory ComputerOfEuclideanDivision theory ComputerOfEuclideanDivision
use int.Int use int.Int
use int.Abs
use int.EuclideanDivision as ED use int.EuclideanDivision as ED
use int.ComputerDivision as CD use int.ComputerDivision as CD
let lemma cdiv_cases_0 (n d:int)
requires { n >= 0 }
requires { d <> 0 }
ensures { CD.div n d = ED.div n d } =
assert { (ED.div n d) * d + (ED.mod n d) = n = (CD.div n d) * d + (CD.mod n d) };
assert { 0 <= (ED.mod n d) < abs d };
assert { 0 <= (CD.mod n d) < abs d };
assert { - abs d < (CD.mod n d - ED.mod n d) < abs d };
assert { (ED.div n d - CD.div n d) * d = (CD.mod n d - ED.mod n d) };
if (ED.div n d - CD.div n d) > 0 then begin
if d < 0 then absurd else absurd
end
else if (ED.div n d - CD.div n d) < 0 then begin
if d < 0 then absurd else absurd
end
else
()
let lemma cdiv_cases_1 (n d:int)
requires { n <= 0 }
requires { d <> 0 }
ensures { CD.div n d = - (ED.div (-n) d) } =
assert { -((ED.div (-n) d) * d + (ED.mod (-n) d)) = -(-n) = n = (CD.div n d) * d + (CD.mod n d) };
assert { 0 <= (ED.mod (-n) d) < abs d };
assert { 0 <= -(CD.mod n d) < abs d };
assert { - abs d < (CD.mod n d + ED.mod (-n) d) < abs d };
assert { (ED.div (-n) d + CD.div n d) * d + (CD.mod n d + ED.mod (-n) d) = 0 };
if (ED.div (-n) d + CD.div n d) > 0 then begin
if d < 0 then absurd else absurd
end
else if (ED.div (-n) d + CD.div n d) < 0 then begin
if d < 0 then absurd else absurd
end
else
()
lemma cdiv_cases : forall n d:int [CD.div n d]. lemma cdiv_cases : forall n d:int [CD.div n d].
((n >= 0) -> (d > 0) -> CD.div n d = ED.div n d) /\ ((n >= 0) -> (d <> 0) -> CD.div n d = ED.div n d) /\
((n <= 0) -> (d > 0) -> CD.div n d = -(ED.div (-n) d)) /\ ((n <= 0) -> (d <> 0) -> CD.div n d = -(ED.div (-n) d))
((n >= 0) -> (d < 0) -> CD.div n d = -(ED.div n (-d))) /\
((n <= 0) -> (d < 0) -> CD.div n d = ED.div (-n) (-d))
lemma cmod_cases : forall n d:int [CD.mod n d]. lemma cmod_cases : forall n d:int [CD.mod n d].
((n >= 0) -> (d > 0) -> CD.mod n d = ED.mod n d) /\ ((n >= 0) -> (d <> 0) -> CD.mod n d = ED.mod n d) /\
((n <= 0) -> (d > 0) -> CD.mod n d = -(ED.mod (-n) d)) /\ ((n <= 0) -> (d <> 0) -> CD.mod n d = -(ED.mod (-n) d))
((n >= 0) -> (d < 0) -> CD.mod n d = (ED.mod n (-d))) /\
((n <= 0) -> (d < 0) -> CD.mod n d = -(ED.mod (-n) (-d))) end
theory EuclideanOfComputerDivision
use int.Int
use int.Abs
use int.EuclideanDivision as ED
use int.ComputerDivision as CD
let lemma cdiv_cases_0 (n d:int)
requires { n >= 0 }
requires { d <> 0 }
ensures { CD.div n d = ED.div n d } =
assert { (ED.div n d) * d + (ED.mod n d) = n = (CD.div n d) * d + (CD.mod n d) };
assert { 0 <= (ED.mod n d) < abs d };
assert { 0 <= (CD.mod n d) < abs d };
assert { - abs d < (CD.mod n d - ED.mod n d) < abs d };
assert { (ED.div n d - CD.div n d) * d = (CD.mod n d - ED.mod n d) };
if (ED.div n d - CD.div n d) > 0 then begin
if d < 0 then absurd else absurd
end
else if (ED.div n d - CD.div n d) < 0 then begin
if d < 0 then absurd else absurd
end
else
()
let lemma cdiv_cases_1 (n d:int)
requires { n <= 0 }
requires { d > 0 }
ensures { CD.div n d - (if CD.mod n d = 0 then 0 else 1) = ED.div n d } =
assert { ED.div n d * d + (ED.mod n d) = n = (CD.div n d) * d + (CD.mod n d) };
if CD.mod n d = 0 then begin
()
end else begin
assert { ED.div n d * d + (ED.mod n d) = n = (CD.div n d - 1) * d + (CD.mod n d + d) };
assert { abs d = d };
assert { 0 <= ED.mod n d < d };
assert { 0 < -(CD.mod n d) < d };
assert { 0 < CD.mod n d + d < d };
assert { -d < - CD.mod n d - d + ED.mod n d < d };
assert { (ED.div n d - (CD.div n d - 1)) * d + (- CD.mod n d - d + ED.mod n d) = 0 };
if (ED.div n d - (CD.div n d - 1)) > 0 then begin
absurd
end
else if (ED.div n d - (CD.div n d - 1)) < 0 then begin
absurd
end
else
()
end
let lemma cdiv_cases_2 (n d:int)
requires { n <= 0 }
requires { d < 0 }
ensures { CD.div n d + (if CD.mod n d = 0 then 0 else 1) = ED.div n d } =
assert { ED.div n d * d + (ED.mod n d) = n = (CD.div n d) * d + (CD.mod n d) };
if CD.mod n d = 0 then begin
()
end else begin
assert { ED.div n d * d + (ED.mod n d) = n = (CD.div n d + 1) * d + (CD.mod n d - d) };
assert { abs d = -d };
assert { 0 <= ED.mod n d < -d };
assert { 0 < -(CD.mod n d) < -d };
assert { d < - CD.mod n d + d < 0 };
assert { d < - CD.mod n d + d + ED.mod n d < -d };
assert { (ED.div n d - (CD.div n d + 1)) * d + (- CD.mod n d + d + ED.mod n d) = 0 };
if (ED.div n d - (CD.div n d + 1)) > 0 then begin
absurd
end
else if (ED.div n d - (CD.div n d + 1)) < 0 then begin
absurd
end
else
()
end
lemma ediv_cases : forall n d:int [ED.div n d].
((n >= 0) -> (d <> 0) -> ED.div n d = CD.div n d) /\
((n <= 0) -> (d > 0) -> ED.div n d = CD.div n d - (if CD.mod n d = 0 then 0 else 1)) /\
((n <= 0) -> (d < 0) -> ED.div n d = CD.div n d + (if CD.mod n d = 0 then 0 else 1))
lemma emod_cases : forall n d:int [ED.mod n d].
((n >= 0) -> (d <> 0) -> ED.mod n d = CD.mod n d) /\
((n <= 0) -> (d > 0) -> ED.mod n d = CD.mod n d + (if CD.mod n d = 0 then 0 else d)) /\
((n <= 0) -> (d < 0) -> ED.mod n d = CD.mod n d - (if CD.mod n d = 0 then 0 else d))
end end