Skip to content

Commit

Permalink
stabilize proof
Browse files Browse the repository at this point in the history
  • Loading branch information
@xldenis
xldenis committed Jul 26, 2024
1 parent a3f91b1 commit 3dcbf97
Show file tree
Hide file tree
Showing 2 changed files with 36 additions and 126 deletions.
162 changes: 36 additions & 126 deletions creusot/tests/should_succeed/list_reversal_lasso/why3session.xml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -5,86 +5,26 @@
<prover id="0" name="Z3" version="4.12.4" timelimit="1" steplimit="0" memlimit="1000"/>
<prover id="1" name="Alt-Ergo" version="2.5.3" timelimit="1" steplimit="0" memlimit="1000"/>
<prover id="2" name="CVC5" version="1.0.5" timelimit="1" steplimit="0" memlimit="1000"/>
<prover id="3" name="CVC4" version="1.8" timelimit="1" steplimit="0" memlimit="1000"/>
<file format="coma" proved="true">
<path name=".."/><path name="list_reversal_lasso.coma"/>
<theory name="Core_Ptr_NonNull_NonNull_Type" proved="true">
<goal name="vc_t_nonnull" proved="true">
<proof prover="2"><result status="valid" time="0.008053" steps="27"/></proof>
</goal>
</theory>
<theory name="Core_Marker_PhantomData_Type" proved="true">
<goal name="vc_t_phantomdata" proved="true">
<proof prover="2"><result status="valid" time="0.008700" steps="27"/></proof>
</goal>
</theory>
<theory name="Core_Ptr_Unique_Unique_Type" proved="true">
<goal name="vc_t_unique" proved="true">
<proof prover="2"><result status="valid" time="0.007423" steps="27"/></proof>
</goal>
</theory>
<theory name="Alloc_RawVec_Cap_Type" proved="true">
<goal name="vc_t_cap" proved="true">
<proof prover="2"><result status="valid" time="0.000001" steps="189"/></proof>
</goal>
</theory>
<theory name="Alloc_RawVec_RawVec_Type" proved="true">
<goal name="vc_t_rawvec" proved="true">
<proof prover="2"><result status="valid" time="0.002921" steps="189"/></proof>
</goal>
</theory>
<theory name="Alloc_Vec_Vec_Type" proved="true">
<goal name="vc_t_vec" proved="true">
<proof prover="2"><result status="valid" time="0.004360" steps="189"/></proof>
</goal>
</theory>
<theory name="Alloc_Alloc_Global_Type" proved="true">
<goal name="vc_t_global" proved="true">
<proof prover="2"><result status="valid" time="0.000001" steps="27"/></proof>
</goal>
</theory>
<theory name="ListReversalLasso_Memory_Type" proved="true">
<goal name="vc_t_memory" proved="true">
<proof prover="2"><result status="valid" time="0.000001" steps="189"/></proof>
</goal>
</theory>
<theory name="ListReversalLasso_Impl1_Index" proved="true">
<goal name="vc_index&#39;0" proved="true">
<proof prover="2"><result status="valid" time="0.010572" steps="4967"/></proof>
</goal>
<goal name="vc_index" proved="true">
<proof prover="2"><result status="valid" time="0.028439" steps="9477"/></proof>
</goal>
</theory>
<theory name="ListReversalLasso_Impl2_IndexMut" proved="true">
<goal name="vc_index_mut&#39;0" proved="true">
<proof prover="2"><result status="valid" time="0.007065" steps="5210"/></proof>
</goal>
<goal name="vc_index_mut" proved="true">
<proof prover="2"><result status="valid" time="0.056447" steps="13839"/></proof>
</goal>
</theory>
<theory name="ListReversalLasso_Impl4_ListReversalSafe" proved="true">
<goal name="vc_index_mut&#39;0" proved="true">
<proof prover="2"><result status="valid" time="0.009311" steps="4924"/></proof>
</goal>
<goal name="vc_index&#39;0" proved="true">
<proof prover="2"><result status="valid" time="0.007023" steps="4924"/></proof>
</goal>
<goal name="vc_list_reversal_safe" proved="true">
<proof prover="2"><result status="valid" time="0.124100" steps="25894"/></proof>
</goal>
</theory>
<theory name="ListReversalLasso_Impl4_ListReversalList" proved="true">
<goal name="vc_replace&#39;0" proved="true">
<proof prover="2"><result status="valid" time="0.010478" steps="5187"/></proof>
</goal>
<goal name="vc_index_mut&#39;0" proved="true">
<proof prover="2"><result status="valid" time="0.017108" steps="5187"/></proof>
</goal>
<goal name="vc_list_reversal_list" proved="true">
<proof prover="0"><result status="timeout" time="1.000000" steps="2284627"/></proof>
<proof prover="1"><result status="timeout" time="1.000000" steps="9923"/></proof>
<proof prover="2"><result status="timeout" time="1.000000" steps="178269"/></proof>
<transf name="split_vc" proved="true" >
<goal name="vc_list_reversal_list.0" expl="loop invariant" proved="true">
<proof prover="2"><result status="valid" time="0.014781" steps="7045"/></proof>
Expand Down Expand Up @@ -132,16 +72,7 @@
</goal>
</theory>
<theory name="ListReversalLasso_Impl4_ListReversalLoop" proved="true">
<goal name="vc_replace&#39;0" proved="true">
<proof prover="2"><result status="valid" time="0.009838" steps="5187"/></proof>
</goal>
<goal name="vc_index_mut&#39;0" proved="true">
<proof prover="2"><result status="valid" time="0.007594" steps="5187"/></proof>
</goal>
<goal name="vc_list_reversal_loop" proved="true">
<proof prover="0"><result status="timeout" time="1.000000" steps="2306363"/></proof>
<proof prover="1"><result status="timeout" time="1.000000" steps="11663"/></proof>
<proof prover="2"><result status="timeout" time="1.000000" steps="173651"/></proof>
<transf name="split_vc" proved="true" >
<goal name="vc_list_reversal_loop.0" expl="loop invariant" proved="true">
<proof prover="2"><result status="valid" time="0.024544" steps="9418"/></proof>
Expand All @@ -162,9 +93,6 @@
<proof prover="1"><result status="valid" time="0.068348" steps="665"/></proof>
</goal>
<goal name="vc_list_reversal_loop.6" expl="postcondition" proved="true">
<proof prover="0"><result status="timeout" time="1.000000" steps="1729074"/></proof>
<proof prover="1"><result status="timeout" time="1.000000" steps="10836"/></proof>
<proof prover="2"><result status="timeout" time="1.000000" steps="133050"/></proof>
<transf name="split_vc" proved="true" >
<goal name="vc_list_reversal_loop.6.0" expl="postcondition" proved="true">
<proof prover="1" timelimit="5" memlimit="2000"><result status="valid" time="4.168868" steps="38855"/></proof>
Expand Down Expand Up @@ -208,16 +136,7 @@
</goal>
</theory>
<theory name="ListReversalLasso_Impl4_ListReversalLasso" proved="true">
<goal name="vc_replace&#39;0" proved="true">
<proof prover="2"><result status="valid" time="0.010438" steps="5187"/></proof>
</goal>
<goal name="vc_index_mut&#39;0" proved="true">
<proof prover="2"><result status="valid" time="0.013574" steps="5187"/></proof>
</goal>
<goal name="vc_list_reversal_lasso" proved="true">
<proof prover="0"><result status="timeout" time="1.000000" steps="1688325"/></proof>
<proof prover="1"><result status="timeout" time="1.000000" steps="8476"/></proof>
<proof prover="2"><result status="timeout" time="1.000000" steps="216314"/></proof>
<transf name="split_vc" proved="true" >
<goal name="vc_list_reversal_lasso.0" expl="loop invariant" proved="true">
<proof prover="2"><result status="valid" time="0.025380" steps="7295"/></proof>
Expand All @@ -235,14 +154,8 @@
<proof prover="2"><result status="valid" time="0.056178" steps="15791"/></proof>
</goal>
<goal name="vc_list_reversal_lasso.5" expl="postcondition" proved="true">
<proof prover="0"><result status="timeout" time="1.000000" steps="1639253"/></proof>
<proof prover="1"><result status="timeout" time="1.000000" steps="7532"/></proof>
<proof prover="2"><result status="timeout" time="1.000000" steps="211553"/></proof>
<transf name="split_vc" proved="true" >
<goal name="vc_list_reversal_lasso.5.0" expl="postcondition" proved="true">
<proof prover="0" timelimit="5" memlimit="2000"><result status="timeout" time="5.000000" steps="8943428"/></proof>
<proof prover="1" timelimit="5" memlimit="2000"><result status="timeout" time="5.000000" steps="50619"/></proof>
<proof prover="2" timelimit="5" memlimit="2000"><result status="timeout" time="5.000000" steps="704220"/></proof>
<transf name="inline_goal" proved="true" >
<goal name="vc_list_reversal_lasso.5.0.0" expl="postcondition" proved="true">
<transf name="split_all_full" proved="true" >
Expand All @@ -256,9 +169,6 @@
<proof prover="2"><result status="valid" time="0.796825" steps="185143"/></proof>
</goal>
<goal name="vc_list_reversal_lasso.5.0.0.3" expl="postcondition" proved="true">
<proof prover="0"><result status="timeout" time="1.000000" steps="2602128"/></proof>
<proof prover="1"><result status="timeout" time="1.000000" steps="8692"/></proof>
<proof prover="2"><result status="timeout" time="1.000000" steps="169372"/></proof>
<transf name="split_vc" proved="true" >
<goal name="vc_list_reversal_lasso.5.0.0.3.0" expl="postcondition" proved="true">
<proof prover="1" timelimit="5" memlimit="2000"><result status="valid" time="3.299007" steps="31068"/></proof>
Expand Down Expand Up @@ -290,14 +200,8 @@
<proof prover="2"><result status="valid" time="0.018920" steps="10575"/></proof>
</goal>
<goal name="vc_list_reversal_lasso.12" expl="loop invariant" proved="true">
<proof prover="0"><result status="timeout" time="1.000000" steps="2685935"/></proof>
<proof prover="1"><result status="timeout" time="1.000000" steps="10097"/></proof>
<proof prover="2"><result status="timeout" time="1.000000" steps="202665"/></proof>
<transf name="split_vc" proved="true" >
<goal name="vc_list_reversal_lasso.12.0" expl="loop invariant" proved="true">
<proof prover="0" timelimit="5" memlimit="2000"><result status="timeout" time="5.000000" steps="9836895"/></proof>
<proof prover="1" timelimit="5" memlimit="2000"><result status="timeout" time="5.000000" steps="43348"/></proof>
<proof prover="2" timelimit="5" memlimit="2000"><result status="timeout" time="5.000000" steps="680508"/></proof>
<transf name="inline_goal" proved="true" >
<goal name="vc_list_reversal_lasso.12.0.0" expl="loop invariant" proved="true">
<transf name="split_all_full" proved="true" >
Expand All @@ -318,12 +222,13 @@
</transf>
</goal>
<goal name="vc_list_reversal_lasso.12.1" expl="loop invariant" proved="true">
<proof prover="1" timelimit="5" memlimit="2000"><result status="valid" time="3.640039" steps="29914"/></proof>
<transf name="remove" proved="true" arg1="zero,one,(-),(&gt;),(&lt;=),(&gt;=),abs,snoc,(++),borrow_logic,get_id,usize&#39;maxInt,usize&#39;minInt,usize&#39;eq,min,max,to_int,in_bounds,memory_0,invariant&#39;3,max&#39;0,invariant&#39;2,invariant&#39;1,invariant&#39;0,index_logic&#39;1,resolve&#39;1,Assoc1,Unit_def_l,Unit_def_r,Inv_def_l,Inv_def_r,Comm1,Assoc,Mul_distr_l,Mul_distr_r,Comm,Unitary,NonTrivialRing,Refl,Trans,Antisymm,Total,ZeroLessOne,CompatOrderAdd,CompatOrderMult,Abs_le,Abs_pos,Div_mod,Div_bound,Mod_bound,Mod_sign_neg,Div_1,Mod_1,Div_inf,(==)&#39;spec,create&#39;spec&#39;0,empty&#39;def,snoc&#39;spec,snoc&#39;spec&#39;0,snoc&#39;spec&#39;1,([..])&#39;spec,([..])&#39;spec&#39;0,([..])&#39;def,([_..])&#39;def,([.._])&#39;def,(++)&#39;spec,(++)&#39;spec&#39;0,(++)&#39;spec&#39;1,usize&#39;inj,to_int_in_bounds,extensionality,inner_spec,inv&#39;3,shallow_model&#39;0_spec,inv&#39;2,inv&#39;0,Assert18,Assert7,Assert4,H10,H4">
<goal name="vc_list_reversal_lasso.12.1.0" expl="loop invariant" proved="true">
<proof prover="1" timelimit="0.31527" memlimit="2000"><result status="valid" time="0.316375" steps="5473"/></proof>
</goal>
</transf>
</goal>
<goal name="vc_list_reversal_lasso.12.2" expl="loop invariant" proved="true">
<proof prover="0" timelimit="5" memlimit="2000"><result status="timeout" time="5.000000" steps="9817082"/></proof>
<proof prover="1" timelimit="5" memlimit="2000"><result status="timeout" time="5.000000" steps="52172"/></proof>
<proof prover="2" timelimit="5" memlimit="2000"><result status="timeout" time="5.000000" steps="641962"/></proof>
<transf name="inline_goal" proved="true" >
<goal name="vc_list_reversal_lasso.12.2.0" expl="loop invariant" proved="true">
<transf name="split_all_full" proved="true" >
Expand All @@ -334,9 +239,6 @@
<proof prover="2"><result status="valid" time="0.230872" steps="60151"/></proof>
</goal>
<goal name="vc_list_reversal_lasso.12.2.0.2" proved="true">
<proof prover="0"><result status="timeout" time="1.000000" steps="2417205"/></proof>
<proof prover="1"><result status="timeout" time="1.000000" steps="10762"/></proof>
<proof prover="2"><result status="timeout" time="1.000000" steps="214458"/></proof>
<transf name="split_vc" proved="true" >
<goal name="vc_list_reversal_lasso.12.2.0.2.0" proved="true">
<proof prover="1" timelimit="5" memlimit="2000"><result status="valid" time="1.046999" steps="9229"/></proof>
Expand All @@ -353,34 +255,53 @@
</transf>
</goal>
<goal name="vc_list_reversal_lasso.13" expl="loop invariant" proved="true">
<proof prover="0"><result status="timeout" time="1.000000" steps="2690227"/></proof>
<proof prover="1"><result status="timeout" time="1.000000" steps="8793"/></proof>
<proof prover="2"><result status="timeout" time="1.000000" steps="211519"/></proof>
<transf name="split_vc" proved="true" >
<goal name="vc_list_reversal_lasso.13.0" expl="loop invariant" proved="true">
<proof prover="1" timelimit="5" memlimit="2000"><result status="valid" time="1.519904" steps="12367"/></proof>
<transf name="inline_goal" proved="true" >
<goal name="vc_list_reversal_lasso.13.0.0" expl="loop invariant" proved="true">
<transf name="split_all_full" proved="true" >
<goal name="vc_list_reversal_lasso.13.0.0.0" proved="true">
<proof prover="1"><result status="valid" time="0.046121" steps="683"/></proof>
</goal>
<goal name="vc_list_reversal_lasso.13.0.0.1" proved="true">
<proof prover="3"><result status="valid" time="0.420334" steps="83508"/></proof>
</goal>
<goal name="vc_list_reversal_lasso.13.0.0.2" proved="true">
<proof prover="1"><result status="valid" time="0.069163" steps="1173"/></proof>
</goal>
<goal name="vc_list_reversal_lasso.13.0.0.3" proved="true">
<proof prover="2"><result status="valid" time="0.710538" steps="154593"/></proof>
</goal>
</transf>
</goal>
</transf>
</goal>
<goal name="vc_list_reversal_lasso.13.1" expl="loop invariant" proved="true">
<proof prover="1" timelimit="5" memlimit="2000"><result status="valid" time="1.229106" steps="10855"/></proof>
<proof prover="1"><result status="valid" time="0.610102" steps="10855"/></proof>
</goal>
<goal name="vc_list_reversal_lasso.13.2" expl="loop invariant" proved="true">
<proof prover="1" timelimit="5" memlimit="2000"><result status="valid" time="1.617694" steps="15894"/></proof>
<transf name="remove" proved="true" arg1="zero,one,(-),(&gt;),(&lt;=),(&gt;=),abs,(++),borrow_logic,get_id,usize&#39;maxInt,usize&#39;minInt,usize&#39;eq,min,max,to_int,in_bounds,memory_0,invariant&#39;3,max&#39;0,invariant&#39;2,invariant&#39;1,invariant&#39;0,index_logic&#39;2,resolve&#39;1,Assoc1,Unit_def_l,Unit_def_r,Inv_def_l,Inv_def_r,Comm1,Assoc,Mul_distr_l,Mul_distr_r,Comm,Unitary,NonTrivialRing,Refl,Trans,Antisymm,Total,ZeroLessOne,CompatOrderAdd,CompatOrderMult,Abs_le,Abs_pos,Div_mod,Div_bound,Mod_bound,Div_sign_pos,Div_sign_neg,Mod_sign_pos,Mod_sign_neg,Rounds_toward_zero,Div_1,Mod_1,Div_inf,snoc&#39;spec,snoc&#39;spec&#39;0,([..])&#39;spec,([..])&#39;spec&#39;0,([..])&#39;def,([_..])&#39;def,([.._])&#39;def,(++)&#39;spec,(++)&#39;spec&#39;0,(++)&#39;spec&#39;1,usize&#39;inj,to_int_in_bounds,extensionality,inv&#39;3,shallow_model&#39;0_spec,inv&#39;2,inv&#39;1,inv&#39;0,Assert18,Assert14,Assert12,Assert9,Assert8,Assert7,Assert6,Assert5,Assert4,Assert3,Assert2,Assert1,Assert,Assert16,H6,H4,H15,H11,H3,H2">
<goal name="vc_list_reversal_lasso.13.2.0" expl="loop invariant" proved="true">
<proof prover="1" timelimit="0.092563"><result status="valid" time="0.091017" steps="1673"/></proof>
</goal>
</transf>
</goal>
</transf>
</goal>
<goal name="vc_list_reversal_lasso.14" expl="loop invariant" proved="true">
<proof prover="0"><result status="timeout" time="1.000000" steps="2640458"/></proof>
<proof prover="1"><result status="timeout" time="1.000000" steps="9517"/></proof>
<proof prover="2"><result status="timeout" time="1.000000" steps="248681"/></proof>
<transf name="split_vc" proved="true" >
<goal name="vc_list_reversal_lasso.14.0" expl="loop invariant" proved="true">
<proof prover="1"><result status="valid" time="0.528542" steps="4590"/></proof>
</goal>
<goal name="vc_list_reversal_lasso.14.1" expl="loop invariant" proved="true">
<proof prover="1" timelimit="5" memlimit="2000"><result status="valid" time="2.082820" steps="17515"/></proof>
<proof prover="3"><result status="valid" time="0.510933" steps="77148"/></proof>
</goal>
<goal name="vc_list_reversal_lasso.14.2" expl="loop invariant" proved="true">
<proof prover="1" timelimit="5" memlimit="2000"><result status="valid" time="1.895103" steps="17720"/></proof>
<transf name="remove" proved="true" arg1="zero,one,(-),(&gt;),(&lt;=),(&gt;=),abs,singleton,cons,snoc,(++),borrow_logic,get_id,usize&#39;maxInt,usize&#39;minInt,usize&#39;eq,in_bounds,memory_0,invariant&#39;3,invariant&#39;2,invariant&#39;1,invariant&#39;0,Assoc1,Unit_def_l,Unit_def_r,Inv_def_l,Inv_def_r,Comm1,Assoc,Mul_distr_l,Mul_distr_r,Comm,Unitary,NonTrivialRing,Refl,Trans,Antisymm,Total,ZeroLessOne,CompatOrderAdd,CompatOrderMult,Abs_le,Abs_pos,Div_mod,Div_bound,Mod_bound,Div_sign_pos,Div_sign_neg,Mod_sign_pos,Mod_sign_neg,Rounds_toward_zero,Div_1,Mod_1,Div_inf,Mod_inf,Div_mult,Mod_mult,(==)&#39;spec,(==)&#39;spec&#39;0,empty&#39;def,set&#39;spec,set&#39;spec&#39;0,set&#39;spec&#39;1,set&#39;def,([&lt;-])&#39;def,singleton&#39;spec,singleton&#39;spec&#39;0,cons&#39;spec,cons&#39;spec&#39;0,cons&#39;spec&#39;1,snoc&#39;spec,snoc&#39;spec&#39;0,snoc&#39;spec&#39;1,([..])&#39;spec,([..])&#39;spec&#39;0,([_..])&#39;def,([.._])&#39;def,(++)&#39;spec,(++)&#39;spec&#39;0,(++)&#39;spec&#39;1,usize&#39;inj,inv&#39;3,inv&#39;1,inv&#39;0,Assert21,Assert17,Assert10,Assert7,Assert3,H13,Assert20,Assert19,Assert18,H5,H3,H14,H12,H11,H10,H4,H2,H1,Assert2,Assert1,Assert">
<goal name="vc_list_reversal_lasso.14.2.0" expl="loop invariant" proved="true">
<proof prover="1" timelimit="0.187113"><result status="valid" time="0.189428" steps="2659"/></proof>
</goal>
</transf>
</goal>
</transf>
</goal>
Expand All @@ -390,14 +311,6 @@
</transf>
</goal>
</theory>
<theory name="Core_Option_Option_Type" proved="true">
<goal name="vc_none" proved="true">
<proof prover="2"><result status="valid" time="0.006672" steps="27"/></proof>
</goal>
<goal name="vc_some" proved="true">
<proof prover="2"><result status="valid" time="0.004238" steps="27"/></proof>
</goal>
</theory>
<theory name="ListReversalLasso_Impl4_FindPtrInSeq_Impl" proved="true">
<goal name="vc_find_ptr_in_seq" proved="true">
<proof prover="2"><result status="valid" time="0.029070" steps="8450"/></proof>
Expand All @@ -410,9 +323,6 @@
</theory>
<theory name="ListReversalLasso_Impl4_FindLassoAux_Impl" proved="true">
<goal name="vc_find_lasso_aux" proved="true">
<proof prover="0"><result status="timeout" time="1.000000" steps="3029666"/></proof>
<proof prover="1"><result status="timeout" time="1.000000" steps="8072"/></proof>
<proof prover="2"><result status="timeout" time="1.000000" steps="130948"/></proof>
<transf name="split_vc" proved="true" >
<goal name="vc_find_lasso_aux.0" proved="true">
<proof prover="2"><result status="valid" time="0.032432" steps="10396"/></proof>
Expand Down
Binary file modified creusot/tests/should_succeed/list_reversal_lasso/why3shapes.gz
View file
Binary file not shown.

0 comments on commit 3dcbf97

Please sign in to comment.