Skip to content

Commit 6b49bd1

Browse files
voidcvoidc
committed
Update proofs
1 parent 17b0aff commit 6b49bd1

32 files changed

+1216
-1159
lines changed

‎creusot/tests/should_succeed/hillel.mlcfg‎

Lines changed: 20 additions & 20 deletions
Original file line numberDiff line numberDiff line change
@@ -1110,7 +1110,7 @@ module CreusotContracts_Std1_Slice_Impl15_Produces
11101110
predicate produces (self : Core_Slice_Iter_Iter_Type.t_iter t) (visited : Seq.seq t) (tl : Core_Slice_Iter_Iter_Type.t_iter t)
11111111

11121112
=
1113-
[#"../../../../creusot-contracts/src/std/slice.rs" 379 12 379 66] ToRefSeq0.to_ref_seq (ShallowModel0.shallow_model self) = Seq.(++) visited (ToRefSeq0.to_ref_seq (ShallowModel0.shallow_model tl))
1113+
[#"../../../../creusot-contracts/src/std/slice.rs" 378 12 378 66] ToRefSeq0.to_ref_seq (ShallowModel0.shallow_model self) = Seq.(++) visited (ToRefSeq0.to_ref_seq (ShallowModel0.shallow_model tl))
11141114
val produces (self : Core_Slice_Iter_Iter_Type.t_iter t) (visited : Seq.seq t) (tl : Core_Slice_Iter_Iter_Type.t_iter t) : bool
11151115
ensures { result = produces self visited tl }
11161116

@@ -1183,7 +1183,7 @@ module Core_Slice_Impl0_Iter_Interface
11831183
clone CreusotContracts_Std1_Slice_Impl13_ShallowModel_Stub as ShallowModel0 with
11841184
type t = t
11851185
val iter (self : slice t) : Core_Slice_Iter_Iter_Type.t_iter t
1186-
ensures { [#"../../../../creusot-contracts/src/std/slice.rs" 232 0 325 1] ShallowModel0.shallow_model result = self }
1186+
ensures { [#"../../../../creusot-contracts/src/std/slice.rs" 232 0 324 1] ShallowModel0.shallow_model result = self }
11871187

11881188
end
11891189
module CreusotContracts_Std1_Iter_IntoIterator_IntoIterPre_Stub
@@ -1320,7 +1320,7 @@ module CreusotContracts_Std1_Slice_Impl15_Completed
13201320
clone CreusotContracts_Resolve_Impl1_Resolve_Stub as Resolve0 with
13211321
type t = Core_Slice_Iter_Iter_Type.t_iter t
13221322
predicate completed (self : borrowed (Core_Slice_Iter_Iter_Type.t_iter t)) =
1323-
[#"../../../../creusot-contracts/src/std/slice.rs" 372 20 372 61] Resolve0.resolve self /\ ShallowModel1.shallow_model (ShallowModel0.shallow_model self) = Seq.empty
1323+
[#"../../../../creusot-contracts/src/std/slice.rs" 371 20 371 61] Resolve0.resolve self /\ ShallowModel1.shallow_model (ShallowModel0.shallow_model self) = Seq.empty
13241324
val completed (self : borrowed (Core_Slice_Iter_Iter_Type.t_iter t)) : bool
13251325
ensures { result = completed self }
13261326

@@ -1451,10 +1451,10 @@ module CreusotContracts_Std1_Slice_Impl15_ProducesRefl_Interface
14511451
type t = t
14521452
function produces_refl (a : Core_Slice_Iter_Iter_Type.t_iter t) : ()
14531453
val produces_refl (a : Core_Slice_Iter_Iter_Type.t_iter t) : ()
1454-
ensures { [#"../../../../creusot-contracts/src/std/slice.rs" 385 14 385 39] Produces0.produces a (Seq.empty ) a }
1454+
ensures { [#"../../../../creusot-contracts/src/std/slice.rs" 384 14 384 39] Produces0.produces a (Seq.empty ) a }
14551455
ensures { result = produces_refl a }
14561456

1457-
axiom produces_refl_spec : forall a : Core_Slice_Iter_Iter_Type.t_iter t . [#"../../../../creusot-contracts/src/std/slice.rs" 385 14 385 39] Produces0.produces a (Seq.empty ) a
1457+
axiom produces_refl_spec : forall a : Core_Slice_Iter_Iter_Type.t_iter t . [#"../../../../creusot-contracts/src/std/slice.rs" 384 14 384 39] Produces0.produces a (Seq.empty ) a
14581458
end
14591459
module CreusotContracts_Std1_Slice_Impl15_ProducesRefl
14601460
type t
@@ -1463,12 +1463,12 @@ module CreusotContracts_Std1_Slice_Impl15_ProducesRefl
14631463
clone CreusotContracts_Std1_Slice_Impl15_Produces_Stub as Produces0 with
14641464
type t = t
14651465
function produces_refl (a : Core_Slice_Iter_Iter_Type.t_iter t) : () =
1466-
[#"../../../../creusot-contracts/src/std/slice.rs" 383 4 383 10] ()
1466+
[#"../../../../creusot-contracts/src/std/slice.rs" 382 4 382 10] ()
14671467
val produces_refl (a : Core_Slice_Iter_Iter_Type.t_iter t) : ()
1468-
ensures { [#"../../../../creusot-contracts/src/std/slice.rs" 385 14 385 39] Produces0.produces a (Seq.empty ) a }
1468+
ensures { [#"../../../../creusot-contracts/src/std/slice.rs" 384 14 384 39] Produces0.produces a (Seq.empty ) a }
14691469
ensures { result = produces_refl a }
14701470

1471-
axiom produces_refl_spec : forall a : Core_Slice_Iter_Iter_Type.t_iter t . [#"../../../../creusot-contracts/src/std/slice.rs" 385 14 385 39] Produces0.produces a (Seq.empty ) a
1471+
axiom produces_refl_spec : forall a : Core_Slice_Iter_Iter_Type.t_iter t . [#"../../../../creusot-contracts/src/std/slice.rs" 384 14 384 39] Produces0.produces a (Seq.empty ) a
14721472
end
14731473
module CreusotContracts_Std1_Slice_Impl15_ProducesTrans_Stub
14741474
type t
@@ -1490,12 +1490,12 @@ module CreusotContracts_Std1_Slice_Impl15_ProducesTrans_Interface
14901490
function produces_trans (a : Core_Slice_Iter_Iter_Type.t_iter t) (ab : Seq.seq t) (b : Core_Slice_Iter_Iter_Type.t_iter t) (bc : Seq.seq t) (c : Core_Slice_Iter_Iter_Type.t_iter t) : ()
14911491

14921492
val produces_trans (a : Core_Slice_Iter_Iter_Type.t_iter t) (ab : Seq.seq t) (b : Core_Slice_Iter_Iter_Type.t_iter t) (bc : Seq.seq t) (c : Core_Slice_Iter_Iter_Type.t_iter t) : ()
1493-
requires {[#"../../../../creusot-contracts/src/std/slice.rs" 390 15 390 32] Produces0.produces a ab b}
1494-
requires {[#"../../../../creusot-contracts/src/std/slice.rs" 391 15 391 32] Produces0.produces b bc c}
1495-
ensures { [#"../../../../creusot-contracts/src/std/slice.rs" 392 14 392 42] Produces0.produces a (Seq.(++) ab bc) c }
1493+
requires {[#"../../../../creusot-contracts/src/std/slice.rs" 389 15 389 32] Produces0.produces a ab b}
1494+
requires {[#"../../../../creusot-contracts/src/std/slice.rs" 390 15 390 32] Produces0.produces b bc c}
1495+
ensures { [#"../../../../creusot-contracts/src/std/slice.rs" 391 14 391 42] Produces0.produces a (Seq.(++) ab bc) c }
14961496
ensures { result = produces_trans a ab b bc c }
14971497

1498-
axiom produces_trans_spec : forall a : Core_Slice_Iter_Iter_Type.t_iter t, ab : Seq.seq t, b : Core_Slice_Iter_Iter_Type.t_iter t, bc : Seq.seq t, c : Core_Slice_Iter_Iter_Type.t_iter t . ([#"../../../../creusot-contracts/src/std/slice.rs" 390 15 390 32] Produces0.produces a ab b) -> ([#"../../../../creusot-contracts/src/std/slice.rs" 391 15 391 32] Produces0.produces b bc c) -> ([#"../../../../creusot-contracts/src/std/slice.rs" 392 14 392 42] Produces0.produces a (Seq.(++) ab bc) c)
1498+
axiom produces_trans_spec : forall a : Core_Slice_Iter_Iter_Type.t_iter t, ab : Seq.seq t, b : Core_Slice_Iter_Iter_Type.t_iter t, bc : Seq.seq t, c : Core_Slice_Iter_Iter_Type.t_iter t . ([#"../../../../creusot-contracts/src/std/slice.rs" 389 15 389 32] Produces0.produces a ab b) -> ([#"../../../../creusot-contracts/src/std/slice.rs" 390 15 390 32] Produces0.produces b bc c) -> ([#"../../../../creusot-contracts/src/std/slice.rs" 391 14 391 42] Produces0.produces a (Seq.(++) ab bc) c)
14991499
end
15001500
module CreusotContracts_Std1_Slice_Impl15_ProducesTrans
15011501
type t
@@ -1507,14 +1507,14 @@ module CreusotContracts_Std1_Slice_Impl15_ProducesTrans
15071507
function produces_trans (a : Core_Slice_Iter_Iter_Type.t_iter t) (ab : Seq.seq t) (b : Core_Slice_Iter_Iter_Type.t_iter t) (bc : Seq.seq t) (c : Core_Slice_Iter_Iter_Type.t_iter t) : ()
15081508

15091509
=
1510-
[#"../../../../creusot-contracts/src/std/slice.rs" 388 4 388 10] ()
1510+
[#"../../../../creusot-contracts/src/std/slice.rs" 387 4 387 10] ()
15111511
val produces_trans (a : Core_Slice_Iter_Iter_Type.t_iter t) (ab : Seq.seq t) (b : Core_Slice_Iter_Iter_Type.t_iter t) (bc : Seq.seq t) (c : Core_Slice_Iter_Iter_Type.t_iter t) : ()
1512-
requires {[#"../../../../creusot-contracts/src/std/slice.rs" 390 15 390 32] Produces0.produces a ab b}
1513-
requires {[#"../../../../creusot-contracts/src/std/slice.rs" 391 15 391 32] Produces0.produces b bc c}
1514-
ensures { [#"../../../../creusot-contracts/src/std/slice.rs" 392 14 392 42] Produces0.produces a (Seq.(++) ab bc) c }
1512+
requires {[#"../../../../creusot-contracts/src/std/slice.rs" 389 15 389 32] Produces0.produces a ab b}
1513+
requires {[#"../../../../creusot-contracts/src/std/slice.rs" 390 15 390 32] Produces0.produces b bc c}
1514+
ensures { [#"../../../../creusot-contracts/src/std/slice.rs" 391 14 391 42] Produces0.produces a (Seq.(++) ab bc) c }
15151515
ensures { result = produces_trans a ab b bc c }
15161516

1517-
axiom produces_trans_spec : forall a : Core_Slice_Iter_Iter_Type.t_iter t, ab : Seq.seq t, b : Core_Slice_Iter_Iter_Type.t_iter t, bc : Seq.seq t, c : Core_Slice_Iter_Iter_Type.t_iter t . ([#"../../../../creusot-contracts/src/std/slice.rs" 390 15 390 32] Produces0.produces a ab b) -> ([#"../../../../creusot-contracts/src/std/slice.rs" 391 15 391 32] Produces0.produces b bc c) -> ([#"../../../../creusot-contracts/src/std/slice.rs" 392 14 392 42] Produces0.produces a (Seq.(++) ab bc) c)
1517+
axiom produces_trans_spec : forall a : Core_Slice_Iter_Iter_Type.t_iter t, ab : Seq.seq t, b : Core_Slice_Iter_Iter_Type.t_iter t, bc : Seq.seq t, c : Core_Slice_Iter_Iter_Type.t_iter t . ([#"../../../../creusot-contracts/src/std/slice.rs" 389 15 389 32] Produces0.produces a ab b) -> ([#"../../../../creusot-contracts/src/std/slice.rs" 390 15 390 32] Produces0.produces b bc c) -> ([#"../../../../creusot-contracts/src/std/slice.rs" 391 14 391 42] Produces0.produces a (Seq.(++) ab bc) c)
15181518
end
15191519
module Hillel_InsertUnique_Interface
15201520
type t
@@ -2034,7 +2034,7 @@ module Core_Slice_Impl0_Len_Interface
20342034
type t = slice t,
20352035
type ShallowModelTy0.shallowModelTy = Seq.seq t
20362036
val len (self : slice t) : usize
2037-
ensures { [#"../../../../creusot-contracts/src/std/slice.rs" 232 0 325 1] Seq.length (ShallowModel0.shallow_model self) = UIntSize.to_int result }
2037+
ensures { [#"../../../../creusot-contracts/src/std/slice.rs" 232 0 324 1] Seq.length (ShallowModel0.shallow_model self) = UIntSize.to_int result }
20382038

20392039
end
20402040
module CreusotContracts_Std1_Iter_Iterator_Completed_Stub
@@ -2857,7 +2857,7 @@ module CreusotContracts_Std1_Slice_Impl11_IntoIterPre
28572857
use prelude.Borrow
28582858
use prelude.Slice
28592859
predicate into_iter_pre (self : slice t) =
2860-
[#"../../../../creusot-contracts/src/std/slice.rs" 331 20 331 24] true
2860+
[#"../../../../creusot-contracts/src/std/slice.rs" 330 20 330 24] true
28612861
val into_iter_pre (self : slice t) : bool
28622862
ensures { result = into_iter_pre self }
28632863

@@ -2887,7 +2887,7 @@ module CreusotContracts_Std1_Slice_Impl11_IntoIterPost
28872887
clone CreusotContracts_Std1_Slice_Impl13_ShallowModel_Stub as ShallowModel0 with
28882888
type t = t
28892889
predicate into_iter_post (self : slice t) (res : Core_Slice_Iter_Iter_Type.t_iter t) =
2890-
[#"../../../../creusot-contracts/src/std/slice.rs" 337 20 337 32] self = ShallowModel0.shallow_model res
2890+
[#"../../../../creusot-contracts/src/std/slice.rs" 336 20 336 32] self = ShallowModel0.shallow_model res
28912891
val into_iter_post (self : slice t) (res : Core_Slice_Iter_Iter_Type.t_iter t) : bool
28922892
ensures { result = into_iter_post self res }
28932893

‎creusot/tests/should_succeed/index_range.mlcfg‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -563,7 +563,7 @@ module Core_Slice_Impl0_Len_Interface
563563
type t = slice t,
564564
type ShallowModelTy0.shallowModelTy = Seq.seq t
565565
val len (self : slice t) : usize
566-
ensures { [#"../../../../creusot-contracts/src/std/slice.rs" 232 0 325 1] Seq.length (ShallowModel0.shallow_model self) = UIntSize.to_int result }
566+
ensures { [#"../../../../creusot-contracts/src/std/slice.rs" 232 0 324 1] Seq.length (ShallowModel0.shallow_model self) = UIntSize.to_int result }
567567

568568
end
569569
module Alloc_Vec_Impl9_Deref_Interface

‎creusot/tests/should_succeed/iterators/01_range.mlcfg‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -473,7 +473,7 @@ module CreusotContracts_Invariant_Impl1_Invariant
473473
clone CreusotContracts_Invariant_Invariant_Invariant_Stub as Invariant0 with
474474
type self = t
475475
predicate invariant' (self : borrowed t) =
476-
[#"../../../../../creusot-contracts/src/invariant.rs" 38 20 38 39] Invariant0.invariant' ( * self)
476+
[#"../../../../../creusot-contracts/src/invariant.rs" 36 20 36 39] Invariant0.invariant' ( * self)
477477
val invariant' (self : borrowed t) : bool
478478
ensures { result = invariant' self }
479479

‎creusot/tests/should_succeed/iterators/02_iter_mut.mlcfg‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -587,7 +587,7 @@ module CreusotContracts_Invariant_Impl1_Invariant
587587
clone CreusotContracts_Invariant_Invariant_Invariant_Stub as Invariant0 with
588588
type self = t
589589
predicate invariant' (self : borrowed t) =
590-
[#"../../../../../creusot-contracts/src/invariant.rs" 38 20 38 39] Invariant0.invariant' ( * self)
590+
[#"../../../../../creusot-contracts/src/invariant.rs" 36 20 36 39] Invariant0.invariant' ( * self)
591591
val invariant' (self : borrowed t) : bool
592592
ensures { result = invariant' self }
593593

0 commit comments

Comments
 (0)