Commit 536cc258 authored by POLLIEN Baptiste's avatar POLLIEN Baptiste
Browse files

Start rmat_of_eulers

parent aa6dd827
...@@ -56,7 +56,7 @@ ...@@ -56,7 +56,7 @@
"params": {}, "params": {},
"select": "select":
{ "select": "inside-step", { "select": "inside-step",
"at": 3, "at": 6,
"kind": "have", "kind": "have",
"occur": 0, "occur": 0,
"target": "(L_trace_2_ Mf32_2 rm_0)", "target": "(L_trace_2_ Mf32_2 rm_0)",
...@@ -68,7 +68,7 @@ ...@@ -68,7 +68,7 @@
"params": {}, "params": {},
"select": "select":
{ "select": "inside-step", { "select": "inside-step",
"at": 3, "at": 6,
"kind": "have", "kind": "have",
"occur": 0, "occur": 0,
"target": "(L_trace_1_ (L_l_RMat_of_FloatRMat Mf32_2 rm_0))", "target": "(L_trace_1_ (L_l_RMat_of_FloatRMat Mf32_2 rm_0))",
...@@ -80,7 +80,7 @@ ...@@ -80,7 +80,7 @@
"params": {}, "params": {},
"select": "select":
{ "select": "inside-step", { "select": "inside-step",
"at": 3, "at": 4,
"kind": "have", "kind": "have",
"occur": 0, "occur": 0,
"target": "(L_l_RMat_of_FloatRMat Mf32_2 rm_0)", "target": "(L_l_RMat_of_FloatRMat Mf32_2 rm_0)",
...@@ -89,5 +89,5 @@ ...@@ -89,5 +89,5 @@
{ "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": 3.5527, "time": 4.9965,
"steps": 2040 } ] } } ] } } ] } } ] } } ] } } ] } } ] } } ] } } ] } } ] "steps": 1942 } ] } } ] } } ] } } ] } } ] } } ] } } ] } } ] } } ] } } ]
...@@ -56,7 +56,7 @@ ...@@ -56,7 +56,7 @@
"params": {}, "params": {},
"select": "select":
{ "select": "inside-step", { "select": "inside-step",
"at": 3, "at": 6,
"kind": "have", "kind": "have",
"occur": 0, "occur": 0,
"target": "(L_trace_2_ Mf32_2 rm_0)", "target": "(L_trace_2_ Mf32_2 rm_0)",
...@@ -68,7 +68,7 @@ ...@@ -68,7 +68,7 @@
"params": {}, "params": {},
"select": "select":
{ "select": "inside-step", { "select": "inside-step",
"at": 3, "at": 6,
"kind": "have", "kind": "have",
"occur": 0, "occur": 0,
"target": "(L_trace_1_ (L_l_RMat_of_FloatRMat Mf32_2 rm_0))", "target": "(L_trace_1_ (L_l_RMat_of_FloatRMat Mf32_2 rm_0))",
...@@ -80,7 +80,7 @@ ...@@ -80,7 +80,7 @@
"params": {}, "params": {},
"select": "select":
{ "select": "inside-step", { "select": "inside-step",
"at": 3, "at": 4,
"kind": "have", "kind": "have",
"occur": 0, "occur": 0,
"target": "(L_l_RMat_of_FloatRMat Mf32_2 rm_0)", "target": "(L_l_RMat_of_FloatRMat Mf32_2 rm_0)",
...@@ -89,5 +89,5 @@ ...@@ -89,5 +89,5 @@
{ "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": 2.8084, "time": 3.9911,
"steps": 1398 } ] } } ] } } ] } } ] } } ] } } ] } } ] } } ] } } ] } } ] "steps": 1765 } ] } } ] } } ] } } ] } } ] } } ] } } ] } } ] } } ] } } ]
...@@ -17,7 +17,7 @@ ...@@ -17,7 +17,7 @@
"params": {}, "params": {},
"select": "select":
{ "select": "inside-step", { "select": "inside-step",
"at": 3, "at": 6,
"kind": "have", "kind": "have",
"occur": 0, "occur": 0,
"target": "(L_trace_2_ Mf32_2 rm_0)", "target": "(L_trace_2_ Mf32_2 rm_0)",
...@@ -29,7 +29,7 @@ ...@@ -29,7 +29,7 @@
"params": {}, "params": {},
"select": "select":
{ "select": "inside-step", { "select": "inside-step",
"at": 3, "at": 6,
"kind": "have", "kind": "have",
"occur": 0, "occur": 0,
"target": "(L_trace_1_ (L_l_RMat_of_FloatRMat Mf32_2 rm_0))", "target": "(L_trace_1_ (L_l_RMat_of_FloatRMat Mf32_2 rm_0))",
...@@ -86,20 +86,20 @@ ...@@ -86,20 +86,20 @@
{ "Goal 1/4": { "Goal 1/4":
[ { "prover": "Alt-Ergo:2.3.3", [ { "prover": "Alt-Ergo:2.3.3",
"verdict": "valid", "verdict": "valid",
"time": 2.569, "time": 2.7552,
"steps": 357 } ], "steps": 357 } ],
"Goal 2/4": "Goal 2/4":
[ { "prover": "Alt-Ergo:2.3.3", [ { "prover": "Alt-Ergo:2.3.3",
"verdict": "valid", "verdict": "valid",
"time": 2.7146, "time": 2.3541,
"steps": 380 } ], "steps": 380 } ],
"Goal 3/4": "Goal 3/4":
[ { "prover": "Alt-Ergo:2.3.3", [ { "prover": "Alt-Ergo:2.3.3",
"verdict": "valid", "verdict": "valid",
"time": 2.8463, "time": 2.2624,
"steps": 379 } ], "steps": 379 } ],
"Goal 4/4": "Goal 4/4":
[ { "prover": "Alt-Ergo:2.3.3", [ { "prover": "Alt-Ergo:2.3.3",
"verdict": "valid", "verdict": "valid",
"time": 2.7158, "time": 2.2096,
"steps": 379 } ] } } ] } } ] } } ] } } ] } } ] } } ] } } ] } } ] } } ] "steps": 379 } ] } } ] } } ] } } ] } } ] } } ] } } ] } } ] } } ] } } ]
[ { "header": "Definition", "tactic": "Wp.unfold", "params": {}, [ { "header": "Definition", "tactic": "Wp.unfold", "params": {},
"select": { "select": "inside-step", "at": 2, "kind": "have", "occur": 0, "select": { "select": "inside-step", "at": 4, "kind": "have", "occur": 0,
"target": "(L_l_RMat_of_FloatRMat Mf32_6 rm_0)", "target": "(L_l_RMat_of_FloatRMat Mf32_6 rm_0)",
"pattern": "L_l_RMat_of_FloatRMat$Mf32$rm" }, "pattern": "L_l_RMat_of_FloatRMat$Mf32$rm" },
"children": { "Unfold 'L_l_RMat_of_FloatRMat'": [ { "header": "Definition", "children": { "Unfold 'L_l_RMat_of_FloatRMat'": [ { "header": "Definition",
"tactic": "Wp.unfold", "tactic": "Wp.unfold",
"params": {}, "params": {},
"select": { "select": "inside-step", "select": { "select": "inside-step",
"at": 2, "at": 4,
"kind": "have", "kind": "have",
"occur": 0, "occur": 0,
"target": "let a_0 = (shiftfield_F6_FloatRMat_m rm_0) in\n(P_rotation_matrix\n {\n F9_RealRMat_s_a00 = Mf32_6[(shift_float32 a_0 0)] ;\n F9_RealRMat_s_a01 = Mf32_6[(shift_float32 a_0 1)] ;\n F9_RealRMat_s_a02 = Mf32_6[(shift_float32 a_0 2)] ;\n F9_RealRMat_s_a10 = Mf32_6[(shift_float32 a_0 3)] ;\n F9_RealRMat_s_a11 = Mf32_6[(shift_float32 a_0 4)] ;\n F9_RealRMat_s_a12 = Mf32_6[(shift_float32 a_0 5)] ;\n F9_RealRMat_s_a20 = Mf32_6[(shift_float32 a_0 6)] ;\n F9_RealRMat_s_a21 = Mf32_6[(shift_float32 a_0 7)] ;\n F9_RealRMat_s_a22 = Mf32_6[(shift_float32 a_0 8)]\n })", "target": "let a_0 = (shiftfield_F6_FloatRMat_m rm_0) in\n(P_rotation_matrix\n {\n F9_RealRMat_s_a00 = Mf32_6[(shift_float32 a_0 0)] ;\n F9_RealRMat_s_a01 = Mf32_6[(shift_float32 a_0 1)] ;\n F9_RealRMat_s_a02 = Mf32_6[(shift_float32 a_0 2)] ;\n F9_RealRMat_s_a10 = Mf32_6[(shift_float32 a_0 3)] ;\n F9_RealRMat_s_a11 = Mf32_6[(shift_float32 a_0 4)] ;\n F9_RealRMat_s_a12 = Mf32_6[(shift_float32 a_0 5)] ;\n F9_RealRMat_s_a20 = Mf32_6[(shift_float32 a_0 6)] ;\n F9_RealRMat_s_a21 = Mf32_6[(shift_float32 a_0 7)] ;\n F9_RealRMat_s_a22 = Mf32_6[(shift_float32 a_0 8)]\n })",
...@@ -17,7 +17,7 @@ ...@@ -17,7 +17,7 @@
"params": {}, "params": {},
"select": "select":
{ "select": "inside-step", { "select": "inside-step",
"at": 2, "at": 4,
"kind": "have", "kind": "have",
"occur": 0, "occur": 0,
"target": "let a_0 = (shiftfield_F6_FloatRMat_m rm_0) in\n(L_transpose\n {\n F9_RealRMat_s_a00 = Mf32_6[(shift_float32 a_0 0)] ;\n F9_RealRMat_s_a01 = Mf32_6[(shift_float32 a_0 1)] ;\n F9_RealRMat_s_a02 = Mf32_6[(shift_float32 a_0 2)] ;\n F9_RealRMat_s_a10 = Mf32_6[(shift_float32 a_0 3)] ;\n F9_RealRMat_s_a11 = Mf32_6[(shift_float32 a_0 4)] ;\n F9_RealRMat_s_a12 = Mf32_6[(shift_float32 a_0 5)] ;\n F9_RealRMat_s_a20 = Mf32_6[(shift_float32 a_0 6)] ;\n F9_RealRMat_s_a21 = Mf32_6[(shift_float32 a_0 7)] ;\n F9_RealRMat_s_a22 = Mf32_6[(shift_float32 a_0 8)]\n })", "target": "let a_0 = (shiftfield_F6_FloatRMat_m rm_0) in\n(L_transpose\n {\n F9_RealRMat_s_a00 = Mf32_6[(shift_float32 a_0 0)] ;\n F9_RealRMat_s_a01 = Mf32_6[(shift_float32 a_0 1)] ;\n F9_RealRMat_s_a02 = Mf32_6[(shift_float32 a_0 2)] ;\n F9_RealRMat_s_a10 = Mf32_6[(shift_float32 a_0 3)] ;\n F9_RealRMat_s_a11 = Mf32_6[(shift_float32 a_0 4)] ;\n F9_RealRMat_s_a12 = Mf32_6[(shift_float32 a_0 5)] ;\n F9_RealRMat_s_a20 = Mf32_6[(shift_float32 a_0 6)] ;\n F9_RealRMat_s_a21 = Mf32_6[(shift_float32 a_0 7)] ;\n F9_RealRMat_s_a22 = Mf32_6[(shift_float32 a_0 8)]\n })",
...@@ -29,7 +29,7 @@ ...@@ -29,7 +29,7 @@
"params": {}, "params": {},
"select": "select":
{ "select": "inside-step", { "select": "inside-step",
"at": 2, "at": 4,
"kind": "have", "kind": "have",
"occur": 0, "occur": 0,
"target": "let a_0 = (shiftfield_F6_FloatRMat_m rm_0) in\nlet r_0 = Mf32_6[(shift_float32 a_0 0)] in\nlet r_1 = Mf32_6[(shift_float32 a_0 1)] in\nlet r_2 = Mf32_6[(shift_float32 a_0 2)] in\nlet r_3 = Mf32_6[(shift_float32 a_0 3)] in\nlet r_4 = Mf32_6[(shift_float32 a_0 4)] in\nlet r_5 = Mf32_6[(shift_float32 a_0 5)] in\nlet r_6 = Mf32_6[(shift_float32 a_0 6)] in\nlet r_7 = Mf32_6[(shift_float32 a_0 7)] in\nlet r_8 = Mf32_6[(shift_float32 a_0 8)] in\n(L_mult_RealRMat\n {\n F9_RealRMat_s_a00 = r_0 ;\n F9_RealRMat_s_a01 = r_1 ;\n F9_RealRMat_s_a02 = r_2 ;\n F9_RealRMat_s_a10 = r_3 ;\n F9_RealRMat_s_a11 = r_4 ;\n F9_RealRMat_s_a12 = r_5 ;\n F9_RealRMat_s_a20 = r_6 ;\n F9_RealRMat_s_a21 = r_7 ;\n F9_RealRMat_s_a22 = r_8\n }\n {\n F9_RealRMat_s_a00 = r_0 ;\n F9_RealRMat_s_a01 = r_3 ;\n F9_RealRMat_s_a02 = r_6 ;\n F9_RealRMat_s_a10 = r_1 ;\n F9_RealRMat_s_a11 = r_4 ;\n F9_RealRMat_s_a12 = r_7 ;\n F9_RealRMat_s_a20 = r_2 ;\n F9_RealRMat_s_a21 = r_5 ;\n F9_RealRMat_s_a22 = r_8\n })", "target": "let a_0 = (shiftfield_F6_FloatRMat_m rm_0) in\nlet r_0 = Mf32_6[(shift_float32 a_0 0)] in\nlet r_1 = Mf32_6[(shift_float32 a_0 1)] in\nlet r_2 = Mf32_6[(shift_float32 a_0 2)] in\nlet r_3 = Mf32_6[(shift_float32 a_0 3)] in\nlet r_4 = Mf32_6[(shift_float32 a_0 4)] in\nlet r_5 = Mf32_6[(shift_float32 a_0 5)] in\nlet r_6 = Mf32_6[(shift_float32 a_0 6)] in\nlet r_7 = Mf32_6[(shift_float32 a_0 7)] in\nlet r_8 = Mf32_6[(shift_float32 a_0 8)] in\n(L_mult_RealRMat\n {\n F9_RealRMat_s_a00 = r_0 ;\n F9_RealRMat_s_a01 = r_1 ;\n F9_RealRMat_s_a02 = r_2 ;\n F9_RealRMat_s_a10 = r_3 ;\n F9_RealRMat_s_a11 = r_4 ;\n F9_RealRMat_s_a12 = r_5 ;\n F9_RealRMat_s_a20 = r_6 ;\n F9_RealRMat_s_a21 = r_7 ;\n F9_RealRMat_s_a22 = r_8\n }\n {\n F9_RealRMat_s_a00 = r_0 ;\n F9_RealRMat_s_a01 = r_3 ;\n F9_RealRMat_s_a02 = r_6 ;\n F9_RealRMat_s_a10 = r_1 ;\n F9_RealRMat_s_a11 = r_4 ;\n F9_RealRMat_s_a12 = r_7 ;\n F9_RealRMat_s_a20 = r_2 ;\n F9_RealRMat_s_a21 = r_5 ;\n F9_RealRMat_s_a22 = r_8\n })",
...@@ -41,7 +41,7 @@ ...@@ -41,7 +41,7 @@
"params": {}, "params": {},
"select": "select":
{ "select": "inside-step", { "select": "inside-step",
"at": 2, "at": 4,
"kind": "have", "kind": "have",
"occur": 0, "occur": 0,
"target": "let a_0 = (shiftfield_F6_FloatRMat_m rm_0) in\nlet r_0 = Mf32_6[(shift_float32 a_0 0)] in\nlet r_1 = Mf32_6[(shift_float32 a_0 1)] in\nlet r_2 = Mf32_6[(shift_float32 a_0 2)] in\nlet r_3 = Mf32_6[(shift_float32 a_0 3)] in\nlet r_4 = Mf32_6[(shift_float32 a_0 4)] in\nlet r_5 = Mf32_6[(shift_float32 a_0 5)] in\nlet r_6 = ((r_0*r_3)+(r_1*r_4)+(r_2*r_5)) in\nlet r_7 = Mf32_6[(shift_float32 a_0 6)] in\nlet r_8 = Mf32_6[(shift_float32 a_0 7)] in\nlet r_9 = Mf32_6[(shift_float32 a_0 8)] in\nlet r_10 = ((r_0*r_7)+(r_1*r_8)+(r_2*r_9)) in\nlet r_11 = ((r_3*r_7)+(r_4*r_8)+(r_5*r_9)) in\n(EqS9_RealRMat_s\n {\n F9_RealRMat_s_a00 = (r_0*r_0)+(r_1*r_1)+(r_2*r_2) ;\n F9_RealRMat_s_a01 = r_6 ;\n F9_RealRMat_s_a02 = r_10 ;\n F9_RealRMat_s_a10 = r_6 ;\n F9_RealRMat_s_a11 = (r_3*r_3)+(r_4*r_4)+(r_5*r_5) ;\n F9_RealRMat_s_a12 = r_11 ;\n F9_RealRMat_s_a20 = r_10 ;\n F9_RealRMat_s_a21 = r_11 ;\n F9_RealRMat_s_a22 = (r_7*r_7)+(r_8*r_8)+(r_9*r_9)\n } L_id_rmat)", "target": "let a_0 = (shiftfield_F6_FloatRMat_m rm_0) in\nlet r_0 = Mf32_6[(shift_float32 a_0 0)] in\nlet r_1 = Mf32_6[(shift_float32 a_0 1)] in\nlet r_2 = Mf32_6[(shift_float32 a_0 2)] in\nlet r_3 = Mf32_6[(shift_float32 a_0 3)] in\nlet r_4 = Mf32_6[(shift_float32 a_0 4)] in\nlet r_5 = Mf32_6[(shift_float32 a_0 5)] in\nlet r_6 = ((r_0*r_3)+(r_1*r_4)+(r_2*r_5)) in\nlet r_7 = Mf32_6[(shift_float32 a_0 6)] in\nlet r_8 = Mf32_6[(shift_float32 a_0 7)] in\nlet r_9 = Mf32_6[(shift_float32 a_0 8)] in\nlet r_10 = ((r_0*r_7)+(r_1*r_8)+(r_2*r_9)) in\nlet r_11 = ((r_3*r_7)+(r_4*r_8)+(r_5*r_9)) in\n(EqS9_RealRMat_s\n {\n F9_RealRMat_s_a00 = (r_0*r_0)+(r_1*r_1)+(r_2*r_2) ;\n F9_RealRMat_s_a01 = r_6 ;\n F9_RealRMat_s_a02 = r_10 ;\n F9_RealRMat_s_a10 = r_6 ;\n F9_RealRMat_s_a11 = (r_3*r_3)+(r_4*r_4)+(r_5*r_5) ;\n F9_RealRMat_s_a12 = r_11 ;\n F9_RealRMat_s_a20 = r_10 ;\n F9_RealRMat_s_a21 = r_11 ;\n F9_RealRMat_s_a22 = (r_7*r_7)+(r_8*r_8)+(r_9*r_9)\n } L_id_rmat)",
...@@ -53,7 +53,7 @@ ...@@ -53,7 +53,7 @@
"params": {}, "params": {},
"select": "select":
{ "select": "inside-step", { "select": "inside-step",
"at": 2, "at": 4,
"kind": "have", "kind": "have",
"occur": 0, "occur": 0,
"target": "L_id_rmat", "target": "L_id_rmat",
...@@ -62,4 +62,4 @@ ...@@ -62,4 +62,4 @@
{ "Unfold 'L_id_rmat'": { "Unfold 'L_id_rmat'":
[ { "prover": "CVC4:1.9-prerelease:strings+counterexamples", [ { "prover": "CVC4:1.9-prerelease:strings+counterexamples",
"verdict": "valid", "verdict": "valid",
"time": 0.54 } ] } } ] } } ] } } ] } } ] } } ] } } ] "time": 0.27 } ] } } ] } } ] } } ] } } ] } } ] } } ]
[ { "prover": "Z3:4.8.6:noBV", "verdict": "failed" },
{ "prover": "Z3:4.8.6:counterexamples", "verdict": "failed" },
{ "prover": "Z3:4.8.6", "verdict": "failed" },
{ "prover": "CVC4:1.9-prerelease:strings+counterexamples",
"verdict": "failed" },
{ "prover": "Alt-Ergo:2.3.3", "verdict": "failed" } ]
[ { "prover": "Z3:4.8.6:noBV", "verdict": "failed" },
{ "prover": "Z3:4.8.6:counterexamples", "verdict": "failed" },
{ "prover": "Z3:4.8.6", "verdict": "failed" },
{ "prover": "CVC4:1.9-prerelease:strings+counterexamples",
"verdict": "failed" },
{ "prover": "Alt-Ergo:2.3.3", "verdict": "failed" } ]
[ { "prover": "Z3:4.8.6:noBV", "verdict": "timeout", "time": 10. }, [ { "prover": "script", "verdict": "timeout", "time": 10. },
{ "prover": "Z3:4.8.6:counterexamples", "verdict": "timeout", "time": 10. }, { "header": "Definition", "tactic": "Wp.unfold", "params": {},
{ "prover": "Z3:4.8.6", "verdict": "timeout", "time": 10. }, "select": { "select": "clause-goal",
"target": "let a_0 = (shiftfield_F6_FloatRMat_m rm_0) in\nlet r_0 =\n (\\sqrt\n (1+Mf32_6[(shift_float32 a_0 0)]+Mf32_6[(shift_float32 a_0 4)]+\n Mf32_6[(shift_float32 a_0 8)])) in\nlet m_0 = Mf32_6[(shiftfield_F4_FloatQuat_qi q_1)->1/2*r_0] in\nlet r_1 = (2*r_0) in\nlet m_1 =\n m_0[(shiftfield_F4_FloatQuat_qx q_1)\n ->(m_0[(shift_float32 a_0 5)]-m_0[(shift_float32 a_0 7)]) div r_1] in\nlet m_2 =\n m_1[(shiftfield_F4_FloatQuat_qy q_1)\n ->(m_1[(shift_float32 a_0 6)]-m_1[(shift_float32 a_0 2)]) div r_1] in\n(P_unary_quaterion\n m_2[(shiftfield_F4_FloatQuat_qz q_1)\n ->(m_2[(shift_float32 a_0 1)]-m_2[(shift_float32 a_0 3)]) div r_1] q_1)",
"pattern": "P_unary_quaterion[=]$q[=]shiftfield_F4_FloatQuat_qz" },
"children": { "Unfold 'P_unary_quaterion'": [ { "header": "Definition",
"tactic": "Wp.unfold",
"params": {},
"select": { "select": "inside-goal",
"occur": 2,
"target": "(shift_float32 (shiftfield_F6_FloatRMat_m rm_0) 8)",
"pattern": "shift_float32shiftfield_F6_FloatRMat_m" },
"children": { "Unfold 'shift_float32'":
[ { "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": "CVC4:1.9-prerelease:strings+counterexamples", { "prover": "CVC4:1.9-prerelease:strings+counterexamples",
"verdict": "timeout", "time": 10. }, "verdict": "timeout",
{ "prover": "Alt-Ergo:2.3.3", "verdict": "timeout", "time": 10. } ] "time": 10. },
{ "prover": "Alt-Ergo:2.3.3",
"verdict": "timeout",
"time": 10. } ] } } ] } } ]
[ { "header": "Definition", "tactic": "Wp.unfold", "params": {}, [ { "header": "Definition", "tactic": "Wp.unfold", "params": {},
"select": { "select": "inside-step", "at": 2, "kind": "have", "occur": 0, "select": { "select": "inside-step", "at": 4, "kind": "have", "occur": 0,
"target": "(L_l_RMat_of_FloatRMat Mf32_6 rm_0)", "target": "(L_l_RMat_of_FloatRMat Mf32_6 rm_0)",
"pattern": "L_l_RMat_of_FloatRMat$Mf32$rm" }, "pattern": "L_l_RMat_of_FloatRMat$Mf32$rm" },
"children": { "Unfold 'L_l_RMat_of_FloatRMat'": [ { "header": "Definition", "children": { "Unfold 'L_l_RMat_of_FloatRMat'": [ { "header": "Definition",
"tactic": "Wp.unfold", "tactic": "Wp.unfold",
"params": {}, "params": {},
"select": { "select": "inside-step", "select": { "select": "inside-step",
"at": 2, "at": 4,
"kind": "have", "kind": "have",
"occur": 0, "occur": 0,
"target": "let a_0 = (shiftfield_F6_FloatRMat_m rm_0) in\n(P_rotation_matrix\n {\n F9_RealRMat_s_a00 = Mf32_6[(shift_float32 a_0 0)] ;\n F9_RealRMat_s_a01 = Mf32_6[(shift_float32 a_0 1)] ;\n F9_RealRMat_s_a02 = Mf32_6[(shift_float32 a_0 2)] ;\n F9_RealRMat_s_a10 = Mf32_6[(shift_float32 a_0 3)] ;\n F9_RealRMat_s_a11 = Mf32_6[(shift_float32 a_0 4)] ;\n F9_RealRMat_s_a12 = Mf32_6[(shift_float32 a_0 5)] ;\n F9_RealRMat_s_a20 = Mf32_6[(shift_float32 a_0 6)] ;\n F9_RealRMat_s_a21 = Mf32_6[(shift_float32 a_0 7)] ;\n F9_RealRMat_s_a22 = Mf32_6[(shift_float32 a_0 8)]\n })", "target": "let a_0 = (shiftfield_F6_FloatRMat_m rm_0) in\n(P_rotation_matrix\n {\n F9_RealRMat_s_a00 = Mf32_6[(shift_float32 a_0 0)] ;\n F9_RealRMat_s_a01 = Mf32_6[(shift_float32 a_0 1)] ;\n F9_RealRMat_s_a02 = Mf32_6[(shift_float32 a_0 2)] ;\n F9_RealRMat_s_a10 = Mf32_6[(shift_float32 a_0 3)] ;\n F9_RealRMat_s_a11 = Mf32_6[(shift_float32 a_0 4)] ;\n F9_RealRMat_s_a12 = Mf32_6[(shift_float32 a_0 5)] ;\n F9_RealRMat_s_a20 = Mf32_6[(shift_float32 a_0 6)] ;\n F9_RealRMat_s_a21 = Mf32_6[(shift_float32 a_0 7)] ;\n F9_RealRMat_s_a22 = Mf32_6[(shift_float32 a_0 8)]\n })",
...@@ -17,7 +17,7 @@ ...@@ -17,7 +17,7 @@
"params": {}, "params": {},
"select": "select":
{ "select": "inside-step", { "select": "inside-step",
"at": 2, "at": 4,
"kind": "have", "kind": "have",
"occur": 0, "occur": 0,
"target": "let a_0 = (shiftfield_F6_FloatRMat_m rm_0) in\n(L_transpose\n {\n F9_RealRMat_s_a00 = Mf32_6[(shift_float32 a_0 0)] ;\n F9_RealRMat_s_a01 = Mf32_6[(shift_float32 a_0 1)] ;\n F9_RealRMat_s_a02 = Mf32_6[(shift_float32 a_0 2)] ;\n F9_RealRMat_s_a10 = Mf32_6[(shift_float32 a_0 3)] ;\n F9_RealRMat_s_a11 = Mf32_6[(shift_float32 a_0 4)] ;\n F9_RealRMat_s_a12 = Mf32_6[(shift_float32 a_0 5)] ;\n F9_RealRMat_s_a20 = Mf32_6[(shift_float32 a_0 6)] ;\n F9_RealRMat_s_a21 = Mf32_6[(shift_float32 a_0 7)] ;\n F9_RealRMat_s_a22 = Mf32_6[(shift_float32 a_0 8)]\n })", "target": "let a_0 = (shiftfield_F6_FloatRMat_m rm_0) in\n(L_transpose\n {\n F9_RealRMat_s_a00 = Mf32_6[(shift_float32 a_0 0)] ;\n F9_RealRMat_s_a01 = Mf32_6[(shift_float32 a_0 1)] ;\n F9_RealRMat_s_a02 = Mf32_6[(shift_float32 a_0 2)] ;\n F9_RealRMat_s_a10 = Mf32_6[(shift_float32 a_0 3)] ;\n F9_RealRMat_s_a11 = Mf32_6[(shift_float32 a_0 4)] ;\n F9_RealRMat_s_a12 = Mf32_6[(shift_float32 a_0 5)] ;\n F9_RealRMat_s_a20 = Mf32_6[(shift_float32 a_0 6)] ;\n F9_RealRMat_s_a21 = Mf32_6[(shift_float32 a_0 7)] ;\n F9_RealRMat_s_a22 = Mf32_6[(shift_float32 a_0 8)]\n })",
...@@ -29,7 +29,7 @@ ...@@ -29,7 +29,7 @@
"params": {}, "params": {},
"select": "select":
{ "select": "inside-step", { "select": "inside-step",
"at": 2, "at": 4,
"kind": "have", "kind": "have",
"occur": 0, "occur": 0,
"target": "L_id_rmat", "target": "L_id_rmat",
...@@ -41,7 +41,7 @@ ...@@ -41,7 +41,7 @@
"params": {}, "params": {},
"select": "select":
{ "select": "inside-step", { "select": "inside-step",
"at": 2, "at": 4,
"kind": "have", "kind": "have",
"occur": 0, "occur": 0,
"target": "let a_0 = (shiftfield_F6_FloatRMat_m rm_0) in\nlet r_0 = Mf32_6[(shift_float32 a_0 0)] in\nlet r_1 = Mf32_6[(shift_float32 a_0 1)] in\nlet r_2 = Mf32_6[(shift_float32 a_0 2)] in\nlet r_3 = Mf32_6[(shift_float32 a_0 3)] in\nlet r_4 = Mf32_6[(shift_float32 a_0 4)] in\nlet r_5 = Mf32_6[(shift_float32 a_0 5)] in\nlet r_6 = Mf32_6[(shift_float32 a_0 6)] in\nlet r_7 = Mf32_6[(shift_float32 a_0 7)] in\nlet r_8 = Mf32_6[(shift_float32 a_0 8)] in\n(L_mult_RealRMat\n {\n F9_RealRMat_s_a00 = r_0 ;\n F9_RealRMat_s_a01 = r_1 ;\n F9_RealRMat_s_a02 = r_2 ;\n F9_RealRMat_s_a10 = r_3 ;\n F9_RealRMat_s_a11 = r_4 ;\n F9_RealRMat_s_a12 = r_5 ;\n F9_RealRMat_s_a20 = r_6 ;\n F9_RealRMat_s_a21 = r_7 ;\n F9_RealRMat_s_a22 = r_8\n }\n {\n F9_RealRMat_s_a00 = r_0 ;\n F9_RealRMat_s_a01 = r_3 ;\n F9_RealRMat_s_a02 = r_6 ;\n F9_RealRMat_s_a10 = r_1 ;\n F9_RealRMat_s_a11 = r_4 ;\n F9_RealRMat_s_a12 = r_7 ;\n F9_RealRMat_s_a20 = r_2 ;\n F9_RealRMat_s_a21 = r_5 ;\n F9_RealRMat_s_a22 = r_8\n })", "target": "let a_0 = (shiftfield_F6_FloatRMat_m rm_0) in\nlet r_0 = Mf32_6[(shift_float32 a_0 0)] in\nlet r_1 = Mf32_6[(shift_float32 a_0 1)] in\nlet r_2 = Mf32_6[(shift_float32 a_0 2)] in\nlet r_3 = Mf32_6[(shift_float32 a_0 3)] in\nlet r_4 = Mf32_6[(shift_float32 a_0 4)] in\nlet r_5 = Mf32_6[(shift_float32 a_0 5)] in\nlet r_6 = Mf32_6[(shift_float32 a_0 6)] in\nlet r_7 = Mf32_6[(shift_float32 a_0 7)] in\nlet r_8 = Mf32_6[(shift_float32 a_0 8)] in\n(L_mult_RealRMat\n {\n F9_RealRMat_s_a00 = r_0 ;\n F9_RealRMat_s_a01 = r_1 ;\n F9_RealRMat_s_a02 = r_2 ;\n F9_RealRMat_s_a10 = r_3 ;\n F9_RealRMat_s_a11 = r_4 ;\n F9_RealRMat_s_a12 = r_5 ;\n F9_RealRMat_s_a20 = r_6 ;\n F9_RealRMat_s_a21 = r_7 ;\n F9_RealRMat_s_a22 = r_8\n }\n {\n F9_RealRMat_s_a00 = r_0 ;\n F9_RealRMat_s_a01 = r_3 ;\n F9_RealRMat_s_a02 = r_6 ;\n F9_RealRMat_s_a10 = r_1 ;\n F9_RealRMat_s_a11 = r_4 ;\n F9_RealRMat_s_a12 = r_7 ;\n F9_RealRMat_s_a20 = r_2 ;\n F9_RealRMat_s_a21 = r_5 ;\n F9_RealRMat_s_a22 = r_8\n })",
...@@ -53,7 +53,7 @@ ...@@ -53,7 +53,7 @@
"params": {}, "params": {},
"select": "select":
{ "select": "inside-step", { "select": "inside-step",
"at": 2, "at": 4,
"kind": "have", "kind": "have",
"occur": 0, "occur": 0,
"target": "let a_0 = (shiftfield_F6_FloatRMat_m rm_0) in\nlet r_0 = Mf32_6[(shift_float32 a_0 0)] in\nlet r_1 = Mf32_6[(shift_float32 a_0 1)] in\nlet r_2 = Mf32_6[(shift_float32 a_0 2)] in\nlet r_3 = Mf32_6[(shift_float32 a_0 3)] in\nlet r_4 = Mf32_6[(shift_float32 a_0 4)] in\nlet r_5 = Mf32_6[(shift_float32 a_0 5)] in\nlet r_6 = ((r_0*r_3)+(r_1*r_4)+(r_2*r_5)) in\nlet r_7 = Mf32_6[(shift_float32 a_0 6)] in\nlet r_8 = Mf32_6[(shift_float32 a_0 7)] in\nlet r_9 = Mf32_6[(shift_float32 a_0 8)] in\nlet r_10 = ((r_0*r_7)+(r_1*r_8)+(r_2*r_9)) in\nlet r_11 = ((r_3*r_7)+(r_4*r_8)+(r_5*r_9)) in\n(EqS9_RealRMat_s\n {\n F9_RealRMat_s_a00 = (r_0*r_0)+(r_1*r_1)+(r_2*r_2) ;\n F9_RealRMat_s_a01 = r_6 ;\n F9_RealRMat_s_a02 = r_10 ;\n F9_RealRMat_s_a10 = r_6 ;\n F9_RealRMat_s_a11 = (r_3*r_3)+(r_4*r_4)+(r_5*r_5) ;\n F9_RealRMat_s_a12 = r_11 ;\n F9_RealRMat_s_a20 = r_10 ;\n F9_RealRMat_s_a21 = r_11 ;\n F9_RealRMat_s_a22 = (r_7*r_7)+(r_8*r_8)+(r_9*r_9)\n }\n {\n F9_RealRMat_s_a00 = 1 ;\n F9_RealRMat_s_a01 = 0 ;\n F9_RealRMat_s_a02 = 0 ;\n F9_RealRMat_s_a10 = 0 ;\n F9_RealRMat_s_a11 = 1 ;\n F9_RealRMat_s_a12 = 0 ;\n F9_RealRMat_s_a20 = 0 ;\n F9_RealRMat_s_a21 = 0 ;\n F9_RealRMat_s_a22 = 1\n })", "target": "let a_0 = (shiftfield_F6_FloatRMat_m rm_0) in\nlet r_0 = Mf32_6[(shift_float32 a_0 0)] in\nlet r_1 = Mf32_6[(shift_float32 a_0 1)] in\nlet r_2 = Mf32_6[(shift_float32 a_0 2)] in\nlet r_3 = Mf32_6[(shift_float32 a_0 3)] in\nlet r_4 = Mf32_6[(shift_float32 a_0 4)] in\nlet r_5 = Mf32_6[(shift_float32 a_0 5)] in\nlet r_6 = ((r_0*r_3)+(r_1*r_4)+(r_2*r_5)) in\nlet r_7 = Mf32_6[(shift_float32 a_0 6)] in\nlet r_8 = Mf32_6[(shift_float32 a_0 7)] in\nlet r_9 = Mf32_6[(shift_float32 a_0 8)] in\nlet r_10 = ((r_0*r_7)+(r_1*r_8)+(r_2*r_9)) in\nlet r_11 = ((r_3*r_7)+(r_4*r_8)+(r_5*r_9)) in\n(EqS9_RealRMat_s\n {\n F9_RealRMat_s_a00 = (r_0*r_0)+(r_1*r_1)+(r_2*r_2) ;\n F9_RealRMat_s_a01 = r_6 ;\n F9_RealRMat_s_a02 = r_10 ;\n F9_RealRMat_s_a10 = r_6 ;\n F9_RealRMat_s_a11 = (r_3*r_3)+(r_4*r_4)+(r_5*r_5) ;\n F9_RealRMat_s_a12 = r_11 ;\n F9_RealRMat_s_a20 = r_10 ;\n F9_RealRMat_s_a21 = r_11 ;\n F9_RealRMat_s_a22 = (r_7*r_7)+(r_8*r_8)+(r_9*r_9)\n }\n {\n F9_RealRMat_s_a00 = 1 ;\n F9_RealRMat_s_a01 = 0 ;\n F9_RealRMat_s_a02 = 0 ;\n F9_RealRMat_s_a10 = 0 ;\n F9_RealRMat_s_a11 = 1 ;\n F9_RealRMat_s_a12 = 0 ;\n F9_RealRMat_s_a20 = 0 ;\n F9_RealRMat_s_a21 = 0 ;\n F9_RealRMat_s_a22 = 1\n })",
...@@ -62,5 +62,5 @@ ...@@ -62,5 +62,5 @@
{ "Unfold 'EqS9_RealRMat_s'": { "Unfold 'EqS9_RealRMat_s'":
[ { "prover": "Z3:4.8.6", [ { "prover": "Z3:4.8.6",
"verdict": "valid", "verdict": "valid",
"time": 1.57, "time": 1.6,
"steps": 3136482 } ] } } ] } } ] } } ] } } ] } } ] } } ] "steps": 3136482 } ] } } ] } } ] } } ] } } ] } } ] } } ]
[ { "prover": "Z3:4.8.6:noBV", "verdict": "failed" },
{ "prover": "Z3:4.8.6:counterexamples", "verdict": "failed" },
{ "prover": "Z3:4.8.6", "verdict": "failed" },
{ "prover": "CVC4:1.9-prerelease:strings+counterexamples",
"verdict": "failed" },
{ "prover": "Alt-Ergo:2.3.3", "verdict": "failed" } ]
[ { "prover": "Z3:4.8.6:noBV", "verdict": "failed" },
{ "prover": "Z3:4.8.6:counterexamples", "verdict": "failed" },
{ "prover": "Z3:4.8.6", "verdict": "failed" },
{ "prover": "CVC4:1.9-prerelease:strings+counterexamples",
"verdict": "failed" },
{ "prover": "Alt-Ergo:2.3.3", "verdict": "failed" } ]
[ { "prover": "Z3:4.8.6:noBV", "verdict": "failed" },
{ "prover": "Z3:4.8.6:counterexamples", "verdict": "failed" },
{ "prover": "Z3:4.8.6", "verdict": "failed" },
{ "prover": "CVC4:1.9-prerelease:strings+counterexamples",
"verdict": "failed" },
{ "prover": "Alt-Ergo:2.3.3", "verdict": "failed" } ]
[ { "prover": "Z3:4.8.6:noBV", "verdict": "failed" },
{ "prover": "Z3:4.8.6:counterexamples", "verdict": "failed" },
{ "prover": "Z3:4.8.6", "verdict": "failed" },
{ "prover": "CVC4:1.9-prerelease:strings+counterexamples",
"verdict": "failed" },
{ "prover": "Alt-Ergo:2.3.3", "verdict": "failed" } ]
[ { "prover": "Z3:4.8.6:noBV", "verdict": "failed" },
{ "prover": "Z3:4.8.6:counterexamples", "verdict": "failed" },
{ "prover": "Z3:4.8.6", "verdict": "failed" },
{ "prover": "CVC4:1.9-prerelease:strings+counterexamples",
"verdict": "failed" },
{ "prover": "Alt-Ergo:2.3.3", "verdict": "failed" } ]
[ { "prover": "Z3:4.8.6:noBV", "verdict": "failed" },
{ "prover": "Z3:4.8.6:counterexamples", "verdict": "failed" },
{ "prover": "Z3:4.8.6", "verdict": "failed" },
{ "prover": "CVC4:1.9-prerelease:strings+counterexamples",
"verdict": "failed" },
{ "prover": "Alt-Ergo:2.3.3", "verdict": "failed" } ]
[ { "prover": "Z3:4.8.6:noBV", "verdict": "failed" },
{ "prover": "Z3:4.8.6:counterexamples", "verdict": "failed" },
{ "prover": "Z3:4.8.6", "verdict": "failed" },
{ "prover": "CVC4:1.9-prerelease:strings+counterexamples",
"verdict": "failed" },
{ "prover": "Alt-Ergo:2.3.3", "verdict": "failed" } ]
...@@ -66,7 +66,7 @@ ...@@ -66,7 +66,7 @@
"params": {}, "params": {},
"select": "select":
{ "select": "inside-step", { "select": "inside-step",
"at": 3, "at": 6,
"kind": "have", "kind": "have",
"occur": 0, "occur": 0,
"target": "(L_trace_2_ Mf32_2 rm_0)", "target": "(L_trace_2_ Mf32_2 rm_0)",
...@@ -78,7 +78,7 @@ ...@@ -78,7 +78,7 @@
"params": {}, "params": {},
"select": "select":
{ "select": "inside-step", { "select": "inside-step",
"at": 3, "at": 6,
"kind": "have", "kind": "have",
"occur": 0, "occur": 0,
"target": "(L_trace_1_ (L_l_RMat_of_FloatRMat Mf32_2 rm_0))", "target": "(L_trace_1_ (L_l_RMat_of_FloatRMat Mf32_2 rm_0))",
...@@ -90,7 +90,7 @@ ...@@ -90,7 +90,7 @@
"params": {}, "params": {},
"select": "select":
{ "select": "inside-step", { "select": "inside-step",
"at": 3, "at": 4,
"kind": "have", "kind": "have",
"occur": 0, "occur": 0,
"target": "(L_l_RMat_of_FloatRMat Mf32_2 rm_0)", "target": "(L_l_RMat_of_FloatRMat Mf32_2 rm_0)",
...@@ -99,5 +99,5 @@ ...@@ -99,5 +99,5 @@
{ "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.8543, "time": 4.7685,
"steps": 1495 } ] } } ] } } ] } } ] } } ] } } ] } } ] } } ] } } ] } } ] } } ] "steps": 1358 } ] } } ] } } ] } } ] } } ] } } ] } } ] } } ] } } ] } } ] } } ]
...@@ -3,9 +3,9 @@ ...@@ -3,9 +3,9 @@
"target": "(separated rm_0 9 q_0 4)", "target": "(separated rm_0 9 q_0 4)",
"pattern": "separated$rm9$q4" }, "pattern": "separated$rm9$q4" },
"children": { "WrongBase": [ { "prover": "CVC4:1.9-prerelease:strings+counterexamples", "children": { "WrongBase": [ { "prover": "CVC4:1.9-prerelease:strings+counterexamples",
"verdict": "valid", "time": 1. } ], "verdict": "valid", "time": 0.67 } ],
"OnLeft": [ { "prover": "CVC4:1.9-prerelease:strings+counterexamples", "OnLeft": [ { "prover": "CVC4:1.9-prerelease:strings+counterexamples",
"verdict": "valid", "time": 4.45 } ], "verdict": "valid", "time": 4.1 } ],
"OnRight": [ { "prover": "CVC4:1.9-prerelease:strings+counterexamples", "OnRight": [ { "prover": "CVC4:1.9-prerelease:strings+counterexamples",
"verdict": "valid", "time": 4.22 } ], "verdict": "valid", "time": 3.74 } ],
"OverLap": [ { "prover": "qed", "verdict": "valid" } ] } } ] "OverLap": [ { "prover": "qed", "verdict": "valid" } ] } } ]
...@@ -3,9 +3,9 @@ ...@@ -3,9 +3,9 @@
"target": "(separated rm_0 9 q_0 4)", "target": "(separated rm_0 9 q_0 4)",
"pattern": "separated$rm9$q4" }, "pattern": "separated$rm9$q4" },
"children": { "WrongBase": [ { "prover": "CVC4:1.9-prerelease:strings+counterexamples",