Skip to content
GitLab
Projects
Groups
Snippets
Help
Loading...
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Sign in
Toggle navigation
Open sidebar
POLLIEN Baptiste
paparazzi-frama-c
Commits
b1951d7f
Commit
b1951d7f
authored
Apr 21, 2021
by
POLLIEN Baptiste
Browse files
Adding lemma for rotation matrix
parent
756f5bc0
Changes
4
Hide whitespace changes
Inline
Side-by-side
Showing
4 changed files
with
183 additions
and
6 deletions
+183
-6
sw/airborne/.frama-c/wp/script/lemma_float_rmat_of_eulers_321_2.json
.../.frama-c/wp/script/lemma_float_rmat_of_eulers_321_2.json
+7
-6
sw/airborne/.frama-c/wp/script/lemma_rotatio_matrix_to_eq.json
...rborne/.frama-c/wp/script/lemma_rotatio_matrix_to_eq.json
+153
-0
sw/airborne/.frama-c/wp/script/lemma_rotation_matrix_to_eq.json
...borne/.frama-c/wp/script/lemma_rotation_matrix_to_eq.json
+8
-0
sw/airborne/math/pprz_algebra_float_convert_rmat_frama_c.h
sw/airborne/math/pprz_algebra_float_convert_rmat_frama_c.h
+15
-0
No files found.
sw/airborne/.frama-c/wp/script/lemma_float_rmat_of_eulers_321_2.json
View file @
b1951d7f
[
{
"prover"
:
"Z3:4.8.6:noBV"
,
"verdict"
:
"timeout"
,
"time"
:
1
0
.
},
{
"prover"
:
"Z3:4.8.6:counterexamples"
,
"verdict"
:
"timeout"
,
"time"
:
1
0
.
},
{
"prover"
:
"Z3:4.8.6"
,
"verdict"
:
"timeout"
,
"time"
:
1
0
.
},
{
"prover"
:
"Coq:8.12.2"
,
"verdict"
:
"
unknown"
},
[
{
"prover"
:
"Z3:4.8.6:noBV"
,
"verdict"
:
"timeout"
,
"time"
:
1
5
.
},
{
"prover"
:
"Z3:4.8.6:counterexamples"
,
"verdict"
:
"timeout"
,
"time"
:
1
5
.
},
{
"prover"
:
"Z3:4.8.6"
,
"verdict"
:
"timeout"
,
"time"
:
1
5
.
},
{
"prover"
:
"Coq:8.12.2"
,
"verdict"
:
"
valid"
,
"time"
:
0.52
},
{
"prover"
:
"CVC4:1.9-prerelease:strings+counterexamples"
,
"verdict"
:
"timeout"
,
"time"
:
10
.
},
{
"prover"
:
"Alt-Ergo:2.3.3"
,
"verdict"
:
"timeout"
,
"time"
:
10
.
}
]
"verdict"
:
"timeout"
,
"time"
:
15
.
},
{
"prover"
:
"Alt-Ergo:2.3.3"
,
"verdict"
:
"timeout"
,
"time"
:
16.9815
,
"steps"
:
46
}
]
sw/airborne/.frama-c/wp/script/lemma_rotatio_matrix_to_eq.json
0 → 100644
View file @
b1951d7f
[
{
"prover"
:
"Z3:4.8.6:noBV"
,
"verdict"
:
"timeout"
,
"time"
:
15
.
},
{
"prover"
:
"Z3:4.8.6:counterexamples"
,
"verdict"
:
"timeout"
,
"time"
:
15
.
},
{
"prover"
:
"Z3:4.8.6"
,
"verdict"
:
"timeout"
,
"time"
:
15
.
},
{
"prover"
:
"Coq:8.12.2"
,
"verdict"
:
"unknown"
},
{
"prover"
:
"CVC4:1.9-prerelease:strings+counterexamples"
,
"verdict"
:
"timeout"
,
"time"
:
15
.
},
{
"prover"
:
"Alt-Ergo:2.3.3"
,
"verdict"
:
"timeout"
,
"time"
:
15
.
},
{
"header"
:
"Definition"
,
"tactic"
:
"Wp.unfold"
,
"params"
:
{},
"select"
:
{
"select"
:
"inside-goal"
,
"occur"
:
0
,
"target"
:
"(L_l_RMat_of_FloatRMat Mf32_0 rm_0)"
,
"pattern"
:
"L_l_RMat_of_FloatRMat$Mf32$rm"
},
"children"
:
{
"Unfold 'L_l_RMat_of_FloatRMat'"
:
[
{
"prover"
:
"Z3:4.8.6:noBV"
,
"verdict"
:
"timeout"
,
"time"
:
15
.
},
{
"prover"
:
"Z3:4.8.6:counterexamples"
,
"verdict"
:
"timeout"
,
"time"
:
15
.
},
{
"prover"
:
"Z3:4.8.6"
,
"verdict"
:
"timeout"
,
"time"
:
15
.
},
{
"prover"
:
"Coq:8.12.2"
,
"verdict"
:
"unknown"
},
{
"prover"
:
"CVC4:1.9-prerelease:strings+counterexamples"
,
"verdict"
:
"timeout"
,
"time"
:
15
.
},
{
"prover"
:
"Alt-Ergo:2.3.3"
,
"verdict"
:
"timeout"
,
"time"
:
15
.
},
{
"header"
:
"Definition"
,
"tactic"
:
"Wp.unfold"
,
"params"
:
{},
"select"
:
{
"select"
:
"inside-goal"
,
"occur"
:
0
,
"target"
:
"let a_0 = (shiftfield_F9_FloatRMat_m rm_0) in
\n
(P_rotation_matrix
\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
})"
,
"pattern"
:
"P_rotation_matrix{RealRMat_s}[][]"
},
"children"
:
{
"Unfold 'P_rotation_matrix'"
:
[
{
"prover"
:
"Z3:4.8.6:noBV"
,
"verdict"
:
"timeout"
,
"time"
:
15
.
},
{
"prover"
:
"Z3:4.8.6:counterexamples"
,
"verdict"
:
"unknown"
},
{
"prover"
:
"Z3:4.8.6"
,
"verdict"
:
"timeout"
,
"time"
:
15
.
},
{
"prover"
:
"Coq:8.12.2"
,
"verdict"
:
"unknown"
},
{
"prover"
:
"CVC4:1.9-prerelease:strings+counterexamples"
,
"verdict"
:
"timeout"
,
"time"
:
15
.
},
{
"prover"
:
"Alt-Ergo:2.3.3"
,
"verdict"
:
"timeout"
,
"time"
:
15
.
},
{
"header"
:
"Definition"
,
"tactic"
:
"Wp.unfold"
,
"params"
:
{},
"select"
:
{
"select"
:
"inside-goal"
,
"occur"
:
0
,
"target"
:
"L_id_rmat"
,
"pattern"
:
"L_id_rmat"
},
"children"
:
{
"Unfold 'L_id_rmat'"
:
[
{
"prover"
:
"Z3:4.8.6:noBV"
,
"verdict"
:
"timeout"
,
"time"
:
15
.
},
{
"prover"
:
"Z3:4.8.6:counterexamples"
,
"verdict"
:
"unknown"
},
{
"prover"
:
"Z3:4.8.6"
,
"verdict"
:
"timeout"
,
"time"
:
15
.
},
{
"prover"
:
"Coq:8.12.2"
,
"verdict"
:
"unknown"
},
{
"prover"
:
"CVC4:1.9-prerelease:strings+counterexamples"
,
"verdict"
:
"timeout"
,
"time"
:
15
.
},
{
"prover"
:
"Alt-Ergo:2.3.3"
,
"verdict"
:
"timeout"
,
"time"
:
15
.
},
{
"header"
:
"Definition"
,
"tactic"
:
"Wp.unfold"
,
"params"
:
{},
"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
})"
,
"pattern"
:
"L_transpose{RealRMat_s}[][][][][]"
},
"children"
:
{
"Unfold 'L_transpose'"
:
[
{
"prover"
:
"Z3:4.8.6:noBV"
,
"verdict"
:
"timeout"
,
"time"
:
15
.
},
{
"prover"
:
"Z3:4.8.6:counterexamples"
,
"verdict"
:
"unknown"
},
{
"prover"
:
"Z3:4.8.6"
,
"verdict"
:
"timeout"
,
"time"
:
15
.
},
{
"prover"
:
"Coq:8.12.2"
,
"verdict"
:
"unknown"
},
{
"prover"
:
"CVC4:1.9-prerelease:strings+counterexamples"
,
"verdict"
:
"timeout"
,
"time"
:
15
.
},
{
"prover"
:
"Alt-Ergo:2.3.3"
,
"verdict"
:
"timeout"
,
"time"
:
15
.
},
{
"header"
:
"Definition"
,
"tactic"
:
"Wp.unfold"
,
"params"
:
{},
"select"
:
{
"select"
:
"inside-goal"
,
"occur"
:
0
,
"target"
:
"let a_0 = (shiftfield_F9_FloatRMat_m rm_0) in
\n
let r_0 = Mf32_0[(shift_float32 a_0 0)] in
\n
let r_1 = Mf32_0[(shift_float32 a_0 1)] in
\n
let r_2 = Mf32_0[(shift_float32 a_0 2)] in
\n
let r_3 = Mf32_0[(shift_float32 a_0 3)] in
\n
let r_4 = Mf32_0[(shift_float32 a_0 4)] in
\n
let r_5 = Mf32_0[(shift_float32 a_0 5)] in
\n
let r_6 = Mf32_0[(shift_float32 a_0 6)] in
\n
let r_7 = Mf32_0[(shift_float32 a_0 7)] in
\n
let r_8 = Mf32_0[(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
})"
,
"pattern"
:
"L_mult_RealRMat{RealRMat_s}{RealRMat_s}"
},
"children"
:
{
"Unfold 'L_mult_RealRMat'"
:
[
{
"prover"
:
"Z3:4.8.6:noBV"
,
"verdict"
:
"timeout"
,
"time"
:
15
.
},
{
"prover"
:
"Z3:4.8.6:counterexamples"
,
"verdict"
:
"unknown"
},
{
"prover"
:
"Z3:4.8.6"
,
"verdict"
:
"timeout"
,
"time"
:
15
.
},
{
"prover"
:
"Coq:8.12.2"
,
"verdict"
:
"unknown"
},
{
"prover"
:
"CVC4:1.9-prerelease:strings+counterexamples"
,
"verdict"
:
"timeout"
,
"time"
:
15
.
},
{
"prover"
:
"Alt-Ergo:2.3.3"
,
"verdict"
:
"timeout"
,
"time"
:
15
.
},
{
"header"
:
"Definition"
,
"tactic"
:
"Wp.unfold"
,
"params"
:
{},
"select"
:
{
"select"
:
"inside-goal"
,
"occur"
:
0
,
"target"
:
"let a_0 = (shiftfield_F9_FloatRMat_m rm_0) in
\n
let r_0 = Mf32_0[(shift_float32 a_0 0)] in
\n
let r_1 = Mf32_0[(shift_float32 a_0 1)] in
\n
let r_2 = Mf32_0[(shift_float32 a_0 2)] in
\n
let r_3 = Mf32_0[(shift_float32 a_0 3)] in
\n
let r_4 = Mf32_0[(shift_float32 a_0 4)] in
\n
let r_5 = Mf32_0[(shift_float32 a_0 5)] in
\n
let r_6 = ((r_0*r_3)+(r_1*r_4)+(r_2*r_5)) in
\n
let r_7 = Mf32_0[(shift_float32 a_0 6)] in
\n
let r_8 = Mf32_0[(shift_float32 a_0 7)] in
\n
let r_9 = Mf32_0[(shift_float32 a_0 8)] in
\n
let r_10 = ((r_0*r_7)+(r_1*r_8)+(r_2*r_9)) in
\n
let r_11 = ((r_3*r_7)+(r_4*r_8)+(r_5*r_9)) in
\n
(EqS12_RealRMat_s
\n
{
\n
F12_RealRMat_s_a00 = (r_0*r_0)+(r_1*r_1)+(r_2*r_2) ;
\n
F12_RealRMat_s_a01 = r_6 ;
\n
F12_RealRMat_s_a02 = r_10 ;
\n
F12_RealRMat_s_a10 = r_6 ;
\n
F12_RealRMat_s_a11 = (r_3*r_3)+(r_4*r_4)+(r_5*r_5) ;
\n
F12_RealRMat_s_a12 = r_11 ;
\n
F12_RealRMat_s_a20 = r_10 ;
\n
F12_RealRMat_s_a21 = r_11 ;
\n
F12_RealRMat_s_a22 = (r_7*r_7)+(r_8*r_8)+(r_9*r_9)
\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}"
},
"children"
:
{
"Unfold 'EqS12_RealRMat_s'"
:
[
{
"prover"
:
"Z3:4.8.6:noBV"
,
"verdict"
:
"unknown"
},
{
"prover"
:
"Z3:4.8.6:counterexamples"
,
"verdict"
:
"unknown"
},
{
"prover"
:
"Z3:4.8.6"
,
"verdict"
:
"unknown"
},
{
"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"
:
15
.
}
]
}
}
]
}
}
]
}
}
]
}
}
]
}
}
]
}
}
]
sw/airborne/.frama-c/wp/script/lemma_rotation_matrix_to_eq.json
0 → 100644
View file @
b1951d7f
[
{
"header"
:
"Definition"
,
"tactic"
:
"Wp.unfold"
,
"params"
:
{},
"select"
:
{
"select"
:
"inside-goal"
,
"occur"
:
0
,
"target"
:
"(P_rotation_matrix (L_l_RMat_of_FloatRMat Mf32_0 rm_0))"
,
"pattern"
:
"P_rotation_matrixL_l_RMat_of_FloatRMat"
},
"children"
:
{
"Unfold 'P_rotation_matrix'"
:
[
{
"prover"
:
"Z3:4.8.6:counterexamples"
,
"verdict"
:
"valid"
,
"time"
:
13.61
,
"steps"
:
27265631
}
]
}
}
]
sw/airborne/math/pprz_algebra_float_convert_rmat_frama_c.h
View file @
b1951d7f
...
...
@@ -126,6 +126,21 @@ logic RealRMat l_RMat_of_FloatRMat(struct FloatRMat *rmat) =
mult_RealRMat(rmat, transpose(rmat)) == id_rmat;
*/
/*@
lemma rotation_matrix_to_eq:
\forall struct FloatRMat *rm;
\valid(rm)
==>
(rotation_matrix(l_RMat_of_FloatRMat(rm)) <==>
(SQR(rm->m[0]) + SQR(rm->m[1]) + SQR(rm->m[2]) == 1.0
&& SQR(rm->m[3]) + SQR(rm->m[4]) + SQR(rm->m[5]) == 1.0
&& SQR(rm->m[6]) + SQR(rm->m[7]) + SQR(rm->m[8]) == 1.0
&& rm->m[0] * rm->m[3] + rm->m[1] * rm->m[4] + rm->m[2] * rm->m[5] == 0
&& rm->m[0] * rm->m[6] + rm->m[1] * rm->m[7] + rm->m[2] * rm->m[8] == 0
&& rm->m[3] * rm->m[6] + rm->m[4] * rm->m[7] + rm->m[5] * rm->m[8] == 0
));
*/
/*******************************
* CONVERT QUAT TO RMAT
* *****************************/
...
...
Write
Preview
Markdown
is supported
0%
Try again
or
attach a new file
.
Attach a file
Cancel
You are about to add
0
people
to the discussion. Proceed with caution.
Finish editing this message first!
Cancel
Please
register
or
sign in
to comment