Support for Ghost Types

[ArquintL]

This PR adds support for Ghost Types, i.e., the ability to mark a named type or type alias as ghost such that this type is erased. This feature came up in the context of structs that are declared for verification-only purposes and, thus, contain only ghost fields. To avoid any confusion, we restrict ghostness of a type declaration to match the ghostness of its RHS. In addition, this PR fixes an issue where type declarations were not correctly considered being ghost despite declaring a name for a ghost type. As a side-effect, ADT can no longer be method receiver as they are ghost.

In addition, this PR makes PPermissionType and PPredType ghost types, which did not use to be the case.

[jcp19]

Oh, cool!

Do I see it correctly that, for two instances x and y of ghost struct type T (containing at least one field), x == y will always yield true? If so, maybe we can change the encoding such that it matches === in those cases.

[Felalolf]

I only have one minor comment, the rest seems fine.

[ArquintL]

I'm not the biggest fan of special casing the encoding for ghost structs as this seems rather confusing to users. Instead, I've implemented a type checker warning for this case in the separate PR #826

[jcp19]

I'm not the biggest fan of special casing the encoding for ghost structs as this seems rather confusing to users. Instead, I've implemented a type checker warning for this case in the separate PR #826

Hmm, in that case, I would rather throw a type error rather than a warning, given that == between ghost structs becomes rather useless. In fact, I think that the current solution introduces a special case - so far, for all ghost types, == matches ===. With the introduction of ghost structs, this will no longer be the case.

The way I see it, ghost structs are useful as alternatives to ADT with a single constructor. However, for ADTs we do have a meaningful ==, whereas for ghost structs, we can only resort to ===.

EDIT: To add to this, I had two instances where I was bitten by the unexpected semantics for ==, one in a first attempt while trying out these changes in scion (I changed some types to be ghost structs instead of adts and, without noticing, some of my specs became vacuously true), and one instance with my student who was verifying the go standard library stated a lemma that was also vacuously true without noticing. If you really insist on keeping these semantics for equality, then I think that reporting anything less than a type error here is way too dangerous.

[ArquintL]

I agree with your statement that ghost types use == like ===. My fear is related to the different semantics between a ghost struct and a struct with just ghost fields, which feels like very similar things to me, but maybe I'm wrong here and we should indeed have == mean different things for ghost structs and structs with just ghost fields

[ArquintL]

@jcp19 I've now implemented equality (==) for ghost structs to match ===. Could you take a look at the most recent commit? In particular, I have the impression that type equality for StructT was missing some checks, namely that the fields have the same names. Is this correct?

[jcp19]

So far, I am just clarifying a bigger point that I noticed while I was looking at the tests. After that is clarified, I will take a look at the rest

[jcp19]

I think I found an unsoundness in ghost embeddings, please check out my comment

[jcp19]

LGTM! Before merging, please let me try these changes out in SCION to see if there are any blocking issues. I will let you know soon

[jcp19]

Interestingly, trying to verify the path package in VerifiedSCION as is leads to multiple type errors (expected) and an exception (unexpected):

