>> Hello. My name is Igor Konnov,
I'm working at Informal Systems.
I'm going to give you the first part of
this talk on type inference for TLA+ in Apalache.
The second part will begin by Jure Kukovec who's
finishing his visit at Turin.
We decided to split this job of recording the video.
That's why we have basically two talks for the price of one.
The title says we do type inference in Apalache.
If you haven't seen this tool,
you can go on the Apalache webpage on GitHub.
That's a symbolic model checker
for TLA+ as you develop them at Informal Systems,
and it happened to be developed at Turin.
In a nutshell, we have been
developing this model checker for about five years.
It reduces the verification questions too,
since you solve them and we had been
focusing on application of
this model checker in the context of fault tolerance,
distributed algorithms, and blockchains.
That's what we are doing at Informal Systems.
Now, if you want to find more information about how it's working,
you can check that OOPSLA paper that is mentioned on the slide.
However, this talk is not about the model checker,
although that's a very interesting topic for me.
This talk is about how you go from
an untyped language like TLA+ to a typed language like SMT.
I guess SMT solvers require types and codings.
Essentially, this talk is about how you type an untyped language.
In this talk, they're going to present to you two tools.
One is the Type checker,
the new Type checker we have,
and another one is a Type inference tool.
The type checker is planned for the next release.
It's breaking out.
That's some local analysis of operator definitions.
If it cannot deliver,
it asks the user to give it to some annotations.
Type inferer doesn't require any annotations and
thus global analysis of the specification.
However, it's much harder to make it robust tool.
That's why it's still a prototype.
It's actually working but it will take a bit more time to make
it a tool that would be used for either origins.
What's important here, that the both tools are
completely independent of the model checker.
You don't have to understand the model checker.
You don't have to use the model checker in
order to do type inference tools.
Let's talk about the type checker.
I will focus on it then Jure will talk about the type inference.
Okay, let's have a quick demo here.
I'll show you how the type checker is working on a simple example.
It's just called CarTalkPuzzle.
I took it from the repository of the TLA specifications.
You can look the specification yourself.
If you look at it, you'll see that there are
some non-trivial definitions that use recursion,
that use functions sets.
It's not always clear
what the arguments are that breakers are doing,
until you read the recommendations,
if you read the comments here.
Let's see what our type checker can
tell us about this specification.
We'll just run the type checker result writes in annotations
and see where it complains about the specification.
It complains in line 51 here,
it says that it found a polymorphic type, basically some constant.
The tasks has to give the concrete type here.
We don't allow polymorphic types,
user-defined operators,
although TLA operators are obviously polymorphic.
What's going on here?
You have to choose operator that just
provides some elements of a set.
Of course, that checker cannot figure out the exact type.
What we can do here, we can
define the signature of this operator sum.
In order to do that, I will have to extend the module,
type inlet extended Apalache module
and to write the type annotation.
Let's go and we do it now.
I will just copy this type annotation
from my cheat sheet because I figured out the types before.
Say here that the operator, Sum,
is taking a function of integers to
integers and it's taking a set of integers.
As a result, it returns an integer.
That's our syntax for operators.
Let's see if default type checker is convinced here.
Yes. Now it complains about another thing,
it says that it doesn't know the type of
P. Indeed P is just a constant,
as well as N. What we can do here,
we can introduce the assumptions,
I'll just say one and fill right here,
the assumptions about types of the parameters,
N and P are integers.
Let's run the type checker again.
Now it goes through,
but now it complains in line 169.
Here it's actually interesting.
It says that it cannot choose between a function and a sequence,
because B can be either a sequence or
a function given the current types in this operator.
It cannot figure it out. You can again help
the type checker and give a concrete type for image.
This time it's not so trivial.
It took me a while to figure out the exact type.
But it actually takes a set of integers and, again,
a function of integers to integers,
and then again returns a set of integers.
Let's run the type checker again.
Now the type checker has happy. What does it mean?
It means that our type checker managed to compute
the types of all expressions in
all operator definitions in this specification.
All of you wrote just four type annotations here.
We gave the type annotations for the parameters,
and we gave type annotations for
two operators that are actually quite
trickier and the type checker gave up on them.
That ends this small demo. Let's continue.
I hope I have your attention now after that short demo,
and now I'd like to explain to you
how this type checker is actually working.
I believe it's very simple and I think you'll agree with me.
Before we can do that, let's talk about the type syntax.
That's actually the syntax we use for type annotations,
but it also will help you in understanding how the tools run.
First of all, we have basic types like Booleans,
integers, strings, and reals, nothing unexpected.
We have uninterpreted types,
and wait until the next slide, I will explain all this.
We also have functions from sum types to sum types.
We have sets and sequences.
They're actually homogeneous in the sense that you cannot
put objects of different types into a set or a sequence.
However, there is an exception for records.
Wait until the slide when we talk about records.
There are tuples and records, and of course,
there are operators that may have a fixed number of
arguments to the results.
There are type variables that allow us to talk about
polymorphic types and type annotations and type inference.
If you want to see more details,
go to the Apalache repository and check
these architectural decision record types.
Uninterpreted types, I promised them to you.
Often, if you look at the specification,
you see constants, and
these constants are often sets or just some values.
Usually, it actually doesn't matter
whether these sets are sets of integers,
Boolean, strings, so on, so forth.
You can see these examples in Paxos, for instance,
there are sets of values, sets of acceptors.
You see it in other examples like
prisoners, missionaries, and cannibals.
In all these cases, actually,
you should use uninterpreted types
because the only thing you can do
about uninterpreted types is to compare objects,
say, inside sets of uninterpreted types.
In this case, acceptors will be just the set of processes,
you don't know what processes are,
you can always say if two processes are equal or not.
The same applies to values.
If you have seen model values,
then you'll see that's actually uninterpreted values.
You can say that these are model values of types A,
B, C, D, and so on.
A, B, C, D, and so on are actually uninterpreted types in TLC.
So that's how you can express these things.
How does our type checker works?
Good to say it is embarrassingly simple.
Let's see if I convince you.
First of all, before the type checker [inaudible] should annotate
all the built-in operators with
some signatures, operator signatures.
Plenty of TLA operators are quite simple in that sense.
Say arithmetic operators take two integers and return an integer.
Some operators are also simple,
but they're polymorphic, and they're also very [inaudible].
For instance, set constructors take
several elements and return a set of lows elements.
Say, there are two elements,
it will return a set of the same type.
You can argue that in TLA,
set elements might have different types,
yes, but not on our type system,
not in our type checker.
Records are a bit of an exception,
you'll see it later.
Several operators actually can be treated as overloaded operators.
For instance, the tuple operator creates either a tuple,
so in this case a pair,
or a sequence of elements of the same type.
Again, you can say sequences are tuples,
tuples are sequences, yes.
In untyped TLA, that is true,
not in our type system.
We will reject some specifications
that you believe are actually okay.
There are a few hardcore operators that actually
bind some values to the variables.
For instance, a set filter in our system
becomes this huge operator that says you have an operator,
it takes some type a,
and it returns a Boolean that's a predicate.
Given this predicate, it returns a set of a's.
Actually, what is happening here,
how does it do that?
It binds a name x to the elements of the set S,
gives this x to P and P has to figure out what to do about this x.
If you looked at all
these annotation set we wanted to have and figured out
that there is a very simple language that can
describe all of the TLA operators,
if you think about them in terms of a type system.
That's what we call a simple lambda-calculus over types.
It has just six constructs that you see here.
First of all, you can have a type, that's obvious.
You just have to type like int or a function from instance.
You can have a variable name.
You can have a lambda abstraction as you have
seen in the previous slide just
binds the variables x_1 to x_k to
the elements of the sets that are
presented by expressions e_1 to e_K,
and these names can be used inside
expression e. Now that definition, not surprisingly,
binds expression e_1 to the name
x and this name x can be used inside the expression e_2.
Application by name, like if you have a user-defined operator,
if you just take the operator name
and apply it to the arguments e_1 to e_k.
The most interesting case here is,
of course, application by type.
You have a choice of types,
operator types to choose from and you apply one
of these operators to the arguments e_1 to e_k.
It's a very simple language,
much simpler than TLA.
However, you can translate every TLA expression,
all the built-in operators and
user-defined operators into this simple language.
What can we do about this simple language?
Well, we can take an expression in
this language and do further types by doing equation solving.
I'll just show you an example here.
Here's a TLA operator, a very simple one.
You translate it into our calculus.
You have a Lambda expression,
a signature int into bool,
and you pass x and int. What do you do then?
Well, you make equations,
introduce equations for this operator,
for this slide expression.
You say there is a type a_1 that
should have this shape because I know there is lambda inside.
For the lambda, I know that this expression should be a set.
So I say a_4 is a set and it has
this shape and it actually happens to be equal to set of a.
Because, well, that's going to do here and
a_2 expresses the elements that are going to be bound to x.
Then we jump to inside this expression.
You see an operator application here,
you know the number of arguments.
You say it's a_5.
It has two arguments and returns a_3.
What are these arguments?
Well, they have to be equal to the value of x and
x is encoded by the variable a_2,
and the second argument is int, right?
You have the signatures,
so this operator actually has to match this signature as well.
We solve these equations and you have the answer.
Well, I was using this kind of special squiggly equality,
it's not exactly the equality.
What we mean by this is unification.
In basic cases like ints,
you just say they're equal, like terms.
If you have variables unification,
you can say whether they're equal or not
and return a binding as a result.
Or in this case,
you can have two bindings.
We solve some of the equations here.
The most interesting case here is records.
We actually can unify
records that have a different number of fields.
In this case, we would produce
joint records that has all these fields that are unified,
but we don't allow to unify records that
have the sign types different types to the same name.
So in this way, we can have
records of different types mixed into the same set,
like you can see in Paxos,
but we still stay relatively precise in our type checking.
As a side effect, since we solve equations of a type unification,
we can do some local type inference.
So there are some boundaries of
this type checking and we think it's
actually quite good for the user to understand what's going on.
The limit type computation to operate
their boundaries if a type checker
cannot find the types precisely in
that definition or operator definition just fails as [inaudible] ,
we don't allow polymorphism in user-defined operators,
and that's actually a very good topic for the meeting to discuss.
At the same time, they allow polymorphic, monomorphic,
and overloaded built-in operators.
Otherwise, we wouldn't be able to do the type checking.
So that finishes my part about the type checker and
now [inaudible] continues with type inference.
>> Hello everyone, welcome to this part of the talk
where we discuss type inference in TLA.
This talk is going to be about five things roughly.
First, it's going to be about our Type System in practice.
I'm going to walk you through some examples
and for some of the experiments we've done,
and then I'll talk a bit more about the behind-the-scenes theory,
how we actually do this at the first-order logic level,
how we encode types of strings,
and then finally how encode types of TLA expressions.
So here's what we do at a conceptual level.
So first, we use
the TLA specification to get some bounds information.
So we're not going to use all of the types in the type system.
For a concrete specification,
we only have to care about a finite number of them, specifically,
finite [inaudible] records and tuples,
it's going to simplify a lot of things.
Then we keep the specification or
any sub-expression we're interested in and we
create the SMT constraints from that expression's syntax tree.
Then we have two options,
either we have a satisfiable set of constraints, we get a model,
and from that model,
we reconstruct the types maybe with some post-processing
where we make this more user-presentable.
Or alternatively, we have a type error,
in which case the user has to go and fix the specification.
All right. So let's walk through an example.
So here's a very simple specification that does
almost nothing and then we'll maybe see
how we get constraints from this [inaudible]
Basically, here's the approach in a sentence.
We're going to look at every expression,
and every sub-expression of that expression.
We're going to assign it an SMT variable.
In this case, if p then y else of
A is assigned the SMT variable t_1.
When we're going to read the solution,
we're going to say our t_1 holds the body of p especially.
The top-level body of p is
defined with an if-then-else operator which has a known type.
In order to encode this type, we take,
for example, in this case,
the polymorphic type, any Alpha, bool Alpha,
Alpha to Alpha, and we walk through
the arguments of p and we encode each of these arguments,
the type that the operator says the argument has to have.
For example, p will have to have type bool,
y and set Alpha will have to have type Alpha,
and the entire expression will have to have type Alpha.
Here, in this case,
we use the variable c_1 to represent
the type Alpha because we don't know what Alpha is at this point.
We use bool for t_2 because p has to be a boolean.
Next, we just walk through the arguments.
For example, p and y,
they're handled in the same way.
One is a constant, one is variable,
but at the type inference level,
there is no difference between the two.
Each constant and variable gets a pre-assigned SMT
variable so that anywhere in the specification where we use p,
we use the same type variable to refer to it in the encoding.
For the set constructor,
the story is similar to the analysis constructors.
It's a built-in operator.
It has a known type.
It's one argument that creates a set.
The process is very similar,
so t_4 has to be a set type.
T_5 has to be the type of the content of the set,
and because Alpha is,
again, unconstrained at this point,
we use a fresh variable in c_2.
Then we move to A.
A is a user-defined operator,
so we're going to need to create a fresh instance of A
where we replace the arguments data if it has any,
correctly with the arguments passed 2A.
In this case, A is null, so this isn't a consideration,
but we would have to do this at this point in general.
To analyze the type of A,
we have to look at the body of A.
So we repeat the process we just performed on the body
of B on the body of A.
But this time we're going to take instead of t_1
as at the top level term to encode the body of A,
we're going to use the here freshly created c_3
for this particular instance of A,
which might be important if they had
different ways of passing parameters.
For plus, plus, again has a known type.
It's int and int to int, so we
create the constraints that mirror that.
Then we finish off by looking at the x,
which has the SMT variable v_x,
and 2, which is an integer literal.
So it just becomes if.
You have this set of constraints.
What we do with these constraints is
we pass it to an SMT solver and
the SMT solver will find that this is
a satisfiable set of constraints.
Our recovery will then from the SMT model,
recover the following types for all of the variables,
constants, and operators in this specification.
As you can see, p has to be Boolean
because it's part of the if and else condition.
Similarly, A is a nullary operator that prefers an integer.
The other ones follow from bool of if then else.
Both branches of the nulls have to return the set of integers,
and then the body of B has types of integers as this
y because set the of A has type set of integer.
This is exactly what you would expect.
Of course this happens automatically.
I didn't have to think about any of this.
I just had to push the "Run" button and I got this for free.
You can see how this would work.
In larger specifications, the constraints would be
much bigger and it will be much
harder for me to manually solve them.
So such a tool that would be very welcome,
especially in the designing phase
of the specification before it's fully completed.
Next, let's look at some experiments.
We took 35 specifications from the community repository you see on
the screen and we basically ran them through the tool.
Here you see the benchmark sizes.
The reason you see 42 instead of 35 is because
the specifications highlighted in red had type errors.
So we added a minimal fixed specification to
this benchmark to show
how you can make those specification step correct.
We ended up with most specifications
being under 200, maybe under 400,
and then this one outlier specification
reaches roughly 1,100-1,200 lines of coding.
These are realistic sizes.
These are the specifications you would come across in real life.
So think it's quite the representative benchmarks.
Let's look at how the tool did.
Good news, the tool took less
than a second for the majority of the specifications,
so with this outlier being
roughly 10 seconds for the
largest 1,100 lines of code specification,
which is the protocol 802.16-AuthorizationPKMv35.
[inaudible].
There's benchmarks that includes
many other well-known other specification,
it includes the CarTalkPuzzle that Igor showed you in his demo.
Only in this case, we didn't have to manually annotate
anything and the tool still found the type of,
for example, the recursive function sum to be
the same type that the annotation was used.
But it did so automatically without need of user interference.
But it also managed to type check in for types work,
Pascos, and [inaudible] algorithm, Bosco.
Interestingly enough, our Raft had a type error which
we corrected as in specification 39.
These are the benchmarks.
The times look to be very good for this [inaudible] tool.
There were some quotes,
some interesting site cases, let's say.
One benchmark, for example,
Queens.tla did not type check.
But for the reason that it
uses queens in one instance
as a sequence and then the other instances as a function,
which in our type system,
does not permit it because we treat those things as separate,
independent objects that you cannot unify through.
But of course, in the untyped interpretation of tla,
functions and sequences are one and the same,
so using either syntax layer
nor the function sets syntax interchangeably is perfectly valid.
What you could do in our framework to solve
this concrete problem is you could enter
this casting operator, in which case,
you cast on the two expressions,
and you would quickly find that this
is a then valid undercasting [inaudible] ,
which we don't currently support.
The other one which is interesting
is the DijkstraMutex specification.
This one is interesting because it's an instance of
a specification that is statically not typeable,
but would be correct under a dynamic typing scheme.
The way these operators are set up,
so Ia3A to la4A,
guarantee that any execution will
traverse them in a very specific order.
The way this temp variable is being
used is being used basically as a place holder,
as a miscellaneous, if you will,
where a certain value is just propagated into
the next phase instead of having
to define a fresh variable for
each instance or for the phase between la3A and la4A.
Attempt is just being reused,
but it's being used in such a way that it's not consistent typed.
For example, it's initially defined to be
an integer, but then at some point,
it changes to be set of integers,
which is not allowed in our system.
This, you cannot just fix with [inaudible].
These are the experiments. Now, let's
look at what happens under the hood.
Under the hood, what we would want
is to pick a type and return return.
It seems like this will work for most things,
but unfortunately, there are exceptions,
and those exceptions are records.
The problem with records is there's
an infinite family of records with arbitrary numbers of
fields and you want to have
a finite number of terms at
the SMT encoding level. How do we solve this?
Well, we solve this by cheating.
We start the process by looking at
a specification and in any given specification,
there are only finitely many couple of
indices and only finitely many record fields.
We take that information and we use this to modify our encoding on
a specification-specification basis to avoid
having to introduce infinitely many term constructors.
This is our encoding. So we define abstract datatype S_T.
Most functions are what you would expect.
You have the classic constants input string,
and then the function set sequence and fun.
Then we have these special constructors for records, and couples,
and operators where we use one constructor for, for example,
all sizes of records,
and that one constructor conceptually
has all of the possible fields in the specification.
Then you use additional analysis in
the recovery phase to figure out when a record term is given,
which record it actually represent
and filter out per user fields so we
don't get to be the record type that is then unusable.
But this allows us to have one constructor.
Or in the case of operators,
finitely many constructors per abstract type family.
Some examples. Int obviously is translated into int,
so the value of 1 would be encoded as lowercase int.
But on the other end,
tuples, for example, the tuple 1 and TRUE,
are encoded with the term tup,
which takes more than just the two arguments for 1 and TRUE.
It fix the tuple size,
which is known to be 2.
Int and bool, which are the types of the first two arguments,
and then it takes the additional arguments equal to the number
of indices up to the maximal index in the specification.
The recovery will then take care
of making sure that because the tuple size is 2,
we only recover the first two fields because those are
the actually present fields in this tuple type.
Now, let's talk about actually encoding types.
How do you do this,he process that I've just hinted at previously?
We use the type-term compatibility,
the syntax that you see here on the screen to encode that term.
This x represents a type, in this case, term.
Let's give you an example and not a definition. Let's see.
You have the tuple type Alpha_1 int and record h to Alpha_2,
and you're in a specification with the maximal tuples as
a four and only two record fields,
of which h is the second.
The encoding for this would be the t,
which is the term that represents the type-term,
is a tuple of
size three because that's the number of fields [inaudible] has,
but it takes four arguments,
c_1 through c_4 because that's
the maximal number of fields in the specification.
However, only c_1 through c_3 have additional constraints that
come from the actual arguments of the tuple type.
C_1 has to be Alpha_1,
and because Alpha_1 is a type variable,
there's no much more we can do besides assign it in
SMT variable a_1 with no additional constraints.
C_2 is an integer because int maps to lowercase integer,
and c_3 is however you resolve
the encoding of the record type h to Alpha_2.
In our case, this is by assigning c_3 to be the record type c_5,
c_6 because NF is 2,
so we have two record fields of which h is the second because
the second c_6 has the additional constraint that encodes Alpha_2.
But because, again, Alpha_2 is an unconstrained type variable,
it just gets assigned to variable a_2.
This is how you would encode type-term.
You get these types that you wish to
encode from built-in operators.
Essentially, with the exception of user-defined operators,
the entirety of a TLS specification is just each chain
of the built-in operator applications.
If we're able to figure out the types of those expressions,
this should give us constraints for the entire specification.
Operators have types ranging from simple to more complex.
For example, plus has the very simple type,
it takes two integers and it returns an integer.
On the other hand, set union is polymorphic,
it takes two sets of
the same kind and returns another set of that same kind.
But it could be anything,
it can take two integer sets or it can take
two sets of strings or it can take two sets of records.
As long as the two arguments are of the same type,
it is valid to apply set union.
The particularity with the set construction operator is that
here we do have an infinite family of set constructors,
but that's not a problem because it's
an infinite family in the type system,
not in the SMT part.
We have one operator priority,
and all of them take n arguments
of the same type and return a set.
Now, what is interesting and different from what
you might have seen is the treatment of certain,
what we call overload operators.
In this case, for example, the tuple constructor.
But overloaded means, is that the single operator,
syntactically, is able to produce
expressions of two different types that are incompatible.
In this case, the tuple constructor has,
basically, two types that make up its,
what we call complex schema.
The first one is a type that takes
two arguments of any types and returns a tuple,
and the second one takes
two arguments of the same type and returns a sequence.
What this basically means is that,
in a vacuum, this operator can be used for either,
but we don't know which it's actually being used
for until we take additional constraints from the context.
I had already used the word schema before.
Schema is what we refer to the type of an operator.
So the type of an operator is called a schema,
and it's primitive if the operator is not overloaded.
The primitive schema basically
declares the type variables that the operator has as polymorphic,
and then tells you the types of
the arguments and the type of returns.
X_1 through X_n are the types of the arguments,
Y is the type of return,
and this operator is
polymorphic and it takes k number of variables.
Or it could be a complex schema which
belongs to an overloaded operator,
which is just a finite collection of primitive schemes.
We'll see later that the complex schemas are really where the,
pun intended, complexity of solving this problem comes.
How do we make a constraint from a known schema?
Well, we compute what is called a schema instance.
The schema instance encodes the fact
that this particular instance of
operator application is compatible with
one of the instantiations of the operator types.
Because the operator is polymorphic in general,
and any particular application has complete arguments,
we just have to make sure that
the instance of this operator is typed correctly.
You can interpret this schema instance as reading a term, t-hat,
encodes the type of the result,
and terms t_1 through t_n encode the types of
the n arguments of the operator to which the schema belongs.
Problem is that we have
disjunctive constraints that come from complex schemas,
and this is really why we need to use SMT because SMT
gives us a nice way of solving disjunctive constraints.
Whereas, in a purely conjunctive setting,
we can maybe use something else, something more efficient.
However, because we're not in that setting,
we have to rely on SMT solver to solve
this set of potentially disjunctive constraints for us.
How do we put all that we've learned together and
actually determine the types of TLA expressions?
We use the similar syntax we were using before to denote
that a term x represents the type of TLA
expression e. The way we do this,
I'm not going to give you definitions,
I'm going to show you by example.
The way we do this, for example,
for literals, is exactly what you would expect.
An integer literal, for example,
42, you can just say that,
if it's trying to be represented by the term x,
then x is an int, and that's the end of it.
More complex, for example,
the application of plus or any other built-in operator.
In that case, we have to analyze three things.
First, we have to figure out the schema instance for
plus for which we compute s plus c_1, c_2, x.
The return of plus,
which is equal to the body
of the expression we're currently analyzing,
has to be represented by x.
For the two arguments,
you want to need two in this case,
we have to create fresh SMT variables,
c_1 and c_2, to represent them.
Then we compute the schema instance.
In addition, we recurse over
all the arguments because the arguments
themselves might be complex expressions,
and we compute their representations as well.
So we compute the encoding of e_1 into c_1,
and we compute the encoding of e_2 into c_2.
For plus, the schema in question here,
s plus, is just int, int to int.
It would tell us that c_1 has to be an int,
c_2 has to be an int, and x has to be an int,
as expected for plus.
The more interesting case is the one
with an overloaded operator, for example.
If we had the expression tuple 1, 2,
we do the same thing as before,
but now the schema instance is different.
Because the operator here is overloaded,
the schema instance is essentially
a disjunction of two different things.
It's a schema instance for s_1 and
a schema instance for s_2, where, here,
s_1 and s_2 are the two primitive schemas that make up
the complex schema which this operator holds.
Everything else is exactly the same,
so we recurse on one,
we recurse on two in exactly the same way.
These two schemas, concretely,
for the tuple constructor,
are the tuple schema s_1,
where we take two arguments and return
a tuple of potentially different types,
and the schema s_2, which we take
two arguments of the same type and return a sequence of that.
We compute both of these constraints for s_1 and for s_2,
and then we just add the structure.
Here is really where the complexity comes from if anywhere.
This is how you would do it.
Of course, there are special cases.
There are cases where you need to manage user-defined operators.
There are cases where you need to
match [inaudible] expressions and stuff like that.
I'm not going to give you expressions for those.
If you're interested, contact me or Igor,
and we'll point you towards our paper.
Now, the question is,
the thing we're doing,
is it actually correct? Or what does that mean?
We have a theorem that says that,
if we manage to find a model and recover types from that model,
the types we recover are sensible.
What that means is that every variable in
the specification is type consistently across all of its uses,
across all of the operators.
Second, although the types that we do infer,
because we infer types for every intermediate expression as well,
are compatible with what the schemas accept.
For example, the schema of
an overloaded operator would
accept a type that's a model type of either one,
and we always get one of those as a result as stated by theorem.
Essentially, this theorem says that the types we get
back from the model are useful and are reasonable.
In conclusion, we provide you
with the tools for either type checking
or type inferring types in your TLA+ specifications,
which you can use to make your work easier,
to make fewer mistakes and catch them quicker.
These tools work in practice in
a reasonable amount of time and return
types which we believe are useful to TLA specification designers.
Thank you for listening. If you have any questions,
please direct them to me or Igor,
and we'll be happy to answer any of them. Thank you very much.