Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Fix conversion of Quint nullary polymorphic operators #3044

Merged
merged 4 commits into from
Dec 13, 2024

Conversation

bugarela
Copy link
Collaborator

@bugarela bugarela commented Dec 10, 2024

Hello :octocat:

Here's another fix for the conversion from Quint. I was hitting problems whenever None was used to construct values of different types inside the same operator. Upon debugging, I realized this was specific to nullary operators (such as None), and that the builder itself enforces that the same name has the same type in a same scope. A concrete example:

pure def f(x) = 
  pure val a = if (x > 2) Some(x) else None
  pure val b = if (x < 5) Some(true) else None

  (a, b)

One solution could be to use a polymorphic type (a type variable) for constructing the None name in TLA+, but that is too general and causes issues later on. So, instead, I wrote a new builder method polymorphicName that bypasses this check, and used that to construct names for nullary operators.

This is only a problem currently for nullary operators, as regular operators go through the application translation (not the name expression translation) and are dealt with differently.

  • Tests added for any new code
  • Ran make fmt-fix (or had formatting run automatically on all files edited)
  • Documentation added for any new functionality
  • Entries added to ./unreleased/ for any new functionality

@bugarela bugarela marked this pull request as ready for review December 10, 2024 13:08
@bugarela bugarela requested a review from Kukovec as a code owner December 10, 2024 13:08
@bugarela bugarela requested a review from konnov December 10, 2024 13:08
@bugarela
Copy link
Collaborator Author

Although my fix is sufficient to get over the conversion phase and produce valid TLA+, I see now that it is not sufficient to make snowcat happy:

error: internal error: while type checking in Apalache:
'unknown location,__QUINT_LAMBDA111's type annotation ((None({ tag: Str }) | Some(a36), a36) => None({ tag: Str }) | Some(a29)) is too general, inferred: ((None({ tag: Str }) | Some(a29), a29) => None({ tag: Str }) | Some(a29))'
Please report an issue: https://github.com/informalsystems/quint/issues/new

So more to investigate. This PR still unblocks things, so might be worth moving foward with it at this point. I'm not sure.

@konnov
Copy link
Collaborator

konnov commented Dec 10, 2024

Yeah, the behavior of None is annoying in Quint. What I don't see is why this should be resolved at the level of TLA+. I thought that the Quint typechecker would assign proper types to the different instances of None. If this is the case, I believe that instead of propagating polymorphism to Apalache, I would rather produce different names for the different instances of None that carry different types. Otherwise, Apalache may not have sufficient context to infer the proper types.

@konnov
Copy link
Collaborator

konnov commented Dec 10, 2024

I guess, this is the related issue: informalsystems/quint#1451

@bugarela
Copy link
Collaborator Author

I thought that the Quint typechecker would assign proper types to the different instances of None. If this is the case,

it is

I believe that instead of propagating polymorphism to Apalache, I would rather produce different names for the different instances of None that carry different types. Otherwise, Apalache may not have sufficient context to infer the proper types.

Hmmm but Apalache doesn't need to infer the types, as we annotate everything. However, in the end, it complains that our annotation is too general. I'll need to further debug to understand if it is actually too general and Quint has to provide a more specific type, or if Apalache is expecting something too strict.

Regarding the issue, I just confirmed that this PR fixed it. That spec works both with quint compile and quint verify. So that's more confirmation for me that this PR is worth moving foward with and that the "too general" issue is another problem to solve (probably the same as in informalsystems/quint#1398)

@konnov
Copy link
Collaborator

konnov commented Dec 11, 2024

The most important question for me is whether there was a reason for not allowing something like (F: Int)(...) and (F: Bool)(...) in the builder, unless F is defined as polymorphic. Perhaps, @Kukovec could help us to understand it.

@Kukovec
Copy link
Collaborator

Kukovec commented Dec 11, 2024

The most important question for me is whether there was a reason for not allowing something like (F: Int)(...) and (F: Bool)(...) in the builder, unless F is defined as polymorphic. Perhaps, @Kukovec could help us to understand it.

I mean, the reason it's not allowed is simple, the basic notion of socpe-safety is that one name is only allowed to have one type in a given scope. For polymorphic operators, F() may have types Bool and Int in different instances, but F should have () => t in both.
Please don't add methods to the specifically scope-safe builder that makes it explicitly scope-unsafe, just use the unsafe builder.
If you call

def appOp(Op: TlaEx, args: TlaEx*): TlaEx = {
// To support polymorphic operators, we first attempt to compute the post-unification types
val opType = TlaType1.fromTypeTag(Op.typeTag)
require(opType.isInstanceOf[OperT1], s"appOp of ${Op} not tagged with type OperT1, but ${opType}")
val OperT1(_, resT) = opType.asInstanceOf[OperT1]
val argTs = args.map(a => TlaType1.fromTypeTag(a.typeTag))
val mockOperT = OperT1(argTs, resT)
val unifOpt = new TypeUnifier(new TypeVarPool()).unify(Substitution.empty, opType, mockOperT)
unifOpt match {
case Some((subst, unifiedOperT)) =>
val retypedArgs = args.zip(argTs).map { case (arg, argT) =>
arg.withTag(Typed(subst.subRec(argT)))
}
val retypedOp = Op.withTag(Typed(unifiedOperT))
retypedOp match {
// This is a workaround for the fact that that we currently de-lambda,
// because lambdas are not supported in the Apalache IR. See
// https://github.com/informalsystems/apalache/issues/2532
case LetInEx(nameEx @ NameEx(operName), decl) if operName == decl.name =>
val appliedByName = buildBySignatureLookup(TlaOper.apply, nameEx +: retypedArgs: _*)
LetInEx(appliedByName, decl)(appliedByName.typeTag)
case _ => buildBySignatureLookup(TlaOper.apply, retypedOp +: retypedArgs: _*)
}
case None =>
throw new TBuilderTypeException(
s"Operator application argument types ${mockOperT} do not unify with the operator type ${opType} in ${Op}(${args
.mkString(", ")}).")
}
}
with your type-instances (() => Int or () => Bool) it should give you what you want.

@konnov
Copy link
Collaborator

konnov commented Dec 11, 2024

Right! If we expect the types to be correct, we can just use UnsafeBuilder.

@bugarela
Copy link
Collaborator Author

Ok, thanks for the input, it makes sense! Took me some time to figure out how to do it as I couldn't use point in Quint.scala. I ended up having to change the imports in unexpected ways, but it worked out in the end.

Copy link
Collaborator

@konnov konnov left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Looks great! Thanks for fixing it and going the extra mile in using UnsafeBuilder!

@konnov
Copy link
Collaborator

konnov commented Dec 13, 2024

I will merge it right away to a cut a fresh release

@konnov konnov merged commit 8b661d7 into main Dec 13, 2024
10 checks passed
@konnov konnov deleted the gabriela/fix-quint-nullary-polymorphism branch December 13, 2024 16:56
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

3 participants