[info] An assumption was violated during execution.
[info] Logic error: This case should be unreachable, but got unknown
[info] viper.gobra.util.Violation$LogicException: Logic error: This case should be unreachable, but got unknown
[info] 	at viper.gobra.util.Violation$.violation(Violation.scala:27)
[info] 	at viper.gobra.frontend.info.implementation.typing.ExprTyping.getTypeFromCtxt(ExprTyping.scala:903)
[info] 	at viper.gobra.frontend.info.implementation.typing.ExprTyping.getNonInterfaceTypeFromCtxt(ExprTyping.scala:821)
[info] 	at viper.gobra.frontend.info.implementation.typing.ExprTyping.intExprWithinTypeBounds(ExprTyping.scala:636)
[info] 	at viper.gobra.frontend.info.implementation.typing.ExprTyping.numExprWithinTypeBounds(ExprTyping.scala:632)
[info] 	at viper.gobra.frontend.info.implementation.typing.ExprTyping.wellDefActualExpr(ExprTyping.scala:220)
[info] 	at viper.gobra.frontend.info.implementation.typing.ExprTyping.$anonfun$wellDefExpr$1(ExprTyping.scala:212)
[info] 	at viper.gobra.frontend.info.implementation.typing.BaseTyping$$anon$1.compute(BaseTyping.scala:104)
[info] 	at viper.gobra.frontend.info.implementation.typing.BaseTyping$$anon$1.compute(BaseTyping.scala:98)
[info] 	at viper.gobra.util.Computation.apply(Computation.scala:16)
[info] 	at viper.gobra.util.Computation.apply$(Computation.scala:16)
[info] 	at viper.gobra.frontend.info.implementation.typing.BaseTyping$$anon$1.viper$gobra$util$Safety$$super$apply(BaseTyping.scala:98)
[info] 	at viper.gobra.util.Safety.apply(Computation.scala:31)
[info] 	at viper.gobra.util.Safety.apply$(Computation.scala:31)
[info] 	at viper.gobra.frontend.info.implementation.typing.BaseTyping$$anon$1.viper$gobra$util$Memoization$$super$apply(BaseTyping.scala:98)
[info] 	at viper.gobra.util.Memoization.$anonfun$store$1(Computation.scala:21)
[info] 	at org.bitbucket.inkytonik.kiama.attribution.AttributionCore$CachedAttribute.liftedTree1$1(AttributionCore.scala:58)
[info] 	at org.bitbucket.inkytonik.kiama.attribution.AttributionCore$CachedAttribute.apply(AttributionCore.scala:56)
[info] 	at viper.gobra.util.Memoization.apply(Computation.scala:23)
[info] 	at viper.gobra.util.Memoization.apply$(Computation.scala:23)
[info] 	at viper.gobra.frontend.info.implementation.typing.BaseTyping$$anon$1.apply(BaseTyping.scala:98)
[info] 	at viper.gobra.frontend.info.implementation.Errors$$anonfun$1.applyOrElse(Errors.scala:26)
[info] 	at viper.gobra.frontend.info.implementation.Errors$$anonfun$1.applyOrElse(Errors.scala:18)
[info] 	at scala.PartialFunction$OrElse.apply(PartialFunction.scala:266)
[info] 	at scala.collection.StrictOptimizedIterableOps.flatMap(StrictOptimizedIterableOps.scala:118)
[info] 	at scala.collection.StrictOptimizedIterableOps.flatMap$(StrictOptimizedIterableOps.scala:105)
[info] 	at scala.collection.immutable.Vector.flatMap(Vector.scala:113)
[info] 	at org.bitbucket.inkytonik.kiama.util.Messaging$.collectMessages(Messaging.scala:113)
[info] 	at viper.gobra.frontend.info.implementation.Errors.viper$gobra$frontend$info$implementation$Errors$$x$1(Errors.scala:18)
[info] 	at viper.gobra.frontend.info.implementation.Errors.viper$gobra$frontend$info$implementation$Errors$$x$1$(Errors.scala:16)
[info] 	at viper.gobra.frontend.info.implementation.TypeInfoImpl.viper$gobra$frontend$info$implementation$Errors$$x$1$lzycompute(TypeInfoImpl.scala:24)
[info] 	at viper.gobra.frontend.info.implementation.TypeInfoImpl.viper$gobra$frontend$info$implementation$Errors$$x$1(TypeInfoImpl.scala:24)
[info] 	at viper.gobra.frontend.info.implementation.Errors.errors(Errors.scala:16)
[info] 	at viper.gobra.frontend.info.implementation.Errors.errors$(Errors.scala:16)
[info] 	at viper.gobra.frontend.info.implementation.TypeInfoImpl.errors$lzycompute(TypeInfoImpl.scala:24)
[info] 	at viper.gobra.frontend.info.implementation.TypeInfoImpl.errors(TypeInfoImpl.scala:24)
[info] 	at viper.gobra.frontend.info.Info$.checkSources(Info.scala:270)
[info] 	at viper.gobra.frontend.info.Info$Context$TypeCheckJob.typeCheck(Info.scala:170)
[info] 	at viper.gobra.frontend.info.Info$Context$TypeCheckJob.compute(Info.scala:159)
[info] 	at viper.gobra.frontend.info.Info$Context$TypeCheckJob.compute(Info.scala:134)
[info] 	at viper.gobra.util.Job.execute(TaskManager.scala:44)
[info] 	at viper.gobra.util.Job.execute$(TaskManager.scala:35)
[info] 	at viper.gobra.frontend.info.Info$Context$TypeCheckJob.execute(Info.scala:134)
[info] 	at viper.gobra.util.TaskManager.$anonfun$addIfAbsent$1(TaskManager.scala:68)
[info] 	at scala.concurrent.Future$.$anonfun$apply$1(Future.scala:678)
[info] 	at scala.concurrent.impl.Promise$Transformation.run(Promise.scala:467)
[info] 	at java.base/java.util.concurrent.ThreadPoolExecutor.runWorker(ThreadPoolExecutor.java:1128)
[info] 	at java.base/java.util.concurrent.ThreadPoolExecutor$Worker.run(ThreadPoolExecutor.java:628)
[info] 	at java.base/java.lang.Thread.run(Thread.java:829)

[jcp19]

No blocking issues found in SCION, I have a PR ready to land as soon as this is merged (viperproject/VerifiedSCION#398), so feel free to do so when the tests pass

[ArquintL]

No blocking issues found in SCION

How come an exception is not a blocking issue? ^^

[jcp19]

No blocking issues found in SCION

How come an exception is not a blocking issue? ^^

Good point 🤣 By blocking issues, I was looking out for idioms that are used in practice that are no longer allowed or easily replaceable, whereas this is an exception that occurs when type errors should be thrown. I agree this should be fixed before merging

[ArquintL]

Interestingly, trying to verify the path package in VerifiedSCION as is leads to multiple type errors (expected) and an exception (unexpected):

I just checked: merging this PR with #855 and running the following command in the VerifiedSCION repo (viperproject/VerifiedSCION@a6638e1) no longer results in an exception but (as expected) type errors

[ArquintL]

CI is currently failing as #855 must be first merged

[jcp19]

@ArquintL from my side, we can go ahead and merge this