Self referential types and non-strictly-positive occurrences

[nishanthkarthik]

Hello! I'm trying a permissions-ish representation for a tree data structure using GhostPtrToken.

struct Node {
    token: GhostPtrToken<Node>,
    children: Vec<GhostPtr<Node>>,
}

impl Node {
    #[open(self)]
    #[predicate]
    fn inv(self) -> bool {
        pearlite!{
            (forall<p: GhostPtr<Node>> self.children@.contains(p) ==> self.token@.contains(p))
            && (forall<p: GhostPtr<Node>> self.token@.contains(p) ==> self.children@.contains(p))
            && (forall<p: GhostPtr<Node>> self.children@.contains(p) ==> self.token@.lookup(p).inv())
        }
    }
}

I get the error from creusot (I built the latest commit)

Constructor C_Node contains a non strictly positive occurrence of type t_node

I vaguely remember seeing this before but I forget what the workaround was. Any input appreciated :)

Thanks!

[xldenis]

Hi!

We'll take a look and see what we can come up with, this sounds familiar, but I'm not sure if we have a good solution, this sounds quite familiar to: https://gitlab.inria.fr/why3/why3/-/issues/710

[jhjourdan]

Actually, in this case, we could plainly ignore recursion through GhostPtrToken, because a GhostPtrToken<T> does not logically contain a value of type T, so we don't have a problem to logically interpret this type.

[xldenis]

module T_creusot_contracts__ghost_ptr__GhostPtrToken [#"/Users/xavier/Code/creusot/creusot-contracts/src/ghost_ptr.rs" 14 0 14 35]
  type t_GhostPtrToken 't
end
module T_sacha__Node [#"/Users/xavier/Code/creusot/sacha.rs" 23 0 23 11]
  use T_alloc__alloc__Global as Global'0
  
  use prelude.prelude.Opaque
  
  use T_alloc__vec__Vec as Vec'0
  
  use T_creusot_contracts__ghost_ptr__GhostPtrToken as GhostPtrToken'0
  
  type t_Node  =
    | C_Node (GhostPtrToken'0.t_GhostPtrToken (t_Node)) (Vec'0.t_Vec opaque_ptr (Global'0.t_Global))
  
  function any_l (_ : 'b) : 'a
  
  let rec t_Node (input:t_Node) (ret  (token:GhostPtrToken'0.t_GhostPtrToken (t_Node)) (children:Vec'0.t_Vec opaque_ptr (Global'0.t_Global)))= any
    [ good (token:GhostPtrToken'0.t_GhostPtrToken (t_Node)) (children:Vec'0.t_Vec opaque_ptr (Global'0.t_Global))-> {C_Node token children
      = input}
      (! ret {token} {children}) ]
    
  
  function t_Node__children (self : t_Node) : Vec'0.t_Vec opaque_ptr (Global'0.t_Global) =
    match self with
      | C_Node _ a -> a
      end
  
  function t_Node__token (self : t_Node) : GhostPtrToken'0.t_GhostPtrToken (t_Node) =
    match self with
      | C_Node a _ -> a
      end
end

What would you propose as the alternative encoding of this type? and the mechanism to achieve it?

[xldenis]

I guess we could include a Snapshot<*const T> in the type to keep its ZSTness but allow us to remove the #[trusted] tag on it.

[jhjourdan]

All right, I was mistaken: we should not ignore recursion through GhostPtrToken<T>, because it logically contains T, but we should instead ignore recursion through GhostPtr<T>, which is just an address (the type actually does not depend on T).

And it seems like we indeed use opaque_ptr when translated into Coma, so we are doing the right thing for GhostPtr<T>.

Now let's come back to our problem here: in order to accept this definition, we would need to annotate parameters of trusted types with an attribute telling whether this parameter is used in a strictly positive way in this type. Once this is done, we would need to do something similar in Why3, which is non-trivial.

But anyway, now that I think about it, I have to say that this type definition is a bit weird: why do you have a token in each tree node? This allows duplicated children for one node, but disallow more involved subtree sharing. This seems to be somewhat half-way between a native definition using Box and a definition fully based on permissions that would use a global token for the full tree (shared between all its nodes). If you used such a definition, you would not have a problem with non-wellfounded recursive types.

[nishanthkarthik]

About the representation: In viper, I use predicates to reason about the ownership of direct children. Example. At every node, I can conclude that only the current node holds the permissions to its children. Secondly, with an axiom like for every pair of GhostPtrTokens, their models do not share a pointer, I can show that there are no cycles in this tree. In the end, I am trying to emulate the behavior of viper predicates with permissions and separating conjunctions using GhostPtrToken.

The sea-of-nodes approach: I typically use this for graphs but a single token for the entire tree makes it hard to prove the absence of cycles based on my attempts so far.

The simple definition using direct Box'd children works too, but this is not sufficient to prove the functional properties I'm looking for.

[jhjourdan]

The simple definition using direct Box'd children works too, but this is not sufficient to prove the functional properties I'm looking for.

What are these? I don't see how such a representation can allow proving more properties than the approach based on Boxes. The induction principle (allowing to prove lemmas by induction, or to define logical function by recursion) is equivalent to the absence of cycles: there is nothing you can prove with the absence of cycles you cannot prove by induction.

The only reason I can see you would need such a definition is that children can be shared. But it seems weird to allow sharing of children but not of subtrees in general.

[nishanthkarthik]

My goal is to use GhostPtrToken specifically to translate separation logic proofs in viper into creusot. That also means translating the functional specs using viper permissions into creusot specs almost mechanically.

The Tree example is just an attempt at that. I'm not sharing any child nodes in the same parent node. Ignoring the why of what I'm trying to do, I think the what in the original issue still has merit. Rephrasing my problem more abstractly, can I hold a GhostPtrToken in T, as long as I show that the holder is not managed by this token?