From 27c38afcdf3aacc48bdf1cafce748d11a6adf275 Mon Sep 17 00:00:00 2001
From: dewert99 <dewert10@gmail.com>
Date: Sat, 3 Aug 2024 10:59:19 -0700
Subject: [PATCH] Fix spec that `GhostPtrToken`'s don't contain null pointers
 to apply to `Ref` and `Mut` variants

---
 creusot-contracts/src/ghost_ptr.rs            |   5 +-
 creusot/tests/should_succeed/bug/949.coma     |  99 +++++---
 .../tests/should_succeed/ghost_ptr_token.coma | 239 ++++++++++--------
 .../ghost_ptr_token/why3session.xml           |  66 ++++-
 .../ghost_ptr_token/why3shapes.gz             | Bin 557 -> 857 bytes
 5 files changed, 264 insertions(+), 145 deletions(-)

diff --git a/creusot-contracts/src/ghost_ptr.rs b/creusot-contracts/src/ghost_ptr.rs
index 69278b30f1..ff1e2bc562 100644
--- a/creusot-contracts/src/ghost_ptr.rs
+++ b/creusot-contracts/src/ghost_ptr.rs
@@ -29,6 +29,7 @@ impl<T: ?Sized> ShallowModel for GhostPtrToken<T> {
 
     #[trusted]
     #[logic]
+    #[ensures(result.get(GhostPtr::null_logic()) == None)]
     #[open(self)]
     fn shallow_model(self) -> Self::ShallowModelTy {
         absurd
@@ -132,7 +133,6 @@ impl<T: ?Sized> GhostPtrExt<T> for GhostPtr<T> {
     #[trusted]
     #[open(self)]
     #[logic]
-    #[ensures(forall<t: GhostPtrToken<T>> !t@.contains(result))]
     #[ensures(result.addr_logic() == 0)]
     #[ensures(forall<ptr: GhostPtr<T>> ptr.addr_logic() == result.addr_logic() ==> ptr == result)]
     fn null_logic() -> Self {
@@ -153,6 +153,7 @@ impl<'a, T: ?Sized> ShallowModel for GhostPtrTokenRef<'a, T> {
     #[trusted]
     #[logic]
     #[open(self)]
+    #[ensures(result.get(GhostPtr::null_logic()) == None)]
     fn shallow_model(self) -> Self::ShallowModelTy {
         absurd
     }
@@ -197,6 +198,7 @@ impl<'a, T: ?Sized> GhostPtrTokenMut<'a, T> {
     #[trusted]
     #[logic]
     #[open(self)]
+    #[ensures(result.get(GhostPtr::null_logic()) == None)]
     pub fn cur(self) -> FMap<GhostPtr<T>, T> {
         absurd
     }
@@ -204,6 +206,7 @@ impl<'a, T: ?Sized> GhostPtrTokenMut<'a, T> {
     #[trusted]
     #[logic(prophetic)]
     #[open(self)]
+    #[ensures(result.get(GhostPtr::null_logic()) == None)]
     pub fn fin(self) -> FMap<GhostPtr<T>, T> {
         absurd
     }
diff --git a/creusot/tests/should_succeed/bug/949.coma b/creusot/tests/should_succeed/bug/949.coma
index 6d092f99f4..00ff3f0221 100644
--- a/creusot/tests/should_succeed/bug/949.coma
+++ b/creusot/tests/should_succeed/bug/949.coma
@@ -127,47 +127,55 @@ module C949_Main
   
   let%span span26 = "../../../../../creusot-contracts/src/logic/fmap.rs" 62 8 62 27
   
-  let%span span27 = "../../../../../creusot-contracts/src/ghost_ptr.rs" 96 4 96 39
+  let%span span27 = "../../../../../creusot-contracts/src/ghost_ptr.rs" 136 14 136 38
   
-  let%span span28 = "../../../../../creusot-contracts/src/ghost_ptr.rs" 97 14 97 54
+  let%span span28 = "../../../../../creusot-contracts/src/ghost_ptr.rs" 137 4 137 98
   
-  let%span span29 = "../../../../../creusot-contracts/src/ghost_ptr.rs" 98 14 98 46
+  let%span span29 = "../../../../../creusot-contracts/src/ghost_ptr.rs" 32 14 32 56
   
-  let%span span30 = "../../../../../creusot-contracts/src/ghost_ptr.rs" 99 4 99 57
+  let%span span30 = "../../../../../creusot-contracts/src/ghost_ptr.rs" 34 4 34 50
   
-  let%span span31 = "../../../../../creusot-contracts/src/util.rs" 16 19 16 23
+  let%span span31 = "../../../../../creusot-contracts/src/ghost_ptr.rs" 97 4 97 39
   
-  let%span span32 = "../../../../../creusot-contracts/src/util.rs" 15 14 15 30
+  let%span span32 = "../../../../../creusot-contracts/src/ghost_ptr.rs" 98 14 98 54
   
-  let%span span33 = "../../../../../creusot-contracts/src/util.rs" 16 4 16 40
+  let%span span33 = "../../../../../creusot-contracts/src/ghost_ptr.rs" 99 14 99 46
   
-  let%span span34 = "../../../../../creusot-contracts/src/logic/fmap.rs" 38 18 38 22
+  let%span span34 = "../../../../../creusot-contracts/src/ghost_ptr.rs" 100 4 100 57
   
-  let%span span35 = "../../../../../creusot-contracts/src/logic/fmap.rs" 38 24 38 25
+  let%span span35 = "../../../../../creusot-contracts/src/util.rs" 16 19 16 23
   
-  let%span span36 = "../../../../../creusot-contracts/src/logic/fmap.rs" 38 30 38 31
+  let%span span36 = "../../../../../creusot-contracts/src/util.rs" 15 14 15 30
   
-  let%span span37 = "../../../../../creusot-contracts/src/logic/fmap.rs" 35 14 35 71
+  let%span span37 = "../../../../../creusot-contracts/src/util.rs" 16 4 16 40
   
-  let%span span38 = "../../../../../creusot-contracts/src/logic/fmap.rs" 36 4 36 63
+  let%span span38 = "../../../../../creusot-contracts/src/logic/fmap.rs" 38 18 38 22
   
-  let%span span39 = "../../../../../creusot-contracts/src/logic/fmap.rs" 37 4 37 68
+  let%span span39 = "../../../../../creusot-contracts/src/logic/fmap.rs" 38 24 38 25
   
-  let%span span40 = "../../../../../creusot-contracts/src/logic/fmap.rs" 38 4 38 43
+  let%span span40 = "../../../../../creusot-contracts/src/logic/fmap.rs" 38 30 38 31
   
-  let%span span41 = "../../../../../creusot-contracts/src/ghost_ptr.rs" 70 35 70 38
+  let%span span41 = "../../../../../creusot-contracts/src/logic/fmap.rs" 35 14 35 71
   
-  let%span span42 = "../../../../../creusot-contracts/src/ghost_ptr.rs" 66 4 66 42
+  let%span span42 = "../../../../../creusot-contracts/src/logic/fmap.rs" 36 4 36 63
   
-  let%span span43 = "../../../../../creusot-contracts/src/ghost_ptr.rs" 69 14 69 55
+  let%span span43 = "../../../../../creusot-contracts/src/logic/fmap.rs" 37 4 37 68
   
-  let%span span44 = "../../../../../creusot-contracts/src/logic/fmap.rs" 85 14 85 31
+  let%span span44 = "../../../../../creusot-contracts/src/logic/fmap.rs" 38 4 38 43
   
-  let%span span45 = "../../../../../creusot-contracts/src/logic/fmap.rs" 86 14 86 49
+  let%span span45 = "../../../../../creusot-contracts/src/ghost_ptr.rs" 71 35 71 38
   
-  let%span span46 = "../../../../../creusot-contracts/src/logic/fmap.rs" 87 4 87 26
+  let%span span46 = "../../../../../creusot-contracts/src/ghost_ptr.rs" 67 4 67 42
   
-  let%span span47 = "../../../../../creusot-contracts/src/ghost_ptr.rs" 40 14 40 38
+  let%span span47 = "../../../../../creusot-contracts/src/ghost_ptr.rs" 70 14 70 55
+  
+  let%span span48 = "../../../../../creusot-contracts/src/logic/fmap.rs" 85 14 85 31
+  
+  let%span span49 = "../../../../../creusot-contracts/src/logic/fmap.rs" 86 14 86 49
+  
+  let%span span50 = "../../../../../creusot-contracts/src/logic/fmap.rs" 87 4 87 26
+  
+  let%span span51 = "../../../../../creusot-contracts/src/ghost_ptr.rs" 41 14 41 38
   
   use prelude.prelude.Int32
   
@@ -283,39 +291,50 @@ module C949_Main
   function lookup_unsized'0 [@inline:trivial] (self : FMap'0.t_fmap opaque_ptr int32) (k : opaque_ptr) : int32 =
     [%#span26] unwrap'0 (get'0 self k)
   
+  function addr_logic'0 (self : opaque_ptr) : int
+  
+  function null_logic'0 (_1 : ()) : opaque_ptr
+  
+  axiom null_logic'0_spec : forall _1 : () . ([%#span28] forall ptr : opaque_ptr . addr_logic'0 ptr
+  = addr_logic'0 (null_logic'0 _1)  -> ptr = null_logic'0 _1)
+  && ([%#span27] addr_logic'0 (null_logic'0 _1) = 0)
+  
   function shallow_model'0 (self : GhostPtrToken'0.t_ghostptrtoken int32) : FMap'0.t_fmap opaque_ptr int32
   
+  axiom shallow_model'0_spec : forall self : GhostPtrToken'0.t_ghostptrtoken int32 . ([%#span30] inv'1 (shallow_model'0 self))
+  && ([%#span29] get'0 (shallow_model'0 self) (null_logic'0 ()) = Option'0.C_None)
+  
   use prelude.prelude.Borrow
   
-  let rec ptr_to_box'0 (self:borrowed (GhostPtrToken'0.t_ghostptrtoken int32)) (ptr:opaque_ptr) (return'  (ret:int32))= {[@expl:precondition] [%#span27] contains'0 (shallow_model'0 self.current) ptr}
+  let rec ptr_to_box'0 (self:borrowed (GhostPtrToken'0.t_ghostptrtoken int32)) (ptr:opaque_ptr) (return'  (ret:int32))= {[@expl:precondition] [%#span31] contains'0 (shallow_model'0 self.current) ptr}
     any
-    [ return' (result:int32)-> {[%#span30] inv'0 result}
-      {[%#span29] shallow_model'0 self.final = remove'0 (shallow_model'0 self.current) ptr}
-      {[%#span28] result = lookup_unsized'0 (shallow_model'0 self.current) ptr}
+    [ return' (result:int32)-> {[%#span34] inv'0 result}
+      {[%#span33] shallow_model'0 self.final = remove'0 (shallow_model'0 self.current) ptr}
+      {[%#span32] result = lookup_unsized'0 (shallow_model'0 self.current) ptr}
       (! return' {result}) ]
     
   
   function make_sized'0 (self : int32) : int32
   
-  axiom make_sized'0_spec : forall self : int32 . ([%#span31] inv'5 self)
-   -> ([%#span33] inv'0 (make_sized'0 self)) && ([%#span32] make_sized'0 self = self)
+  axiom make_sized'0_spec : forall self : int32 . ([%#span35] inv'5 self)
+   -> ([%#span37] inv'0 (make_sized'0 self)) && ([%#span36] make_sized'0 self = self)
   
   function insert'0 (self : FMap'0.t_fmap opaque_ptr int32) (k : opaque_ptr) (v : int32) : FMap'0.t_fmap opaque_ptr int32
     
   
-  axiom insert'0_spec : forall self : FMap'0.t_fmap opaque_ptr int32, k : opaque_ptr, v : int32 . ([%#span34] inv'1 self)
-   -> ([%#span35] inv'2 k)
-   -> ([%#span36] inv'3 v)
-   -> ([%#span40] inv'1 (insert'0 self k v))
-  && ([%#span39] not contains'0 self k  -> len'0 (insert'0 self k v) = len'0 self + 1)
-  && ([%#span38] contains'0 self k  -> len'0 (insert'0 self k v) = len'0 self)
-  && ([%#span37] view'0 (insert'0 self k v) = Map.set (view'0 self) k (Option'0.C_Some (make_sized'0 v)))
+  axiom insert'0_spec : forall self : FMap'0.t_fmap opaque_ptr int32, k : opaque_ptr, v : int32 . ([%#span38] inv'1 self)
+   -> ([%#span39] inv'2 k)
+   -> ([%#span40] inv'3 v)
+   -> ([%#span44] inv'1 (insert'0 self k v))
+  && ([%#span43] not contains'0 self k  -> len'0 (insert'0 self k v) = len'0 self + 1)
+  && ([%#span42] contains'0 self k  -> len'0 (insert'0 self k v) = len'0 self)
+  && ([%#span41] view'0 (insert'0 self k v) = Map.set (view'0 self) k (Option'0.C_Some (make_sized'0 v)))
   
-  let rec ptr_from_box'0 (self:borrowed (GhostPtrToken'0.t_ghostptrtoken int32)) (val':int32) (return'  (ret:opaque_ptr))= {[@expl:precondition] [%#span41] inv'0 val'}
+  let rec ptr_from_box'0 (self:borrowed (GhostPtrToken'0.t_ghostptrtoken int32)) (val':int32) (return'  (ret:opaque_ptr))= {[@expl:precondition] [%#span45] inv'0 val'}
     any
-    [ return' (result:opaque_ptr)-> {[%#span43] shallow_model'0 self.final
+    [ return' (result:opaque_ptr)-> {[%#span47] shallow_model'0 self.final
       = insert'0 (shallow_model'0 self.current) result val'}
-      {[%#span42] not contains'0 (shallow_model'0 self.current) result}
+      {[%#span46] not contains'0 (shallow_model'0 self.current) result}
       (! return' {result}) ]
     
   
@@ -323,11 +342,11 @@ module C949_Main
   
   function empty'0 (_1 : ()) : FMap'0.t_fmap opaque_ptr int32
   
-  axiom empty'0_spec : forall _1 : () . ([%#span46] inv'1 (empty'0 _1))
-  && ([%#span45] view'0 (empty'0 _1) = Const.const (Option'0.C_None)) && ([%#span44] len'0 (empty'0 _1) = 0)
+  axiom empty'0_spec : forall _1 : () . ([%#span50] inv'1 (empty'0 _1))
+  && ([%#span49] view'0 (empty'0 _1) = Const.const (Option'0.C_None)) && ([%#span48] len'0 (empty'0 _1) = 0)
   
   let rec new'0 (_1:()) (return'  (ret:GhostPtrToken'0.t_ghostptrtoken int32))= any
-    [ return' (result:GhostPtrToken'0.t_ghostptrtoken int32)-> {[%#span47] shallow_model'0 result = empty'0 ()}
+    [ return' (result:GhostPtrToken'0.t_ghostptrtoken int32)-> {[%#span51] shallow_model'0 result = empty'0 ()}
       (! return' {result}) ]
     
   
diff --git a/creusot/tests/should_succeed/ghost_ptr_token.coma b/creusot/tests/should_succeed/ghost_ptr_token.coma
index 9fecd25a1b..6b5463622f 100644
--- a/creusot/tests/should_succeed/ghost_ptr_token.coma
+++ b/creusot/tests/should_succeed/ghost_ptr_token.coma
@@ -8,6 +8,22 @@ end
 module CreusotContracts_Logic_Fmap_FMap_Type
   type t_fmap 'k 'v
 end
+module Core_Option_Option_Type
+  type t_option 't =
+    | C_None
+    | C_Some 't
+  
+  function any_l (_ : 'b) : 'a
+  
+  let rec none < 't > (input:t_option 't) (ret  )= any
+    [ good -> {C_None  = input} (! ret) | bad -> {C_None  <> input} {false} any ]
+    
+  
+  let rec some < 't > (input:t_option 't) (ret  (field_0:'t))= any
+    [ good (field_0:'t)-> {C_Some field_0 = input} (! ret {field_0})
+    | bad (field_0:'t)-> {C_Some field_0 <> input} {false} any ]
+    
+end
 module Core_Panicking_AssertKind_Type
   type t_assertkind  =
     | C_Eq
@@ -27,22 +43,6 @@ module Core_Panicking_AssertKind_Type
   let rec match' (input:t_assertkind) (ret  )= any
     [ good -> {C_Match  = input} (! ret) | bad -> {C_Match  <> input} {false} any ]
     
-end
-module Core_Option_Option_Type
-  type t_option 't =
-    | C_None
-    | C_Some 't
-  
-  function any_l (_ : 'b) : 'a
-  
-  let rec none < 't > (input:t_option 't) (ret  )= any
-    [ good -> {C_None  = input} (! ret) | bad -> {C_None  <> input} {false} any ]
-    
-  
-  let rec some < 't > (input:t_option 't) (ret  (field_0:'t))= any
-    [ good (field_0:'t)-> {C_Some field_0 = input} (! ret {field_0})
-    | bad (field_0:'t)-> {C_Some field_0 <> input} {false} any ]
-    
 end
 module Core_Ptr_NonNull_NonNull_Type
   use prelude.prelude.Opaque
@@ -148,93 +148,109 @@ module GhostPtrToken_Test
   
   let%span span25 = "../../../../creusot-contracts/src/logic/fmap.rs" 79 8 79 27
   
-  let%span span26 = "../../../../creusot-contracts/src/model.rs" 90 8 90 31
+  let%span span26 = "../../../../creusot-contracts/src/ghost_ptr.rs" 136 14 136 38
+  
+  let%span span27 = "../../../../creusot-contracts/src/ghost_ptr.rs" 137 4 137 98
+  
+  let%span span28 = "../../../../creusot-contracts/src/ghost_ptr.rs" 32 14 32 56
+  
+  let%span span29 = "../../../../creusot-contracts/src/ghost_ptr.rs" 34 4 34 50
+  
+  let%span span30 = "../../../../creusot-contracts/src/model.rs" 90 8 90 31
+  
+  let%span span31 = "../../../../creusot-contracts/src/ghost_ptr.rs" 80 4 80 36
+  
+  let%span span32 = "../../../../creusot-contracts/src/ghost_ptr.rs" 81 14 81 51
   
-  let%span span27 = "../../../../creusot-contracts/src/ghost_ptr.rs" 79 4 79 36
+  let%span span33 = "../../../../creusot-contracts/src/ghost_ptr.rs" 82 4 82 49
   
-  let%span span28 = "../../../../creusot-contracts/src/ghost_ptr.rs" 80 14 80 51
+  let%span span34 = "../../../../creusot-contracts/src/resolve.rs" 26 20 26 34
   
-  let%span span29 = "../../../../creusot-contracts/src/ghost_ptr.rs" 81 4 81 49
+  let%span span35 = "" 0 0 0 0
   
-  let%span span30 = "../../../../creusot-contracts/src/resolve.rs" 26 20 26 34
+  let%span span36 = "" 0 0 0 0
   
-  let%span span31 = "" 0 0 0 0
+  let%span span37 = "../../../../creusot-contracts/src/std/mem.rs" 13 22 13 30
   
-  let%span span32 = "" 0 0 0 0
+  let%span span38 = "../../../../creusot-contracts/src/std/mem.rs" 14 22 14 30
   
-  let%span span33 = "../../../../creusot-contracts/src/std/mem.rs" 13 22 13 30
+  let%span span39 = "../../../../creusot-contracts/src/resolve.rs" 46 8 46 12
   
-  let%span span34 = "../../../../creusot-contracts/src/std/mem.rs" 14 22 14 30
+  let%span span40 = "../../../../creusot-contracts/src/resolve.rs" 17 8 17 60
   
-  let%span span35 = "../../../../creusot-contracts/src/resolve.rs" 46 8 46 12
+  let%span span41 = "../../../../creusot-contracts/src/ghost_ptr.rs" 209 14 209 56
   
-  let%span span36 = "../../../../creusot-contracts/src/resolve.rs" 17 8 17 60
+  let%span span42 = "../../../../creusot-contracts/src/ghost_ptr.rs" 210 4 210 44
   
-  let%span span37 = "../../../../creusot-contracts/src/ghost_ptr.rs" 277 8 277 32
+  let%span span43 = "../../../../creusot-contracts/src/ghost_ptr.rs" 201 14 201 56
   
-  let%span span38 = "../../../../creusot-contracts/src/logic/fmap.rs" 13 15 13 19
+  let%span span44 = "../../../../creusot-contracts/src/ghost_ptr.rs" 202 4 202 44
   
-  let%span span39 = "../../../../creusot-contracts/src/logic/fmap.rs" 12 14 12 25
+  let%span span45 = "../../../../creusot-contracts/src/ghost_ptr.rs" 280 8 280 32
   
-  let%span span40 = "../../../../creusot-contracts/src/util.rs" 16 19 16 23
+  let%span span46 = "../../../../creusot-contracts/src/logic/fmap.rs" 13 15 13 19
   
-  let%span span41 = "../../../../creusot-contracts/src/util.rs" 15 14 15 30
+  let%span span47 = "../../../../creusot-contracts/src/logic/fmap.rs" 12 14 12 25
   
-  let%span span42 = "../../../../creusot-contracts/src/util.rs" 16 4 16 40
+  let%span span48 = "../../../../creusot-contracts/src/util.rs" 16 19 16 23
   
-  let%span span43 = "../../../../creusot-contracts/src/logic/fmap.rs" 38 18 38 22
+  let%span span49 = "../../../../creusot-contracts/src/util.rs" 15 14 15 30
   
-  let%span span44 = "../../../../creusot-contracts/src/logic/fmap.rs" 38 24 38 25
+  let%span span50 = "../../../../creusot-contracts/src/util.rs" 16 4 16 40
   
-  let%span span45 = "../../../../creusot-contracts/src/logic/fmap.rs" 38 30 38 31
+  let%span span51 = "../../../../creusot-contracts/src/logic/fmap.rs" 38 18 38 22
   
-  let%span span46 = "../../../../creusot-contracts/src/logic/fmap.rs" 35 14 35 71
+  let%span span52 = "../../../../creusot-contracts/src/logic/fmap.rs" 38 24 38 25
   
-  let%span span47 = "../../../../creusot-contracts/src/logic/fmap.rs" 36 4 36 63
+  let%span span53 = "../../../../creusot-contracts/src/logic/fmap.rs" 38 30 38 31
   
-  let%span span48 = "../../../../creusot-contracts/src/logic/fmap.rs" 37 4 37 68
+  let%span span54 = "../../../../creusot-contracts/src/logic/fmap.rs" 35 14 35 71
   
-  let%span span49 = "../../../../creusot-contracts/src/logic/fmap.rs" 38 4 38 43
+  let%span span55 = "../../../../creusot-contracts/src/logic/fmap.rs" 36 4 36 63
   
-  let%span span50 = "../../../../creusot-contracts/src/logic/fmap.rs" 47 18 47 22
+  let%span span56 = "../../../../creusot-contracts/src/logic/fmap.rs" 37 4 37 68
   
-  let%span span51 = "../../../../creusot-contracts/src/logic/fmap.rs" 47 24 47 25
+  let%span span57 = "../../../../creusot-contracts/src/logic/fmap.rs" 38 4 38 43
   
-  let%span span52 = "../../../../creusot-contracts/src/logic/fmap.rs" 45 14 45 55
+  let%span span58 = "../../../../creusot-contracts/src/logic/fmap.rs" 47 18 47 22
   
-  let%span span53 = "../../../../creusot-contracts/src/logic/fmap.rs" 46 14 46 84
+  let%span span59 = "../../../../creusot-contracts/src/logic/fmap.rs" 47 24 47 25
   
-  let%span span54 = "../../../../creusot-contracts/src/logic/fmap.rs" 47 4 47 37
+  let%span span60 = "../../../../creusot-contracts/src/logic/fmap.rs" 45 14 45 55
   
-  let%span span55 = "../../../../creusot-contracts/src/ghost_ptr.rs" 243 15 243 42
+  let%span span61 = "../../../../creusot-contracts/src/logic/fmap.rs" 46 14 46 84
   
-  let%span span56 = "../../../../creusot-contracts/src/ghost_ptr.rs" 244 14 244 59
+  let%span span62 = "../../../../creusot-contracts/src/logic/fmap.rs" 47 4 47 37
   
-  let%span span57 = "../../../../creusot-contracts/src/ghost_ptr.rs" 245 14 245 56
+  let%span span63 = "../../../../creusot-contracts/src/ghost_ptr.rs" 246 15 246 42
   
-  let%span span58 = "../../../../creusot-contracts/src/ghost_ptr.rs" 246 14 246 65
+  let%span span64 = "../../../../creusot-contracts/src/ghost_ptr.rs" 247 14 247 59
   
-  let%span span59 = "../../../../creusot-contracts/src/ghost_ptr.rs" 247 14 247 42
+  let%span span65 = "../../../../creusot-contracts/src/ghost_ptr.rs" 248 14 248 56
   
-  let%span span60 = "../../../../creusot-contracts/src/ghost_ptr.rs" 248 4 248 58
+  let%span span66 = "../../../../creusot-contracts/src/ghost_ptr.rs" 249 14 249 65
   
-  let%span span61 = "../../../../creusot-contracts/src/ghost_ptr.rs" 124 14 124 38
+  let%span span67 = "../../../../creusot-contracts/src/ghost_ptr.rs" 250 14 250 42
   
-  let%span span62 = "../../../../creusot-contracts/src/ghost_ptr.rs" 125 14 125 38
+  let%span span68 = "../../../../creusot-contracts/src/ghost_ptr.rs" 251 4 251 58
   
-  let%span span63 = "../../../../creusot-contracts/src/ghost_ptr.rs" 70 35 70 38
+  let%span span69 = "../../../../creusot-contracts/src/ghost_ptr.rs" 125 14 125 38
   
-  let%span span64 = "../../../../creusot-contracts/src/ghost_ptr.rs" 66 4 66 42
+  let%span span70 = "../../../../creusot-contracts/src/ghost_ptr.rs" 126 14 126 38
   
-  let%span span65 = "../../../../creusot-contracts/src/ghost_ptr.rs" 69 14 69 55
+  let%span span71 = "../../../../creusot-contracts/src/ghost_ptr.rs" 71 35 71 38
   
-  let%span span66 = "../../../../creusot-contracts/src/logic/fmap.rs" 85 14 85 31
+  let%span span72 = "../../../../creusot-contracts/src/ghost_ptr.rs" 67 4 67 42
   
-  let%span span67 = "../../../../creusot-contracts/src/logic/fmap.rs" 86 14 86 49
+  let%span span73 = "../../../../creusot-contracts/src/ghost_ptr.rs" 70 14 70 55
   
-  let%span span68 = "../../../../creusot-contracts/src/logic/fmap.rs" 87 4 87 26
+  let%span span74 = "../../../../creusot-contracts/src/logic/fmap.rs" 85 14 85 31
   
-  let%span span69 = "../../../../creusot-contracts/src/ghost_ptr.rs" 40 14 40 38
+  let%span span75 = "../../../../creusot-contracts/src/logic/fmap.rs" 86 14 86 49
+  
+  let%span span76 = "../../../../creusot-contracts/src/logic/fmap.rs" 87 4 87 26
+  
+  let%span span77 = "../../../../creusot-contracts/src/ghost_ptr.rs" 41 14 41 38
   
   use prelude.prelude.Int32
   
@@ -338,97 +354,114 @@ module GhostPtrToken_Test
   function contains'0 [@inline:trivial] (self : FMap'0.t_fmap opaque_ptr int32) (k : opaque_ptr) : bool =
     [%#span25] get'0 self k <> Option'0.C_None
   
+  use prelude.prelude.Int
+  
+  function addr_logic'0 (self : opaque_ptr) : int
+  
+  function null_logic'0 (_1 : ()) : opaque_ptr
+  
+  axiom null_logic'0_spec : forall _1 : () . ([%#span27] forall ptr : opaque_ptr . addr_logic'0 ptr
+  = addr_logic'0 (null_logic'0 _1)  -> ptr = null_logic'0 _1)
+  && ([%#span26] addr_logic'0 (null_logic'0 _1) = 0)
+  
   function shallow_model'0 (self : GhostPtrToken'0.t_ghostptrtoken int32) : FMap'0.t_fmap opaque_ptr int32
   
+  axiom shallow_model'0_spec : forall self : GhostPtrToken'0.t_ghostptrtoken int32 . ([%#span29] inv'3 (shallow_model'0 self))
+  && ([%#span28] get'0 (shallow_model'0 self) (null_logic'0 ()) = Option'0.C_None)
+  
   function shallow_model'1 (self : GhostPtrToken'0.t_ghostptrtoken int32) : FMap'0.t_fmap opaque_ptr int32 =
-    [%#span26] shallow_model'0 self
+    [%#span30] shallow_model'0 self
   
-  let rec ptr_as_ref'0 (self:GhostPtrToken'0.t_ghostptrtoken int32) (ptr:opaque_ptr) (return'  (ret:int32))= {[@expl:precondition] [%#span27] contains'0 (shallow_model'1 self) ptr}
+  let rec ptr_as_ref'0 (self:GhostPtrToken'0.t_ghostptrtoken int32) (ptr:opaque_ptr) (return'  (ret:int32))= {[@expl:precondition] [%#span31] contains'0 (shallow_model'1 self) ptr}
     any
-    [ return' (result:int32)-> {[%#span29] inv'2 result}
-      {[%#span28] result = lookup_unsized'0 (shallow_model'1 self) ptr}
+    [ return' (result:int32)-> {[%#span33] inv'2 result}
+      {[%#span32] result = lookup_unsized'0 (shallow_model'1 self) ptr}
       (! return' {result}) ]
     
   
   predicate resolve'2 (self : borrowed int32) =
-    [%#span30] self.final = self.current
+    [%#span34] self.final = self.current
   
-  let rec swap'0 (x:borrowed int32) (y:borrowed int32) (return'  (ret:()))= {[@expl:precondition] [%#span32] inv'1 y}
-    {[@expl:precondition] [%#span31] inv'1 x}
+  let rec swap'0 (x:borrowed int32) (y:borrowed int32) (return'  (ret:()))= {[@expl:precondition] [%#span36] inv'1 y}
+    {[@expl:precondition] [%#span35] inv'1 x}
     any
-    [ return' (result:())-> {[%#span34] y.final = x.current} {[%#span33] x.final = y.current} (! return' {result}) ]
+    [ return' (result:())-> {[%#span38] y.final = x.current} {[%#span37] x.final = y.current} (! return' {result}) ]
     
   
   predicate resolve'3 (self : int32) =
-    [%#span35] true
+    [%#span39] true
   
   predicate resolve'1 (self : (int32, int32)) =
-    [%#span36] resolve'3 (let (a, _) = self in a) /\ resolve'3 (let (_, a) = self in a)
+    [%#span40] resolve'3 (let (a, _) = self in a) /\ resolve'3 (let (_, a) = self in a)
   
   use CreusotContracts_GhostPtr_GhostPtrTokenMut_Type as GhostPtrTokenMut'0
   
   function fin'0 (self : GhostPtrTokenMut'0.t_ghostptrtokenmut int32) : FMap'0.t_fmap opaque_ptr int32
   
+  axiom fin'0_spec : forall self : GhostPtrTokenMut'0.t_ghostptrtokenmut int32 . ([%#span42] inv'3 (fin'0 self))
+  && ([%#span41] get'0 (fin'0 self) (null_logic'0 ()) = Option'0.C_None)
+  
   function cur'0 (self : GhostPtrTokenMut'0.t_ghostptrtokenmut int32) : FMap'0.t_fmap opaque_ptr int32
   
-  predicate resolve'0 (self : GhostPtrTokenMut'0.t_ghostptrtokenmut int32) =
-    [%#span37] cur'0 self = fin'0 self
+  axiom cur'0_spec : forall self : GhostPtrTokenMut'0.t_ghostptrtokenmut int32 . ([%#span44] inv'3 (cur'0 self))
+  && ([%#span43] get'0 (cur'0 self) (null_logic'0 ()) = Option'0.C_None)
   
-  use prelude.prelude.Int
+  predicate resolve'0 (self : GhostPtrTokenMut'0.t_ghostptrtokenmut int32) =
+    [%#span45] cur'0 self = fin'0 self
   
   function len'0 (self : FMap'0.t_fmap opaque_ptr int32) : int
   
-  axiom len'0_spec : forall self : FMap'0.t_fmap opaque_ptr int32 . ([%#span38] inv'3 self)
-   -> ([%#span39] len'0 self >= 0)
+  axiom len'0_spec : forall self : FMap'0.t_fmap opaque_ptr int32 . ([%#span46] inv'3 self)
+   -> ([%#span47] len'0 self >= 0)
   
   use map.Map
   
   function make_sized'0 (self : int32) : int32
   
-  axiom make_sized'0_spec : forall self : int32 . ([%#span40] inv'2 self)
-   -> ([%#span42] inv'0 (make_sized'0 self)) && ([%#span41] make_sized'0 self = self)
+  axiom make_sized'0_spec : forall self : int32 . ([%#span48] inv'2 self)
+   -> ([%#span50] inv'0 (make_sized'0 self)) && ([%#span49] make_sized'0 self = self)
   
   function insert'0 (self : FMap'0.t_fmap opaque_ptr int32) (k : opaque_ptr) (v : int32) : FMap'0.t_fmap opaque_ptr int32
     
   
-  axiom insert'0_spec : forall self : FMap'0.t_fmap opaque_ptr int32, k : opaque_ptr, v : int32 . ([%#span43] inv'3 self)
-   -> ([%#span44] inv'4 k)
-   -> ([%#span45] inv'5 v)
-   -> ([%#span49] inv'3 (insert'0 self k v))
-  && ([%#span48] not contains'0 self k  -> len'0 (insert'0 self k v) = len'0 self + 1)
-  && ([%#span47] contains'0 self k  -> len'0 (insert'0 self k v) = len'0 self)
-  && ([%#span46] view'0 (insert'0 self k v) = Map.set (view'0 self) k (Option'0.C_Some (make_sized'0 v)))
+  axiom insert'0_spec : forall self : FMap'0.t_fmap opaque_ptr int32, k : opaque_ptr, v : int32 . ([%#span51] inv'3 self)
+   -> ([%#span52] inv'4 k)
+   -> ([%#span53] inv'5 v)
+   -> ([%#span57] inv'3 (insert'0 self k v))
+  && ([%#span56] not contains'0 self k  -> len'0 (insert'0 self k v) = len'0 self + 1)
+  && ([%#span55] contains'0 self k  -> len'0 (insert'0 self k v) = len'0 self)
+  && ([%#span54] view'0 (insert'0 self k v) = Map.set (view'0 self) k (Option'0.C_Some (make_sized'0 v)))
   
   function remove'0 (self : FMap'0.t_fmap opaque_ptr int32) (k : opaque_ptr) : FMap'0.t_fmap opaque_ptr int32
   
-  axiom remove'0_spec : forall self : FMap'0.t_fmap opaque_ptr int32, k : opaque_ptr . ([%#span50] inv'3 self)
-   -> ([%#span51] inv'4 k)
-   -> ([%#span54] inv'3 (remove'0 self k))
-  && ([%#span53] len'0 (remove'0 self k) = (if contains'0 self k then len'0 self - 1 else len'0 self))
-  && ([%#span52] view'0 (remove'0 self k) = Map.set (view'0 self) k (Option'0.C_None))
+  axiom remove'0_spec : forall self : FMap'0.t_fmap opaque_ptr int32, k : opaque_ptr . ([%#span58] inv'3 self)
+   -> ([%#span59] inv'4 k)
+   -> ([%#span62] inv'3 (remove'0 self k))
+  && ([%#span61] len'0 (remove'0 self k) = (if contains'0 self k then len'0 self - 1 else len'0 self))
+  && ([%#span60] view'0 (remove'0 self k) = Map.set (view'0 self) k (Option'0.C_None))
   
-  let rec take_mut'0 (self:borrowed (GhostPtrTokenMut'0.t_ghostptrtokenmut int32)) (ptr:opaque_ptr) (return'  (ret:borrowed int32))= {[@expl:precondition] [%#span55] contains'0 (cur'0 self.current) ptr}
+  let rec take_mut'0 (self:borrowed (GhostPtrTokenMut'0.t_ghostptrtokenmut int32)) (ptr:opaque_ptr) (return'  (ret:borrowed int32))= {[@expl:precondition] [%#span63] contains'0 (cur'0 self.current) ptr}
     any
-    [ return' (result:borrowed int32)-> {[%#span60] inv'1 result}
-      {[%#span59] not contains'0 (fin'0 self.final) ptr}
-      {[%#span58] fin'0 self.current = insert'0 (fin'0 self.final) ptr result.final}
-      {[%#span57] cur'0 self.final = remove'0 (cur'0 self.current) ptr}
-      {[%#span56] result.current = lookup_unsized'0 (cur'0 self.current) ptr}
+    [ return' (result:borrowed int32)-> {[%#span68] inv'1 result}
+      {[%#span67] not contains'0 (fin'0 self.final) ptr}
+      {[%#span66] fin'0 self.current = insert'0 (fin'0 self.final) ptr result.final}
+      {[%#span65] cur'0 self.final = remove'0 (cur'0 self.current) ptr}
+      {[%#span64] result.current = lookup_unsized'0 (cur'0 self.current) ptr}
       (! return' {result}) ]
     
   
   let rec borrow_mut'0 (self:borrowed (GhostPtrToken'0.t_ghostptrtoken int32)) (return'  (ret:GhostPtrTokenMut'0.t_ghostptrtokenmut int32))= any
-    [ return' (result:GhostPtrTokenMut'0.t_ghostptrtokenmut int32)-> {[%#span62] fin'0 result
+    [ return' (result:GhostPtrTokenMut'0.t_ghostptrtokenmut int32)-> {[%#span70] fin'0 result
       = shallow_model'0 self.final}
-      {[%#span61] cur'0 result = shallow_model'0 self.current}
+      {[%#span69] cur'0 result = shallow_model'0 self.current}
       (! return' {result}) ]
     
   
-  let rec ptr_from_box'0 (self:borrowed (GhostPtrToken'0.t_ghostptrtoken int32)) (val':int32) (return'  (ret:opaque_ptr))= {[@expl:precondition] [%#span63] inv'0 val'}
+  let rec ptr_from_box'0 (self:borrowed (GhostPtrToken'0.t_ghostptrtoken int32)) (val':int32) (return'  (ret:opaque_ptr))= {[@expl:precondition] [%#span71] inv'0 val'}
     any
-    [ return' (result:opaque_ptr)-> {[%#span65] shallow_model'0 self.final
+    [ return' (result:opaque_ptr)-> {[%#span73] shallow_model'0 self.final
       = insert'0 (shallow_model'0 self.current) result val'}
-      {[%#span64] not contains'0 (shallow_model'0 self.current) result}
+      {[%#span72] not contains'0 (shallow_model'0 self.current) result}
       (! return' {result}) ]
     
   
@@ -436,11 +469,11 @@ module GhostPtrToken_Test
   
   function empty'0 (_1 : ()) : FMap'0.t_fmap opaque_ptr int32
   
-  axiom empty'0_spec : forall _1 : () . ([%#span68] inv'3 (empty'0 _1))
-  && ([%#span67] view'0 (empty'0 _1) = Const.const (Option'0.C_None)) && ([%#span66] len'0 (empty'0 _1) = 0)
+  axiom empty'0_spec : forall _1 : () . ([%#span76] inv'3 (empty'0 _1))
+  && ([%#span75] view'0 (empty'0 _1) = Const.const (Option'0.C_None)) && ([%#span74] len'0 (empty'0 _1) = 0)
   
   let rec new'0 (_1:()) (return'  (ret:GhostPtrToken'0.t_ghostptrtoken int32))= any
-    [ return' (result:GhostPtrToken'0.t_ghostptrtoken int32)-> {[%#span69] shallow_model'0 result = empty'0 ()}
+    [ return' (result:GhostPtrToken'0.t_ghostptrtoken int32)-> {[%#span77] shallow_model'0 result = empty'0 ()}
       (! return' {result}) ]
     
   
diff --git a/creusot/tests/should_succeed/ghost_ptr_token/why3session.xml b/creusot/tests/should_succeed/ghost_ptr_token/why3session.xml
index 21cf658b82..521b59cb83 100644
--- a/creusot/tests/should_succeed/ghost_ptr_token/why3session.xml
+++ b/creusot/tests/should_succeed/ghost_ptr_token/why3session.xml
@@ -5,9 +5,73 @@
 <prover id="0" name="Z3" version="4.12.4" timelimit="5" steplimit="0" memlimit="1000"/>
 <file format="coma" proved="true">
 <path name=".."/><path name="ghost_ptr_token.coma"/>
+<theory name="Core_Option_Option_Type" proved="true">
+ <goal name="vc_none" proved="true">
+ <proof prover="0"><result status="valid" time="0.039440" steps="6"/></proof>
+ </goal>
+ <goal name="vc_some" proved="true">
+ <proof prover="0"><result status="valid" time="0.032989" steps="6"/></proof>
+ </goal>
+</theory>
+<theory name="Core_Panicking_AssertKind_Type" proved="true">
+ <goal name="vc_eq" proved="true">
+ <proof prover="0"><result status="valid" time="0.008151" steps="6"/></proof>
+ </goal>
+ <goal name="vc_ne" proved="true">
+ <proof prover="0"><result status="valid" time="0.012068" steps="6"/></proof>
+ </goal>
+ <goal name="vc_match&#39;" proved="true">
+ <proof prover="0"><result status="valid" time="0.012266" steps="6"/></proof>
+ </goal>
+</theory>
+<theory name="Core_Ptr_NonNull_NonNull_Type" proved="true">
+ <goal name="vc_t_nonnull" proved="true">
+ <proof prover="0"><result status="valid" time="0.023770" steps="6"/></proof>
+ </goal>
+</theory>
+<theory name="Core_Marker_PhantomData_Type" proved="true">
+ <goal name="vc_t_phantomdata" proved="true">
+ <proof prover="0"><result status="valid" time="0.022519" steps="6"/></proof>
+ </goal>
+</theory>
+<theory name="Core_Ptr_Unique_Unique_Type" proved="true">
+ <goal name="vc_t_unique" proved="true">
+ <proof prover="0"><result status="valid" time="0.018228" steps="6"/></proof>
+ </goal>
+</theory>
 <theory name="GhostPtrToken_Test" proved="true">
+ <goal name="vc_ptr_as_ref&#39;0" proved="true">
+ <proof prover="0"><result status="valid" time="0.017566" steps="1068"/></proof>
+ </goal>
+ <goal name="vc_swap&#39;0" proved="true">
+ <proof prover="0"><result status="valid" time="0.015835" steps="1068"/></proof>
+ </goal>
+ <goal name="vc_take_mut&#39;0" proved="true">
+ <proof prover="0"><result status="valid" time="0.021763" steps="1539"/></proof>
+ </goal>
+ <goal name="vc_borrow_mut&#39;0" proved="true">
+ <proof prover="0"><result status="valid" time="0.012774" steps="1539"/></proof>
+ </goal>
+ <goal name="vc_ptr_from_box&#39;0" proved="true">
+ <proof prover="0"><result status="valid" time="0.018142" steps="1539"/></proof>
+ </goal>
+ <goal name="vc_new&#39;0" proved="true">
+ <proof prover="0"><result status="valid" time="0.015133" steps="1646"/></proof>
+ </goal>
+ <goal name="vc_promoted0" proved="true">
+ <proof prover="0"><result status="valid" time="0.013410" steps="1646"/></proof>
+ </goal>
+ <goal name="vc_promoted1" proved="true">
+ <proof prover="0"><result status="valid" time="0.021817" steps="1646"/></proof>
+ </goal>
+ <goal name="vc_promoted2" proved="true">
+ <proof prover="0"><result status="valid" time="0.010922" steps="1646"/></proof>
+ </goal>
+ <goal name="vc_promoted3" proved="true">
+ <proof prover="0"><result status="valid" time="0.014226" steps="1646"/></proof>
+ </goal>
  <goal name="vc_test" proved="true">
- <proof prover="0"><result status="valid" time="0.031281" steps="76743"/></proof>
+ <proof prover="0"><result status="valid" time="0.031281" steps="102957"/></proof>
  </goal>
 </theory>
 </file>
diff --git a/creusot/tests/should_succeed/ghost_ptr_token/why3shapes.gz b/creusot/tests/should_succeed/ghost_ptr_token/why3shapes.gz
index 7b7a76b9e930cbaa47e01e7a1c63de7c6e6922a2..0ade85f0b54db511f3bb32165d757f4354f4d0ad 100644
GIT binary patch
literal 857
zcmV-f1E%~RiwFP!00000|Ls)EsvAcT-Rmo~OX3jds(uG<z!)yA&E3TGR`k;rcchU=
zqbriHPtQ{iJ4OU2H-vx|rK)pIpQ)<u@82vBAKgA3mM^I}Z0g<5OR;?O!=hcJ?Y{kO
z-4_?_C%4(Xd?zh=oMK^Nj=9A-W|qz|wQP>j@;L@8=9pOdxX5pZ*d2FGa^a)%RVo#=
z%8v{8;NGo&t+%NZPmSA`ytevGm~yMpqFz0@2dfL|sotfYzkM#qmrXhq9CW{dEzY^s
z=od&&a4|OPs{XJEg}6Ib)%3>#gu;HXfVcV84X=ZIP3N&c=|gHusdTxj>eG5#$5eGy
zdWClHkNYZ-@skGg^b4d5#k|>dDRzg>1ifH~W7DPh9qb8O*uOluD)m|-oI5Ip5xD2H
zK5TwZv8&7Sn<jWuS&iEQvgZvGD!D^y+76&BXp5y~sh!8y<)$UMlEZFRgQ+h_jAm6g
zxlr%g4l>KVZ;t6}<R52xfNtadOkwEKXZ+Q4amI+1^xQIa`RPsC)-T;{K(L6H-#sLz
zaZFaP@te^mg8OL>16=zZgf9JFi%b@$h?aD3aX7JmDLO3e@5W^OobJv#v^R@$F85Mx
zz25BFcb4&C&(NO6z*TkqeB7^(yK$^Hn-ARvyUO{xY3fq}Y@hGRSS%k@1|Tddi`r7K
z6fGsCIkOirS~%I)@=|uQ_>iyOlVU=>dNV%dRoTo#U6s{@*PBTHK>fq#zP-A!fA3lS
zOHdZiGB!L4Pec6Zs>5Y|b$M;|H(1fdLI)kPCrJ_|5EaG1AO)_7lYwalOEBa<kff1$
zsaeWgtAH7pr^+c2qJ*d<{l=h_JVr_|MiwJwlK22#kPIX;nHd>C5<*Bm3c;gN7!#3+
zqW2n^_DK&QmxzLpiQ_DA35*6QG*<||JV%`H0VF_0nUkbGC!HcALOCj!N}O_?QwK7@
z3{V4T01ObLjWW^*!woak;35Lgr0_8Zsk4(L`$&RQR7;l~&-ZAcWLoBo3<)IXV~ivx
zL79t8ahm$x7%Vc{fHEKr2m}1Tq)G{i#EFPy{v0D{0!&lQWu%znFjIr@zwp0NSW?m5
jX{DgtWFC0%IY;j)^-K!sR1rq}OUi!$*~9pWSPcLGTMee@

literal 557
zcmV+|0@D2-iwFP!00000|HV~HkDD+MzVj<`+jgr;j12}VrBbv~WG=aMHCHqNM~ebD
z3nZxh^))Y(Y#-{OZ6pq#zIlB!9-DWMtLBAHs##rB-Q>FZv=Xbw_fGptd3AXR(A~~h
zAXw}pv)Ds!F-Om0hQ7ss!eSSLt#jCnn9fzLD1D)Qp^PPr4_k-U^pt$jr835@rjy|#
zjFy0zizkUuyrVTnCTOQCHN=-k<9W$dXZ)c5#%Qr{@uU|_gY<b#g{pcU(!~N}Dmtp9
z$-k+rw=?t2O5RxFscT?E+*rwQjjG$;!DRFhd}>r{W%S(K>}@)KLzAeVq?p9=*!ZNn
zYI_%(?zujz-vxiL;VJZ!`&EWv3O~lj(*n%MaGo6*ziz!&rM~p13TAbJo4yBPJg-IS
zt$#kt6!g);6yE3^5?$-PO=2YmR-zarjulmTYQOfrVd`!c;S1f@YFevwEU}n}RIN_(
zs(nJwrRVdhPz<{XP@(nld`iyMbgX3VT2bgODRrib2cSb<Q9*lM*Sa$f<?&A#gb107
z43KeT9x{O}K<1m_SS>I~=<r@z%x)ST?Cvu$BKX~h@p_2OW;VJos|oizk>P>*&viF9
zH}>Dw8eRgkc*vviQP_=mOGR_d$Jf`^`wJ`T3~xd*{7N0iPxmelL+*<#JESTTf;=Hq
vy62(CIAtpcBnSz<1Wy8&z$AbKS4J|FffUl0p5)T7(sjNAJ%0lKq6Yu~DIOF-