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

Adding Coq proof script

parent df02b4a5
......@@ -89,5 +89,5 @@
{ "Unfold 'L_l_RMat_of_FloatRMat'":
[ { "prover": "Alt-Ergo:2.3.3",
"verdict": "valid",
"time": 1.2982,
"steps": 989 } ] } } ] } } ] } } ] } } ] } } ] } } ] } } ] } } ] } } ]
"time": 1.364,
"steps": 992 } ] } } ] } } ] } } ] } } ] } } ] } } ] } } ] } } ] } } ]
......@@ -36,5 +36,5 @@
{ "Unfold 'L_trace_2_'":
[ { "prover": "Alt-Ergo:2.3.3",
"verdict": "valid",
"time": 2.6921,
"steps": 1249 } ] } } ] } } ] } } ] } } ]
"time": 2.5319,
"steps": 1252 } ] } } ] } } ] } } ] } } ]
......@@ -58,8 +58,8 @@
{ "Unfold 'L_l_FloatQuat_of_RMat_2_max_1_'":
[ { "prover": "Alt-Ergo:2.3.3",
"verdict": "valid",
"time": 1.7844,
"steps": 1008 },
"time": 2.5305,
"steps": 1013 },
{ "header": "Definition",
"tactic": "Wp.unfold",
"params": {},
......
......@@ -49,8 +49,8 @@
{ "Then":
[ { "prover": "Z3:4.8.6:counterexamples",
"verdict": "valid",
"time": 0.29,
"steps": 429570 } ],
"time": 0.5,
"steps": 431175 } ],
"Else":
[ { "header": "Split",
"tactic": "Wp.split",
......@@ -76,8 +76,8 @@
{ "Then":
[ { "prover": "Z3:4.8.6:counterexamples",
"verdict": "valid",
"time": 0.32,
"steps": 394374 } ],
"time": 0.39,
"steps": 395604 } ],
"Else":
[ { "header": "Split",
"tactic": "Wp.split",
......@@ -92,13 +92,13 @@
{ "Then":
[ { "prover": "Z3:4.8.6",
"verdict": "valid",
"time": 0.04,
"steps": 207345 } ],
"time": 0.08,
"steps": 223243 } ],
"Else":
[ { "prover": "Z3:4.8.6:counterexamples",
"verdict": "valid",
"time": 0.49,
"steps": 393035 } ] } } ] } } ],
"time": 0.36,
"steps": 394729 } ] } } ] } } ],
"Else":
[ { "header": "Split",
"tactic": "Wp.split",
......@@ -113,10 +113,10 @@
{ "Then":
[ { "prover": "Z3:4.8.6:counterexamples",
"verdict": "valid",
"time": 0.29,
"steps": 393824 } ],
"time": 0.39,
"steps": 395218 } ],
"Else":
[ { "prover": "Z3:4.8.6:counterexamples",
"verdict": "valid",
"time": 0.5,
"steps": 390520 } ] } } ] } } ] } } ] } } ] } } ] } } ] } } ]
"time": 0.4,
"steps": 392197 } ] } } ] } } ] } } ] } } ] } } ] } } ] } } ]
......@@ -3,5 +3,5 @@
"target": "(P_rotation_matrix (L_l_RMat_of_FloatRMat Mf32_1 rm_0))",
"pattern": "P_rotation_matrixL_l_RMat_of_FloatRMat" },
"children": { "Filter": [ { "prover": "Alt-Ergo:2.3.3",
"verdict": "valid", "time": 4.7786,
"steps": 1623 } ] } } ]
"verdict": "valid", "time": 6.2335,
"steps": 1628 } ] } } ]
......@@ -79,5 +79,5 @@
{ "Unfold 'EqS13_RealQuat_s'":
[ { "prover": "Alt-Ergo:2.3.3",
"verdict": "valid",
"time": 9.2189,
"steps": 4599 } ] } } ] } } ] } } ] } } ] } } ] } } ] } } ] } } ]
"time": 7.3667,
"steps": 4632 } ] } } ] } } ] } } ] } } ] } } ] } } ] } } ] } } ]
......@@ -59,30 +59,30 @@
{ "Goal 1/6":
[ { "prover": "Alt-Ergo:2.3.3",
"verdict": "valid",
"time": 1.5198,
"time": 1.419,
"steps": 102 } ],
"Goal 2/6":
[ { "prover": "Z3:4.8.6:counterexamples",
"verdict": "valid",
"time": 0.03,
"steps": 65603 } ],
"time": 0.04,
"steps": 69389 } ],
"Goal 3/6":
[ { "prover": "Z3:4.8.6:counterexamples",
"verdict": "valid",
"time": 0.05,
"steps": 65611 } ],
"time": 0.04,
"steps": 69395 } ],
"Goal 4/6":
[ { "prover": "Alt-Ergo:2.3.3",
"verdict": "valid",
"time": 2.4062,
"time": 2.5923,
"steps": 102 } ],
"Goal 5/6":
[ { "prover": "Alt-Ergo:2.3.3",
"verdict": "valid",
"time": 1.7948,
"time": 2.0899,
"steps": 102 } ],
"Goal 6/6":
[ { "prover": "Alt-Ergo:2.3.3",
"verdict": "valid",
"time": 1.6473,
"time": 1.8943,
"steps": 102 } ] } } ] } } ] } } ] } } ] } } ] } } ] } } ]
......@@ -11,5 +11,5 @@
"children": { "Unfold 'P_special_orthogonal'":
[ { "prover": "Alt-Ergo:2.3.3",
"verdict": "valid",
"time": 2.004,
"time": 2.4431,
"steps": 102 } ] } } ] } } ]
......@@ -59,30 +59,30 @@
{ "Goal 1/6":
[ { "prover": "Alt-Ergo:2.3.3",
"verdict": "valid",
"time": 1.5519,
"time": 1.3571,
"steps": 102 } ],
"Goal 2/6":
[ { "prover": "Z3:4.8.6",
"verdict": "valid",
"time": 0.49,
"steps": 2395621 } ],
"time": 0.51,
"steps": 2414090 } ],
"Goal 3/6":
[ { "prover": "Alt-Ergo:2.3.3",
"verdict": "valid",
"time": 2.404,
"time": 2.4556,
"steps": 102 } ],
"Goal 4/6":
[ { "prover": "Z3:4.8.6",
"verdict": "valid",
"time": 0.63,
"steps": 2395606 } ],
"time": 0.55,
"steps": 2414075 } ],
"Goal 5/6":
[ { "prover": "Alt-Ergo:2.3.3",
"verdict": "valid",
"time": 1.9978,
"time": 1.889,
"steps": 102 } ],
"Goal 6/6":
[ { "prover": "Alt-Ergo:2.3.3",
"verdict": "valid",
"time": 1.8339,
"time": 1.9076,
"steps": 102 } ] } } ] } } ] } } ] } } ] } } ] } } ] } } ]
......@@ -11,5 +11,5 @@
"children": { "Unfold 'P_special_orthogonal'":
[ { "prover": "Alt-Ergo:2.3.3",
"verdict": "valid",
"time": 1.9255,
"time": 1.9546,
"steps": 102 } ] } } ] } } ]
......@@ -3,9 +3,9 @@
"target": "(separated rm_0 9 q_0 4)",
"pattern": "separated$rm9$q4" },
"children": { "WrongBase": [ { "prover": "CVC4:1.9-prerelease:strings+counterexamples",
"verdict": "valid", "time": 1.03 } ],
"verdict": "valid", "time": 1.09 } ],
"OnLeft": [ { "prover": "CVC4:1.9-prerelease:strings+counterexamples",
"verdict": "valid", "time": 4.37 } ],
"verdict": "valid", "time": 4.23 } ],
"OnRight": [ { "prover": "CVC4:1.9-prerelease:strings+counterexamples",
"verdict": "valid", "time": 4.26 } ],
"verdict": "valid", "time": 4.53 } ],
"OverLap": [ { "prover": "qed", "verdict": "valid" } ] } } ]
......@@ -3,9 +3,9 @@
"target": "(separated rm_0 9 q_0 4)",
"pattern": "separated$rm9$q4" },
"children": { "WrongBase": [ { "prover": "CVC4:1.9-prerelease:strings+counterexamples",
"verdict": "valid", "time": 4.54 } ],
"verdict": "valid", "time": 3.6 } ],
"OnLeft": [ { "prover": "CVC4:1.9-prerelease:strings+counterexamples",
"verdict": "valid", "time": 6.1 } ],
"verdict": "valid", "time": 6.07 } ],
"OnRight": [ { "prover": "CVC4:1.9-prerelease:strings+counterexamples",
"verdict": "valid", "time": 5.76 } ],
"verdict": "valid", "time": 5.57 } ],
"OverLap": [ { "prover": "qed", "verdict": "valid" } ] } } ]
......@@ -3,7 +3,7 @@
"target": "(separated rm_0 9 q_0 4)",
"pattern": "separated$rm9$q4" },
"children": { "WrongBase": [ { "prover": "Alt-Ergo:2.3.3",
"verdict": "valid", "time": 13.8492,
"verdict": "valid", "time": 12.7704,
"steps": 130 } ],
"OnLeft": [ { "header": "Definition",
"tactic": "Wp.unfold", "params": {},
......@@ -15,7 +15,7 @@
"children": { "Unfold 'P_unary_quaternion_1_'":
[ { "prover": "CVC4:1.9-prerelease:strings+counterexamples",
"verdict": "valid",
"time": 5.93 } ] } } ],
"time": 7.14 } ] } } ],
"OnRight": [ { "header": "Definition",
"tactic": "Wp.unfold", "params": {},
"select": { "select": "inside-step",
......@@ -26,5 +26,5 @@
"children": { "Unfold 'P_unary_quaternion_1_'":
[ { "prover": "CVC4:1.9-prerelease:strings+counterexamples",
"verdict": "valid",
"time": 6.06 } ] } } ],
"time": 7.47 } ] } } ],
"OverLap": [ { "prover": "qed", "verdict": "valid" } ] } } ]
......@@ -3,9 +3,9 @@
"target": "(separated rm_0 9 q_0 4)",
"pattern": "separated$rm9$q4" },
"children": { "WrongBase": [ { "prover": "CVC4:1.9-prerelease:strings+counterexamples",
"verdict": "valid", "time": 6. } ],
"verdict": "valid", "time": 5.72 } ],
"OnLeft": [ { "prover": "CVC4:1.9-prerelease:strings+counterexamples",
"verdict": "valid", "time": 9.26 } ],
"verdict": "valid", "time": 10.1 } ],
"OnRight": [ { "prover": "CVC4:1.9-prerelease:strings+counterexamples",
"verdict": "valid", "time": 12.66 } ],
"verdict": "valid", "time": 10.07 } ],
"OverLap": [ { "prover": "qed", "verdict": "valid" } ] } } ]
......@@ -12,4 +12,4 @@
"children": { "Unfold 'L_l_RMat_of_FloatQuat_1_'":
[ { "prover": "CVC4:1.9-prerelease:strings+counterexamples",
"verdict": "valid",
"time": 3.24 } ] } } ] } } ]
"time": 3.42 } ] } } ] } } ]
[ { "header": "Definition", "tactic": "Wp.unfold", "params": {},
[ { "prover": "script", "verdict": "valid" },
{ "header": "Definition", "tactic": "Wp.unfold", "params": {},
"select": { "select": "clause-goal",
"target": "let a_0 = (shiftfield_F9_FloatRMat_m rm_0) in\nlet r_0 = Mf32_1[(shiftfield_F7_FloatQuat_qi q_0)] in\nlet r_1 = (2*r_0*r_0) in\nlet r_2 = Mf32_1[(shiftfield_F7_FloatQuat_qx q_0)] in\nlet r_3 = Mf32_1[(shiftfield_F7_FloatQuat_qz q_0)] in\nlet r_4 = (2*r_0*r_3) in\nlet r_5 = Mf32_1[(shiftfield_F7_FloatQuat_qy q_0)] in\nlet r_6 = (2*r_2*r_5) in\nlet r_7 = (2*r_0*r_5) in\nlet r_8 = (2*r_2*r_3) in\nlet r_9 = (2*r_0*r_2) in\nlet r_10 = (2*r_5*r_3) in\n(P_rotation_matrix\n (L_l_RMat_of_FloatRMat\n Mf32_1[(shift_float32 a_0 0)->r_1+(2*r_2*r_2)-1][(shift_float32 a_0 1)\n ->r_4+r_6][(shift_float32 a_0 2)->r_8-r_7][(shift_float32 a_0 3)\n ->r_6-r_4][(shift_float32 a_0 4)->r_1+(2*r_5*r_5)-1]\n [(shift_float32 a_0 5)->r_9+r_10][(shift_float32 a_0 6)->r_7+r_8]\n [(shift_float32 a_0 7)->r_10-r_9][(shift_float32 a_0 8)\n ->r_1+(2*r_3*r_3)-1] rm_0))",
"pattern": "P_rotation_matrixL_l_RMat_of_FloatRMat" },
......@@ -72,12 +73,46 @@
{ "Unfold 'P_unary_quaternion_1_'":
[ { "prover": "CVC4:1.9-prerelease:strings+counterexamples",
"verdict": "valid",
"time": 1.29 } ] } } ],
"time": 2.52 } ] } } ],
"Goal 2/6":
[ { "prover": "Alt-Ergo:2.3.3",
[ { "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": 16. },
{ "header": "Definition",
"tactic": "Wp.unfold",
"params": {},
"select":
{ "select": "inside-step",
"at": 2,
"kind": "have",
"occur": 0,
"target": "(P_unary_quaternion_1_ Mf32_1 q_0)",
"pattern": "P_unary_quaternion_1_$Mf32$q" },
"children":
{ "Unfold 'P_unary_quaternion_1_'":
[ { "prover": "Coq:8.12.2",
"verdict": "unknown" },
{ "prover": "CVC4:1.9-prerelease:strings+counterexamples",
"verdict": "valid",
"time": 10.5076,
"steps": 134 } ],
"time": 1.66 },
{ "prover": "Alt-Ergo:2.3.3",
"verdict": "valid",
"time": 1.5465,
"steps": 28 } ] } } ],
"Goal 3/6":
[ { "header": "Definition",
"tactic": "Wp.unfold",
......@@ -93,12 +128,25 @@
{ "Unfold 'P_unary_quaternion_1_'":
[ { "prover": "CVC4:1.9-prerelease:strings+counterexamples",
"verdict": "valid",
"time": 1.03 } ] } } ],
"time": 1.57 } ] } } ],
"Goal 4/6":
[ { "prover": "Alt-Ergo:2.3.3",
"verdict": "valid",
"time": 9.7143,
"steps": 138 },
[ { "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": 15. },
{ "header": "Definition",
"tactic": "Wp.unfold",
"params": {},
......@@ -107,20 +155,50 @@
"at": 2,
"kind": "have",
"occur": 0,
"target": "(P_unary_quaternion Mf32_1 q_0)",
"pattern": "P_unary_quaternion$Mf32$q" },
"target": "(P_unary_quaternion_1_ Mf32_1 q_0)",
"pattern": "P_unary_quaternion_1_$Mf32$q" },
"children":
{ "Unfold 'P_unary_quaternion'":
{ "Unfold 'P_unary_quaternion_1_'":
[ { "prover": "Coq:8.12.2",
"verdict": "unknown" },
{ "prover": "CVC4:1.9-prerelease:strings+counterexamples",
"verdict": "valid",
"time": 1.37 } ] } } ],
"time": 1.4 } ] } } ],
"Goal 5/6":
[ { "prover": "Alt-Ergo:2.3.3",
[ { "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": 18. },
{ "header": "Definition",
"tactic": "Wp.unfold",
"params": {},
"select":
{ "select": "inside-step",
"at": 2,
"kind": "have",
"occur": 0,
"target": "(P_unary_quaternion_1_ Mf32_1 q_0)",
"pattern": "P_unary_quaternion_1_$Mf32$q" },
"children":
{ "Unfold 'P_unary_quaternion_1_'":
[ { "prover": "Coq:8.12.2",
"verdict": "unknown" },
{ "prover": "CVC4:1.9-prerelease:strings+counterexamples",
"verdict": "valid",
"time": 13.0984,
"steps": 138 } ],
"time": 1.68 } ] } } ],
"Goal 6/6":
[ { "header": "Definition",
"tactic": "Wp.unfold",
......@@ -134,7 +212,37 @@
"pattern": "shift_float32shiftfield_F9_FloatRMat_m" },
"children":
{ "Unfold 'shift_float32'":
[ { "prover": "Alt-Ergo:2.3.3",
[ { "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": 18. },
{ "header": "Definition",
"tactic": "Wp.unfold",
"params": {},
"select":
{ "select": "inside-step",
"at": 2,
"kind": "have",
"occur": 0,
"target": "(P_unary_quaternion_1_ Mf32_1 q_0)",
"pattern": "P_unary_quaternion_1_$Mf32$q" },
"children":
{ "Unfold 'P_unary_quaternion_1_'":
[ { "prover": "Coq:8.12.2",
"verdict": "unknown" },
{ "prover": "CVC4:1.9-prerelease:strings+counterexamples",
"verdict": "valid",
"time": 13.1437,
"steps": 138 } ] } } ] } } ] } } ] } } ] } } ] } } ] } } ] } } ]
"time": 1.43 } ] } } ] } } ] } } ] } } ] } } ] } } ] } } ] } } ] } } ]
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