From 8e81b4e60414ddac1072ce1e0902175c5781b41b Mon Sep 17 00:00:00 2001 From: arnaudgolfouse Date: Mon, 10 Mar 2025 11:20:52 +0100 Subject: [PATCH] Use subtraction of `Int` in `linked_list` --- tests/should_succeed/linked_list.coma | 526 +++++++++++--------- tests/should_succeed/linked_list.rs | 13 +- tests/should_succeed/linked_list/proof.json | 75 +-- 3 files changed, 320 insertions(+), 294 deletions(-) diff --git a/tests/should_succeed/linked_list.coma b/tests/should_succeed/linked_list.coma index ab5a407a0..c20ec98d8 100644 --- a/tests/should_succeed/linked_list.coma +++ b/tests/should_succeed/linked_list.coma @@ -1,6 +1,6 @@ -module M_linked_list__qyi10858349784728989480__new [#"linked_list.rs" 72 4 72 27] (* List *) - let%span slinked_list0 = "linked_list.rs" 72 20 72 27 - let%span slinked_list1 = "linked_list.rs" 71 14 71 35 +module M_linked_list__qyi10858349784728989480__new [#"linked_list.rs" 61 4 61 27] (* List *) + let%span slinked_list0 = "linked_list.rs" 61 20 61 27 + let%span slinked_list1 = "linked_list.rs" 60 14 60 35 let%span sptr2 = "../../creusot-contracts/src/std/ptr.rs" 121 22 121 44 let%span sseq3 = "../../creusot-contracts/src/logic/seq.rs" 427 4 427 34 let%span sseq4 = "../../creusot-contracts/src/logic/seq.rs" 425 14 425 36 @@ -8,7 +8,7 @@ module M_linked_list__qyi10858349784728989480__new [#"linked_list.rs" 72 4 72 27 let%span sptr6 = "../../creusot-contracts/src/std/ptr.rs" 80 14 80 48 let%span sptr7 = "../../creusot-contracts/src/std/ptr.rs" 82 8 82 30 let%span sghost8 = "../../creusot-contracts/src/ghost.rs" 224 4 224 12 - let%span slinked_list9 = "linked_list.rs" 67 4 67 41 + let%span slinked_list9 = "linked_list.rs" 56 4 56 41 let%span slinked_list10 = "linked_list.rs" 26 12 36 69 let%span sboxed11 = "../../creusot-contracts/src/std/boxed.rs" 33 8 33 18 let%span sseq12 = "../../creusot-contracts/src/logic/seq.rs" 629 20 629 95 @@ -134,7 +134,7 @@ module M_linked_list__qyi10858349784728989480__new [#"linked_list.rs" 72 4 72 27 | {t_List__first'0 = first ; t_List__last'0 = last ; t_List__seq'0 = seq} -> inv'1 seq end) - function seq_map'0 [#"linked_list.rs" 66 0 66 66] (s : Seq.seq t_PtrOwn'0) (f : Map.map t_PtrOwn'0 t_T'0) : Seq.seq t_T'0 + function seq_map'0 [#"linked_list.rs" 55 0 55 66] (s : Seq.seq t_PtrOwn'0) (f : Map.map t_PtrOwn'0 t_T'0) : Seq.seq t_T'0 = [%#slinked_list9] Seq.create (Seq.length s) (fun (i : int) -> Map.get f (Seq.get s i)) @@ -144,7 +144,7 @@ module M_linked_list__qyi10858349784728989480__new [#"linked_list.rs" 72 4 72 27 meta "compute_max_steps" 1000000 - let rec new'0[#"linked_list.rs" 72 4 72 27] (return' (ret:t_List'0))= (! bb0 + let rec new'0[#"linked_list.rs" 61 4 61 27] (return' (ret:t_List'0))= (! bb0 [ bb0 = s0 [ s0 = null'0 (fun (_ret':Opaque.ptr) -> [ &_2 <- _ret' ] s1) | s1 = bb1 ] | bb1 = s0 [ s0 = null'0 (fun (_ret':Opaque.ptr) -> [ &_3 <- _ret' ] s1) | s1 = bb2 ] | bb2 = s0 [ s0 = new'1 (fun (_ret':t_GhostBox'0) -> [ &_4 <- _ret' ] s1) | s1 = bb3 ] @@ -161,63 +161,66 @@ module M_linked_list__qyi10858349784728989480__new [#"linked_list.rs" 72 4 72 27 (! return' {result}) ] end -module M_linked_list__qyi10858349784728989480__push_back [#"linked_list.rs" 77 4 77 37] (* List *) - let%span slinked_list0 = "linked_list.rs" 77 26 77 30 - let%span slinked_list1 = "linked_list.rs" 77 32 77 33 - let%span slinked_list2 = "linked_list.rs" 76 14 76 47 - let%span sptr3 = "../../creusot-contracts/src/std/ptr.rs" 121 22 121 44 - let%span sptr_own4 = "../../creusot-contracts/src/ptr_own.rs" 68 20 68 23 - let%span sptr_own5 = "../../creusot-contracts/src/ptr_own.rs" 68 4 68 68 - let%span sptr_own6 = "../../creusot-contracts/src/ptr_own.rs" 67 14 67 67 - let%span sptr7 = "../../creusot-contracts/src/std/ptr.rs" 107 18 107 48 - let%span sghost8 = "../../creusot-contracts/src/ghost.rs" 69 14 69 18 - let%span sghost9 = "../../creusot-contracts/src/ghost.rs" 69 4 69 36 - let%span sghost10 = "../../creusot-contracts/src/ghost.rs" 68 14 68 35 - let%span sseq11 = "../../creusot-contracts/src/logic/seq.rs" 451 22 451 26 - let%span sseq12 = "../../creusot-contracts/src/logic/seq.rs" 450 14 450 34 - let%span slinked_list13 = "linked_list.rs" 56 10 56 25 - let%span sghost14 = "../../creusot-contracts/src/ghost.rs" 85 22 85 26 - let%span sghost15 = "../../creusot-contracts/src/ghost.rs" 85 4 85 48 - let%span sghost16 = "../../creusot-contracts/src/ghost.rs" 84 14 84 36 - let%span sseq17 = "../../creusot-contracts/src/logic/seq.rs" 553 30 553 34 - let%span sseq18 = "../../creusot-contracts/src/logic/seq.rs" 553 4 553 65 - let%span sseq19 = "../../creusot-contracts/src/logic/seq.rs" 547 14 550 5 - let%span sseq20 = "../../creusot-contracts/src/logic/seq.rs" 551 14 551 76 - let%span sseq21 = "../../creusot-contracts/src/logic/seq.rs" 552 14 552 44 - let%span soption22 = "../../creusot-contracts/src/std/option.rs" 89 27 89 39 - let%span soption23 = "../../creusot-contracts/src/std/option.rs" 90 26 90 46 - let%span sghost24 = "../../creusot-contracts/src/ghost.rs" 185 15 185 16 - let%span sghost25 = "../../creusot-contracts/src/ghost.rs" 185 4 185 28 - let%span sghost26 = "../../creusot-contracts/src/ghost.rs" 183 14 183 28 - let%span sptr_own27 = "../../creusot-contracts/src/ptr_own.rs" 104 41 104 44 - let%span sptr_own28 = "../../creusot-contracts/src/ptr_own.rs" 99 15 99 31 - let%span sptr_own29 = "../../creusot-contracts/src/ptr_own.rs" 104 4 104 81 - let%span sptr_own30 = "../../creusot-contracts/src/ptr_own.rs" 100 14 100 35 - let%span sptr_own31 = "../../creusot-contracts/src/ptr_own.rs" 102 14 102 53 - let%span sptr_own32 = "../../creusot-contracts/src/ptr_own.rs" 103 14 103 52 - let%span sghost33 = "../../creusot-contracts/src/ghost.rs" 210 22 210 26 - let%span sghost34 = "../../creusot-contracts/src/ghost.rs" 210 4 210 32 - let%span sghost35 = "../../creusot-contracts/src/ghost.rs" 208 14 208 31 - let%span sseq36 = "../../creusot-contracts/src/logic/seq.rs" 494 32 494 36 - let%span sseq37 = "../../creusot-contracts/src/logic/seq.rs" 494 38 494 39 - let%span sseq38 = "../../creusot-contracts/src/logic/seq.rs" 493 14 493 40 - let%span slinked_list39 = "linked_list.rs" 48 12 48 74 - let%span sptr40 = "../../creusot-contracts/src/std/ptr.rs" 80 14 80 48 - let%span sptr41 = "../../creusot-contracts/src/std/ptr.rs" 82 8 82 30 - let%span sghost42 = "../../creusot-contracts/src/ghost.rs" 224 4 224 12 - let%span sseq43 = "../../creusot-contracts/src/logic/seq.rs" 86 8 86 82 - let%span sresolve44 = "../../creusot-contracts/src/resolve.rs" 54 20 54 34 - let%span slinked_list45 = "linked_list.rs" 67 4 67 41 - let%span sseq46 = "../../creusot-contracts/src/logic/seq.rs" 629 20 629 95 - let%span sptr_own47 = "../../creusot-contracts/src/ptr_own.rs" 51 8 51 35 - let%span sinvariant48 = "../../creusot-contracts/src/invariant.rs" 35 20 35 44 - let%span sboxed49 = "../../creusot-contracts/src/std/boxed.rs" 33 8 33 18 - let%span sinvariant50 = "../../creusot-contracts/src/invariant.rs" 25 8 25 18 - let%span slinked_list51 = "linked_list.rs" 26 12 36 69 +module M_linked_list__qyi10858349784728989480__push_back [#"linked_list.rs" 66 4 66 37] (* List *) + let%span slinked_list0 = "linked_list.rs" 75 53 75 57 + let%span slinked_list1 = "linked_list.rs" 66 26 66 30 + let%span slinked_list2 = "linked_list.rs" 66 32 66 33 + let%span slinked_list3 = "linked_list.rs" 65 14 65 47 + let%span sptr4 = "../../creusot-contracts/src/std/ptr.rs" 121 22 121 44 + let%span sptr_own5 = "../../creusot-contracts/src/ptr_own.rs" 68 20 68 23 + let%span sptr_own6 = "../../creusot-contracts/src/ptr_own.rs" 68 4 68 68 + let%span sptr_own7 = "../../creusot-contracts/src/ptr_own.rs" 67 14 67 67 + let%span sptr8 = "../../creusot-contracts/src/std/ptr.rs" 107 18 107 48 + let%span sghost9 = "../../creusot-contracts/src/ghost.rs" 69 14 69 18 + let%span sghost10 = "../../creusot-contracts/src/ghost.rs" 69 4 69 36 + let%span sghost11 = "../../creusot-contracts/src/ghost.rs" 68 14 68 35 + let%span sseq12 = "../../creusot-contracts/src/logic/seq.rs" 451 22 451 26 + let%span sseq13 = "../../creusot-contracts/src/logic/seq.rs" 450 14 450 34 + let%span sint14 = "../../creusot-contracts/src/logic/int.rs" 56 14 56 31 + let%span sghost15 = "../../creusot-contracts/src/ghost.rs" 210 22 210 26 + let%span sghost16 = "../../creusot-contracts/src/ghost.rs" 210 4 210 32 + let%span sghost17 = "../../creusot-contracts/src/ghost.rs" 208 14 208 31 + let%span sint18 = "../../creusot-contracts/src/logic/int.rs" 258 14 258 36 + let%span sghost19 = "../../creusot-contracts/src/ghost.rs" 85 22 85 26 + let%span sghost20 = "../../creusot-contracts/src/ghost.rs" 85 4 85 48 + let%span sghost21 = "../../creusot-contracts/src/ghost.rs" 84 14 84 36 + let%span sseq22 = "../../creusot-contracts/src/logic/seq.rs" 553 30 553 34 + let%span sseq23 = "../../creusot-contracts/src/logic/seq.rs" 553 4 553 65 + let%span sseq24 = "../../creusot-contracts/src/logic/seq.rs" 547 14 550 5 + let%span sseq25 = "../../creusot-contracts/src/logic/seq.rs" 551 14 551 76 + let%span sseq26 = "../../creusot-contracts/src/logic/seq.rs" 552 14 552 44 + let%span soption27 = "../../creusot-contracts/src/std/option.rs" 89 27 89 39 + let%span soption28 = "../../creusot-contracts/src/std/option.rs" 90 26 90 46 + let%span sghost29 = "../../creusot-contracts/src/ghost.rs" 185 15 185 16 + let%span sghost30 = "../../creusot-contracts/src/ghost.rs" 185 4 185 28 + let%span sghost31 = "../../creusot-contracts/src/ghost.rs" 183 14 183 28 + let%span sptr_own32 = "../../creusot-contracts/src/ptr_own.rs" 104 41 104 44 + let%span sptr_own33 = "../../creusot-contracts/src/ptr_own.rs" 99 15 99 31 + let%span sptr_own34 = "../../creusot-contracts/src/ptr_own.rs" 104 4 104 81 + let%span sptr_own35 = "../../creusot-contracts/src/ptr_own.rs" 100 14 100 35 + let%span sptr_own36 = "../../creusot-contracts/src/ptr_own.rs" 102 14 102 53 + let%span sptr_own37 = "../../creusot-contracts/src/ptr_own.rs" 103 14 103 52 + let%span sseq38 = "../../creusot-contracts/src/logic/seq.rs" 494 32 494 36 + let%span sseq39 = "../../creusot-contracts/src/logic/seq.rs" 494 38 494 39 + let%span sseq40 = "../../creusot-contracts/src/logic/seq.rs" 493 14 493 40 + let%span slinked_list41 = "linked_list.rs" 48 12 48 74 + let%span sptr42 = "../../creusot-contracts/src/std/ptr.rs" 80 14 80 48 + let%span sptr43 = "../../creusot-contracts/src/std/ptr.rs" 82 8 82 30 + let%span sghost44 = "../../creusot-contracts/src/ghost.rs" 224 4 224 12 + let%span sseq45 = "../../creusot-contracts/src/logic/seq.rs" 86 8 86 82 + let%span sresolve46 = "../../creusot-contracts/src/resolve.rs" 54 20 54 34 + let%span slinked_list47 = "linked_list.rs" 56 4 56 41 + let%span sseq48 = "../../creusot-contracts/src/logic/seq.rs" 629 20 629 95 + let%span sptr_own49 = "../../creusot-contracts/src/ptr_own.rs" 51 8 51 35 + let%span sinvariant50 = "../../creusot-contracts/src/invariant.rs" 35 20 35 44 + let%span sboxed51 = "../../creusot-contracts/src/std/boxed.rs" 33 8 33 18 + let%span sinvariant52 = "../../creusot-contracts/src/invariant.rs" 25 8 25 18 + let%span slinked_list53 = "linked_list.rs" 26 12 36 69 use creusot.prelude.Opaque use seq.Seq use mach.int.Int + use creusot.int.Int128 use creusot.prelude.MutBorrow use creusot.prelude.Any use map.Map @@ -225,12 +228,12 @@ module M_linked_list__qyi10858349784728989480__push_back [#"linked_list.rs" 77 4 function addr_logic'0 (self : Opaque.ptr) : int function is_null_logic'0 (self : Opaque.ptr) : bool = - [%#sptr41] addr_logic'0 self = 0 + [%#sptr43] addr_logic'0 self = 0 - axiom is_null_logic'0_spec : forall self : Opaque.ptr . [%#sptr40] is_null_logic'0 self = (addr_logic'0 self = 0) + axiom is_null_logic'0_spec : forall self : Opaque.ptr . [%#sptr42] is_null_logic'0 self = (addr_logic'0 self = 0) let rec null'0 (return' (ret:Opaque.ptr))= any - [ return' (result:Opaque.ptr)-> {[%#sptr3] is_null_logic'0 result} (! return' {result}) ] + [ return' (result:Opaque.ptr)-> {[%#sptr4] is_null_logic'0 result} (! return' {result}) ] type t_T'0 @@ -254,7 +257,7 @@ module M_linked_list__qyi10858349784728989480__push_back [#"linked_list.rs" 77 4 end predicate invariant'6 (self : t_Cell'0) = - [%#sboxed49] inv'3 self + [%#sboxed51] inv'3 self predicate inv'9 (_1 : t_Cell'0) @@ -263,7 +266,7 @@ module M_linked_list__qyi10858349784728989480__push_back [#"linked_list.rs" 77 4 function ptr'0 (self : t_PtrOwn'0) : Opaque.ptr predicate invariant'1 (self : t_PtrOwn'0) = - [%#sptr_own47] not is_null_logic'0 (ptr'0 self) + [%#sptr_own49] not is_null_logic'0 (ptr'0 self) predicate inv'2 (_1 : t_PtrOwn'0) @@ -274,114 +277,139 @@ module M_linked_list__qyi10858349784728989480__push_back [#"linked_list.rs" 77 4 end) predicate invariant'11 (self : t_PtrOwn'0) = - [%#sboxed49] inv'2 self + [%#sboxed51] inv'2 self - predicate inv'20 (_1 : t_PtrOwn'0) + predicate inv'22 (_1 : t_PtrOwn'0) - axiom inv_axiom'19 [@rewrite] : forall x : t_PtrOwn'0 [inv'20 x] . inv'20 x = invariant'11 x + axiom inv_axiom'21 [@rewrite] : forall x : t_PtrOwn'0 [inv'22 x] . inv'22 x = invariant'11 x - predicate inv'16 (_1 : t_GhostBox'0) + predicate inv'18 (_1 : t_GhostBox'0) - axiom inv_axiom'15 [@rewrite] : forall x : t_GhostBox'0 [inv'16 x] . inv'16 x + axiom inv_axiom'17 [@rewrite] : forall x : t_GhostBox'0 [inv'18 x] . inv'18 x = match x with - | {t_GhostBox__0'0 = a_0} -> inv'20 a_0 + | {t_GhostBox__0'0 = a_0} -> inv'22 a_0 end predicate inv'10 (_1 : (Opaque.ptr, t_GhostBox'0)) axiom inv_axiom'9 [@rewrite] : forall x : (Opaque.ptr, t_GhostBox'0) [inv'10 x] . inv'10 x - = (let (x0, x1) = x in inv'16 x1) + = (let (x0, x1) = x in inv'18 x1) function inner_logic'0 (self : t_GhostBox'0) : t_PtrOwn'0 = - [%#sghost42] self.t_GhostBox__0'0 + [%#sghost44] self.t_GhostBox__0'0 function val'0 (self : t_PtrOwn'0) : t_Cell'0 - let rec from_box'0 (val':t_Cell'0) (return' (ret:(Opaque.ptr, t_GhostBox'0)))= {[@expl:from_box 'val' type invariant] [%#sptr_own4] inv'9 val'} + let rec from_box'0 (val':t_Cell'0) (return' (ret:(Opaque.ptr, t_GhostBox'0)))= {[@expl:from_box 'val' type invariant] [%#sptr_own5] inv'9 val'} any - [ return' (result:(Opaque.ptr, t_GhostBox'0))-> {[%#sptr_own5] inv'10 result} - {[%#sptr_own6] ptr'0 (inner_logic'0 (let (_, a) = result in a)) = (let (a, _) = result in a) + [ return' (result:(Opaque.ptr, t_GhostBox'0))-> {[%#sptr_own6] inv'10 result} + {[%#sptr_own7] ptr'0 (inner_logic'0 (let (_, a) = result in a)) = (let (a, _) = result in a) /\ val'0 (inner_logic'0 (let (_, a) = result in a)) = val'} (! return' {result}) ] - type t_GhostBox'1 = + type t_GhostBox'2 = { t_GhostBox__0'1: Seq.seq t_PtrOwn'0 } type t_List'0 = - { t_List__first'0: Opaque.ptr; t_List__last'0: Opaque.ptr; t_List__seq'0: t_GhostBox'1 } + { t_List__first'0: Opaque.ptr; t_List__last'0: Opaque.ptr; t_List__seq'0: t_GhostBox'2 } let rec is_null'0 (self:Opaque.ptr) (return' (ret:bool))= any - [ return' (result:bool)-> {[%#sptr7] result = is_null_logic'0 self} (! return' {result}) ] + [ return' (result:bool)-> {[%#sptr8] result = is_null_logic'0 self} (! return' {result}) ] predicate invariant'0 (self : Seq.seq t_PtrOwn'0) = - [%#sseq46] forall i : int . 0 <= i /\ i < Seq.length self -> inv'20 (Seq.get self i) + [%#sseq48] forall i : int . 0 <= i /\ i < Seq.length self -> inv'22 (Seq.get self i) predicate inv'1 (_1 : Seq.seq t_PtrOwn'0) axiom inv_axiom'1 [@rewrite] : forall x : Seq.seq t_PtrOwn'0 [inv'1 x] . inv'1 x = invariant'0 x predicate invariant'10 (self : Seq.seq t_PtrOwn'0) = - [%#sboxed49] inv'1 self + [%#sboxed51] inv'1 self - predicate inv'19 (_1 : Seq.seq t_PtrOwn'0) + predicate inv'21 (_1 : Seq.seq t_PtrOwn'0) - axiom inv_axiom'18 [@rewrite] : forall x : Seq.seq t_PtrOwn'0 [inv'19 x] . inv'19 x = invariant'10 x + axiom inv_axiom'20 [@rewrite] : forall x : Seq.seq t_PtrOwn'0 [inv'21 x] . inv'21 x = invariant'10 x - predicate inv'0 (_1 : t_GhostBox'1) + predicate inv'0 (_1 : t_GhostBox'2) - axiom inv_axiom'0 [@rewrite] : forall x : t_GhostBox'1 [inv'0 x] . inv'0 x + axiom inv_axiom'0 [@rewrite] : forall x : t_GhostBox'2 [inv'0 x] . inv'0 x = match x with - | {t_GhostBox__0'1 = a_0} -> inv'19 a_0 + | {t_GhostBox__0'1 = a_0} -> inv'21 a_0 end - predicate invariant'7 (self : t_GhostBox'1) = - [%#sinvariant50] inv'0 self + predicate invariant'7 (self : t_GhostBox'2) = + [%#sinvariant52] inv'0 self - predicate inv'11 (_1 : t_GhostBox'1) + predicate inv'11 (_1 : t_GhostBox'2) - axiom inv_axiom'10 [@rewrite] : forall x : t_GhostBox'1 [inv'11 x] . inv'11 x = invariant'7 x + axiom inv_axiom'10 [@rewrite] : forall x : t_GhostBox'2 [inv'11 x] . inv'11 x = invariant'7 x predicate invariant'8 (self : Seq.seq t_PtrOwn'0) = - [%#sinvariant50] inv'1 self + [%#sinvariant52] inv'1 self predicate inv'12 (_1 : Seq.seq t_PtrOwn'0) axiom inv_axiom'11 [@rewrite] : forall x : Seq.seq t_PtrOwn'0 [inv'12 x] . inv'12 x = invariant'8 x - let rec deref'0 (self:t_GhostBox'1) (return' (ret:Seq.seq t_PtrOwn'0))= {[@expl:deref 'self' type invariant] [%#sghost8] inv'11 self} + let rec deref'0 (self:t_GhostBox'2) (return' (ret:Seq.seq t_PtrOwn'0))= {[@expl:deref 'self' type invariant] [%#sghost9] inv'11 self} any - [ return' (result:Seq.seq t_PtrOwn'0)-> {[%#sghost9] inv'12 result} - {[%#sghost10] self.t_GhostBox__0'1 = result} + [ return' (result:Seq.seq t_PtrOwn'0)-> {[%#sghost10] inv'12 result} + {[%#sghost11] self.t_GhostBox__0'1 = result} (! return' {result}) ] - let rec len_ghost'0 (self:Seq.seq t_PtrOwn'0) (return' (ret:int))= {[@expl:len_ghost 'self' type invariant] [%#sseq11] inv'12 self} - any [ return' (result:int)-> {[%#sseq12] result = Seq.length self} (! return' {result}) ] + let rec len_ghost'0 (self:Seq.seq t_PtrOwn'0) (return' (ret:int))= {[@expl:len_ghost 'self' type invariant] [%#sseq12] inv'12 self} + any [ return' (result:int)-> {[%#sseq13] result = Seq.length self} (! return' {result}) ] + + type t_GhostBox'1 = + { t_GhostBox__0'2: int } + + function inner_logic'1 (self : t_GhostBox'1) : int = + [%#sghost44] self.t_GhostBox__0'2 + + let rec new'0 (value:Int128.t) (return' (ret:t_GhostBox'1))= any + [ return' (result:t_GhostBox'1)-> {[%#sint14] inner_logic'1 result = Int128.to_int value} (! return' {result}) ] + - let rec minus_one'0 (x:int) (return' (ret:int))= any - [ return' (result:int)-> {[%#slinked_list13] result = x - 1} (! return' {result}) ] + predicate inv'13 (_1 : t_GhostBox'1) + axiom inv_axiom'12 [@rewrite] : forall x : t_GhostBox'1 [inv'13 x] . inv'13 x = true - predicate invariant'9 (self : MutBorrow.t t_GhostBox'1) = - [%#sinvariant48] inv'0 self.current /\ inv'0 self.final + predicate inv'14 (_1 : int) - predicate inv'13 (_1 : MutBorrow.t t_GhostBox'1) + axiom inv_axiom'13 [@rewrite] : forall x : int [inv'14 x] . inv'14 x = true - axiom inv_axiom'12 [@rewrite] : forall x : MutBorrow.t t_GhostBox'1 [inv'13 x] . inv'13 x = invariant'9 x + let rec into_inner'0 (self:t_GhostBox'1) (return' (ret:int))= {[@expl:into_inner 'self' type invariant] [%#sghost15] inv'13 self} + any + [ return' (result:int)-> {[%#sghost16] inv'14 result} + {[%#sghost17] result = self.t_GhostBox__0'2} + (! return' {result}) ] + + + let rec sub'0 (self:int) (other:int) (return' (ret:int))= any + [ return' (result:int)-> {[%#sint18] result = self - other} (! return' {result}) ] + + + predicate invariant'9 (self : MutBorrow.t t_GhostBox'2) = + [%#sinvariant50] inv'0 self.current /\ inv'0 self.final + + predicate inv'15 (_1 : MutBorrow.t t_GhostBox'2) + + axiom inv_axiom'14 [@rewrite] : forall x : MutBorrow.t t_GhostBox'2 [inv'15 x] . inv'15 x = invariant'9 x predicate invariant'2 (self : MutBorrow.t (Seq.seq t_PtrOwn'0)) = - [%#sinvariant48] inv'1 self.current /\ inv'1 self.final + [%#sinvariant50] inv'1 self.current /\ inv'1 self.final predicate inv'4 (_1 : MutBorrow.t (Seq.seq t_PtrOwn'0)) axiom inv_axiom'4 [@rewrite] : forall x : MutBorrow.t (Seq.seq t_PtrOwn'0) [inv'4 x] . inv'4 x = invariant'2 x - let rec deref_mut'0 (self:MutBorrow.t t_GhostBox'1) (return' (ret:MutBorrow.t (Seq.seq t_PtrOwn'0)))= {[@expl:deref_mut 'self' type invariant] [%#sghost14] inv'13 self} + let rec deref_mut'0 (self:MutBorrow.t t_GhostBox'2) (return' (ret:MutBorrow.t (Seq.seq t_PtrOwn'0)))= {[@expl:deref_mut 'self' type invariant] [%#sghost19] inv'15 self} any - [ return' (result:MutBorrow.t (Seq.seq t_PtrOwn'0))-> {[%#sghost15] inv'4 result} - {[%#sghost16] result + [ return' (result:MutBorrow.t (Seq.seq t_PtrOwn'0))-> {[%#sghost20] inv'4 result} + {[%#sghost21] result = MutBorrow.borrow_logic (self.current).t_GhostBox__0'1 (self.final).t_GhostBox__0'1 (MutBorrow.inherit_id (MutBorrow.get_id self) 1)} (! return' {result}) ] @@ -391,15 +419,15 @@ module M_linked_list__qyi10858349784728989480__push_back [#"linked_list.rs" 77 4 | C_Some'0 (MutBorrow.t t_PtrOwn'0) predicate invariant'3 (self : MutBorrow.t t_PtrOwn'0) = - [%#sinvariant48] inv'2 self.current /\ inv'2 self.final + [%#sinvariant50] inv'2 self.current /\ inv'2 self.final predicate inv'5 (_1 : MutBorrow.t t_PtrOwn'0) axiom inv_axiom'5 [@rewrite] : forall x : MutBorrow.t t_PtrOwn'0 [inv'5 x] . inv'5 x = invariant'3 x - predicate inv'14 (_1 : t_Option'0) + predicate inv'16 (_1 : t_Option'0) - axiom inv_axiom'13 [@rewrite] : forall x : t_Option'0 [inv'14 x] . inv'14 x + axiom inv_axiom'15 [@rewrite] : forall x : t_Option'0 [inv'16 x] . inv'16 x = match x with | C_None'0 -> true | C_Some'0 a_0 -> inv'5 a_0 @@ -410,168 +438,168 @@ module M_linked_list__qyi10858349784728989480__push_back [#"linked_list.rs" 77 4 | C_Some'1 t_PtrOwn'0 function get'0 (self : Seq.seq t_PtrOwn'0) (ix : int) : t_Option'1 = - [%#sseq43] if 0 <= ix /\ ix < Seq.length self then C_Some'1 (Seq.get self ix) else C_None'1 + [%#sseq45] if 0 <= ix /\ ix < Seq.length self then C_Some'1 (Seq.get self ix) else C_None'1 - let rec get_mut_ghost'0 (self:MutBorrow.t (Seq.seq t_PtrOwn'0)) (index:int) (return' (ret:t_Option'0))= {[@expl:get_mut_ghost 'self' type invariant] [%#sseq17] inv'4 self} + let rec get_mut_ghost'0 (self:MutBorrow.t (Seq.seq t_PtrOwn'0)) (index:int) (return' (ret:t_Option'0))= {[@expl:get_mut_ghost 'self' type invariant] [%#sseq22] inv'4 self} any - [ return' (result:t_Option'0)-> {[%#sseq18] inv'14 result} - {[%#sseq19] match result with + [ return' (result:t_Option'0)-> {[%#sseq23] inv'16 result} + {[%#sseq24] match result with | C_None'0 -> get'0 self.current index = C_None'1 /\ self.current = self.final | C_Some'0 r -> get'0 self.current index = C_Some'1 (r.current) /\ r.final = Seq.get self.final index end} - {[%#sseq20] forall i : int . i <> index -> get'0 self.current i = get'0 self.final i} - {[%#sseq21] Seq.length self.current = Seq.length self.final} + {[%#sseq25] forall i : int . i <> index -> get'0 self.current i = get'0 self.final i} + {[%#sseq26] Seq.length self.current = Seq.length self.final} (! return' {result}) ] - let rec unwrap'0 (self:t_Option'0) (return' (ret:MutBorrow.t t_PtrOwn'0))= {[@expl:unwrap 'self' type invariant] inv'14 self} - {[@expl:unwrap requires] [%#soption22] self <> C_None'0} + let rec unwrap'0 (self:t_Option'0) (return' (ret:MutBorrow.t t_PtrOwn'0))= {[@expl:unwrap 'self' type invariant] inv'16 self} + {[@expl:unwrap requires] [%#soption27] self <> C_None'0} any [ return' (result:MutBorrow.t t_PtrOwn'0)-> {inv'5 result} - {[%#soption23] C_Some'0 result = self} + {[%#soption28] C_Some'0 result = self} (! return' {result}) ] - type t_GhostBox'2 = - { t_GhostBox__0'2: MutBorrow.t t_PtrOwn'0 } + type t_GhostBox'3 = + { t_GhostBox__0'3: MutBorrow.t t_PtrOwn'0 } predicate invariant'12 (self : MutBorrow.t t_PtrOwn'0) = - [%#sboxed49] inv'5 self + [%#sboxed51] inv'5 self - predicate inv'21 (_1 : MutBorrow.t t_PtrOwn'0) + predicate inv'23 (_1 : MutBorrow.t t_PtrOwn'0) - axiom inv_axiom'20 [@rewrite] : forall x : MutBorrow.t t_PtrOwn'0 [inv'21 x] . inv'21 x = invariant'12 x + axiom inv_axiom'22 [@rewrite] : forall x : MutBorrow.t t_PtrOwn'0 [inv'23 x] . inv'23 x = invariant'12 x - predicate inv'15 (_1 : t_GhostBox'2) + predicate inv'17 (_1 : t_GhostBox'3) - axiom inv_axiom'14 [@rewrite] : forall x : t_GhostBox'2 [inv'15 x] . inv'15 x + axiom inv_axiom'16 [@rewrite] : forall x : t_GhostBox'3 [inv'17 x] . inv'17 x = match x with - | {t_GhostBox__0'2 = a_0} -> inv'21 a_0 + | {t_GhostBox__0'3 = a_0} -> inv'23 a_0 end - let rec new'0 (x:MutBorrow.t t_PtrOwn'0) (return' (ret:t_GhostBox'2))= {[@expl:new 'x' type invariant] [%#sghost24] inv'5 x} + let rec new'1 (x:MutBorrow.t t_PtrOwn'0) (return' (ret:t_GhostBox'3))= {[@expl:new 'x' type invariant] [%#sghost29] inv'5 x} any - [ return' (result:t_GhostBox'2)-> {[%#sghost25] inv'15 result} - {[%#sghost26] result.t_GhostBox__0'2 = x} + [ return' (result:t_GhostBox'3)-> {[%#sghost30] inv'17 result} + {[%#sghost31] result.t_GhostBox__0'3 = x} (! return' {result}) ] - function inner_logic'1 (self : t_GhostBox'2) : MutBorrow.t t_PtrOwn'0 = - [%#sghost42] self.t_GhostBox__0'2 + function inner_logic'2 (self : t_GhostBox'3) : MutBorrow.t t_PtrOwn'0 = + [%#sghost44] self.t_GhostBox__0'3 predicate invariant'4 (self : MutBorrow.t t_Cell'0) = - [%#sinvariant48] inv'3 self.current /\ inv'3 self.final + [%#sinvariant50] inv'3 self.current /\ inv'3 self.final predicate inv'6 (_1 : MutBorrow.t t_Cell'0) axiom inv_axiom'6 [@rewrite] : forall x : MutBorrow.t t_Cell'0 [inv'6 x] . inv'6 x = invariant'4 x - let rec as_mut'0 (ptr:Opaque.ptr) (own:t_GhostBox'2) (return' (ret:MutBorrow.t t_Cell'0))= {[@expl:as_mut 'own' type invariant] [%#sptr_own27] inv'15 own} - {[@expl:as_mut requires] [%#sptr_own28] ptr = ptr'0 (inner_logic'1 own).current} + let rec as_mut'0 (ptr:Opaque.ptr) (own:t_GhostBox'3) (return' (ret:MutBorrow.t t_Cell'0))= {[@expl:as_mut 'own' type invariant] [%#sptr_own32] inv'17 own} + {[@expl:as_mut requires] [%#sptr_own33] ptr = ptr'0 (inner_logic'2 own).current} any - [ return' (result:MutBorrow.t t_Cell'0)-> {[%#sptr_own29] inv'6 result} - {[%#sptr_own30] result.current = val'0 (inner_logic'1 own).current} - {[%#sptr_own31] ptr'0 (inner_logic'1 own).final = ptr'0 (inner_logic'1 own).current} - {[%#sptr_own32] val'0 (inner_logic'1 own).final = result.final} + [ return' (result:MutBorrow.t t_Cell'0)-> {[%#sptr_own34] inv'6 result} + {[%#sptr_own35] result.current = val'0 (inner_logic'2 own).current} + {[%#sptr_own36] ptr'0 (inner_logic'2 own).final = ptr'0 (inner_logic'2 own).current} + {[%#sptr_own37] val'0 (inner_logic'2 own).final = result.final} (! return' {result}) ] predicate resolve'4 (self : MutBorrow.t (Seq.seq t_PtrOwn'0)) = - [%#sresolve44] self.final = self.current + [%#sresolve46] self.final = self.current predicate resolve'0 (_1 : MutBorrow.t (Seq.seq t_PtrOwn'0)) = resolve'4 _1 predicate resolve'5 (self : MutBorrow.t t_PtrOwn'0) = - [%#sresolve44] self.final = self.current + [%#sresolve46] self.final = self.current predicate resolve'1 (_1 : MutBorrow.t t_PtrOwn'0) = resolve'5 _1 predicate resolve'6 (self : MutBorrow.t t_Cell'0) = - [%#sresolve44] self.final = self.current + [%#sresolve46] self.final = self.current predicate resolve'2 (_1 : MutBorrow.t t_Cell'0) = resolve'6 _1 - let rec into_inner'0 (self:t_GhostBox'0) (return' (ret:t_PtrOwn'0))= {[@expl:into_inner 'self' type invariant] [%#sghost33] inv'16 self} + let rec into_inner'1 (self:t_GhostBox'0) (return' (ret:t_PtrOwn'0))= {[@expl:into_inner 'self' type invariant] [%#sghost15] inv'18 self} any - [ return' (result:t_PtrOwn'0)-> {[%#sghost34] inv'2 result} - {[%#sghost35] result = self.t_GhostBox__0'0} + [ return' (result:t_PtrOwn'0)-> {[%#sghost16] inv'2 result} + {[%#sghost17] result = self.t_GhostBox__0'0} (! return' {result}) ] - let rec push_back_ghost'0 (self:MutBorrow.t (Seq.seq t_PtrOwn'0)) (x:t_PtrOwn'0) (return' (ret:()))= {[@expl:push_back_ghost 'self' type invariant] [%#sseq36] inv'4 self} - {[@expl:push_back_ghost 'x' type invariant] [%#sseq37] inv'2 x} - any [ return' (result:())-> {[%#sseq38] self.final = Seq.snoc self.current x} (! return' {result}) ] + let rec push_back_ghost'0 (self:MutBorrow.t (Seq.seq t_PtrOwn'0)) (x:t_PtrOwn'0) (return' (ret:()))= {[@expl:push_back_ghost 'self' type invariant] [%#sseq38] inv'4 self} + {[@expl:push_back_ghost 'x' type invariant] [%#sseq39] inv'2 x} + any [ return' (result:())-> {[%#sseq40] self.final = Seq.snoc self.current x} (! return' {result}) ] - function inner_logic'2 (self : t_GhostBox'1) : Seq.seq t_PtrOwn'0 = - [%#sghost42] self.t_GhostBox__0'1 + function inner_logic'3 (self : t_GhostBox'2) : Seq.seq t_PtrOwn'0 = + [%#sghost44] self.t_GhostBox__0'1 predicate invariant'13 [#"linked_list.rs" 24 4 24 30] (self : t_List'0) = - [%#slinked_list51] inner_logic'2 self.t_List__seq'0 = (Seq.empty : Seq.seq t_PtrOwn'0) + [%#slinked_list53] inner_logic'3 self.t_List__seq'0 = (Seq.empty : Seq.seq t_PtrOwn'0) /\ is_null_logic'0 self.t_List__first'0 /\ is_null_logic'0 self.t_List__last'0 - \/ Seq.length (inner_logic'2 self.t_List__seq'0) > 0 - /\ self.t_List__first'0 = ptr'0 (Seq.get (inner_logic'2 self.t_List__seq'0) 0) + \/ Seq.length (inner_logic'3 self.t_List__seq'0) > 0 + /\ self.t_List__first'0 = ptr'0 (Seq.get (inner_logic'3 self.t_List__seq'0) 0) /\ self.t_List__last'0 - = ptr'0 (Seq.get (inner_logic'2 self.t_List__seq'0) (Seq.length (inner_logic'2 self.t_List__seq'0) - 1)) - /\ (forall i : int . 0 <= i /\ i < Seq.length (inner_logic'2 self.t_List__seq'0) - 1 - -> (val'0 (Seq.get (inner_logic'2 self.t_List__seq'0) i)).t_Cell__next'0 - = ptr'0 (Seq.get (inner_logic'2 self.t_List__seq'0) (i + 1))) - /\ is_null_logic'0 (val'0 (Seq.get (inner_logic'2 self.t_List__seq'0) (Seq.length (inner_logic'2 self.t_List__seq'0) + = ptr'0 (Seq.get (inner_logic'3 self.t_List__seq'0) (Seq.length (inner_logic'3 self.t_List__seq'0) - 1)) + /\ (forall i : int . 0 <= i /\ i < Seq.length (inner_logic'3 self.t_List__seq'0) - 1 + -> (val'0 (Seq.get (inner_logic'3 self.t_List__seq'0) i)).t_Cell__next'0 + = ptr'0 (Seq.get (inner_logic'3 self.t_List__seq'0) (i + 1))) + /\ is_null_logic'0 (val'0 (Seq.get (inner_logic'3 self.t_List__seq'0) (Seq.length (inner_logic'3 self.t_List__seq'0) - 1))).t_Cell__next'0 - predicate inv'22 (_1 : t_List'0) + predicate inv'24 (_1 : t_List'0) - axiom inv_axiom'21 [@rewrite] : forall x : t_List'0 [inv'22 x] . inv'22 x + axiom inv_axiom'23 [@rewrite] : forall x : t_List'0 [inv'24 x] . inv'24 x = (invariant'13 x /\ match x with | {t_List__first'0 = first ; t_List__last'0 = last ; t_List__seq'0 = seq} -> inv'0 seq end) predicate invariant'5 (self : MutBorrow.t t_List'0) = - [%#sinvariant48] inv'22 self.current /\ inv'22 self.final + [%#sinvariant50] inv'24 self.current /\ inv'24 self.final predicate inv'7 (_1 : MutBorrow.t t_List'0) axiom inv_axiom'7 [@rewrite] : forall x : MutBorrow.t t_List'0 [inv'7 x] . inv'7 x = invariant'5 x predicate resolve'7 (self : MutBorrow.t t_List'0) = - [%#sresolve44] self.final = self.current + [%#sresolve46] self.final = self.current predicate resolve'3 (_1 : MutBorrow.t t_List'0) = resolve'7 _1 - type t_GhostBox'3 = - { t_GhostBox__0'3: () } + type t_GhostBox'4 = + { t_GhostBox__0'4: () } - predicate inv'17 (_1 : ()) + predicate inv'19 (_1 : ()) - axiom inv_axiom'16 [@rewrite] : forall x : () [inv'17 x] . inv'17 x = true + axiom inv_axiom'18 [@rewrite] : forall x : () [inv'19 x] . inv'19 x = true - predicate inv'18 (_1 : t_GhostBox'3) + predicate inv'20 (_1 : t_GhostBox'4) - axiom inv_axiom'17 [@rewrite] : forall x : t_GhostBox'3 [inv'18 x] . inv'18 x = true + axiom inv_axiom'19 [@rewrite] : forall x : t_GhostBox'4 [inv'20 x] . inv'20 x = true - let rec new'1 (x:()) (return' (ret:t_GhostBox'3))= {[@expl:new 'x' type invariant] [%#sghost24] inv'17 x} + let rec new'2 (x:()) (return' (ret:t_GhostBox'4))= {[@expl:new 'x' type invariant] [%#sghost29] inv'19 x} any - [ return' (result:t_GhostBox'3)-> {[%#sghost25] inv'18 result} - {[%#sghost26] result.t_GhostBox__0'3 = x} + [ return' (result:t_GhostBox'4)-> {[%#sghost30] inv'20 result} + {[%#sghost31] result.t_GhostBox__0'4 = x} (! return' {result}) ] - function seq_map'0 [#"linked_list.rs" 66 0 66 66] (s : Seq.seq t_PtrOwn'0) (f : Map.map t_PtrOwn'0 t_T'0) : Seq.seq t_T'0 + function seq_map'0 [#"linked_list.rs" 55 0 55 66] (s : Seq.seq t_PtrOwn'0) (f : Map.map t_PtrOwn'0 t_T'0) : Seq.seq t_T'0 = - [%#slinked_list45] Seq.create (Seq.length s) (fun (i : int) -> Map.get f (Seq.get s i)) + [%#slinked_list47] Seq.create (Seq.length s) (fun (i : int) -> Map.get f (Seq.get s i)) function view'0 [#"linked_list.rs" 46 4 46 33] (self : t_List'0) : Seq.seq t_T'0 = - [%#slinked_list39] seq_map'0 (inner_logic'2 self.t_List__seq'0) (fun (ptr_own : t_PtrOwn'0) -> (val'0 ptr_own).t_Cell__v'0) + [%#slinked_list41] seq_map'0 (inner_logic'3 self.t_List__seq'0) (fun (ptr_own : t_PtrOwn'0) -> (val'0 ptr_own).t_Cell__v'0) meta "compute_max_steps" 1000000 - let rec push_back'0[#"linked_list.rs" 77 4 77 37] (self:MutBorrow.t t_List'0) (x:t_T'0) (return' (ret:()))= {[@expl:push_back 'self' type invariant] [%#slinked_list0] inv'7 self} - {[@expl:push_back 'x' type invariant] [%#slinked_list1] inv'8 x} + let rec push_back'0[#"linked_list.rs" 66 4 66 37] (self:MutBorrow.t t_List'0) (x:t_T'0) (return' (ret:()))= {[@expl:push_back 'self' type invariant] [%#slinked_list1] inv'7 self} + {[@expl:push_back 'x' type invariant] [%#slinked_list2] inv'8 x} (! bb0 [ bb0 = bb1 | bb1 = s0 [ s0 = null'0 (fun (_ret':Opaque.ptr) -> [ &_7 <- _ret' ] s1) | s1 = bb2 ] @@ -590,44 +618,48 @@ module M_linked_list__qyi10858349784728989480__push_back [#"linked_list.rs" 77 4 | bb8 = s0 [ s0 = [ &self <- { self with current = { self.current with t_List__first'0 = cell_ptr } } ] s1 | s1 = [ &self <- { self with current = { self.current with t_List__last'0 = cell_ptr } } ] s2 - | s2 = bb18 ] + | s2 = bb20 ] | bb9 = s0 [ s0 = deref'0 {(self.current).t_List__seq'0} (fun (_ret':Seq.seq t_PtrOwn'0) -> [ &_26 <- _ret' ] s1) | s1 = bb10 ] | bb10 = s0 [ s0 = len_ghost'0 {_26} (fun (_ret':int) -> [ &_24 <- _ret' ] s1) | s1 = bb11 ] - | bb11 = s0 [ s0 = minus_one'0 {_24} (fun (_ret':int) -> [ &off <- _ret' ] s1) | s1 = bb12 ] - | bb12 = s0 + | bb11 = s0 + [ s0 = new'0 {[%#slinked_list0] (1 : Int128.t)} (fun (_ret':t_GhostBox'1) -> [ &_29 <- _ret' ] s1) | s1 = bb12 ] + + | bb12 = s0 [ s0 = into_inner'0 {_29} (fun (_ret':int) -> [ &_28 <- _ret' ] s1) | s1 = bb13 ] + | bb13 = s0 [ s0 = sub'0 {_24} {_28} (fun (_ret':int) -> [ &off <- _ret' ] s1) | s1 = bb14 ] + | bb14 = s0 [ s0 = {inv'0 (self.current).t_List__seq'0} - MutBorrow.borrow_mut {(self.current).t_List__seq'0} - (fun (_ret':MutBorrow.t t_GhostBox'1) -> - [ &_32 <- _ret' ] + MutBorrow.borrow_mut {(self.current).t_List__seq'0} + (fun (_ret':MutBorrow.t t_GhostBox'2) -> + [ &_34 <- _ret' ] -{inv'0 _ret'.final}- [ &self <- { self with current = { self.current with t_List__seq'0 = _ret'.final } } ] s1) - | s1 = deref_mut'0 {_32} (fun (_ret':MutBorrow.t (Seq.seq t_PtrOwn'0)) -> [ &_31 <- _ret' ] s2) - | s2 = bb13 ] + | s1 = deref_mut'0 {_34} (fun (_ret':MutBorrow.t (Seq.seq t_PtrOwn'0)) -> [ &_33 <- _ret' ] s2) + | s2 = bb15 ] - | bb13 = s0 - [ s0 = {inv'1 _31.current} - MutBorrow.borrow_final {_31.current} {MutBorrow.get_id _31} + | bb15 = s0 + [ s0 = {inv'1 _33.current} + MutBorrow.borrow_final {_33.current} {MutBorrow.get_id _33} (fun (_ret':MutBorrow.t (Seq.seq t_PtrOwn'0)) -> - [ &_30 <- _ret' ] + [ &_32 <- _ret' ] -{inv'1 _ret'.final}- - [ &_31 <- { _31 with current = _ret'.final } ] + [ &_33 <- { _33 with current = _ret'.final } ] s1) - | s1 = get_mut_ghost'0 {_30} {off} (fun (_ret':t_Option'0) -> [ &_29 <- _ret' ] s2) - | s2 = bb14 ] + | s1 = get_mut_ghost'0 {_32} {off} (fun (_ret':t_Option'0) -> [ &_31 <- _ret' ] s2) + | s2 = bb16 ] - | bb14 = s0 [ s0 = unwrap'0 {_29} (fun (_ret':MutBorrow.t t_PtrOwn'0) -> [ &_28 <- _ret' ] s1) | s1 = bb15 ] - | bb15 = s0 - [ s0 = {inv'2 _28.current} - MutBorrow.borrow_final {_28.current} {MutBorrow.get_id _28} + | bb16 = s0 [ s0 = unwrap'0 {_31} (fun (_ret':MutBorrow.t t_PtrOwn'0) -> [ &_30 <- _ret' ] s1) | s1 = bb17 ] + | bb17 = s0 + [ s0 = {inv'2 _30.current} + MutBorrow.borrow_final {_30.current} {MutBorrow.get_id _30} (fun (_ret':MutBorrow.t t_PtrOwn'0) -> [ &_22 <- _ret' ] -{inv'2 _ret'.final}- - [ &_28 <- { _28 with current = _ret'.final } ] + [ &_30 <- { _30 with current = _ret'.final } ] s1) | s1 = {inv'2 _22.current} MutBorrow.borrow_final {_22.current} {MutBorrow.get_id _22} @@ -636,14 +668,14 @@ module M_linked_list__qyi10858349784728989480__push_back [#"linked_list.rs" 77 4 -{inv'2 _ret'.final}- [ &_22 <- { _22 with current = _ret'.final } ] s2) - | s2 = new'0 {_21} (fun (_ret':t_GhostBox'2) -> [ &_20 <- _ret' ] s3) - | s3 = bb16 ] + | s2 = new'1 {_21} (fun (_ret':t_GhostBox'3) -> [ &_20 <- _ret' ] s3) + | s3 = bb18 ] - | bb16 = s0 + | bb18 = s0 [ s0 = as_mut'0 {(self.current).t_List__last'0} {_20} (fun (_ret':MutBorrow.t t_Cell'0) -> [ &_18 <- _ret' ] s1) - | s1 = bb17 ] + | s1 = bb19 ] - | bb17 = s0 + | bb19 = s0 [ s0 = {inv'3 _18.current} MutBorrow.borrow_final {_18.current} {MutBorrow.get_id _18} (fun (_ret':MutBorrow.t t_Cell'0) -> @@ -651,10 +683,10 @@ module M_linked_list__qyi10858349784728989480__push_back [#"linked_list.rs" 77 4 -{inv'3 _ret'.final}- [ &_18 <- { _18 with current = _ret'.final } ] s1) - | s1 = {[@expl:type invariant] inv'4 _31} s2 - | s2 = -{resolve'0 _31}- s3 - | s3 = {[@expl:type invariant] inv'5 _28} s4 - | s4 = -{resolve'1 _28}- s5 + | s1 = {[@expl:type invariant] inv'4 _33} s2 + | s2 = -{resolve'0 _33}- s3 + | s3 = {[@expl:type invariant] inv'5 _30} s4 + | s4 = -{resolve'1 _30}- s5 | s5 = {[@expl:type invariant] inv'5 _22} s6 | s6 = -{resolve'1 _22}- s7 | s7 = {[@expl:type invariant] inv'6 _18} s8 @@ -663,47 +695,47 @@ module M_linked_list__qyi10858349784728989480__push_back [#"linked_list.rs" 77 4 | s10 = {[@expl:type invariant] inv'6 cell_last} s11 | s11 = -{resolve'2 cell_last}- s12 | s12 = [ &self <- { self with current = { self.current with t_List__last'0 = cell_ptr } } ] s13 - | s13 = bb18 ] + | s13 = bb20 ] - | bb18 = s0 + | bb20 = s0 [ s0 = {inv'0 (self.current).t_List__seq'0} MutBorrow.borrow_final - + {(self.current).t_List__seq'0} {MutBorrow.inherit_id (MutBorrow.get_id self) 3} - (fun (_ret':MutBorrow.t t_GhostBox'1) -> - [ &_40 <- _ret' ] + (fun (_ret':MutBorrow.t t_GhostBox'2) -> + [ &_42 <- _ret' ] -{inv'0 _ret'.final}- [ &self <- { self with current = { self.current with t_List__seq'0 = _ret'.final } } ] s1) - | s1 = deref_mut'0 {_40} (fun (_ret':MutBorrow.t (Seq.seq t_PtrOwn'0)) -> [ &_39 <- _ret' ] s2) - | s2 = bb19 ] + | s1 = deref_mut'0 {_42} (fun (_ret':MutBorrow.t (Seq.seq t_PtrOwn'0)) -> [ &_41 <- _ret' ] s2) + | s2 = bb21 ] - | bb19 = s0 - [ s0 = {inv'1 _39.current} - MutBorrow.borrow_final {_39.current} {MutBorrow.get_id _39} + | bb21 = s0 + [ s0 = {inv'1 _41.current} + MutBorrow.borrow_final {_41.current} {MutBorrow.get_id _41} (fun (_ret':MutBorrow.t (Seq.seq t_PtrOwn'0)) -> - [ &_38 <- _ret' ] + [ &_40 <- _ret' ] -{inv'1 _ret'.final}- - [ &_39 <- { _39 with current = _ret'.final } ] + [ &_41 <- { _41 with current = _ret'.final } ] s1) - | s1 = into_inner'0 {cell_own} (fun (_ret':t_PtrOwn'0) -> [ &_41 <- _ret' ] s2) - | s2 = bb20 ] + | s1 = into_inner'1 {cell_own} (fun (_ret':t_PtrOwn'0) -> [ &_43 <- _ret' ] s2) + | s2 = bb22 ] - | bb20 = s0 [ s0 = push_back_ghost'0 {_38} {_41} (fun (_ret':()) -> [ &_37 <- _ret' ] s1) | s1 = bb21 ] - | bb21 = s0 - [ s0 = {[@expl:type invariant] inv'4 _39} s1 - | s1 = -{resolve'0 _39}- s2 + | bb22 = s0 [ s0 = push_back_ghost'0 {_40} {_43} (fun (_ret':()) -> [ &_39 <- _ret' ] s1) | s1 = bb23 ] + | bb23 = s0 + [ s0 = {[@expl:type invariant] inv'4 _41} s1 + | s1 = -{resolve'0 _41}- s2 | s2 = {[@expl:type invariant] inv'7 self} s3 | s3 = -{resolve'3 self}- s4 - | s4 = new'1 {_37} (fun (_ret':t_GhostBox'3) -> [ &_36 <- _ret' ] s5) - | s5 = bb22 ] + | s4 = new'2 {_39} (fun (_ret':t_GhostBox'4) -> [ &_38 <- _ret' ] s5) + | s5 = bb24 ] - | bb22 = bb23 - | bb23 = bb24 | bb24 = bb25 | bb25 = bb26 - | bb26 = return' {_0} ] + | bb26 = bb27 + | bb27 = bb28 + | bb28 = return' {_0} ] ) [ & _0 : () = Any.any_l () | & self : MutBorrow.t t_List'0 = self @@ -717,33 +749,35 @@ module M_linked_list__qyi10858349784728989480__push_back [#"linked_list.rs" 77 4 | & _13 : bool = Any.any_l () | & cell_last : MutBorrow.t t_Cell'0 = Any.any_l () | & _18 : MutBorrow.t t_Cell'0 = Any.any_l () - | & _20 : t_GhostBox'2 = Any.any_l () + | & _20 : t_GhostBox'3 = Any.any_l () | & _21 : MutBorrow.t t_PtrOwn'0 = Any.any_l () | & _22 : MutBorrow.t t_PtrOwn'0 = Any.any_l () | & off : int = Any.any_l () | & _24 : int = Any.any_l () | & _26 : Seq.seq t_PtrOwn'0 = Any.any_l () - | & _28 : MutBorrow.t t_PtrOwn'0 = Any.any_l () - | & _29 : t_Option'0 = Any.any_l () - | & _30 : MutBorrow.t (Seq.seq t_PtrOwn'0) = Any.any_l () - | & _31 : MutBorrow.t (Seq.seq t_PtrOwn'0) = Any.any_l () - | & _32 : MutBorrow.t t_GhostBox'1 = Any.any_l () - | & _36 : t_GhostBox'3 = Any.any_l () - | & _37 : () = Any.any_l () - | & _38 : MutBorrow.t (Seq.seq t_PtrOwn'0) = Any.any_l () - | & _39 : MutBorrow.t (Seq.seq t_PtrOwn'0) = Any.any_l () - | & _40 : MutBorrow.t t_GhostBox'1 = Any.any_l () - | & _41 : t_PtrOwn'0 = Any.any_l () ] + | & _28 : int = Any.any_l () + | & _29 : t_GhostBox'1 = Any.any_l () + | & _30 : MutBorrow.t t_PtrOwn'0 = Any.any_l () + | & _31 : t_Option'0 = Any.any_l () + | & _32 : MutBorrow.t (Seq.seq t_PtrOwn'0) = Any.any_l () + | & _33 : MutBorrow.t (Seq.seq t_PtrOwn'0) = Any.any_l () + | & _34 : MutBorrow.t t_GhostBox'2 = Any.any_l () + | & _38 : t_GhostBox'4 = Any.any_l () + | & _39 : () = Any.any_l () + | & _40 : MutBorrow.t (Seq.seq t_PtrOwn'0) = Any.any_l () + | & _41 : MutBorrow.t (Seq.seq t_PtrOwn'0) = Any.any_l () + | & _42 : MutBorrow.t t_GhostBox'2 = Any.any_l () + | & _43 : t_PtrOwn'0 = Any.any_l () ] - [ return' (result:())-> {[@expl:push_back ensures] [%#slinked_list2] view'0 self.final + [ return' (result:())-> {[@expl:push_back ensures] [%#slinked_list3] view'0 self.final = Seq.snoc (view'0 self.current) x} (! return' {result}) ] end -module M_linked_list__qyi10858349784728989480__push_front [#"linked_list.rs" 97 4 97 38] (* List *) - let%span slinked_list0 = "linked_list.rs" 97 27 97 31 - let%span slinked_list1 = "linked_list.rs" 97 33 97 34 - let%span slinked_list2 = "linked_list.rs" 96 14 96 48 +module M_linked_list__qyi10858349784728989480__push_front [#"linked_list.rs" 86 4 86 38] (* List *) + let%span slinked_list0 = "linked_list.rs" 86 27 86 31 + let%span slinked_list1 = "linked_list.rs" 86 33 86 34 + let%span slinked_list2 = "linked_list.rs" 85 14 85 48 let%span sptr_own3 = "../../creusot-contracts/src/ptr_own.rs" 59 15 59 16 let%span sptr_own4 = "../../creusot-contracts/src/ptr_own.rs" 59 4 59 56 let%span sptr_own5 = "../../creusot-contracts/src/ptr_own.rs" 58 14 58 64 @@ -766,7 +800,7 @@ module M_linked_list__qyi10858349784728989480__push_front [#"linked_list.rs" 97 let%span sptr22 = "../../creusot-contracts/src/std/ptr.rs" 80 14 80 48 let%span sptr23 = "../../creusot-contracts/src/std/ptr.rs" 82 8 82 30 let%span sresolve24 = "../../creusot-contracts/src/resolve.rs" 54 20 54 34 - let%span slinked_list25 = "linked_list.rs" 67 4 67 41 + let%span slinked_list25 = "linked_list.rs" 56 4 56 41 let%span sseq26 = "../../creusot-contracts/src/logic/seq.rs" 629 20 629 95 let%span sinvariant27 = "../../creusot-contracts/src/invariant.rs" 35 20 35 44 let%span sptr_own28 = "../../creusot-contracts/src/ptr_own.rs" 51 8 51 35 @@ -987,7 +1021,7 @@ module M_linked_list__qyi10858349784728989480__push_front [#"linked_list.rs" 97 (! return' {result}) ] - function seq_map'0 [#"linked_list.rs" 66 0 66 66] (s : Seq.seq t_PtrOwn'0) (f : Map.map t_PtrOwn'0 t_T'0) : Seq.seq t_T'0 + function seq_map'0 [#"linked_list.rs" 55 0 55 66] (s : Seq.seq t_PtrOwn'0) (f : Map.map t_PtrOwn'0 t_T'0) : Seq.seq t_T'0 = [%#slinked_list25] Seq.create (Seq.length s) (fun (i : int) -> Map.get f (Seq.get s i)) @@ -1000,7 +1034,7 @@ module M_linked_list__qyi10858349784728989480__push_front [#"linked_list.rs" 97 meta "compute_max_steps" 1000000 - let rec push_front'0[#"linked_list.rs" 97 4 97 38] (self:MutBorrow.t t_List'0) (x:t_T'0) (return' (ret:()))= {[@expl:push_front 'self' type invariant] [%#slinked_list0] inv'3 self} + let rec push_front'0[#"linked_list.rs" 86 4 86 38] (self:MutBorrow.t t_List'0) (x:t_T'0) (return' (ret:()))= {[@expl:push_front 'self' type invariant] [%#slinked_list0] inv'3 self} {[@expl:push_front 'x' type invariant] [%#slinked_list1] inv'4 x} (! bb0 [ bb0 = bb1 diff --git a/tests/should_succeed/linked_list.rs b/tests/should_succeed/linked_list.rs index fe4f70eb0..554590e94 100644 --- a/tests/should_succeed/linked_list.rs +++ b/tests/should_succeed/linked_list.rs @@ -50,17 +50,6 @@ impl View for List { } } -// TODO: see issue #1251 -#[trusted] -#[pure] -#[ensures(result == x - 1)] -fn minus_one(x: Int) -> Int { - #[allow(unreachable_code)] - { - loop {} - } -} - #[logic] #[open(self)] pub fn seq_map(s: Seq, f: logic::Mapping) -> Seq { @@ -83,7 +72,7 @@ impl List { } else { let cell_last = unsafe { PtrOwn::as_mut(self.last, ghost! { - let off = minus_one(self.seq.len_ghost()); + let off = self.seq.len_ghost() - 1int; self.seq.get_mut_ghost(off).unwrap() }) }; diff --git a/tests/should_succeed/linked_list/proof.json b/tests/should_succeed/linked_list/proof.json index cfb743e1d..a6cedec0f 100644 --- a/tests/should_succeed/linked_list/proof.json +++ b/tests/should_succeed/linked_list/proof.json @@ -13,61 +13,64 @@ }, "M_linked_list__qyi10858349784728989480__push_back": { "vc_as_mut'0": { "prover": "cvc5@1.0.5", "time": 0.012 }, - "vc_deref'0": { "prover": "cvc5@1.0.5", "time": 0.013 }, + "vc_deref'0": { "prover": "cvc5@1.0.5", "time": 0.033 }, "vc_deref_mut'0": { "prover": "cvc5@1.0.5", "time": 0.011 }, "vc_from_box'0": { "prover": "cvc5@1.0.5", "time": 0.012 }, - "vc_get_mut_ghost'0": { "prover": "cvc5@1.0.5", "time": 0.012 }, - "vc_into_inner'0": { "prover": "cvc5@1.0.5", "time": 0.011 }, + "vc_get_mut_ghost'0": { "prover": "cvc5@1.0.5", "time": 0.032 }, + "vc_into_inner'0": { "prover": "cvc5@1.0.5", "time": 0.031 }, + "vc_into_inner'1": { "prover": "cvc5@1.0.5", "time": 0.026 }, "vc_is_null'0": { "prover": "cvc5@1.0.5", "time": 0.011 }, - "vc_len_ghost'0": { "prover": "cvc5@1.0.5", "time": 0.01 }, - "vc_minus_one'0": { "prover": "cvc5@1.0.5", "time": 0.012 }, - "vc_new'0": { "prover": "cvc5@1.0.5", "time": 0.013 }, + "vc_len_ghost'0": { "prover": "cvc5@1.0.5", "time": 0.033 }, + "vc_new'0": { "prover": "cvc5@1.0.5", "time": 0.026 }, "vc_new'1": { "prover": "cvc5@1.0.5", "time": 0.009 }, + "vc_new'2": { "prover": "cvc5@1.0.5", "time": 0.028 }, "vc_null'0": { "prover": "cvc5@1.0.5", "time": 0.011 }, "vc_push_back'0": { "tactic": "split_vc", "children": [ - { "prover": "cvc5@1.0.5", "time": 0.022 }, - { "prover": "cvc5@1.0.5", "time": 0.033 }, - { "prover": "cvc5@1.0.5", "time": 0.02 }, { "prover": "cvc5@1.0.5", "time": 0.031 }, - { "prover": "cvc5@1.0.5", "time": 0.035 }, + { "prover": "cvc5@1.0.5", "time": 0.049 }, + { "prover": "cvc5@1.0.5", "time": 0.029 }, + { "prover": "cvc5@1.0.5", "time": 0.026 }, + { "prover": "cvc5@1.0.5", "time": 0.048 }, + { "prover": "cvc5@1.0.5", "time": 0.047 }, + { "prover": "cvc5@1.0.5", "time": 0.028 }, + { "prover": "cvc5@1.0.5", "time": 0.063 }, + { "prover": "cvc5@1.0.5", "time": 0.04 }, + { "prover": "cvc5@1.0.5", "time": 0.046 }, + { "prover": "cvc5@1.0.5", "time": 0.049 }, + { "prover": "cvc5@1.0.5", "time": 0.023 }, + { "prover": "cvc5@1.0.5", "time": 0.057 }, { "prover": "cvc5@1.0.5", "time": 0.02 }, - { "prover": "cvc5@1.0.5", "time": 0.031 }, - { "prover": "cvc5@1.0.5", "time": 0.012 }, - { "prover": "cvc5@1.0.5", "time": 0.032 }, - { "prover": "cvc5@1.0.5", "time": 0.034 }, - { "prover": "cvc5@1.0.5", "time": 0.016 }, - { "prover": "cvc5@1.0.5", "time": 0.034 }, - { "prover": "cvc5@1.0.5", "time": 0.017 }, - { "prover": "cvc5@1.0.5", "time": 0.039 }, - { "prover": "cvc5@1.0.5", "time": 0.038 }, - { "prover": "cvc5@1.0.5", "time": 0.033 }, - { "prover": "cvc5@1.0.5", "time": 0.038 }, - { "prover": "cvc5@1.0.5", "time": 0.042 }, - { "prover": "z3@4.12.4", "time": 0.014 }, + { "prover": "cvc5@1.0.5", "time": 0.054 }, + { "prover": "cvc5@1.0.5", "time": 0.06 }, + { "prover": "cvc5@1.0.5", "time": 0.045 }, { "prover": "cvc5@1.0.5", "time": 0.046 }, - { "prover": "cvc5@1.0.5", "time": 0.077 }, - { "prover": "z3@4.12.4", "time": 0.03 }, - { "prover": "cvc5@1.0.5", "time": 0.078 }, - { "prover": "cvc5@1.0.5", "time": 0.04 }, - { "prover": "cvc5@1.0.5", "time": 0.052 }, - { "prover": "z3@4.12.4", "time": 0.01 }, - { "prover": "cvc5@1.0.5", "time": 0.064 }, + { "prover": "z3@4.12.4", "time": 0.018 }, + { "prover": "cvc5@1.0.5", "time": 0.062 }, + { "prover": "cvc5@1.0.5", "time": 0.066 }, + { "prover": "z3@4.12.4", "time": 0.026 }, + { "prover": "cvc5@1.0.5", "time": 0.07 }, + { "prover": "cvc5@1.0.5", "time": 0.099 }, + { "prover": "cvc5@1.0.5", "time": 0.055 }, { "prover": "z3@4.12.4", "time": 0.041 }, - { "prover": "cvc5@1.0.5", "time": 0.026 }, - { "prover": "z3@4.12.4", "time": 0.047 } + { "prover": "cvc5@1.0.5", "time": 0.033 }, + { "prover": "z3@4.12.4", "time": 0.023 }, + { "prover": "z3@4.12.4", "time": 0.038 }, + { "prover": "z3@4.12.4", "time": 0.025 }, + { "prover": "z3@4.12.4", "time": 0.066 } ] }, - "vc_push_back_ghost'0": { "prover": "cvc5@1.0.5", "time": 0.012 }, - "vc_unwrap'0": { "prover": "cvc5@1.0.5", "time": 0.012 } + "vc_push_back_ghost'0": { "prover": "cvc5@1.0.5", "time": 0.026 }, + "vc_sub'0": { "prover": "cvc5@1.0.5", "time": 0.031 }, + "vc_unwrap'0": { "prover": "cvc5@1.0.5", "time": 0.032 } }, "M_linked_list__qyi10858349784728989480__push_front": { "vc_deref_mut'0": { "prover": "cvc5@1.0.5", "time": 0.02 }, - "vc_into_inner'0": { "prover": "cvc5@1.0.5", "time": 0.011 }, + "vc_into_inner'0": { "prover": "cvc5@1.0.5", "time": 0.022 }, "vc_is_null'0": { "prover": "cvc5@1.0.5", "time": 0.009 }, "vc_new'0": { "prover": "cvc5@1.0.5", "time": 0.01 }, - "vc_new'1": { "prover": "cvc5@1.0.5", "time": 0.006 }, + "vc_new'1": { "prover": "cvc5@1.0.5", "time": 0.02 }, "vc_push_front'0": { "prover": "z3@4.12.4", "time": 0.033 }, "vc_push_front_ghost'0": { "prover": "cvc5@1.0.5", "time": 0.012 } },