Une MAJ de sécurité est nécessaire sur notre version actuelle. Elle sera effectuée lundi 02/08 entre 12h30 et 13h. L'interruption de service devrait durer quelques minutes (probablement moins de 5 minutes).

Commit 091f023c authored by Raphael Rieu-Helft's avatar Raphael Rieu-Helft
Browse files

Reification and side condition generation improvements

parent b5d67fb3
...@@ -53,7 +53,6 @@ end ...@@ -53,7 +53,6 @@ end
module LinearEquationsDecision module LinearEquationsDecision
use import int.Int use import int.Int
type coeff type coeff
clone LinearEquationsCoeffs as C with type t = coeff clone LinearEquationsCoeffs as C with type t = coeff
...@@ -296,6 +295,8 @@ let rec norm_eq_aux (ex acc_e:expr) (acc_c:coeff) : (expr, coeff) ...@@ -296,6 +295,8 @@ let rec norm_eq_aux (ex acc_e:expr) (acc_c:coeff) : (expr, coeff)
norm_eq_aux e2 ae ac norm_eq_aux e2 ae ac
end end
use import debug.Debug
let norm_eq (e:equality) : (expr, coeff) let norm_eq (e:equality) : (expr, coeff)
returns { (ex, c) -> forall y z. returns { (ex, c) -> forall y z.
interp_eq e y z <-> interp_eq (ex, Cst c) y z } interp_eq e y z <-> interp_eq (ex, Cst c) y z }
...@@ -474,8 +475,6 @@ let sub_expr (e1 e2:expr) ...@@ -474,8 +475,6 @@ let sub_expr (e1 e2:expr)
= C.(+) (C.(+) v1 (C.(-_) v2)) v2 = v1 }; = C.(+) (C.(+) v1 (C.(-_) v2)) v2 = v1 };
r r
use import debug.Debug
let rec same_eq (eq1 eq2: equality) : bool let rec same_eq (eq1 eq2: equality) : bool
ensures { result -> forall y z. interp_eq eq1 y z -> interp_eq eq2 y z } ensures { result -> forall y z. interp_eq eq1 y z -> interp_eq eq2 y z }
raises { C.Unknown -> true } raises { C.Unknown -> true }
...@@ -660,15 +659,17 @@ let linear_decision (l: context) (g: equality) : bool ...@@ -660,15 +659,17 @@ let linear_decision (l: context) (g: equality) : bool
variant { length l - i } variant { length l - i }
requires { length l - i = length ctx } requires { length l - i = length ctx }
requires { 0 <= i <= length l } requires { 0 <= i <= length l }
raises { C.Unknown -> true }
raises { Absurd -> true } raises { Absurd -> true }
= match ctx with = match ctx with
| Nil -> () | Nil -> ()
| Cons e t -> | Cons e t ->
assert { i < length l }; assert { i < length l };
let ex, c = norm_eq e in try
if (not (C.eq c C.czero)) then b[i] <- C.add b[i] c; let ex, c = norm_eq e in
fill_expr ex i; if (not (C.eq c C.czero)) then b[i] <- C.add b[i] c;
fill_expr ex i;
with C.Unknown -> () (* some equalities are in the context but cannot be normalized, typically they are useless, ignore them *)
end;
fill_ctx t (i+1) fill_ctx t (i+1)
end in end in
let rec fill_goal (ex:expr) : unit let rec fill_goal (ex:expr) : unit
...@@ -808,7 +809,7 @@ use import int.Abs ...@@ -808,7 +809,7 @@ use import int.Abs
type t = (int, int) type t = (int, int)
type rvars = int -> real type rvars = int -> real
exception Unknown exception QError
let constant rzero = (0,1) let constant rzero = (0,1)
let constant rone = (1,1) let constant rone = (1,1)
...@@ -889,10 +890,10 @@ let simp (t:t) : t ...@@ -889,10 +890,10 @@ let simp (t:t) : t
let radd (a b:t) let radd (a b:t)
ensures { forall y. rinterp result y = rinterp a y +. rinterp b y } ensures { forall y. rinterp result y = rinterp a y +. rinterp b y }
raises { Unknown -> true } raises { QError -> true }
= match (a,b) with = match (a,b) with
| (n1,d1), (n2,d2) -> | (n1,d1), (n2,d2) ->
if d1 = 0 || d2 = 0 then raise Unknown if d1 = 0 || d2 = 0 then raise QError
else begin else begin
let r = (n1*d2 + n2*d1, d1*d2) in let r = (n1*d2 + n2*d1, d1*d2) in
let ghost d = from_int d1 *. from_int d2 in let ghost d = from_int d1 *. from_int d2 in
...@@ -908,10 +909,10 @@ let radd (a b:t) ...@@ -908,10 +909,10 @@ let radd (a b:t)
let rmul (a b:t) let rmul (a b:t)
ensures { forall y. rinterp result y = rinterp a y *. rinterp b y } ensures { forall y. rinterp result y = rinterp a y *. rinterp b y }
raises { Unknown -> true } raises { QError -> true }
= match (a,b) with = match (a,b) with
| (n1,d1), (n2, d2) -> | (n1,d1), (n2, d2) ->
if d1 = 0 || d2 = 0 then raise Unknown if d1 = 0 || d2 = 0 then raise QError
else begin else begin
let r = (n1*n2, d1*d2) in let r = (n1*n2, d1*d2) in
assert { forall y. rinterp r y = rinterp a y *. rinterp b y assert { forall y. rinterp r y = rinterp a y *. rinterp b y
...@@ -939,9 +940,9 @@ let rinv (a:t) ...@@ -939,9 +940,9 @@ let rinv (a:t)
requires { not req a rzero } requires { not req a rzero }
ensures { not req result rzero } ensures { not req result rzero }
ensures { forall y. rinterp result y *. rinterp a y = 1.0 } ensures { forall y. rinterp result y *. rinterp a y = 1.0 }
raises { Unknown -> true } raises { QError -> true }
= match a with = match a with
| (n,d) -> if n = 0 || d = 0 then raise Unknown else (d,n) | (n,d) -> if n = 0 || d = 0 then raise QError else (d,n)
end end
end end
...@@ -952,7 +953,7 @@ use import RationalCoeffs ...@@ -952,7 +953,7 @@ use import RationalCoeffs
use import real.RealInfix use import real.RealInfix
use import real.FromInt use import real.FromInt
clone export LinearEquationsDecision with type C.a = real, function C.(+) = (+.), function C.( * ) = ( *. ), function C.(-_) = (-._), function C.(-) = (-.), type coeff = t, type C.cvars=int -> real, function C.interp=rinterp, exception C.Unknown = Unknown, constant C.azero = Real.zero, constant C.aone = Real.one, predicate C.ale = (<=.), val C.czero=rzero, val C.cone=rone, lemma C.sub_def, lemma C.zero_def, lemma C.one_def, val C.add=radd, val C.mul=rmul, val C.opp=ropp, val C.eq=req, val C.inv=rinv, goal C.A.ZeroLessOne, goal C.A.CompatOrderAdd, goal C.A.CompatOrderMult, goal C.A.Unitary, goal C.A.NonTrivialRing, goal C.A.Mul_distr_l, goal C.A.Mul_distr_r, goal C.A.Inv_def_l, goal C.A.Inv_def_r, goal C.A.MulAssoc.Assoc, goal C.A.Assoc, goal C.A.MulComm.Comm, goal C.A.Comm, goal C.A.Unit_def_l, goal C.A.Unit_def_r clone export LinearEquationsDecision with type C.a = real, function C.(+) = (+.), function C.( * ) = ( *. ), function C.(-_) = (-._), function C.(-) = (-.), type coeff = t, type C.cvars=int -> real, function C.interp=rinterp, exception C.Unknown = QError, constant C.azero = Real.zero, constant C.aone = Real.one, predicate C.ale = (<=.), val C.czero=rzero, val C.cone=rone, lemma C.sub_def, lemma C.zero_def, lemma C.one_def, val C.add=radd, val C.mul=rmul, val C.opp=ropp, val C.eq=req, val C.inv=rinv, goal C.A.ZeroLessOne, goal C.A.CompatOrderAdd, goal C.A.CompatOrderMult, goal C.A.Unitary, goal C.A.NonTrivialRing, goal C.A.Mul_distr_l, goal C.A.Mul_distr_r, goal C.A.Inv_def_l, goal C.A.Inv_def_r, goal C.A.MulAssoc.Assoc, goal C.A.Assoc, goal C.A.MulComm.Comm, goal C.A.Comm, goal C.A.Unit_def_l, goal C.A.Unit_def_r
end end
...@@ -963,21 +964,21 @@ use import int.Int ...@@ -963,21 +964,21 @@ use import int.Int
function id (t:int) (v:int -> int) : int = t function id (t:int) (v:int -> int) : int = t
let predicate eq (a b:int) = a=b let predicate eq (a b:int) = a=b
exception Unknown exception NError
let inv (t:int) : int let inv (t:int) : int
(*ensures { forall v: int -> int. id result v * id t v = one }*) (*ensures { forall v: int -> int. id result v * id t v = one }*)
ensures { not (eq result zero) } ensures { not (eq result zero) }
raises { Unknown -> true } raises { NError -> true }
= raise Unknown = raise NError
clone export LinearEquationsDecision with type C.a = int, function C.(+)=(+), function C.(*) = (*), function C.(-_) = (-_), function C.(-) = (-), type coeff = int, type C.cvars = int->int,function C.interp = id, constant C.azero = zero, constant C.aone = one, predicate C.ale= (<=), val C.czero = zero, val C.cone = one, lemma C.sub_def, lemma C.zero_def, lemma C.one_def, val C.add = (+), val C.mul = (*), val C.opp = (-_), val C.eq = eq, val C.inv = inv, goal C.A.ZeroLessOne, goal C.A.CompatOrderAdd, goal C.A.CompatOrderMult, goal C.A.Unitary, goal C.A.NonTrivialRing, goal C.A.Mul_distr_l, goal C.A.Mul_distr_r, goal C.A.Inv_def_l, goal C.A.Inv_def_r, goal C.A.MulAssoc.Assoc, goal C.A.Assoc, goal C.A.MulComm.Comm, goal C.A.Comm, goal C.A.Unit_def_l, goal C.A.Unit_def_r clone export LinearEquationsDecision with type C.a = int, function C.(+)=(+), function C.(*) = (*), function C.(-_) = (-_), function C.(-) = (-), type coeff = int, type C.cvars = int->int,function C.interp = id, constant C.azero = zero, constant C.aone = one, predicate C.ale= (<=), val C.czero = zero, val C.cone = one, lemma C.sub_def, lemma C.zero_def, lemma C.one_def, val C.add = (+), val C.mul = (*), val C.opp = (-_), val C.eq = eq, val C.inv = inv, goal C.A.ZeroLessOne, goal C.A.CompatOrderAdd, goal C.A.CompatOrderMult, goal C.A.Unitary, goal C.A.NonTrivialRing, goal C.A.Mul_distr_l, goal C.A.Mul_distr_r, goal C.A.Inv_def_l, goal C.A.Inv_def_r, goal C.A.MulAssoc.Assoc, goal C.A.Assoc, goal C.A.MulComm.Comm, goal C.A.Comm, goal C.A.Unit_def_l, goal C.A.Unit_def_r
use import real.FromInt use import real.FromInt
use import RationalCoeffs use import RationalCoeffs
use LinearDecisionRational as R use LinearDecisionRational as R
use import list.List use import list.List
let function m (x:int) : (int, int) let function m (x:int) : (int, int)
ensures { forall z. rinterp result z = from_int x } ensures { forall z. rinterp result z = from_int x }
= (x,1) = (x,1)
...@@ -1029,7 +1030,7 @@ let int_decision (l: context') (g: equality') : bool ...@@ -1029,7 +1030,7 @@ let int_decision (l: context') (g: equality') : bool
requires { valid_ctx' l } requires { valid_ctx' l }
requires { valid_eq' g } requires { valid_eq' g }
ensures { forall y z. result -> interp_ctx' l g y z } ensures { forall y z. result -> interp_ctx' l g y z }
raises { R.Absurd -> true | (* R.NonLinear -> true | *) Unknown -> true } raises { R.Absurd -> true | QError -> true }
= R.decision (m_ctx l) (m_eq g) = R.decision (m_ctx l) (m_eq g)
end end
...@@ -1043,6 +1044,7 @@ use import int.Int ...@@ -1043,6 +1044,7 @@ use import int.Int
use import real.RealInfix use import real.RealInfix
use import real.FromInt use import real.FromInt
meta "compute_max_steps" 0x10000
meta coercion function from_int meta coercion function from_int
goal g: forall x y: real. goal g: forall x y: real.
...@@ -1056,6 +1058,8 @@ module TestInt ...@@ -1056,6 +1058,8 @@ module TestInt
use import LinearDecisionInt use import LinearDecisionInt
use import int.Int use import int.Int
meta "compute_max_steps" 0x10000
goal g: forall x y:int. goal g: forall x y:int.
3 * x + 2 * y = 21 -> 3 * x + 2 * y = 21 ->
7 * x + 4 * y = 47 -> 7 * x + 4 * y = 47 ->
...@@ -1111,7 +1115,7 @@ function minterp (t:t) (y:evars) : real ...@@ -1111,7 +1115,7 @@ function minterp (t:t) (y:evars) : real
qinterp q *. pow rradix (from_int (interp_exp e y)) qinterp q *. pow rradix (from_int (interp_exp e y))
end end
exception Unknown exception MPError
let rec opp_exp (e:exp) let rec opp_exp (e:exp)
ensures { forall y. interp_exp result y = - interp_exp e y } ensures { forall y. interp_exp result y = - interp_exp e y }
...@@ -1129,19 +1133,19 @@ let rec add_sub_exp (e1 e2:exp) (s:bool) : exp ...@@ -1129,19 +1133,19 @@ let rec add_sub_exp (e1 e2:exp) (s:bool) : exp
if s if s
then interp_exp result y = interp_exp e1 y + interp_exp e2 y then interp_exp result y = interp_exp e1 y + interp_exp e2 y
else interp_exp result y = interp_exp e1 y - interp_exp e2 y } else interp_exp result y = interp_exp e1 y - interp_exp e2 y }
raises { Unknown -> true } raises { MPError -> true }
variant { e2, e1 } variant { e2, e1 }
= =
let rec add_atom (e a:exp) (s:bool) : (exp, bool) let rec add_atom (e a:exp) (s:bool) : (exp, bool)
returns { r, _ -> forall y. returns { r, _ -> forall y.
if s then interp_exp r y = interp_exp e y + interp_exp a y if s then interp_exp r y = interp_exp e y + interp_exp a y
else interp_exp r y = interp_exp e y - interp_exp a y } else interp_exp r y = interp_exp e y - interp_exp a y }
raises { Unknown -> true } raises { MPError -> true }
variant { e } variant { e }
= match (e,a) with = match (e,a) with
| Lit n1, Lit n2 -> (if s then Lit (n1+n2) else Lit (n1-n2)), true | Lit n1, Lit n2 -> (if s then Lit (n1+n2) else Lit (n1-n2)), True
| Lit n, Var i | Lit n, Var i
-> if n = 0 then (if s then Var i else Minus (Var i)), true -> if n = 0 then (if s then Var i else Minus (Var i)), True
else (if s then Plus e a else Sub e a), False else (if s then Plus e a else Sub e a), False
| Var i, Lit n | Var i, Lit n
-> if n = 0 then Var i, true -> if n = 0 then Var i, true
...@@ -1159,6 +1163,9 @@ let rec add_sub_exp (e1 e2:exp) (s:bool) : exp ...@@ -1159,6 +1163,9 @@ let rec add_sub_exp (e1 e2:exp) (s:bool) : exp
else else
if i = j then Lit 0, True if i = j then Lit 0, True
else Sub e a, False else Sub e a, False
| Minus (Var i), Minus (Var j) ->
if (not s) && (i=j) then Lit 0, true
else (if s then Plus e a else Sub e a), False
| Minus _, Minus _ -> (if s then Plus e a else Sub e a), False | Minus _, Minus _ -> (if s then Plus e a else Sub e a), False
| Plus e1 e2, _ -> | Plus e1 e2, _ ->
let r, b = add_atom e1 a s in let r, b = add_atom e1 a s in
...@@ -1179,7 +1186,7 @@ let rec add_sub_exp (e1 e2:exp) (s:bool) : exp ...@@ -1179,7 +1186,7 @@ let rec add_sub_exp (e1 e2:exp) (s:bool) : exp
if b then Sub e1 r, True if b then Sub e1 r, True
else if s then Sub (Plus e1 a) e2, False else if s then Sub (Plus e1 a) e2, False
else Sub e1 (Plus e2 a), False else Sub e1 (Plus e2 a), False
| _ -> raise Unknown | _ -> raise MPError
end end
in in
match e2 with match e2 with
...@@ -1204,14 +1211,14 @@ let rec add_sub_exp (e1 e2:exp) (s:bool) : exp ...@@ -1204,14 +1211,14 @@ let rec add_sub_exp (e1 e2:exp) (s:bool) : exp
let add_exp (e1 e2:exp) : exp let add_exp (e1 e2:exp) : exp
ensures { forall y. interp_exp result y = interp_exp e1 y + interp_exp e2 y } ensures { forall y. interp_exp result y = interp_exp e1 y + interp_exp e2 y }
raises { Unknown -> True } raises { MPError -> True }
= add_sub_exp e1 e2 True = add_sub_exp e1 e2 True
let rec zero_exp (e:exp) : bool let rec zero_exp (e:exp) : bool
ensures { result -> forall y. interp_exp e y = 0 } ensures { result -> forall y. interp_exp e y = 0 }
variant { e } variant { e }
raises { Unknown -> true } raises { MPError -> true }
= =
let rec all_zero (e:exp) : bool let rec all_zero (e:exp) : bool
ensures { result -> forall y. interp_exp e y = 0 } ensures { result -> forall y. interp_exp e y = 0 }
...@@ -1230,7 +1237,7 @@ let rec zero_exp (e:exp) : bool ...@@ -1230,7 +1237,7 @@ let rec zero_exp (e:exp) : bool
let rec same_exp (e1 e2: exp) let rec same_exp (e1 e2: exp)
ensures { result -> forall y. interp_exp e1 y = interp_exp e2 y } ensures { result -> forall y. interp_exp e1 y = interp_exp e2 y }
variant { e1, e2 } variant { e1, e2 }
raises { Unknown -> true } raises { MPError -> true }
= match e1, e2 with = match e1, e2 with
| Lit n1, Lit n2 -> n1 = n2 | Lit n1, Lit n2 -> n1 = n2
| Var v1, Var v2 -> v1 = v2 | Var v1, Var v2 -> v1 = v2
...@@ -1240,8 +1247,8 @@ let rec same_exp (e1 e2: exp) ...@@ -1240,8 +1247,8 @@ let rec same_exp (e1 e2: exp)
let madd (a b:t) let madd (a b:t)
ensures { forall y. minterp result y = minterp a y +. minterp b y } ensures { forall y. minterp result y = minterp a y +. minterp b y }
raises { Unknown -> true } raises { MPError -> true }
raises { Q.Unknown -> true } raises { Q.QError -> true }
= match a, b with = match a, b with
| (q1, e1), (q2, e2) -> | (q1, e1), (q2, e2) ->
if Q.req q1 Q.rzero then b if Q.req q1 Q.rzero then b
...@@ -1256,13 +1263,13 @@ let madd (a b:t) ...@@ -1256,13 +1263,13 @@ let madd (a b:t)
= qinterp q1 *. p +. qinterp q2 *. p = qinterp q1 *. p +. qinterp q2 *. p
= minterp a y +. minterp b y }; = minterp a y +. minterp b y };
(q,e1) end (q,e1) end
else (print a; print b; raise Unknown) else raise MPError
end end
let mmul (a b:t) let mmul (a b:t)
ensures { forall y. minterp result y = minterp a y *. minterp b y } ensures { forall y. minterp result y = minterp a y *. minterp b y }
raises { Q.Unknown -> true } raises { Q.QError -> true }
raises { Unknown -> true } raises { MPError -> true }
= match a, b with = match a, b with
| (q1,e1), (q2,e2) -> | (q1,e1), (q2,e2) ->
let q = Q.rmul q1 q2 in let q = Q.rmul q1 q2 in
...@@ -1310,7 +1317,7 @@ let minv (a:t) ...@@ -1310,7 +1317,7 @@ let minv (a:t)
requires { not meq a mzero } requires { not meq a mzero }
ensures { not meq result mzero } ensures { not meq result mzero }
(* ensures { forall y. minterp result y *. minterp a y = 1.0 } no need to prove this*) (* ensures { forall y. minterp result y *. minterp a y = 1.0 } no need to prove this*)
raises { Q.Unknown -> true } raises { Q.QError -> true }
= match a with = match a with
| (q,e) -> (Q.rinv q, opp_exp e) | (q,e) -> (Q.rinv q, opp_exp e)
end end
...@@ -1324,7 +1331,7 @@ use import real.RealInfix ...@@ -1324,7 +1331,7 @@ use import real.RealInfix
type coeff = t type coeff = t
clone export LinearEquationsDecision with type C.a = real, function C.(+) = (+.), function C.( *) = ( *.), function C.(-_) = (-._), function C.(-) = (-.), type coeff = t, type C.cvars=evars, function C.interp=minterp, exception C.Unknown = Q.Unknown, constant C.azero = Real.zero, constant C.aone = Real.one, predicate C.ale = (<=.), val C.czero=mzero, val C.cone=mone, lemma C.sub_def, lemma C.zero_def, lemma C.one_def, val C.add=madd, val C.mul=mmul, val C.opp=mopp, val C.eq=meq, val C.inv=minv, goal C.A.ZeroLessOne, goal C.A.CompatOrderAdd, goal C.A.CompatOrderMult, goal C.A.Unitary, goal C.A.NonTrivialRing, goal C.A.Mul_distr_l, goal C.A.Mul_distr_r, goal C.A.Inv_def_l, goal C.A.Inv_def_r, goal C.A.MulAssoc.Assoc, goal C.A.Assoc, goal C.A.MulComm.Comm, goal C.A.Comm, goal C.A.Unit_def_l, goal C.A.Unit_def_r clone export LinearEquationsDecision with type C.a = real, function C.(+) = (+.), function C.( *) = ( *.), function C.(-_) = (-._), function C.(-) = (-.), type coeff = t, type C.cvars=evars, function C.interp=minterp, exception C.Unknown = MPError, constant C.azero = Real.zero, constant C.aone = Real.one, predicate C.ale = (<=.), val C.czero=mzero, val C.cone=mone, lemma C.sub_def, lemma C.zero_def, lemma C.one_def, val C.add=madd, val C.mul=mmul, val C.opp=mopp, val C.eq=meq, val C.inv=minv, goal C.A.ZeroLessOne, goal C.A.CompatOrderAdd, goal C.A.CompatOrderMult, goal C.A.Unitary, goal C.A.NonTrivialRing, goal C.A.Mul_distr_l, goal C.A.Mul_distr_r, goal C.A.Inv_def_l, goal C.A.Inv_def_r, goal C.A.MulAssoc.Assoc, goal C.A.Assoc, goal C.A.MulComm.Comm, goal C.A.Comm, goal C.A.Unit_def_l, goal C.A.Unit_def_r
end end
module LinearDecisionIntMP module LinearDecisionIntMP
...@@ -1349,18 +1356,18 @@ function mpinterp (t:t) (y:evars) : int ...@@ -1349,18 +1356,18 @@ function mpinterp (t:t) (y:evars) : int
let mpadd (a b:t) : t let mpadd (a b:t) : t
ensures { forall y. mpinterp result y = mpinterp a y + mpinterp b y } ensures { forall y. mpinterp result y = mpinterp a y + mpinterp b y }
raises { Unknown -> true } raises { MPError -> true }
= raise Unknown = raise MPError
let mpmul (a b:t) : t let mpmul (a b:t) : t
ensures { forall y. mpinterp result y = mpinterp a y * mpinterp b y } ensures { forall y. mpinterp result y = mpinterp a y * mpinterp b y }
raises { Unknown -> true } raises { MPError -> true }
= raise Unknown = raise MPError
let mpopp (a:t) : t let mpopp (a:t) : t
ensures { forall y. mpinterp result y = - mpinterp a y } ensures { forall y. mpinterp result y = - mpinterp a y }
raises { Unknown -> true } raises { MPError -> true }
= raise Unknown = raise MPError
let predicate mpeq (a b:t) let predicate mpeq (a b:t)
ensures { result -> forall y. mpinterp a y = mpinterp b y } ensures { result -> forall y. mpinterp a y = mpinterp b y }
...@@ -1370,8 +1377,8 @@ let predicate mpeq (a b:t) ...@@ -1370,8 +1377,8 @@ let predicate mpeq (a b:t)
let mpinv (a:t) : t let mpinv (a:t) : t
ensures { not mpeq result mpzero } ensures { not mpeq result mpzero }
raises { Unknown -> true } raises { MPError -> true }
= raise Unknown = raise MPError
clone export LinearEquationsDecision with type C.a = int, function C.(+) = (+), function C.(*) = (*), function C.(-_) = (-_), function C.(-) = (-), type coeff = t, type C.cvars = int->int, function C.interp = mpinterp, constant C.azero = zero, constant C.aone = one, val C.czero = mpzero, val C.cone = mpone, predicate C.ale = (<=), lemma C.sub_def, lemma C.zero_def, lemma C.one_def, val C.add = mpadd, val C.mul = mpmul, val C.opp = mpopp, val C.eq = mpeq, val C.inv = mpinv, goal C.A.ZeroLessOne, goal C.A.CompatOrderAdd, goal C.A.CompatOrderMult, goal C.A.Unitary, goal C.A.NonTrivialRing, goal C.A.Mul_distr_l, goal C.A.Mul_distr_r, goal C.A.Inv_def_l, goal C.A.Inv_def_r, goal C.A.MulAssoc.Assoc, goal C.A.Assoc, goal C.A.MulComm.Comm, goal C.A.Comm, goal C.A.Unit_def_l, goal C.A.Unit_def_r clone export LinearEquationsDecision with type C.a = int, function C.(+) = (+), function C.(*) = (*), function C.(-_) = (-_), function C.(-) = (-), type coeff = t, type C.cvars = int->int, function C.interp = mpinterp, constant C.azero = zero, constant C.aone = one, val C.czero = mpzero, val C.cone = mpone, predicate C.ale = (<=), lemma C.sub_def, lemma C.zero_def, lemma C.one_def, val C.add = mpadd, val C.mul = mpmul, val C.opp = mpopp, val C.eq = mpeq, val C.inv = mpinv, goal C.A.ZeroLessOne, goal C.A.CompatOrderAdd, goal C.A.CompatOrderMult, goal C.A.Unitary, goal C.A.NonTrivialRing, goal C.A.Mul_distr_l, goal C.A.Mul_distr_r, goal C.A.Inv_def_l, goal C.A.Inv_def_r, goal C.A.MulAssoc.Assoc, goal C.A.Assoc, goal C.A.MulComm.Comm, goal C.A.Comm, goal C.A.Unit_def_l, goal C.A.Unit_def_r
...@@ -1469,7 +1476,7 @@ let mp_decision (l: context') (g: equality') : bool ...@@ -1469,7 +1476,7 @@ let mp_decision (l: context') (g: equality') : bool
requires { valid_eq' g } requires { valid_eq' g }
ensures { forall y z. result -> pos_ctx' l z -> pos_eq' g z ensures { forall y z. result -> pos_ctx' l z -> pos_eq' g z
-> interp_ctx' l g y z } -> interp_ctx' l g y z }
raises { R.Absurd -> true | Unknown -> true | Q.Unknown -> true } raises { R.Absurd -> true | MPError -> true | Q.QError -> true }
= =
R.decision (m_ctx l) (m_eq g) R.decision (m_ctx l) (m_eq g)
...@@ -1868,8 +1875,6 @@ let prop_ctx (l:context') (g:equality') : (context', equality') ...@@ -1868,8 +1875,6 @@ let prop_ctx (l:context') (g:equality') : (context', equality')
Cons h' t' Cons h' t'
end end
in in
(*propagate (propagate (propagate l)),
propagate_eq (propagate_eq (propagate_eq g))*)
propagate l, propagate_eq g propagate l, propagate_eq g
use LinearDecisionRationalMP as R use LinearDecisionRationalMP as R
...@@ -1879,8 +1884,8 @@ let prop_ctx (l:context') (g:equality') : (context', equality') ...@@ -1879,8 +1884,8 @@ let prop_ctx (l:context') (g:equality') : (context', equality')
requires { valid_eq' g } requires { valid_eq' g }
ensures { forall y z. result -> pos_ctx' l z -> pos_eq' g z ensures { forall y z. result -> pos_ctx' l z -> pos_eq' g z
-> y = z -> interp_ctx' l g y z } -> y = z -> interp_ctx' l g y z }
raises { | OutOfBounds -> true | E.Unknown -> true raises { | OutOfBounds -> true | E.MPError -> true
| E.Q.Unknown -> true | R.Absurd -> true} | E.Q.QError -> true | R.Absurd -> true}
= let l', g' = prop_ctx l g in = let l', g' = prop_ctx l g in
mp_decision l' g' mp_decision l' g'
...@@ -1893,6 +1898,8 @@ use import mach.int.UInt64 ...@@ -1893,6 +1898,8 @@ use import mach.int.UInt64
use import int.Int use import int.Int
use import int.Power use import int.Power
meta "compute_max_steps" 0x10000
goal g: forall i x c r: int. goal g: forall i x c r: int.
0 <= i -> 0 <= i ->
x + (2 * (power radix i) * c) = r -> x + (2 * (power radix i) * c) = r ->
...@@ -1922,6 +1929,8 @@ module Test2 ...@@ -1922,6 +1929,8 @@ module Test2
use import int.Int use import int.Int
use import LinearDecisionInt use import LinearDecisionInt
meta "compute_max_steps" 0x10000
goal g: forall x y z: int. goal g: forall x y z: int.
x + y = 0 -> x + y = 0 ->
y - z = 0 -> y - z = 0 ->
...@@ -1966,6 +1975,8 @@ module TestFmla ...@@ -1966,6 +1975,8 @@ module TestFmla
use import Fmla use import Fmla
meta "compute_max_steps" 0x10000
goal g: goal g:
forall a: value. forall a: value.
((forall x. forall y. foo (add x (add (add a dummy) y))) = True) ((forall x. forall y. foo (add x (add (add a dummy) y))) = True)
......
...@@ -808,6 +808,66 @@ module N ...@@ -808,6 +808,66 @@ module N
end end
end end
(** [incr x y sz] adds to [x] the value of the limb [y] in place.
[x] has size [sz]. The addition must not overflow. This corresponds
to [mpn_incr] *)
let incr (x:t) (y:limb) (sz:int32) : unit
requires { valid x sz }
requires { sz > 0 }
requires { value x sz + y < power radix sz }
ensures { value x sz = value (old x) sz + y }
ensures { forall j. j < x.offset \/ x.offset + sz <= j ->
(pelts x)[j] = (pelts (old x))[j] }
writes { x.data.elts }
=
let ghost ox = { x } in
let c = ref y in
let lx : ref limb = ref 0 in
let i : ref int32 = ref 0 in
while not (Limb.(=) !c 0) do
invariant { 0 <= !i <= sz }
invariant { !i = sz -> !c = 0 }
invariant { !i > 0 -> 0 <= !c <= 1 }
invariant { value x !i + (power radix !i) * !c
= value ox !i + y }
invariant { forall j. !i <= j < sz ->
(pelts x)[x.offset + j] = (pelts ox)[x.offset + j] }
invariant { forall j. j < x.offset \/ x.offset + sz <= j ->
(pelts x)[j] = (pelts ox)[j] }
variant { sz - !i }
label StartLoop in
lx := get_ofs x !i;
assert { !lx = (pelts ox)[ox.offset + !i] };
let (res, carry) = add_with_carry !lx !c 0 in (*TODO*)
assert { res + radix * carry = !lx + !c }; (* TODO remove this *)
value_sub_update_no_change (pelts x) (x.offset + p2i !i)
(x.offset + p2i !i + 1)
(x.offset + p2i sz) res;
set_ofs x !i res;
assert { forall j. !i < j < sz ->
(pelts x)[x.offset + j]
= (pelts ox)[x.offset + j] };
assert { value x !i + (power radix !i) * !c = value ox !i + y };
c := carry;
value_tail x !i;
value_tail ox !i;
assert { value x (!i+1) + power radix (!i+1) * !c =
value ox (!i+1) + y };
i := Int32.(+) !i 1;
assert { !i = sz -> !c = 0
by value x sz + power radix sz * !c = value ox sz + y
so value ox sz + y < power radix sz
so 0 <= !c <= 1};
done;
value_concat x !i sz;
value_concat ox !i sz;
assert { forall j. x.offset + !i <= j < x.offset + sz ->
(pelts x)[j] = (pelts ox)[j]
by let k = j - x.offset in
!i <= k < sz
so (pelts x)[x.offset + k] = (pelts ox)[x.offset + k]};
value_sub_frame (pelts x) (pelts ox) (x.offset + p2i !i) (x.offset + p2i sz)
(** [sub_limb r x y sz] substracts [y] from [(x, sz)] and writes (** [sub_limb r x y sz] substracts [y] from [(x, sz)] and writes
the result to [(r, sz)]. Returns borrow, either 0 or the result to [(r, sz)]. Returns borrow, either 0 or
...@@ -1745,14 +1805,14 @@ module N ...@@ -1745,14 +1805,14 @@ module N
(** [mul r x y sx sy] multiplies [(x, sx)] and [(y,sy)] and writes (** [mul r x y sx sy] multiplies [(x, sx)] and [(y,sy)] and writes
the result in [(r, sx+sy)]. [sx] must be greater than or equal to the result in [(r, sx+sy)]. [sx] must be greater than or equal to
[sy]. Corresponds to [mpn_mul]. *) [sy]. Corresponds to [mpn_mul]. *)
let mul (r x y:t) (sx sy:int32) : limb let mul (r x y:t) (sx sy:int32) : unit
requires { 0 < sy <= sx } requires { 0 < sy <= sx }
requires { valid x sx } requires { valid x sx }
requires { valid y sy } requires { valid y sy }
requires { valid r (sy + sx) } requires { valid r (sy + sx) }
writes { r.data.elts } writes { r.data.elts }