search

viperproject / gobra

Gobra is an automated, modular verifier for Go programs, based on the Viper verification infrastructure.
https://gobra.ethz.ch
Other
111 stars 28 forks source link

Support for Ghost Types #773

Open ArquintL opened 3 months ago

ArquintL commented 3 months ago

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.

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

jcp19 commented 3 months ago

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.