Merge branch 'master' into thane/fix-protogen

.github/CODEOWNERS

@@ -7,4 +7,7 @@
 # global owners are only requested if there isn't a more specific
 # codeowner specified below. For this reason, the global codeowners
 # are often repeated in package-level definitions.
-*      @ebuchman @cmwaters @tychoish @williambanfield @creachadair
+*       @ebuchman @cmwaters @tychoish @williambanfield @creachadair @sergio-mena @jmalicevic @thanethomson @ancazamfir
+
+# Spec related changes can be approved by the protocol design team
+/spec   @josef-widder @milosevic @cason

CHANGELOG.md

@@ -2,6 +2,27 @@
 
 Friendly reminder: We have a [bug bounty program](https://hackerone.com/cosmos).
 
+## v0.35.2
+
+February 28, 2022
+
+Special thanks to external contributors on this release: @ashcherbakov, @yihuang, @waelsy123
+
+### IMPROVEMENTS
+
+- [consensus] [\#7875](https://github.com/tendermint/tendermint/pull/7875) additional timing metrics. (@williambanfield)
+
+### BUG FIXES
+
+- [abci] [\#7990](https://github.com/tendermint/tendermint/pull/7990) revert buffer limit change. (@williambanfield)
+- [cli] [#7837](https://github.com/tendermint/tendermint/pull/7837) fix app hash in state rollback. (@yihuang)
+- [cli] [\#7869](https://github.com/tendermint/tendermint/pull/7869) Update unsafe-reset-all command to match release v35. (waelsy123)
+- [light] [\#7640](https://github.com/tendermint/tendermint/pull/7640) Light Client: fix absence proof verification (@ashcherbakov)
+- [light] [\#7641](https://github.com/tendermint/tendermint/pull/7641) Light Client: fix querying against the latest height (@ashcherbakov)
+- [mempool] [\#7718](https://github.com/tendermint/tendermint/pull/7718) return duplicate tx errors more consistently. (@tychoish)
+- [rpc] [\#7744](https://github.com/tendermint/tendermint/pull/7744) fix layout of endpoint list. (@creachadair)
+- [statesync] [\#7886](https://github.com/tendermint/tendermint/pull/7886) assert app version matches. (@cmwaters)
+
 ## v0.35.1
 
 January 26, 2022

Makefile

@@ -240,9 +240,7 @@ build-docs:
 		mkdir -p ~/output/$${path_prefix} ; \
 		cp -r .vuepress/dist/* ~/output/$${path_prefix}/ ; \
 		cp ~/output/$${path_prefix}/index.html ~/output ; \
-	done < versions ; \
-	mkdir -p ~/output/master ; \
-	cp -r .vuepress/dist/* ~/output/master/
+	done < versions ;
 .PHONY: build-docs
 
 ###############################################################################
@@ -349,3 +347,4 @@ split-test-packages:$(BUILDDIR)/packages.txt
 	split -d -n l/$(NUM_SPLIT) $< $<.
 test-group-%:split-test-packages
 	cat $(BUILDDIR)/packages.txt.$* | xargs go test -mod=readonly -timeout=5m -race -coverprofile=$(BUILDDIR)/$*.profile.out
+

docs/architecture/README.md

@@ -86,13 +86,16 @@ Note the context/background should be written in the present tense.
 - [ADR-075: RPC Event Subscription Interface](./adr-075-rpc-subscription.md)
 - [ADR-076: Combine Spec and Tendermint Repositories](./adr-076-combine-spec-repo.md)
 
+### Deprecated
+
+None
+
 ### Rejected
 
 - [ADR-023: ABCI-Propose-tx](./adr-023-ABCI-propose-tx.md)
 - [ADR-029: Check-Tx-Consensus](./adr-029-check-tx-consensus.md)
 - [ADR-058: Event-Hashing](./adr-058-event-hashing.md)
 
-
 ### Proposed
 
 - [ADR-007: Trust-Metric-Usage](./adr-007-trust-metric-usage.md)

docs/architecture/adr-075-rpc-subscription.md

@@ -2,6 +2,7 @@
 
 ## Changelog
 
+- 01-Mar-2022: Update long-polling interface (@creachadair).
 - 10-Feb-2022: Updates to reflect implementation.
 - 26-Jan-2022: Marked accepted.
 - 22-Jan-2022: Updated and expanded (@creachadair).
@@ -347,8 +348,8 @@ limit.
 
 The `wait_time` parameter is used to effect polling. If `before` is empty and
 no items are available, the server will wait for up to `wait_time` for matching
-items to arrive at the head of the log. If `wait_time` is zero, the server will
-return whatever eligible items are available immediately.
+items to arrive at the head of the log. If `wait_time` is zero or negative, the
+server will wait for a default (positive) interval.
 
 If `before` non-empty, `wait_time` is ignored: new results are only added to
 the head of the log, so there is no need to wait.  This allows the client to

docs/architecture/adr-template.md

@@ -6,12 +6,30 @@
 
 ## Status
 
-> A decision may be "proposed" if it hasn't been agreed upon yet, or "accepted"
-> once it is agreed upon. Once the ADR has been implemented mark the ADR as
-> "implemented". If a later ADR changes or reverses a decision, it may be marked
-> as "deprecated" or "superseded" with a reference to its replacement.
+> An architecture decision is considered "proposed" when a PR containing the ADR
+> is submitted. When merged, an ADR must have a status associated with it, which
+> must be one of: "Accepted", "Rejected", "Deprecated" or "Superseded".
+>
+> An accepted ADR's implementation status must be tracked via a tracking issue,
+> milestone or project board (only one of these is necessary). For example:
+>
+>     Accepted
+>
+>     [Tracking issue](https://github.com/tendermint/tendermint/issues/123)
+>     [Milestone](https://github.com/tendermint/tendermint/milestones/123)
+>     [Project board](https://github.com/orgs/tendermint/projects/123)
+>
+> Rejected ADRs are captured as a record of recommendations that we specifically
+> do not (and possibly never) want to implement. The ADR itself must, for
+> posterity, include reasoning as to why it was rejected.
+>
+> If an ADR is deprecated, simply write "Deprecated" in this section. If an ADR
+> is superseded by one or more other ADRs, provide local a reference to those
+> ADRs, e.g.:
+>
+>     Superseded by [ADR 123](./adr-123.md)
 
-{Deprecated|Declined|Accepted|Implemented}
+Accepted | Rejected | Deprecated | Superseded by
 
 ## Context
 

docs/versions

@@ -1,3 +1,4 @@
+master                  master
 v0.33.x                 v0.33
 v0.34.x                 v0.34
 v0.35.x                 v0.35

internal/consensus/common_test.go

@@ -370,7 +370,11 @@ func subscribeToVoter(ctx context.Context, t *testing.T, cs *State, addr []byte)
 		vote := msg.Data().(types.EventDataVote)
 		// we only fire for our own votes
 		if bytes.Equal(addr, vote.Vote.ValidatorAddress) {
-			ch <- msg
+			select {
+			case <-ctx.Done():
+				return ctx.Err()
+			case ch <- msg:
+			}
 		}
 		return nil
 	}, types.EventQueryVote); err != nil {
@@ -401,7 +405,10 @@ func subscribeToVoterBuffered(ctx context.Context, t *testing.T, cs *State, addr
 			vote := msg.Data().(types.EventDataVote)
 			// we only fire for our own votes
 			if bytes.Equal(addr, vote.Vote.ValidatorAddress) {
-				ch <- msg
+				select {
+				case <-ctx.Done():
+				case ch <- msg:
+				}
 			}
 		}
 	}()

internal/consensus/reactor_test.go

@@ -188,10 +188,17 @@ func waitForAndValidateBlock(
 
 	ctx, cancel := context.WithCancel(bctx)
 	defer cancel()
+
 	fn := func(j int) {
 		msg, err := blocksSubs[j].Next(ctx)
-		if !assert.NoError(t, err) {
-			cancel()
+		switch {
+		case errors.Is(err, context.DeadlineExceeded):
+			return
+		case errors.Is(err, context.Canceled):
+			return
+		case err != nil:
+			cancel() // terminate other workers
+			require.NoError(t, err)
 			return
 		}
 
@@ -217,6 +224,10 @@ func waitForAndValidateBlock(
 	}
 
 	wg.Wait()
+
+	if err := ctx.Err(); errors.Is(err, context.DeadlineExceeded) {
+		t.Fatal("encountered timeout")
+	}
 }
 
 func waitForAndValidateBlockWithTx(
@@ -236,8 +247,14 @@ func waitForAndValidateBlockWithTx(
 		ntxs := 0
 		for {
 			msg, err := blocksSubs[j].Next(ctx)
-			if !assert.NoError(t, err) {
-				cancel()
+			switch {
+			case errors.Is(err, context.DeadlineExceeded):
+				return
+			case errors.Is(err, context.Canceled):
+				return
+			case err != nil:
+				cancel() // terminate other workers
+				t.Fatalf("problem waiting for %d subscription: %v", j, err)
 				return
 			}
 
@@ -268,6 +285,9 @@ func waitForAndValidateBlockWithTx(
 	}
 
 	wg.Wait()
+	if err := ctx.Err(); errors.Is(err, context.DeadlineExceeded) {
+		t.Fatal("encountered timeout")
+	}
 }
 
 func waitForBlockWithUpdatedValsAndValidateIt(
@@ -287,8 +307,14 @@ func waitForBlockWithUpdatedValsAndValidateIt(
 
 		for {
 			msg, err := blocksSubs[j].Next(ctx)
-			if !assert.NoError(t, err) {
-				cancel()
+			switch {
+			case errors.Is(err, context.DeadlineExceeded):
+				return
+			case errors.Is(err, context.Canceled):
+				return
+			case err != nil:
+				cancel() // terminate other workers
+				t.Fatalf("problem waiting for %d subscription: %v", j, err)
 				return
 			}
 
@@ -311,6 +337,9 @@ func waitForBlockWithUpdatedValsAndValidateIt(
 	}
 
 	wg.Wait()
+	if err := ctx.Err(); errors.Is(err, context.DeadlineExceeded) {
+		t.Fatal("encountered timeout")
+	}
 }
 
 func ensureBlockSyncStatus(t *testing.T, msg tmpubsub.Message, complete bool, height int64) {
@@ -342,6 +371,8 @@ func TestReactorBasic(t *testing.T) {
 	}
 
 	var wg sync.WaitGroup
+	errCh := make(chan error, len(rts.subs))
+
 	for _, sub := range rts.subs {
 		wg.Add(1)
 
@@ -349,14 +380,32 @@ func TestReactorBasic(t *testing.T) {
 		go func(s eventbus.Subscription) {
 			defer wg.Done()
 			_, err := s.Next(ctx)
-			if !assert.NoError(t, err) {
-				cancel()
+			switch {
+			case errors.Is(err, context.DeadlineExceeded):
+				return
+			case errors.Is(err, context.Canceled):
+				return
+			case err != nil:
+				errCh <- err
+				cancel() // terminate other workers
+				return
 			}
 		}(sub)
 	}
 
 	wg.Wait()
+	if err := ctx.Err(); errors.Is(err, context.DeadlineExceeded) {
+		t.Fatal("encountered timeout")
+	}
+	select {
+	case err := <-errCh:
+		if err != nil {
+			t.Fatal(err)
+		}
+	default:
+	}
 
+	errCh = make(chan error, len(rts.blocksyncSubs))
 	for _, sub := range rts.blocksyncSubs {
 		wg.Add(1)
 
@@ -364,8 +413,14 @@ func TestReactorBasic(t *testing.T) {
 		go func(s eventbus.Subscription) {
 			defer wg.Done()
 			msg, err := s.Next(ctx)
-			if !assert.NoError(t, err) {
-				cancel()
+			switch {
+			case errors.Is(err, context.DeadlineExceeded):
+				return
+			case errors.Is(err, context.Canceled):
+				return
+			case err != nil:
+				errCh <- err
+				cancel() // terminate other workers
 				return
 			}
 			ensureBlockSyncStatus(t, msg, true, 0)
@@ -373,6 +428,17 @@ func TestReactorBasic(t *testing.T) {
 	}
 
 	wg.Wait()
+	if err := ctx.Err(); errors.Is(err, context.DeadlineExceeded) {
+		t.Fatal("encountered timeout")
+	}
+
+	select {
+	case err := <-errCh:
+		if err != nil {
+			t.Fatal(err)
+		}
+	default:
+	}
 }
 
 func TestReactorWithEvidence(t *testing.T) {
@@ -709,7 +775,7 @@ func TestReactorVotingPowerChange(t *testing.T) {
 }
 
 func TestReactorValidatorSetChanges(t *testing.T) {
-	ctx, cancel := context.WithTimeout(context.Background(), time.Minute)
+	ctx, cancel := context.WithTimeout(context.Background(), 2*time.Minute)
 	defer cancel()
 
 	cfg := configSetup(t)
@@ -752,7 +818,11 @@ func TestReactorValidatorSetChanges(t *testing.T) {
 		go func(s eventbus.Subscription) {
 			defer wg.Done()
 			_, err := s.Next(ctx)
-			if !assert.NoError(t, err) {
+			switch {
+			case err == nil:
+			case errors.Is(err, context.DeadlineExceeded):
+			default:
+				t.Log(err)
 				cancel()
 			}
 		}(sub)
@@ -760,6 +830,17 @@ func TestReactorValidatorSetChanges(t *testing.T) {
 
 	wg.Wait()
 
+	// after the wait returns, either there was an error with a
+	// subscription (very unlikely, and causes the context to be
+	// canceled manually), there was a timeout and the test's root context
+	// was canceled (somewhat likely,) or the test can proceed
+	// (common.)
+	if err := ctx.Err(); errors.Is(err, context.DeadlineExceeded) {
+		t.Fatal("encountered timeout")
+	} else if errors.Is(err, context.Canceled) {
+		t.Fatal("subscription encountered unexpected error")
+	}
+
 	newValidatorPubKey1, err := states[nVals].privValidator.GetPubKey(ctx)
 	require.NoError(t, err)
 

internal/consensus/wal_generator.go

@@ -30,8 +30,10 @@ import (
 // stripped down version of node (proxy app, event bus, consensus state) with a
 // persistent kvstore application and special consensus wal instance
 // (byteBufferWAL) and waits until numBlocks are created.
-// If the node fails to produce given numBlocks, it returns an error.
-func WALGenerateNBlocks(ctx context.Context, t *testing.T, logger log.Logger, wr io.Writer, numBlocks int) (err error) {
+// If the node fails to produce given numBlocks, it fails the test.
+func WALGenerateNBlocks(ctx context.Context, t *testing.T, logger log.Logger, wr io.Writer, numBlocks int) {
+	t.Helper()
+
 	cfg := getConfig(t)
 
 	app := kvstore.NewPersistentKVStoreApplication(logger, filepath.Join(cfg.DBDir(), "wal_generator"))
@@ -46,35 +48,37 @@ func WALGenerateNBlocks(ctx context.Context, t *testing.T, logger log.Logger, wr
 	privValidatorStateFile := cfg.PrivValidator.StateFile()
 	privValidator, err := privval.LoadOrGenFilePV(privValidatorKeyFile, privValidatorStateFile)
 	if err != nil {
-		return err
+		t.Fatal(err)
 	}
 	genDoc, err := types.GenesisDocFromFile(cfg.GenesisFile())
 	if err != nil {
-		return fmt.Errorf("failed to read genesis file: %w", err)
+		t.Fatal(fmt.Errorf("failed to read genesis file: %w", err))
 	}
 	blockStoreDB := dbm.NewMemDB()
 	stateDB := blockStoreDB
 	stateStore := sm.NewStore(stateDB)
 	state, err := sm.MakeGenesisState(genDoc)
 	if err != nil {
-		return fmt.Errorf("failed to make genesis state: %w", err)
+		t.Fatal(fmt.Errorf("failed to make genesis state: %w", err))
 	}
 	state.Version.Consensus.App = kvstore.ProtocolVersion
 	if err = stateStore.Save(state); err != nil {
-		t.Error(err)
+		t.Fatal(err)
 	}
 
 	blockStore := store.NewBlockStore(blockStoreDB)
 
 	proxyApp := proxy.NewAppConns(abciclient.NewLocalCreator(app), logger.With("module", "proxy"), proxy.NopMetrics())
 	if err := proxyApp.Start(ctx); err != nil {
-		return fmt.Errorf("failed to start proxy app connections: %w", err)
+		t.Fatal(fmt.Errorf("failed to start proxy app connections: %w", err))
 	}
+	t.Cleanup(proxyApp.Wait)
 
 	eventBus := eventbus.NewDefault(logger.With("module", "events"))
 	if err := eventBus.Start(ctx); err != nil {
-		return fmt.Errorf("failed to start event bus: %w", err)
+		t.Fatal(fmt.Errorf("failed to start event bus: %w", err))
 	}
+	t.Cleanup(func() { eventBus.Stop(); eventBus.Wait() })
 
 	mempool := emptyMempool{}
 	evpool := sm.EmptyEvidencePool{}
@@ -91,22 +95,24 @@ func WALGenerateNBlocks(ctx context.Context, t *testing.T, logger log.Logger, wr
 	wal := newByteBufferWAL(logger, NewWALEncoder(wr), int64(numBlocks), numBlocksWritten)
 	// see wal.go#103
 	if err := wal.Write(EndHeightMessage{0}); err != nil {
-		t.Error(err)
+		t.Fatal(err)
 	}
 
 	consensusState.wal = wal
 
 	if err := consensusState.Start(ctx); err != nil {
-		return fmt.Errorf("failed to start consensus state: %w", err)
+		t.Fatal(fmt.Errorf("failed to start consensus state: %w", err))
 	}
+	t.Cleanup(consensusState.Wait)
+
+	defer consensusState.Stop()
+	timer := time.NewTimer(time.Minute)
+	defer timer.Stop()
 
 	select {
 	case <-numBlocksWritten:
-		consensusState.Stop()
-		return nil
-	case <-time.After(1 * time.Minute):
-		consensusState.Stop()
-		return fmt.Errorf("waited too long for tendermint to produce %d blocks (grep logs for `wal_generator`)", numBlocks)
+	case <-timer.C:
+		t.Fatal(fmt.Errorf("waited too long for tendermint to produce %d blocks (grep logs for `wal_generator`)", numBlocks))
 	}
 }
 
@@ -115,9 +121,7 @@ func WALWithNBlocks(ctx context.Context, t *testing.T, logger log.Logger, numBlo
 	var b bytes.Buffer
 	wr := bufio.NewWriter(&b)
 
-	if err := WALGenerateNBlocks(ctx, t, logger, wr, numBlocks); err != nil {
-		return []byte{}, err
-	}
+	WALGenerateNBlocks(ctx, t, logger, wr, numBlocks)
 
 	wr.Flush()
 	return b.Bytes(), nil

internal/consensus/wal_test.go

@@ -3,6 +3,7 @@ package consensus
 import (
 	"bytes"
 	"context"
+	"os"
 	"path/filepath"
 
 	"testing"
@@ -41,13 +42,12 @@ func TestWALTruncate(t *testing.T) {
 	require.NoError(t, err)
 	err = wal.Start(ctx)
 	require.NoError(t, err)
-	t.Cleanup(wal.Wait)
+	t.Cleanup(func() { wal.Stop(); wal.Group().Stop(); wal.Group().Wait(); wal.Wait() })
 
 	// 60 block's size nearly 70K, greater than group's headBuf size(4096 * 10),
 	// when headBuf is full, truncate content will Flush to the file. at this
 	// time, RotateFile is called, truncate content exist in each file.
-	err = WALGenerateNBlocks(ctx, t, logger, wal.Group(), 60)
-	require.NoError(t, err)
+	WALGenerateNBlocks(ctx, t, logger, wal.Group(), 60)
 
 	// put the leakcheck here so it runs after other cleanup
 	// functions.
@@ -112,7 +112,7 @@ func TestWALWrite(t *testing.T) {
 	require.NoError(t, err)
 	err = wal.Start(ctx)
 	require.NoError(t, err)
-	t.Cleanup(wal.Wait)
+	t.Cleanup(func() { wal.Stop(); wal.Group().Stop(); wal.Group().Wait(); wal.Wait() })
 
 	// 1) Write returns an error if msg is too big
 	msg := &BlockPartMessage{
@@ -151,7 +151,6 @@ func TestWALSearchForEndHeight(t *testing.T) {
 
 	wal, err := NewWAL(ctx, logger, walFile)
 	require.NoError(t, err)
-	t.Cleanup(func() { wal.Stop(); wal.Wait() })
 
 	h := int64(3)
 	gr, found, err := wal.SearchForEndHeight(h, &WALSearchOptions{})
@@ -176,24 +175,24 @@ func TestWALPeriodicSync(t *testing.T) {
 
 	walDir := t.TempDir()
 	walFile := filepath.Join(walDir, "wal")
-	wal, err := NewWAL(ctx, log.TestingLogger(), walFile, autofile.GroupCheckDuration(1*time.Millisecond))
+	defer os.RemoveAll(walFile)
 
+	wal, err := NewWAL(ctx, log.TestingLogger(), walFile, autofile.GroupCheckDuration(250*time.Millisecond))
 	require.NoError(t, err)
 
 	wal.SetFlushInterval(walTestFlushInterval)
 	logger := log.NewNopLogger()
 
 	// Generate some data
-	err = WALGenerateNBlocks(ctx, t, logger, wal.Group(), 5)
-	require.NoError(t, err)
+	WALGenerateNBlocks(ctx, t, logger, wal.Group(), 5)
 
 	// We should have data in the buffer now
 	assert.NotZero(t, wal.Group().Buffered())
 
 	require.NoError(t, wal.Start(ctx))
-	t.Cleanup(func() { wal.Stop(); wal.Wait() })
+	t.Cleanup(func() { wal.Stop(); wal.Group().Stop(); wal.Group().Wait(); wal.Wait() })
 
-	time.Sleep(walTestFlushInterval + (10 * time.Millisecond))
+	time.Sleep(walTestFlushInterval + (20 * time.Millisecond))
 
 	// The data should have been flushed by the periodic sync
 	assert.Zero(t, wal.Group().Buffered())

internal/libs/autofile/group.go

@@ -274,6 +274,10 @@ func (g *Group) checkTotalSizeLimit(ctx context.Context) {
 	g.mtx.Lock()
 	defer g.mtx.Unlock()
 
+	if err := ctx.Err(); err != nil {
+		return
+	}
+
 	if g.totalSizeLimit == 0 {
 		return
 	}
@@ -290,6 +294,11 @@ func (g *Group) checkTotalSizeLimit(ctx context.Context) {
 			g.logger.Error("Group's head may grow without bound", "head", g.Head.Path)
 			return
 		}
+
+		if ctx.Err() != nil {
+			return
+		}
+
 		pathToRemove := filePathForIndex(g.Head.Path, index, gInfo.MaxIndex)
 		fInfo, err := os.Stat(pathToRemove)
 		if err != nil {
@@ -314,6 +323,10 @@ func (g *Group) rotateFile(ctx context.Context) {
 	g.mtx.Lock()
 	defer g.mtx.Unlock()
 
+	if err := ctx.Err(); err != nil {
+		return
+	}
+
 	headPath := g.Head.Path
 
 	if err := g.headBuf.Flush(); err != nil {

internal/p2p/pex/reactor_test.go

@@ -1,6 +1,4 @@
-// Temporarily disabled pending ttps://github.com/tendermint/tendermint/issues/7626.
-//go:build issue7626
-
+//nolint:unused
 package pex_test
 
 import (
@@ -103,6 +101,7 @@ func TestReactorSendsRequestsTooOften(t *testing.T) {
 }
 
 func TestReactorSendsResponseWithoutRequest(t *testing.T) {
+	t.Skip("This test needs updated https://github.com/tendermint/tendermint/issue/7634")
 	ctx, cancel := context.WithCancel(context.Background())
 	defer cancel()
 
@@ -124,6 +123,7 @@ func TestReactorSendsResponseWithoutRequest(t *testing.T) {
 }
 
 func TestReactorNeverSendsTooManyPeers(t *testing.T) {
+	t.Skip("This test needs updated https://github.com/tendermint/tendermint/issue/7634")
 	ctx, cancel := context.WithCancel(context.Background())
 	defer cancel()
 
@@ -235,6 +235,7 @@ func TestReactorLargePeerStoreInASmallNetwork(t *testing.T) {
 }
 
 func TestReactorWithNetworkGrowth(t *testing.T) {
+	t.Skip("This test needs updated https://github.com/tendermint/tendermint/issue/7634")
 	ctx, cancel := context.WithCancel(context.Background())
 	defer cancel()
 
@@ -686,20 +687,16 @@ func (r *reactorTestSuite) connectPeers(ctx context.Context, t *testing.T, sourc
 
 	select {
 	case peerUpdate := <-targetSub.Updates():
-		require.Equal(t, p2p.PeerUpdate{
-			NodeID: node1,
-			Status: p2p.PeerStatusUp,
-		}, peerUpdate)
+		require.Equal(t, peerUpdate.NodeID, node1)
+		require.Equal(t, peerUpdate.Status, p2p.PeerStatusUp)
 	case <-time.After(2 * time.Second):
 		require.Fail(t, "timed out waiting for peer", "%v accepting %v",
 			targetNode, sourceNode)
 	}
 	select {
 	case peerUpdate := <-sourceSub.Updates():
-		require.Equal(t, p2p.PeerUpdate{
-			NodeID: node2,
-			Status: p2p.PeerStatusUp,
-		}, peerUpdate)
+		require.Equal(t, peerUpdate.NodeID, node2)
+		require.Equal(t, peerUpdate.Status, p2p.PeerStatusUp)
 	case <-time.After(2 * time.Second):
 		require.Fail(t, "timed out waiting for peer", "%v dialing %v",
 			sourceNode, targetNode)

internal/rpc/core/events.go

@@ -165,8 +165,11 @@ func (env *Environment) Events(ctx context.Context,
 		maxItems = 100
 	}
 
+	const minWaitTime = 1 * time.Second
 	const maxWaitTime = 30 * time.Second
-	if waitTime > maxWaitTime {
+	if waitTime < minWaitTime {
+		waitTime = minWaitTime
+	} else if waitTime > maxWaitTime {
 		waitTime = maxWaitTime
 	}
 
@@ -185,7 +188,7 @@ func (env *Environment) Events(ctx context.Context,
 	accept := func(itm *eventlog.Item) error {
 		// N.B. We accept up to one item more than requested, so we can tell how
 		// to set the "more" flag in the response.
-		if len(items) > maxItems {
+		if len(items) > maxItems || itm.Cursor.Before(after) {
 			return eventlog.ErrStopScan
 		}
 		if cursorInRange(itm.Cursor, before, after) && query.Matches(itm.Events) {
@@ -194,7 +197,7 @@ func (env *Environment) Events(ctx context.Context,
 		return nil
 	}
 
-	if waitTime > 0 && before.IsZero() {
+	if before.IsZero() {
 		ctx, cancel := context.WithTimeout(ctx, waitTime)
 		defer cancel()
 

internal/statesync/reactor_test.go

@@ -600,7 +600,7 @@ func TestReactor_StateProviderP2P(t *testing.T) {
 	require.NoError(t, err)
 	rts.reactor.syncer.stateProvider = rts.reactor.stateProvider
 
-	actx, cancel := context.WithTimeout(ctx, 10*time.Second)
+	actx, cancel := context.WithTimeout(ctx, time.Second)
 	defer cancel()
 
 	appHash, err := rts.reactor.stateProvider.AppHash(actx, 5)

internal/statesync/stateprovider.go

@@ -3,7 +3,6 @@ package statesync
 import (
 	"bytes"
 	"context"
-	"errors"
 	"fmt"
 	"math/rand"
 	"strings"
@@ -331,7 +330,7 @@ func (s *stateProviderP2P) State(ctx context.Context, height uint64) (sm.State,
 	// We'll also need to fetch consensus params via P2P.
 	state.ConsensusParams, err = s.consensusParams(ctx, currentLightBlock.Height)
 	if err != nil {
-		return sm.State{}, err
+		return sm.State{}, fmt.Errorf("fetching consensus params: %w", err)
 	}
 	// validate the consensus params
 	if !bytes.Equal(nextLightBlock.ConsensusHash, state.ConsensusParams.HashConsensusParams()) {
@@ -355,80 +354,110 @@ func (s *stateProviderP2P) addProvider(p lightprovider.Provider) {
 // consensusParams sends out a request for consensus params blocking
 // until one is returned.
 //
-// If it fails to get a valid set of consensus params from any of the
-// providers it returns an error; however, it will retry indefinitely
-// (with backoff) until the context is canceled.
+// It attempts to send requests to all witnesses in parallel, but if
+// none responds it will retry them all sometime later until it
+// receives some response. This operation will block until it receives
+// a response or the context is canceled.
 func (s *stateProviderP2P) consensusParams(ctx context.Context, height int64) (types.ConsensusParams, error) {
-	var iterCount int64
+	ctx, cancel := context.WithCancel(ctx)
+	defer cancel()
 
-	timer := time.NewTimer(0)
-	defer timer.Stop()
-	for {
-		params, err := s.tryGetConsensusParamsFromWitnesses(ctx, height)
-		if err != nil {
-			return types.ConsensusParams{}, err
-		}
-		if params != nil {
-			return *params, nil
-		}
-		iterCount++
+	out := make(chan types.ConsensusParams)
 
-		// jitter+backoff the retry loop
-		timer.Reset(time.Duration(iterCount)*consensusParamsResponseTimeout +
-			time.Duration(100*rand.Int63n(iterCount))*time.Millisecond) // nolint:gosec
-		select {
-		case <-ctx.Done():
-			return types.ConsensusParams{}, ctx.Err()
-		case <-timer.C:
+	retryAll := func() (<-chan struct{}, error) {
+		wg := &sync.WaitGroup{}
+
+		for _, provider := range s.lc.Witnesses() {
+			p, ok := provider.(*BlockProvider)
+			if !ok {
+				return nil, fmt.Errorf("witness is not BlockProvider [%T]", provider)
+			}
+
+			peer, err := types.NewNodeID(p.String())
+			if err != nil {
+				return nil, fmt.Errorf("invalid provider (%s) node id: %w", p.String(), err)
+			}
+
+			wg.Add(1)
+			go func(p *BlockProvider, peer types.NodeID) {
+				defer wg.Done()
+
+				timer := time.NewTimer(0)
+				defer timer.Stop()
+				var iterCount int64
+
+				for {
+					iterCount++
+					if err := s.paramsSendCh.Send(ctx, p2p.Envelope{
+						To: peer,
+						Message: &ssproto.ParamsRequest{
+							Height: uint64(height),
+						},
+					}); err != nil {
+						// this only errors if
+						// the context is
+						// canceled which we
+						// don't need to
+						// propagate here
+						return
+					}
+
+					// jitter+backoff the retry loop
+					timer.Reset(time.Duration(iterCount)*consensusParamsResponseTimeout +
+						time.Duration(100*rand.Int63n(iterCount))*time.Millisecond) // nolint:gosec
+
+					select {
+					case <-timer.C:
+						continue
+					case <-ctx.Done():
+						return
+					case params, ok := <-s.paramsRecvCh:
+						if !ok {
+							return
+						}
+						select {
+						case <-ctx.Done():
+							return
+						case out <- params:
+							return
+						}
+					}
+				}
+
+			}(p, peer)
 		}
+		sig := make(chan struct{})
+		go func() { wg.Wait(); close(sig) }()
+		return sig, nil
 	}
-}
 
-// tryGetConsensusParamsFromWitnesses attempts to get consensus
-// parameters from the light clients available witnesses. If both
-// return parameters are nil, then it can be retried.
-func (s *stateProviderP2P) tryGetConsensusParamsFromWitnesses(
-	ctx context.Context,
-	height int64,
-) (*types.ConsensusParams, error) {
 	timer := time.NewTimer(0)
 	defer timer.Stop()
-	for _, provider := range s.lc.Witnesses() {
-		p, ok := provider.(*BlockProvider)
-		if !ok {
-			panic("expected p2p state provider to use p2p block providers")
-		}
 
-		// extract the nodeID of the provider
-		peer, err := types.NewNodeID(p.String())
+	var iterCount int64
+	for {
+		iterCount++
+		sig, err := retryAll()
 		if err != nil {
-			return nil, fmt.Errorf("invalid provider (%s) node id: %w", p.String(), err)
-		}
-
-		if err := s.paramsSendCh.Send(ctx, p2p.Envelope{
-			To: peer,
-			Message: &ssproto.ParamsRequest{
-				Height: uint64(height),
-			},
-		}); err != nil {
-			return nil, err
+			return types.ConsensusParams{}, err
 		}
-
-		timer.Reset(consensusParamsResponseTimeout)
 		select {
-		// if we get no response from this provider we move on to the next one
-		case <-timer.C:
-			continue
-		case <-ctx.Done():
-			return nil, ctx.Err()
-		case params, ok := <-s.paramsRecvCh:
-			if !ok {
-				return nil, errors.New("params channel closed")
+		case <-sig:
+			// jitter+backoff the retry loop
+			timer.Reset(time.Duration(iterCount)*consensusParamsResponseTimeout +
+				time.Duration(100*rand.Int63n(iterCount))*time.Millisecond) // nolint:gosec
+			select {
+			case param := <-out:
+				return param, nil
+			case <-ctx.Done():
+				return types.ConsensusParams{}, ctx.Err()
+			case <-timer.C:
 			}
-			return &params, nil
+		case <-ctx.Done():
+			return types.ConsensusParams{}, ctx.Err()
+		case param := <-out:
+			return param, nil
 		}
 	}
 
-	// signal to caller to retry.
-	return nil, nil
 }

proto/tendermint/abci/types.proto

@@ -380,15 +380,13 @@ message TxResult {
 message TxRecord {
   TxAction       action     = 1;
   bytes          tx         = 2;
-  repeated bytes new_hashes = 3;
 
   // TxAction contains App-provided information on what to do with a transaction that is part of a raw proposal
   enum TxAction {
     UNKNOWN    = 0;  // Unknown action
-    UNMODIFIED = 1;  // The Application did not modify this transaction. Ignore new_hashes field
-    ADDED      = 2;  // The Application added this transaction. Ignore new_hashes field
+    UNMODIFIED = 1;  // The Application did not modify this transaction.
+    ADDED      = 2;  // The Application added this transaction.
     REMOVED    = 3;  // The Application wants this transaction removed from the proposal and the mempool.
-                     // Use #new_hashes field if the transaction was modified
   }
 }
 

rpc/client/eventstream/eventstream_test.go

@@ -90,6 +90,55 @@ func TestStream_lostItem(t *testing.T) {
 	s.stopWait()
 }
 
+func TestMinPollTime(t *testing.T) {
+	defer leaktest.Check(t)
+
+	s := newStreamTester(t, ``, eventlog.LogSettings{
+		WindowSize: 30 * time.Second,
+	}, nil)
+
+	s.publish("bad", "whatever")
+
+	// Waiting for an item on a log with no matching events incurs a minimum
+	// wait time and reports no events.
+	ctx := context.Background()
+	filter := &coretypes.EventFilter{Query: `tm.event = 'good'`}
+	var zero cursor.Cursor
+
+	t.Run("NoneMatch", func(t *testing.T) {
+		start := time.Now()
+
+		// Request a very short delay, and affirm we got the server's minimum.
+		rsp, err := s.env.Events(ctx, filter, 1, zero, zero, 10*time.Millisecond)
+		if err != nil {
+			t.Fatalf("Events failed: %v", err)
+		} else if elapsed := time.Since(start); elapsed < time.Second {
+			t.Errorf("Events returned too quickly: got %v, wanted 1s", elapsed)
+		} else if len(rsp.Items) != 0 {
+			t.Errorf("Events returned %d items, expected none", len(rsp.Items))
+		}
+	})
+
+	s.publish("good", "whatever")
+
+	// Waiting for an available matching item incurs no delay.
+	t.Run("SomeMatch", func(t *testing.T) {
+		start := time.Now()
+
+		// Request a long-ish delay and affirm we don't block for it.
+		// Check for this by ensuring we return sooner than the minimum delay,
+		// since we don't know the exact timing.
+		rsp, err := s.env.Events(ctx, filter, 1, zero, zero, 10*time.Second)
+		if err != nil {
+			t.Fatalf("Events failed: %v", err)
+		} else if elapsed := time.Since(start); elapsed > 500*time.Millisecond {
+			t.Errorf("Events returned too slowly: got %v, wanted immediate", elapsed)
+		} else if len(rsp.Items) == 0 {
+			t.Error("Events returned no items, wanted at least 1")
+		}
+	})
+}
+
 // testItem is a wrapper for comparing item results in a friendly output format
 // for the cmp package.
 type testItem struct {

spec/abci++/abci++_methods_002_draft.md

@@ -312,17 +312,20 @@ From the App's perspective, they'll probably skip ProcessProposal
     | app_signed_updates      | repeated bytes                                   | Optional changes to the *app_signed* part of vote extensions.                               | 7            |
 
 * **Usage**:
-    * Contains a preliminary block to be proposed, called _raw block_, which the Application can modify.
     * The first five parameters of `RequestPrepareProposal` are the same as `RequestProcessProposal`
       and `RequestFinalizeBlock`.
     * The header contains the height, timestamp, and more - it exactly matches the
       Tendermint block header.
-    * The Application can modify the transactions received in `RequestPrepareProposal` before sending
-      them in `ResponsePrepareProposal`. In that case, `ResponsePrepareProposal.modified_tx` is set to true.
-    * If `ResponsePrepareProposal.modified_tx` is false, then Tendermint will ignore the contents of
-      `ResponsePrepareProposal.tx_records`.
-    * If the Application modifies the transactions, the modified transactions MUST NOT exceed the configured maximum size,
-      contained in `RequestPrepareProposal.max_tx_bytes`.
+    * `RequestPrepareProposal` contains a preliminary set of transactions `txs` that Tendermint considers to be a good block proposal, called _raw block_. The Application can modify this set via `ResponsePrepareProposal.tx_records` (see [TxRecord](#txrecord)).
+        * In this case, the Application should set `ResponsePrepareProposal.modified_tx` to true.
+        * The Application _can_ reorder, remove or add transactions to the raw block. Let `tx` be a transaction in `txs`:
+            * If the Application considers that `tx` should not be proposed in this block, e.g., there are other transactions with higher priority, then it should not include it in `tx_records`. In this case, Tendermint won't remove `tx` from the mempool. The Application should be extra-careful, as abusing this feature may cause transactions to stay forever in the mempool.
+            * If the Application considers that a `tx` should not be included in the proposal and removed from the mempool, then the Application should include it in `tx_records` and _mark_ it as "REMOVE". In this case, Tendermint will remove `tx` from the mempool.
+            * If the Application wants to add a new transaction, then the Application should include it in `tx_records` and _mark_ it as "ADD". In this case, Tendermint will add it to the mempool.
+        * The Application should be aware that removing and adding transactions may compromise _traceability_.
+          > Consider the following example: the Application transforms a client-submitted transaction `t1` into a second transaction `t2`, i.e., the Application asks Tendermint to remove `t1` and add `t2` to the mempool. If a client wants to eventually check what happened to `t1`, it will discover that `t_1` is not in the mempool or in a committed block, getting the wrong idea that `t_1` did not make it into a block. Note that `t_2` _will be_ in a committed block, but unless the Application tracks this information, no component will be aware of it. Thus, if the Application wants traceability, it is its responsability to support it. For instance, the Application could attach to a transformed transaction a list with the hashes of the transactions it derives from. 
+        * If the Application modifies the set of transactions, the modified transactions MUST NOT exceed the configured maximum size `RequestPrepareProposal.max_tx_bytes`.
+    * If the Application does not modify the preliminary set of transactions `txs`, then it sets `ResponsePrepareProposal.modified_tx` to false. In this case, Tendermint will ignore the contents of `ResponsePrepareProposal.tx_records`.
     * If the Application modifies the *app_signed* part of vote extensions via `ResponsePrepareProposal.app_signed_updates`,
       the new total size of those extensions cannot exceed their initial size.
     * The Application may choose to not modify the *app_signed* part of vote extensions by leaving parameter
@@ -352,21 +355,9 @@ From the App's perspective, they'll probably skip ProcessProposal
       `ResponseFinalizeBlock`.
     * Likewise, in next-block execution mode, the Application must keep all responses to executing transactions
       until it can call `ResponseFinalizeBlock`.
-    * The Application can change the transaction list via `ResponsePrepareProposal.tx_records`.
-      See [TxRecord](#txrecord) for further information on how to use it. Some notes:
-        * To remove a transaction from the proposed block the Application _marks_ the transaction as
-          "REMOVE". It does not remove it from the list. The transaction will also be removed from the mempool.
-        * Removing a transaction from the list means it is too early to propose that transaction,
-          so it will be excluded from the proposal but will stay in the mempool for later proposals.
-          The Application should be extra-careful, as abusing this feature may cause transactions to
-          stay forever in the mempool.
-        * The `new_hashes` field, besides helping with mempool maintenance, helps Tendermint handle
-          queries such as "what happened with this Tx?", by answering "it was modified into these ones".
-        * The Application _can_ reorder the transactions in the list.
     * As a sanity check, Tendermint will check the returned parameters for validity if the Application modified them.
       In particular, `ResponsePrepareProposal.tx_records` will be deemed invalid if
         * There is a duplicate transaction in the list.
-        * The `new_hashes` field contains a dangling reference to a non-existing transaction.
         * A new or modified transaction is marked as "TXUNMODIFIED" or "TXREMOVED".
         * An unmodified transaction is marked as "TXADDED".
         * A transaction is marked as "TXUNKNOWN".
@@ -403,7 +394,7 @@ and _p_'s _validValue_ is `nil`:
         * remove transactions (invalid) from the proposal and from the mempool - `TxAction = REMOVED`
         * remove transactions from the proposal but not from the mempool (effectively _delaying_ them) - the
           Application removes the transaction from the list
-        * modify transactions (e.g. aggregate them) - `TxAction = ADDED` followed by `TxAction = REMOVED`
+        * modify transactions (e.g. aggregate them) - `TxAction = ADDED` followed by `TxAction = REMOVED`. As explained above, this compromises client traceability, unless it is implemented at the Application level.
         * reorder transactions - the Application reorders transactions in the list
 4. If the block is modified, the Application sets `ResponsePrepareProposal.modified` to true,
    and includes the modified block in the return parameters (see the rules in section _Usage_).
@@ -832,20 +823,18 @@ Most of the data structures used in ABCI are shared [common data structures](../
 ```protobuf
   enum TxAction {
     TXUNKNOWN    = 0;  // Unknown action
-    TXUNMODIFIED = 1;  // The Application did not modify this transaction. Ignore new_hashes field
-    TXADDED      = 2;  // The Application added this transaction. Ignore new_hashes field
+    TXUNMODIFIED = 1;  // The Application did not modify this transaction.
+    TXADDED      = 2;  // The Application added this transaction.
     TXREMOVED    = 3;  // The Application wants this transaction removed from the proposal and the mempool.
-                       // Use new_hashes field if the transaction was modified
   }
 ```
 
 * **Usage**:
     * If `Action` is TXUNKNOWN, a problem happened in the Application. Tendermint will ignore this transaction. **TODO** should we panic?
-    * If `Action` is TXUNMODIFIED, Tendermint includes the transaction in the proposal. Nothing to do on the mempool. Field `new_hashes` is ignored.
-    * If `Action` is TXADDED, Tendermint includes the transaction in the proposal. The transaction is also added to the mempool and gossipped. Field `new_hashes` is ignored.
+    * If `Action` is TXUNMODIFIED, Tendermint includes the transaction in the proposal. Nothing to do on the mempool.
+    * If `Action` is TXADDED, Tendermint includes the transaction in the proposal. The transaction is also added to the mempool and gossipped.
     * If `Action` is TXREMOVED, Tendermint excludes the transaction from the proposal. The transaction is also removed from the mempool if it exists,
-      similar to `CheckTx` returning _false_. Tendermint can use field `new_hashes` to help clients trace transactions that have been modified into other transactions.
-
+      similar to `CheckTx` returning _false_.
 ### TxRecord
 
 * **Fields**:
@@ -854,25 +843,3 @@ Most of the data structures used in ABCI are shared [common data structures](../
     |------------|-----------------------|------------------------------------------------------------------|--------------|
     | action     | [TxAction](#txaction) | What should Tendermint do with this transaction?                 | 1            |
     | tx         | bytes                 | Transaction contents                                             | 2            |
-    | new_hashes | repeated bytes        | List of hashes of successor transactions                         | 3            |
-
-* **Usage**:
-    * The hashes contained in `new_hashes` MUST follow the same algorithm used by Tendermint for hashing transactions
-      that are in the mempool.
-    * As `new_hashes` is a list, `TxRecord` allows to trace many-to-many modifications. Some examples:
-        * Transaction $t1$ modified into $t2$ is represented with these records
-            * $t2$ "ADDED"
-            * $t1$ "REMOVED"; `new_hashes` contains [$id(t2)$]
-        * Transaction $t1$ modified into $t2$ and $t3$ is represented with these `TxRecord` records
-            * $t2$ "ADDED"
-            * $t3$ "ADDED"
-            * $t1$ "REMOVED"; `new_hashes` contains [$id(t2)$, $id(t3)$]
-        * Transactions $t1$ and $t2$ aggregated into $t3$ is represented with these `TxRecord` records
-            * $t3$ "ADDED"
-            * $t1$ "REMOVED"; `new_hashes` contains [$id(t3)$]
-            * $t2$ "REMOVED"; `new_hashes` contains [$id(t3)$]
-        * Transactions $t1$ and $t2$ combined into $t3$ and $t4$ is represented with these `TxRecord` records
-            * $t3$ "ADDED"
-            * $t4$ "ADDED"
-            * $t1$ "REMOVED" and `new_hashes` containing [$id(t3)$, $id(t4)$]
-            * $t2$ "REMOVED" and `new_hashes` containing [$id(t3)$, $id(t4)$]

spec/consensus/proposer-based-timestamp/tla/Apalache.tla

@@ -0,0 +1,109 @@
+--------------------------- MODULE Apalache -----------------------------------
+(*
+ * This is a standard module for use with the Apalache model checker.
+ * The meaning of the operators is explained in the comments.
+ * Many of the operators serve as additional annotations of their arguments.
+ * As we like to preserve compatibility with TLC and TLAPS, we define the
+ * operator bodies by erasure. The actual interpretation of the operators is
+ * encoded inside Apalache. For the moment, these operators are mirrored in
+ * the class at.forsyte.apalache.tla.lir.oper.ApalacheOper.
+ *                                                                          
+ * Igor Konnov, Jure Kukovec, Informal Systems 2020-2021                    
+ *)
+
+(**
+ * An assignment of an expression e to a state variable x. Typically, one
+ * uses the non-primed version of x in the initializing predicate Init and
+ * the primed version of x (that is, x') in the transition predicate Next.
+ * Although TLA+ does not have a concept of a variable assignment, we find
+ * this concept extremely useful for symbolic model checking. In pure TLA+,
+ * one would simply write x = e, or x \in {e}.
+ *
+ * Apalache automatically converts some expressions of the form
+ * x = e or x \in {e} into assignments. However, if you like to annotate
+ * assignments by hand, you can use this operator.
+ *
+ * For a further discussion on that matter, see:
+ * https://github.com/informalsystems/apalache/blob/ik/idiomatic-tla/docs/idiomatic/assignments.md
+ *)
+x := e == x = e
+
+(**
+ * A generator of a data structure. Given a positive integer `bound`, and
+ * assuming that the type of the operator application is known, we
+ * recursively generate a TLA+ data structure as a tree, whose width is
+ * bound by the number `bound`.
+ *
+ * The body of this operator is redefined by Apalache.
+ *)
+Gen(size) == {}
+
+(**
+ * Convert a set of pairs S to a function F. Note that if S contains at least
+ * two pairs <<x, y>> and <<u, v>> such that x = u and y /= v,
+ * then F is not uniquely defined. We use CHOOSE to resolve this ambiguity.
+ * Apalache implements a more efficient encoding of this operator
+ * than the default one.
+ *
+ * @type: Set(<<a, b>>) => (a -> b);
+ *)
+SetAsFun(S) ==
+    LET Dom == { x: <<x, y>> \in S }
+        Rng == { y: <<x, y>> \in S }
+    IN
+    [ x \in Dom |-> CHOOSE y \in Rng: <<x, y>> \in S ]
+
+(**
+ * As TLA+ is untyped, one can use function- and sequence-specific operators
+ * interchangeably. However, to maintain correctness w.r.t. our type-system,
+ * an explicit cast is needed when using functions as sequences.
+ *)
+LOCAL INSTANCE Sequences
+FunAsSeq(fn, maxSeqLen) == SubSeq(fn, 1, maxSeqLen)
+
+(**
+ * Annotating an expression \E x \in S: P as Skolemizable. That is, it can
+ * be replaced with an expression c \in S /\ P(c) for a fresh constant c.
+ * Not every exisential can be replaced with a constant, this should be done
+ * with care. Apalache detects Skolemizable expressions by static analysis.
+ *)
+Skolem(e) == e
+
+(**
+ * A hint to the model checker to expand a set S, instead of dealing
+ * with it symbolically. Apalache finds out which sets have to be expanded
+ * by static analysis.
+ *)
+Expand(S) == S
+
+(**
+ * A hint to the model checker to replace its argument Cardinality(S) >= k
+ * with a series of existential quantifiers for a constant k.
+ * Similar to Skolem, this has to be done carefully. Apalache automatically
+ * places this hint by static analysis.
+ *)
+ConstCardinality(cardExpr) == cardExpr
+
+(**
+ * The folding operator, used to implement computation over a set.
+ * Apalache implements a more efficient encoding than the one below.
+ * (from the community modules).
+ *)
+RECURSIVE FoldSet(_,_,_)
+FoldSet( Op(_,_), v, S ) == IF S = {}
+                            THEN v
+                            ELSE LET w == CHOOSE x \in S: TRUE
+                                  IN LET T == S \ {w}
+                                      IN FoldSet( Op, Op(v,w), T )
+
+(**
+ * The folding operator, used to implement computation over a sequence.
+ * Apalache implements a more efficient encoding than the one below.
+ * (from the community modules).
+ *)
+RECURSIVE FoldSeq(_,_,_)
+FoldSeq( Op(_,_), v, seq ) == IF seq = <<>>
+                              THEN v
+                              ELSE FoldSeq( Op, Op(v,Head(seq)), Tail(seq) )
+
+===============================================================================

spec/consensus/proposer-based-timestamp/tla/MC_PBT.tla

@@ -0,0 +1,77 @@
+----------------------------- MODULE MC_PBT -------------------------------
+CONSTANT 
+  \* @type: ROUND -> PROCESS;
+  Proposer
+
+VARIABLES
+  \* @type: PROCESS -> ROUND;
+  round,    \* a process round number
+  \* @type: PROCESS -> STEP;
+  step,     \* a process step
+  \* @type: PROCESS -> DECISION;
+  decision, \* process decision
+  \* @type: PROCESS -> VALUE;
+  lockedValue,  \* a locked value
+  \* @type: PROCESS -> ROUND;
+  lockedRound,  \* a locked round
+  \* @type: PROCESS -> PROPOSAL;
+  validValue,   \* a valid value
+  \* @type: PROCESS -> ROUND;
+  validRound    \* a valid round
+
+\* time-related variables
+VARIABLES  
+  \* @type: PROCESS -> TIME;
+  localClock, \* a process local clock: Corr -> Ticks
+  \* @type: TIME;
+  realTime   \* a reference Newtonian real time
+
+\* book-keeping variables
+VARIABLES
+  \* @type: ROUND -> Set(PROPMESSAGE);
+  msgsPropose,   \* PROPOSE messages broadcast in the system, Rounds -> Messages
+  \* @type: ROUND -> Set(PREMESSAGE);
+  msgsPrevote,   \* PREVOTE messages broadcast in the system, Rounds -> Messages
+  \* @type: ROUND -> Set(PREMESSAGE);
+  msgsPrecommit, \* PRECOMMIT messages broadcast in the system, Rounds -> Messages
+  \* @type: Set(MESSAGE);
+  evidence, \* the messages that were used by the correct processes to make transitions
+  \* @type: ACTION;
+  action,       \* we use this variable to see which action was taken
+  \* @type: PROCESS -> Set(PROPMESSAGE);
+  receivedTimelyProposal, \* used to keep track when a process receives a timely VALUE message
+  \* @type: <<ROUND,PROCESS>> -> TIME;
+  inspectedProposal \* used to keep track when a process tries to receive a message
+  
+\* Invariant support
+VARIABLES
+  \* @type: ROUND -> TIME;
+  beginRound, \* the minimum of the local clocks at the time any process entered a new round
+  \* @type: PROCESS -> TIME;
+  endConsensus, \* the local time when a decision is made
+  \* @type: ROUND -> TIME;
+  lastBeginRound, \* the maximum of the local clocks in each round
+  \* @type: ROUND -> TIME;
+  proposalTime, \* the real time when a proposer proposes in a round
+  \* @type: ROUND -> TIME;
+  proposalReceivedTime \* the real time when a correct process first receives a proposal message in a round
+
+
+INSTANCE TendermintPBT_002_draft WITH
+  Corr <- {"c1", "c2"},
+  Faulty <- {"f3", "f4"},
+  N <- 4,
+  T <- 1,
+  ValidValues <- { "v0", "v1" },
+  InvalidValues <- {"v2"},
+  MaxRound <- 5,
+  MaxTimestamp <- 10,
+  MinTimestamp <- 2,
+  Delay <- 2,        
+  Precision <- 2
+
+\* run Apalache with --cinit=CInit
+CInit == \* the proposer is arbitrary -- works for safety
+  Proposer \in [Rounds -> AllProcs]
+
+=============================================================================    

spec/consensus/proposer-based-timestamp/tla/TendermintPBT_002_draft.tla

@@ -5,10 +5,11 @@
  the Tendermint TLA+ specification for fork accountability: 
     https://github.com/tendermint/spec/blob/master/spec/light-client/accountability/TendermintAcc_004_draft.tla
  
- * Version 1. A preliminary specification.
+ * Version 2. A preliminary specification.
 
  Zarko Milosevic, Igor Konnov, Informal Systems, 2019-2020.
  Ilina Stoilkovska, Josef Widder, Informal Systems, 2021.
+ Jure Kukovec, Informal Systems, 2022.
  *)
 
 EXTENDS Integers, FiniteSets, Apalache, typedefs
@@ -38,13 +39,11 @@ CONSTANTS
   \* @type: TIME;
   MaxTimestamp,  \* the maximal value of the clock tick
   \* @type: TIME;
-  Delay,         \* message delay
+  MinTimestamp,  \* the minimal value of the clock tick
   \* @type: TIME;
-  Precision,     \* clock precision: the maximal difference between two local clocks  
+  Delay,         \* message delay
   \* @type: TIME;
-  Accuracy,      \* clock accuracy: the maximal difference between a local clock and the real time
-  \* @type: Bool;
-  ClockDrift     \* is there clock drift between the local clocks and the global clock
+  Precision     \* clock precision: the maximal difference between two local clocks  
 
 ASSUME(N = Cardinality(Corr \union Faulty))
 
@@ -66,24 +65,39 @@ Values == ValidValues \union InvalidValues \* the set of all values
 \* @type: VALUE;
 NilValue == "None"  \* a special value for a nil round, outside of Values
 \* @type: Set(PROPOSAL);
-Proposals == Values \X Timestamps
+Proposals == Values \X Timestamps \X Rounds
 \* @type: PROPOSAL;
-NilProposal == <<NilValue, NilTimestamp>>
+NilProposal == <<NilValue, NilTimestamp, NilRound>>
 \* @type: Set(VALUE);
 ValuesOrNil == Values \union {NilValue}
 \* @type: Set(DECISION);
-Decisions == Values \X Timestamps \X Rounds
+Decisions == Proposals \X Rounds
 \* @type: DECISION;
-NilDecision == <<NilValue, NilTimestamp, NilRound>>
-
+NilDecision == <<NilProposal, NilRound>>
 
+ValidProposals == ValidValues \X (MinTimestamp..MaxTimestamp) \X Rounds
 \* a value hash is modeled as identity
 \* @type: (t) => t;
 Id(v) == v
 
 \* The validity predicate
-\* @type: (VALUE) => Bool;
-IsValid(v) == v \in ValidValues
+\* @type: (PROPOSAL) => Bool;
+IsValid(p) == p \in ValidProposals
+
+\* Time validity check. If we want MaxTimestamp = \infty, set ValidTime(t) == TRUE
+ValidTime(t) == t < MaxTimestamp
+
+\* @type: (PROPMESSAGE) => VALUE;
+MessageValue(msg) == msg.proposal[1]
+\* @type: (PROPMESSAGE) => TIME;
+MessageTime(msg) == msg.proposal[2]
+\* @type: (PROPMESSAGE) => ROUND;
+MessageRound(msg) == msg.proposal[3]
+
+\* @type: (TIME, TIME) => Bool;
+IsTimely(processTime, messageTime) ==
+  /\ processTime >= messageTime - Precision
+  /\ processTime <= messageTime + Precision + Delay
 
 \* the two thresholds that are used in the algorithm
 \* @type: Int;
@@ -91,23 +105,24 @@ THRESHOLD1 == T + 1     \* at least one process is not faulty
 \* @type: Int;
 THRESHOLD2 == 2 * T + 1 \* a quorum when having N > 3 * T
 
+\* @type: (TIME, TIME) => TIME;
+Min2(a,b) == IF a <= b THEN a ELSE b
 \* @type: (Set(TIME)) => TIME;
-Min(S) == CHOOSE x \in S : \A y \in S : x <= y
+Min(S) == FoldSet( Min2, MaxTimestamp, S )
+\* Min(S) == CHOOSE x \in S : \A y \in S : x <= y
 
+\* @type: (TIME, TIME) => TIME;
+Max2(a,b) == IF a >= b THEN a ELSE b
 \* @type: (Set(TIME)) => TIME;
-Max(S) == CHOOSE x \in S : \A y \in S : y <= x
-
-(********************* TYPE ANNOTATIONS FOR APALACHE **************************)
-
-\* a type annotation for an empty set of messages
-\* @type: Set(MESSAGE);
-EmptyMsgSet == {}
-
-\* @type: Set(RCVPROP);
-EmptyRcvProp == {}
+Max(S) == FoldSet( Max2, NilTimestamp, S )
+\* Max(S) == CHOOSE x \in S : \A y \in S : y <= x
 
-\* @type: Set(PROCESS);
-EmptyProcSet == {}
+\* @type: (Set(MESSAGE)) => Int;
+Card(S) == 
+  LET 
+    \* @type: (Int, MESSAGE) => Int;
+    PlusOne(i, m) == i + 1
+  IN FoldSet( PlusOne, 0, S )
 
 (********************* PROTOCOL STATE VARIABLES ******************************)
 VARIABLES
@@ -121,11 +136,15 @@ VARIABLES
   lockedValue,  \* a locked value
   \* @type: PROCESS -> ROUND;
   lockedRound,  \* a locked round
-  \* @type: PROCESS -> VALUE;
+  \* @type: PROCESS -> PROPOSAL;
   validValue,   \* a valid value
   \* @type: PROCESS -> ROUND;
   validRound    \* a valid round
 
+coreVars == 
+  <<round, step, decision, lockedValue, 
+  lockedRound, validValue, validRound>>
+
 \* time-related variables
 VARIABLES  
   \* @type: PROCESS -> TIME;
@@ -133,6 +152,8 @@ VARIABLES
   \* @type: TIME;
   realTime   \* a reference Newtonian real time
 
+temporalVars == <<localClock, realTime>>
+
 \* book-keeping variables
 VARIABLES
   \* @type: ROUND -> Set(PROPMESSAGE);
@@ -145,28 +166,35 @@ VARIABLES
   evidence, \* the messages that were used by the correct processes to make transitions
   \* @type: ACTION;
   action,       \* we use this variable to see which action was taken
-  \* @type: Set(RCVPROP);
+  \* @type: PROCESS -> Set(PROPMESSAGE);
   receivedTimelyProposal, \* used to keep track when a process receives a timely PROPOSAL message
-  \* @type: ROUND -> Set(PROCESS);
-  inspectedProposal, \* used to keep track when a process tries to receive a message
-  \* @type: TIME;
-  beginConsensus, \* the minimum of the local clocks in the initial state
+  \* @type: <<ROUND,PROCESS>> -> TIME;
+  inspectedProposal \* used to keep track when a process tries to receive a message
+  
+\* Action is excluded from the tuple, because it always changes
+bookkeepingVars == 
+  <<msgsPropose, msgsPrevote, msgsPrecommit, 
+  evidence, (*action,*) receivedTimelyProposal, 
+  inspectedProposal>>
+
+\* Invariant support
+VARIABLES
+  \* @type: ROUND -> TIME;
+  beginRound, \* the minimum of the local clocks at the time any process entered a new round
   \* @type: PROCESS -> TIME;
   endConsensus, \* the local time when a decision is made
-  \* @type: TIME;
-  lastBeginConsensus, \* the maximum of the local clocks in the initial state
+  \* @type: ROUND -> TIME;
+  lastBeginRound, \* the maximum of the local clocks in each round
   \* @type: ROUND -> TIME;
   proposalTime, \* the real time when a proposer proposes in a round
   \* @type: ROUND -> TIME;
   proposalReceivedTime \* the real time when a correct process first receives a proposal message in a round
 
+invariantVars == 
+  <<beginRound, endConsensus, lastBeginRound,
+  proposalTime, proposalReceivedTime>>
+
 (* to see a type invariant, check TendermintAccInv3 *)  
- 
-\* a handy definition used in UNCHANGED
-vars == <<round, step, decision, lockedValue, lockedRound,
-          validValue, validRound, evidence, msgsPropose, msgsPrevote, msgsPrecommit,
-          localClock, realTime, receivedTimelyProposal, inspectedProposal, action,
-          beginConsensus, endConsensus, lastBeginConsensus, proposalTime, proposalReceivedTime>>
 
 (********************* PROTOCOL INITIALIZATION ******************************)
 \* @type: (ROUND) => Set(PROPMESSAGE);
@@ -255,30 +283,37 @@ BenignRoundsInMessages(msgfun) ==
 \* The initial states of the protocol. Some faults can be in the system already.
 Init ==
     /\ round = [p \in Corr |-> 0]
-    /\ \/ /\ ~ClockDrift
-          /\ localClock \in [Corr -> 0..Accuracy]
-       \/ /\ ClockDrift
-          /\ localClock = [p \in Corr |-> 0]
+    /\ localClock \in [Corr -> MinTimestamp..(MinTimestamp + Precision)]
     /\ realTime = 0
     /\ step = [p \in Corr |-> "PROPOSE"]
     /\ decision = [p \in Corr |-> NilDecision]
     /\ lockedValue = [p \in Corr |-> NilValue]
     /\ lockedRound = [p \in Corr |-> NilRound]
-    /\ validValue = [p \in Corr |-> NilValue]
+    /\ validValue = [p \in Corr |-> NilProposal]
     /\ validRound = [p \in Corr |-> NilRound]
     /\ msgsPropose \in [Rounds -> SUBSET AllFaultyProposals]
     /\ msgsPrevote \in [Rounds -> SUBSET AllFaultyPrevotes]
     /\ msgsPrecommit \in [Rounds -> SUBSET AllFaultyPrecommits]
-    /\ receivedTimelyProposal = EmptyRcvProp
-    /\ inspectedProposal = [r \in Rounds |-> EmptyProcSet]
+    /\ receivedTimelyProposal = [p \in Corr |-> {}]
+    /\ inspectedProposal = [r \in Rounds, p \in Corr |-> NilTimestamp]
     /\ BenignRoundsInMessages(msgsPropose)
     /\ BenignRoundsInMessages(msgsPrevote)
     /\ BenignRoundsInMessages(msgsPrecommit)
-    /\ evidence = EmptyMsgSet
+    /\ evidence = {}
     /\ action' = "Init"
-    /\ beginConsensus = Min({localClock[p] : p \in Corr})
+    /\ beginRound = 
+      [r \in Rounds |-> 
+        IF r = 0
+        THEN Min({localClock[p] : p \in Corr})
+        ELSE MaxTimestamp
+      ]
     /\ endConsensus = [p \in Corr |-> NilTimestamp]
-    /\ lastBeginConsensus = Max({localClock[p] : p \in Corr})
+    /\ lastBeginRound = 
+      [r \in Rounds |-> 
+        IF r = 0
+        THEN Max({localClock[p] : p \in Corr})
+        ELSE NilTimestamp
+      ]
     /\ proposalTime = [r \in Rounds |-> NilTimestamp]
     /\ proposalReceivedTime = [r \in Rounds |-> NilTimestamp]
 
@@ -296,7 +331,7 @@ BroadcastProposal(pSrc, pRound, pProposal, pValidRound) ==
       validRound |-> pValidRound
     ]
   IN
-  msgsPropose' = [msgsPropose EXCEPT ![pRound] = msgsPropose[pRound] \union {newMsg}]
+  /\ msgsPropose' = [msgsPropose EXCEPT ![pRound] = msgsPropose[pRound] \union {newMsg}]
 
 \* @type: (PROCESS, ROUND, PROPOSAL) => Bool;
 BroadcastPrevote(pSrc, pRound, pId) ==
@@ -310,7 +345,7 @@ BroadcastPrevote(pSrc, pRound, pId) ==
       id    |-> pId
     ]
   IN
-  msgsPrevote' = [msgsPrevote EXCEPT ![pRound] = msgsPrevote[pRound] \union {newMsg}]
+  /\ msgsPrevote' = [msgsPrevote EXCEPT ![pRound] = msgsPrevote[pRound] \union {newMsg}]
 
 \* @type: (PROCESS, ROUND, PROPOSAL) => Bool;
 BroadcastPrecommit(pSrc, pRound, pId) ==
@@ -324,7 +359,7 @@ BroadcastPrecommit(pSrc, pRound, pId) ==
       id    |-> pId
     ]
   IN
-  msgsPrecommit' = [msgsPrecommit EXCEPT ![pRound] = msgsPrecommit[pRound] \union {newMsg}]
+  /\ msgsPrecommit' = [msgsPrecommit EXCEPT ![pRound] = msgsPrecommit[pRound] \union {newMsg}]
 
 (***************************** TIME **************************************)
 
@@ -339,14 +374,14 @@ SynchronizedLocalClocks ==
                /\ localClock[q] - localClock[p] < Precision
     
 \* [PBTS-PROPOSE.0]
-\* @type: (VALUE, TIME) => PROPOSAL;
-Proposal(v, t) ==
-    <<v, t>>
+\* @type: (VALUE, TIME, ROUND) => PROPOSAL;
+Proposal(v, t, r) ==
+    <<v, t, r>>
 
 \* [PBTS-DECISION-ROUND.0]
-\* @type: (VALUE, TIME, ROUND) => DECISION;
-Decision(v, t, r) ==
-    <<v, t, r>>
+\* @type: (PROPOSAL, ROUND) => DECISION;
+Decision(p, r) ==
+    <<p, r>>
 
 (**************** MESSAGE PROCESSING TRANSITIONS *************************)
 \* lines 12-13
@@ -354,7 +389,10 @@ Decision(v, t, r) ==
 StartRound(p, r) ==
    /\ step[p] /= "DECIDED" \* a decided process does not participate in consensus
    /\ round' = [round EXCEPT ![p] = r]
-   /\ step' = [step EXCEPT ![p] = "PROPOSE"] 
+   /\ step' = [step EXCEPT ![p] = "PROPOSE"]
+   \* We only need to update (last)beginRound[r] once a process enters round `r`
+   /\ beginRound' = [beginRound EXCEPT ![r] = Min2(@, localClock[p])]
+   /\ lastBeginRound' = [lastBeginRound EXCEPT ![r] = Max2(@, localClock[p])]
 
 \* lines 14-19, a proposal may be sent later
 \* @type: (PROCESS) => Bool;
@@ -365,20 +403,22 @@ InsertProposal(p) ==
     \* if the proposer is sending a proposal, then there are no other proposals
     \* by the correct processes for the same round
   /\ \A m \in msgsPropose[r]: m.src /= p
+  \* /\ localClock[p] > 
   /\ \E v \in ValidValues: 
-      LET value == 
-        IF validValue[p] /= NilValue 
+      LET proposal == 
+        IF validValue[p] /= NilProposal 
         THEN validValue[p]
-        ELSE v
-      IN LET 
-        proposal == Proposal(value, localClock[p]) 
+        ELSE Proposal(v, localClock[p], r)
       IN               
-      /\ BroadcastProposal(p, round[p], proposal, validRound[p])
+      /\ BroadcastProposal(p, r, proposal, validRound[p])
       /\ proposalTime' = [proposalTime EXCEPT ![r] = realTime]
-  /\ UNCHANGED <<evidence, round, decision, lockedValue, lockedRound,
-                validValue, step, validRound, msgsPrevote, msgsPrecommit,
-                localClock, realTime, receivedTimelyProposal, inspectedProposal,
-                beginConsensus, endConsensus, lastBeginConsensus, proposalReceivedTime>>
+  /\ UNCHANGED <<temporalVars, coreVars>>
+  /\ UNCHANGED 
+    <<(*msgsPropose,*) msgsPrevote, msgsPrecommit, 
+    evidence, receivedTimelyProposal, inspectedProposal>>
+  /\ UNCHANGED
+    <<beginRound, endConsensus, lastBeginRound,
+    (*proposalTime,*) proposalReceivedTime>>
   /\ action' = "InsertProposal"
   
 \* a new action used to filter messages that are not on time
@@ -394,92 +434,120 @@ ReceiveProposal(p) ==
             type       |-> "PROPOSAL", 
             src        |-> Proposer[round[p]],
             round      |-> round[p], 
-            proposal   |-> Proposal(v, t), 
+            proposal   |-> Proposal(v, t, r), 
             validRound |-> NilRound
           ] 
        IN
       /\ msg \in msgsPropose[round[p]] 
-      /\ p \notin inspectedProposal[r]
-      /\ <<p, msg>> \notin receivedTimelyProposal
-      /\ inspectedProposal' = [inspectedProposal EXCEPT ![r] = @ \union {p}]
-      /\ \/ /\ localClock[p] - Precision < t 
-            /\ t < localClock[p] + Precision + Delay
-            /\ receivedTimelyProposal' = receivedTimelyProposal \union {<<p, msg>>}
-            /\ \/ /\ proposalReceivedTime[r] = NilTimestamp
-                  /\ proposalReceivedTime' = [proposalReceivedTime EXCEPT ![r] = realTime]
-               \/ /\ proposalReceivedTime[r] /= NilTimestamp
-                  /\ UNCHANGED proposalReceivedTime
-         \/ /\ \/ localClock[p] - Precision >= t
-               \/ t >= localClock[p] + Precision + Delay
-            /\ UNCHANGED <<receivedTimelyProposal, proposalReceivedTime>>
-      /\ UNCHANGED <<round, step, decision, lockedValue, lockedRound,
-          validValue, validRound, evidence, msgsPropose, msgsPrevote, msgsPrecommit,
-          localClock, realTime, beginConsensus, endConsensus, lastBeginConsensus, proposalTime>>
+      /\ inspectedProposal[r,p] = NilTimestamp
+      /\ msg \notin receivedTimelyProposal[p]
+      /\ inspectedProposal' = [inspectedProposal EXCEPT ![r,p] = localClock[p]]
+      /\ LET 
+          isTimely == IsTimely(localClock[p], t)
+         IN
+          \/ /\ isTimely
+             /\ receivedTimelyProposal' = [receivedTimelyProposal EXCEPT ![p] = @ \union {msg}]
+             /\ LET
+                  isNilTimestamp == proposalReceivedTime[r] = NilTimestamp
+                IN
+                  \/ /\ isNilTimestamp
+                     /\ proposalReceivedTime' = [proposalReceivedTime EXCEPT ![r] = realTime]
+                  \/ /\ ~isNilTimestamp
+                     /\ UNCHANGED proposalReceivedTime
+          \/ /\ ~isTimely
+             /\ UNCHANGED <<receivedTimelyProposal, proposalReceivedTime>>
+      /\ UNCHANGED <<temporalVars, coreVars>>
+      /\ UNCHANGED
+        <<msgsPropose, msgsPrevote, msgsPrecommit, 
+        evidence(*, receivedTimelyProposal, inspectedProposal*)>>
+      /\ UNCHANGED 
+        <<beginRound, endConsensus, lastBeginRound,
+        proposalTime(*, proposalReceivedTime*)>>
       /\ action' = "ReceiveProposal"
       
 \* lines 22-27
 \* @type: (PROCESS) => Bool;
 UponProposalInPropose(p) ==
   \E v \in Values, t \in Timestamps:
+    LET 
+      r == round[p]
+    IN LET
+      \* @type: PROPOSAL;
+      prop == Proposal(v,t,r)
+    IN
     /\ step[p] = "PROPOSE" (* line 22 *)
     /\ LET 
         \* @type: PROPMESSAGE; 
         msg ==
         [
           type       |-> "PROPOSAL", 
-          src        |-> Proposer[round[p]],
-          round      |-> round[p], 
-          proposal   |-> Proposal(v, t), 
+          src        |-> Proposer[r],
+          round      |-> r, 
+          proposal   |-> prop, 
           validRound |-> NilRound
         ] 
        IN
-      /\ <<p, msg>> \in receivedTimelyProposal \* updated line 22
+      /\ msg \in receivedTimelyProposal[p] \* updated line 22
       /\ evidence' = {msg} \union evidence
     /\ LET mid == (* line 23 *)
-         IF IsValid(v) /\ (lockedRound[p] = NilRound \/ lockedValue[p] = v)
-         THEN Id(Proposal(v, t))
+         IF IsValid(prop) /\ (lockedRound[p] = NilRound \/ lockedValue[p] = v)
+         THEN Id(prop)
          ELSE NilProposal
        IN
-       BroadcastPrevote(p, round[p], mid) \* lines 24-26
+       BroadcastPrevote(p, r, mid) \* lines 24-26
     /\ step' = [step EXCEPT ![p] = "PREVOTE"]
-    /\ UNCHANGED <<round, decision, lockedValue, lockedRound,
-                   validValue, validRound, msgsPropose, msgsPrecommit,
-                   localClock, realTime, receivedTimelyProposal, inspectedProposal,
-                   beginConsensus, endConsensus, lastBeginConsensus, proposalTime, proposalReceivedTime>>
+    /\ UNCHANGED <<temporalVars, invariantVars>>
+    /\ UNCHANGED
+      <<round, (*step,*) decision, lockedValue, 
+      lockedRound, validValue, validRound>>
+    /\ UNCHANGED 
+      <<msgsPropose, (*msgsPrevote,*) msgsPrecommit, 
+      (*evidence,*) receivedTimelyProposal, inspectedProposal>>
     /\ action' = "UponProposalInPropose"
 
 \* lines 28-33        
 \* [PBTS-ALG-OLD-PREVOTE.0]
 \* @type: (PROCESS) => Bool;
 UponProposalInProposeAndPrevote(p) ==
-  \E v \in Values, t1 \in Timestamps, t2 \in Timestamps, vr \in Rounds:
-    /\ step[p] = "PROPOSE" /\ 0 <= vr /\ vr < round[p] \* line 28, the while part
-    /\ LET 
+  \E v \in Values, t \in Timestamps, vr \in Rounds, pr \in Rounds:
+    LET 
+      r == round[p]
+    IN LET
+      \* @type: PROPOSAL;
+      prop == Proposal(v,t,pr)
+    IN
+    /\ step[p] = "PROPOSE" /\ 0 <= vr /\ vr < r \* line 28, the while part
+    /\ pr <= vr
+    /\ LET
         \* @type: PROPMESSAGE; 
         msg ==
         [
           type       |-> "PROPOSAL", 
-          src        |-> Proposer[round[p]],
-          round      |-> round[p], 
-          proposal   |-> Proposal(v, t1), 
+          src        |-> Proposer[r],
+          round      |-> r, 
+          proposal   |-> prop, 
           validRound |-> vr
         ]
        IN
-       /\ <<p, msg>> \in receivedTimelyProposal \* updated line 28
-       /\ LET PV == { m \in msgsPrevote[vr]: m.id = Id(Proposal(v, t2)) } IN
+       \* Changed from 001: no need to re-check timeliness
+       /\ msg \in msgsPropose[r] \* line 28
+       /\ LET PV == { m \in msgsPrevote[vr]: m.id = Id(prop) } IN
           /\ Cardinality(PV) >= THRESHOLD2 \* line 28
           /\ evidence' = PV \union {msg} \union evidence
     /\ LET mid == (* line 29 *)
-         IF IsValid(v) /\ (lockedRound[p] <= vr \/ lockedValue[p] = v)
-         THEN Id(Proposal(v, t1)) 
+         IF IsValid(prop) /\ (lockedRound[p] <= vr \/ lockedValue[p] = v)
+         THEN Id(prop) 
          ELSE NilProposal 
        IN
-       BroadcastPrevote(p, round[p], mid) \* lines 24-26
+       BroadcastPrevote(p, r, mid) \* lines 24-26
     /\ step' = [step EXCEPT ![p] = "PREVOTE"]
-    /\ UNCHANGED <<round, decision, lockedValue, lockedRound,
-                   validValue, validRound, msgsPropose, msgsPrecommit,
-                   localClock, realTime, receivedTimelyProposal, inspectedProposal,
-                   beginConsensus, endConsensus, lastBeginConsensus, proposalTime, proposalReceivedTime>>
+    /\ UNCHANGED <<temporalVars, invariantVars>>
+    /\ UNCHANGED
+      <<round, (*step,*) decision, lockedValue, 
+      lockedRound, validValue, validRound>>
+    /\ UNCHANGED 
+      <<msgsPropose, (*msgsPrevote,*) msgsPrecommit, 
+      (*evidence,*) receivedTimelyProposal, inspectedProposal>>
     /\ action' = "UponProposalInProposeAndPrevote"
                      
 \* lines 34-35 + lines 61-64 (onTimeoutPrevote)
@@ -494,10 +562,13 @@ UponQuorumOfPrevotesAny(p) ==
       /\ evidence' = MyEvidence \union evidence
       /\ BroadcastPrecommit(p, round[p], NilProposal)
       /\ step' = [step EXCEPT ![p] = "PRECOMMIT"]
-      /\ UNCHANGED <<round, decision, lockedValue, lockedRound,
-                    validValue, validRound, msgsPropose, msgsPrevote,
-                    localClock, realTime, receivedTimelyProposal, inspectedProposal,
-                    beginConsensus, endConsensus, lastBeginConsensus, proposalTime, proposalReceivedTime>>
+      /\ UNCHANGED <<temporalVars, invariantVars>>
+      /\ UNCHANGED
+        <<round, (*step,*) decision, lockedValue, 
+        lockedRound, validValue, validRound>>
+      /\ UNCHANGED 
+        <<msgsPropose, msgsPrevote, (*msgsPrecommit, *)
+        (*evidence,*) receivedTimelyProposal, inspectedProposal>>
       /\ action' = "UponQuorumOfPrevotesAny"
                      
 \* lines 36-46
@@ -505,36 +576,47 @@ UponQuorumOfPrevotesAny(p) ==
 \* @type: (PROCESS) => Bool;
 UponProposalInPrevoteOrCommitAndPrevote(p) ==
   \E v \in ValidValues, t \in Timestamps, vr \in RoundsOrNil:
+    LET 
+      r == round[p]
+    IN LET
+      \* @type: PROPOSAL;
+      prop == Proposal(v,t,r)
+    IN
     /\ step[p] \in {"PREVOTE", "PRECOMMIT"} \* line 36
     /\ LET
         \* @type: PROPMESSAGE; 
         msg ==
         [
           type       |-> "PROPOSAL", 
-          src        |-> Proposer[round[p]],
-          round      |-> round[p], 
-          proposal   |-> Proposal(v, t), 
+          src        |-> Proposer[r],
+          round      |-> r, 
+          proposal   |-> prop, 
           validRound |-> vr
         ] 
        IN 
-        /\ <<p, msg>> \in receivedTimelyProposal \* updated line 36
-        /\ LET PV == { m \in msgsPrevote[round[p]]: m.id = Id(Proposal(v, t)) } IN
+        \* Changed from 001: no need to re-check timeliness
+        /\ msg \in msgsPropose[r] \* line 36
+        /\ LET PV == { m \in msgsPrevote[r]: m.id = Id(prop) } IN
           /\ Cardinality(PV) >= THRESHOLD2 \* line 36
           /\ evidence' = PV \union {msg} \union evidence
     /\  IF step[p] = "PREVOTE"
         THEN \* lines 38-41:
           /\ lockedValue' = [lockedValue EXCEPT ![p] = v]
-          /\ lockedRound' = [lockedRound EXCEPT ![p] = round[p]]
-          /\ BroadcastPrecommit(p, round[p], Id(Proposal(v, t)))
+          /\ lockedRound' = [lockedRound EXCEPT ![p] = r]
+          /\ BroadcastPrecommit(p, r, Id(prop))
           /\ step' = [step EXCEPT ![p] = "PRECOMMIT"]
         ELSE
           UNCHANGED <<lockedValue, lockedRound, msgsPrecommit, step>>
       \* lines 42-43
-    /\ validValue' = [validValue EXCEPT ![p] = v]
-    /\ validRound' = [validRound EXCEPT ![p] = round[p]]
-    /\ UNCHANGED <<round, decision, msgsPropose, msgsPrevote,
-                  localClock, realTime, receivedTimelyProposal, inspectedProposal,
-                  beginConsensus, endConsensus, lastBeginConsensus, proposalTime, proposalReceivedTime>>
+    /\ validValue' = [validValue EXCEPT ![p] = prop]
+    /\ validRound' = [validRound EXCEPT ![p] = r]
+    /\ UNCHANGED <<temporalVars, invariantVars>>
+    /\ UNCHANGED
+      <<round, (*step,*) decision(*, lockedValue, 
+      lockedRound, validValue, validRound*)>>
+    /\ UNCHANGED 
+      <<msgsPropose, msgsPrevote, (*msgsPrecommit, *)
+      (*evidence,*) receivedTimelyProposal, inspectedProposal>>
     /\ action' = "UponProposalInPrevoteOrCommitAndPrevote"
 
 \* lines 47-48 + 65-67 (onTimeoutPrecommit)
@@ -547,11 +629,17 @@ UponQuorumOfPrecommitsAny(p) ==
       /\ Cardinality(Committers) >= THRESHOLD2 \* line 47
       /\ evidence' = MyEvidence \union evidence
       /\ round[p] + 1 \in Rounds
-      /\ StartRound(p, round[p] + 1)   
-      /\ UNCHANGED <<decision, lockedValue, lockedRound, validValue,
-                    validRound, msgsPropose, msgsPrevote, msgsPrecommit,
-                    localClock, realTime, receivedTimelyProposal, inspectedProposal,
-                    beginConsensus, endConsensus, lastBeginConsensus, proposalTime, proposalReceivedTime>>
+      /\ StartRound(p, round[p] + 1)
+      /\ UNCHANGED temporalVars
+      /\ UNCHANGED
+        <<(*beginRound,*) endConsensus, (*lastBeginRound,*)
+        proposalTime, proposalReceivedTime>>
+      /\ UNCHANGED
+        <<(*round, step,*) decision, lockedValue, 
+        lockedRound, validValue, validRound>>
+      /\ UNCHANGED 
+        <<msgsPropose, msgsPrevote, msgsPrecommit,
+        (*evidence,*) receivedTimelyProposal, inspectedProposal>>
       /\ action' = "UponQuorumOfPrecommitsAny"
                      
 \* lines 49-54        
@@ -559,7 +647,11 @@ UponQuorumOfPrecommitsAny(p) ==
 \* @type: (PROCESS) => Bool;
 UponProposalInPrecommitNoDecision(p) ==
   /\ decision[p] = NilDecision \* line 49
-  /\ \E v \in ValidValues, t \in Timestamps (* line 50*) , r \in Rounds, vr \in RoundsOrNil:
+  /\ \E v \in ValidValues, t \in Timestamps (* line 50*) , r \in Rounds, pr \in Rounds, vr \in RoundsOrNil:
+    LET
+      \* @type: PROPOSAL;
+      prop == Proposal(v,t,pr)
+    IN
     /\ LET
         \* @type: PROPMESSAGE; 
         msg == 
@@ -567,24 +659,30 @@ UponProposalInPrecommitNoDecision(p) ==
           type       |-> "PROPOSAL", 
           src        |-> Proposer[r],
           round      |-> r, 
-          proposal   |-> Proposal(v, t), 
+          proposal   |-> prop, 
           validRound |-> vr
         ] 
        IN 
      /\ msg \in msgsPropose[r] \* line 49
-     /\ p \in inspectedProposal[r]
-     /\ LET PV == { m \in msgsPrecommit[r]: m.id = Id(Proposal(v, t)) } IN
+     /\ inspectedProposal[r,p] /= NilTimestamp \* Keep?
+     /\ LET PV == { m \in msgsPrecommit[r]: m.id = Id(prop) } IN
        /\ Cardinality(PV) >= THRESHOLD2 \* line 49
        /\ evidence' = PV \union {msg} \union evidence
-       /\ decision' = [decision EXCEPT ![p] = Decision(v, t, round[p])] \* update the decision, line 51
+       /\ decision' = [decision EXCEPT ![p] = Decision(prop, r)] \* update the decision, line 51
     \* The original algorithm does not have 'DECIDED', but it increments the height.
     \* We introduced 'DECIDED' here to prevent the process from changing its decision.
        /\ endConsensus' = [endConsensus EXCEPT ![p] = localClock[p]]
        /\ step' = [step EXCEPT ![p] = "DECIDED"]
-       /\ UNCHANGED <<round, lockedValue, lockedRound, validValue,
-                     validRound, msgsPropose, msgsPrevote, msgsPrecommit,
-                     localClock, realTime, receivedTimelyProposal, inspectedProposal,
-                     beginConsensus, lastBeginConsensus, proposalTime, proposalReceivedTime>>
+       /\ UNCHANGED temporalVars
+       /\ UNCHANGED
+         <<round, (*step, decision,*) lockedValue, 
+         lockedRound, validValue, validRound>>
+       /\ UNCHANGED 
+         <<msgsPropose, msgsPrevote, msgsPrecommit,
+         (*evidence,*) receivedTimelyProposal, inspectedProposal>>
+       /\ UNCHANGED
+         <<beginRound, (*endConsensus,*) lastBeginRound,
+         proposalTime, proposalReceivedTime>>
        /\ action' = "UponProposalInPrecommitNoDecision"
                                                           
 \* the actions below are not essential for safety, but added for completeness
@@ -596,10 +694,13 @@ OnTimeoutPropose(p) ==
   /\ p /= Proposer[round[p]]
   /\ BroadcastPrevote(p, round[p], NilProposal)
   /\ step' = [step EXCEPT ![p] = "PREVOTE"]
-  /\ UNCHANGED <<round, lockedValue, lockedRound, validValue,
-                validRound, decision, evidence, msgsPropose, msgsPrecommit,
-                localClock, realTime, receivedTimelyProposal, inspectedProposal,
-                beginConsensus, endConsensus, lastBeginConsensus, proposalTime, proposalReceivedTime>>
+  /\ UNCHANGED <<temporalVars, invariantVars>>
+  /\ UNCHANGED
+    <<round, (*step,*) decision, lockedValue, 
+    lockedRound, validValue, validRound>>
+  /\ UNCHANGED 
+    <<msgsPropose, (*msgsPrevote,*) msgsPrecommit,
+    evidence, receivedTimelyProposal, inspectedProposal>>
   /\ action' = "OnTimeoutPropose"
 
 \* lines 44-46
@@ -611,10 +712,13 @@ OnQuorumOfNilPrevotes(p) ==
     /\ evidence' = PV \union evidence
     /\ BroadcastPrecommit(p, round[p], Id(NilProposal))
     /\ step' = [step EXCEPT ![p] = "PRECOMMIT"]
-    /\ UNCHANGED <<round, lockedValue, lockedRound, validValue,
-                  validRound, decision, msgsPropose, msgsPrevote,
-                  localClock, realTime, receivedTimelyProposal, inspectedProposal,
-                  beginConsensus, endConsensus, lastBeginConsensus, proposalTime, proposalReceivedTime>>
+    /\ UNCHANGED <<temporalVars, invariantVars>>
+    /\ UNCHANGED
+      <<round, (*step,*) decision, lockedValue, 
+      lockedRound, validValue, validRound>>
+    /\ UNCHANGED 
+      <<msgsPropose, msgsPrevote, (*msgsPrecommit,*)
+      (*evidence,*) receivedTimelyProposal, inspectedProposal>>
     /\ action' = "OnQuorumOfNilPrevotes"
 
 \* lines 55-56
@@ -627,10 +731,16 @@ OnRoundCatchup(p) ==
         /\ Cardinality(Faster) >= THRESHOLD1
         /\ evidence' = MyEvidence \union evidence
         /\ StartRound(p, r)
-        /\ UNCHANGED <<decision, lockedValue, lockedRound, validValue,
-                      validRound, msgsPropose, msgsPrevote, msgsPrecommit,
-                      localClock, realTime, receivedTimelyProposal, inspectedProposal,
-                      beginConsensus, endConsensus, lastBeginConsensus, proposalTime, proposalReceivedTime>>
+        /\ UNCHANGED temporalVars
+        /\ UNCHANGED
+          <<(*beginRound,*) endConsensus, (*lastBeginRound,*)
+          proposalTime, proposalReceivedTime>>
+        /\ UNCHANGED
+          <<(*round, step,*) decision, lockedValue, 
+          lockedRound, validValue, validRound>>
+        /\ UNCHANGED 
+          <<msgsPropose, msgsPrevote, msgsPrecommit,
+          (*evidence,*) receivedTimelyProposal, inspectedProposal>>
         /\ action' = "OnRoundCatchup"
 
 
@@ -638,28 +748,24 @@ OnRoundCatchup(p) ==
 \* advance the global clock
 \* @type: Bool;
 AdvanceRealTime == 
-    /\ realTime < MaxTimestamp
-    /\ realTime' = realTime + 1
-    /\ \/ /\ ~ClockDrift
-          /\ localClock' = [p \in Corr |-> localClock[p] + 1]  
-       \/ /\ ClockDrift
-          /\ UNCHANGED localClock
-    /\ UNCHANGED <<round, step, decision, lockedValue, lockedRound,
-                  validValue, validRound, evidence, msgsPropose, msgsPrevote, msgsPrecommit,
-                  localClock, receivedTimelyProposal, inspectedProposal,
-                  beginConsensus, endConsensus, lastBeginConsensus, proposalTime, proposalReceivedTime>> 
+    /\ ValidTime(realTime)
+    /\ \E t \in Timestamps:
+      /\ t > realTime
+      /\ realTime' = t
+      /\ localClock' = [p \in Corr |-> localClock[p] + (t - realTime)]  
+    /\ UNCHANGED <<coreVars, bookkeepingVars, invariantVars>>
     /\ action' = "AdvanceRealTime"
     
-\* advance the local clock of node p
-\* @type: (PROCESS) => Bool;
-AdvanceLocalClock(p) ==
-    /\ localClock[p] < MaxTimestamp
-    /\ localClock' = [localClock EXCEPT ![p] = @ + 1]
-    /\ UNCHANGED <<round, step, decision, lockedValue, lockedRound,
-                  validValue, validRound, evidence, msgsPropose, msgsPrevote, msgsPrecommit,
-                  realTime, receivedTimelyProposal, inspectedProposal,
-                  beginConsensus, endConsensus, lastBeginConsensus, proposalTime, proposalReceivedTime>>
-    /\ action' = "AdvanceLocalClock"
+\* advance the local clock of node p to some larger time t, not necessarily by 1
+\* #type: (PROCESS) => Bool;
+\* AdvanceLocalClock(p) ==
+\*     /\ ValidTime(localClock[p])
+\*     /\ \E t \in Timestamps:
+\*       /\ t > localClock[p] 
+\*       /\ localClock' = [localClock EXCEPT ![p] = t]
+\*     /\ UNCHANGED <<coreVars, bookkeepingVars, invariantVars>>
+\*     /\ UNCHANGED realTime
+\*     /\ action' = "AdvanceLocalClock"
 
 \* process timely messages
 \* @type: (PROCESS) => Bool;
@@ -684,10 +790,8 @@ MessageProcessing(p) ==
  * A system transition. In this specificatiom, the system may eventually deadlock,
  * e.g., when all processes decide. This is expected behavior, as we focus on safety.
  *)
-Next ==
+Next == 
   \/ AdvanceRealTime
-  \/ /\ ClockDrift
-     /\ \E p \in Corr: AdvanceLocalClock(p)
   \/ /\ SynchronizedLocalClocks
      /\ \E p \in Corr: MessageProcessing(p)
 
@@ -700,59 +804,62 @@ AgreementOnValue ==
     \A p, q \in Corr:
         /\ decision[p] /= NilDecision
         /\ decision[q] /= NilDecision
-        => \E v \in ValidValues, t1 \in Timestamps, t2 \in Timestamps, r1 \in Rounds, r2 \in Rounds : 
-            /\ decision[p] = Decision(v, t1, r1)
-            /\ decision[q] = Decision(v, t2, r2)
-
-\* [PBTS-INV-TIME-AGR.0]
-AgreementOnTime ==
-    \A p, q \in Corr: 
-        \A v1 \in ValidValues, v2 \in ValidValues, t1 \in Timestamps, t2 \in Timestamps, r \in Rounds :
-            /\ decision[p] = Decision(v1, t1, r)
-            /\ decision[q] = Decision(v2, t2, r)
-            => t1 = t2
+        => \E v \in ValidValues, t \in Timestamps, pr \in Rounds, r1 \in Rounds, r2 \in Rounds : 
+            LET prop == Proposal(v,t,pr)
+            IN
+            /\ decision[p] = Decision(prop, r1)
+            /\ decision[q] = Decision(prop, r2)
 
 \* [PBTS-CONSENSUS-TIME-VALID.0]
 ConsensusTimeValid ==
-    \A p \in Corr, t \in Timestamps : 
+    \A p \in Corr: 
     \* if a process decides on v and t
-    (\E v \in ValidValues, r \in Rounds : decision[p] = Decision(v, t, r))
+      \E v \in ValidValues, t \in Timestamps, pr \in Rounds, dr \in Rounds : 
+        decision[p] = Decision(Proposal(v,t,pr), dr)
         \* then 
-        => /\ beginConsensus - Precision <= t 
-           /\ t < endConsensus[p] + Precision + Delay
+        \* TODO: consider tighter bound where beginRound[pr] is replaced
+        \* w/ MedianOfRound[pr]
+        => (/\ beginRound[pr] - Precision - Delay <= t 
+            /\ t <= endConsensus[p] + Precision)
 
 \* [PBTS-CONSENSUS-SAFE-VALID-CORR-PROP.0]
 ConsensusSafeValidCorrProp ==
-    \A v \in ValidValues, t \in Timestamps :
-        \* if the proposer in the first round is correct
-       (/\ Proposer[0] \in Corr
-        \* and there exists a process that decided on v, t 
-        /\ \E p \in Corr, r \in Rounds : decision[p] = Decision(v, t, r))
-            \* then t is between the minimal and maximal initial local time
-            => /\ beginConsensus <= t 
-               /\ t <= lastBeginConsensus
+    \A v \in ValidValues:
+      \* and there exists a process that decided on v, t 
+      /\ \E p \in Corr, t \in Timestamps, pr \in Rounds, dr \in Rounds : 
+        \* if the proposer in the round is correct
+        (/\ Proposer[pr] \in Corr
+        /\ decision[p] = Decision(Proposal(v,t,pr), dr))
+          \* then t is between the minimal and maximal initial local time
+          => /\ beginRound[pr] <= t 
+             /\ t <= lastBeginRound[pr]
 
 \* [PBTS-CONSENSUS-REALTIME-VALID-CORR.0]
 ConsensusRealTimeValidCorr ==
-    \A t \in Timestamps, r \in Rounds :
-       (/\ \E p \in Corr, v \in ValidValues : decision[p] = Decision(v, t, r) 
-        /\ proposalTime[r] /= NilTimestamp)
-        => /\ proposalTime[r] - Accuracy < t
-           /\ t < proposalTime[r] + Accuracy
+  \A r \in Rounds :
+    \E p \in Corr, v \in ValidValues, t \in Timestamps, pr \in Rounds: 
+     (/\ decision[p] = Decision(Proposal(v,t,pr), r) 
+      /\ proposalTime[r] /= NilTimestamp)
+        => (/\ proposalTime[r] - Precision <= t
+            /\ t <= proposalTime[r] + Precision)
 
 \* [PBTS-CONSENSUS-REALTIME-VALID.0]
 ConsensusRealTimeValid ==
     \A t \in Timestamps, r \in Rounds :
-       (\E p \in Corr, v \in ValidValues : decision[p] = Decision(v, t, r)) 
-        => /\ proposalReceivedTime[r] - Accuracy - Precision < t
-           /\ t < proposalReceivedTime[r] + Accuracy + Precision + Delay
+       (\E p \in Corr, v \in ValidValues, pr \in Rounds : 
+        decision[p] = Decision(Proposal(v,t,pr), r)) 
+        => /\ proposalReceivedTime[r] - Precision < t
+           /\ t < proposalReceivedTime[r] + Precision + Delay
+
+DecideAfterMin == TRUE
+  \* if decide => time > min
 
 \* [PBTS-MSG-FAIR.0]
 BoundedDelay ==
     \A r \in Rounds : 
         (/\ proposalTime[r] /= NilTimestamp
          /\ proposalTime[r] + Delay < realTime)
-            => inspectedProposal[r] = Corr
+            => \A p \in Corr: inspectedProposal[r,p] /= NilTimestamp
 
 \* [PBTS-CONSENSUS-TIME-LIVE.0]
 ConsensusTimeLive ==
@@ -761,19 +868,18 @@ ConsensusTimeLive ==
         /\ proposalTime[r] + Delay < realTime 
         /\ Proposer[r] \in Corr
         /\ round[p] <= r)
-            => \E msg \in RoundProposals(r) : <<p, msg>> \in receivedTimelyProposal
+            => \E msg \in RoundProposals(r) : msg \in receivedTimelyProposal[p]
 
 \* a conjunction of all invariants
 Inv ==
     /\ AgreementOnValue 
-    /\ AgreementOnTime
     /\ ConsensusTimeValid
     /\ ConsensusSafeValidCorrProp
-    /\ ConsensusRealTimeValid
-    /\ ConsensusRealTimeValidCorr
-    /\ BoundedDelay
+    \* /\ ConsensusRealTimeValid
+    \* /\ ConsensusRealTimeValidCorr
+    \* /\ BoundedDelay
 
-Liveness ==
-    ConsensusTimeLive    
+\* Liveness ==
+\*     ConsensusTimeLive    
 
 =============================================================================    

spec/consensus/proposer-based-timestamp/tla/typedefs.tla

@@ -7,9 +7,8 @@
   @typeAlias: ACTION = Str;
   @typeAlias: TRACE = Seq(Str);
   @typeAlias: TIME = Int;
-  @typeAlias: PROPOSAL = <<VALUE, TIME>>;
-  @typeAlias: DECISION = <<VALUE, TIME, ROUND>>;
-  @typeAlias: RCVPROP = <<PROCESS, PROPMESSAGE>>;
+  @typeAlias: PROPOSAL = <<VALUE, TIME, ROUND>>;
+  @typeAlias: DECISION = <<PROPOSAL, ROUND>>;
   @typeAlias: PROPMESSAGE = 
   [
     type: STEP,