spec(abci): slight improvements to ABCI spec (@Angrav's feedback from…

… Anoma) (cometbft#2929)

---

#### PR checklist

- [ ] ~~Tests written/updated~~
- [ ] ~~Changelog entry added in `.changelog` (we use
[unclog](https://github.com/informalsystems/unclog) to manage our
changelog)~~
- [x] Updated relevant documentation (`docs/` or `spec/`) and code
comments
- [x] Title follows the [Conventional
Commits](https://www.conventionalcommits.org/en/v1.0.0/) spec

---------

Co-authored-by: Andy Nogueira <[email protected]>

spec/abci/abci++_basic_concepts.md

@@ -123,6 +123,8 @@ call sequences of these methods.
   update its state accordingly. Cryptographic commitments to the block and transaction results,
   returned via the corresponding parameters in `FinalizeBlockResponse`, are included in the header
   of the next block. CometBFT calls it when a new block is decided.
+  When calling `FinalizeBlock` with a block, the consensus algorithm run by CometBFT guarantees
+  that at least one non-byzantine validator has run `ProcessProposal` on that block.
 
 - [**Commit:**](./abci++_methods.md#commit) Instructs the Application to persist its
   state. It is a fundamental part of CometBFT's crash-recovery mechanism that ensures the

spec/abci/abci++_comet_expected_behavior.md

@@ -157,14 +157,17 @@ did not store any state CometBFT calls `InitChain`. After this, CometBFT enters
   `FinalizeBlock`, followed by a call to `Commit`. In each round, the sequence of method calls
   depends on whether the local process is the proposer or not. Note that, if a height contains zero
   rounds, this means the process is replaying an already decided value (catch-up mode).
+  When calling `FinalizeBlock` with a block, the consensus algorithm run by CometBFT guarantees
+  that at least one non-byzantine validator has run `ProcessProposal` on that block.
+
 
 >```abnf
 >consensus-height    = *consensus-round finalize-block commit
 >consensus-round     = proposer / non-proposer
 >```
 
 * For every round, if the local process is the proposer of the current round, CometBFT calls `PrepareProposal`.
-  A successful execution of `PrepareProposal` implies in a proposal block being (i)signed and (ii)stored
+  A successful execution of `PrepareProposal` results in a proposal block being (i) signed and (ii) stored
   (e.g., in stable storage).
 
   A crash during this step will direct how the node proceeds the next time it is executed, for the same round, after restarted.
@@ -187,7 +190,10 @@ did not store any state CometBFT calls `InitChain`. After this, CometBFT enters
 >```
 
 * Also for every round, if the local process is _not_ the proposer of the current round, CometBFT
-  will call `ProcessProposal` at most once. At most one call to `ExtendVote` may occur only after
+  will call `ProcessProposal` at most once.
+  Under certain conditions, CometBFT may not call `ProcessProposal` in a round;
+  see [this section](./abci++_example_scenarios.md#scenario-3) for an example.
+  At most one call to `ExtendVote` may occur only after
   `ProcessProposal` is called. A number of calls to `VerifyVoteExtension` can occur in any order
   with respect to `ProcessProposal` and `ExtendVote` throughout the round. The reasons are the same
   as above, namely, the process running slightly late in the current round, or votes from future

spec/abci/abci++_methods.md

@@ -625,7 +625,7 @@ without calling `VerifyVoteExtension` to verify it.
 * **Usage**:
     * Contains the fields of the newly decided block.
     * This method is equivalent to the call sequence `BeginBlock`, [`DeliverTx`],
-      and `EndBlock` in the previous version of ABCI.
+      and `EndBlock` in ABCI 1.0.
     * The height and time values match the values from the header of the proposed block.
     * The Application can use `FinalizeBlockRequest.decided_last_commit` and `FinalizeBlockRequest.misbehavior`
       to determine rewards and punishments for the validators.
@@ -661,6 +661,8 @@ without calling `VerifyVoteExtension` to verify it.
       making the Application's state evolve in the context of state machine replication.
     * Currently, CometBFT will fill up all fields in `FinalizeBlockRequest`, even if they were
       already passed on to the Application via `PrepareProposalRequest` or `ProcessProposalRequest`.
+    * When calling `FinalizeBlock` with a block, the consensus algorithm run by CometBFT guarantees
+      that at least one non-byzantine validator has run `ProcessProposal` on that block.
 
 #### When does CometBFT call `FinalizeBlock`?