Commit 5c094437 authored by POLLIEN Baptiste's avatar POLLIEN Baptiste
Browse files

Updating code for frama-c 23 using ref memory model

parent fa35ea99
......@@ -14,20 +14,14 @@ Required software
-----------------
To run the verification, the following software are required:
- Frama-C, a compiled version from
[source](https://git.frama-c.com/pub/frama-c) using commit `3fa7de0c`
- Alt-Ergo 2.3.3
- Frama-C 23.0 (Vanadium)
- Alt-Ergo 2.4.0
- CVC4 1.9-prerelease
- Z3 4.8.6
- Coq 8.12.2
- Why3 1.3.3
- Why3 1.4.0
- ctags
**Note:** This specific version of Frama-C is needed because it
fixes a bug that prevented proving some goals. Also, the
_statement contracts_ are used in the proofs, but this feature
has been removed in newer versions.
How to launch the verification process
--------------------------------------
......@@ -93,9 +87,9 @@ the _preconditions_ specified in the contract of the function.
- `-wp-fct $FUNCTION`: launches the WP verification with the following
options:
- `-wp-cache update`: enables and uses cache.
- `-wp-model real+Cast`: enables the `real` model to represent the
- `-wp-model real+Cast+ref`: enables the `real` model to represent the
arithmetic on floating-point numbers. The `Cast` option enables the
usage of cast in the code.
usage of cast in the code. Finally, the `ref` option is used to enable optimization for reference parameters.
- `-wp-prover alt-ergo,cvc4-strings-ce,z3,z3-ce,z3-nobv,tip`:
adds the different provers needed to verify the goals.
- `-cpp-extra-args=-I../include`: adds the include directory of
......
......@@ -56,18 +56,17 @@
"params": {},
"select":
{ "select": "clause-step",
"at": 9,
"at": 13,
"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)])",
"target": "let a_0 = (shiftfield_F6_FloatRMat_m rm_0) in\n0<\n(Mf32_23[(shift_float32 a_0 0)]+Mf32_23[(shift_float32 a_0 4)]+\n Mf32_23[(shift_float32 a_0 8)])",
"pattern": "<0+[][][]$Mf32shift_float32$Mf32" },
"children":
{ "Then":
[ { "prover": "Alt-Ergo:2.3.3",
[ { "prover": "CVC4:1.9-prerelease:strings+counterexamples",
"verdict": "valid",
"time": 8.5531,
"steps": 758 } ],
"time": 1.97 } ],
"Else":
[ { "prover": "Alt-Ergo:2.3.3",
[ { "prover": "Alt-Ergo:2.4.0",
"verdict": "valid",
"time": 1.9398,
"steps": 982 } ] } } ] } } ] } } ] } } ] } } ] } } ] } } ]
"time": 12.0861,
"steps": 160794 } ] } } ] } } ] } } ] } } ] } } ] } } ] } } ]
......@@ -27,14 +27,14 @@
"params": {},
"select":
{ "select": "inside-step",
"at": 3,
"at": 7,
"kind": "have",
"occur": 0,
"target": "(L_trace_2_ Mf32_1 rm_0)",
"target": "(L_trace_2_ Mf32_23 rm_0)",
"pattern": "L_trace_2_$Mf32$rm" },
"children":
{ "Unfold 'L_trace_2_'":
[ { "prover": "Alt-Ergo:2.3.3",
[ { "prover": "Alt-Ergo:2.4.0",
"verdict": "valid",
"time": 4.2827,
"steps": 1246 } ] } } ] } } ] } } ] } } ]
"time": 11.6594,
"steps": 186185 } ] } } ] } } ] } } ] } } ]
......@@ -17,10 +17,10 @@
"params": {},
"select":
{ "select": "inside-step",
"at": 3,
"at": 7,
"kind": "have",
"occur": 0,
"target": "(L_trace_2_ Mf32_1 rm_0)",
"target": "(L_trace_2_ Mf32_23 rm_0)",
"pattern": "L_trace_2_$Mf32$rm" },
"children":
{ "Unfold 'L_trace_2_'":
......@@ -29,10 +29,10 @@
"params": {},
"select":
{ "select": "inside-step",
"at": 3,
"at": 7,
"kind": "have",
"occur": 0,
"target": "(L_trace_1_ (L_l_RMat_of_FloatRMat Mf32_1 rm_0))",
"target": "(L_trace_1_ (L_l_RMat_of_FloatRMat Mf32_23 rm_0))",
"pattern": "L_trace_1_L_l_RMat_of_FloatRMat$Mf32" },
"children":
{ "Unfold 'L_trace_1_'":
......@@ -56,10 +56,10 @@
"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",
[ { "prover": "Alt-Ergo:2.4.0",
"verdict": "valid",
"time": 2.7437,
"steps": 999 },
"time": 14.7875,
"steps": 280210 },
{ "header": "Definition",
"tactic": "Wp.unfold",
"params": {},
......@@ -88,22 +88,22 @@
"pattern": "&====[]*[]/[]/[]/$Mf32shiftfield_F4_FloatQuat_qz" },
"children":
{ "Goal 1/4":
[ { "prover": "Alt-Ergo:2.3.3",
[ { "prover": "Alt-Ergo:2.4.0",
"verdict": "valid",
"time": 4.0255,
"steps": 752 } ],
"Goal 2/4":
[ { "prover": "Alt-Ergo:2.3.3",
[ { "prover": "Alt-Ergo:2.4.0",
"verdict": "valid",
"time": 4.6182,
"steps": 779 } ],
"Goal 3/4":
[ { "prover": "Alt-Ergo:2.3.3",
[ { "prover": "Alt-Ergo:2.4.0",
"verdict": "valid",
"time": 4.7327,
"steps": 778 } ],
"Goal 4/4":
[ { "prover": "Alt-Ergo:2.3.3",
[ { "prover": "Alt-Ergo:2.4.0",
"verdict": "valid",
"time": 3.5847,
"steps": 778 } ] } } ] } } ] } } ] } } ] } } ] } } ] } } ] } } ] } } ]
[ { "header": "Split", "tactic": "Wp.split", "params": {},
"select": { "select": "clause-step", "at": 8, "kind": "branch",
"select": { "select": "clause-step", "at": 13, "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.728, "steps": 717 } ],
"Else": [ { "prover": "Alt-Ergo:2.3.3", "verdict": "valid",
"time": 5.6067, "steps": 1323 } ] } } ]
"children": { "Then": [ { "prover": "Alt-Ergo:2.4.0", "verdict": "valid",
"time": 0.9391, "steps": 12743 } ],
"Else": [ { "prover": "Alt-Ergo:2.4.0", "verdict": "valid",
"time": 3.0924, "steps": 49088 } ] } } ]
[ { "header": "Filter", "tactic": "Wp.filter", "params": { "anti": false },
"select": { "select": "inside-step", "at": 2, "kind": "have", "occur": 0,
"select": { "select": "inside-step", "at": 5, "kind": "have", "occur": 0,
"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": 7.5488,
"steps": 1615 } ] } } ]
"children": { "Filter": [ { "prover": "Alt-Ergo:2.4.0",
"verdict": "valid", "time": 6.5365,
"steps": 81768 } ] } } ]
......@@ -37,10 +37,10 @@
"params": {},
"select":
{ "select": "inside-step",
"at": 3,
"at": 7,
"kind": "have",
"occur": 0,
"target": "(L_trace_2_ Mf32_1 rm_0)",
"target": "(L_trace_2_ Mf32_23 rm_0)",
"pattern": "L_trace_2_$Mf32$rm" },
"children":
{ "Unfold 'L_trace_2_'":
......@@ -49,10 +49,10 @@
"params": {},
"select":
{ "select": "inside-step",
"at": 3,
"at": 7,
"kind": "have",
"occur": 0,
"target": "(L_trace_1_ (L_l_RMat_of_FloatRMat Mf32_1 rm_0))",
"target": "(L_trace_1_ (L_l_RMat_of_FloatRMat Mf32_23 rm_0))",
"pattern": "L_trace_1_L_l_RMat_of_FloatRMat$Mf32" },
"children":
{ "Unfold 'L_trace_1_'":
......@@ -61,17 +61,17 @@
"params": {},
"select":
{ "select": "inside-step",
"at": 3,
"at": 4,
"kind": "have",
"occur": 0,
"target": "(L_l_RMat_of_FloatRMat Mf32_1 rm_0)",
"target": "(L_l_RMat_of_FloatRMat Mf32_23 rm_0)",
"pattern": "L_l_RMat_of_FloatRMat$Mf32$rm" },
"children":
{ "Unfold 'L_l_RMat_of_FloatRMat'":
[ { "prover": "Alt-Ergo:2.3.3",
[ { "prover": "Alt-Ergo:2.4.0",
"verdict": "valid",
"time": 4.0889,
"steps": 805 },
"time": 6.8,
"steps": 77630 },
{ "header": "Definition",
"tactic": "Wp.unfold",
"params": {},
......@@ -81,7 +81,7 @@
"pattern": "EqS13_RealQuat_s{RealQuat_s}{RealQuat_s}" },
"children":
{ "Unfold 'EqS13_RealQuat_s'":
[ { "prover": "Alt-Ergo:2.3.3",
[ { "prover": "Alt-Ergo:2.4.0",
"verdict": "valid",
"time": 7.4511,
"steps": 4632 } ] } } ] } } ] } } ] } } ] } } ] } } ] } } ] } } ]
......@@ -29,7 +29,7 @@
"pattern": "L_l_RMat_of_FloatRMat[=]$m_a2b[=]" },
"children":
{ "Unfold 'L_l_RMat_of_FloatRMat'":
[ { "prover": "Alt-Ergo:2.3.3",
[ { "prover": "Alt-Ergo:2.4.0",
"verdict": "valid",
"time": 10.519,
"steps": 11772 } ] } } ] } } ] } } ] } } ]
"time": 10.1893,
"steps": 160389 } ] } } ] } } ] } } ] } } ]
......@@ -57,32 +57,32 @@
"pattern": "&======+1+1+1+0+0+0*************" },
"children":
{ "Goal 1/6":
[ { "prover": "Alt-Ergo:2.3.3",
[ { "prover": "Alt-Ergo:2.4.0",
"verdict": "valid",
"time": 2.2922,
"steps": 102 } ],
"time": 1.4855,
"steps": 2577 } ],
"Goal 2/6":
[ { "prover": "Z3:4.8.6",
"verdict": "valid",
"time": 0.83,
"steps": 2451125 } ],
"time": 0.53,
"steps": 2455394 } ],
"Goal 3/6":
[ { "prover": "Z3:4.8.6",
"verdict": "valid",
"time": 0.81,
"steps": 2451102 } ],
"time": 0.5,
"steps": 2455367 } ],
"Goal 4/6":
[ { "prover": "Alt-Ergo:2.3.3",
[ { "prover": "Alt-Ergo:2.4.0",
"verdict": "valid",
"time": 4.2691,
"steps": 102 } ],
"time": 1.9211,
"steps": 3020 } ],
"Goal 5/6":
[ { "prover": "Alt-Ergo:2.3.3",
[ { "prover": "Alt-Ergo:2.4.0",
"verdict": "valid",
"time": 3.9021,
"steps": 102 } ],
"time": 1.7791,
"steps": 2812 } ],
"Goal 6/6":
[ { "prover": "Alt-Ergo:2.3.3",
[ { "prover": "Alt-Ergo:2.4.0",
"verdict": "valid",
"time": 3.3381,
"steps": 102 } ] } } ] } } ] } } ] } } ] } } ] } } ] } } ]
"time": 1.465,
"steps": 2812 } ] } } ] } } ] } } ] } } ] } } ] } } ] } } ]
......@@ -9,7 +9,7 @@
"target": "let r_0 = Mf32_9[(shiftfield_F7_FloatEulers_phi e_1)] in\nlet r_1 = (\\sin r_0) in\nlet r_2 = Mf32_9[(shiftfield_F7_FloatEulers_psi e_1)] in\nlet r_3 = (\\sin r_2) in\nlet r_4 = Mf32_9[(shiftfield_F7_FloatEulers_theta e_1)] in\nlet r_5 = (\\sin r_4) in\nlet r_6 = (\\cos r_2) in\nlet r_7 = (\\cos r_4) in\nlet r_8 = (\\cos r_0) in\n(P_special_orthogonal\n {\n F13_RealRMat_s_a00 = (r_6*r_7)-(r_1*r_3*r_5) ;\n F13_RealRMat_s_a01 = (r_3*r_7)+(r_1*r_5*r_6) ;\n F13_RealRMat_s_a02 = -1*r_5*r_8 ;\n F13_RealRMat_s_a10 = -1*r_3*r_8 ;\n F13_RealRMat_s_a11 = r_8*r_6 ;\n F13_RealRMat_s_a12 = r_1 ;\n F13_RealRMat_s_a20 = (r_5*r_6)+(r_1*r_3*r_7) ;\n F13_RealRMat_s_a21 = (r_3*r_5)-(r_1*r_6*r_7) ;\n F13_RealRMat_s_a22 = r_8*r_7\n })",
"pattern": "P_special_orthogonal{RealRMat_s}" },
"children": { "Unfold 'P_special_orthogonal'":
[ { "prover": "Alt-Ergo:2.3.3",
[ { "prover": "Alt-Ergo:2.4.0",
"verdict": "valid",
"time": 2.9475,
"steps": 102 } ] } } ] } } ]
"time": 1.8116,
"steps": 2939 } ] } } ] } } ]
......@@ -57,31 +57,31 @@
"pattern": "&======+1+1+0+1+0+0*************" },
"children":
{ "Goal 1/6":
[ { "prover": "Alt-Ergo:2.3.3",
[ { "prover": "Alt-Ergo:2.4.0",
"verdict": "valid",
"time": 2.5181,
"steps": 102 } ],
"time": 1.4972,
"steps": 2575 } ],
"Goal 2/6":
[ { "prover": "Z3:4.8.6",
"verdict": "valid",
"time": 0.44,
"steps": 2451116 } ],
"time": 0.5,
"steps": 2455383 } ],
"Goal 3/6":
[ { "prover": "Alt-Ergo:2.3.3",
[ { "prover": "Alt-Ergo:2.4.0",
"verdict": "valid",
"time": 3.9076,
"steps": 102 } ],
"time": 1.9764,
"steps": 2964 } ],
"Goal 4/6":
[ { "prover": "CVC4:1.9-prerelease:strings+counterexamples",
"verdict": "valid",
"time": 9.19 } ],
"time": 7.91 } ],
"Goal 5/6":
[ { "prover": "Alt-Ergo:2.3.3",
[ { "prover": "Alt-Ergo:2.4.0",
"verdict": "valid",
"time": 3.8367,
"steps": 102 } ],
"time": 1.3098,
"steps": 2802 } ],
"Goal 6/6":
[ { "prover": "Alt-Ergo:2.3.3",
[ { "prover": "Alt-Ergo:2.4.0",
"verdict": "valid",
"time": 3.0174,
"steps": 102 } ] } } ] } } ] } } ] } } ] } } ] } } ] } } ]
"time": 1.3971,
"steps": 2814 } ] } } ] } } ] } } ] } } ] } } ] } } ] } } ]
......@@ -9,7 +9,7 @@
"target": "let r_0 = Mf32_9[(shiftfield_F7_FloatEulers_psi e_1)] in\nlet r_1 = (\\cos r_0) in\nlet r_2 = Mf32_9[(shiftfield_F7_FloatEulers_theta e_1)] in\nlet r_3 = (\\cos r_2) in\nlet r_4 = (\\sin r_0) in\nlet r_5 = (\\sin r_2) in\nlet r_6 = Mf32_9[(shiftfield_F7_FloatEulers_phi e_1)] in\nlet r_7 = (\\cos r_6) in\nlet r_8 = (\\sin r_6) in\n(P_special_orthogonal\n {\n F13_RealRMat_s_a00 = r_1*r_3 ;\n F13_RealRMat_s_a01 = r_4*r_3 ;\n F13_RealRMat_s_a02 = -r_5 ;\n F13_RealRMat_s_a10 = (r_8*r_5*r_1)-(r_4*r_7) ;\n F13_RealRMat_s_a11 = (r_7*r_1)+(r_8*r_4*r_5) ;\n F13_RealRMat_s_a12 = r_8*r_3 ;\n F13_RealRMat_s_a20 = (r_8*r_4)+(r_5*r_7*r_1) ;\n F13_RealRMat_s_a21 = (r_4*r_5*r_7)-(r_8*r_1) ;\n F13_RealRMat_s_a22 = r_7*r_3\n })",
"pattern": "P_special_orthogonal{RealRMat_s}" },
"children": { "Unfold 'P_special_orthogonal'":
[ { "prover": "Alt-Ergo:2.3.3",
[ { "prover": "Alt-Ergo:2.4.0",
"verdict": "valid",
"time": 3.1177,
"steps": 102 } ] } } ] } } ]
"time": 1.5834,
"steps": 2925 } ] } } ] } } ]
[ { "header": "Split", "tactic": "Wp.split", "params": {},
"select": { "select": "inside-step", "at": 2, "kind": "have", "occur": 0,
"select": { "select": "inside-step", "at": 5, "kind": "have", "occur": 0,
"target": "(separated rm_0 9 q_0 4)",
"pattern": "separated$rm9$q4" },
"children": { "True": [ { "header": "Separated",
"tactic": "Wp.separated", "params": {},
"select": { "select": "clause-step", "at": 2,
"select": { "select": "clause-step", "at": 5,
"kind": "have",
"target": "(separated rm_0 9 q_0 4)",
"pattern": "separated$rm9$q4" },
"children": { "WrongBase": [ { "prover": "CVC4:1.9-prerelease:strings+counterexamples",
"verdict": "valid",
"time": 7.76 } ],
"time": 6.64 } ],
"OnLeft": [ { "prover": "CVC4:1.9-prerelease:strings+counterexamples",
"verdict": "valid",
"time": 12.1 } ],
"time": 10.38 } ],
"OnRight": [ { "prover": "CVC4:1.9-prerelease:strings+counterexamples",
"verdict": "valid",
"time": 11.83 } ],
"time": 10.16 } ],
"OverLap": [ { "prover": "qed",
"verdict": "valid" } ] } } ],
"False": [ { "prover": "qed", "verdict": "valid" } ] } } ]
[ { "header": "Split", "tactic": "Wp.split", "params": {},
"select": { "select": "inside-step", "at": 2, "kind": "have", "occur": 0,
"select": { "select": "inside-step", "at": 5, "kind": "have", "occur": 0,
"target": "(separated rm_0 9 q_0 4)",
"pattern": "separated$rm9$q4" },
"children": { "True": [ { "header": "Separated",
"tactic": "Wp.separated", "params": {},
"select": { "select": "clause-step", "at": 2,
"select": { "select": "clause-step", "at": 5,
"kind": "have",
"target": "(separated rm_0 9 q_0 4)",
"pattern": "separated$rm9$q4" },
"children": { "WrongBase": [ { "prover": "CVC4:1.9-prerelease:strings+counterexamples",
"verdict": "valid",
"time": 4.25 } ],
"time": 3.49 } ],
"OnLeft": [ { "prover": "CVC4:1.9-prerelease:strings+counterexamples",
"verdict": "valid",
"time": 6.4 } ],
"time": 5.31 } ],
"OnRight": [ { "prover": "CVC4:1.9-prerelease:strings+counterexamples",
"verdict": "valid",
"time": 5.93 } ],
"time": 5.16 } ],
"OverLap": [ { "prover": "qed",
"verdict": "valid" } ] } } ],
"False": [ { "prover": "qed", "verdict": "valid" } ] } } ]
[ { "header": "Separated", "tactic": "Wp.separated", "params": {},
"select": { "select": "inside-step", "at": 2, "kind": "have", "occur": 0,
"select": { "select": "inside-step", "at": 5, "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": 2.36 } ],
"verdict": "valid", "time": 2.02 } ],
"OnLeft": [ { "prover": "CVC4:1.9-prerelease:strings+counterexamples",
"verdict": "valid", "time": 4.7 } ],
"verdict": "valid", "time": 3.87 } ],
"OnRight": [ { "prover": "CVC4:1.9-prerelease:strings+counterexamples",
"verdict": "valid", "time": 4.6 } ],
"verdict": "valid", "time": 4.01 } ],
"OverLap": [ { "prover": "qed", "verdict": "valid" } ] } } ]
[ { "header": "Split", "tactic": "Wp.split", "params": {},
"select": { "select": "inside-step", "at": 2, "kind": "have", "occur": 0,
"select": { "select": "inside-step", "at": 5, "kind": "have", "occur": 0,
"target": "(separated rm_0 9 q_0 4)",
"pattern": "separated$rm9$q4" },
"children": { "True": [ { "header": "Separated",
"tactic": "Wp.separated", "params": {},
"select": { "select": "clause-step", "at": 2,
"select": { "select": "clause-step", "at": 5,
"kind": "have",
"target": "(separated rm_0 9 q_0 4)",
"pattern": "separated$rm9$q4" },
"children": { "WrongBase": [ { "prover": "Alt-Ergo:2.3.3",
"children": { "WrongBase": [ { "prover": "Alt-Ergo:2.4.0",
"verdict": "valid",
"time": 13.8324,
"steps": 136 } ],
"time": 11.8184,
"steps": 69285 } ],
"OnLeft": [ { "prover": "CVC4:1.9-prerelease:strings+counterexamples",
"verdict": "valid",
"time": 16.72 } ],
"time": 14.86 } ],
"OnRight": [ { "header": "Range",
"tactic": "Wp.range",
"params":
......@@ -22,7 +22,7 @@
"sup": 0 },
"select":
{ "select": "inside-step",
"at": 2,
"at": 5,
"kind": "have",
"occur": 0,
"target": "(offset rm_0)",
......@@ -31,17 +31,17 @@
{ "Lower 0":
[ { "prover": "Z3:4.8.6",
"verdict": "valid",
"time": 0.06,
"steps": 248124 } ],
"time": 0.05,
"steps": 252625 } ],
"Value 0":
[ { "prover": "Z3:4.8.6",
"verdict": "valid",
"time": 0.05,
"steps": 248515 } ],
"steps": 253023 } ],
"Upper 0":
[ { "prover": "CVC4:1.9-prerelease:strings+counterexamples",
"verdict": "valid",
"time": 15.5 } ] } } ],
"time": 13.57 } ] } } ],
"OverLap": [ { "prover": "qed",
"verdict": "valid" } ] } } ],
"False": [ { "prover": "qed", "verdict": "valid" } ] } } ]
......@@ -31,5 +31,5 @@
{ "Unfold 'L_l_RMat_of_FloatRMat'":
[ { "prover": "Z3:4.8.6",
"verdict": "valid",
"time": 0.07,
"steps": 144735 } ] } } ] } } ] } } ] } } ]
"time": 0.04,
"steps": 149450 } ] } } ] } } ] } } ] } } ]
......@@ -54,14 +54,14 @@
"params": {},
"select":
{ "select": "inside-step",
"at": 2,
"at": 4,
"kind": "have",
"occur": 0,
"target": "(P_unary_quaternion_1_ Mf32_1 q_0)",
"pattern": "P_unary_quaternion_1_$Mf32$q" },
"children":
{ "Unfold 'P_unary_quaternion_1_'":
[ { "prover": "Alt-Ergo:2.3.3",
[ { "prover": "Alt-Ergo:2.4.0",
"verdict": "valid",
"time": 8.597,
"steps": 144 } ] } } ] } } ] } } ] } } ] } } ] } } ] } } ]
"time": 5.5712,