diff --git a/creusot-contracts/src/logic/seq.rs b/creusot-contracts/src/logic/seq.rs index 966b6a395..2d683c161 100644 --- a/creusot-contracts/src/logic/seq.rs +++ b/creusot-contracts/src/logic/seq.rs @@ -548,7 +548,7 @@ impl Seq { None => self.get(index) == None && *self == ^self, Some(r) => self.get(index) == Some(*r) && ^r == (^self)[index], })] - #[ensures(forall i != index ==> (*self).get(index) == (^self).get(index))] + #[ensures(forall i != index ==> (*self).get(i) == (^self).get(i))] #[ensures((*self).len() == (^self).len())] pub fn get_mut_ghost(&mut self, index: Int) -> Option<&mut T> { let _ = index; diff --git a/tests/should_succeed/ghost/ghost_vec.coma b/tests/should_succeed/ghost/ghost_vec.coma index 295de6db5..91831dd13 100644 --- a/tests/should_succeed/ghost/ghost_vec.coma +++ b/tests/should_succeed/ghost/ghost_vec.coma @@ -53,7 +53,7 @@ module M_ghost_vec__ghost_vec [#"ghost_vec.rs" 4 0 4 18] let%span sseq51 = "../../../creusot-contracts/src/logic/seq.rs" 553 30 553 34 let%span sseq52 = "../../../creusot-contracts/src/logic/seq.rs" 553 4 553 65 let%span sseq53 = "../../../creusot-contracts/src/logic/seq.rs" 547 14 550 5 - let%span sseq54 = "../../../creusot-contracts/src/logic/seq.rs" 551 14 551 84 + let%span sseq54 = "../../../creusot-contracts/src/logic/seq.rs" 551 14 551 76 let%span sseq55 = "../../../creusot-contracts/src/logic/seq.rs" 552 14 552 44 let%span sseq56 = "../../../creusot-contracts/src/logic/seq.rs" 580 31 580 35 let%span sseq57 = "../../../creusot-contracts/src/logic/seq.rs" 580 4 580 49 @@ -219,7 +219,7 @@ module M_ghost_vec__ghost_vec [#"ghost_vec.rs" 4 0 4 18] | C_None'2 -> get'0 self.current index = C_None'0 /\ self.current = self.final | C_Some'1 r -> get'0 self.current index = C_Some'2 (r.current) /\ r.final = Seq.get self.final index end} - {[%#sseq54] forall i : int . i <> index -> get'0 self.current index = get'0 self.final index} + {[%#sseq54] forall i : int . i <> index -> get'0 self.current i = get'0 self.final i} {[%#sseq55] Seq.length self.current = Seq.length self.final} (! return' {result}) ] diff --git a/tests/should_succeed/ghost/ghost_vec/proof.json b/tests/should_succeed/ghost/ghost_vec/proof.json index 8acd6789e..094ba185e 100644 --- a/tests/should_succeed/ghost/ghost_vec/proof.json +++ b/tests/should_succeed/ghost/ghost_vec/proof.json @@ -9,14 +9,97 @@ "M_ghost_vec__ghost_vec": { "vc_deref'0": { "prover": "cvc5@1.0.5", "time": 0.03 }, "vc_deref_mut'0": { "prover": "cvc5@1.0.5", "time": 0.017 }, - "vc_get_ghost'0": { "prover": "cvc5@1.0.5", "time": 0.04 }, + "vc_get_ghost'0": { "prover": "cvc5@1.0.5", "time": 0.018 }, "vc_get_mut_ghost'0": { "prover": "cvc5@1.0.5", "time": 0.03 }, - "vc_ghost_vec'0": { "prover": "cvc5@1.0.5", "time": 0.273 }, + "vc_ghost_vec'0": { + "tactic": "split_vc", + "children": [ + { "prover": "cvc5@1.0.5", "time": 0.026 }, + { "prover": "cvc5@1.0.5", "time": 0.026 }, + { "prover": "cvc5@1.0.5", "time": 0.028 }, + { "prover": "cvc5@1.0.5", "time": 0.027 }, + { "prover": "cvc5@1.0.5", "time": 0.031 }, + { "prover": "cvc5@1.0.5", "time": 0.038 }, + { "prover": "cvc5@1.0.5", "time": 0.036 }, + { "prover": "cvc5@1.0.5", "time": 0.03 }, + { "prover": "cvc5@1.0.5", "time": 0.031 }, + { "prover": "cvc5@1.0.5", "time": 0.031 }, + { "prover": "cvc5@1.0.5", "time": 0.04 }, + { "prover": "cvc5@1.0.5", "time": 0.032 }, + { "prover": "cvc5@1.0.5", "time": 0.05 }, + { "prover": "cvc5@1.0.5", "time": 0.024 }, + { "prover": "cvc5@1.0.5", "time": 0.04 }, + { "prover": "cvc5@1.0.5", "time": 0.061 }, + { "prover": "cvc5@1.0.5", "time": 0.034 }, + { "prover": "cvc5@1.0.5", "time": 0.033 }, + { "prover": "cvc5@1.0.5", "time": 0.043 }, + { "prover": "cvc5@1.0.5", "time": 0.035 }, + { "prover": "cvc5@1.0.5", "time": 0.035 }, + { "prover": "cvc5@1.0.5", "time": 0.027 }, + { "prover": "cvc5@1.0.5", "time": 0.043 }, + { "prover": "cvc5@1.0.5", "time": 0.043 }, + { "prover": "cvc5@1.0.5", "time": 0.032 }, + { "prover": "cvc5@1.0.5", "time": 0.052 }, + { "prover": "cvc5@1.0.5", "time": 0.036 }, + { "prover": "cvc5@1.0.5", "time": 0.031 }, + { "prover": "cvc5@1.0.5", "time": 0.052 }, + { "prover": "cvc5@1.0.5", "time": 0.047 }, + { "prover": "cvc5@1.0.5", "time": 0.036 }, + { "prover": "cvc5@1.0.5", "time": 0.05 }, + { "prover": "cvc5@1.0.5", "time": 0.059 }, + { "prover": "cvc5@1.0.5", "time": 0.035 }, + { "prover": "cvc5@1.0.5", "time": 0.041 }, + { "prover": "cvc5@1.0.5", "time": 0.05 }, + { "prover": "cvc5@1.0.5", "time": 0.06 }, + { "prover": "cvc5@1.0.5", "time": 0.039 }, + { "prover": "cvc5@1.0.5", "time": 0.058 }, + { "prover": "cvc5@1.0.5", "time": 0.078 }, + { "prover": "cvc5@1.0.5", "time": 0.155 }, + { "prover": "cvc5@1.0.5", "time": 0.089 }, + { "prover": "cvc5@1.0.5", "time": 0.124 }, + { "prover": "cvc5@1.0.5", "time": 0.072 }, + { "prover": "cvc5@1.0.5", "time": 0.039 }, + { "prover": "cvc5@1.0.5", "time": 0.043 }, + { "prover": "cvc5@1.0.5", "time": 0.041 }, + { "prover": "cvc5@1.0.5", "time": 0.038 }, + { "prover": "cvc5@1.0.5", "time": 0.035 }, + { "prover": "cvc5@1.0.5", "time": 0.042 }, + { "prover": "cvc5@1.0.5", "time": 0.036 }, + { "prover": "cvc5@1.0.5", "time": 0.04 }, + { "prover": "cvc5@1.0.5", "time": 0.052 }, + { "prover": "cvc5@1.0.5", "time": 0.044 }, + { "prover": "cvc5@1.0.5", "time": 0.044 }, + { "prover": "cvc5@1.0.5", "time": 0.039 }, + { "prover": "cvc5@1.0.5", "time": 0.041 }, + { "prover": "cvc5@1.0.5", "time": 0.041 }, + { "prover": "cvc5@1.0.5", "time": 0.065 }, + { "prover": "cvc5@1.0.5", "time": 0.044 }, + { "prover": "cvc5@1.0.5", "time": 0.062 }, + { "prover": "cvc5@1.0.5", "time": 0.037 }, + { "prover": "cvc5@1.0.5", "time": 0.077 }, + { + "tactic": "split_vc", + "children": [ + { "prover": "cvc5@1.0.5", "time": 0.036 }, + { "prover": "alt-ergo@2.6.0", "time": 1.1 } + ] + }, + { + "tactic": "split_vc", + "children": [ + { "prover": "cvc5@1.0.5", "time": 0.037 }, + { "prover": "cvc5@1.0.5", "time": 0.854 } + ] + }, + { "prover": "cvc5@1.0.5", "time": 0.108 }, + { "prover": "cvc5@1.0.5", "time": 0.036 } + ] + }, "vc_into_inner'0": { "prover": "cvc5@1.0.5", "time": 0.018 }, "vc_len_ghost'0": { "prover": "cvc5@1.0.5", "time": 0.014 }, "vc_new'0": { "prover": "cvc5@1.0.5", "time": 0.012 }, "vc_new'1": { "prover": "cvc5@1.0.5", "time": 0.023 }, - "vc_new'2": { "prover": "cvc5@1.0.5", "time": 0.043 }, + "vc_new'2": { "prover": "cvc5@1.0.5", "time": 0.02 }, "vc_pop_back_ghost'0": { "prover": "cvc5@1.0.5", "time": 0.027 }, "vc_pop_front_ghost'0": { "prover": "cvc5@1.0.5", "time": 0.027 }, "vc_push_back_ghost'0": { "prover": "cvc5@1.0.5", "time": 0.014 }, diff --git a/tests/should_succeed/linked_list.coma b/tests/should_succeed/linked_list.coma index 3d5878427..56f6c8f63 100644 --- a/tests/should_succeed/linked_list.coma +++ b/tests/should_succeed/linked_list.coma @@ -189,63 +189,58 @@ module M_linked_list__qyi10858349784728989480__push_back [#"linked_list.rs" 77 4 let%span sptr_own6 = "../../creusot-contracts/src/ptr_own.rs" 61 4 61 68 let%span sptr_own7 = "../../creusot-contracts/src/ptr_own.rs" 60 14 60 67 let%span sptr8 = "../../creusot-contracts/src/std/ptr.rs" 107 18 107 48 - let%span sghost9 = "../../creusot-contracts/src/ghost.rs" 141 27 141 31 - let%span sghost10 = "../../creusot-contracts/src/ghost.rs" 141 4 141 52 - let%span sghost11 = "../../creusot-contracts/src/ghost.rs" 140 14 140 39 - let%span sghost12 = "../../creusot-contracts/src/ghost.rs" 85 22 85 26 - let%span sghost13 = "../../creusot-contracts/src/ghost.rs" 85 4 85 48 - let%span sghost14 = "../../creusot-contracts/src/ghost.rs" 84 14 84 36 - 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 sseq18 = "../../creusot-contracts/src/logic/seq.rs" 494 32 494 36 - let%span sseq19 = "../../creusot-contracts/src/logic/seq.rs" 494 38 494 39 - let%span sseq20 = "../../creusot-contracts/src/logic/seq.rs" 493 14 493 40 - let%span sghost21 = "../../creusot-contracts/src/ghost.rs" 185 15 185 16 - let%span sghost22 = "../../creusot-contracts/src/ghost.rs" 185 4 185 28 - let%span sghost23 = "../../creusot-contracts/src/ghost.rs" 183 14 183 28 - let%span sghost24 = "../../creusot-contracts/src/ghost.rs" 69 14 69 18 - let%span sghost25 = "../../creusot-contracts/src/ghost.rs" 69 4 69 36 - let%span sghost26 = "../../creusot-contracts/src/ghost.rs" 68 14 68 35 - let%span sseq27 = "../../creusot-contracts/src/logic/seq.rs" 451 22 451 26 - let%span sseq28 = "../../creusot-contracts/src/logic/seq.rs" 450 14 450 34 - let%span slinked_list29 = "linked_list.rs" 56 10 56 25 - let%span sseq30 = "../../creusot-contracts/src/logic/seq.rs" 553 30 553 34 - let%span sseq31 = "../../creusot-contracts/src/logic/seq.rs" 553 4 553 65 - let%span sseq32 = "../../creusot-contracts/src/logic/seq.rs" 547 14 550 5 - let%span sseq33 = "../../creusot-contracts/src/logic/seq.rs" 551 14 551 84 - let%span sseq34 = "../../creusot-contracts/src/logic/seq.rs" 552 14 552 44 - let%span soption35 = "../../creusot-contracts/src/std/option.rs" 31 0 423 1 - let%span sptr_own36 = "../../creusot-contracts/src/ptr_own.rs" 83 34 83 37 - let%span sptr_own37 = "../../creusot-contracts/src/ptr_own.rs" 78 15 78 31 - let%span sptr_own38 = "../../creusot-contracts/src/ptr_own.rs" 83 4 83 74 - let%span sptr_own39 = "../../creusot-contracts/src/ptr_own.rs" 79 14 79 35 - let%span sptr_own40 = "../../creusot-contracts/src/ptr_own.rs" 81 14 81 53 - let%span sptr_own41 = "../../creusot-contracts/src/ptr_own.rs" 82 14 82 52 - let%span slinked_list42 = "linked_list.rs" 48 12 48 74 - let%span sptr43 = "../../creusot-contracts/src/std/ptr.rs" 80 14 80 48 - let%span sptr44 = "../../creusot-contracts/src/std/ptr.rs" 82 8 82 30 - let%span sghost45 = "../../creusot-contracts/src/ghost.rs" 224 4 224 12 - let%span sresolve46 = "../../creusot-contracts/src/resolve.rs" 54 20 54 34 - let%span sghost47 = "../../creusot-contracts/src/ghost.rs" 108 4 108 27 - let%span sseq48 = "../../creusot-contracts/src/logic/seq.rs" 80 4 80 12 - let%span slinked_list49 = "linked_list.rs" 67 4 67 41 - let%span sseq50 = "../../creusot-contracts/src/logic/seq.rs" 629 20 629 95 - let%span sinvariant51 = "../../creusot-contracts/src/invariant.rs" 35 20 35 44 - let%span sresolve52 = "../../creusot-contracts/src/resolve.rs" 68 8 68 23 - let%span sptr_own53 = "../../creusot-contracts/src/ptr_own.rs" 44 20 44 66 - let%span sboxed54 = "../../creusot-contracts/src/std/boxed.rs" 33 8 33 18 - let%span sinvariant55 = "../../creusot-contracts/src/invariant.rs" 25 8 25 18 - let%span slinked_list56 = "linked_list.rs" 26 12 36 69 + 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 slinked_list14 = "linked_list.rs" 56 10 56 25 + let%span sghost15 = "../../creusot-contracts/src/ghost.rs" 85 22 85 26 + let%span sghost16 = "../../creusot-contracts/src/ghost.rs" 85 4 85 48 + let%span sghost17 = "../../creusot-contracts/src/ghost.rs" 84 14 84 36 + let%span sseq18 = "../../creusot-contracts/src/logic/seq.rs" 553 30 553 34 + let%span sseq19 = "../../creusot-contracts/src/logic/seq.rs" 553 4 553 65 + let%span sseq20 = "../../creusot-contracts/src/logic/seq.rs" 547 14 550 5 + let%span sseq21 = "../../creusot-contracts/src/logic/seq.rs" 551 14 551 76 + let%span sseq22 = "../../creusot-contracts/src/logic/seq.rs" 552 14 552 44 + let%span soption23 = "../../creusot-contracts/src/std/option.rs" 31 0 423 1 + 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" 83 34 83 37 + let%span sptr_own28 = "../../creusot-contracts/src/ptr_own.rs" 78 15 78 31 + let%span sptr_own29 = "../../creusot-contracts/src/ptr_own.rs" 83 4 83 74 + let%span sptr_own30 = "../../creusot-contracts/src/ptr_own.rs" 79 14 79 35 + let%span sptr_own31 = "../../creusot-contracts/src/ptr_own.rs" 81 14 81 53 + let%span sptr_own32 = "../../creusot-contracts/src/ptr_own.rs" 82 14 82 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" 80 4 80 12 + 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" 44 20 44 66 + 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 use creusot.prelude.Opaque function addr_logic'0 (self : Opaque.ptr) : int function is_null_logic'0 (self : Opaque.ptr) : bool = - [%#sptr44] addr_logic'0 self = 0 + [%#sptr41] addr_logic'0 self = 0 - axiom is_null_logic'0_spec : forall self : Opaque.ptr . [%#sptr43] is_null_logic'0 self = (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) let rec null'0 (_1:()) (return' (ret:Opaque.ptr))= any [ return' (result:Opaque.ptr)-> {[%#sptr4] is_null_logic'0 result} (! return' {result}) ] @@ -256,21 +251,21 @@ module M_linked_list__qyi10858349784728989480__push_back [#"linked_list.rs" 77 4 type t_Cell'0 = { t_Cell__v'0: t_T'0; t_Cell__next'0: Opaque.ptr } - predicate inv'10 (_1 : t_T'0) + predicate inv'7 (_1 : t_T'0) - predicate inv'27 (_1 : t_Cell'0) + predicate inv'21 (_1 : t_Cell'0) - axiom inv_axiom'26 [@rewrite] : forall x : t_Cell'0 [inv'27 x] . inv'27 x + axiom inv_axiom'20 [@rewrite] : forall x : t_Cell'0 [inv'21 x] . inv'21 x = match x with - | {t_Cell__v'0 = v ; t_Cell__next'0 = next} -> inv'10 v + | {t_Cell__v'0 = v ; t_Cell__next'0 = next} -> inv'7 v end - predicate invariant'7 (self : t_Cell'0) = - [%#sboxed54] inv'27 self + predicate invariant'6 (self : t_Cell'0) = + [%#sboxed49] inv'21 self - predicate inv'11 (_1 : t_Cell'0) + predicate inv'8 (_1 : t_Cell'0) - axiom inv_axiom'10 [@rewrite] : forall x : t_Cell'0 [inv'11 x] . inv'11 x = invariant'7 x + axiom inv_axiom'7 [@rewrite] : forall x : t_Cell'0 [inv'8 x] . inv'8 x = invariant'6 x type t_PtrOwn'0 @@ -281,38 +276,38 @@ module M_linked_list__qyi10858349784728989480__push_back [#"linked_list.rs" 77 4 function val'0 (self : t_PtrOwn'0) : t_Cell'0 - predicate invariant'3 (self : t_PtrOwn'0) = - [%#sptr_own53] not is_null_logic'0 (ptr'0 self) /\ inv'11 (val'0 self) + predicate invariant'1 (self : t_PtrOwn'0) = + [%#sptr_own47] not is_null_logic'0 (ptr'0 self) /\ inv'8 (val'0 self) - predicate inv'6 (_1 : t_PtrOwn'0) + predicate inv'2 (_1 : t_PtrOwn'0) - axiom inv_axiom'6 [@rewrite] : forall x : t_PtrOwn'0 [inv'6 x] . inv'6 x = invariant'3 x + axiom inv_axiom'2 [@rewrite] : forall x : t_PtrOwn'0 [inv'2 x] . inv'2 x = invariant'1 x - predicate invariant'15 (self : t_PtrOwn'0) = - [%#sboxed54] inv'6 self + predicate invariant'11 (self : t_PtrOwn'0) = + [%#sboxed49] inv'2 self - predicate inv'24 (_1 : t_PtrOwn'0) + predicate inv'19 (_1 : t_PtrOwn'0) - axiom inv_axiom'23 [@rewrite] : forall x : t_PtrOwn'0 [inv'24 x] . inv'24 x = invariant'15 x + axiom inv_axiom'18 [@rewrite] : forall x : t_PtrOwn'0 [inv'19 x] . inv'19 x = invariant'11 x - predicate inv'5 (_1 : t_GhostBox'0) + predicate inv'15 (_1 : t_GhostBox'0) - axiom inv_axiom'5 [@rewrite] : forall x : t_GhostBox'0 [inv'5 x] . inv'5 x + axiom inv_axiom'14 [@rewrite] : forall x : t_GhostBox'0 [inv'15 x] . inv'15 x = match x with - | {t_GhostBox__0'0 = a_0} -> inv'24 a_0 + | {t_GhostBox__0'0 = a_0} -> inv'19 a_0 end - predicate inv'12 (_1 : (Opaque.ptr, t_GhostBox'0)) + predicate inv'9 (_1 : (Opaque.ptr, t_GhostBox'0)) - axiom inv_axiom'11 [@rewrite] : forall x : (Opaque.ptr, t_GhostBox'0) [inv'12 x] . inv'12 x - = (let (x0, x1) = x in inv'5 x1) + axiom inv_axiom'8 [@rewrite] : forall x : (Opaque.ptr, t_GhostBox'0) [inv'9 x] . inv'9 x + = (let (x0, x1) = x in inv'15 x1) function inner_logic'0 (self : t_GhostBox'0) : t_PtrOwn'0 = - [%#sghost45] self.t_GhostBox__0'0 + [%#sghost42] self.t_GhostBox__0'0 - 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'11 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'8 val'} any - [ return' (result:(Opaque.ptr, t_GhostBox'0))-> {[%#sptr_own6] inv'12 result} + [ return' (result:(Opaque.ptr, t_GhostBox'0))-> {[%#sptr_own6] inv'9 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}) ] @@ -330,8 +325,6 @@ module M_linked_list__qyi10858349784728989480__push_back [#"linked_list.rs" 77 4 [ return' (result:bool)-> {[%#sptr8] result = is_null_logic'0 self} (! return' {result}) ] - use creusot.prelude.MutBorrow - use mach.int.Int use seq.Seq @@ -339,336 +332,257 @@ module M_linked_list__qyi10858349784728989480__push_back [#"linked_list.rs" 77 4 use seq.Seq predicate invariant'0 (self : Seq.seq t_PtrOwn'0) = - [%#sseq50] forall i : int . 0 <= i /\ i < Seq.length self -> inv'24 (Seq.get self i) + [%#sseq46] forall i : int . 0 <= i /\ i < Seq.length self -> inv'19 (Seq.get self i) - predicate inv'2 (_1 : Seq.seq t_PtrOwn'0) + predicate inv'1 (_1 : Seq.seq t_PtrOwn'0) - axiom inv_axiom'2 [@rewrite] : forall x : Seq.seq t_PtrOwn'0 [inv'2 x] . inv'2 x = invariant'0 x + axiom inv_axiom'1 [@rewrite] : forall x : Seq.seq t_PtrOwn'0 [inv'1 x] . inv'1 x = invariant'0 x - predicate invariant'13 (self : Seq.seq t_PtrOwn'0) = - [%#sboxed54] inv'2 self + predicate invariant'10 (self : Seq.seq t_PtrOwn'0) = + [%#sboxed49] inv'1 self - predicate inv'22 (_1 : Seq.seq t_PtrOwn'0) + predicate inv'18 (_1 : Seq.seq t_PtrOwn'0) - axiom inv_axiom'21 [@rewrite] : forall x : Seq.seq t_PtrOwn'0 [inv'22 x] . inv'22 x = invariant'13 x + axiom inv_axiom'17 [@rewrite] : forall x : Seq.seq t_PtrOwn'0 [inv'18 x] . inv'18 x = invariant'10 x predicate inv'0 (_1 : t_GhostBox'1) axiom inv_axiom'0 [@rewrite] : forall x : t_GhostBox'1 [inv'0 x] . inv'0 x = match x with - | {t_GhostBox__0'1 = a_0} -> inv'22 a_0 + | {t_GhostBox__0'1 = a_0} -> inv'18 a_0 end - predicate invariant'8 (self : MutBorrow.t t_GhostBox'1) = - [%#sinvariant51] inv'0 self.current /\ inv'0 self.final - - predicate inv'13 (_1 : MutBorrow.t t_GhostBox'1) - - axiom inv_axiom'12 [@rewrite] : forall x : MutBorrow.t t_GhostBox'1 [inv'13 x] . inv'13 x = invariant'8 x - - type t_GhostBox'2 = - { t_GhostBox__0'2: MutBorrow.t (Seq.seq t_PtrOwn'0) } - - predicate invariant'4 (self : MutBorrow.t (Seq.seq t_PtrOwn'0)) = - [%#sinvariant51] inv'2 self.current /\ inv'2 self.final + predicate invariant'7 (self : t_GhostBox'1) = + [%#sinvariant50] inv'0 self - predicate inv'7 (_1 : MutBorrow.t (Seq.seq t_PtrOwn'0)) + predicate inv'10 (_1 : t_GhostBox'1) - axiom inv_axiom'7 [@rewrite] : forall x : MutBorrow.t (Seq.seq t_PtrOwn'0) [inv'7 x] . inv'7 x = invariant'4 x + axiom inv_axiom'9 [@rewrite] : forall x : t_GhostBox'1 [inv'10 x] . inv'10 x = invariant'7 x - predicate invariant'14 (self : MutBorrow.t (Seq.seq t_PtrOwn'0)) = - [%#sboxed54] inv'7 self + predicate invariant'8 (self : Seq.seq t_PtrOwn'0) = + [%#sinvariant50] inv'1 self - predicate inv'23 (_1 : MutBorrow.t (Seq.seq t_PtrOwn'0)) + predicate inv'11 (_1 : Seq.seq t_PtrOwn'0) - axiom inv_axiom'22 [@rewrite] : forall x : MutBorrow.t (Seq.seq t_PtrOwn'0) [inv'23 x] . inv'23 x = invariant'14 x + axiom inv_axiom'10 [@rewrite] : forall x : Seq.seq t_PtrOwn'0 [inv'11 x] . inv'11 x = invariant'8 x - predicate inv'1 (_1 : t_GhostBox'2) - - axiom inv_axiom'1 [@rewrite] : forall x : t_GhostBox'2 [inv'1 x] . inv'1 x - = match x with - | {t_GhostBox__0'2 = a_0} -> inv'23 a_0 - end - - let rec borrow_mut'0 (self:MutBorrow.t t_GhostBox'1) (return' (ret:t_GhostBox'2))= {[@expl:borrow_mut 'self' type invariant] [%#sghost9] inv'13 self} + let rec deref'0 (self:t_GhostBox'1) (return' (ret:Seq.seq t_PtrOwn'0))= {[@expl:deref 'self' type invariant] [%#sghost9] inv'10 self} any - [ return' (result:t_GhostBox'2)-> {[%#sghost10] inv'1 result} - {[%#sghost11] result.t_GhostBox__0'2 - = 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:Seq.seq t_PtrOwn'0)-> {[%#sghost10] inv'11 result} + {[%#sghost11] self.t_GhostBox__0'1 = result} (! return' {result}) ] - predicate invariant'9 (self : MutBorrow.t t_GhostBox'2) = - [%#sinvariant51] inv'1 self.current /\ inv'1 self.final + let rec len_ghost'0 (self:Seq.seq t_PtrOwn'0) (return' (ret:int))= {[@expl:len_ghost 'self' type invariant] [%#sseq12] inv'11 self} + any [ return' (result:int)-> {[%#sseq13] result = Seq.length self} (! return' {result}) ] - predicate inv'14 (_1 : MutBorrow.t t_GhostBox'2) + let rec minus_one'0 (x:int) (return' (ret:int))= any + [ return' (result:int)-> {[%#slinked_list14] result = x - 1} (! return' {result}) ] - axiom inv_axiom'13 [@rewrite] : forall x : MutBorrow.t t_GhostBox'2 [inv'14 x] . inv'14 x = invariant'9 x - predicate invariant'1 (self : MutBorrow.t (MutBorrow.t (Seq.seq t_PtrOwn'0))) = - [%#sinvariant51] inv'7 self.current /\ inv'7 self.final + use creusot.prelude.MutBorrow - predicate inv'3 (_1 : MutBorrow.t (MutBorrow.t (Seq.seq t_PtrOwn'0))) + predicate invariant'9 (self : MutBorrow.t t_GhostBox'1) = + [%#sinvariant48] inv'0 self.current /\ inv'0 self.final - axiom inv_axiom'3 [@rewrite] : forall x : MutBorrow.t (MutBorrow.t (Seq.seq t_PtrOwn'0)) [inv'3 x] . inv'3 x - = invariant'1 x + predicate inv'12 (_1 : MutBorrow.t t_GhostBox'1) - let rec deref_mut'0 (self:MutBorrow.t t_GhostBox'2) (return' (ret:MutBorrow.t (MutBorrow.t (Seq.seq t_PtrOwn'0))))= {[@expl:deref_mut 'self' type invariant] [%#sghost12] inv'14 self} - any - [ return' (result:MutBorrow.t (MutBorrow.t (Seq.seq t_PtrOwn'0)))-> {[%#sghost13] inv'3 result} - {[%#sghost14] result - = MutBorrow.borrow_logic (self.current).t_GhostBox__0'2 (self.final).t_GhostBox__0'2 (MutBorrow.inherit_id (MutBorrow.get_id self) 1)} - (! return' {result}) ] - - - let rec into_inner'0 (self:t_GhostBox'0) (return' (ret:t_PtrOwn'0))= {[@expl:into_inner 'self' type invariant] [%#sghost15] inv'5 self} - any - [ return' (result:t_PtrOwn'0)-> {[%#sghost16] inv'6 result} - {[%#sghost17] result = self.t_GhostBox__0'0} - (! return' {result}) ] + axiom inv_axiom'11 [@rewrite] : forall x : MutBorrow.t t_GhostBox'1 [inv'12 x] . inv'12 x = invariant'9 x + predicate invariant'2 (self : MutBorrow.t (Seq.seq t_PtrOwn'0)) = + [%#sinvariant48] inv'1 self.current /\ inv'1 self.final - use seq.Seq + predicate inv'3 (_1 : MutBorrow.t (Seq.seq t_PtrOwn'0)) - 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] [%#sseq18] inv'7 self} - {[@expl:push_back_ghost 'x' type invariant] [%#sseq19] inv'6 x} - any [ return' (result:())-> {[%#sseq20] self.final = Seq.snoc self.current x} (! return' {result}) ] + axiom inv_axiom'3 [@rewrite] : forall x : MutBorrow.t (Seq.seq t_PtrOwn'0) [inv'3 x] . inv'3 x = invariant'2 x - predicate resolve'7 (self : MutBorrow.t (MutBorrow.t (Seq.seq t_PtrOwn'0))) = - [%#sresolve46] self.final = self.current + 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] [%#sghost15] inv'12 self} + any + [ return' (result:MutBorrow.t (Seq.seq t_PtrOwn'0))-> {[%#sghost16] inv'3 result} + {[%#sghost17] 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}) ] - predicate resolve'0 (_1 : MutBorrow.t (MutBorrow.t (Seq.seq t_PtrOwn'0))) = - resolve'7 _1 - predicate resolve'11 (self : MutBorrow.t (Seq.seq t_PtrOwn'0)) = - [%#sresolve46] self.final = self.current + type t_Option'0 = + | C_None'0 + | C_Some'0 (MutBorrow.t t_PtrOwn'0) - predicate resolve'4 (_1 : MutBorrow.t (Seq.seq t_PtrOwn'0)) = - resolve'11 _1 + predicate invariant'3 (self : MutBorrow.t t_PtrOwn'0) = + [%#sinvariant48] inv'2 self.current /\ inv'2 self.final - predicate resolve'14 (self : MutBorrow.t (Seq.seq t_PtrOwn'0)) = - [%#sresolve52] resolve'4 self + predicate inv'4 (_1 : MutBorrow.t t_PtrOwn'0) - predicate resolve'8 (self : t_GhostBox'2) = - [%#sghost47] resolve'14 self.t_GhostBox__0'2 + axiom inv_axiom'4 [@rewrite] : forall x : MutBorrow.t t_PtrOwn'0 [inv'4 x] . inv'4 x = invariant'3 x - predicate resolve'1 (_1 : t_GhostBox'2) = - resolve'8 _1 + predicate inv'13 (_1 : t_Option'0) - function inner_logic'2 (self : t_GhostBox'1) : Seq.seq t_PtrOwn'0 = - [%#sghost45] self.t_GhostBox__0'1 + axiom inv_axiom'12 [@rewrite] : forall x : t_Option'0 [inv'13 x] . inv'13 x + = match x with + | C_None'0 -> true + | C_Some'0 a_0 -> inv'4 a_0 + end - use seq.Seq + type t_Option'1 = + | C_None'1 + | C_Some'1 t_PtrOwn'0 use seq.Seq - predicate invariant'16 [#"linked_list.rs" 24 4 24 30] (self : t_List'0) = - [%#slinked_list56] inner_logic'2 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) - /\ 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) - - 1))).t_Cell__next'0 - - predicate inv'25 (_1 : t_List'0) - - axiom inv_axiom'24 [@rewrite] : forall x : t_List'0 [inv'25 x] . inv'25 x - = (invariant'16 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'2 (self : MutBorrow.t t_List'0) = - [%#sinvariant51] inv'25 self.current /\ inv'25 self.final - - predicate inv'4 (_1 : MutBorrow.t t_List'0) - - axiom inv_axiom'4 [@rewrite] : forall x : MutBorrow.t t_List'0 [inv'4 x] . inv'4 x = invariant'2 x - - predicate resolve'9 (self : MutBorrow.t t_List'0) = - [%#sresolve46] self.final = self.current - - predicate resolve'2 (_1 : MutBorrow.t t_List'0) = - resolve'9 _1 - - predicate inv'15 (_1 : ()) - - axiom inv_axiom'14 [@rewrite] : forall x : () [inv'15 x] . inv'15 x = true - - type t_GhostBox'3 = - { t_GhostBox__0'3: () } - - predicate inv'16 (_1 : t_GhostBox'3) - - axiom inv_axiom'15 [@rewrite] : forall x : t_GhostBox'3 [inv'16 x] . inv'16 x = true + 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 - let rec new'0 (x:()) (return' (ret:t_GhostBox'3))= {[@expl:new 'x' type invariant] [%#sghost21] inv'15 x} + 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] [%#sseq18] inv'3 self} any - [ return' (result:t_GhostBox'3)-> {[%#sghost22] inv'16 result} - {[%#sghost23] result.t_GhostBox__0'3 = x} + [ return' (result:t_Option'0)-> {[%#sseq19] inv'13 result} + {[%#sseq20] 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} + {[%#sseq21] forall i : int . i <> index -> get'0 self.current i = get'0 self.final i} + {[%#sseq22] Seq.length self.current = Seq.length self.final} (! return' {result}) ] - predicate resolve'16 (_1 : t_PtrOwn'0) = - true - - predicate resolve'15 (self : t_PtrOwn'0) = - [%#sresolve52] resolve'16 self - - predicate resolve'10 (self : t_GhostBox'0) = - [%#sghost47] resolve'15 self.t_GhostBox__0'0 + let rec unwrap'0 (self:t_Option'0) (return' (ret:MutBorrow.t t_PtrOwn'0))= {[@expl:unwrap 'self' type invariant] inv'13 self} + {[@expl:unwrap requires] [%#soption23] self <> C_None'0} + any + [ return' (result:MutBorrow.t t_PtrOwn'0)-> {inv'4 result} + {[%#soption23] C_Some'0 result = self} + (! return' {result}) ] - predicate resolve'3 (_1 : t_GhostBox'0) = - resolve'10 _1 - predicate invariant'10 (self : t_GhostBox'2) = - [%#sinvariant55] inv'1 self + type t_GhostBox'2 = + { t_GhostBox__0'2: MutBorrow.t t_PtrOwn'0 } - predicate inv'17 (_1 : t_GhostBox'2) + predicate invariant'12 (self : MutBorrow.t t_PtrOwn'0) = + [%#sboxed49] inv'4 self - axiom inv_axiom'16 [@rewrite] : forall x : t_GhostBox'2 [inv'17 x] . inv'17 x = invariant'10 x + predicate inv'20 (_1 : MutBorrow.t t_PtrOwn'0) - predicate invariant'11 (self : MutBorrow.t (Seq.seq t_PtrOwn'0)) = - [%#sinvariant55] inv'7 self + axiom inv_axiom'19 [@rewrite] : forall x : MutBorrow.t t_PtrOwn'0 [inv'20 x] . inv'20 x = invariant'12 x - predicate inv'18 (_1 : MutBorrow.t (Seq.seq t_PtrOwn'0)) + predicate inv'14 (_1 : t_GhostBox'2) - axiom inv_axiom'17 [@rewrite] : forall x : MutBorrow.t (Seq.seq t_PtrOwn'0) [inv'18 x] . inv'18 x = invariant'11 x + axiom inv_axiom'13 [@rewrite] : forall x : t_GhostBox'2 [inv'14 x] . inv'14 x + = match x with + | {t_GhostBox__0'2 = a_0} -> inv'20 a_0 + end - let rec deref'0 (self:t_GhostBox'2) (return' (ret:MutBorrow.t (Seq.seq t_PtrOwn'0)))= {[@expl:deref 'self' type invariant] [%#sghost24] inv'17 self} + let rec new'0 (x:MutBorrow.t t_PtrOwn'0) (return' (ret:t_GhostBox'2))= {[@expl:new 'x' type invariant] [%#sghost24] inv'4 x} any - [ return' (result:MutBorrow.t (Seq.seq t_PtrOwn'0))-> {[%#sghost25] inv'18 result} - {[%#sghost26] self.t_GhostBox__0'2 = result} + [ return' (result:t_GhostBox'2)-> {[%#sghost25] inv'14 result} + {[%#sghost26] result.t_GhostBox__0'2 = x} (! return' {result}) ] - predicate invariant'12 (self : Seq.seq t_PtrOwn'0) = - [%#sinvariant55] inv'2 self + function inner_logic'1 (self : t_GhostBox'2) : MutBorrow.t t_PtrOwn'0 = + [%#sghost42] self.t_GhostBox__0'2 - predicate inv'19 (_1 : Seq.seq t_PtrOwn'0) + predicate invariant'4 (self : MutBorrow.t t_Cell'0) = + [%#sinvariant48] inv'21 self.current /\ inv'21 self.final - axiom inv_axiom'18 [@rewrite] : forall x : Seq.seq t_PtrOwn'0 [inv'19 x] . inv'19 x = invariant'12 x + predicate inv'5 (_1 : MutBorrow.t t_Cell'0) - let rec len_ghost'0 (self:Seq.seq t_PtrOwn'0) (return' (ret:int))= {[@expl:len_ghost 'self' type invariant] [%#sseq27] inv'19 self} - any [ return' (result:int)-> {[%#sseq28] result = Seq.length self} (! return' {result}) ] + axiom inv_axiom'5 [@rewrite] : forall x : MutBorrow.t t_Cell'0 [inv'5 x] . inv'5 x = invariant'4 x - let rec minus_one'0 (x:int) (return' (ret:int))= any - [ return' (result:int)-> {[%#slinked_list29] result = x - 1} (! return' {result}) ] - - - let rec into_inner'1 (self:t_GhostBox'2) (return' (ret:MutBorrow.t (Seq.seq t_PtrOwn'0)))= {[@expl:into_inner 'self' type invariant] [%#sghost15] inv'1 self} + 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'14 own} + {[@expl:as_mut requires] [%#sptr_own28] ptr = ptr'0 (inner_logic'1 own).current} any - [ return' (result:MutBorrow.t (Seq.seq t_PtrOwn'0))-> {[%#sghost16] inv'7 result} - {[%#sghost17] result = self.t_GhostBox__0'2} + [ return' (result:MutBorrow.t t_Cell'0)-> {[%#sptr_own29] inv'5 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}) ] - type t_Option'0 = - | C_None'0 - | C_Some'0 (MutBorrow.t t_PtrOwn'0) - - predicate invariant'5 (self : MutBorrow.t t_PtrOwn'0) = - [%#sinvariant51] inv'6 self.current /\ inv'6 self.final - - predicate inv'8 (_1 : MutBorrow.t t_PtrOwn'0) + predicate resolve'4 (self : MutBorrow.t (Seq.seq t_PtrOwn'0)) = + [%#sresolve44] self.final = self.current - axiom inv_axiom'8 [@rewrite] : forall x : MutBorrow.t t_PtrOwn'0 [inv'8 x] . inv'8 x = invariant'5 x + predicate resolve'0 (_1 : MutBorrow.t (Seq.seq t_PtrOwn'0)) = + resolve'4 _1 - predicate inv'20 (_1 : t_Option'0) + predicate resolve'5 (self : MutBorrow.t t_PtrOwn'0) = + [%#sresolve44] self.final = self.current - axiom inv_axiom'19 [@rewrite] : forall x : t_Option'0 [inv'20 x] . inv'20 x - = match x with - | C_None'0 -> true - | C_Some'0 a_0 -> inv'8 a_0 - end + predicate resolve'1 (_1 : MutBorrow.t t_PtrOwn'0) = + resolve'5 _1 - type t_Option'1 = - | C_None'1 - | C_Some'1 t_PtrOwn'0 + predicate resolve'6 (self : MutBorrow.t t_Cell'0) = + [%#sresolve44] self.final = self.current - function get'0 (self : Seq.seq t_PtrOwn'0) (ix : int) : t_Option'1 = - [%#sseq48] if 0 <= ix /\ ix < Seq.length self then C_Some'1 (Seq.get self ix) else C_None'1 + predicate resolve'2 (_1 : MutBorrow.t t_Cell'0) = + resolve'6 _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] [%#sseq30] inv'7 self} + let rec into_inner'0 (self:t_GhostBox'0) (return' (ret:t_PtrOwn'0))= {[@expl:into_inner 'self' type invariant] [%#sghost33] inv'15 self} any - [ return' (result:t_Option'0)-> {[%#sseq31] inv'20 result} - {[%#sseq32] 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} - {[%#sseq33] forall i : int . i <> index -> get'0 self.current index = get'0 self.final index} - {[%#sseq34] Seq.length self.current = Seq.length self.final} + [ return' (result:t_PtrOwn'0)-> {[%#sghost34] inv'2 result} + {[%#sghost35] result = self.t_GhostBox__0'0} (! return' {result}) ] - let rec unwrap'0 (self:t_Option'0) (return' (ret:MutBorrow.t t_PtrOwn'0))= {[@expl:unwrap 'self' type invariant] inv'20 self} - {[@expl:unwrap requires] [%#soption35] self <> C_None'0} - any - [ return' (result:MutBorrow.t t_PtrOwn'0)-> {inv'8 result} - {[%#soption35] C_Some'0 result = self} - (! return' {result}) ] - + use seq.Seq - type t_GhostBox'4 = - { t_GhostBox__0'4: MutBorrow.t t_PtrOwn'0 } + 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'3 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}) ] - predicate invariant'17 (self : MutBorrow.t t_PtrOwn'0) = - [%#sboxed54] inv'8 self + function inner_logic'2 (self : t_GhostBox'1) : Seq.seq t_PtrOwn'0 = + [%#sghost42] self.t_GhostBox__0'1 - predicate inv'26 (_1 : MutBorrow.t t_PtrOwn'0) + use seq.Seq - axiom inv_axiom'25 [@rewrite] : forall x : MutBorrow.t t_PtrOwn'0 [inv'26 x] . inv'26 x = invariant'17 x + 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) + /\ 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) + /\ 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) + - 1))).t_Cell__next'0 - predicate inv'21 (_1 : t_GhostBox'4) + predicate inv'22 (_1 : t_List'0) - axiom inv_axiom'20 [@rewrite] : forall x : t_GhostBox'4 [inv'21 x] . inv'21 x - = match x with - | {t_GhostBox__0'4 = a_0} -> inv'26 a_0 - end + axiom inv_axiom'21 [@rewrite] : forall x : t_List'0 [inv'22 x] . inv'22 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) - let rec new'1 (x:MutBorrow.t t_PtrOwn'0) (return' (ret:t_GhostBox'4))= {[@expl:new 'x' type invariant] [%#sghost21] inv'8 x} - any - [ return' (result:t_GhostBox'4)-> {[%#sghost22] inv'21 result} - {[%#sghost23] result.t_GhostBox__0'4 = x} - (! return' {result}) ] + predicate invariant'5 (self : MutBorrow.t t_List'0) = + [%#sinvariant48] inv'22 self.current /\ inv'22 self.final + predicate inv'6 (_1 : MutBorrow.t t_List'0) - function inner_logic'1 (self : t_GhostBox'4) : MutBorrow.t t_PtrOwn'0 = - [%#sghost45] self.t_GhostBox__0'4 + axiom inv_axiom'6 [@rewrite] : forall x : MutBorrow.t t_List'0 [inv'6 x] . inv'6 x = invariant'5 x - predicate invariant'6 (self : MutBorrow.t t_Cell'0) = - [%#sinvariant51] inv'27 self.current /\ inv'27 self.final + predicate resolve'7 (self : MutBorrow.t t_List'0) = + [%#sresolve44] self.final = self.current - predicate inv'9 (_1 : MutBorrow.t t_Cell'0) + predicate resolve'3 (_1 : MutBorrow.t t_List'0) = + resolve'7 _1 - axiom inv_axiom'9 [@rewrite] : forall x : MutBorrow.t t_Cell'0 [inv'9 x] . inv'9 x = invariant'6 x + predicate inv'16 (_1 : ()) - let rec as_mut'0 (ptr:Opaque.ptr) (own:t_GhostBox'4) (return' (ret:MutBorrow.t t_Cell'0))= {[@expl:as_mut 'own' type invariant] [%#sptr_own36] inv'21 own} - {[@expl:as_mut requires] [%#sptr_own37] ptr = ptr'0 (inner_logic'1 own).current} - any - [ return' (result:MutBorrow.t t_Cell'0)-> {[%#sptr_own38] inv'9 result} - {[%#sptr_own39] result.current = val'0 (inner_logic'1 own).current} - {[%#sptr_own40] ptr'0 (inner_logic'1 own).final = ptr'0 (inner_logic'1 own).current} - {[%#sptr_own41] val'0 (inner_logic'1 own).final = result.final} - (! return' {result}) ] + axiom inv_axiom'15 [@rewrite] : forall x : () [inv'16 x] . inv'16 x = true + type t_GhostBox'3 = + { t_GhostBox__0'3: () } - predicate resolve'12 (self : MutBorrow.t t_PtrOwn'0) = - [%#sresolve46] self.final = self.current + predicate inv'17 (_1 : t_GhostBox'3) - predicate resolve'5 (_1 : MutBorrow.t t_PtrOwn'0) = - resolve'12 _1 + axiom inv_axiom'16 [@rewrite] : forall x : t_GhostBox'3 [inv'17 x] . inv'17 x = true - predicate resolve'13 (self : MutBorrow.t t_Cell'0) = - [%#sresolve46] self.final = self.current + let rec new'1 (x:()) (return' (ret:t_GhostBox'3))= {[@expl:new 'x' type invariant] [%#sghost24] inv'16 x} + any + [ return' (result:t_GhostBox'3)-> {[%#sghost25] inv'17 result} + {[%#sghost26] result.t_GhostBox__0'3 = x} + (! return' {result}) ] - predicate resolve'6 (_1 : MutBorrow.t t_Cell'0) = - resolve'13 _1 use creusot.prelude.Any @@ -683,17 +597,17 @@ module M_linked_list__qyi10858349784728989480__push_back [#"linked_list.rs" 77 4 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 = - [%#slinked_list49] Seq.create (Seq.length s) (fun (i : int) -> Map.get f (Seq.get s i)) + [%#slinked_list45] 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_list42] 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_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) use seq.Seq 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_list1] inv'4 self} - {[@expl:push_back 'x' type invariant] [%#slinked_list2] inv'10 x} + 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_list1] inv'6 self} + {[@expl:push_back 'x' type invariant] [%#slinked_list2] inv'7 x} (! bb0 [ bb0 = bb1 | bb1 = s0 [ s0 = null'0 {[%#slinked_list0] ()} (fun (_ret':Opaque.ptr) -> [ &_7 <- _ret' ] s1) | s1 = bb2 ] @@ -706,136 +620,118 @@ module M_linked_list__qyi10858349784728989480__push_back [#"linked_list.rs" 77 4 | s2 = bb6 ] | bb6 = s0 - [ s0 = is_null'0 {(self.current).t_List__last'0} (fun (_ret':bool) -> [ &_12 <- _ret' ] s1) | s1 = bb7 ] + [ s0 = is_null'0 {(self.current).t_List__last'0} (fun (_ret':bool) -> [ &_13 <- _ret' ] s1) | s1 = bb7 ] - | bb7 = any [ br0 -> {_12 = false} (! bb16) | br1 -> {_12} (! bb8) ] + | bb7 = any [ br0 -> {_13 = false} (! bb9) | br1 -> {_13} (! bb8) ] | 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 = {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) -> - [ &_17 <- _ret' ] - -{inv'0 _ret'.final}- - [ &self <- { self with current = { self.current with t_List__seq'0 = _ret'.final } } ] - s3) - | s3 = borrow_mut'0 {_17} (fun (_ret':t_GhostBox'2) -> [ &seq <- _ret' ] s4) - | s4 = bb9 ] + | s2 = bb18 ] | bb9 = s0 - [ s0 = {inv'1 seq} - MutBorrow.borrow_mut {seq} - (fun (_ret':MutBorrow.t t_GhostBox'2) -> [ &_22 <- _ret' ] -{inv'1 _ret'.final}- [ &seq <- _ret'.final ] s1) - | s1 = deref_mut'0 {_22} (fun (_ret':MutBorrow.t (MutBorrow.t (Seq.seq t_PtrOwn'0))) -> [ &_21 <- _ret' ] s2) - | s2 = bb10 ] - - | bb10 = s0 - [ s0 = {inv'2 (_21.current).current} - MutBorrow.borrow_mut {(_21.current).current} - (fun (_ret':MutBorrow.t (Seq.seq t_PtrOwn'0)) -> - [ &_20 <- _ret' ] - -{inv'2 _ret'.final}- - [ &_21 <- { _21 with current = { _21.current with current = _ret'.final } } ] - s1) - | s1 = into_inner'0 {cell_own} (fun (_ret':t_PtrOwn'0) -> [ &_23 <- _ret' ] s2) - | s2 = bb11 ] + [ s0 = deref'0 {(self.current).t_List__seq'0} (fun (_ret':Seq.seq t_PtrOwn'0) -> [ &_25 <- _ret' ] s1) + | s1 = bb10 ] - | bb11 = s0 [ s0 = push_back_ghost'0 {_20} {_23} (fun (_ret':()) -> [ &_19 <- _ret' ] s1) | s1 = bb12 ] + | bb10 = s0 [ s0 = len_ghost'0 {_25} (fun (_ret':int) -> [ &_23 <- _ret' ] s1) | s1 = bb11 ] + | bb11 = s0 [ s0 = minus_one'0 {_23} (fun (_ret':int) -> [ &off <- _ret' ] s1) | s1 = bb12 ] | bb12 = s0 - [ s0 = {[@expl:type invariant] inv'3 _21} s1 - | s1 = -{resolve'0 _21}- s2 - | s2 = {[@expl:type invariant] inv'1 seq} s3 - | s3 = -{resolve'1 seq}- s4 - | s4 = {[@expl:type invariant] inv'4 self} s5 - | s5 = -{resolve'2 self}- s6 - | s6 = new'0 {_19} (fun (_ret':t_GhostBox'3) -> [ &_18 <- _ret' ] s7) - | s7 = bb13 ] - - | bb13 = bb14 - | bb14 = bb15 - | bb15 = bb27 - | bb16 = s0 - [ s0 = {[@expl:type invariant] inv'5 cell_own} s1 - | s1 = -{resolve'3 cell_own}- s2 - | s2 = {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} + [ 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) -> - [ &_26 <- _ret' ] + [ &_31 <- _ret' ] -{inv'0 _ret'.final}- [ &self <- { self with current = { self.current with t_List__seq'0 = _ret'.final } } ] - s3) - | s3 = borrow_mut'0 {_26} (fun (_ret':t_GhostBox'2) -> [ &seq1 <- _ret' ] s4) - | s4 = bb17 ] - - | bb17 = s0 - [ s0 = deref'0 {seq1} (fun (_ret':MutBorrow.t (Seq.seq t_PtrOwn'0)) -> [ &_35 <- _ret' ] s1) | s1 = bb18 ] - - | bb18 = s0 [ s0 = len_ghost'0 {_35.current} (fun (_ret':int) -> [ &_33 <- _ret' ] s1) | s1 = bb19 ] - | bb19 = s0 [ s0 = minus_one'0 {_33} (fun (_ret':int) -> [ &off <- _ret' ] s1) | s1 = bb20 ] - | bb20 = s0 - [ s0 = into_inner'1 {seq1} (fun (_ret':MutBorrow.t (Seq.seq t_PtrOwn'0)) -> [ &_40 <- _ret' ] s1) | s1 = bb21 ] + s1) + | s1 = deref_mut'0 {_31} (fun (_ret':MutBorrow.t (Seq.seq t_PtrOwn'0)) -> [ &_30 <- _ret' ] s2) + | s2 = bb13 ] - | bb21 = s0 - [ s0 = {inv'2 _40.current} - MutBorrow.borrow_final {_40.current} {MutBorrow.get_id _40} + | bb13 = s0 + [ s0 = {inv'1 _30.current} + MutBorrow.borrow_final {_30.current} {MutBorrow.get_id _30} (fun (_ret':MutBorrow.t (Seq.seq t_PtrOwn'0)) -> - [ &_39 <- _ret' ] - -{inv'2 _ret'.final}- - [ &_40 <- { _40 with current = _ret'.final } ] + [ &_29 <- _ret' ] + -{inv'1 _ret'.final}- + [ &_30 <- { _30 with current = _ret'.final } ] s1) - | s1 = get_mut_ghost'0 {_39} {off} (fun (_ret':t_Option'0) -> [ &_38 <- _ret' ] s2) - | s2 = bb22 ] + | s1 = get_mut_ghost'0 {_29} {off} (fun (_ret':t_Option'0) -> [ &_28 <- _ret' ] s2) + | s2 = bb14 ] - | bb22 = s0 [ s0 = unwrap'0 {_38} (fun (_ret':MutBorrow.t t_PtrOwn'0) -> [ &_37 <- _ret' ] s1) | s1 = bb23 ] - | bb23 = s0 - [ s0 = {inv'6 _37.current} - MutBorrow.borrow_final {_37.current} {MutBorrow.get_id _37} + | bb14 = s0 [ s0 = unwrap'0 {_28} (fun (_ret':MutBorrow.t t_PtrOwn'0) -> [ &_27 <- _ret' ] s1) | s1 = bb15 ] + | bb15 = s0 + [ s0 = {inv'2 _27.current} + MutBorrow.borrow_final {_27.current} {MutBorrow.get_id _27} (fun (_ret':MutBorrow.t t_PtrOwn'0) -> - [ &_31 <- _ret' ] - -{inv'6 _ret'.final}- - [ &_37 <- { _37 with current = _ret'.final } ] + [ &_21 <- _ret' ] + -{inv'2 _ret'.final}- + [ &_27 <- { _27 with current = _ret'.final } ] s1) - | s1 = {inv'6 _31.current} - MutBorrow.borrow_final {_31.current} {MutBorrow.get_id _31} + | s1 = {inv'2 _21.current} + MutBorrow.borrow_final {_21.current} {MutBorrow.get_id _21} (fun (_ret':MutBorrow.t t_PtrOwn'0) -> - [ &_30 <- _ret' ] - -{inv'6 _ret'.final}- - [ &_31 <- { _31 with current = _ret'.final } ] + [ &_20 <- _ret' ] + -{inv'2 _ret'.final}- + [ &_21 <- { _21 with current = _ret'.final } ] s2) - | s2 = new'1 {_30} (fun (_ret':t_GhostBox'4) -> [ &_29 <- _ret' ] s3) - | s3 = bb24 ] + | s2 = new'0 {_20} (fun (_ret':t_GhostBox'2) -> [ &_19 <- _ret' ] s3) + | s3 = bb16 ] - | bb24 = s0 - [ s0 = as_mut'0 {(self.current).t_List__last'0} {_29} + | bb16 = s0 + [ s0 = as_mut'0 {(self.current).t_List__last'0} {_19} (fun (_ret':MutBorrow.t t_Cell'0) -> [ &cell_last <- _ret' ] s1) - | s1 = bb25 ] + | s1 = bb17 ] - | bb25 = s0 - [ s0 = {[@expl:type invariant] inv'7 _40} s1 - | s1 = -{resolve'4 _40}- s2 - | s2 = {[@expl:type invariant] inv'8 _37} s3 - | s3 = -{resolve'5 _37}- s4 - | s4 = {[@expl:type invariant] inv'8 _31} s5 - | s5 = -{resolve'5 _31}- s6 + | bb17 = s0 + [ s0 = {[@expl:type invariant] inv'3 _30} s1 + | s1 = -{resolve'0 _30}- s2 + | s2 = {[@expl:type invariant] inv'4 _27} s3 + | s3 = -{resolve'1 _27}- s4 + | s4 = {[@expl:type invariant] inv'4 _21} s5 + | s5 = -{resolve'1 _21}- s6 | s6 = [ &cell_last <- { cell_last with current = { cell_last.current with t_Cell__next'0 = cell_ptr } } ] s7 - | s7 = {[@expl:type invariant] inv'9 cell_last} s8 - | s8 = -{resolve'6 cell_last}- s9 + | s7 = {[@expl:type invariant] inv'5 cell_last} s8 + | s8 = -{resolve'2 cell_last}- s9 | s9 = [ &self <- { self with current = { self.current with t_List__last'0 = cell_ptr } } ] s10 - | s10 = {[@expl:type invariant] inv'4 self} s11 - | s11 = -{resolve'2 self}- s12 - | s12 = bb26 ] + | s10 = bb18 ] - | bb26 = bb27 - | bb27 = bb28 - | bb28 = bb29 - | bb29 = bb30 - | bb30 = return' {_0} ] + | bb18 = 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) -> + [ &_39 <- _ret' ] + -{inv'0 _ret'.final}- + [ &self <- { self with current = { self.current with t_List__seq'0 = _ret'.final } } ] + s1) + | s1 = deref_mut'0 {_39} (fun (_ret':MutBorrow.t (Seq.seq t_PtrOwn'0)) -> [ &_38 <- _ret' ] s2) + | s2 = bb19 ] + + | bb19 = s0 + [ s0 = {inv'1 _38.current} + MutBorrow.borrow_final {_38.current} {MutBorrow.get_id _38} + (fun (_ret':MutBorrow.t (Seq.seq t_PtrOwn'0)) -> + [ &_37 <- _ret' ] + -{inv'1 _ret'.final}- + [ &_38 <- { _38 with current = _ret'.final } ] + s1) + | s1 = into_inner'0 {cell_own} (fun (_ret':t_PtrOwn'0) -> [ &_40 <- _ret' ] s2) + | s2 = bb20 ] + + | bb20 = s0 [ s0 = push_back_ghost'0 {_37} {_40} (fun (_ret':()) -> [ &_36 <- _ret' ] s1) | s1 = bb21 ] + | bb21 = s0 + [ s0 = {[@expl:type invariant] inv'3 _38} s1 + | s1 = -{resolve'0 _38}- s2 + | s2 = {[@expl:type invariant] inv'6 self} s3 + | s3 = -{resolve'3 self}- s4 + | s4 = new'1 {_36} (fun (_ret':t_GhostBox'3) -> [ &_35 <- _ret' ] s5) + | s5 = bb22 ] + + | bb22 = bb23 + | bb23 = bb24 + | bb24 = bb25 + | bb25 = bb26 + | bb26 = return' {_0} ] ) [ & _0 : () = Any.any_l () | & self : MutBorrow.t t_List'0 = self @@ -846,71 +742,63 @@ module M_linked_list__qyi10858349784728989480__push_back [#"linked_list.rs" 77 4 | & cell_ptr : Opaque.ptr = Any.any_l () | & cell_own : t_GhostBox'0 = Any.any_l () | & _10 : (Opaque.ptr, t_GhostBox'0) = Any.any_l () - | & _12 : bool = Any.any_l () - | & seq : t_GhostBox'2 = Any.any_l () - | & _17 : MutBorrow.t t_GhostBox'1 = Any.any_l () - | & _18 : t_GhostBox'3 = Any.any_l () - | & _19 : () = Any.any_l () - | & _20 : MutBorrow.t (Seq.seq t_PtrOwn'0) = Any.any_l () - | & _21 : MutBorrow.t (MutBorrow.t (Seq.seq t_PtrOwn'0)) = Any.any_l () - | & _22 : MutBorrow.t t_GhostBox'2 = Any.any_l () - | & _23 : t_PtrOwn'0 = Any.any_l () - | & seq1 : t_GhostBox'2 = Any.any_l () - | & _26 : MutBorrow.t t_GhostBox'1 = Any.any_l () + | & _13 : bool = Any.any_l () | & cell_last : MutBorrow.t t_Cell'0 = Any.any_l () - | & _29 : t_GhostBox'4 = Any.any_l () - | & _30 : MutBorrow.t t_PtrOwn'0 = Any.any_l () - | & _31 : MutBorrow.t t_PtrOwn'0 = Any.any_l () + | & _19 : t_GhostBox'2 = Any.any_l () + | & _20 : MutBorrow.t t_PtrOwn'0 = Any.any_l () + | & _21 : MutBorrow.t t_PtrOwn'0 = Any.any_l () | & off : int = Any.any_l () - | & _33 : int = Any.any_l () - | & _35 : MutBorrow.t (Seq.seq t_PtrOwn'0) = Any.any_l () - | & _37 : MutBorrow.t t_PtrOwn'0 = Any.any_l () - | & _38 : t_Option'0 = Any.any_l () - | & _39 : MutBorrow.t (Seq.seq t_PtrOwn'0) = Any.any_l () - | & _40 : MutBorrow.t (Seq.seq t_PtrOwn'0) = Any.any_l () ] + | & _23 : int = Any.any_l () + | & _25 : Seq.seq t_PtrOwn'0 = Any.any_l () + | & _27 : MutBorrow.t t_PtrOwn'0 = Any.any_l () + | & _28 : t_Option'0 = Any.any_l () + | & _29 : MutBorrow.t (Seq.seq t_PtrOwn'0) = Any.any_l () + | & _30 : MutBorrow.t (Seq.seq t_PtrOwn'0) = Any.any_l () + | & _31 : MutBorrow.t t_GhostBox'1 = Any.any_l () + | & _35 : t_GhostBox'3 = Any.any_l () + | & _36 : () = Any.any_l () + | & _37 : MutBorrow.t (Seq.seq t_PtrOwn'0) = Any.any_l () + | & _38 : MutBorrow.t (Seq.seq t_PtrOwn'0) = Any.any_l () + | & _39 : MutBorrow.t t_GhostBox'1 = Any.any_l () + | & _40 : t_PtrOwn'0 = Any.any_l () ] [ 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" 95 4 95 38] (* List *) + let%span slinked_list0 = "linked_list.rs" 95 27 95 31 + let%span slinked_list1 = "linked_list.rs" 95 33 95 34 + let%span slinked_list2 = "linked_list.rs" 94 14 94 48 let%span sptr_own3 = "../../creusot-contracts/src/ptr_own.rs" 52 15 52 16 let%span sptr_own4 = "../../creusot-contracts/src/ptr_own.rs" 52 4 52 56 let%span sptr_own5 = "../../creusot-contracts/src/ptr_own.rs" 51 14 51 64 let%span sptr6 = "../../creusot-contracts/src/std/ptr.rs" 107 18 107 48 - let%span sghost7 = "../../creusot-contracts/src/ghost.rs" 141 27 141 31 - let%span sghost8 = "../../creusot-contracts/src/ghost.rs" 141 4 141 52 - let%span sghost9 = "../../creusot-contracts/src/ghost.rs" 140 14 140 39 - let%span sghost10 = "../../creusot-contracts/src/ghost.rs" 85 22 85 26 - let%span sghost11 = "../../creusot-contracts/src/ghost.rs" 85 4 85 48 - let%span sghost12 = "../../creusot-contracts/src/ghost.rs" 84 14 84 36 - let%span sghost13 = "../../creusot-contracts/src/ghost.rs" 210 22 210 26 - let%span sghost14 = "../../creusot-contracts/src/ghost.rs" 210 4 210 32 - let%span sghost15 = "../../creusot-contracts/src/ghost.rs" 208 14 208 31 - let%span sseq16 = "../../creusot-contracts/src/logic/seq.rs" 472 33 472 37 - let%span sseq17 = "../../creusot-contracts/src/logic/seq.rs" 472 39 472 40 - let%span sseq18 = "../../creusot-contracts/src/logic/seq.rs" 471 14 471 41 - let%span sghost19 = "../../creusot-contracts/src/ghost.rs" 185 15 185 16 - let%span sghost20 = "../../creusot-contracts/src/ghost.rs" 185 4 185 28 - let%span sghost21 = "../../creusot-contracts/src/ghost.rs" 183 14 183 28 - let%span slinked_list22 = "linked_list.rs" 48 12 48 74 - let%span sseq23 = "../../creusot-contracts/src/logic/seq.rs" 247 8 247 27 - let%span sghost24 = "../../creusot-contracts/src/ghost.rs" 224 4 224 12 - let%span sptr25 = "../../creusot-contracts/src/std/ptr.rs" 80 14 80 48 - let%span sptr26 = "../../creusot-contracts/src/std/ptr.rs" 82 8 82 30 - let%span sresolve27 = "../../creusot-contracts/src/resolve.rs" 54 20 54 34 - let%span sghost28 = "../../creusot-contracts/src/ghost.rs" 108 4 108 27 - let%span slinked_list29 = "linked_list.rs" 67 4 67 41 - let%span sseq30 = "../../creusot-contracts/src/logic/seq.rs" 629 20 629 95 - let%span sinvariant31 = "../../creusot-contracts/src/invariant.rs" 35 20 35 44 - let%span sresolve32 = "../../creusot-contracts/src/resolve.rs" 68 8 68 23 - let%span sptr_own33 = "../../creusot-contracts/src/ptr_own.rs" 44 20 44 66 - let%span sboxed34 = "../../creusot-contracts/src/std/boxed.rs" 33 8 33 18 - let%span slinked_list35 = "linked_list.rs" 26 12 36 69 + let%span sghost7 = "../../creusot-contracts/src/ghost.rs" 85 22 85 26 + let%span sghost8 = "../../creusot-contracts/src/ghost.rs" 85 4 85 48 + let%span sghost9 = "../../creusot-contracts/src/ghost.rs" 84 14 84 36 + let%span sghost10 = "../../creusot-contracts/src/ghost.rs" 210 22 210 26 + let%span sghost11 = "../../creusot-contracts/src/ghost.rs" 210 4 210 32 + let%span sghost12 = "../../creusot-contracts/src/ghost.rs" 208 14 208 31 + let%span sseq13 = "../../creusot-contracts/src/logic/seq.rs" 472 33 472 37 + let%span sseq14 = "../../creusot-contracts/src/logic/seq.rs" 472 39 472 40 + let%span sseq15 = "../../creusot-contracts/src/logic/seq.rs" 471 14 471 41 + let%span sghost16 = "../../creusot-contracts/src/ghost.rs" 185 15 185 16 + let%span sghost17 = "../../creusot-contracts/src/ghost.rs" 185 4 185 28 + let%span sghost18 = "../../creusot-contracts/src/ghost.rs" 183 14 183 28 + let%span slinked_list19 = "linked_list.rs" 48 12 48 74 + let%span sseq20 = "../../creusot-contracts/src/logic/seq.rs" 247 8 247 27 + let%span sghost21 = "../../creusot-contracts/src/ghost.rs" 224 4 224 12 + 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 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" 44 20 44 66 + let%span sboxed29 = "../../creusot-contracts/src/std/boxed.rs" 33 8 33 18 + let%span slinked_list30 = "linked_list.rs" 26 12 36 69 use creusot.prelude.Opaque @@ -929,13 +817,13 @@ module M_linked_list__qyi10858349784728989480__push_front [#"linked_list.rs" 97 type t_Cell'0 = { t_Cell__v'0: t_T'0; t_Cell__next'0: Opaque.ptr } - predicate inv'5 (_1 : t_T'0) + predicate inv'4 (_1 : t_T'0) - predicate inv'6 (_1 : t_Cell'0) + predicate inv'5 (_1 : t_Cell'0) - axiom inv_axiom'5 [@rewrite] : forall x : t_Cell'0 [inv'6 x] . inv'6 x + axiom inv_axiom'4 [@rewrite] : forall x : t_Cell'0 [inv'5 x] . inv'5 x = match x with - | {t_Cell__v'0 = v ; t_Cell__next'0 = next} -> inv'5 v + | {t_Cell__v'0 = v ; t_Cell__next'0 = next} -> inv'4 v end type t_GhostBox'0 = @@ -944,53 +832,53 @@ module M_linked_list__qyi10858349784728989480__push_front [#"linked_list.rs" 97 function addr_logic'0 (self : Opaque.ptr) : int function is_null_logic'0 (self : Opaque.ptr) : bool = - [%#sptr26] addr_logic'0 self = 0 + [%#sptr23] addr_logic'0 self = 0 - axiom is_null_logic'0_spec : forall self : Opaque.ptr . [%#sptr25] is_null_logic'0 self = (addr_logic'0 self = 0) + axiom is_null_logic'0_spec : forall self : Opaque.ptr . [%#sptr22] is_null_logic'0 self = (addr_logic'0 self = 0) function ptr'0 (self : t_PtrOwn'0) : Opaque.ptr - predicate invariant'11 (self : t_Cell'0) = - [%#sboxed34] inv'6 self + predicate invariant'8 (self : t_Cell'0) = + [%#sboxed29] inv'5 self - predicate inv'19 (_1 : t_Cell'0) + predicate inv'15 (_1 : t_Cell'0) - axiom inv_axiom'18 [@rewrite] : forall x : t_Cell'0 [inv'19 x] . inv'19 x = invariant'11 x + axiom inv_axiom'14 [@rewrite] : forall x : t_Cell'0 [inv'15 x] . inv'15 x = invariant'8 x function val'0 (self : t_PtrOwn'0) : t_Cell'0 - predicate invariant'5 (self : t_PtrOwn'0) = - [%#sptr_own33] not is_null_logic'0 (ptr'0 self) /\ inv'19 (val'0 self) + predicate invariant'4 (self : t_PtrOwn'0) = + [%#sptr_own28] not is_null_logic'0 (ptr'0 self) /\ inv'15 (val'0 self) - predicate inv'11 (_1 : t_PtrOwn'0) + predicate inv'9 (_1 : t_PtrOwn'0) - axiom inv_axiom'10 [@rewrite] : forall x : t_PtrOwn'0 [inv'11 x] . inv'11 x = invariant'5 x + axiom inv_axiom'8 [@rewrite] : forall x : t_PtrOwn'0 [inv'9 x] . inv'9 x = invariant'4 x - predicate invariant'9 (self : t_PtrOwn'0) = - [%#sboxed34] inv'11 self + predicate invariant'6 (self : t_PtrOwn'0) = + [%#sboxed29] inv'9 self - predicate inv'17 (_1 : t_PtrOwn'0) + predicate inv'13 (_1 : t_PtrOwn'0) - axiom inv_axiom'16 [@rewrite] : forall x : t_PtrOwn'0 [inv'17 x] . inv'17 x = invariant'9 x + axiom inv_axiom'12 [@rewrite] : forall x : t_PtrOwn'0 [inv'13 x] . inv'13 x = invariant'6 x - predicate inv'10 (_1 : t_GhostBox'0) + predicate inv'8 (_1 : t_GhostBox'0) - axiom inv_axiom'9 [@rewrite] : forall x : t_GhostBox'0 [inv'10 x] . inv'10 x + axiom inv_axiom'7 [@rewrite] : forall x : t_GhostBox'0 [inv'8 x] . inv'8 x = match x with - | {t_GhostBox__0'0 = a_0} -> inv'17 a_0 + | {t_GhostBox__0'0 = a_0} -> inv'13 a_0 end - predicate inv'7 (_1 : (Opaque.ptr, t_GhostBox'0)) + predicate inv'6 (_1 : (Opaque.ptr, t_GhostBox'0)) - axiom inv_axiom'6 [@rewrite] : forall x : (Opaque.ptr, t_GhostBox'0) [inv'7 x] . inv'7 x - = (let (x0, x1) = x in inv'10 x1) + axiom inv_axiom'5 [@rewrite] : forall x : (Opaque.ptr, t_GhostBox'0) [inv'6 x] . inv'6 x + = (let (x0, x1) = x in inv'8 x1) function inner_logic'0 (self : t_GhostBox'0) : t_PtrOwn'0 = - [%#sghost24] self.t_GhostBox__0'0 + [%#sghost21] self.t_GhostBox__0'0 - let rec new'0 (v:t_Cell'0) (return' (ret:(Opaque.ptr, t_GhostBox'0)))= {[@expl:new 'v' type invariant] [%#sptr_own3] inv'6 v} + let rec new'0 (v:t_Cell'0) (return' (ret:(Opaque.ptr, t_GhostBox'0)))= {[@expl:new 'v' type invariant] [%#sptr_own3] inv'5 v} any - [ return' (result:(Opaque.ptr, t_GhostBox'0))-> {[%#sptr_own4] inv'7 result} + [ return' (result:(Opaque.ptr, t_GhostBox'0))-> {[%#sptr_own4] inv'6 result} {[%#sptr_own5] 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)) = v} (! return' {result}) ] @@ -1009,134 +897,79 @@ module M_linked_list__qyi10858349784728989480__push_front [#"linked_list.rs" 97 use seq.Seq predicate invariant'0 (self : Seq.seq t_PtrOwn'0) = - [%#sseq30] forall i : int . 0 <= i /\ i < Seq.length self -> inv'17 (Seq.get self i) + [%#sseq26] forall i : int . 0 <= i /\ i < Seq.length self -> inv'13 (Seq.get self i) - predicate inv'2 (_1 : Seq.seq t_PtrOwn'0) + predicate inv'1 (_1 : Seq.seq t_PtrOwn'0) - axiom inv_axiom'2 [@rewrite] : forall x : Seq.seq t_PtrOwn'0 [inv'2 x] . inv'2 x = invariant'0 x + axiom inv_axiom'1 [@rewrite] : forall x : Seq.seq t_PtrOwn'0 [inv'1 x] . inv'1 x = invariant'0 x - predicate invariant'7 (self : Seq.seq t_PtrOwn'0) = - [%#sboxed34] inv'2 self + predicate invariant'5 (self : Seq.seq t_PtrOwn'0) = + [%#sboxed29] inv'1 self - predicate inv'15 (_1 : Seq.seq t_PtrOwn'0) + predicate inv'12 (_1 : Seq.seq t_PtrOwn'0) - axiom inv_axiom'14 [@rewrite] : forall x : Seq.seq t_PtrOwn'0 [inv'15 x] . inv'15 x = invariant'7 x + axiom inv_axiom'11 [@rewrite] : forall x : Seq.seq t_PtrOwn'0 [inv'12 x] . inv'12 x = invariant'5 x predicate inv'0 (_1 : t_GhostBox'1) axiom inv_axiom'0 [@rewrite] : forall x : t_GhostBox'1 [inv'0 x] . inv'0 x = match x with - | {t_GhostBox__0'1 = a_0} -> inv'15 a_0 + | {t_GhostBox__0'1 = a_0} -> inv'12 a_0 end predicate invariant'3 (self : MutBorrow.t t_GhostBox'1) = - [%#sinvariant31] inv'0 self.current /\ inv'0 self.final - - predicate inv'8 (_1 : MutBorrow.t t_GhostBox'1) - - axiom inv_axiom'7 [@rewrite] : forall x : MutBorrow.t t_GhostBox'1 [inv'8 x] . inv'8 x = invariant'3 x - - type t_GhostBox'2 = - { t_GhostBox__0'2: MutBorrow.t (Seq.seq t_PtrOwn'0) } - - predicate invariant'6 (self : MutBorrow.t (Seq.seq t_PtrOwn'0)) = - [%#sinvariant31] inv'2 self.current /\ inv'2 self.final + [%#sinvariant27] inv'0 self.current /\ inv'0 self.final - predicate inv'12 (_1 : MutBorrow.t (Seq.seq t_PtrOwn'0)) + predicate inv'7 (_1 : MutBorrow.t t_GhostBox'1) - axiom inv_axiom'11 [@rewrite] : forall x : MutBorrow.t (Seq.seq t_PtrOwn'0) [inv'12 x] . inv'12 x = invariant'6 x + axiom inv_axiom'6 [@rewrite] : forall x : MutBorrow.t t_GhostBox'1 [inv'7 x] . inv'7 x = invariant'3 x - predicate invariant'8 (self : MutBorrow.t (Seq.seq t_PtrOwn'0)) = - [%#sboxed34] inv'12 self + predicate invariant'1 (self : MutBorrow.t (Seq.seq t_PtrOwn'0)) = + [%#sinvariant27] inv'1 self.current /\ inv'1 self.final - predicate inv'16 (_1 : MutBorrow.t (Seq.seq t_PtrOwn'0)) + predicate inv'2 (_1 : MutBorrow.t (Seq.seq t_PtrOwn'0)) - axiom inv_axiom'15 [@rewrite] : forall x : MutBorrow.t (Seq.seq t_PtrOwn'0) [inv'16 x] . inv'16 x = invariant'8 x + axiom inv_axiom'2 [@rewrite] : forall x : MutBorrow.t (Seq.seq t_PtrOwn'0) [inv'2 x] . inv'2 x = invariant'1 x - predicate inv'1 (_1 : t_GhostBox'2) - - axiom inv_axiom'1 [@rewrite] : forall x : t_GhostBox'2 [inv'1 x] . inv'1 x - = match x with - | {t_GhostBox__0'2 = a_0} -> inv'16 a_0 - end - - let rec borrow_mut'0 (self:MutBorrow.t t_GhostBox'1) (return' (ret:t_GhostBox'2))= {[@expl:borrow_mut 'self' type invariant] [%#sghost7] inv'8 self} + 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] [%#sghost7] inv'7 self} any - [ return' (result:t_GhostBox'2)-> {[%#sghost8] inv'1 result} - {[%#sghost9] result.t_GhostBox__0'2 + [ return' (result:MutBorrow.t (Seq.seq t_PtrOwn'0))-> {[%#sghost8] inv'2 result} + {[%#sghost9] 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}) ] - predicate invariant'4 (self : MutBorrow.t t_GhostBox'2) = - [%#sinvariant31] inv'1 self.current /\ inv'1 self.final - - predicate inv'9 (_1 : MutBorrow.t t_GhostBox'2) - - axiom inv_axiom'8 [@rewrite] : forall x : MutBorrow.t t_GhostBox'2 [inv'9 x] . inv'9 x = invariant'4 x - - predicate invariant'1 (self : MutBorrow.t (MutBorrow.t (Seq.seq t_PtrOwn'0))) = - [%#sinvariant31] inv'12 self.current /\ inv'12 self.final - - predicate inv'3 (_1 : MutBorrow.t (MutBorrow.t (Seq.seq t_PtrOwn'0))) - - axiom inv_axiom'3 [@rewrite] : forall x : MutBorrow.t (MutBorrow.t (Seq.seq t_PtrOwn'0)) [inv'3 x] . inv'3 x - = invariant'1 x - - let rec deref_mut'0 (self:MutBorrow.t t_GhostBox'2) (return' (ret:MutBorrow.t (MutBorrow.t (Seq.seq t_PtrOwn'0))))= {[@expl:deref_mut 'self' type invariant] [%#sghost10] inv'9 self} - any - [ return' (result:MutBorrow.t (MutBorrow.t (Seq.seq t_PtrOwn'0)))-> {[%#sghost11] inv'3 result} - {[%#sghost12] result - = MutBorrow.borrow_logic (self.current).t_GhostBox__0'2 (self.final).t_GhostBox__0'2 (MutBorrow.inherit_id (MutBorrow.get_id self) 1)} - (! return' {result}) ] - - - let rec into_inner'0 (self:t_GhostBox'0) (return' (ret:t_PtrOwn'0))= {[@expl:into_inner 'self' type invariant] [%#sghost13] inv'10 self} + let rec into_inner'0 (self:t_GhostBox'0) (return' (ret:t_PtrOwn'0))= {[@expl:into_inner 'self' type invariant] [%#sghost10] inv'8 self} any - [ return' (result:t_PtrOwn'0)-> {[%#sghost14] inv'11 result} - {[%#sghost15] result = self.t_GhostBox__0'0} + [ return' (result:t_PtrOwn'0)-> {[%#sghost11] inv'9 result} + {[%#sghost12] result = self.t_GhostBox__0'0} (! return' {result}) ] use seq.Seq function push_front'2 [@inline:trivial] (self : Seq.seq t_PtrOwn'0) (x : t_PtrOwn'0) : Seq.seq t_PtrOwn'0 = - [%#sseq23] Seq.cons x self + [%#sseq20] Seq.cons x self - let rec push_front_ghost'0 (self:MutBorrow.t (Seq.seq t_PtrOwn'0)) (x:t_PtrOwn'0) (return' (ret:()))= {[@expl:push_front_ghost 'self' type invariant] [%#sseq16] inv'12 self} - {[@expl:push_front_ghost 'x' type invariant] [%#sseq17] inv'11 x} - any [ return' (result:())-> {[%#sseq18] self.final = push_front'2 self.current x} (! return' {result}) ] + let rec push_front_ghost'0 (self:MutBorrow.t (Seq.seq t_PtrOwn'0)) (x:t_PtrOwn'0) (return' (ret:()))= {[@expl:push_front_ghost 'self' type invariant] [%#sseq13] inv'2 self} + {[@expl:push_front_ghost 'x' type invariant] [%#sseq14] inv'9 x} + any [ return' (result:())-> {[%#sseq15] self.final = push_front'2 self.current x} (! return' {result}) ] - predicate resolve'3 (self : MutBorrow.t (MutBorrow.t (Seq.seq t_PtrOwn'0))) = - [%#sresolve27] self.final = self.current + predicate resolve'2 (self : MutBorrow.t (Seq.seq t_PtrOwn'0)) = + [%#sresolve24] self.final = self.current - predicate resolve'0 (_1 : MutBorrow.t (MutBorrow.t (Seq.seq t_PtrOwn'0))) = - resolve'3 _1 - - predicate resolve'8 (self : MutBorrow.t (Seq.seq t_PtrOwn'0)) = - [%#sresolve27] self.final = self.current - - predicate resolve'7 (_1 : MutBorrow.t (Seq.seq t_PtrOwn'0)) = - resolve'8 _1 - - predicate resolve'6 (self : MutBorrow.t (Seq.seq t_PtrOwn'0)) = - [%#sresolve32] resolve'7 self - - predicate resolve'4 (self : t_GhostBox'2) = - [%#sghost28] resolve'6 self.t_GhostBox__0'2 - - predicate resolve'1 (_1 : t_GhostBox'2) = - resolve'4 _1 + predicate resolve'0 (_1 : MutBorrow.t (Seq.seq t_PtrOwn'0)) = + resolve'2 _1 function inner_logic'1 (self : t_GhostBox'1) : Seq.seq t_PtrOwn'0 = - [%#sghost24] self.t_GhostBox__0'1 + [%#sghost21] self.t_GhostBox__0'1 use seq.Seq use seq.Seq - predicate invariant'10 [#"linked_list.rs" 24 4 24 30] (self : t_List'0) = - [%#slinked_list35] inner_logic'1 self.t_List__seq'0 = (Seq.empty : Seq.seq t_PtrOwn'0) + predicate invariant'7 [#"linked_list.rs" 24 4 24 30] (self : t_List'0) = + [%#slinked_list30] inner_logic'1 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'1 self.t_List__seq'0) > 0 /\ self.t_List__first'0 = ptr'0 (Seq.get (inner_logic'1 self.t_List__seq'0) 0) @@ -1148,42 +981,42 @@ module M_linked_list__qyi10858349784728989480__push_front [#"linked_list.rs" 97 /\ is_null_logic'0 (val'0 (Seq.get (inner_logic'1 self.t_List__seq'0) (Seq.length (inner_logic'1 self.t_List__seq'0) - 1))).t_Cell__next'0 - predicate inv'18 (_1 : t_List'0) + predicate inv'14 (_1 : t_List'0) - axiom inv_axiom'17 [@rewrite] : forall x : t_List'0 [inv'18 x] . inv'18 x - = (invariant'10 x + axiom inv_axiom'13 [@rewrite] : forall x : t_List'0 [inv'14 x] . inv'14 x + = (invariant'7 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'2 (self : MutBorrow.t t_List'0) = - [%#sinvariant31] inv'18 self.current /\ inv'18 self.final + [%#sinvariant27] inv'14 self.current /\ inv'14 self.final - predicate inv'4 (_1 : MutBorrow.t t_List'0) + predicate inv'3 (_1 : MutBorrow.t t_List'0) - axiom inv_axiom'4 [@rewrite] : forall x : MutBorrow.t t_List'0 [inv'4 x] . inv'4 x = invariant'2 x + axiom inv_axiom'3 [@rewrite] : forall x : MutBorrow.t t_List'0 [inv'3 x] . inv'3 x = invariant'2 x - predicate resolve'5 (self : MutBorrow.t t_List'0) = - [%#sresolve27] self.final = self.current + predicate resolve'3 (self : MutBorrow.t t_List'0) = + [%#sresolve24] self.final = self.current - predicate resolve'2 (_1 : MutBorrow.t t_List'0) = - resolve'5 _1 + predicate resolve'1 (_1 : MutBorrow.t t_List'0) = + resolve'3 _1 - predicate inv'13 (_1 : ()) + predicate inv'10 (_1 : ()) - axiom inv_axiom'12 [@rewrite] : forall x : () [inv'13 x] . inv'13 x = true + axiom inv_axiom'9 [@rewrite] : forall x : () [inv'10 x] . inv'10 x = true - type t_GhostBox'3 = - { t_GhostBox__0'3: () } + type t_GhostBox'2 = + { t_GhostBox__0'2: () } - predicate inv'14 (_1 : t_GhostBox'3) + predicate inv'11 (_1 : t_GhostBox'2) - axiom inv_axiom'13 [@rewrite] : forall x : t_GhostBox'3 [inv'14 x] . inv'14 x = true + axiom inv_axiom'10 [@rewrite] : forall x : t_GhostBox'2 [inv'11 x] . inv'11 x = true - let rec new'1 (x:()) (return' (ret:t_GhostBox'3))= {[@expl:new 'x' type invariant] [%#sghost19] inv'13 x} + let rec new'1 (x:()) (return' (ret:t_GhostBox'2))= {[@expl:new 'x' type invariant] [%#sghost16] inv'10 x} any - [ return' (result:t_GhostBox'3)-> {[%#sghost20] inv'14 result} - {[%#sghost21] result.t_GhostBox__0'3 = x} + [ return' (result:t_GhostBox'2)-> {[%#sghost17] inv'11 result} + {[%#sghost18] result.t_GhostBox__0'2 = x} (! return' {result}) ] @@ -1200,20 +1033,20 @@ module M_linked_list__qyi10858349784728989480__push_front [#"linked_list.rs" 97 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 = - [%#slinked_list29] Seq.create (Seq.length s) (fun (i : int) -> Map.get f (Seq.get s i)) + [%#slinked_list25] 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_list22] seq_map'0 (inner_logic'1 self.t_List__seq'0) (fun (ptr_own : t_PtrOwn'0) -> (val'0 ptr_own).t_Cell__v'0) + [%#slinked_list19] seq_map'0 (inner_logic'1 self.t_List__seq'0) (fun (ptr_own : t_PtrOwn'0) -> (val'0 ptr_own).t_Cell__v'0) use seq.Seq function push_front'1 [@inline:trivial] (self : Seq.seq t_T'0) (x : t_T'0) : Seq.seq t_T'0 = - [%#sseq23] Seq.cons x self + [%#sseq20] Seq.cons x self 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'4 self} - {[@expl:push_front 'x' type invariant] [%#slinked_list1] inv'5 x} + let rec push_front'0[#"linked_list.rs" 95 4 95 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 | bb1 = s0 [ s0 = [ &_7 <- { t_Cell__v'0 = x; t_Cell__next'0 = (self.current).t_List__first'0 } ] s1 | s1 = bb2 ] @@ -1240,47 +1073,37 @@ module M_linked_list__qyi10858349784728989480__push_front [#"linked_list.rs" 97 {(self.current).t_List__seq'0} {MutBorrow.inherit_id (MutBorrow.get_id self) 3} (fun (_ret':MutBorrow.t t_GhostBox'1) -> - [ &_16 <- _ret' ] + [ &_19 <- _ret' ] -{inv'0 _ret'.final}- [ &self <- { self with current = { self.current with t_List__seq'0 = _ret'.final } } ] s1) - | s1 = borrow_mut'0 {_16} (fun (_ret':t_GhostBox'2) -> [ &seq <- _ret' ] s2) + | s1 = deref_mut'0 {_19} (fun (_ret':MutBorrow.t (Seq.seq t_PtrOwn'0)) -> [ &_18 <- _ret' ] s2) | s2 = bb9 ] | bb9 = s0 - [ s0 = {inv'1 seq} - MutBorrow.borrow_mut {seq} - (fun (_ret':MutBorrow.t t_GhostBox'2) -> [ &_21 <- _ret' ] -{inv'1 _ret'.final}- [ &seq <- _ret'.final ] s1) - | s1 = deref_mut'0 {_21} (fun (_ret':MutBorrow.t (MutBorrow.t (Seq.seq t_PtrOwn'0))) -> [ &_20 <- _ret' ] s2) - | s2 = bb10 ] - - | bb10 = s0 - [ s0 = {inv'2 (_20.current).current} - MutBorrow.borrow_mut {(_20.current).current} + [ s0 = {inv'1 _18.current} + MutBorrow.borrow_final {_18.current} {MutBorrow.get_id _18} (fun (_ret':MutBorrow.t (Seq.seq t_PtrOwn'0)) -> - [ &_19 <- _ret' ] - -{inv'2 _ret'.final}- - [ &_20 <- { _20 with current = { _20.current with current = _ret'.final } } ] + [ &_17 <- _ret' ] + -{inv'1 _ret'.final}- + [ &_18 <- { _18 with current = _ret'.final } ] s1) - | s1 = into_inner'0 {cell_own} (fun (_ret':t_PtrOwn'0) -> [ &_22 <- _ret' ] s2) - | s2 = bb11 ] + | s1 = into_inner'0 {cell_own} (fun (_ret':t_PtrOwn'0) -> [ &_20 <- _ret' ] s2) + | s2 = bb10 ] - | bb11 = s0 [ s0 = push_front_ghost'0 {_19} {_22} (fun (_ret':()) -> [ &_18 <- _ret' ] s1) | s1 = bb12 ] - | bb12 = s0 - [ s0 = {[@expl:type invariant] inv'3 _20} s1 - | s1 = -{resolve'0 _20}- s2 - | s2 = {[@expl:type invariant] inv'1 seq} s3 - | s3 = -{resolve'1 seq}- s4 - | s4 = {[@expl:type invariant] inv'4 self} s5 - | s5 = -{resolve'2 self}- s6 - | s6 = new'1 {_18} (fun (_ret':t_GhostBox'3) -> [ &_17 <- _ret' ] s7) - | s7 = bb13 ] + | bb10 = s0 [ s0 = push_front_ghost'0 {_17} {_20} (fun (_ret':()) -> [ &_16 <- _ret' ] s1) | s1 = bb11 ] + | bb11 = s0 + [ s0 = {[@expl:type invariant] inv'2 _18} s1 + | s1 = -{resolve'0 _18}- s2 + | s2 = {[@expl:type invariant] inv'3 self} s3 + | s3 = -{resolve'1 self}- s4 + | s4 = new'1 {_16} (fun (_ret':t_GhostBox'2) -> [ &_15 <- _ret' ] s5) + | s5 = bb12 ] + | bb12 = bb13 | bb13 = bb14 | bb14 = bb15 - | bb15 = bb16 - | bb16 = bb17 - | bb17 = return' {_0} ] + | bb15 = return' {_0} ] ) [ & _0 : () = Any.any_l () | & self : MutBorrow.t t_List'0 = self @@ -1290,14 +1113,12 @@ module M_linked_list__qyi10858349784728989480__push_front [#"linked_list.rs" 97 | & _6 : (Opaque.ptr, t_GhostBox'0) = Any.any_l () | & _7 : t_Cell'0 = Any.any_l () | & _12 : bool = Any.any_l () - | & seq : t_GhostBox'2 = Any.any_l () - | & _16 : MutBorrow.t t_GhostBox'1 = Any.any_l () - | & _17 : t_GhostBox'3 = Any.any_l () - | & _18 : () = Any.any_l () - | & _19 : MutBorrow.t (Seq.seq t_PtrOwn'0) = Any.any_l () - | & _20 : MutBorrow.t (MutBorrow.t (Seq.seq t_PtrOwn'0)) = Any.any_l () - | & _21 : MutBorrow.t t_GhostBox'2 = Any.any_l () - | & _22 : t_PtrOwn'0 = Any.any_l () ] + | & _15 : t_GhostBox'2 = Any.any_l () + | & _16 : () = Any.any_l () + | & _17 : MutBorrow.t (Seq.seq t_PtrOwn'0) = Any.any_l () + | & _18 : MutBorrow.t (Seq.seq t_PtrOwn'0) = Any.any_l () + | & _19 : MutBorrow.t t_GhostBox'1 = Any.any_l () + | & _20 : t_PtrOwn'0 = Any.any_l () ] [ return' (result:())-> {[@expl:push_front ensures] [%#slinked_list2] view'0 self.final = push_front'1 (view'0 self.current) x} diff --git a/tests/should_succeed/linked_list.rs b/tests/should_succeed/linked_list.rs index 8c94cb0ed..65fcee52a 100644 --- a/tests/should_succeed/linked_list.rs +++ b/tests/should_succeed/linked_list.rs @@ -80,17 +80,15 @@ impl List { if self.last.is_null() { self.first = cell_ptr; self.last = cell_ptr; - let mut seq = self.seq.borrow_mut(); - ghost! { seq.push_back_ghost(cell_own.into_inner()) }; } else { - let seq = self.seq.borrow_mut(); let cell_last = PtrOwn::as_mut(self.last, ghost! { - let off = minus_one(seq.len_ghost()); - seq.into_inner().get_mut_ghost(off).unwrap() + let off = minus_one(self.seq.len_ghost()); + self.seq.get_mut_ghost(off).unwrap() }); cell_last.next = cell_ptr; self.last = cell_ptr; } + ghost! { self.seq.push_back_ghost(cell_own.into_inner()) }; } #[ensures((^self)@ == (*self)@.push_front(x))] @@ -100,7 +98,6 @@ impl List { if self.last.is_null() { self.last = cell_ptr; } - let mut seq = self.seq.borrow_mut(); - ghost! { seq.push_front_ghost(cell_own.into_inner()) }; + ghost! { self.seq.push_front_ghost(cell_own.into_inner()) }; } } diff --git a/tests/should_succeed/linked_list/proof.json b/tests/should_succeed/linked_list/proof.json index f26c6bfff..e0a52b2b5 100644 --- a/tests/should_succeed/linked_list/proof.json +++ b/tests/should_succeed/linked_list/proof.json @@ -8,20 +8,18 @@ "proofs": { "M_linked_list__qyi10858349784728989480__new": { "vc_new'0": { "prover": "cvc5@1.0.5", "time": 0.023 }, - "vc_new'1": { "prover": "cvc5@1.0.5", "time": 0.023 }, + "vc_new'1": { "prover": "cvc5@1.0.5", "time": 0.011 }, "vc_null'0": { "prover": "cvc5@1.0.5", "time": 0.011 } }, "M_linked_list__qyi10858349784728989480__push_back": { "vc_as_mut'0": { "prover": "cvc5@1.0.5", "time": 0.012 }, - "vc_borrow_mut'0": { "prover": "cvc5@1.0.5", "time": 0.015 }, - "vc_deref'0": { "prover": "cvc5@1.0.5", "time": 0.028 }, + "vc_deref'0": { "prover": "cvc5@1.0.5", "time": 0.013 }, "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_into_inner'1": { "prover": "cvc5@1.0.5", "time": 0.016 }, "vc_is_null'0": { "prover": "cvc5@1.0.5", "time": 0.011 }, - "vc_len_ghost'0": { "prover": "cvc5@1.0.5", "time": 0.026 }, + "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_new'1": { "prover": "cvc5@1.0.5", "time": 0.009 }, @@ -29,48 +27,40 @@ "vc_push_back'0": { "tactic": "split_vc", "children": [ - { "prover": "cvc5@1.0.5", "time": 0.03 }, + { "prover": "cvc5@1.0.5", "time": 0.021 }, { "prover": "cvc5@1.0.5", "time": 0.026 }, - { "prover": "cvc5@1.0.5", "time": 0.054 }, - { "prover": "cvc5@1.0.5", "time": 0.055 }, + { "prover": "cvc5@1.0.5", "time": 0.014 }, + { "prover": "cvc5@1.0.5", "time": 0.027 }, + { "prover": "cvc5@1.0.5", "time": 0.034 }, + { "prover": "cvc5@1.0.5", "time": 0.017 }, + { "prover": "cvc5@1.0.5", "time": 0.027 }, + { "prover": "cvc5@1.0.5", "time": 0.017 }, + { "prover": "cvc5@1.0.5", "time": 0.035 }, { "prover": "cvc5@1.0.5", "time": 0.026 }, - { "prover": "cvc5@1.0.5", "time": 0.06 }, - { "prover": "cvc5@1.0.5", "time": 0.012 }, - { "prover": "cvc5@1.0.5", "time": 0.056 }, - { "prover": "cvc5@1.0.5", "time": 0.056 }, - { "prover": "cvc5@1.0.5", "time": 0.023 }, - { "prover": "cvc5@1.0.5", "time": 0.06 }, - { "prover": "cvc5@1.0.5", "time": 0.059 }, - { "prover": "cvc5@1.0.5", "time": 0.021 }, - { "prover": "cvc5@1.0.5", "time": 0.052 }, - { "prover": "cvc5@1.0.5", "time": 0.061 }, + { "prover": "cvc5@1.0.5", "time": 0.022 }, + { "prover": "cvc5@1.0.5", "time": 0.026 }, + { "prover": "cvc5@1.0.5", "time": 0.013 }, + { "prover": "cvc5@1.0.5", "time": 0.028 }, { "prover": "cvc5@1.0.5", "time": 0.031 }, - { "prover": "cvc5@1.0.5", "time": 0.066 }, - { "prover": "cvc5@1.0.5", "time": 0.038 }, - { "prover": "z3@4.12.4", "time": 0.073 }, - { "prover": "cvc5@1.0.5", "time": 0.051 }, - { "prover": "cvc5@1.0.5", "time": 0.046 }, - { "prover": "z3@4.12.4", "time": 0.01 }, - { "prover": "cvc5@1.0.5", "time": 0.012 }, - { "prover": "cvc5@1.0.5", "time": 0.009 }, - { "prover": "cvc5@1.0.5", "time": 0.027 }, - { "prover": "cvc5@1.0.5", "time": 0.024 }, - { "prover": "cvc5@1.0.5", "time": 0.024 }, - { "prover": "cvc5@1.0.5", "time": 0.05 }, - { "prover": "cvc5@1.0.5", "time": 0.015 }, - { "prover": "cvc5@1.0.5", "time": 0.055 }, - { "prover": "cvc5@1.0.5", "time": 0.063 }, + { "prover": "cvc5@1.0.5", "time": 0.032 }, { "prover": "cvc5@1.0.5", "time": 0.033 }, - { "prover": "cvc5@1.0.5", "time": 0.011 }, - { "prover": "cvc5@1.0.5", "time": 0.092 }, - { "prover": "cvc5@1.0.5", "time": 0.105 } + { "prover": "cvc5@1.0.5", "time": 0.056 }, + { "prover": "z3@4.12.4", "time": 0.031 }, + { "prover": "cvc5@1.0.5", "time": 0.045 }, + { "prover": "cvc5@1.0.5", "time": 0.041 }, + { "prover": "z3@4.12.4", "time": 0.028 }, + { "prover": "cvc5@1.0.5", "time": 0.048 }, + { "prover": "cvc5@1.0.5", "time": 0.028 }, + { "prover": "cvc5@1.0.5", "time": 0.043 }, + { "prover": "z3@4.12.4", "time": 0.031 }, + { "prover": "cvc5@1.0.5", "time": 0.025 }, + { "prover": "z3@4.12.4", "time": 0.044 } ] }, "vc_push_back_ghost'0": { "prover": "cvc5@1.0.5", "time": 0.012 }, "vc_unwrap'0": { "prover": "cvc5@1.0.5", "time": 0.012 } }, "M_linked_list__qyi10858349784728989480__push_front": { - "vc_borrow_mut'0": { "prover": "cvc5@1.0.5", "time": 0.011 }, "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_is_null'0": { "prover": "cvc5@1.0.5", "time": 0.009 },