[feature] Ghost generic formal parameters

[yannickmoy]

Summary

Currently, SPARK RM does not allow generic formal parameters. In particular, it is not possible to pass ghost subprograms as generic actual parameters in a generic instantiation. The following is illegal:

   generic
      type T is private;
      with function Precond (X : T) return Boolean;
      with procedure Callee (X : in out T);
   procedure Wrapper (X : in out T)
     with Pre => Precond (X);

   procedure Wrapper (X : in out T) is
   begin
      Callee (X);
   end Wrapper;

   function Not_Last (X : Integer) return Boolean is (X < Integer'Last)
     with Ghost;

   procedure Incr (X : in out Integer)
     with Pre => Not_Last (X)
   is
   begin
      X := X + 1;
   end Incr;

   procedure Inst_Incr is new Wrapper (Integer, Not_Last, Incr);

Motivation

Ghost and generics are two orthogonal features in SPARK that do not work ideally together currently. So that use of generics forces some logically ghost entities to be declared without the Ghost aspect, so that they can be passed as generic formal parameters.

Caveats and alternatives

None. This is a natural extension to Ghost semantics to allow its specification on generic formal parameters.

[yannickmoy]

I propose to modify SPARK RM 6.9 "Ghost entities" as follows:

• legality rule 5 should allow explicit Ghost aspect for generic formal parameters
• legality rule 10 should add as a valid reference of a ghost entity its appearance as an actual parameter in a generic instantiation, or as the default parameter in a generic definition, when the corresponding formal parameter is ghost
• a new legality rule should specify that, in a generic instantiation, the actual parameter corresponding to a ghost generic formal object parameter, either of mode IN OUT or of mode IN and of access-to-variable type, or a ghost generic formal procedure parameter, should be ghost (which means that it should be an object in the case of a mode IN parameter of access-to-variable type)

[sttaft]

In a separate e-mail chain, I questioned why we require the actual for a ghost formal to also be ghost. Here are some comments from Yannick and Claire:

Claire:

I think it makes sense if we want to be able to do the verification of ghost compatibility in the generic package instead of the instance. Indeed, if V : in out T; is an object parameter and procedure P (X : in out T); a procedure parameter, both ghost, then a call P (V); in the generic only make sense if either V is indeed ghost or both are not.

Yannick:

The issue is really for formal objects. I've amended the comment in the Issue. Better to continue the conversation there btw!

Claire:

You are sure? If a procedure happens to not be ghost, then it might have a non-ghost global output, and then calling it with some ghost expressions as parameters might be wrong.

[yannickmoy]

I agree with Claire. So that should be formal object parameters and formal procedure parameters.

[sttaft]

Claire:

I think it makes sense if we want to be able to do the verification of ghost compatibility in the generic package instead of the instance. Indeed, if V : in out T; is an object parameter and procedure P (X : in out T); a procedure parameter, both ghost, then a call P (V); in the generic only make sense if either V is indeed ghost or both are not.

I thought it was OK to pass a non-ghost parameter to a ghost procedure.

I guess the issue is focused on formal in-out objects, where clearly ghost code is not allowed to update a non-ghost object. And as Claire pointed out, if the non-ghost procedure, even if parameterless, has a non-ghost global that it is updating, then just calling the non-ghost procedure would not be permitted from a ghost context. So I am convinced, at least for formal in-out objects and formal procedures. Non-ghost formal IN objects and formal functions would seem to be safe.

[yannickmoy]

Let's make it all formal objects, as IN formal parameters of some access types could still be writable in SPARK.

[sttaft]

On further thought, formal IN objects can be specified via an arbitrary expression, so perhaps ghost vs. non-ghost is not meaningful. So actually might have to special case formal IN objects of an access type. And actually, a formal IN object is equivalent to a locally-declared constant whose initializing expression is the actual parameter. So I would presume that there are existing rules that control what can be the initializing expression for a local Ghost constant, and we can just use those rules.

[clairedross]

I am not sure I understand your comment. Surely, it would not be OK to give a ghost expression as an actual if the parameter is not Ghost?

On Mon, May 9, 2022 at 4:20 PM sttaft @.***> wrote:

On further thought, formal IN objects can be specified via an arbitrary expression, so perhaps ghost vs. non-ghost is not meaningful. So actually might have to special case formal IN objects of an access type.

— Reply to this email directly, view it on GitHub https://github.com/AdaCore/ada-spark-rfcs/issues/91#issuecomment-1121166373, or unsubscribe https://github.com/notifications/unsubscribe-auth/AB6NCMLX3CSZK6PZWX4F3V3VJENJXANCNFSM5VISXK4Q . You are receiving this because you are subscribed to this thread.Message ID: @.***>

-- Claire Dross Senior Software Engineer, AdaCore

[yannickmoy]

@clairedross this is taken care of by legality check 10 about valid occurrences of ghost entities

@sttaft I'd just forbid formal IN objects of access type, rather than go down the route of specifying this, as it will add much complexity for no actual use in SPARK.

[clairedross]

On Mon, May 9, 2022 at 4:54 PM yannickmoy @.***> wrote:

@clairedross https://github.com/clairedross this is taken care of by legality check 10 about valid occurrences of ghost entities

You mean that it would be OK to give a non-ghost procedure instead of a ghost one as long as it does not have non-ghost global output, right? Fine with me.

@sttaft https://github.com/sttaft I'd just forbid formal IN objects of access type, rather than go down the route of specifying this, as it will add much complexity for no actual use in SPARK.

IN parameters on a named access-to-variable type are already special cased for procedures, so it could make sense to special case them here too. -- Claire Dross Senior Software Engineer, AdaCore

[yannickmoy]

@clairedross no, that's not what I meant. I agree we should not accept non-ghost actual procedures for ghost formal procedures. I thought you were talking about formal parameters (in the generic instantiation) instead of parameters (in the call).

Regarding IN formals of access-to-variable type, I can live with a simple rule: when the formal is ghost, actual must be a ghost object.