Commit b8d7d146 authored by POLLIEN Baptiste's avatar POLLIEN Baptiste
Browse files

Update verification

parent b0a63524
...@@ -64,10 +64,10 @@ ...@@ -64,10 +64,10 @@
{ "Then": { "Then":
[ { "prover": "Z3:4.8.6:counterexamples", [ { "prover": "Z3:4.8.6:counterexamples",
"verdict": "valid", "verdict": "valid",
"time": 0.49, "time": 0.55,
"steps": 504498 } ], "steps": 505046 } ],
"Else": "Else":
[ { "prover": "Alt-Ergo:2.3.3", [ { "prover": "Alt-Ergo:2.3.3",
"verdict": "valid", "verdict": "valid",
"time": 1.5609, "time": 1.5624,
"steps": 988 } ] } } ] } } ] } } ] } } ] } } ] } } ] } } ] "steps": 988 } ] } } ] } } ] } } ] } } ] } } ] } } ] } } ]
...@@ -36,5 +36,5 @@ ...@@ -36,5 +36,5 @@
{ "Unfold 'L_trace_2_'": { "Unfold 'L_trace_2_'":
[ { "prover": "Alt-Ergo:2.3.3", [ { "prover": "Alt-Ergo:2.3.3",
"verdict": "valid", "verdict": "valid",
"time": 3.552, "time": 2.5621,
"steps": 1254 } ] } } ] } } ] } } ] } } ] "steps": 1254 } ] } } ] } } ] } } ] } } ]
...@@ -58,7 +58,7 @@ ...@@ -58,7 +58,7 @@
{ "Unfold 'L_l_FloatQuat_of_RMat_2_max_1_'": { "Unfold 'L_l_FloatQuat_of_RMat_2_max_1_'":
[ { "prover": "Alt-Ergo:2.3.3", [ { "prover": "Alt-Ergo:2.3.3",
"verdict": "valid", "verdict": "valid",
"time": 2.8336, "time": 2.0838,
"steps": 1013 }, "steps": 1013 },
{ "header": "Definition", { "header": "Definition",
"tactic": "Wp.unfold", "tactic": "Wp.unfold",
......
...@@ -49,8 +49,8 @@ ...@@ -49,8 +49,8 @@
{ "Then": { "Then":
[ { "prover": "Z3:4.8.6:counterexamples", [ { "prover": "Z3:4.8.6:counterexamples",
"verdict": "valid", "verdict": "valid",
"time": 0.49, "time": 0.35,
"steps": 439844 } ], "steps": 440524 } ],
"Else": "Else":
[ { "header": "Split", [ { "header": "Split",
"tactic": "Wp.split", "tactic": "Wp.split",
...@@ -76,8 +76,8 @@ ...@@ -76,8 +76,8 @@
{ "Then": { "Then":
[ { "prover": "Z3:4.8.6:counterexamples", [ { "prover": "Z3:4.8.6:counterexamples",
"verdict": "valid", "verdict": "valid",
"time": 0.41, "time": 0.42,
"steps": 404171 } ], "steps": 404711 } ],
"Else": "Else":
[ { "header": "Split", [ { "header": "Split",
"tactic": "Wp.split", "tactic": "Wp.split",
...@@ -92,13 +92,13 @@ ...@@ -92,13 +92,13 @@
{ "Then": { "Then":
[ { "prover": "Z3:4.8.6", [ { "prover": "Z3:4.8.6",
"verdict": "valid", "verdict": "valid",
"time": 0.09, "time": 0.07,
"steps": 259776 } ], "steps": 263164 } ],
"Else": "Else":
[ { "prover": "Z3:4.8.6:counterexamples", [ { "prover": "Z3:4.8.6:counterexamples",
"verdict": "valid", "verdict": "valid",
"time": 0.5, "time": 0.39,
"steps": 403279 } ] } } ] } } ], "steps": 403819 } ] } } ] } } ],
"Else": "Else":
[ { "header": "Split", [ { "header": "Split",
"tactic": "Wp.split", "tactic": "Wp.split",
...@@ -113,10 +113,10 @@ ...@@ -113,10 +113,10 @@
{ "Then": { "Then":
[ { "prover": "Z3:4.8.6:counterexamples", [ { "prover": "Z3:4.8.6:counterexamples",
"verdict": "valid", "verdict": "valid",
"time": 0.46, "time": 0.38,
"steps": 404145 } ], "steps": 404825 } ],
"Else": "Else":
[ { "prover": "Z3:4.8.6:counterexamples", [ { "prover": "Z3:4.8.6:counterexamples",
"verdict": "valid", "verdict": "valid",
"time": 0.43, "time": 0.41,
"steps": 400912 } ] } } ] } } ] } } ] } } ] } } ] } } ] } } ] "steps": 401454 } ] } } ] } } ] } } ] } } ] } } ] } } ] } } ]
...@@ -3,5 +3,5 @@ ...@@ -3,5 +3,5 @@
"target": "(P_rotation_matrix (L_l_RMat_of_FloatRMat Mf32_1 rm_0))", "target": "(P_rotation_matrix (L_l_RMat_of_FloatRMat Mf32_1 rm_0))",
"pattern": "P_rotation_matrixL_l_RMat_of_FloatRMat" }, "pattern": "P_rotation_matrixL_l_RMat_of_FloatRMat" },
"children": { "Filter": [ { "prover": "Alt-Ergo:2.3.3", "children": { "Filter": [ { "prover": "Alt-Ergo:2.3.3",
"verdict": "valid", "time": 5.7427, "verdict": "valid", "time": 5.4778,
"steps": 1628 } ] } } ] "steps": 1628 } ] } } ]
...@@ -70,7 +70,7 @@ ...@@ -70,7 +70,7 @@
{ "Unfold 'L_l_RMat_of_FloatRMat'": { "Unfold 'L_l_RMat_of_FloatRMat'":
[ { "prover": "Alt-Ergo:2.3.3", [ { "prover": "Alt-Ergo:2.3.3",
"verdict": "valid", "verdict": "valid",
"time": 4.5503, "time": 3.7112,
"steps": 809 }, "steps": 809 },
{ "header": "Definition", { "header": "Definition",
"tactic": "Wp.unfold", "tactic": "Wp.unfold",
......
[ { "header": "Definition", "tactic": "Wp.unfold", "params": {},
"select": { "select": "inside-goal", "occur": 0,
"target": "(L_cross_product v2_0 v1_0)",
"pattern": "L_cross_product$v2$v1" },
"children": { "Unfold 'L_cross_product'": [ { "header": "Definition",
"tactic": "Wp.unfold",
"params": {},
"select": { "select": "inside-goal",
"occur": 0,
"target": "let r_0 = v1_0.F12_RealVect3_s_y in\nlet r_1 = v2_0.F12_RealVect3_s_z in\nlet r_2 = v1_0.F12_RealVect3_s_z in\nlet r_3 = v2_0.F12_RealVect3_s_y in\nlet r_4 = v2_0.F12_RealVect3_s_x in\nlet r_5 = v1_0.F12_RealVect3_s_x in\n(L_mult_scalar_1_ -1\n {\n F12_RealVect3_s_x = (r_2*r_3)-(r_0*r_1) ;\n F12_RealVect3_s_y = (r_5*r_1)-(r_2*r_4) ;\n F12_RealVect3_s_z = (r_0*r_4)-(r_5*r_3)\n })",
"pattern": "L_mult_scalar_1_-1{RealVect3_s}+" },
"children": { "Unfold 'L_mult_scalar_1_'":
[ { "header": "Definition",
"tactic": "Wp.unfold",
"params": {},
"select":
{ "select": "inside-goal",
"occur": 0,
"target": "(L_cross_product v1_0 v2_0)",
"pattern": "L_cross_product$v1$v2" },
"children":
{ "Unfold 'L_cross_product'":
[ { "header": "Definition",
"tactic": "Wp.unfold",
"params": {},
"select":
{ "select": "clause-goal",
"target": "let r_0 = v1_0.F12_RealVect3_s_z in\nlet r_1 = v2_0.F12_RealVect3_s_y in\nlet r_2 = (r_0*r_1) in\nlet r_3 = v1_0.F12_RealVect3_s_y in\nlet r_4 = v2_0.F12_RealVect3_s_z in\nlet r_5 = (r_3*r_4) in\nlet r_6 = v1_0.F12_RealVect3_s_x in\nlet r_7 = (r_6*r_4) in\nlet r_8 = v2_0.F12_RealVect3_s_x in\nlet r_9 = (r_0*r_8) in\nlet r_10 = (r_3*r_8) in\nlet r_11 = (r_6*r_1) in\n(EqS12_RealVect3_s\n {\n F12_RealVect3_s_x = r_5-r_2 ;\n F12_RealVect3_s_y = r_9-r_7 ;\n F12_RealVect3_s_z = r_11-r_10\n }\n {\n F12_RealVect3_s_x = -1*(r_2-r_5) ;\n F12_RealVect3_s_y = -1*(r_7-r_9) ;\n F12_RealVect3_s_z = -1*(r_10-r_11)\n })",
"pattern": "EqS12_RealVect3_s{RealVect3_s}{RealVect3_s}" },
"children":
{ "Unfold 'EqS12_RealVect3_s'":
[ { "prover": "Alt-Ergo:2.3.3",
"verdict": "valid",
"time": 0.0181,
"steps": 8 },
{ "header": "Split",
"tactic": "Wp.split",
"params": {},
"select":
{ "select": "clause-goal",
"target": "let r_0 = v1_0.F12_RealVect3_s_x in\nlet r_1 = v2_0.F12_RealVect3_s_x in\nlet r_2 = (r_0*r_1) in\nlet r_3 = v1_0.F12_RealVect3_s_y in\nlet r_4 = v2_0.F12_RealVect3_s_y in\nlet r_5 = (r_3*r_4) in\nlet r_6 = v2_0.F12_RealVect3_s_z in\nlet r_7 = (r_3*r_6) in\nlet r_8 = v1_0.F12_RealVect3_s_z in\nlet r_9 = (r_8*r_4) in\nlet r_10 = (r_8*r_1) in\nlet r_11 = (r_0*r_6) in\n(r_2=(r_5+(-1*(r_2-r_5)))) /\\ (r_7=(r_9+(-1*(r_9-r_7))))\n/\\ (r_10=(r_11+(-1*(r_11-r_10))))",
"pattern": "&===*+*+*+.F12_RealVect3_s_x.F12_RealVect3_s_x" },
"children":
{ "Goal 1/3":
[ { "prover": "Z3:4.8.6:noBV",
"verdict": "timeout",
"time": 10. },
{ "prover": "Z3:4.8.6:counterexamples",
"verdict": "unknown" },
{ "prover": "Z3:4.8.6",
"verdict": "timeout",
"time": 10. },
{ "prover": "Coq:8.12.2",
"verdict": "unknown" },
{ "prover": "CVC4:1.9-prerelease:strings+counterexamples",
"verdict": "unknown" },
{ "prover": "Alt-Ergo:2.3.3",
"verdict": "timeout",
"time": 10. } ],
"Goal 2/3":
[ { "prover": "Alt-Ergo:2.3.3",
"verdict": "valid",
"time": 0.0062,
"steps": 8 } ],
"Goal 3/3":
[ { "prover": "Alt-Ergo:2.3.3",
"verdict": "valid",
"time": 0.0109,
"steps": 8 } ] } } ] } } ] } } ] } } ] } } ]
...@@ -63,5 +63,5 @@ ...@@ -63,5 +63,5 @@
{ "Unfold 'EqS13_RealRMat_s'": { "Unfold 'EqS13_RealRMat_s'":
[ { "prover": "Z3:4.8.6:counterexamples", [ { "prover": "Z3:4.8.6:counterexamples",
"verdict": "valid", "verdict": "valid",
"time": 0.04, "time": 0.03,
"steps": 51791 } ] } } ] } } ] } } ] } } ] } } ] } } ] } } ] "steps": 51791 } ] } } ] } } ] } } ] } } ] } } ] } } ] } } ]
[ { "prover": "Z3:4.8.6:noBV", "verdict": "timeout", "time": 10. },
{ "prover": "Z3:4.8.6:counterexamples", "verdict": "timeout", "time": 10. },
{ "prover": "Z3:4.8.6", "verdict": "timeout", "time": 10. },
{ "prover": "Coq:8.12.2", "verdict": "unknown" },
{ "prover": "CVC4:1.9-prerelease:strings+counterexamples",
"verdict": "timeout", "time": 10. },
{ "prover": "Alt-Ergo:2.3.3", "verdict": "timeout", "time": 10. } ]
...@@ -317,7 +317,7 @@ logic RealQuat conj(struct FloatQuat *q) = ...@@ -317,7 +317,7 @@ logic RealQuat conj(struct FloatQuat *q) =
/*@ ghost /*@ ghost
struct RealQuatVect_s {float scalar; struct RealQuatVect_s {float scalar;
struct RealVect3_s v;}; struct RealVect3_s vect;};
*/ */
//@ type RealQuatVect = struct RealQuatVect_s; //@ type RealQuatVect = struct RealQuatVect_s;
...@@ -330,16 +330,16 @@ logic RealQuat conj(struct FloatQuat *q) = ...@@ -330,16 +330,16 @@ logic RealQuat conj(struct FloatQuat *q) =
vqz) \ vqz) \
{{empty_quatvect \ {{empty_quatvect \
\with .scalar = (float) (vqi)} \ \with .scalar = (float) (vqi)} \
\with .v = ({{{empty_vect3 \ \with .vect = ({{{empty_vect3 \
\with .x = (float) (vqx)} \ \with .x = (float) (vqx)} \
\with .y = (float) (vqy)} \ \with .y = (float) (vqy)} \
\with .z = (float) (vqz)})} \with .z = (float) (vqz)})}
#define REALQUATVECT_FVECT(vqi, \ #define REALQUATVECT_FVECT(vqi, \
vect) \ v) \
{{empty_quatvect \ {{empty_quatvect \
\with .scalar = (float) (vqi)} \ \with .scalar = (float) (vqi)} \
\with .v = (vect)} \with .vect = (v)}
/*@ /*@
logic RealQuatVect l_QuatVect_of_FloatQuat(struct FloatQuat *q) = logic RealQuatVect l_QuatVect_of_FloatQuat(struct FloatQuat *q) =
...@@ -348,7 +348,7 @@ logic RealQuatVect l_QuatVect_of_FloatQuat(struct FloatQuat *q) = ...@@ -348,7 +348,7 @@ logic RealQuatVect l_QuatVect_of_FloatQuat(struct FloatQuat *q) =
/*@ /*@
logic RealQuat l_Quat_of_RealQuatVect(RealQuatVect q) = logic RealQuat l_Quat_of_RealQuatVect(RealQuatVect q) =
REALQUAT(q.scalar, q.v.x, q.v.y, q.v.y); REALQUAT(q.scalar, q.vect.x, q.vect.y, q.vect.y);
*/ */
/*@ /*@
...@@ -358,11 +358,11 @@ logic RealQuatVect l_QuatVect_of_RealQuat(RealQuat q) = ...@@ -358,11 +358,11 @@ logic RealQuatVect l_QuatVect_of_RealQuat(RealQuat q) =
/*@ /*@
logic RealQuatVect mult_RealQuatVect(RealQuatVect q1, RealQuatVect q2) = logic RealQuatVect mult_RealQuatVect(RealQuatVect q1, RealQuatVect q2) =
\let scalar = q1.scalar * q2.scalar - scalar_product(q1.v, q2.v); \let scalar = q1.scalar * q2.scalar - scalar_product(q1.vect, q2.vect);
\let vect = add_RealVect3(add_RealVect3( \let vect = add_RealVect3(add_RealVect3(
mult_scalar(q1.scalar, q2.v), mult_scalar(q1.scalar, q2.vect),
mult_scalar(q2.scalar, q1.v)), mult_scalar(q2.scalar, q1.vect)),
cross_product(q1.v, q2.v)); cross_product(q1.vect, q2.vect));
REALQUATVECT_FVECT(scalar, vect); REALQUATVECT_FVECT(scalar, vect);
*/ */
...@@ -373,7 +373,7 @@ logic RealQuatVect conj_v(struct FloatQuat *q) = ...@@ -373,7 +373,7 @@ logic RealQuatVect conj_v(struct FloatQuat *q) =
/*@ /*@
logic RealQuatVect conj_v(RealQuatVect q) = logic RealQuatVect conj_v(RealQuatVect q) =
\let vect = neg_vect(q.v); \let vect = neg_vect(q.vect);
REALQUATVECT_FVECT(q.scalar, vect); REALQUATVECT_FVECT(q.scalar, vect);
*/ */
...@@ -501,14 +501,28 @@ logic RealRMat l_RMat_of_FloatQuat(RealQuat q) = ...@@ -501,14 +501,28 @@ logic RealRMat l_RMat_of_FloatQuat(RealQuat q) =
==> special_orthogonal(l_RMat_of_FloatQuat(q)); ==> special_orthogonal(l_RMat_of_FloatQuat(q));
*/ */
/*@
logic RealQuatVect rotation_with_quat(RealQuatVect q, RealQuatVect v) =
mult_RealQuatVect(mult_RealQuatVect(q, v), conj_v(q));
*/
/*@
logic RealQuatVect rotation_with_quat(RealQuatVect q, RealVect3 v) =
rotation_with_quat(q, REALQUATVECT_FVECT(0, v));
*/
/*@
logic RealQuatVect rotation_with_quat(struct FloatQuat *q, RealVect3 v) =
rotation_with_quat(l_QuatVect_of_FloatQuat(q), v);
*/
/*@ /*@
lemma verify_rmat_of_quat_formula: lemma verify_rmat_of_quat_formula:
\forall struct FloatQuat *q, struct FloatVect3 *v; \forall struct FloatQuat *q, struct FloatVect3 *v;
\let vect = l_Vect_of_FloatVect3(v); \let vect = l_Vect_of_FloatVect3(v);
\let rmat = l_RMat_of_FloatQuat(q); \let rmat = l_RMat_of_FloatQuat(q);
\let mult_quat = mult_RealQuatVect(l_QuatVect_of_FloatQuat(q), REALQUATVECT_FVECT(0, vect)); \let quat_rot = rotation_with_quat(q, vect);
mult_RealQuatVect(mult_quat, conj_v(q)) quat_rot == REALQUATVECT_FVECT(0, mult_RealRMat_RealVect3(rmat, vect));
== REALQUATVECT_FVECT(0, mult_RealRMat_RealVect3(rmat, vect));
*/ */
/******************************* /*******************************
......
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