Add requirement for CheckTx in ABCI spec

[sergio-mena]

Contributes to #615 and #24

Following today's discussions with @otrack and @hvanz, we agreed I'd give a try at adding an additional requirement in ABCI spec to restrict the possible app implementations of CheckTx.

This might help simplify the mempool spec, which can refer to this ABCI requirement to become simpler.

The advantage of this approach is that we add this requirement to those we already require all ABCI applications to abide by.

---

PR checklist

• Tests written/updated
• Changelog entry added in .changelog (we use unclog to manage our changelog)
• Updated relevant documentation (docs/ or spec/) and code comments

[jmalicevic]

I assume the point of (b) is to show that a transaction will eventually leave the mempool one way or the other? I did not read the rest of the text in the file, and can't remember whether it is written down, but if it is not, it might be useful to emphasize that here.

[sergio-mena]

Good point. Let me try to clarify that

[jmalicevic]

Where for all times t <= t_stable , the value was OK(CheckTxCode_tx,p,t) ?

[lasarojc]

Good point. Otherwise there will be no stability until stable and if stable can take very long to arrive, we are back to square one in practice.

[sergio-mena]

I would let @otrack and @hvanz chime in here, but I have the impression we cannot require anything from the app before t_stable. This condition is just making sure that we don't oscillate forever: which apps can easily fulfill with e.g., nonces, or ttl. But remember that CheckTx cannot offer strong guarantees when just looking at a particular CheckTx call. BTW, I'm adding a sentence at @jmalicevic's suggestion that hopefully clarifies this point. I will extend that sentence with (parts of) this explanation.

[lasarojc]

I see. Maybe a better name for the property would be "eventual stability" or "eventual non-oscillation", given that it can oscillate for a while.

[sergio-mena]

I had changed it to "finite-oscillation", but I must confess "eventual non-oscillation" sounds sexier... preferences?

[hvanz]

Isn't it more precise to talk about height instead of time? That is, a transaction tx is validated by p's application at a certain height h. The response by the application should be deterministic for tx at height h.

[sergio-mena]

I thought about it. I know the mempool gets height info from Consensus, which is a dependency between the two modules. I used time here in the hope that, one day, we can get rid of height info in the mempool. If you have a strong opinion on this, we can change time for height.

Also, now that I think of it, if we use height, then we need an additional (previous) requirement that the result does not change within one height if executed several times. Actually, I like this two-requirement solution. If you also like it more than what's there I'll change it.

[hvanz]

I thought that it was a requirement that handling CheckTx in the application should be deterministic when validated against the same height. In the section "Specifics of ResponseCheckTx" in this document, it says that the Data field does not need to be deterministic (which btw is not mentioned in proto/tendermint/abci/types.proto). But it doesn't say anything about the code field of the response.

[sergio-mena]

I'd heard rumors (very old, tho, when I was starting) that some apps where updating the "CheckTx state" upon running CheckTx on incoming TXs during a height. No longer sure I did understand at the time.

Anyway, I don't think we were formally specifying CheckTx before this PR (rather, we've been documenting CheckTx)

[lasarojc]

if the transaction stays in the mempool long enough

Does it have to stay in the mempool or could it be added and removed repeatedly before the stabilization?

[sergio-mena]

That's what I understand we're trying to avoid: some nodes saying it's valid, gossiping it, then saying it is invalid... and the TX circulating around the p2p network but always disappearing them moment it is to be proposed.
Check the latest version, where I try to clarify that.

[hvanz]

If the transaction is removed and added again, it will need to pass through CheckTx, with the possibility to be rejected the second time. If it stays "long enough" in the mempool, without being rechecked, most probably it will eventually become invalid, while in the mempool.

[jmalicevic]

I have been thinking about this stateless requirement. And somehow I am not sure it is actually true. I know it should be stateless to be more lightweight, but the sole fact that it can become invalid upon calling CheckTx on RecheckTx seems to indicate the call in fact is not stateless because the response changes based on the state change between heights.

