Commit 2b2194c6 authored by POLLIEN Baptiste's avatar POLLIEN Baptiste
Browse files

All RTE are proved

parent 5e991b74
[ { "prover": "CVC4:1.9-prerelease:strings+counterexamples",
"verdict": "timeout", "time": 10. },
{ "prover": "Alt-Ergo:2.3.3", "verdict": "timeout", "time": 10. } ]
[ { "prover": "Alt-Ergo:2.3.3", "verdict": "valid", "time": 11.8615,
"steps": 7683 } ]
[ { "header": "Definition", "tactic": "Wp.unfold", "params": {},
"select": { "select": "clause-step", "at": 30, "kind": "have",
"target": "let a_0 = Mptr_2[(shift_PTR o_0 i_0)] in\n(P_rvalid_int_mat_3_ Malloc_2 Mptr_2\n (havoc Mint_undef_0 Mint_13 (shift_sint32 a_0 0) l_0)\n [(shift_sint32 a_0 j_0)->v_0] b_0 n_0 l_0\n (to_sint32\n (\\truncate (\\sqrt (real_of_int (to_sint32 (2147483647 div n_0)))))))",
"pattern": "P_rvalid_int_mat_3_$Malloc$Mptr[=]" },
"children": { "Unfold 'P_rvalid_int_mat_3_'": [ { "header": "Definition",
"tactic": "Wp.unfold",
"params": {},
"select": { "select": "clause-step",
"at": 31,
"kind": "have",
"target": "let a_1 = Mptr_2[(shift_PTR o_0 i_0)] in\n(P_rvalid_int_mat_3_ Malloc_2 Mptr_2\n (havoc Mint_undef_0 Mint_13 (shift_sint32 a_1 0) l_0)\n [(shift_sint32 a_1 j_0)->v_0] a_0 m_0 n_0\n (to_sint32\n (\\truncate (\\sqrt (real_of_int (to_sint32 (2147483647 div n_0)))))))",
"pattern": "P_rvalid_int_mat_3_$Malloc$Mptr[=]" },
"children": { "Unfold 'P_rvalid_int_mat_3_'":
[ { "prover": "CVC4:1.9-prerelease:strings+counterexamples",
"verdict": "valid",
"time": 1.04 } ] } } ] } } ]
[ { "header": "Definition", "tactic": "Wp.unfold", "params": {},
"select": { "select": "clause-step", "at": 31, "kind": "have",
"target": "let a_0 = Mptr_2[(shift_PTR o_3 i_0)] in\n(P_rvalid_int_mat_3_ Malloc_2 Mptr_2\n (havoc Mint_undef_0 Mint_13 (shift_sint32 a_0 0) l_0)\n [(shift_sint32 a_0 j_0)->v_0] b_0 n_0 l_0\n (to_sint32 (\\truncate (\\sqrt (real_of_int (2147483647 div n_0))))))",
"select": { "select": "clause-step", "at": 30, "kind": "have",
"target": "let a_0 = Mptr_2[(shift_PTR o_0 i_0)] in\n(P_rvalid_int_mat_3_ Malloc_2 Mptr_2\n (havoc Mint_undef_0 Mint_13 (shift_sint32 a_0 0) l_0)\n [(shift_sint32 a_0 j_0)->v_0] b_0 n_0 l_0\n (to_sint32\n (\\truncate (\\sqrt (real_of_int (to_sint32 (2147483647 div n_0)))))))",
"pattern": "P_rvalid_int_mat_3_$Malloc$Mptr[=]" },
"children": { "Unfold 'P_rvalid_int_mat_3_'": [ { "prover": "CVC4:1.9-prerelease:strings+counterexamples",
"verdict": "valid",
"time": 2.6 } ] } } ]
"time": 6.7 },
{ "header": "Definition",
"tactic": "Wp.unfold",
"params": {},
"select": { "select": "inside-step",
"at": 30,
"kind": "have",
"occur": 0,
"target": "(P_rvalid_int_mat_2_ Malloc_2 Mptr_2 a_0 m_0 n_0)",
"pattern": "P_rvalid_int_mat_2_$Malloc$Mptr$a" },
"children": { "Unfold 'P_rvalid_int_mat_2_'":
[ { "header": "Definition",
"tactic": "Wp.unfold",
"params": {},
"select":
{ "select": "clause-step",
"at": 29,
"kind": "have",
"target": "let a_0 = Mptr_2[(shift_PTR o_0 i_0)] in\n(P_rvalid_int_mat_3_ Malloc_2 Mptr_2\n (havoc Mint_undef_0 Mint_13 (shift_sint32 a_0 0) l_0)\n [(shift_sint32 a_0 j_0)->v_0] b_0 n_0 l_0\n (to_sint32\n (\\truncate (\\sqrt (real_of_int (to_sint32 (2147483647 div n_0)))))))",
"pattern": "P_rvalid_int_mat_3_$Malloc$Mptr[=]" },
"children":
{ "Unfold 'P_rvalid_int_mat_3_'":
[ { "header": "Definition",
"tactic": "Wp.unfold",
"params": {},
"select":
{ "select": "inside-step",
"at": 29,
"kind": "have",
"occur": 0,
"target": "(P_rvalid_int_mat_2_ Malloc_2 Mptr_2 b_0 n_0 l_0)",
"pattern": "P_rvalid_int_mat_2_$Malloc$Mptr$b" },
"children":
{ "Unfold 'P_rvalid_int_mat_2_'":
[ { "prover": "CVC4:1.9-prerelease:strings+counterexamples",
"verdict": "valid",
"time": 0.77 } ] } } ] } } ] } } ] } } ]
[ { "prover": "Alt-Ergo:2.3.3", "verdict": "timeout", "time": 10. } ]
[ { "prover": "Alt-Ergo:2.3.3", "verdict": "timeout", "time": 10. } ]
[ { "prover": "CVC4:1.9-prerelease:strings+counterexamples",
"verdict": "timeout", "time": 10. },
{ "prover": "Alt-Ergo:2.3.3", "verdict": "timeout", "time": 10. } ]
......@@ -4,4 +4,4 @@
"target": "let a_0 = (shiftfield_F15_Int32RMat_m r_2) in\n(lsl\n (to_sint32\n (\\truncate\n (16384+\n (real_of_int\n (Mint_18[(shift_sint32 a_0 4)]-Mint_18[(shift_sint32 a_0 0)]-\n Mint_18[(shift_sint32 a_0 8)]))))) 14)",
"pattern": "lslto_sint3214\\truncate+16384real_of_int" },
"children": { "gen_shift": [ { "prover": "CVC4:1.9-prerelease:strings+counterexamples",
"verdict": "valid", "time": 0.14 } ] } } ]
"verdict": "valid", "time": 0.25 } ] } } ]
......@@ -4,4 +4,4 @@
"target": "let a_0 = (shiftfield_F15_Int32RMat_m r_3) in\n(lsl\n (to_sint32\n (\\truncate\n (16384+\n (real_of_int\n (Mint_24[(shift_sint32 a_0 8)]-Mint_24[(shift_sint32 a_0 0)]-\n Mint_24[(shift_sint32 a_0 4)]))))) 14)",
"pattern": "lslto_sint3214\\truncate+16384real_of_int" },
"children": { "gen_shift": [ { "prover": "CVC4:1.9-prerelease:strings+counterexamples",
"verdict": "valid", "time": 0.15 } ] } } ]
"verdict": "valid", "time": 0.23 } ] } } ]
......@@ -4,4 +4,4 @@
"target": "let a_0 = (shiftfield_F15_Int32RMat_m r_1) in\n(lsl\n (to_sint32\n (\\truncate\n (16384+\n (real_of_int\n (Mint_12[(shift_sint32 a_0 0)]-Mint_12[(shift_sint32 a_0 4)]-\n Mint_12[(shift_sint32 a_0 8)]))))) 14)",
"pattern": "lslto_sint3214\\truncate+16384real_of_int" },
"children": { "gen_shift": [ { "prover": "CVC4:1.9-prerelease:strings+counterexamples",
"verdict": "valid", "time": 0.14 } ] } } ]
"verdict": "valid", "time": 0.26 } ] } } ]
......@@ -4,5 +4,5 @@
"target": "(lsr (to_sint32 (stheta_0*Mint_3[(shiftfield_F14_Int32Eulers_psi ed_0)])) 14)",
"pattern": "lsrto_sint3214*$stheta[]$Mintshiftfield_F14_Int32Eulers_psi" },
"children": { "gen_shift": [ { "prover": "Alt-Ergo:2.3.3",
"verdict": "valid", "time": 0.0563,
"steps": 244 } ] } } ]
"verdict": "valid", "time": 0.0841,
"steps": 296 } ] } } ]
[ { "prover": "CVC4:1.9-prerelease:strings+counterexamples",
"verdict": "timeout", "time": 10. },
{ "prover": "Alt-Ergo:2.3.3", "verdict": "timeout", "time": 10. } ]
......@@ -1238,38 +1238,6 @@ static inline bool int32_vect_find(const int32_t *a, const int32_t s, int *loc,
//
//
/*@
lemma sqrt_positive:
\forall int a;
a >= 0 ==> \sqrt(a) >= 0;
*/
/*
lemma square_sqrt:
\forall int a, b, n;
n > 0
&& -\sqrt(INT_MAX/n) <= a <= \sqrt(INT_MAX/n)
&& -\sqrt(INT_MAX/n) <= b <= \sqrt(INT_MAX/n)
==> -\sqrt(INT_MAX/n)*\sqrt(INT_MAX/n) <= a * b <= \sqrt(INT_MAX/n) * \sqrt(INT_MAX/n);
*/
/*
lemma square_sqrt_1:
\forall int a, b, n;
n > 0
&& -\sqrt(INT_MAX/n) <= a <= \sqrt(INT_MAX/n)
&& -\sqrt(INT_MAX/n) <= b <= \sqrt(INT_MAX/n)
==> -INT_MAX/n -1 <= a * b <= INT_MAX/n +1;
*/
/*
lemma square_sqrt_2:
\forall int a, b, n;
n > 0
==> \sqrt(INT_MAX/n) * \sqrt(INT_MAX/n) == INT_MAX/n;
*/
/** o = a * b
*
* a: [m x n]
......@@ -1278,8 +1246,8 @@ static inline bool int32_vect_find(const int32_t *a, const int32_t s, int *loc,
*/
/*@
requires valid_int_mat(o, m, l);
requires rvalid_int_mat(a, m, n, (int) \sqrt(INT_MAX/n));
requires rvalid_int_mat(b, n, l, (int) \sqrt(INT_MAX/n));
requires rvalid_int_mat(a, m, n, SQRT_INTM_n);
requires rvalid_int_mat(b, n, l, SQRT_INTM_n);
requires \separated(&(o[0..m-1][0..l-1]), &(a[0..m-1][0..n-1]), &(b[0..n-1][0..l-1]));
requires l > 0;
requires m > 0;
......@@ -1291,16 +1259,16 @@ static inline void int32_mat_mul(int32_t **o, int32_t **a, int32_t **b, int m, i
int i, j, k;
/*@
loop invariant 0 <= i <= m;
loop invariant rvalid_int_mat(a, m, n, (int) \sqrt(INT_MAX/n));
loop invariant rvalid_int_mat(b, n, l, (int) \sqrt(INT_MAX/n));
loop invariant rvalid_int_mat(a, m, n, SQRT_INTM_n);
loop invariant rvalid_int_mat(b, n, l, SQRT_INTM_n);
loop assigns o[0..m-1][0..l-1], i, j, k;
loop variant m - i;
*/
for (i = 0; i < m; i++) {
/*@
loop invariant 0 <= j <= l;
loop invariant rvalid_int_mat(a, m, n, (int) \sqrt(INT_MAX/n));
loop invariant rvalid_int_mat(b, n, l, (int) \sqrt(INT_MAX/n));
loop invariant rvalid_int_mat(a, m, n, SQRT_INTM_n);
loop invariant rvalid_int_mat(b, n, l, SQRT_INTM_n);
loop assigns o[i][0..l-1], j, k;
loop variant l - j;
*/
......@@ -1308,22 +1276,26 @@ static inline void int32_mat_mul(int32_t **o, int32_t **a, int32_t **b, int m, i
o[i][j] = 0;
/*@
loop invariant 0 <= k <= n;
loop invariant rvalid_int_mat(a, m, n, (int) \sqrt(INT_MAX/n));
loop invariant rvalid_int_mat(b, n, l, (int) \sqrt(INT_MAX/n));
loop invariant -k * INT_MAX / n <= o[i][j];
loop invariant o[i][j] <= k * INT_MAX / n;
loop invariant rvalid_int_mat(a, m, n, SQRT_INTM_n);
loop invariant rvalid_int_mat(b, n, l, SQRT_INTM_n);
loop invariant -k * INT_MAX_n <= o[i][j] <= k * INT_MAX_n;
loop assigns o[i][j], k;
loop variant n - k;
*/
for (k = 0; k < n; k++) {
//@ assert rvalid_int_mat(a, m, n, (int) \sqrt(INT_MAX/n));
//@ assert rvalid_int_mat(b, n, l, (int) \sqrt(INT_MAX/n));
//@ assert (int) -\sqrt(INT_MAX/n) <= a[i][k] <= \sqrt(INT_MAX/n);
//@ assert (int) -\sqrt(INT_MAX/n) <= b[k][j] <= \sqrt(INT_MAX/n);
//@assert -INT_MAX/n <= a[i][k] * b[k][j] <= INT_MAX/n;
//@ assert rvalid_int_mat(a, m, n, SQRT_INTM_n);
//@ assert rvalid_int_mat(b, n, l, SQRT_INTM_n);
//@ assert -SQRT_INTM_n <= a[i][k] <= SQRT_INTM_n;
//@ assert -SQRT_INTM_n <= b[k][j] <= SQRT_INTM_n;
//@ assert -INT_MAX_n <= a[i][k] * b[k][j] <= INT_MAX_n;
//@ assert -k * INT_MAX_n <= o[i][j] <= k * INT_MAX_n;
//@ assert -(k+1) * INT_MAX_n <= o[i][j] + a[i][k] * b[k][j]<= (k+1) * INT_MAX_n;
//@ assert k < n;
//@ assert (k+1) * INT_MAX_n <= INT_MAX;
o[i][j] += a[i][k] * b[k][j];
//@ assert rvalid_int_mat(a, m, n, (int) \sqrt(INT_MAX/n));
//@ assert rvalid_int_mat(b, n, l, (int) \sqrt(INT_MAX/n));
//@ assert -(k+1) * INT_MAX_n <= o[i][j] <= (k+1) * INT_MAX_n;
//@ assert rvalid_int_mat(a, m, n, SQRT_INTM_n);
//@ assert rvalid_int_mat(b, n, l, SQRT_INTM_n);
}
}
}
......
......@@ -292,6 +292,115 @@ typedef struct __fc_lldiv_t {
ensures \result.rem == numer % denom; */
extern lldiv_t lldiv(long long int numer, long long int denom);
/*******************************
* LEMMA for MAT_MUL
* *****************************/
#define INT_MAX_n ((int) (INT_MAX/n))
#define SQRT_INTM_n ((int) \sqrt(INT_MAX_n))
/*@
lemma sqrt_positive:
\forall int a;
a >= 0 ==> \sqrt(a) >= 0;
*/
/*
lemma sqrt_le:
\forall int a;
a > 0 ==> \sqrt(a) <= a;
*/
/*@
lemma sqrt_square_eq:
\forall int a;
a > 0 ==> a == \sqrt(a*a);
*/
/*@
lemma square_sqrt_le:
\forall int a;
a > 0 ==> a >= ((int) \sqrt(a)) * ((int) \sqrt(a));
*/
/*@
lemma square_sqrt_le_div:
\forall int a, b;
a > 0 && b > 0 ==> a/b >= ((int) \sqrt(a/b)) * ((int) \sqrt(a/b));
*/
/*@
lemma square_sqrt_bound:
\forall int a, b, bound;
bound > 0
&& -bound <= a <= bound
&& -bound <= b <= bound
==> -bound*bound <= a * b <= bound * bound;
*/
/*@
lemma mul_sqrt_max_n_bound:
\forall int a, b, n;
n > 0
&& -SQRT_INTM_n <= a <= SQRT_INTM_n
&& -SQRT_INTM_n <= b <= (int) \sqrt(INT_MAX/n)
==> -SQRT_INTM_n* SQRT_INTM_n <= a * b <= SQRT_INTM_n * SQRT_INTM_n;
*/
/*@
lemma square_sqrt_le_max:
\forall int n;
n > 0
==> SQRT_INTM_n * SQRT_INTM_n <= INT_MAX_n ;
*/
/*@
lemma n_mul_square_sqrt_le_n_max_n:
\forall int n;
n > 0
==> n * SQRT_INTM_n * SQRT_INTM_n <= n * INT_MAX_n ;
*/
/*@
lemma max_n_le_max:
\forall int n;
n > 0
==> n * INT_MAX_n <= INT_MAX ;
*/
/*@
lemma max_k_le_n_max:
\forall int n, k;
n > 0 && 0 < k < n
==> (k+1) * INT_MAX_n <= n * INT_MAX_n;
*/
/*@
lemma max_k_n_le_max:
\forall int n, k;
n > 0 && 0 < k < n
==> (k+1) * INT_MAX_n <= INT_MAX ;
*/
/*@
lemma n_mul_square_sqrt_le_max:
\forall int n;
n > 0
==> n * SQRT_INTM_n * SQRT_INTM_n <= INT_MAX ;
*/
/*@
lemma square_sqrt_max_n_bound:
\forall int a, b, n;
n > 0
&& -SQRT_INTM_n <= a <= SQRT_INTM_n
&& -SQRT_INTM_n <= b <= SQRT_INTM_n
==> -((int) INT_MAX_n) <= a * b <= ((int) INT_MAX_n);
*/
#ifdef __cplusplus
} /* extern "C" */
#endif
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment