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

Adding proof scripts

parent 0c0d1cd7
[ { "header": "Split", "tactic": "Wp.split", "params": {},
"select": { "select": "clause-step", "at": 9, "kind": "branch",
"target": "let a_0 = (shiftfield_F6_FloatRMat_m rm_0) in\n0<\n(Mf32_1[(shift_float32 a_0 0)]+Mf32_1[(shift_float32 a_0 4)]+\n Mf32_1[(shift_float32 a_0 8)])",
"pattern": "<0+[][][]$Mf32shift_float32$Mf32" },
"children": { "Then": [ { "prover": "Alt-Ergo:2.3.3", "verdict": "valid",
"time": 1.5453, "steps": 308 } ],
"Else": [ { "prover": "Alt-Ergo:2.3.3", "verdict": "valid",
"time": 7.9094, "steps": 539 } ] } } ]
[ { "prover": "CVC4:1.9-prerelease:strings+counterexamples",
"verdict": "timeout", "time": 10. },
{ "prover": "Alt-Ergo:2.3.3", "verdict": "timeout", "time": 10. },
{ "prover": "script", "verdict": "timeout", "time": 10. },
{ "header": "Definition", "tactic": "Wp.unfold", "params": {},
"select": { "select": "clause-goal",
"target": "(P_unary_quaterion Mf32_0 q_0)",
"pattern": "P_unary_quaterion$Mf32$q" },
"children": { "Unfold 'P_unary_quaterion'": [ { "prover": "CVC4:1.9-prerelease:strings+counterexamples",
"verdict": "timeout",
"time": 10. },
{ "prover": "Alt-Ergo:2.3.3",
"verdict": "timeout",
"time": 10. },
{ "header": "Definition",
"tactic": "Wp.unfold",
"params": {},
"select": { "select": "inside-step",
"at": 2,
"kind": "have",
"occur": 0,
"target": "(P_rotation_matrix (L_l_RMat_of_FloatRMat Mf32_27 rm_0))",
"pattern": "P_rotation_matrixL_l_RMat_of_FloatRMat" },
"children": { "Unfold 'P_rotation_matrix'":
[ { "header": "Definition",
"tactic": "Wp.unfold",
"params": {},
"select":
{ "select": "inside-step",
"at": 2,
"kind": "have",
"occur": 0,
"target": "(L_transpose (L_l_RMat_of_FloatRMat Mf32_27 rm_0))",
"pattern": "L_transposeL_l_RMat_of_FloatRMat" },
"children":
{ "Unfold 'L_transpose'":
[ { "header": "Definition",
"tactic": "Wp.unfold",
"params": {},
"select":
{ "select": "inside-step",
"at": 2,
"kind": "have",
"occur": 0,
"target": "let a_0 = (L_l_RMat_of_FloatRMat Mf32_27 rm_0) in\n(L_mult_RealRMat a_0\n {\n a_0 with\n F9_RealRMat_s_a01 = a_0.F9_RealRMat_s_a10 ;\n F9_RealRMat_s_a02 = a_0.F9_RealRMat_s_a20 ;\n F9_RealRMat_s_a10 = a_0.F9_RealRMat_s_a01 ;\n F9_RealRMat_s_a12 = a_0.F9_RealRMat_s_a21 ;\n F9_RealRMat_s_a20 = a_0.F9_RealRMat_s_a02 ;\n F9_RealRMat_s_a21 = a_0.F9_RealRMat_s_a12\n })",
"pattern": "L_mult_RealRMatL_l_RMat_of_FloatRMat" },
"children":
{ "Unfold 'L_mult_RealRMat'":
[ { "header": "Definition",
"tactic": "Wp.unfold",
"params": {},
"select":
{ "select": "inside-step",
"at": 2,
"kind": "have",
"occur": 0,
"target": "let a_0 = (L_l_RMat_of_FloatRMat Mf32_27 rm_0) in\nlet r_0 = a_0.F9_RealRMat_s_a00 in\nlet r_1 = a_0.F9_RealRMat_s_a01 in\nlet r_2 = a_0.F9_RealRMat_s_a02 in\nlet r_3 = a_0.F9_RealRMat_s_a10 in\nlet r_4 = a_0.F9_RealRMat_s_a11 in\nlet r_5 = a_0.F9_RealRMat_s_a12 in\nlet r_6 = ((r_0*r_3)+(r_1*r_4)+(r_2*r_5)) in\nlet r_7 = a_0.F9_RealRMat_s_a20 in\nlet r_8 = a_0.F9_RealRMat_s_a21 in\nlet r_9 = a_0.F9_RealRMat_s_a22 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)",
"pattern": "EqS9_RealRMat_s{RealRMat_s}L_id_rmat" },
"children":
{ "Unfold 'EqS9_RealRMat_s'":
[ { "header": "Split",
"tactic": "Wp.split",
"params": {},
"select":
{ "select": "clause-step",
"at": 8,
"kind": "branch",
"target": "let a_0 = (shiftfield_F6_FloatRMat_m rm_0) in\n0<\n(Mf32_27[(shift_float32 a_0 0)]+Mf32_27[(shift_float32 a_0 4)]+\n Mf32_27[(shift_float32 a_0 8)])",
"pattern": "<0+[][][]$Mf32shift_float32$Mf32" },
"children":
{ "Then":
[ { "prover": "Alt-Ergo:2.3.3",
"verdict": "timeout",
"time": 10. } ],
"Else": [] } } ] } } ] } } ] } } ] } } ] } } ]
[ { "prover": "CVC4:1.9-prerelease:strings+counterexamples",
"verdict": "timeout", "time": 10. },
{ "prover": "Alt-Ergo:2.3.3", "verdict": "timeout", "time": 10. } ]
[ { "header": "Separated", "tactic": "Wp.separated", "params": {},
"select": { "select": "inside-step", "at": 2, "kind": "have", "occur": 0,
"target": "(separated rm_0 9 q_0 4)",
"pattern": "separated$rm9$q4" },
"children": { "WrongBase": [ { "prover": "CVC4:1.9-prerelease:strings+counterexamples",
"verdict": "valid", "time": 0.68 } ],
"OnLeft": [ { "prover": "CVC4:1.9-prerelease:strings+counterexamples",
"verdict": "valid", "time": 3.67 } ],
"OnRight": [ { "prover": "CVC4:1.9-prerelease:strings+counterexamples",
"verdict": "valid", "time": 3.55 } ],
"OverLap": [ { "prover": "qed", "verdict": "valid" } ] } } ]
[ { "header": "Separated", "tactic": "Wp.separated", "params": {},
"select": { "select": "inside-step", "at": 2, "kind": "have", "occur": 0,
"target": "(separated rm_0 9 q_0 4)",
"pattern": "separated$rm9$q4" },
"children": { "WrongBase": [ { "prover": "CVC4:1.9-prerelease:strings+counterexamples",
"verdict": "valid", "time": 3.02 } ],
"OnLeft": [ { "prover": "CVC4:1.9-prerelease:strings+counterexamples",
"verdict": "valid", "time": 4.17 } ],
"OnRight": [ { "prover": "CVC4:1.9-prerelease:strings+counterexamples",
"verdict": "valid", "time": 4.15 } ],
"OverLap": [ { "prover": "qed", "verdict": "valid" } ] } } ]
[ { "header": "Separated", "tactic": "Wp.separated", "params": {},
"select": { "select": "inside-step", "at": 2, "kind": "have", "occur": 0,
"target": "(separated rm_0 9 q_0 4)",
"pattern": "separated$rm9$q4" },
"children": { "WrongBase": [ { "prover": "Alt-Ergo:2.3.3",
"verdict": "valid", "time": 8.8322,
"steps": 114 } ],
"OnLeft": [ { "header": "Definition",
"tactic": "Wp.unfold", "params": {},
"select": { "select": "inside-step",
"at": 3, "kind": "have",
"occur": 0,
"target": "(P_unary_quaterion Mf32_1 q_0)",
"pattern": "P_unary_quaterion$Mf32$q" },
"children": { "Unfold 'P_unary_quaterion'":
[ { "prover": "CVC4:1.9-prerelease:strings+counterexamples",
"verdict": "valid",
"time": 5.6 } ] } } ],
"OnRight": [ { "header": "Definition",
"tactic": "Wp.unfold", "params": {},
"select": { "select": "inside-step",
"at": 3, "kind": "have",
"occur": 0,
"target": "(P_unary_quaterion Mf32_1 q_0)",
"pattern": "P_unary_quaterion$Mf32$q" },
"children": { "Unfold 'P_unary_quaterion'":
[ { "prover": "CVC4:1.9-prerelease:strings+counterexamples",
"verdict": "valid",
"time": 5.76 } ] } } ],
"OverLap": [ { "prover": "qed", "verdict": "valid" } ] } } ]
[ { "header": "Separated", "tactic": "Wp.separated", "params": {},
"select": { "select": "inside-step", "at": 2, "kind": "have", "occur": 0,
"target": "(separated rm_0 9 q_0 4)",
"pattern": "separated$rm9$q4" },
"children": { "WrongBase": [ { "prover": "CVC4:1.9-prerelease:strings+counterexamples",
"verdict": "valid", "time": 5.75 } ],
"OnLeft": [ { "prover": "CVC4:1.9-prerelease:strings+counterexamples",
"verdict": "valid", "time": 12.59 } ],
"OnRight": [ { "prover": "CVC4:1.9-prerelease:strings+counterexamples",
"verdict": "valid", "time": 11.58 } ],
"OverLap": [ { "prover": "qed", "verdict": "valid" } ] } } ]
This diff is collapsed.
[ { "header": "Definition", "tactic": "Wp.unfold", "params": {},
"select": { "select": "clause-step", "at": 31, "kind": "have",
"target": "let a_1 = Mptr_0[(shift_PTR o_0 i_0)] in\n(P_rvalid_int_mat_3_ Malloc_0 Mptr_0\n (havoc Mint_undef_0 Mint_9 (shift_sint32 a_1 0) l_3)[(shift_sint32 a_1 j_0)\n ->v_0] a_0 m_2 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": 6.82 } ] } } ]
[ { "header": "Definition", "tactic": "Wp.unfold", "params": {},
"select": { "select": "clause-step", "at": 30, "kind": "have",
"target": "let a_0 = Mptr_0[(shift_PTR o_0 i_0)] in\n(P_rvalid_int_mat_3_ Malloc_0 Mptr_0\n (havoc Mint_undef_0 Mint_9 (shift_sint32 a_0 0) l_3)[(shift_sint32 a_0 j_0)\n ->v_0] b_0 n_0 l_3\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": 0.79 } ] } } ]
[ { "header": "Definition", "tactic": "Wp.unfold", "params": {},
"select": { "select": "clause-step", "at": 3, "kind": "have",
"target": "(P_rvalid_bound_Int32Quat Malloc_0 Mint_0 q_0 23170)",
"pattern": "P_rvalid_bound_Int32Quat$Malloc$Mint" },
"children": { "Unfold 'P_rvalid_bound_Int32Quat'": [ { "prover": "Alt-Ergo:2.3.3",
"verdict": "valid",
"time": 0.0764,
"steps": 264 } ] } } ]
[ { "header": "Overflow", "tactic": "Wp.overflow", "params": {},
"select": { "select": "inside-goal", "occur": 0,
"target": "(to_sint32 (2147483647 div n_0))",
"pattern": "to_sint32/2147483647$n" },
"children": { "In-Range": [ { "prover": "Alt-Ergo:2.3.3",
"verdict": "valid", "time": 0.016,
"steps": 100 } ],
"No-Overflow": [ { "prover": "Alt-Ergo:2.3.3",
"verdict": "valid", "time": 0.0182,
"steps": 28 } ] } } ]
[ { "header": "Overflow", "tactic": "Wp.overflow", "params": {},
"select": { "select": "inside-goal", "occur": 0,
"target": "(to_sint32 (2147483647 div n_0))",
"pattern": "to_sint32/2147483647$n" },
"children": { "In-Range": [ { "prover": "Alt-Ergo:2.3.3",
"verdict": "valid", "time": 0.0296,
"steps": 85 } ],
"No-Overflow": [ { "prover": "CVC4:1.9-prerelease:strings+counterexamples",
"verdict": "valid", "time": 0.1 } ] } } ]
[ { "prover": "CVC4:1.9-prerelease:strings+counterexamples",
"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. } ]
[ { "prover": "CVC4:1.9-prerelease:strings+counterexamples",
"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. } ]
[ { "prover": "CVC4:1.9-prerelease:strings+counterexamples",
"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. } ]
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