[sergio-mena]

Remember RecheckTx is something you can enable or disable. My understanding is that it should be disabled for app that do stateless CheckTx.

However, your comment made me think of something I hadn't thought about before: should the spec consider CheckTx and RecheckTx as different? If yes, is there any requirement we want to impose in how they must relate?

[jmalicevic]

My understanding is that it should be disabled for app that do stateless CheckTx.

If this is indeed the rule, I believe it should be written down. Maybe it is and I just have not read it. Beacuse otherwise you end up with questions such as mine :)

Then if RecheckTx is enabled, I feel that the check is stateless within a height (because you are not supposed to change the state in the first place), but then the requirement a) should be relaxed such that it is allowed to not succeed only if a block was committed.

[cason]

should the spec consider CheckTx and RecheckTx as different?

Yes, in my opinion.

If yes, is there any requirement we want to impose in how they must relate?

I agree with Jasmina's comments below. If the state of the application hasn't change between CheckTx and ReCheckTx for the same transaction, their output should be the same. In other words, in the absence of state changes (probably we can refer this using heights to indicate state changes), ReCheckTx should be handled as it was a duplicated/second call to CheckTx.

[cason]

Regarding the text specifically, I think that condition (a) prevents the application to implement replay protection mechanisms. And our assumption is kind of that is mandatory the application to implement such mechanisms.

I wonder how we can state condition (a) in a way it still allows the application to reject tx in the case the same tx has already been included in a committed block.

[sergio-mena]

(a) prevents the application to implement replay protection mechanisms

If your app implements replay protection mechanisms, then you must go for (b). I wrote (a) in case the app is OK with a TX being delivered more than once (think of a dead-simple app).

[otrack]

I also believe that it should be about the height and not the time at which the call is made. Moreover, in my view the two requirements can be merged into a single one:

In every run, there is a height after which CheckTx always returns the same value.

This invariant ensures that INV4 in the mempool specification is achievable. INV4 is necessary for a transaction to eventually leave the mempool while doing something useful, that is either committed, or forever invalid. These modifications to the knowledge base are detailing such a point.

[lasarojc]

wrt to

In every run, there is a height after which CheckTx always returns the same value.

what does "after" mean? A possibility would be to consider the height "done" once recheckTx has returned after the agreeing of the corresponding block.

Also, on something that @hvanz asked earlier, during the same height (i.e. in between two recheckTx), does checkTx need to return the same value (supposed the height takes long enough for the tx to be expunged and received again)? That is, does the check change its result based only on the agreed blocks or could it depend on some other condition, such as the size of the mempool? If the first, how could a mempool size cap be implemented while not violating the requirements?

While I see why we would want to not use time, I am not sure using height is the best option since it strengthens the dependency of the mempool on the consensus and I would rather go the other way.
We could instead introduce some logical time, monotonically increasing, which could be implemented using wall clock or height, but doesn't have to be either. Or we could phrase the requirements in terms of invocations of checkTx:

eventually every two consecutive invocations of checkTx return the same value.

[otrack]

what does "after" mean? A possibility would be to consider the height "done" once recheckTx has returned after the agreeing of the corresponding block.

The term "after" refers to heights which are higher than the limit one. Formally, one would write things this way for some process $p$:

$\exists b \in \{true,false\}. \exists h_0 \in \mathbb{N}. \square(p.height &gt; h_0 \implies p.app.checkTx(tx) = b)$

The height corresponds to the value in the consensus module. A cached version of this value (refreshed often enough) works also.

Also, on something that @hvanz asked earlier, during the same height (i.e. in between two recheckTx), does checkTx need to return the same value (supposed the height takes long enough for the tx to be expunged and received again)? That is, does the check change its result based only on the agreed blocks or could it depend on some other condition, such as the size of the mempool? If the first, how could a mempool size cap be implemented while not violating the requirements?

There is no need that a call to $checkTx$ returns twice the same value. After all, such a call is optimistic and might reflect some copy of the application state on which the verification is made. For instance, if $tx1$ enables $tx0$ then checking $tx0$ when $tx1$ is not present returns first $false$. Once $tx1$ is added, $tx0$ can be checked again (e.g., it is received a second time and the cache overflown). This second verification returns $true$.

Stronger requirements are also possible, but in my view applications might be interested with this freedom. For instance, they can try to optimize incoming transactions for better throughput. Such a things would not be possible if we ask that $checkTx$ is deterministic per height.

While I see why we would want to not use time, I am not sure using height is the best option since it strengthens the dependency of the mempool on the consensus and I would rather go the other way. We could instead introduce some logical time, monotonically increasing, which could be implemented using wall clock or height, but doesn't have to be either. Or we could phrase the requirements in terms of invocations of checkTx:

The height captures the progress on the application: the higher it is, the more the application progresses. It is also possible to state things using time. In my view, because the client application "ticks" wrt. the height, it is more accurate to refer to this logical time.

[cason]

I have left some comments, also addressed by other reviewers.

I think we should add a subsection, as this requirement has a different purpose than the other requirements. Essentially, it is not a safety requirement, but more a liveness or performance requirement. I am not really sure where it should fit in the current spec organization, but I am pretty sure we shouldn't mix it with the existent requirements.

[cason]

The return value, or return code, not necessarily an error.

[cason]

should the spec consider CheckTx and RecheckTx as different?

Yes, in my opinion.

If yes, is there any requirement we want to impose in how they must relate?

I agree with Jasmina's comments below. If the state of the application hasn't change between CheckTx and ReCheckTx for the same transaction, their output should be the same. In other words, in the absence of state changes (probably we can refer this using heights to indicate state changes), ReCheckTx should be handled as it was a duplicated/second call to CheckTx.

[cason]

Regarding the text specifically, I think that condition (a) prevents the application to implement replay protection mechanisms. And our assumption is kind of that is mandatory the application to implement such mechanisms.

I wonder how we can state condition (a) in a way it still allows the application to reject tx in the case the same tx has already been included in a committed block.

[cason]

Is that including the possibility of tx been included in a committed block? This should be, in my opinion, provided as the main example of when/how a transaction becomes "forever" invalid.

[sergio-mena]

The PR is trying to provide requirements to the mempool without having to link it to consensus. If that's possible, I prefer it that way (more modular)

[cason]

I didn't fully get the point here. The requirement applies to all processes, but the time at which a transaction becomes invalid may change over processes, right?

Having saying so, my opinion here is that we should replace (clock) times by heights, which represent logical times. This would in particular enable removing this observation. While in fact different processes reach the same height at different times, from that height they should "forever" reject the transaction.

[sergio-mena]

but the time at which a transaction becomes invalid may change over processes, right?

The current version does so. It is a property local to a process, as a first version. If a local requirement is enough, we shouldn't complicate it with a global version. A local requirement is easier to understand (esp, for people less familiar with distributed systems), and check or prove.

The question (to @hvanz and @otrack) is, is the requirement expressed in local terms enough?

[sergio-mena]

In every run, there is a height after which CheckTx always returns the same value.

@otrack this is slightly different (actually, weaker) than what the text of this PR is currently stating ([b] currently requires the TX to eventually fail). But I trust you folks on what we need to require from the App, which I believe will be an assumption in the mempool spec. So, will adapt the text accordingly.

Will also review the new text shortly

[cason]

I think here is not OK(CheckTxCode) but only CheckTxCode_tx,p,h.

[sergio-mena]

What you propose is stronger. I prefer the weakest form that is useful for the spec

[hvanz]

One of the allowed cases here is that the transaction will become valid forever, which is a bit strange if it was invalid at some point before. I mean, in a trivial application such as a kv-store, we have transactions whose validity never changes; they are valid (or invalid) all the time. In a non-trivial application, a transaction is valid possibly during one or multiple periods of time/height. First the transaction is invalid, at some height it will become valid, then at a later height invalid again, then it's valid and committed to a block, at which point is invalid forever.

[cason]

One of the allowed cases here is that the transaction will become valid forever, which is a bit strange if it was invalid at some point before.

I don't think it is that strange. Assume that validity checks the existence of an account used by the transaction. While the account doesn't exist, the transaction is invalid. Once the account is created by another transaction, the transaction becomes valid. A process may receive the transaction while it is lagging behind in the blockchain, so that the transaction creating the account was not yet processed (e.g. delivered) to this process.

[cason]

I mean, in a trivial application such as a kv-store, we have transactions whose validity never changes; they are valid (or invalid) all the time.

In the case of a stateless verification, the validity of a transaction never changes. This means that the property above is always valid, as the verification is timeless/stateless.

[hvanz]

it ensures that a transaction will leave the mempool of all full nodes

We cannot ensure that from Requirement 14. This requirement allows two different processes to non-oscillate at different validity values. One process may stabilize on valid while the other on invalid, and not necessarily at the same time/height. To be able to talk about a global property, I think we cannot avoid talking about transactions committed to the chain, as in INV4.

[cason]

One process may stabilize on valid while the other on invalid, and not necessarily at the same time/height.

Why? Since we are using heights and the application is deterministic, the output at the beginning of a given height should be exactly the same.

The problem I see in those properties is that a statefull validation is dependent on the order at which transactions are verified. In particular, Req. 13 is hard to fulfill given this assumption. The most simpler examples regards duplication: if tx is checked twice against the application, for instance because the mempool fails preventing duplication, a stateful application should reject the second "copy" of the transaction.

[cason]

To be able to talk about a global property, I think we cannot avoid talking about transactions committed to the chain

Agreed.

[sergio-mena]

The sentence in the text going from a local property (the requirement) to a global one was to explain that we only need a local property to obtain a global one. Of course as you rightly point out in your comments, the global property does not trivially follow from the local one. You need other things (such as consensus agreement) to prove it, but I left that of of the text... maybe by trying to be concise, I ended up being unclear

[hvanz]

Yes, there is an implicit assumption related to consensus, which is needed to prove the global property from the local one. I think it will be more clear if we just add a phrase like "assuming two different applications have the same state after transitioning to the same height h".

[cason]

I am afraid we are walking in circles regarding the wording of these additional requirements. Should we try to schedule a synchronous meeting to discuss them?

[cason]

This requirement is somehow preventing the application from implementing replay protection, right?

[sergio-mena]

I don't think so. Replay protection involves different heights

[cason]

Why the height is associated to a particular process? The advantage of using heights instead of time is to make the property global. In fact, since applications are deterministic, the outputs produced by different applications at the same height (which is a global parameter) should be the same.

[sergio-mena]

Yes, but I didn't want to make this requirement global. This is aimed at the app devs. I want the requirements addressed to them to be as imple and understandable as possible.
Then, assuming they respect those, we can deduce that a global property emerges (thanks to consensus agreement)... but we shouldn't confuse app devs by introducing all that "complication" here

[otrack]

Requirement 13 asks that the result of checkTx is stateless at a given height. I do not think we actually need it. It is perfectly possible to refer to height, even if the result is non-deterministic. We simply needs convergence over time of thecheckTx call. Requirement 13 also prevents an application to optimize extractable value (see MEV): Consider some height $h$. Let $T$, $T_1$,.. and $T_n$ (with $n$ large) be some set of transactions. Assume that these transactions are all valid at heigh $h$, and if $T$ executes none of the $T_i$ can. Then, Requirement 13 prevents the application to optimise the block mined at $h+1$ to favor $T_1$,.., $T_n$.

Requirement 14 is local to a process, which I believe is appealing. Notice that if Requirement 13 holds then one may show that the following is true: for any transaction $T$, there exists a heigh $h_0$, and a boolean $b$, such that for any heigh $h&gt;h_0$, $checkTx(T,h)=b$ at any correct process. (This is the requirement I was proposing above.) If we maintain Requirement 13, then I am fine with the wording of Requirement 14. Otherwise, in my view, we should assk for the the global invariant.

nb. as @cason proposed, maybe it would be best that we discuss about this matter to reach an agreement.

[josef-widder]

I think the order is not what is intended here. From the requirement as written here, all tx must have the same b. From the English text below it seems that you want:
for all tx, exists b, exists h, forall p
This also would mean that from some height on, all processes agree on the outcome. This should also be highlighted.

[sergio-mena]

Yes. This was the result of a long discussion yesterday. Initially, I wanted to keep b global and $h_{stable}$ local to the process... but the wording of the requirement became very cumbersome, with several nested "there exists" and "for all". So I decided to leave $h_{stable}$ global to simplify the requirement's wording (and explain in the text that it can just be implemented locally).

Now, your comment is accurate and the reason is that the "There exists" at the beginning is a left-over from when I was trying a local $h_{stable}$.

Let me fix that...

[otrack]

I agree with Josef that the quantifier for $b$ is misplaced. The formula should be

$\forall tx \in Txs. \exists b \in \{true,false\}. \forall p \in correct. \exists h_0 \in \mathbb{N}. \square(p.height &gt; h_0 \implies p.app.checkTx(tx) = b)$ (1)

Alternatively, as proposed earlier, one may also define a height for all the processes. In that case, the formula reads:

$\forall tx \in Txs. \exists b \in \{true,false\}. \exists h_0 \in \mathbb{N}. \forall p \in correct. \square(p.height &gt; h_0 \implies p.app.checkTx(tx) = b)$ (2)

As we discussed, (1) implies (2). So, the weaker the better for the programmer.

[sergio-mena]

Fixed. Please take a look

[josef-widder]

Looks good. I still would add a comment on that all processes must agree on that stable value of b.

[otrack]

I am fine also with the current text.

Regarding "agreement", I am not sure because the term refers to some form of distributed coordination among processes, whereas determinism (or a stable property) is enough here.

[sergio-mena]

@otrack Yes, I tried (1) first but, unlike in the notation you are using, in a notation consistent with the rest of the ABCI spec (all requirements) above I found it very hard to understand... so in the end I went for (2), and explain that, in practice, App devs can just enforce (1)... since as you say (1) implies (2).

We could adapt the whole spec to use a more advanced notation as the one you are using, but I'm not sure now's the moment to do that.

[sergio-mena]

Looks good. I still would add a comment on that all processes must agree on that stable value of b.

I added a sentence at the end

[josef-widder]

Thanks! The new sentence looks good. I think it makes sense that you didn't use the term agree, for the reasons @otrack mentioned above.

[otrack]

I agree with Josef that the quantifier for $b$ is misplaced. The formula should be

$\forall tx \in Txs. \exists b \in \{true,false\}. \forall p \in correct. \exists h_0 \in \mathbb{N}. \square(p.height &gt; h_0 \implies p.app.checkTx(tx) = b)$ (1)

Alternatively, as proposed earlier, one may also define a height for all the processes. In that case, the formula reads:

$\forall tx \in Txs. \exists b \in \{true,false\}. \exists h_0 \in \mathbb{N}. \forall p \in correct. \square(p.height &gt; h_0 \implies p.app.checkTx(tx) = b)$ (2)

As we discussed, (1) implies (2). So, the weaker the better for the programmer.

[otrack]

As a general note, is there some documentation about the ABCI requirements? They are not easy to parse (for instance, this one is clearly difficult) and some documentation / base examples would help the programmer.

[sergio-mena]

As a general note, is there some documentation about the ABCI requirements? They are not easy to parse (for instance, this one is clearly difficult) and some documentation / base examples would help the programmer.

All ABCI requirements we have come up with so far are in this page. @nenadmilosevic95 also wrote some extreme cases (from the point of view of the App) to help app developers understand "uncommon runs" their code needs to support