Skip to content

GitLab

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

Proof for quat to rmat conversion

parent 31c488d6
Expand all Hide whitespace changes
Inline Side-by-side
Showing with 1837 additions and 742 deletions
sw/airborne/.frama-c/wp/script/float_quat_of_rmat_a00_max_ensures.json
View file @ b0a63524
......@@ -18,7 +18,7 @@
"select":
{ "select": "inside-goal",
"occur": 0,
"target": "let a_0 = (shiftfield_F9_FloatRMat_m rm_0) in\n(L_transpose\n {\n F12_RealRMat_s_a00 = Mf32_0[(shift_float32 a_0 0)] ;\n F12_RealRMat_s_a01 = Mf32_0[(shift_float32 a_0 1)] ;\n F12_RealRMat_s_a02 = Mf32_0[(shift_float32 a_0 2)] ;\n F12_RealRMat_s_a10 = Mf32_0[(shift_float32 a_0 3)] ;\n F12_RealRMat_s_a11 = Mf32_0[(shift_float32 a_0 4)] ;\n F12_RealRMat_s_a12 = Mf32_0[(shift_float32 a_0 5)] ;\n F12_RealRMat_s_a20 = Mf32_0[(shift_float32 a_0 6)] ;\n F12_RealRMat_s_a21 = Mf32_0[(shift_float32 a_0 7)] ;\n F12_RealRMat_s_a22 = Mf32_0[(shift_float32 a_0 8)]\n })",
"target": "let a_0 = (shiftfield_F9_FloatRMat_m rm_0) in\n(L_transpose\n {\n F13_RealRMat_s_a00 = Mf32_0[(shift_float32 a_0 0)] ;\n F13_RealRMat_s_a01 = Mf32_0[(shift_float32 a_0 1)] ;\n F13_RealRMat_s_a02 = Mf32_0[(shift_float32 a_0 2)] ;\n F13_RealRMat_s_a10 = Mf32_0[(shift_float32 a_0 3)] ;\n F13_RealRMat_s_a11 = Mf32_0[(shift_float32 a_0 4)] ;\n F13_RealRMat_s_a12 = Mf32_0[(shift_float32 a_0 5)] ;\n F13_RealRMat_s_a20 = Mf32_0[(shift_float32 a_0 6)] ;\n F13_RealRMat_s_a21 = Mf32_0[(shift_float32 a_0 7)] ;\n F13_RealRMat_s_a22 = Mf32_0[(shift_float32 a_0 8)]\n })",
"pattern": "L_transpose{RealRMat_s}[][][][][]" },
"children":
{ "Unfold 'L_transpose'":
......@@ -28,7 +28,7 @@
"select":
{ "select": "inside-goal",
"occur": 0,
"target": "let a_0 = (shiftfield_F9_FloatRMat_m rm_0) in\n(L_l_FloatQuat_of_RMat_0_max_1_\n {\n F12_RealRMat_s_a00 = Mf32_0[(shift_float32 a_0 0)] ;\n F12_RealRMat_s_a01 = Mf32_0[(shift_float32 a_0 3)] ;\n F12_RealRMat_s_a02 = Mf32_0[(shift_float32 a_0 6)] ;\n F12_RealRMat_s_a10 = Mf32_0[(shift_float32 a_0 1)] ;\n F12_RealRMat_s_a11 = Mf32_0[(shift_float32 a_0 4)] ;\n F12_RealRMat_s_a12 = Mf32_0[(shift_float32 a_0 7)] ;\n F12_RealRMat_s_a20 = Mf32_0[(shift_float32 a_0 2)] ;\n F12_RealRMat_s_a21 = Mf32_0[(shift_float32 a_0 5)] ;\n F12_RealRMat_s_a22 = Mf32_0[(shift_float32 a_0 8)]\n })",
"target": "let a_0 = (shiftfield_F9_FloatRMat_m rm_0) in\n(L_l_FloatQuat_of_RMat_0_max_1_\n {\n F13_RealRMat_s_a00 = Mf32_0[(shift_float32 a_0 0)] ;\n F13_RealRMat_s_a01 = Mf32_0[(shift_float32 a_0 3)] ;\n F13_RealRMat_s_a02 = Mf32_0[(shift_float32 a_0 6)] ;\n F13_RealRMat_s_a10 = Mf32_0[(shift_float32 a_0 1)] ;\n F13_RealRMat_s_a11 = Mf32_0[(shift_float32 a_0 4)] ;\n F13_RealRMat_s_a12 = Mf32_0[(shift_float32 a_0 7)] ;\n F13_RealRMat_s_a20 = Mf32_0[(shift_float32 a_0 2)] ;\n F13_RealRMat_s_a21 = Mf32_0[(shift_float32 a_0 5)] ;\n F13_RealRMat_s_a22 = Mf32_0[(shift_float32 a_0 8)]\n })",
"pattern": "L_l_FloatQuat_of_RMat_0_max_1_{RealRMat_s}" },
"children":
{ "Unfold 'L_l_FloatQuat_of_RMat_0_max_1_'":
......@@ -47,47 +47,27 @@
"params": {},
"select":
{ "select": "clause-goal",
"target": "let a_0 = (shiftfield_F9_FloatRMat_m rm_0) in\nlet r_0 =\n (\\sqrt\n (1+Mf32_0[(shift_float32 a_0 0)]-Mf32_0[(shift_float32 a_0 4)]-\n Mf32_0[(shift_float32 a_0 8)])) in\nlet r_1 = (2*r_0) in\n(EqS13_RealQuat_s\n {\n F13_RealQuat_s_qi =\n (Mf32_0[(shift_float32 a_0 5)]-Mf32_0[(shift_float32 a_0 7)]) div r_1 ;\n F13_RealQuat_s_qx = 1/2*r_0 ;\n F13_RealQuat_s_qy =\n (Mf32_0[(shift_float32 a_0 1)]+Mf32_0[(shift_float32 a_0 3)]) div r_1 ;\n F13_RealQuat_s_qz =\n (Mf32_0[(shift_float32 a_0 2)]+Mf32_0[(shift_float32 a_0 6)]) div r_1\n }\n {\n F13_RealQuat_s_qi = Mf32_0[(shiftfield_F7_FloatQuat_qi q_0)] ;\n F13_RealQuat_s_qx = Mf32_0[(shiftfield_F7_FloatQuat_qx q_0)] ;\n F13_RealQuat_s_qy = Mf32_0[(shiftfield_F7_FloatQuat_qy q_0)] ;\n F13_RealQuat_s_qz = Mf32_0[(shiftfield_F7_FloatQuat_qz q_0)]\n })",
"pattern": "EqS13_RealQuat_s{RealQuat_s}{RealQuat_s}" },
"target": "let a_0 = (shiftfield_F9_FloatRMat_m rm_0) in\nlet r_0 =\n (\\sqrt\n (1+Mf32_0[(shift_float32 a_0 0)]-Mf32_0[(shift_float32 a_0 4)]-\n Mf32_0[(shift_float32 a_0 8)])) in\nlet r_1 = (2*r_0) in\n(EqS14_RealQuat_s\n {\n F14_RealQuat_s_qi =\n (Mf32_0[(shift_float32 a_0 5)]-Mf32_0[(shift_float32 a_0 7)]) div r_1 ;\n F14_RealQuat_s_qx = 1/2*r_0 ;\n F14_RealQuat_s_qy =\n (Mf32_0[(shift_float32 a_0 1)]+Mf32_0[(shift_float32 a_0 3)]) div r_1 ;\n F14_RealQuat_s_qz =\n (Mf32_0[(shift_float32 a_0 2)]+Mf32_0[(shift_float32 a_0 6)]) div r_1\n }\n {\n F14_RealQuat_s_qi = Mf32_0[(shiftfield_F7_FloatQuat_qi q_0)] ;\n F14_RealQuat_s_qx = Mf32_0[(shiftfield_F7_FloatQuat_qx q_0)] ;\n F14_RealQuat_s_qy = Mf32_0[(shiftfield_F7_FloatQuat_qy q_0)] ;\n F14_RealQuat_s_qz = Mf32_0[(shiftfield_F7_FloatQuat_qz q_0)]\n })",
"pattern": "EqS14_RealQuat_s{RealQuat_s}{RealQuat_s}" },
"children":
{ "Unfold 'EqS13_RealQuat_s'":
[ { "header": "Definition",
"tactic": "Wp.unfold",
{ "Unfold 'EqS14_RealQuat_s'":
[ { "header": "Split",
"tactic": "Wp.split",
"params": {},
"select":
{ "select": "inside-step",
"at": 3,
"kind": "have",
"occur": 0,
"target": "(L_trace_2_ Mf32_1 rm_0)",
"pattern": "L_trace_2_$Mf32$rm" },
"children":
{ "Unfold 'L_trace_2_'":
[ { "header": "Definition",
"tactic": "Wp.unfold",
"params": {},
"select":
{ "select": "inside-step",
"at": 3,
"kind": "have",
"occur": 0,
"target": "(L_trace_1_ (L_l_RMat_of_FloatRMat Mf32_1 rm_0))",
"pattern": "L_trace_1_L_l_RMat_of_FloatRMat$Mf32" },
{ "select": "clause-step",
"at": 9,
"kind": "branch",
"target": "let a_0 = (shiftfield_F9_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":
{ "Unfold 'L_trace_1_'":
[ { "header": "Definition",
"tactic": "Wp.unfold",
"params": {},
"select":
{ "select": "inside-step",
"at": 3,
"kind": "have",
"occur": 0,
"target": "(L_l_RMat_of_FloatRMat Mf32_1 rm_0)",
"pattern": "L_l_RMat_of_FloatRMat$Mf32$rm" },
"children":
{ "Unfold 'L_l_RMat_of_FloatRMat'":
{ "Then":
[ { "prover": "Z3:4.8.6:counterexamples",
"verdict": "valid",
"time": 0.49,
"steps": 504498 } ],
"Else":
[ { "prover": "Alt-Ergo:2.3.3",
"verdict": "valid",
"time": 1.3969,
"steps": 992 } ] } } ] } } ] } } ] } } ] } } ] } } ] } } ] } } ] } } ]
"time": 1.5609,
"steps": 988 } ] } } ] } } ] } } ] } } ] } } ] } } ] } } ]
sw/airborne/.frama-c/wp/script/float_quat_of_rmat_a11_max_ensures.json
View file @ b0a63524
......@@ -18,7 +18,7 @@
"select":
{ "select": "inside-goal",
"occur": 0,
"target": "let a_0 = (L_l_RMat_of_FloatRMat Mf32_0 rm_0) in\n(L_l_FloatQuat_of_RMat_1_max_1_\n {\n a_0 with\n F12_RealRMat_s_a01 = a_0.F12_RealRMat_s_a10 ;\n F12_RealRMat_s_a02 = a_0.F12_RealRMat_s_a20 ;\n F12_RealRMat_s_a10 = a_0.F12_RealRMat_s_a01 ;\n F12_RealRMat_s_a12 = a_0.F12_RealRMat_s_a21 ;\n F12_RealRMat_s_a20 = a_0.F12_RealRMat_s_a02 ;\n F12_RealRMat_s_a21 = a_0.F12_RealRMat_s_a12\n })",
"target": "let a_0 = (L_l_RMat_of_FloatRMat Mf32_0 rm_0) in\n(L_l_FloatQuat_of_RMat_1_max_1_\n {\n a_0 with\n F13_RealRMat_s_a01 = a_0.F13_RealRMat_s_a10 ;\n F13_RealRMat_s_a02 = a_0.F13_RealRMat_s_a20 ;\n F13_RealRMat_s_a10 = a_0.F13_RealRMat_s_a01 ;\n F13_RealRMat_s_a12 = a_0.F13_RealRMat_s_a21 ;\n F13_RealRMat_s_a20 = a_0.F13_RealRMat_s_a02 ;\n F13_RealRMat_s_a21 = a_0.F13_RealRMat_s_a12\n })",
"pattern": "L_l_FloatQuat_of_RMat_1_max_1_{RealRMat_s}" },
"children":
{ "Unfold 'L_l_FloatQuat_of_RMat_1_max_1_'":
......@@ -36,5 +36,5 @@
{ "Unfold 'L_trace_2_'":
[ { "prover": "Alt-Ergo:2.3.3",
"verdict": "valid",
"time": 3.0198,
"steps": 1252 } ] } } ] } } ] } } ] } } ]
"time": 3.552,
"steps": 1254 } ] } } ] } } ] } } ] } } ]
sw/airborne/.frama-c/wp/script/float_quat_of_rmat_a22_max_ensures.json
View file @ b0a63524
......@@ -52,13 +52,13 @@
"select":
{ "select": "inside-goal",
"occur": 0,
"target": "let a_0 = (L_l_RMat_of_FloatRMat Mf32_0 rm_0) in\n(L_l_FloatQuat_of_RMat_2_max_1_\n {\n a_0 with\n F12_RealRMat_s_a01 = a_0.F12_RealRMat_s_a10 ;\n F12_RealRMat_s_a02 = a_0.F12_RealRMat_s_a20 ;\n F12_RealRMat_s_a10 = a_0.F12_RealRMat_s_a01 ;\n F12_RealRMat_s_a12 = a_0.F12_RealRMat_s_a21 ;\n F12_RealRMat_s_a20 = a_0.F12_RealRMat_s_a02 ;\n F12_RealRMat_s_a21 = a_0.F12_RealRMat_s_a12\n })",
"target": "let a_0 = (L_l_RMat_of_FloatRMat Mf32_0 rm_0) in\n(L_l_FloatQuat_of_RMat_2_max_1_\n {\n a_0 with\n F13_RealRMat_s_a01 = a_0.F13_RealRMat_s_a10 ;\n F13_RealRMat_s_a02 = a_0.F13_RealRMat_s_a20 ;\n F13_RealRMat_s_a10 = a_0.F13_RealRMat_s_a01 ;\n F13_RealRMat_s_a12 = a_0.F13_RealRMat_s_a21 ;\n F13_RealRMat_s_a20 = a_0.F13_RealRMat_s_a02 ;\n F13_RealRMat_s_a21 = a_0.F13_RealRMat_s_a12\n })",
"pattern": "L_l_FloatQuat_of_RMat_2_max_1_{RealRMat_s}" },
"children":
{ "Unfold 'L_l_FloatQuat_of_RMat_2_max_1_'":
[ { "prover": "Alt-Ergo:2.3.3",
"verdict": "valid",
"time": 2.5554,
"time": 2.8336,
"steps": 1013 },
{ "header": "Definition",
"tactic": "Wp.unfold",
......
sw/airborne/.frama-c/wp/script/float_quat_of_rmat_assert.json
View file @ b0a63524
......@@ -9,7 +9,7 @@
"at": 2,
"kind": "have",
"occur": 0,
"target": "let a_0 = (shiftfield_F9_FloatRMat_m rm_0) in\n(P_rotation_matrix\n {\n F12_RealRMat_s_a00 = Mf32_1[(shift_float32 a_0 0)] ;\n F12_RealRMat_s_a01 = Mf32_1[(shift_float32 a_0 1)] ;\n F12_RealRMat_s_a02 = Mf32_1[(shift_float32 a_0 2)] ;\n F12_RealRMat_s_a10 = Mf32_1[(shift_float32 a_0 3)] ;\n F12_RealRMat_s_a11 = Mf32_1[(shift_float32 a_0 4)] ;\n F12_RealRMat_s_a12 = Mf32_1[(shift_float32 a_0 5)] ;\n F12_RealRMat_s_a20 = Mf32_1[(shift_float32 a_0 6)] ;\n F12_RealRMat_s_a21 = Mf32_1[(shift_float32 a_0 7)] ;\n F12_RealRMat_s_a22 = Mf32_1[(shift_float32 a_0 8)]\n })",
"target": "let a_0 = (shiftfield_F9_FloatRMat_m rm_0) in\n(P_rotation_matrix\n {\n F13_RealRMat_s_a00 = Mf32_1[(shift_float32 a_0 0)] ;\n F13_RealRMat_s_a01 = Mf32_1[(shift_float32 a_0 1)] ;\n F13_RealRMat_s_a02 = Mf32_1[(shift_float32 a_0 2)] ;\n F13_RealRMat_s_a10 = Mf32_1[(shift_float32 a_0 3)] ;\n F13_RealRMat_s_a11 = Mf32_1[(shift_float32 a_0 4)] ;\n F13_RealRMat_s_a12 = Mf32_1[(shift_float32 a_0 5)] ;\n F13_RealRMat_s_a20 = Mf32_1[(shift_float32 a_0 6)] ;\n F13_RealRMat_s_a21 = Mf32_1[(shift_float32 a_0 7)] ;\n F13_RealRMat_s_a22 = Mf32_1[(shift_float32 a_0 8)]\n })",
"pattern": "P_rotation_matrix{RealRMat_s}[][]" },
"children": { "Unfold 'P_rotation_matrix'":
[ { "header": "Definition",
......@@ -20,7 +20,7 @@
"at": 2,
"kind": "have",
"occur": 0,
"target": "let a_0 = (shiftfield_F9_FloatRMat_m rm_0) in\n(L_transpose\n {\n F12_RealRMat_s_a00 = Mf32_1[(shift_float32 a_0 0)] ;\n F12_RealRMat_s_a01 = Mf32_1[(shift_float32 a_0 1)] ;\n F12_RealRMat_s_a02 = Mf32_1[(shift_float32 a_0 2)] ;\n F12_RealRMat_s_a10 = Mf32_1[(shift_float32 a_0 3)] ;\n F12_RealRMat_s_a11 = Mf32_1[(shift_float32 a_0 4)] ;\n F12_RealRMat_s_a12 = Mf32_1[(shift_float32 a_0 5)] ;\n F12_RealRMat_s_a20 = Mf32_1[(shift_float32 a_0 6)] ;\n F12_RealRMat_s_a21 = Mf32_1[(shift_float32 a_0 7)] ;\n F12_RealRMat_s_a22 = Mf32_1[(shift_float32 a_0 8)]\n })",
"target": "let a_0 = (shiftfield_F9_FloatRMat_m rm_0) in\n(L_transpose\n {\n F13_RealRMat_s_a00 = Mf32_1[(shift_float32 a_0 0)] ;\n F13_RealRMat_s_a01 = Mf32_1[(shift_float32 a_0 1)] ;\n F13_RealRMat_s_a02 = Mf32_1[(shift_float32 a_0 2)] ;\n F13_RealRMat_s_a10 = Mf32_1[(shift_float32 a_0 3)] ;\n F13_RealRMat_s_a11 = Mf32_1[(shift_float32 a_0 4)] ;\n F13_RealRMat_s_a12 = Mf32_1[(shift_float32 a_0 5)] ;\n F13_RealRMat_s_a20 = Mf32_1[(shift_float32 a_0 6)] ;\n F13_RealRMat_s_a21 = Mf32_1[(shift_float32 a_0 7)] ;\n F13_RealRMat_s_a22 = Mf32_1[(shift_float32 a_0 8)]\n })",
"pattern": "L_transpose{RealRMat_s}[][][][][]" },
"children":
{ "Unfold 'L_transpose'":
......@@ -32,7 +32,7 @@
"at": 2,
"kind": "have",
"occur": 0,
"target": "let a_0 = (shiftfield_F9_FloatRMat_m rm_0) in\nlet r_0 = Mf32_1[(shift_float32 a_0 0)] in\nlet r_1 = Mf32_1[(shift_float32 a_0 1)] in\nlet r_2 = Mf32_1[(shift_float32 a_0 2)] in\nlet r_3 = Mf32_1[(shift_float32 a_0 3)] in\nlet r_4 = Mf32_1[(shift_float32 a_0 4)] in\nlet r_5 = Mf32_1[(shift_float32 a_0 5)] in\nlet r_6 = Mf32_1[(shift_float32 a_0 6)] in\nlet r_7 = Mf32_1[(shift_float32 a_0 7)] in\nlet r_8 = Mf32_1[(shift_float32 a_0 8)] in\n(L_mult_RealRMat\n {\n F12_RealRMat_s_a00 = r_0 ;\n F12_RealRMat_s_a01 = r_1 ;\n F12_RealRMat_s_a02 = r_2 ;\n F12_RealRMat_s_a10 = r_3 ;\n F12_RealRMat_s_a11 = r_4 ;\n F12_RealRMat_s_a12 = r_5 ;\n F12_RealRMat_s_a20 = r_6 ;\n F12_RealRMat_s_a21 = r_7 ;\n F12_RealRMat_s_a22 = r_8\n }\n {\n F12_RealRMat_s_a00 = r_0 ;\n F12_RealRMat_s_a01 = r_3 ;\n F12_RealRMat_s_a02 = r_6 ;\n F12_RealRMat_s_a10 = r_1 ;\n F12_RealRMat_s_a11 = r_4 ;\n F12_RealRMat_s_a12 = r_7 ;\n F12_RealRMat_s_a20 = r_2 ;\n F12_RealRMat_s_a21 = r_5 ;\n F12_RealRMat_s_a22 = r_8\n })",
"target": "let a_0 = (shiftfield_F9_FloatRMat_m rm_0) in\nlet r_0 = Mf32_1[(shift_float32 a_0 0)] in\nlet r_1 = Mf32_1[(shift_float32 a_0 1)] in\nlet r_2 = Mf32_1[(shift_float32 a_0 2)] in\nlet r_3 = Mf32_1[(shift_float32 a_0 3)] in\nlet r_4 = Mf32_1[(shift_float32 a_0 4)] in\nlet r_5 = Mf32_1[(shift_float32 a_0 5)] in\nlet r_6 = Mf32_1[(shift_float32 a_0 6)] in\nlet r_7 = Mf32_1[(shift_float32 a_0 7)] in\nlet r_8 = Mf32_1[(shift_float32 a_0 8)] in\n(L_mult_RealRMat\n {\n F13_RealRMat_s_a00 = r_0 ;\n F13_RealRMat_s_a01 = r_1 ;\n F13_RealRMat_s_a02 = r_2 ;\n F13_RealRMat_s_a10 = r_3 ;\n F13_RealRMat_s_a11 = r_4 ;\n F13_RealRMat_s_a12 = r_5 ;\n F13_RealRMat_s_a20 = r_6 ;\n F13_RealRMat_s_a21 = r_7 ;\n F13_RealRMat_s_a22 = r_8\n }\n {\n F13_RealRMat_s_a00 = r_0 ;\n F13_RealRMat_s_a01 = r_3 ;\n F13_RealRMat_s_a02 = r_6 ;\n F13_RealRMat_s_a10 = r_1 ;\n F13_RealRMat_s_a11 = r_4 ;\n F13_RealRMat_s_a12 = r_7 ;\n F13_RealRMat_s_a20 = r_2 ;\n F13_RealRMat_s_a21 = r_5 ;\n F13_RealRMat_s_a22 = r_8\n })",
"pattern": "L_mult_RealRMat{RealRMat_s}{RealRMat_s}" },
"children":
{ "Unfold 'L_mult_RealRMat'":
......@@ -49,8 +49,8 @@
{ "Then":
[ { "prover": "Z3:4.8.6:counterexamples",
"verdict": "valid",
"time": 0.35,
"steps": 431323 } ],
"time": 0.49,
"steps": 439844 } ],
"Else":
[ { "header": "Split",
"tactic": "Wp.split",
......@@ -76,8 +76,8 @@
{ "Then":
[ { "prover": "Z3:4.8.6:counterexamples",
"verdict": "valid",
"time": 0.48,
"steps": 395625 } ],
"time": 0.41,
"steps": 404171 } ],
"Else":
[ { "header": "Split",
"tactic": "Wp.split",
......@@ -92,13 +92,13 @@
{ "Then":
[ { "prover": "Z3:4.8.6",
"verdict": "valid",
"time": 0.08,
"steps": 226918 } ],
"time": 0.09,
"steps": 259776 } ],
"Else":
[ { "prover": "Z3:4.8.6:counterexamples",
"verdict": "valid",
"time": 0.4,
"steps": 395020 } ] } } ] } } ],
"time": 0.5,
"steps": 403279 } ] } } ] } } ],
"Else":
[ { "header": "Split",
"tactic": "Wp.split",
......@@ -113,10 +113,10 @@
{ "Then":
[ { "prover": "Z3:4.8.6:counterexamples",
"verdict": "valid",
"time": 0.4,
"steps": 395380 } ],
"time": 0.46,
"steps": 404145 } ],
"Else":
[ { "prover": "Z3:4.8.6:counterexamples",
"verdict": "valid",
"time": 0.37,
"steps": 392223 } ] } } ] } } ] } } ] } } ] } } ] } } ] } } ]
"time": 0.43,
"steps": 400912 } ] } } ] } } ] } } ] } } ] } } ] } } ] } } ]
sw/airborne/.frama-c/wp/script/float_quat_of_rmat_assert_2.json
View file @ b0a63524
......@@ -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": 5.4734,
"verdict": "valid", "time": 5.7427,
"steps": 1628 } ] } } ]
sw/airborne/.frama-c/wp/script/float_quat_of_rmat_trace_pos_ensures.json
View file @ b0a63524
......@@ -68,7 +68,11 @@
"pattern": "L_l_RMat_of_FloatRMat$Mf32$rm" },
"children":
{ "Unfold 'L_l_RMat_of_FloatRMat'":
[ { "header": "Definition",
[ { "prover": "Alt-Ergo:2.3.3",
"verdict": "valid",
"time": 4.5503,
"steps": 809 },
{ "header": "Definition",
"tactic": "Wp.unfold",
"params": {},
"select":
......@@ -79,5 +83,5 @@
{ "Unfold 'EqS13_RealQuat_s'":
[ { "prover": "Alt-Ergo:2.3.3",
"verdict": "valid",
"time": 7.162,
"time": 7.4511,
"steps": 4632 } ] } } ] } } ] } } ] } } ] } } ] } } ] } } ] } } ]
sw/airborne/.frama-c/wp/script/lemma_quat_of_rmat_ortho.json
View file @ b0a63524
......@@ -18,7 +18,7 @@
"params": {},
"select":
{ "select": "clause-goal",
"target": "let r_0 = Mf32_0[(shiftfield_F7_FloatQuat_qy q_0)] in\nlet r_1 = (r_0*r_0) in\nlet r_2 = (-r_1) in\nlet r_3 = Mf32_0[(shiftfield_F7_FloatQuat_qz q_0)] in\nlet r_4 = (r_3*r_3) in\nlet r_5 = (-r_4) in\nlet r_6 = Mf32_0[(shiftfield_F7_FloatQuat_qi q_0)] in\nlet r_7 = (r_6*r_6) in\nlet r_8 = Mf32_0[(shiftfield_F7_FloatQuat_qx q_0)] in\nlet r_9 = (r_8*r_8) in\nlet r_10 = (r_6*r_3) in\nlet r_11 = (r_8*r_0) in\nlet r_12 = (r_6*r_0) in\nlet r_13 = (r_8*r_3) in\nlet r_14 = (-r_9) in\nlet r_15 = (r_6*r_8) in\nlet r_16 = (r_0*r_3) in\n(P_rotation_matrix\n {\n F12_RealRMat_s_a00 = r_7+r_9-r_1-r_4 ;\n F12_RealRMat_s_a01 = 2*(r_11-r_10) ;\n F12_RealRMat_s_a02 = 2*(r_12+r_13) ;\n F12_RealRMat_s_a10 = 2*(r_10+r_11) ;\n F12_RealRMat_s_a11 = r_7+r_1-r_9-r_4 ;\n F12_RealRMat_s_a12 = 2*(r_16-r_15) ;\n F12_RealRMat_s_a20 = 2*(r_13-r_12) ;\n F12_RealRMat_s_a21 = 2*(r_15+r_16) ;\n F12_RealRMat_s_a22 = r_7+r_4-r_9-r_1\n })",
"target": "let r_0 = Mf32_0[(shiftfield_F7_FloatQuat_qy q_0)] in\nlet r_1 = (r_0*r_0) in\nlet r_2 = (-r_1) in\nlet r_3 = Mf32_0[(shiftfield_F7_FloatQuat_qz q_0)] in\nlet r_4 = (r_3*r_3) in\nlet r_5 = (-r_4) in\nlet r_6 = Mf32_0[(shiftfield_F7_FloatQuat_qi q_0)] in\nlet r_7 = (r_6*r_6) in\nlet r_8 = Mf32_0[(shiftfield_F7_FloatQuat_qx q_0)] in\nlet r_9 = (r_8*r_8) in\nlet r_10 = (r_6*r_3) in\nlet r_11 = (r_8*r_0) in\nlet r_12 = (r_6*r_0) in\nlet r_13 = (r_8*r_3) in\nlet r_14 = (-r_9) in\nlet r_15 = (r_6*r_8) in\nlet r_16 = (r_0*r_3) in\n(P_rotation_matrix\n {\n F13_RealRMat_s_a00 = r_7+r_9-r_1-r_4 ;\n F13_RealRMat_s_a01 = 2*(r_11-r_10) ;\n F13_RealRMat_s_a02 = 2*(r_12+r_13) ;\n F13_RealRMat_s_a10 = 2*(r_10+r_11) ;\n F13_RealRMat_s_a11 = r_7+r_1-r_9-r_4 ;\n F13_RealRMat_s_a12 = 2*(r_16-r_15) ;\n F13_RealRMat_s_a20 = 2*(r_13-r_12) ;\n F13_RealRMat_s_a21 = 2*(r_15+r_16) ;\n F13_RealRMat_s_a22 = r_7+r_4-r_9-r_1\n })",
"pattern": "P_rotation_matrix{RealRMat_s}+**" },
"children":
{ "Unfold 'P_rotation_matrix'":
......@@ -38,7 +38,7 @@
"select":
{ "select": "inside-goal",
"occur": 0,
"target": "let r_0 = Mf32_0[(shiftfield_F7_FloatQuat_qy q_0)] in\nlet r_1 = (r_0*r_0) in\nlet r_2 = (-r_1) in\nlet r_3 = Mf32_0[(shiftfield_F7_FloatQuat_qz q_0)] in\nlet r_4 = (r_3*r_3) in\nlet r_5 = (-r_4) in\nlet r_6 = Mf32_0[(shiftfield_F7_FloatQuat_qi q_0)] in\nlet r_7 = (r_6*r_6) in\nlet r_8 = Mf32_0[(shiftfield_F7_FloatQuat_qx q_0)] in\nlet r_9 = (r_8*r_8) in\nlet r_10 = (r_6*r_3) in\nlet r_11 = (r_8*r_0) in\nlet r_12 = (r_6*r_0) in\nlet r_13 = (r_8*r_3) in\nlet r_14 = (-r_9) in\nlet r_15 = (r_6*r_8) in\nlet r_16 = (r_0*r_3) in\n(L_transpose\n {\n F12_RealRMat_s_a00 = r_7+r_9-r_1-r_4 ;\n F12_RealRMat_s_a01 = 2*(r_11-r_10) ;\n F12_RealRMat_s_a02 = 2*(r_12+r_13) ;\n F12_RealRMat_s_a10 = 2*(r_10+r_11) ;\n F12_RealRMat_s_a11 = r_7+r_1-r_9-r_4 ;\n F12_RealRMat_s_a12 = 2*(r_16-r_15) ;\n F12_RealRMat_s_a20 = 2*(r_13-r_12) ;\n F12_RealRMat_s_a21 = 2*(r_15+r_16) ;\n F12_RealRMat_s_a22 = r_7+r_4-r_9-r_1\n })",
"target": "let r_0 = Mf32_0[(shiftfield_F7_FloatQuat_qy q_0)] in\nlet r_1 = (r_0*r_0) in\nlet r_2 = (-r_1) in\nlet r_3 = Mf32_0[(shiftfield_F7_FloatQuat_qz q_0)] in\nlet r_4 = (r_3*r_3) in\nlet r_5 = (-r_4) in\nlet r_6 = Mf32_0[(shiftfield_F7_FloatQuat_qi q_0)] in\nlet r_7 = (r_6*r_6) in\nlet r_8 = Mf32_0[(shiftfield_F7_FloatQuat_qx q_0)] in\nlet r_9 = (r_8*r_8) in\nlet r_10 = (r_6*r_3) in\nlet r_11 = (r_8*r_0) in\nlet r_12 = (r_6*r_0) in\nlet r_13 = (r_8*r_3) in\nlet r_14 = (-r_9) in\nlet r_15 = (r_6*r_8) in\nlet r_16 = (r_0*r_3) in\n(L_transpose\n {\n F13_RealRMat_s_a00 = r_7+r_9-r_1-r_4 ;\n F13_RealRMat_s_a01 = 2*(r_11-r_10) ;\n F13_RealRMat_s_a02 = 2*(r_12+r_13) ;\n F13_RealRMat_s_a10 = 2*(r_10+r_11) ;\n F13_RealRMat_s_a11 = r_7+r_1-r_9-r_4 ;\n F13_RealRMat_s_a12 = 2*(r_16-r_15) ;\n F13_RealRMat_s_a20 = 2*(r_13-r_12) ;\n F13_RealRMat_s_a21 = 2*(r_15+r_16) ;\n F13_RealRMat_s_a22 = r_7+r_4-r_9-r_1\n })",
"pattern": "L_transpose{RealRMat_s}+***+***+" },
"children":
{ "Unfold 'L_transpose'":
......@@ -48,7 +48,7 @@
"select":
{ "select": "inside-goal",
"occur": 0,
"target": "let r_0 = Mf32_0[(shiftfield_F7_FloatQuat_qy q_0)] in\nlet r_1 = (r_0*r_0) in\nlet r_2 = (-r_1) in\nlet r_3 = Mf32_0[(shiftfield_F7_FloatQuat_qz q_0)] in\nlet r_4 = (r_3*r_3) in\nlet r_5 = (-r_4) in\nlet r_6 = Mf32_0[(shiftfield_F7_FloatQuat_qi q_0)] in\nlet r_7 = (r_6*r_6) in\nlet r_8 = Mf32_0[(shiftfield_F7_FloatQuat_qx q_0)] in\nlet r_9 = (r_8*r_8) in\nlet r_10 = (r_7+r_9-r_1-r_4) in\nlet r_11 = (r_6*r_3) in\nlet r_12 = (r_8*r_0) in\nlet r_13 = (2*(r_12-r_11)) in\nlet r_14 = (r_6*r_0) in\nlet r_15 = (r_8*r_3) in\nlet r_16 = (2*(r_14+r_15)) in\nlet r_17 = (2*(r_11+r_12)) in\nlet r_18 = (-r_9) in\nlet r_19 = (r_7+r_1-r_9-r_4) in\nlet r_20 = (r_6*r_8) in\nlet r_21 = (r_0*r_3) in\nlet r_22 = (2*(r_21-r_20)) in\nlet r_23 = (2*(r_15-r_14)) in\nlet r_24 = (2*(r_20+r_21)) in\nlet r_25 = (r_7+r_4-r_9-r_1) in\n(L_mult_RealRMat\n {\n F12_RealRMat_s_a00 = r_10 ;\n F12_RealRMat_s_a01 = r_13 ;\n F12_RealRMat_s_a02 = r_16 ;\n F12_RealRMat_s_a10 = r_17 ;\n F12_RealRMat_s_a11 = r_19 ;\n F12_RealRMat_s_a12 = r_22 ;\n F12_RealRMat_s_a20 = r_23 ;\n F12_RealRMat_s_a21 = r_24 ;\n F12_RealRMat_s_a22 = r_25\n }\n {\n F12_RealRMat_s_a00 = r_10 ;\n F12_RealRMat_s_a01 = r_17 ;\n F12_RealRMat_s_a02 = r_23 ;\n F12_RealRMat_s_a10 = r_13 ;\n F12_RealRMat_s_a11 = r_19 ;\n F12_RealRMat_s_a12 = r_24 ;\n F12_RealRMat_s_a20 = r_16 ;\n F12_RealRMat_s_a21 = r_22 ;\n F12_RealRMat_s_a22 = r_25\n })",
"target": "let r_0 = Mf32_0[(shiftfield_F7_FloatQuat_qy q_0)] in\nlet r_1 = (r_0*r_0) in\nlet r_2 = (-r_1) in\nlet r_3 = Mf32_0[(shiftfield_F7_FloatQuat_qz q_0)] in\nlet r_4 = (r_3*r_3) in\nlet r_5 = (-r_4) in\nlet r_6 = Mf32_0[(shiftfield_F7_FloatQuat_qi q_0)] in\nlet r_7 = (r_6*r_6) in\nlet r_8 = Mf32_0[(shiftfield_F7_FloatQuat_qx q_0)] in\nlet r_9 = (r_8*r_8) in\nlet r_10 = (r_7+r_9-r_1-r_4) in\nlet r_11 = (r_6*r_3) in\nlet r_12 = (r_8*r_0) in\nlet r_13 = (2*(r_12-r_11)) in\nlet r_14 = (r_6*r_0) in\nlet r_15 = (r_8*r_3) in\nlet r_16 = (2*(r_14+r_15)) in\nlet r_17 = (2*(r_11+r_12)) in\nlet r_18 = (-r_9) in\nlet r_19 = (r_7+r_1-r_9-r_4) in\nlet r_20 = (r_6*r_8) in\nlet r_21 = (r_0*r_3) in\nlet r_22 = (2*(r_21-r_20)) in\nlet r_23 = (2*(r_15-r_14)) in\nlet r_24 = (2*(r_20+r_21)) in\nlet r_25 = (r_7+r_4-r_9-r_1) in\n(L_mult_RealRMat\n {\n F13_RealRMat_s_a00 = r_10 ;\n F13_RealRMat_s_a01 = r_13 ;\n F13_RealRMat_s_a02 = r_16 ;\n F13_RealRMat_s_a10 = r_17 ;\n F13_RealRMat_s_a11 = r_19 ;\n F13_RealRMat_s_a12 = r_22 ;\n F13_RealRMat_s_a20 = r_23 ;\n F13_RealRMat_s_a21 = r_24 ;\n F13_RealRMat_s_a22 = r_25\n }\n {\n F13_RealRMat_s_a00 = r_10 ;\n F13_RealRMat_s_a01 = r_17 ;\n F13_RealRMat_s_a02 = r_23 ;\n F13_RealRMat_s_a10 = r_13 ;\n F13_RealRMat_s_a11 = r_19 ;\n F13_RealRMat_s_a12 = r_24 ;\n F13_RealRMat_s_a20 = r_16 ;\n F13_RealRMat_s_a21 = r_22 ;\n F13_RealRMat_s_a22 = r_25\n })",
"pattern": "L_mult_RealRMat{RealRMat_s}{RealRMat_s}" },
"children":
{ "Unfold 'L_mult_RealRMat'":
......@@ -57,11 +57,11 @@
"params": {},
"select":
{ "select": "clause-goal",
"target": "let r_0 = Mf32_0[(shiftfield_F7_FloatQuat_qi q_0)] in\nlet r_1 = Mf32_0[(shiftfield_F7_FloatQuat_qy q_0)] in\nlet r_2 = (r_0*r_1) in\nlet r_3 = Mf32_0[(shiftfield_F7_FloatQuat_qx q_0)] in\nlet r_4 = Mf32_0[(shiftfield_F7_FloatQuat_qz q_0)] in\nlet r_5 = (r_3*r_4) in\nlet r_6 = (r_2+r_5) in\nlet r_7 = (r_0*r_4) in\nlet r_8 = (r_3*r_1) in\nlet r_9 = (r_8-r_7) in\nlet r_10 = (r_1*r_1) in\nlet r_11 = (-r_10) in\nlet r_12 = (r_4*r_4) in\nlet r_13 = (-r_12) in\nlet r_14 = (r_0*r_0) in\nlet r_15 = (r_3*r_3) in\nlet r_16 = (r_14+r_15-r_10-r_12) in\nlet r_17 = (r_0*r_3) in\nlet r_18 = (r_1*r_4) in\nlet r_19 = (r_18-r_17) in\nlet r_20 = (r_7+r_8) in\nlet r_21 = (-r_15) in\nlet r_22 = (r_14+r_10-r_15-r_12) in\nlet r_23 = ((4*r_6*r_19)+(2*r_20*r_16)+(2*r_9*r_22)) in\nlet r_24 = (r_17+r_18) in\nlet r_25 = (r_14+r_12-r_15-r_10) in\nlet r_26 = (r_5-r_2) in\nlet r_27 = ((4*r_24*r_9)+(2*r_6*r_25)+(2*r_26*r_16)) in\nlet r_28 = ((4*r_20*r_26)+(2*r_24*r_22)+(2*r_19*r_25)) in\n(EqS12_RealRMat_s\n {\n F12_RealRMat_s_a00 = (4*r_6*r_6)+(4*r_9*r_9)+(r_16*r_16) ;\n F12_RealRMat_s_a01 = r_23 ;\n F12_RealRMat_s_a02 = r_27 ;\n F12_RealRMat_s_a10 = r_23 ;\n F12_RealRMat_s_a11 = (4*r_20*r_20)+(4*r_19*r_19)+(r_22*r_22) ;\n F12_RealRMat_s_a12 = r_28 ;\n F12_RealRMat_s_a20 = r_27 ;\n F12_RealRMat_s_a21 = r_28 ;\n F12_RealRMat_s_a22 = (4*r_24*r_24)+(4*r_26*r_26)+(r_25*r_25)\n }\n {\n F12_RealRMat_s_a00 = 1 ;\n F12_RealRMat_s_a01 = 0 ;\n F12_RealRMat_s_a02 = 0 ;\n F12_RealRMat_s_a10 = 0 ;\n F12_RealRMat_s_a11 = 1 ;\n F12_RealRMat_s_a12 = 0 ;\n F12_RealRMat_s_a20 = 0 ;\n F12_RealRMat_s_a21 = 0 ;\n F12_RealRMat_s_a22 = 1\n })",
"pattern": "EqS12_RealRMat_s{RealRMat_s}{RealRMat_s}" },
"target": "let r_0 = Mf32_0[(shiftfield_F7_FloatQuat_qi q_0)] in\nlet r_1 = Mf32_0[(shiftfield_F7_FloatQuat_qy q_0)] in\nlet r_2 = (r_0*r_1) in\nlet r_3 = Mf32_0[(shiftfield_F7_FloatQuat_qx q_0)] in\nlet r_4 = Mf32_0[(shiftfield_F7_FloatQuat_qz q_0)] in\nlet r_5 = (r_3*r_4) in\nlet r_6 = (r_2+r_5) in\nlet r_7 = (r_0*r_4) in\nlet r_8 = (r_3*r_1) in\nlet r_9 = (r_8-r_7) in\nlet r_10 = (r_1*r_1) in\nlet r_11 = (-r_10) in\nlet r_12 = (r_4*r_4) in\nlet r_13 = (-r_12) in\nlet r_14 = (r_0*r_0) in\nlet r_15 = (r_3*r_3) in\nlet r_16 = (r_14+r_15-r_10-r_12) in\nlet r_17 = (r_0*r_3) in\nlet r_18 = (r_1*r_4) in\nlet r_19 = (r_18-r_17) in\nlet r_20 = (r_7+r_8) in\nlet r_21 = (-r_15) in\nlet r_22 = (r_14+r_10-r_15-r_12) in\nlet r_23 = ((4*r_6*r_19)+(2*r_20*r_16)+(2*r_9*r_22)) in\nlet r_24 = (r_17+r_18) in\nlet r_25 = (r_14+r_12-r_15-r_10) in\nlet r_26 = (r_5-r_2) in\nlet r_27 = ((4*r_24*r_9)+(2*r_6*r_25)+(2*r_26*r_16)) in\nlet r_28 = ((4*r_20*r_26)+(2*r_24*r_22)+(2*r_19*r_25)) in\n(EqS13_RealRMat_s\n {\n F13_RealRMat_s_a00 = (4*r_6*r_6)+(4*r_9*r_9)+(r_16*r_16) ;\n F13_RealRMat_s_a01 = r_23 ;\n F13_RealRMat_s_a02 = r_27 ;\n F13_RealRMat_s_a10 = r_23 ;\n F13_RealRMat_s_a11 = (4*r_20*r_20)+(4*r_19*r_19)+(r_22*r_22) ;\n F13_RealRMat_s_a12 = r_28 ;\n F13_RealRMat_s_a20 = r_27 ;\n F13_RealRMat_s_a21 = r_28 ;\n F13_RealRMat_s_a22 = (4*r_24*r_24)+(4*r_26*r_26)+(r_25*r_25)\n }\n {\n F13_RealRMat_s_a00 = 1 ;\n F13_RealRMat_s_a01 = 0 ;\n F13_RealRMat_s_a02 = 0 ;\n F13_RealRMat_s_a10 = 0 ;\n F13_RealRMat_s_a11 = 1 ;\n F13_RealRMat_s_a12 = 0 ;\n F13_RealRMat_s_a20 = 0 ;\n F13_RealRMat_s_a21 = 0 ;\n F13_RealRMat_s_a22 = 1\n })",
"pattern": "EqS13_RealRMat_s{RealRMat_s}{RealRMat_s}" },
"children":
{ "Unfold 'EqS12_RealRMat_s'":
{ "Unfold 'EqS13_RealRMat_s'":
[ { "prover": "Z3:4.8.6:counterexamples",
"verdict": "valid",
"time": 0.04,
"steps": 46240 } ] } } ] } } ] } } ] } } ] } } ] } } ] } } ]
"steps": 51791 } ] } } ] } } ] } } ] } } ] } } ] } } ] } } ]
sw/airborne/math/pprz_algebra_float_convert_rmat_frama_c.h
View file @ b0a63524
......@@ -17,6 +17,103 @@ extern "C" {
x >= 0 ==> \sqrt(4 * x * x) == 2 * x;
*/
/*******************************
* RealVect3 definition
* *****************************/
/*@ ghost
struct RealVect3_s {float x;
float y;
float z;};
*/
//@ type RealVect3 = struct RealVect3_s;
//@ axiomatic Arbitrary_RealVect3 { logic RealVect3 empty_vect3;}
#define REALVECT3(vx, \
vy, \
vz) \
{{{empty_vect3 \
\with .x = (float) (vx)} \
\with .y = (float) (vy)} \
\with .z = (float) (vz)}
/*@
logic RealVect3 l_Vect_of_FloatVect3(struct FloatVect3 *v) =
REALVECT3(v->x, v->y, v->z);
*/
/*@
logic RealVect3 mult_scalar(real scal, RealVect3 v) =
REALVECT3(scal * v.x, scal * v.y, scal * v.z);
*/
/*@
lemma mult_scalar_neutral:
\forall RealVect3 v;
mult_scalar(1.0, v) == v;
*/
/*@
logic RealVect3 neg_vect(RealVect3 v) =
REALVECT3(-v.x, -v.y, -v.z);
*/
/*@
lemma neg_vect_equi_mult_scalar:
\forall RealVect3 v;
neg_vect(v) == mult_scalar(-1.0, v);
*/
/*@
logic real scalar_product(RealVect3 v1, RealVect3 v2) =
v1.x * v2.x + v1.y * v2.y + v1.z * v2.z;
*/
/*@
lemma comm_scalar_product:
\forall RealVect3 v1, v2;
scalar_product(v1, v2) == scalar_product(v2, v1);
*/
/*@
logic RealVect3 add_RealVect3(RealVect3 v1, RealVect3 v2) =
REALVECT3(
v1.x + v2.x,
v1.y + v2.y,
v1.z + v2.z
);
*/
/*@
lemma comm_add_RealVect3:
\forall RealVect3 v1, v2;
add_RealVect3(v1, v2) == add_RealVect3(v2, v1);
*/
/*@
lemma trans_add_RealVect3:
\forall RealVect3 v1, v2, v3;
add_RealVect3(v1, add_RealVect3(v2, v3)) == add_RealVect3(add_RealVect3(v1, v2), v3);
*/
/*@
logic RealVect3 cross_product(RealVect3 v1, RealVect3 v2) =
REALVECT3(
v1.y * v2.z - v1.z * v2.y,
v1.z * v2.x - v1.x * v2.z,
v1.x * v2.y - v1.y * v2.x
);
*/
/*@
lemma anticomm_cross_product:
\forall RealVect3 v1, v2;
cross_product(v1, v2) == mult_scalar(-1, cross_product(v2, v1));
*/
/*******************************
* RealRMat definition
* *****************************/
......@@ -119,7 +216,20 @@ logic RealRMat l_RMat_of_FloatRMat(struct FloatRMat *rmat) =
mult_RealRMat(id_rmat, rmat) == rmat;
*/
/*@
logic RealVect3 mult_RealRMat_RealVect3(RealRMat rm, RealVect3 v) =
REALVECT3(
rm.a00 * v.x + rm.a01 * v.y + rm.a02 * v.z,
rm.a10 * v.x + rm.a11 * v.y + rm.a12 * v.z,
rm.a20 * v.x + rm.a21 * v.y + rm.a22 * v.z
);
*/
/*@
lemma mult_vect_id_neutral:
\forall RealVect3 v;
mult_RealRMat_RealVect3(id_rmat, v) == v;
*/
/*******************************
......@@ -191,6 +301,89 @@ logic RealQuat l_Quat_of_FloatQuat(struct FloatQuat *q) =
REALQUAT(q->qi, q->qx, q->qy, q->qz);
*/
/*@
logic RealQuat conj(RealQuat q) =
REALQUAT(q.qi, -q.qx, -q.qy, -q.qz);
*/
/*@
logic RealQuat conj(struct FloatQuat *q) =
REALQUAT(q->qi, -q->qx, -q->qy, -q->qz);
*/
/*******************************
* RealQuatVect definition
* *****************************/
/*@ ghost
struct RealQuatVect_s {float scalar;
struct RealVect3_s v;};
*/
//@ type RealQuatVect = struct RealQuatVect_s;
//@ axiomatic Arbitrary_RealQuatVect { logic RealQuatVect empty_quatvect;}
#define REALQUATVECT(vqi, \
vqx, \
vqy, \
vqz) \
{{empty_quatvect \
\with .scalar = (float) (vqi)} \
\with .v = ({{{empty_vect3 \
\with .x = (float) (vqx)} \
\with .y = (float) (vqy)} \
\with .z = (float) (vqz)})}
#define REALQUATVECT_FVECT(vqi, \
vect) \
{{empty_quatvect \
\with .scalar = (float) (vqi)} \
\with .v = (vect)}
/*@
logic RealQuatVect l_QuatVect_of_FloatQuat(struct FloatQuat *q) =
REALQUATVECT(q->qi, q->qx, q->qy, q->qz);
*/
/*@
logic RealQuat l_Quat_of_RealQuatVect(RealQuatVect q) =
REALQUAT(q.scalar, q.v.x, q.v.y, q.v.y);
*/
/*@
logic RealQuatVect l_QuatVect_of_RealQuat(RealQuat q) =
REALQUATVECT(q.qi, q.qx, q.qy, q.qz);
*/
/*@
logic RealQuatVect mult_RealQuatVect(RealQuatVect q1, RealQuatVect q2) =
\let scalar = q1.scalar * q2.scalar - scalar_product(q1.v, q2.v);
\let vect = add_RealVect3(add_RealVect3(
mult_scalar(q1.scalar, q2.v),
mult_scalar(q2.scalar, q1.v)),
cross_product(q1.v, q2.v));
REALQUATVECT_FVECT(scalar, vect);
*/
/*@
logic RealQuatVect conj_v(struct FloatQuat *q) =
REALQUATVECT_FVECT(q->qi, REALVECT3(-q->qx, -q->qy, -q->qz));
*/
/*@
logic RealQuatVect conj_v(RealQuatVect q) =
\let vect = neg_vect(q.v);
REALQUATVECT_FVECT(q.scalar, vect);
*/
/*@
lemma equi_conj:
\forall struct FloatQuat *q;
conj_v(q)
== l_QuatVect_of_RealQuat(conj(l_Quat_of_FloatQuat(q)));
*/
/*******************************
* CONVERT QUAT TO RMAT
* *****************************/
......@@ -308,6 +501,16 @@ logic RealRMat l_RMat_of_FloatQuat(RealQuat q) =
==> special_orthogonal(l_RMat_of_FloatQuat(q));
*/
/*@
lemma verify_rmat_of_quat_formula:
\forall struct FloatQuat *q, struct FloatVect3 *v;
\let vect = l_Vect_of_FloatVect3(v);
\let rmat = l_RMat_of_FloatQuat(q);
\let mult_quat = mult_RealQuatVect(l_QuatVect_of_FloatQuat(q), REALQUATVECT_FVECT(0, vect));
mult_RealQuatVect(mult_quat, conj_v(q))
== REALQUATVECT_FVECT(0, mult_RealRMat_RealVect3(rmat, vect));
*/
/*******************************
* CONVERT RMAT TO QUAT
* *****************************/
......
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