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
085c1207
Commit
085c1207
authored
Apr 16, 2021
by
POLLIEN Baptiste
Browse files
Proof for rmat_of_eulers_312
parent
d5de5e85
Changes
20
Expand all
Hide whitespace changes
Inline
Side-by-side
Showing
20 changed files
with
299 additions
and
584 deletions
+299
-584
sw/airborne/.frama-c/wp/interactive/lemma_float_rmat_of_eulers_321_1.v
...frama-c/wp/interactive/lemma_float_rmat_of_eulers_321_1.v
+13
-51
sw/airborne/.frama-c/wp/interactive/lemma_float_rmat_of_eulers_321_2.v
...frama-c/wp/interactive/lemma_float_rmat_of_eulers_321_2.v
+22
-70
sw/airborne/.frama-c/wp/script/float_quat_of_rmat_a00_max_ensures.json
...frama-c/wp/script/float_quat_of_rmat_a00_max_ensures.json
+21
-3
sw/airborne/.frama-c/wp/script/float_quat_of_rmat_a11_max_ensures.json
...frama-c/wp/script/float_quat_of_rmat_a11_max_ensures.json
+6
-2
sw/airborne/.frama-c/wp/script/float_quat_of_rmat_a22_max_ensures.json
...frama-c/wp/script/float_quat_of_rmat_a22_max_ensures.json
+8
-4
sw/airborne/.frama-c/wp/script/float_quat_of_rmat_assert.json
...irborne/.frama-c/wp/script/float_quat_of_rmat_assert.json
+15
-9
sw/airborne/.frama-c/wp/script/float_quat_of_rmat_assert_12.json
...orne/.frama-c/wp/script/float_quat_of_rmat_assert_12.json
+0
-28
sw/airborne/.frama-c/wp/script/float_quat_of_rmat_assert_2.json
...borne/.frama-c/wp/script/float_quat_of_rmat_assert_2.json
+16
-10
sw/airborne/.frama-c/wp/script/float_quat_of_rmat_trace_pos_ensures.json
...ama-c/wp/script/float_quat_of_rmat_trace_pos_ensures.json
+18
-1
sw/airborne/.frama-c/wp/script/float_rmat_of_eulers_312_ensures.json
.../.frama-c/wp/script/float_rmat_of_eulers_312_ensures.json
+88
-0
sw/airborne/.frama-c/wp/script/float_rmat_of_quat_assert.json
...irborne/.frama-c/wp/script/float_rmat_of_quat_assert.json
+5
-7
sw/airborne/.frama-c/wp/script/float_rmat_of_quat_assert_2.json
...borne/.frama-c/wp/script/float_rmat_of_quat_assert_2.json
+3
-3
sw/airborne/.frama-c/wp/script/float_rmat_of_quat_assert_3.json
...borne/.frama-c/wp/script/float_rmat_of_quat_assert_3.json
+5
-5
sw/airborne/.frama-c/wp/script/float_rmat_of_quat_assert_4.json
...borne/.frama-c/wp/script/float_rmat_of_quat_assert_4.json
+3
-3
sw/airborne/.frama-c/wp/script/float_rmat_of_quat_ensures.json
...rborne/.frama-c/wp/script/float_rmat_of_quat_ensures.json
+24
-219
sw/airborne/.frama-c/wp/script/float_rmat_of_quat_ensures_2.json
...orne/.frama-c/wp/script/float_rmat_of_quat_ensures_2.json
+37
-165
sw/airborne/frama-c-analysis.sh
sw/airborne/frama-c-analysis.sh
+1
-1
sw/airborne/math/pprz_algebra_float.c
sw/airborne/math/pprz_algebra_float.c
+13
-1
sw/airborne/math/pprz_algebra_float.h
sw/airborne/math/pprz_algebra_float.h
+1
-1
sw/airborne/math/pprz_algebra_float_convert_rmat_frama_c.h
sw/airborne/math/pprz_algebra_float_convert_rmat_frama_c.h
+0
-1
No files found.
sw/airborne/.frama-c/wp/interactive/lemma_float_rmat_of_eulers_321_1.v
View file @
085c1207
...
...
@@ -99,21 +99,6 @@ Axiom cdiv_closed_remainder :
(
0
%
Z
<=
(
b
-
a
)
%
Z
)
%
Z
/
\
((
b
-
a
)
%
Z
<
n
)
%
Z
->
((
ZArith
.
BinInt
.
Z
.
rem
a
n
)
=
(
ZArith
.
BinInt
.
Z
.
rem
b
n
))
->
(
a
=
b
).
Axiom
Q_factorisation
:
forall
(
a
:
Reals
.
Rdefinitions
.
R
)
(
b
:
Reals
.
Rdefinitions
.
R
)
(
c
:
Reals
.
Rdefinitions
.
R
),
((
a
*
(
b
+
c
)
%
R
)
%
R
=
((
a
*
b
)
%
R
+
(
a
*
c
)
%
R
)
%
R
).
Axiom
Q_remarkable_identity_2
:
forall
(
a
:
Reals
.
Rdefinitions
.
R
)
(
b
:
Reals
.
Rdefinitions
.
R
),
let
r
:=
(
a
+
((
-
1
%
R
)
%
R
*
b
)
%
R
)
%
R
in
((((
2
%
R
*
a
)
%
R
*
b
)
%
R
+
(
r
*
r
)
%
R
)
%
R
=
((
a
*
a
)
%
R
+
(
b
*
b
)
%
R
)
%
R
).
Axiom
Q_remarkable_identity_1
:
forall
(
a
:
Reals
.
Rdefinitions
.
R
)
(
b
:
Reals
.
Rdefinitions
.
R
),
let
r
:=
(
a
+
b
)
%
R
in
((
r
*
r
)
%
R
=
(((
a
*
a
)
%
R
+
(
b
*
b
)
%
R
)
%
R
+
((
2
%
R
*
a
)
%
R
*
b
)
%
R
)
%
R
).
Axiom
abs_def
:
forall
(
x
:
Numbers
.
BinNums
.
Z
),
((
0
%
Z
<=
x
)
%
Z
->
((
ZArith
.
BinInt
.
Z
.
abs
x
)
=
x
))
/
\
...
...
@@ -136,30 +121,6 @@ Axiom Q_cos_sin_square :
let
r
:=
Reals
.
Rtrigo_def
.
sin
a
in
let
r1
:=
Reals
.
Rtrigo_def
.
cos
a
in
(((
r
*
r
)
%
R
+
(
r1
*
r1
)
%
R
)
%
R
=
1
%
R
).
Axiom
Q_sin_sub
:
forall
(
a
:
Reals
.
Rdefinitions
.
R
)
(
b
:
Reals
.
Rdefinitions
.
R
),
(((
Reals
.
Rtrigo_def
.
sin
a
)
*
(
Reals
.
Rtrigo_def
.
cos
b
))
%
R
=
((
Reals
.
Rtrigo_def
.
sin
(
a
+
((
-
1
%
R
)
%
R
*
b
)
%
R
)
%
R
)
+
((
Reals
.
Rtrigo_def
.
sin
b
)
*
(
Reals
.
Rtrigo_def
.
cos
a
))
%
R
)
%
R
).
Axiom
Q_sin_add
:
forall
(
a
:
Reals
.
Rdefinitions
.
R
)
(
b
:
Reals
.
Rdefinitions
.
R
),
((((
Reals
.
Rtrigo_def
.
sin
a
)
*
(
Reals
.
Rtrigo_def
.
cos
b
))
%
R
+
((
Reals
.
Rtrigo_def
.
sin
b
)
*
(
Reals
.
Rtrigo_def
.
cos
a
))
%
R
)
%
R
=
(
Reals
.
Rtrigo_def
.
sin
(
a
+
b
)
%
R
)).
Axiom
Q_cos_sub
:
forall
(
a
:
Reals
.
Rdefinitions
.
R
)
(
b
:
Reals
.
Rdefinitions
.
R
),
((((
Reals
.
Rtrigo_def
.
sin
a
)
*
(
Reals
.
Rtrigo_def
.
sin
b
))
%
R
+
((
Reals
.
Rtrigo_def
.
cos
a
)
*
(
Reals
.
Rtrigo_def
.
cos
b
))
%
R
)
%
R
=
(
Reals
.
Rtrigo_def
.
cos
(
a
+
((
-
1
%
R
)
%
R
*
b
)
%
R
)
%
R
)).
Axiom
Q_cos_add
:
forall
(
a
:
Reals
.
Rdefinitions
.
R
)
(
b
:
Reals
.
Rdefinitions
.
R
),
(((
Reals
.
Rtrigo_def
.
cos
a
)
*
(
Reals
.
Rtrigo_def
.
cos
b
))
%
R
=
((
Reals
.
Rtrigo_def
.
cos
(
a
+
b
)
%
R
)
+
((
Reals
.
Rtrigo_def
.
sin
a
)
*
(
Reals
.
Rtrigo_def
.
sin
b
))
%
R
)
%
R
).
(
*
Why3
assumption
*
)
Inductive
S12_RealRMat_s
:=
|
S12_RealRMat_s1
:
Reals
.
Rdefinitions
.
R
->
Reals
.
Rdefinitions
.
R
->
...
...
@@ -647,6 +608,17 @@ Proof.
auto
.
Qed
.
Lemma
sin_to_cos_sqr
:
forall
r
,
Rpow_def
.
pow
(
Rtrigo_def
.
sin
r
)
2
=
(
1
%
R
-
Rpow_def
.
pow
(
Rtrigo_def
.
cos
r
)
2
)
%
R
.
Proof
.
intros
r
.
ring_simplify
.
rewrite
<-
Q_cos_sin_square
with
(
a
:=
r
).
ring_simplify
.
auto
.
Qed
.
(
*
Why3
goal
*
)
Theorem
wp_goal
:
forall
(
r
:
Reals
.
Rdefinitions
.
R
)
(
r1
:
Reals
.
Rdefinitions
.
R
)
...
...
@@ -663,20 +635,10 @@ Theorem wp_goal :
(
*
Why3
intros
r
r1
r2
r3
r4
r5
r6
r7
r8
r9
r10
.
*
)
Proof
.
intros
r
r1
r2
r3
r4
r5
r6
r7
r8
r9
r10
.
unfold
r9
,
r10
.
unfold
r9
,
r10
,
r3
,
r4
,
r5
,
r6
,
r7
,
r8
.
ring_simplify
.
rewrite
Rmult_comm
with
(
r1
:=
Rpow_def
.
pow
r5
2
).
rewrite
Rplus_assoc
.
rewrite
<-
Rmult_plus_distr_l
.
unfold
r5
,
r8
;
rewrite
sin_cos_sqr
;
repeat
rewrite
Rmult_comm
with
(
r2
:=
1
%
R
);
repeat
rewrite
Rmult_1_l
.
repeat
rewrite
sin_to_cos_sqr
.
ring_simplify
.
repeat
rewrite
Rmult_assoc
.
repeat
rewrite
<-
Rmult_plus_distr_l
with
(
r1
:=
Rpow_def
.
pow
r3
2
).
rewrite
Rmult_comm
with
(
r1
:=
Rpow_def
.
pow
(
Rtrigo_def
.
sin
r2
)
2
).
rewrite
Rplus_assoc
.
rewrite
<-
Rmult_plus_distr_l
.
rewrite
sin_cos_sqr
;
repeat
rewrite
Rmult_comm
with
(
r2
:=
1
%
R
);
repeat
rewrite
Rmult_1_l
.
unfold
r4
,
r7
.
rewrite
Rplus_comm
with
(
r1
:=
Rpow_def
.
pow
(
Rtrigo_def
.
cos
r1
)
2
).
rewrite
sin_cos_sqr
;
repeat
rewrite
Rmult_comm
with
(
r2
:=
1
%
R
);
repeat
rewrite
Rmult_1_l
.
unfold
r3
,
r6
.
rewrite
sin_cos_sqr
.
auto
.
Qed
.
sw/airborne/.frama-c/wp/interactive/lemma_float_rmat_of_eulers_321_2.v
View file @
085c1207
...
...
@@ -116,19 +116,6 @@ Axiom sqrt_0 : ((Reals.R_sqrt.sqrt 0%R) = 0%R).
Axiom
sqrt_1
:
((
Reals
.
R_sqrt
.
sqrt
1
%
R
)
=
1
%
R
).
Axiom
Q_float_rmat_of_eulers_321
:
forall
(
a
:
Reals
.
Rdefinitions
.
R
)
(
b
:
Reals
.
Rdefinitions
.
R
)
(
c
:
Reals
.
Rdefinitions
.
R
),
let
r
:=
Reals
.
Rtrigo_def
.
sin
a
in
let
r1
:=
Reals
.
Rtrigo_def
.
cos
b
in
let
r2
:=
Reals
.
Rtrigo_def
.
sin
c
in
let
r3
:=
Reals
.
Rtrigo_def
.
cos
a
in
let
r4
:=
Reals
.
Rtrigo_def
.
sin
b
in
let
r5
:=
Reals
.
Rtrigo_def
.
cos
c
in
let
r6
:=
(((
-
1
%
R
)
%
R
*
(
r2
*
r3
)
%
R
)
%
R
+
((
r
*
r4
)
%
R
*
r5
)
%
R
)
%
R
in
let
r7
:=
((
r3
*
r5
)
%
R
+
((
r
*
r4
)
%
R
*
r2
)
%
R
)
%
R
in
((((((
r
*
r
)
%
R
*
r1
)
%
R
*
r1
)
%
R
+
(
r6
*
r6
)
%
R
)
%
R
+
(
r7
*
r7
)
%
R
)
%
R
=
1
%
R
).
Axiom
Q_float_rmat_of_eulers_321_1
:
forall
(
a
:
Reals
.
Rdefinitions
.
R
)
(
b
:
Reals
.
Rdefinitions
.
R
)
(
c
:
Reals
.
Rdefinitions
.
R
),
...
...
@@ -142,50 +129,11 @@ Axiom Q_float_rmat_of_eulers_321_1 :
let
r7
:=
((
r3
*
r5
)
%
R
+
((
r
*
r4
)
%
R
*
r2
)
%
R
)
%
R
in
((((((
r
*
r
)
%
R
*
r1
)
%
R
*
r1
)
%
R
+
(
r6
*
r6
)
%
R
)
%
R
+
(
r7
*
r7
)
%
R
)
%
R
=
1
%
R
).
Axiom
Q_factorisation
:
forall
(
a
:
Reals
.
Rdefinitions
.
R
)
(
b
:
Reals
.
Rdefinitions
.
R
)
(
c
:
Reals
.
Rdefinitions
.
R
),
((
a
*
(
b
+
c
)
%
R
)
%
R
=
((
a
*
b
)
%
R
+
(
a
*
c
)
%
R
)
%
R
).
Axiom
Q_remarkable_identity_2
:
forall
(
a
:
Reals
.
Rdefinitions
.
R
)
(
b
:
Reals
.
Rdefinitions
.
R
),
let
r
:=
(
a
+
((
-
1
%
R
)
%
R
*
b
)
%
R
)
%
R
in
((((
2
%
R
*
a
)
%
R
*
b
)
%
R
+
(
r
*
r
)
%
R
)
%
R
=
((
a
*
a
)
%
R
+
(
b
*
b
)
%
R
)
%
R
).
Axiom
Q_remarkable_identity_1
:
forall
(
a
:
Reals
.
Rdefinitions
.
R
)
(
b
:
Reals
.
Rdefinitions
.
R
),
let
r
:=
(
a
+
b
)
%
R
in
((
r
*
r
)
%
R
=
(((
a
*
a
)
%
R
+
(
b
*
b
)
%
R
)
%
R
+
((
2
%
R
*
a
)
%
R
*
b
)
%
R
)
%
R
).
Axiom
Q_cos_sin_square
:
forall
(
a
:
Reals
.
Rdefinitions
.
R
),
let
r
:=
Reals
.
Rtrigo_def
.
sin
a
in
let
r1
:=
Reals
.
Rtrigo_def
.
cos
a
in
(((
r
*
r
)
%
R
+
(
r1
*
r1
)
%
R
)
%
R
=
1
%
R
).
Axiom
Q_sin_sub
:
forall
(
a
:
Reals
.
Rdefinitions
.
R
)
(
b
:
Reals
.
Rdefinitions
.
R
),
(((
Reals
.
Rtrigo_def
.
sin
a
)
*
(
Reals
.
Rtrigo_def
.
cos
b
))
%
R
=
((
Reals
.
Rtrigo_def
.
sin
(
a
+
((
-
1
%
R
)
%
R
*
b
)
%
R
)
%
R
)
+
((
Reals
.
Rtrigo_def
.
sin
b
)
*
(
Reals
.
Rtrigo_def
.
cos
a
))
%
R
)
%
R
).
Axiom
Q_sin_add
:
forall
(
a
:
Reals
.
Rdefinitions
.
R
)
(
b
:
Reals
.
Rdefinitions
.
R
),
((((
Reals
.
Rtrigo_def
.
sin
a
)
*
(
Reals
.
Rtrigo_def
.
cos
b
))
%
R
+
((
Reals
.
Rtrigo_def
.
sin
b
)
*
(
Reals
.
Rtrigo_def
.
cos
a
))
%
R
)
%
R
=
(
Reals
.
Rtrigo_def
.
sin
(
a
+
b
)
%
R
)).
Axiom
Q_cos_sub
:
forall
(
a
:
Reals
.
Rdefinitions
.
R
)
(
b
:
Reals
.
Rdefinitions
.
R
),
((((
Reals
.
Rtrigo_def
.
sin
a
)
*
(
Reals
.
Rtrigo_def
.
sin
b
))
%
R
+
((
Reals
.
Rtrigo_def
.
cos
a
)
*
(
Reals
.
Rtrigo_def
.
cos
b
))
%
R
)
%
R
=
(
Reals
.
Rtrigo_def
.
cos
(
a
+
((
-
1
%
R
)
%
R
*
b
)
%
R
)
%
R
)).
Axiom
Q_cos_add
:
forall
(
a
:
Reals
.
Rdefinitions
.
R
)
(
b
:
Reals
.
Rdefinitions
.
R
),
(((
Reals
.
Rtrigo_def
.
cos
a
)
*
(
Reals
.
Rtrigo_def
.
cos
b
))
%
R
=
((
Reals
.
Rtrigo_def
.
cos
(
a
+
b
)
%
R
)
+
((
Reals
.
Rtrigo_def
.
sin
a
)
*
(
Reals
.
Rtrigo_def
.
sin
b
))
%
R
)
%
R
).
(
*
Why3
assumption
*
)
Inductive
S12_RealRMat_s
:=
|
S12_RealRMat_s1
:
Reals
.
Rdefinitions
.
R
->
Reals
.
Rdefinitions
.
R
->
...
...
@@ -683,33 +631,37 @@ Proof.
apply
sin_cos_sqr
.
Qed
.
Lemma
sin_to_cos_sqr
:
forall
r
,
Rpow_def
.
pow
(
Rtrigo_def
.
sin
r
)
2
=
(
1
%
R
-
Rpow_def
.
pow
(
Rtrigo_def
.
cos
r
)
2
)
%
R
.
Proof
.
intros
r
.
ring_simplify
.
rewrite
<-
Q_cos_sin_square
with
(
a
:=
r
).
ring_simplify
.
auto
.
Qed
.
(
*
Why3
goal
*
)
Theorem
wp_goal
:
forall
(
r
:
Reals
.
Rdefinitions
.
R
)
(
r1
:
Reals
.
Rdefinitions
.
R
)
(
r2
:
Reals
.
Rdefinitions
.
R
),
let
r3
:=
Reals
.
Rtrigo_def
.
cos
r
in
let
r3
:=
Reals
.
Rtrigo_def
.
sin
r
in
let
r4
:=
Reals
.
Rtrigo_def
.
cos
r1
in
let
r5
:=
Reals
.
Rtrigo_def
.
sin
r
in
let
r6
:=
Reals
.
Rtrigo_def
.
cos
r
2
in
let
r5
:=
Reals
.
Rtrigo_def
.
sin
r
2
in
let
r6
:=
Reals
.
Rtrigo_def
.
cos
r
in
let
r7
:=
Reals
.
Rtrigo_def
.
sin
r1
in
let
r8
:=
Reals
.
Rtrigo_def
.
sin
r2
in
let
r9
:=
(((
-
1
%
R
)
%
R
*
(
r5
*
r6
)
%
R
)
%
R
+
((
r
7
*
r
8
)
%
R
*
r
3
)
%
R
)
%
R
in
let
r10
:=
((
r
5
*
r8
)
%
R
+
((
r
7
*
r
3
)
%
R
*
r
6
)
%
R
)
%
R
in
let
r8
:=
Reals
.
Rtrigo_def
.
cos
r2
in
let
r9
:=
(((
-
1
%
R
)
%
R
*
(
r5
*
r6
)
%
R
)
%
R
+
((
r
3
*
r
7
)
%
R
*
r
8
)
%
R
)
%
R
in
let
r10
:=
((
r
6
*
r8
)
%
R
+
((
r
3
*
r
7
)
%
R
*
r
5
)
%
R
)
%
R
in
((((((
r3
*
r3
)
%
R
*
r4
)
%
R
*
r4
)
%
R
+
(
r9
*
r9
)
%
R
)
%
R
+
(
r10
*
r10
)
%
R
)
%
R
=
1
%
R
).
(
*
Why3
intros
r
r1
r2
r3
r4
r5
r6
r7
r8
r9
r10
.
*
)
Proof
.
intros
r
r1
r2
r3
r4
r5
r6
r7
r8
r9
r10
.
unfold
r9
,
r10
.
ring_simplify
.
rewrite
Rplus_assoc
.
rewrite
<-
Rmult_plus_distr_l
.
unfold
r6
,
r8
.
rewrite
cos_sin_sqr
;
repeat
rewrite
Rmult_comm
with
(
r2
:=
1
%
R
);
repeat
rewrite
Rmult_1_l
.
repeat
rewrite
Rmult_assoc
.
repeat
rewrite
<-
Rmult_plus_distr_l
with
(
r1
:=
Rpow_def
.
pow
r3
2
).
rewrite
Rmult_comm
with
(
r1
:=
Rpow_def
.
pow
(
Rtrigo_def
.
cos
r2
)
2
).
rewrite
Rplus_assoc
.
rewrite
<-
Rmult_plus_distr_l
.
rewrite
cos_sin_sqr
;
repeat
rewrite
Rmult_comm
with
(
r2
:=
1
%
R
);
repeat
rewrite
Rmult_1_l
.
unfold
r4
,
r7
.
rewrite
Rplus_comm
with
(
r1
:=
Rpow_def
.
pow
(
Rtrigo_def
.
cos
r1
)
2
).
rewrite
sin_cos_sqr
;
repeat
rewrite
Rmult_comm
with
(
r2
:=
1
%
R
);
repeat
rewrite
Rmult_1_l
.
unfold
r3
,
r6
.
rewrite
cos_sin_sqr
.
unfold
r9
,
r10
,
r3
,
r4
,
r5
,
r6
,
r7
,
r8
.
ring_simplify
.
repeat
rewrite
sin_to_cos_sqr
.
ring_simplify
.
auto
.
Qed
.
sw/airborne/.frama-c/wp/script/float_quat_of_rmat_a00_max_ensures.json
View file @
085c1207
...
...
@@ -18,7 +18,7 @@
"select"
:
{
"select"
:
"inside-goal"
,
"occur"
:
0
,
"target"
:
"let a_0 = (shiftfield_F
6
_FloatRMat_m rm_0) in
\n
(L_transpose
\n
{
\n
F
9
_RealRMat_s_a00 = Mf32_0[(shift_float32 a_0 0)] ;
\n
F
9
_RealRMat_s_a01 = Mf32_0[(shift_float32 a_0 1)] ;
\n
F
9
_RealRMat_s_a02 = Mf32_0[(shift_float32 a_0 2)] ;
\n
F
9
_RealRMat_s_a10 = Mf32_0[(shift_float32 a_0 3)] ;
\n
F
9
_RealRMat_s_a11 = Mf32_0[(shift_float32 a_0 4)] ;
\n
F
9
_RealRMat_s_a12 = Mf32_0[(shift_float32 a_0 5)] ;
\n
F
9
_RealRMat_s_a20 = Mf32_0[(shift_float32 a_0 6)] ;
\n
F
9
_RealRMat_s_a21 = Mf32_0[(shift_float32 a_0 7)] ;
\n
F
9
_RealRMat_s_a22 = Mf32_0[(shift_float32 a_0 8)]
\n
})"
,
"target"
:
"let a_0 = (shiftfield_F
9
_FloatRMat_m rm_0) in
\n
(L_transpose
\n
{
\n
F
12
_RealRMat_s_a00 = Mf32_0[(shift_float32 a_0 0)] ;
\n
F
12
_RealRMat_s_a01 = Mf32_0[(shift_float32 a_0 1)] ;
\n
F
12
_RealRMat_s_a02 = Mf32_0[(shift_float32 a_0 2)] ;
\n
F
12
_RealRMat_s_a10 = Mf32_0[(shift_float32 a_0 3)] ;
\n
F
12
_RealRMat_s_a11 = Mf32_0[(shift_float32 a_0 4)] ;
\n
F
12
_RealRMat_s_a12 = Mf32_0[(shift_float32 a_0 5)] ;
\n
F
12
_RealRMat_s_a20 = Mf32_0[(shift_float32 a_0 6)] ;
\n
F
12
_RealRMat_s_a21 = Mf32_0[(shift_float32 a_0 7)] ;
\n
F
12
_RealRMat_s_a22 = Mf32_0[(shift_float32 a_0 8)]
\n
})"
,
"pattern"
:
"L_transpose{RealRMat_s}[][][][][]"
},
"children"
:
{
"Unfold 'L_transpose'"
:
...
...
@@ -28,11 +28,29 @@
"select"
:
{
"select"
:
"inside-goal"
,
"occur"
:
0
,
"target"
:
"let a_0 = (shiftfield_F
6
_FloatRMat_m rm_0) in
\n
(L_l_FloatQuat_of_RMat_0_max_1_
\n
{
\n
F
9
_RealRMat_s_a00 = Mf32_0[(shift_float32 a_0 0)] ;
\n
F
9
_RealRMat_s_a01 = Mf32_0[(shift_float32 a_0 3)] ;
\n
F
9
_RealRMat_s_a02 = Mf32_0[(shift_float32 a_0 6)] ;
\n
F
9
_RealRMat_s_a10 = Mf32_0[(shift_float32 a_0 1)] ;
\n
F
9
_RealRMat_s_a11 = Mf32_0[(shift_float32 a_0 4)] ;
\n
F
9
_RealRMat_s_a12 = Mf32_0[(shift_float32 a_0 7)] ;
\n
F
9
_RealRMat_s_a20 = Mf32_0[(shift_float32 a_0 2)] ;
\n
F
9
_RealRMat_s_a21 = Mf32_0[(shift_float32 a_0 5)] ;
\n
F
9
_RealRMat_s_a22 = Mf32_0[(shift_float32 a_0 8)]
\n
})"
,
"target"
:
"let a_0 = (shiftfield_F
9
_FloatRMat_m rm_0) in
\n
(L_l_FloatQuat_of_RMat_0_max_1_
\n
{
\n
F
12
_RealRMat_s_a00 = Mf32_0[(shift_float32 a_0 0)] ;
\n
F
12
_RealRMat_s_a01 = Mf32_0[(shift_float32 a_0 3)] ;
\n
F
12
_RealRMat_s_a02 = Mf32_0[(shift_float32 a_0 6)] ;
\n
F
12
_RealRMat_s_a10 = Mf32_0[(shift_float32 a_0 1)] ;
\n
F
12
_RealRMat_s_a11 = Mf32_0[(shift_float32 a_0 4)] ;
\n
F
12
_RealRMat_s_a12 = Mf32_0[(shift_float32 a_0 7)] ;
\n
F
12
_RealRMat_s_a20 = Mf32_0[(shift_float32 a_0 2)] ;
\n
F
12
_RealRMat_s_a21 = Mf32_0[(shift_float32 a_0 5)] ;
\n
F
12
_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_'"
:
[
{
"header"
:
"Definition"
,
[
{
"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"
:
10.6951
,
"steps"
:
1663
},
{
"header"
:
"Definition"
,
"tactic"
:
"Wp.unfold"
,
"params"
:
{},
"select"
:
...
...
sw/airborne/.frama-c/wp/script/float_quat_of_rmat_a11_max_ensures.json
View file @
085c1207
...
...
@@ -18,11 +18,15 @@
"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
F
9
_RealRMat_s_a01 = a_0.F
9
_RealRMat_s_a10 ;
\n
F
9
_RealRMat_s_a02 = a_0.F
9
_RealRMat_s_a20 ;
\n
F
9
_RealRMat_s_a10 = a_0.F
9
_RealRMat_s_a01 ;
\n
F
9
_RealRMat_s_a12 = a_0.F
9
_RealRMat_s_a21 ;
\n
F
9
_RealRMat_s_a20 = a_0.F
9
_RealRMat_s_a02 ;
\n
F
9
_RealRMat_s_a21 = a_0.F
9
_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
F
12
_RealRMat_s_a01 = a_0.F
12
_RealRMat_s_a10 ;
\n
F
12
_RealRMat_s_a02 = a_0.F
12
_RealRMat_s_a20 ;
\n
F
12
_RealRMat_s_a10 = a_0.F
12
_RealRMat_s_a01 ;
\n
F
12
_RealRMat_s_a12 = a_0.F
12
_RealRMat_s_a21 ;
\n
F
12
_RealRMat_s_a20 = a_0.F
12
_RealRMat_s_a02 ;
\n
F
12
_RealRMat_s_a21 = a_0.F
12
_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_'"
:
[
{
"header"
:
"Definition"
,
[
{
"prover"
:
"Alt-Ergo:2.3.3"
,
"verdict"
:
"valid"
,
"time"
:
7.8582
,
"steps"
:
1632
},
{
"header"
:
"Definition"
,
"tactic"
:
"Wp.unfold"
,
"params"
:
{},
"select"
:
...
...
sw/airborne/.frama-c/wp/script/float_quat_of_rmat_a22_max_ensures.json
View file @
085c1207
...
...
@@ -20,7 +20,7 @@
"at"
:
3
,
"kind"
:
"have"
,
"occur"
:
0
,
"target"
:
"(L_trace_2_ Mf32_
27
rm_0)"
,
"target"
:
"(L_trace_2_ Mf32_
1
rm_0)"
,
"pattern"
:
"L_trace_2_$Mf32$rm"
},
"children"
:
{
"Unfold 'L_trace_2_'"
:
...
...
@@ -32,7 +32,7 @@
"at"
:
3
,
"kind"
:
"have"
,
"occur"
:
0
,
"target"
:
"(L_trace_1_ (L_l_RMat_of_FloatRMat Mf32_
27
rm_0))"
,
"target"
:
"(L_trace_1_ (L_l_RMat_of_FloatRMat Mf32_
1
rm_0))"
,
"pattern"
:
"L_trace_1_L_l_RMat_of_FloatRMat$Mf32"
},
"children"
:
{
"Unfold 'L_trace_1_'"
:
...
...
@@ -52,11 +52,15 @@
"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
F
9
_RealRMat_s_a01 = a_0.F
9
_RealRMat_s_a10 ;
\n
F
9
_RealRMat_s_a02 = a_0.F
9
_RealRMat_s_a20 ;
\n
F
9
_RealRMat_s_a10 = a_0.F
9
_RealRMat_s_a01 ;
\n
F
9
_RealRMat_s_a12 = a_0.F
9
_RealRMat_s_a21 ;
\n
F
9
_RealRMat_s_a20 = a_0.F
9
_RealRMat_s_a02 ;
\n
F
9
_RealRMat_s_a21 = a_0.F
9
_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
F
12
_RealRMat_s_a01 = a_0.F
12
_RealRMat_s_a10 ;
\n
F
12
_RealRMat_s_a02 = a_0.F
12
_RealRMat_s_a20 ;
\n
F
12
_RealRMat_s_a10 = a_0.F
12
_RealRMat_s_a01 ;
\n
F
12
_RealRMat_s_a12 = a_0.F
12
_RealRMat_s_a21 ;
\n
F
12
_RealRMat_s_a20 = a_0.F
12
_RealRMat_s_a02 ;
\n
F
12
_RealRMat_s_a21 = a_0.F
12
_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_'"
:
[
{
"header"
:
"Definition"
,
[
{
"prover"
:
"Alt-Ergo:2.3.3"
,
"verdict"
:
"valid"
,
"time"
:
2.0645
,
"steps"
:
1001
},
{
"header"
:
"Definition"
,
"tactic"
:
"Wp.unfold"
,
"params"
:
{},
"select"
:
...
...
sw/airborne/.frama-c/wp/script/float_quat_of_rmat_assert.json
View file @
085c1207
[
{
"header"
:
"Definition"
,
"tactic"
:
"Wp.unfold"
,
"params"
:
{},
"select"
:
{
"select"
:
"inside-step"
,
"at"
:
4
,
"kind"
:
"have"
,
"occur"
:
0
,
"target"
:
"(L_l_RMat_of_FloatRMat Mf32_
6
rm_0)"
,
"select"
:
{
"select"
:
"inside-step"
,
"at"
:
2
,
"kind"
:
"have"
,
"occur"
:
0
,
"target"
:
"(L_l_RMat_of_FloatRMat Mf32_
5
rm_0)"
,
"pattern"
:
"L_l_RMat_of_FloatRMat$Mf32$rm"
},
"children"
:
{
"Unfold 'L_l_RMat_of_FloatRMat'"
:
[
{
"header"
:
"Definition"
,
"tactic"
:
"Wp.unfold"
,
"params"
:
{},
"select"
:
{
"select"
:
"inside-step"
,
"at"
:
4
,
"at"
:
2
,
"kind"
:
"have"
,
"occur"
:
0
,
"target"
:
"let a_0 = (shiftfield_F
6
_FloatRMat_m rm_0) in
\n
(P_rotation_matrix
\n
{
\n
F
9
_RealRMat_s_a00 = Mf32_
6
[(shift_float32 a_0 0)] ;
\n
F
9
_RealRMat_s_a01 = Mf32_
6
[(shift_float32 a_0 1)] ;
\n
F
9
_RealRMat_s_a02 = Mf32_
6
[(shift_float32 a_0 2)] ;
\n
F
9
_RealRMat_s_a10 = Mf32_
6
[(shift_float32 a_0 3)] ;
\n
F
9
_RealRMat_s_a11 = Mf32_
6
[(shift_float32 a_0 4)] ;
\n
F
9
_RealRMat_s_a12 = Mf32_
6
[(shift_float32 a_0 5)] ;
\n
F
9
_RealRMat_s_a20 = Mf32_
6
[(shift_float32 a_0 6)] ;
\n
F
9
_RealRMat_s_a21 = Mf32_
6
[(shift_float32 a_0 7)] ;
\n
F
9
_RealRMat_s_a22 = Mf32_
6
[(shift_float32 a_0 8)]
\n
})"
,
"target"
:
"let a_0 = (shiftfield_F
9
_FloatRMat_m rm_0) in
\n
(P_rotation_matrix
\n
{
\n
F
12
_RealRMat_s_a00 = Mf32_
5
[(shift_float32 a_0 0)] ;
\n
F
12
_RealRMat_s_a01 = Mf32_
5
[(shift_float32 a_0 1)] ;
\n
F
12
_RealRMat_s_a02 = Mf32_
5
[(shift_float32 a_0 2)] ;
\n
F
12
_RealRMat_s_a10 = Mf32_
5
[(shift_float32 a_0 3)] ;
\n
F
12
_RealRMat_s_a11 = Mf32_
5
[(shift_float32 a_0 4)] ;
\n
F
12
_RealRMat_s_a12 = Mf32_
5
[(shift_float32 a_0 5)] ;
\n
F
12
_RealRMat_s_a20 = Mf32_
5
[(shift_float32 a_0 6)] ;
\n
F
12
_RealRMat_s_a21 = Mf32_
5
[(shift_float32 a_0 7)] ;
\n
F
12
_RealRMat_s_a22 = Mf32_
5
[(shift_float32 a_0 8)]
\n
})"
,
"pattern"
:
"P_rotation_matrix{RealRMat_s}[][]"
},
"children"
:
{
"Unfold 'P_rotation_matrix'"
:
[
{
"header"
:
"Definition"
,
...
...
@@ -17,10 +17,10 @@
"params"
:
{},
"select"
:
{
"select"
:
"inside-step"
,
"at"
:
4
,
"at"
:
2
,
"kind"
:
"have"
,
"occur"
:
0
,
"target"
:
"let a_0 = (shiftfield_F
6
_FloatRMat_m rm_0) in
\n
(L_transpose
\n
{
\n
F
9
_RealRMat_s_a00 = Mf32_
6
[(shift_float32 a_0 0)] ;
\n
F
9
_RealRMat_s_a01 = Mf32_
6
[(shift_float32 a_0 1)] ;
\n
F
9
_RealRMat_s_a02 = Mf32_
6
[(shift_float32 a_0 2)] ;
\n
F
9
_RealRMat_s_a10 = Mf32_
6
[(shift_float32 a_0 3)] ;
\n
F
9
_RealRMat_s_a11 = Mf32_
6
[(shift_float32 a_0 4)] ;
\n
F
9
_RealRMat_s_a12 = Mf32_
6
[(shift_float32 a_0 5)] ;
\n
F
9
_RealRMat_s_a20 = Mf32_
6
[(shift_float32 a_0 6)] ;
\n
F
9
_RealRMat_s_a21 = Mf32_
6
[(shift_float32 a_0 7)] ;
\n
F
9
_RealRMat_s_a22 = Mf32_
6
[(shift_float32 a_0 8)]
\n
})"
,
"target"
:
"let a_0 = (shiftfield_F
9
_FloatRMat_m rm_0) in
\n
(L_transpose
\n
{
\n
F
12
_RealRMat_s_a00 = Mf32_
5
[(shift_float32 a_0 0)] ;
\n
F
12
_RealRMat_s_a01 = Mf32_
5
[(shift_float32 a_0 1)] ;
\n
F
12
_RealRMat_s_a02 = Mf32_
5
[(shift_float32 a_0 2)] ;
\n
F
12
_RealRMat_s_a10 = Mf32_
5
[(shift_float32 a_0 3)] ;
\n
F
12
_RealRMat_s_a11 = Mf32_
5
[(shift_float32 a_0 4)] ;
\n
F
12
_RealRMat_s_a12 = Mf32_
5
[(shift_float32 a_0 5)] ;
\n
F
12
_RealRMat_s_a20 = Mf32_
5
[(shift_float32 a_0 6)] ;
\n
F
12
_RealRMat_s_a21 = Mf32_
5
[(shift_float32 a_0 7)] ;
\n
F
12
_RealRMat_s_a22 = Mf32_
5
[(shift_float32 a_0 8)]
\n
})"
,
"pattern"
:
"L_transpose{RealRMat_s}[][][][][]"
},
"children"
:
{
"Unfold 'L_transpose'"
:
...
...
@@ -29,14 +29,20 @@
"params"
:
{},
"select"
:
{
"select"
:
"inside-step"
,
"at"
:
4
,
"at"
:
2
,
"kind"
:
"have"
,
"occur"
:
0
,
"target"
:
"let a_0 = (shiftfield_F
6
_FloatRMat_m rm_0) in
\n
let r_0 = Mf32_
6
[(shift_float32 a_0 0)] in
\n
let r_1 = Mf32_
6
[(shift_float32 a_0 1)] in
\n
let r_2 = Mf32_
6
[(shift_float32 a_0 2)] in
\n
let r_3 = Mf32_
6
[(shift_float32 a_0 3)] in
\n
let r_4 = Mf32_
6
[(shift_float32 a_0 4)] in
\n
let r_5 = Mf32_
6
[(shift_float32 a_0 5)] in
\n
let r_6 = Mf32_
6
[(shift_float32 a_0 6)] in
\n
let r_7 = Mf32_
6
[(shift_float32 a_0 7)] in
\n
let r_8 = Mf32_
6
[(shift_float32 a_0 8)] in
\n
(L_mult_RealRMat
\n
{
\n
F
9
_RealRMat_s_a00 = r_0 ;
\n
F
9
_RealRMat_s_a01 = r_1 ;
\n
F
9
_RealRMat_s_a02 = r_2 ;
\n
F
9
_RealRMat_s_a10 = r_3 ;
\n
F
9
_RealRMat_s_a11 = r_4 ;
\n
F
9
_RealRMat_s_a12 = r_5 ;
\n
F
9
_RealRMat_s_a20 = r_6 ;
\n
F
9
_RealRMat_s_a21 = r_7 ;
\n
F
9
_RealRMat_s_a22 = r_8
\n
}
\n
{
\n
F
9
_RealRMat_s_a00 = r_0 ;
\n
F
9
_RealRMat_s_a01 = r_3 ;
\n
F
9
_RealRMat_s_a02 = r_6 ;
\n
F
9
_RealRMat_s_a10 = r_1 ;
\n
F
9
_RealRMat_s_a11 = r_4 ;
\n
F
9
_RealRMat_s_a12 = r_7 ;
\n
F
9
_RealRMat_s_a20 = r_2 ;
\n
F
9
_RealRMat_s_a21 = r_5 ;
\n
F
9
_RealRMat_s_a22 = r_8
\n
})"
,
"target"
:
"let a_0 = (shiftfield_F
9
_FloatRMat_m rm_0) in
\n
let r_0 = Mf32_
5
[(shift_float32 a_0 0)] in
\n
let r_1 = Mf32_
5
[(shift_float32 a_0 1)] in
\n
let r_2 = Mf32_
5
[(shift_float32 a_0 2)] in
\n
let r_3 = Mf32_
5
[(shift_float32 a_0 3)] in
\n
let r_4 = Mf32_
5
[(shift_float32 a_0 4)] in
\n
let r_5 = Mf32_
5
[(shift_float32 a_0 5)] in
\n
let r_6 = Mf32_
5
[(shift_float32 a_0 6)] in
\n
let r_7 = Mf32_
5
[(shift_float32 a_0 7)] in
\n
let r_8 = Mf32_
5
[(shift_float32 a_0 8)] in
\n
(L_mult_RealRMat
\n
{
\n
F
12
_RealRMat_s_a00 = r_0 ;
\n
F
12
_RealRMat_s_a01 = r_1 ;
\n
F
12
_RealRMat_s_a02 = r_2 ;
\n
F
12
_RealRMat_s_a10 = r_3 ;
\n
F
12
_RealRMat_s_a11 = r_4 ;
\n
F
12
_RealRMat_s_a12 = r_5 ;
\n
F
12
_RealRMat_s_a20 = r_6 ;
\n
F
12
_RealRMat_s_a21 = r_7 ;
\n
F
12
_RealRMat_s_a22 = r_8
\n
}
\n
{
\n
F
12
_RealRMat_s_a00 = r_0 ;
\n
F
12
_RealRMat_s_a01 = r_3 ;
\n
F
12
_RealRMat_s_a02 = r_6 ;
\n
F
12
_RealRMat_s_a10 = r_1 ;
\n
F
12
_RealRMat_s_a11 = r_4 ;
\n
F
12
_RealRMat_s_a12 = r_7 ;
\n
F
12
_RealRMat_s_a20 = r_2 ;
\n
F
12
_RealRMat_s_a21 = r_5 ;
\n
F
12
_RealRMat_s_a22 = r_8
\n
})"
,
"pattern"
:
"L_mult_RealRMat{RealRMat_s}{RealRMat_s}"
},
"children"
:
{
"Unfold 'L_mult_RealRMat'"
:
[
{
"header"
:
"Definition"
,
[
{
"prover"
:
"CVC4:1.9-prerelease:strings+counterexamples"
,
"verdict"
:
"valid"
,
"time"
:
0.25
},
{
"prover"
:
"Alt-Ergo:2.3.3"
,
"verdict"
:
"timeout"
,
"time"
:
10
.
},
{
"header"
:
"Definition"
,
"tactic"
:
"Wp.unfold"
,
"params"
:
{},
"select"
:
...
...
sw/airborne/.frama-c/wp/script/float_quat_of_rmat_assert_12.json
deleted
100644 → 0
View file @
d5de5e85
[
{
"prover"
:
"script"
,
"verdict"
:
"timeout"
,
"time"
:
10
.
},
{
"header"
:
"Definition"
,
"tactic"
:
"Wp.unfold"
,
"params"
:
{},
"select"
:
{
"select"
:
"clause-goal"
,
"target"
:
"let a_0 = (shiftfield_F6_FloatRMat_m rm_0) in
\n
let 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
\n
let m_0 = Mf32_6[(shiftfield_F4_FloatQuat_qi q_1)->1/2*r_0] in
\n
let r_1 = (2*r_0) in
\n
let 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
\n
let 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"
,
"verdict"
:
"timeout"
,
"time"
:
10
.
},
{
"prover"
:
"Alt-Ergo:2.3.3"
,
"verdict"
:
"timeout"
,
"time"
:
10
.
}
]
}
}
]
}
}
]
sw/airborne/.frama-c/wp/script/float_quat_of_rmat_assert_2.json
View file @
085c1207
[
{
"header"
:
"Definition"
,
"tactic"
:
"Wp.unfold"
,
"params"
:
{},
"select"
:
{
"select"
:
"inside-step"
,
"at"
:
4
,
"kind"
:
"have"
,
"occur"
:
0
,
"target"
:
"(L_l_RMat_of_FloatRMat Mf32_
6
rm_0)"
,
"select"
:
{
"select"
:
"inside-step"
,
"at"
:
2
,
"kind"
:
"have"
,
"occur"
:
0
,
"target"
:
"(L_l_RMat_of_FloatRMat Mf32_
5
rm_0)"
,
"pattern"
:
"L_l_RMat_of_FloatRMat$Mf32$rm"
},
"children"
:
{
"Unfold 'L_l_RMat_of_FloatRMat'"
:
[
{
"header"
:
"Definition"
,
"tactic"
:
"Wp.unfold"
,
"params"
:
{},
"select"
:
{
"select"
:
"inside-step"
,
"at"
:
4
,
"at"
:
2
,
"kind"
:
"have"
,
"occur"
:
0
,
"target"
:
"let a_0 = (shiftfield_F
6
_FloatRMat_m rm_0) in
\n
(P_rotation_matrix
\n
{
\n
F
9
_RealRMat_s_a00 = Mf32_
6
[(shift_float32 a_0 0)] ;
\n
F
9
_RealRMat_s_a01 = Mf32_
6
[(shift_float32 a_0 1)] ;
\n
F
9
_RealRMat_s_a02 = Mf32_
6
[(shift_float32 a_0 2)] ;
\n
F
9
_RealRMat_s_a10 = Mf32_
6
[(shift_float32 a_0 3)] ;
\n
F
9
_RealRMat_s_a11 = Mf32_
6
[(shift_float32 a_0 4)] ;
\n
F
9
_RealRMat_s_a12 = Mf32_
6
[(shift_float32 a_0 5)] ;
\n
F
9
_RealRMat_s_a20 = Mf32_
6
[(shift_float32 a_0 6)] ;
\n
F
9
_RealRMat_s_a21 = Mf32_
6
[(shift_float32 a_0 7)] ;
\n
F
9
_RealRMat_s_a22 = Mf32_
6
[(shift_float32 a_0 8)]
\n
})"
,
"target"
:
"let a_0 = (shiftfield_F
9
_FloatRMat_m rm_0) in
\n
(P_rotation_matrix
\n
{
\n
F
12
_RealRMat_s_a00 = Mf32_
5
[(shift_float32 a_0 0)] ;
\n
F
12
_RealRMat_s_a01 = Mf32_
5
[(shift_float32 a_0 1)] ;
\n
F
12
_RealRMat_s_a02 = Mf32_
5
[(shift_float32 a_0 2)] ;
\n
F
12
_RealRMat_s_a10 = Mf32_
5
[(shift_float32 a_0 3)] ;
\n
F
12
_RealRMat_s_a11 = Mf32_
5
[(shift_float32 a_0 4)] ;
\n
F
12
_RealRMat_s_a12 = Mf32_
5
[(shift_float32 a_0 5)] ;
\n
F
12
_RealRMat_s_a20 = Mf32_
5
[(shift_float32 a_0 6)] ;
\n
F
12
_RealRMat_s_a21 = Mf32_
5
[(shift_float32 a_0 7)] ;
\n
F
12
_RealRMat_s_a22 = Mf32_
5
[(shift_float32 a_0 8)]
\n
})"
,
"pattern"
:
"P_rotation_matrix{RealRMat_s}[][]"
},
"children"
:
{
"Unfold 'P_rotation_matrix'"
:
[
{
"header"
:
"Definition"
,
...
...
@@ -17,10 +17,10 @@
"params"
:
{},
"select"
:
{
"select"
:
"inside-step"
,
"at"
:
4
,
"at"
:
2
,
"kind"
:
"have"
,
"occur"
:
0
,
"target"
:
"let a_0 = (shiftfield_F
6
_FloatRMat_m rm_0) in
\n
(L_transpose
\n
{
\n
F
9
_RealRMat_s_a00 = Mf32_
6
[(shift_float32 a_0 0)] ;
\n
F
9
_RealRMat_s_a01 = Mf32_
6
[(shift_float32 a_0 1)] ;
\n
F
9
_RealRMat_s_a02 = Mf32_
6
[(shift_float32 a_0 2)] ;
\n
F
9
_RealRMat_s_a10 = Mf32_
6
[(shift_float32 a_0 3)] ;
\n
F
9
_RealRMat_s_a11 = Mf32_
6
[(shift_float32 a_0 4)] ;
\n
F
9
_RealRMat_s_a12 = Mf32_
6
[(shift_float32 a_0 5)] ;
\n
F
9
_RealRMat_s_a20 = Mf32_
6
[(shift_float32 a_0 6)] ;
\n
F
9
_RealRMat_s_a21 = Mf32_
6
[(shift_float32 a_0 7)] ;
\n
F
9
_RealRMat_s_a22 = Mf32_
6
[(shift_float32 a_0 8)]
\n
})"
,
"target"
:
"let a_0 = (shiftfield_F
9
_FloatRMat_m rm_0) in
\n
(L_transpose
\n
{
\n
F
12
_RealRMat_s_a00 = Mf32_
5
[(shift_float32 a_0 0)] ;
\n
F
12
_RealRMat_s_a01 = Mf32_
5
[(shift_float32 a_0 1)] ;
\n
F
12
_RealRMat_s_a02 = Mf32_
5
[(shift_float32 a_0 2)] ;
\n
F
12
_RealRMat_s_a10 = Mf32_
5
[(shift_float32 a_0 3)] ;
\n
F
12
_RealRMat_s_a11 = Mf32_
5
[(shift_float32 a_0 4)] ;
\n
F
12
_RealRMat_s_a12 = Mf32_
5
[(shift_float32 a_0 5)] ;
\n
F
12
_RealRMat_s_a20 = Mf32_
5
[(shift_float32 a_0 6)] ;
\n
F
12
_RealRMat_s_a21 = Mf32_
5
[(shift_float32 a_0 7)] ;
\n
F
12
_RealRMat_s_a22 = Mf32_
5
[(shift_float32 a_0 8)]
\n
})"
,
"pattern"
:
"L_transpose{RealRMat_s}[][][][][]"
},
"children"
:
{
"Unfold 'L_transpose'"
:
...
...
@@ -29,7 +29,7 @@
"params"
:
{},
"select"
:
{
"select"
:
"inside-step"
,
"at"
:
4
,
"at"
:
2
,
"kind"
:
"have"
,
"occur"
:
0
,
"target"
:
"L_id_rmat"
,
...
...
@@ -41,14 +41,20 @@
"params"
:
{},
"select"
:
{
"select"
:
"inside-step"
,
"at"
:
4
,
"at"
:
2
,
"kind"
:
"have"
,
"occur"
:
0
,
"target"
:
"let a_0 = (shiftfield_F
6
_FloatRMat_m rm_0) in
\n
let r_0 = Mf32_
6
[(shift_float32 a_0 0)] in
\n
let r_1 = Mf32_
6
[(shift_float32 a_0 1)] in
\n
let r_2 = Mf32_
6
[(shift_float32 a_0 2)] in
\n
let r_3 = Mf32_
6
[(shift_float32 a_0 3)] in
\n
let r_4 = Mf32_
6
[(shift_float32 a_0 4)] in
\n
let r_5 = Mf32_
6
[(shift_float32 a_0 5)] in
\n
let r_6 = Mf32_
6
[(shift_float32 a_0 6)] in
\n
let r_7 = Mf32_
6
[(shift_float32 a_0 7)] in
\n
let r_8 = Mf32_
6
[(shift_float32 a_0 8)] in
\n
(L_mult_RealRMat
\n
{
\n
F
9
_RealRMat_s_a00 = r_0 ;
\n
F
9
_RealRMat_s_a01 = r_1 ;
\n
F
9
_RealRMat_s_a02 = r_2 ;
\n
F
9
_RealRMat_s_a10 = r_3 ;
\n
F
9
_RealRMat_s_a11 = r_4 ;
\n
F
9
_RealRMat_s_a12 = r_5 ;
\n
F
9
_RealRMat_s_a20 = r_6 ;
\n
F
9
_RealRMat_s_a21 = r_7 ;
\n
F
9
_RealRMat_s_a22 = r_8
\n
}
\n
{
\n
F
9
_RealRMat_s_a00 = r_0 ;
\n
F
9
_RealRMat_s_a01 = r_3 ;
\n
F
9
_RealRMat_s_a02 = r_6 ;
\n
F
9
_RealRMat_s_a10 = r_1 ;
\n
F
9
_RealRMat_s_a11 = r_4 ;
\n
F
9
_RealRMat_s_a12 = r_7 ;
\n
F
9
_RealRMat_s_a20 = r_2 ;
\n
F
9
_RealRMat_s_a21 = r_5 ;
\n
F
9
_RealRMat_s_a22 = r_8
\n
})"
,
"target"
:
"let a_0 = (shiftfield_F
9
_FloatRMat_m rm_0) in
\n
let r_0 = Mf32_
5
[(shift_float32 a_0 0)] in
\n
let r_1 = Mf32_
5
[(shift_float32 a_0 1)] in
\n
let r_2 = Mf32_
5
[(shift_float32 a_0 2)] in
\n
let r_3 = Mf32_
5
[(shift_float32 a_0 3)] in
\n
let r_4 = Mf32_
5
[(shift_float32 a_0 4)] in
\n
let r_5 = Mf32_
5
[(shift_float32 a_0 5)] in
\n
let r_6 = Mf32_
5
[(shift_float32 a_0 6)] in
\n
let r_7 = Mf32_
5
[(shift_float32 a_0 7)] in
\n
let r_8 = Mf32_
5
[(shift_float32 a_0 8)] in
\n
(L_mult_RealRMat
\n
{
\n
F
12
_RealRMat_s_a00 = r_0 ;
\n
F
12
_RealRMat_s_a01 = r_1 ;
\n
F
12
_RealRMat_s_a02 = r_2 ;
\n
F
12
_RealRMat_s_a10 = r_3 ;
\n
F
12
_RealRMat_s_a11 = r_4 ;
\n
F
12
_RealRMat_s_a12 = r_5 ;
\n
F
12
_RealRMat_s_a20 = r_6 ;
\n
F
12
_RealRMat_s_a21 = r_7 ;
\n
F
12
_RealRMat_s_a22 = r_8
\n
}
\n
{
\n
F
12
_RealRMat_s_a00 = r_0 ;
\n
F
12
_RealRMat_s_a01 = r_3 ;
\n
F
12
_RealRMat_s_a02 = r_6 ;
\n
F
12
_RealRMat_s_a10 = r_1 ;
\n
F
12
_RealRMat_s_a11 = r_4 ;
\n
F
12
_RealRMat_s_a12 = r_7 ;
\n
F
12
_RealRMat_s_a20 = r_2 ;
\n
F
12
_RealRMat_s_a21 = r_5 ;
\n
F
12
_RealRMat_s_a22 = r_8
\n
})"
,
"pattern"
:
"L_mult_RealRMat{RealRMat_s}{RealRMat_s}"
},
"children"
:
{
"Unfold 'L_mult_RealRMat'"
:
[
{
"header"
:
"Definition"
,
[
{
"prover"
:
"CVC4:1.9-prerelease:strings+counterexamples"
,
"verdict"
:
"valid"
,
"time"
:
9.1
},
{
"prover"
:
"Alt-Ergo:2.3.3"
,
"verdict"
:
"timeout"
,
"time"
:
10
.
},
{
"header"
:
"Definition"
,
"tactic"
:
"Wp.unfold"
,
"params"
:
{},
"select"
:
...
...
sw/airborne/.frama-c/wp/script/float_quat_of_rmat_trace_pos_ensures.json
View file @
085c1207
...
...
@@ -32,7 +32,24 @@
"pattern"
:
"L_l_Quat_of_FloatQuat$Mf32$q"
},
"children"
:
{
"Unfold 'L_l_Quat_of_FloatQuat'"
:
[
{
"header"
:
"Definition"
,
[
{
"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"
:
10
.
},
{
"header"
:
"Definition"
,
"tactic"
:
"Wp.unfold"
,
"params"
:
{},
"select"
:
...
...
sw/airborne/.frama-c/wp/script/float_rmat_of_eulers_312_ensures.json
0 → 100644
View file @
085c1207
[
{
"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_9[(shiftfield_F10_FloatEulers_phi e_1)] in
\n
let r_1 = (
\\
sin r_0) in
\n
let r_2 = Mf32_9[(shiftfield_F10_FloatEulers_psi e_1)] in
\n
let r_3 = (
\\
sin r_2) in
\n
let r_4 = Mf32_9[(shiftfield_F10_FloatEulers_theta e_1)] in
\n
let r_5 = (
\\
sin r_4) in
\n
let r_6 = (
\\
cos r_2) in
\n
let r_7 = (
\\
cos r_4) in
\n
let r_8 = (
\\
cos r_0) in
\n
(L_l_RMat_of_FloatRMat
\n
Mf32_9[(shift_float32 a_0 0)->(r_6*r_7)-(r_1*r_3*r_5)]
\n
[(shift_float32 a_0 1)->(r_3*r_7)+(r_1*r_5*r_6)][(shift_float32 a_0 2)
\n
->-1*r_5*r_8][(shift_float32 a_0 3)->-1*r_3*r_8][(shift_float32 a_0 4)
\n
->r_8*r_6][(shift_float32 a_0 5)->r_1][(shift_float32 a_0 6)
\n
->(r_5*r_6)+(r_1*r_3*r_7)][(shift_float32 a_0 7)
\n
->(r_3*r_5)-(r_1*r_6*r_7)][(shift_float32 a_0 8)->r_8*r_7] rm_0)"
,
"pattern"
:
"L_l_RMat_of_FloatRMat[=]$rm[=]shift_float32"
},
"children"
:
{
"Unfold 'L_l_RMat_of_FloatRMat'"
:
[
{
"header"
:
"Definition"
,
"tactic"
:
"Wp.unfold"
,
"params"
:
{},
"select"
:
{
"select"
:
"clause-goal"
,
"target"
:
"let r_0 = Mf32_9[(shiftfield_F10_FloatEulers_phi e_1)] in
\n
let r_1 = (
\\
sin r_0) in
\n
let r_2 = Mf32_9[(shiftfield_F10_FloatEulers_psi e_1)] in
\n
let r_3 = (
\\
sin r_2) in
\n
let r_4 = Mf32_9[(shiftfield_F10_FloatEulers_theta e_1)] in
\n
let r_5 = (
\\
sin r_4) in
\n
let r_6 = (
\\
cos r_2) in
\n
let r_7 = (
\\
cos r_4) in
\n
let r_8 = (
\\
cos r_0) in
\n
(P_rotation_matrix
\n
{
\n
F12_RealRMat_s_a00 = (r_6*r_7)-(r_1*r_3*r_5) ;
\n
F12_RealRMat_s_a01 = (r_3*r_7)+(r_1*r_5*r_6) ;
\n
F12_RealRMat_s_a02 = -1*r_5*r_8 ;
\n
F12_RealRMat_s_a10 = -1*r_3*r_8 ;
\n
F12_RealRMat_s_a11 = r_8*r_6 ;
\n
F12_RealRMat_s_a12 = r_1 ;
\n
F12_RealRMat_s_a20 = (r_5*r_6)+(r_1*r_3*r_7) ;
\n
F12_RealRMat_s_a21 = (r_3*r_5)-(r_1*r_6*r_7) ;
\n
F12_RealRMat_s_a22 = r_8*r_7
\n
})"
,
"pattern"
:
"P_rotation_matrix{RealRMat_s}++*"
},
"children"
:
{
"Unfold 'P_rotation_matrix'"
:
[
{
"header"
:
"Definition"
,
"tactic"
:
"Wp.unfold"
,
"params"
:
{},
"select"
: