From e8013281281985e3ada7819f42502b09623d24a0 Mon Sep 17 00:00:00 2001
From: William Banfield <4561443+williambanfield@users.noreply.github.com>
Date: Tue, 3 Aug 2021 15:30:05 -0400
Subject: [PATCH] clist: add simple property tests (#6791)

Adds a simple property test to the `clist` package. This test uses the [rapid](https://github.com/flyingmutant/rapid) library and works by modeling the internal clist as a simple array.

Follow up from this mornings workshop with the Regen team.
---
 go.mod                                     |  1 +
 go.sum                                     |  2 +
 internal/libs/clist/clist_property_test.go | 72 ++++++++++++++++++++++
 3 files changed, 75 insertions(+)
 create mode 100644 internal/libs/clist/clist_property_test.go

diff --git a/go.mod b/go.mod
index b6e0fea38..d13c9ea4b 100644
--- a/go.mod
+++ b/go.mod
@@ -39,4 +39,5 @@ require (
 	golang.org/x/net v0.0.0-20210405180319-a5a99cb37ef4
 	google.golang.org/grpc v1.39.0
 	gopkg.in/check.v1 v1.0.0-20200902074654-038fdea0a05b // indirect
+	pgregory.net/rapid v0.4.7 // indirect
 )
diff --git a/go.sum b/go.sum
index 55e08e088..ed2f127b2 100644
--- a/go.sum
+++ b/go.sum
@@ -1437,6 +1437,8 @@ mvdan.cc/lint v0.0.0-20170908181259-adc824a0674b h1:DxJ5nJdkhDlLok9K6qO+5290kphD
 mvdan.cc/lint v0.0.0-20170908181259-adc824a0674b/go.mod h1:2odslEg/xrtNQqCYg2/jCoyKnw3vv5biOc3JnIcYfL4=
 mvdan.cc/unparam v0.0.0-20210104141923-aac4ce9116a7 h1:HT3e4Krq+IE44tiN36RvVEb6tvqeIdtsVSsxmNPqlFU=
 mvdan.cc/unparam v0.0.0-20210104141923-aac4ce9116a7/go.mod h1:hBpJkZE8H/sb+VRFvw2+rBpHNsTBcvSpk61hr8mzXZE=
+pgregory.net/rapid v0.4.7 h1:MTNRktPuv5FNqOO151TM9mDTa+XHcX6ypYeISDVD14g=
+pgregory.net/rapid v0.4.7/go.mod h1:UYpPVyjFHzYBGHIxLFoupi8vwk6rXNzRY9OMvVxFIOU=
 rsc.io/binaryregexp v0.2.0/go.mod h1:qTv7/COck+e2FymRvadv62gMdZztPaShugOCi3I+8D8=
 rsc.io/quote/v3 v3.1.0/go.mod h1:yEA65RcK8LyAZtP9Kv3t0HmxON59tX3rD+tICJqUlj0=
 rsc.io/sampler v1.3.0/go.mod h1:T1hPZKmBbMNahiBKFy5HrXp6adAjACjK9JXDnKaTXpA=
diff --git a/internal/libs/clist/clist_property_test.go b/internal/libs/clist/clist_property_test.go
new file mode 100644
index 000000000..cdc173ee5
--- /dev/null
+++ b/internal/libs/clist/clist_property_test.go
@@ -0,0 +1,72 @@
+package clist_test
+
+import (
+	"testing"
+
+	"github.com/stretchr/testify/require"
+	"pgregory.net/rapid"
+
+	"github.com/tendermint/tendermint/internal/libs/clist"
+)
+
+func TestCListProperties(t *testing.T) {
+	rapid.Check(t, rapid.Run(&clistModel{}))
+}
+
+// clistModel is used by the rapid state machine testing framework.
+// clistModel contains both the clist that is being tested and a slice of *clist.CElements
+// that will be used to model the expected clist behavior.
+type clistModel struct {
+	clist *clist.CList
+
+	model []*clist.CElement
+}
+
+// Init is a method used by the rapid state machine testing library.
+// Init is called when the test starts to initialize the data that will be used
+// in the state machine test.
+func (m *clistModel) Init(t *rapid.T) {
+	m.clist = clist.New()
+	m.model = []*clist.CElement{}
+}
+
+// PushBack defines an action that will be randomly selected across by the rapid state
+// machines testing library. Every call to PushBack calls PushBack on the clist and
+// performs a similar action on the model data.
+func (m *clistModel) PushBack(t *rapid.T) {
+	value := rapid.String().Draw(t, "value").(string)
+	el := m.clist.PushBack(value)
+	m.model = append(m.model, el)
+}
+
+// Remove defines an action that will be randomly selected across by the rapid state
+// machine testing library. Every call to Remove selects an element from the model
+// and calls Remove on the CList with that element. The same element is removed from
+// the model to keep the objects in sync.
+func (m *clistModel) Remove(t *rapid.T) {
+	if len(m.model) == 0 {
+		return
+	}
+	ix := rapid.IntRange(0, len(m.model)-1).Draw(t, "index").(int)
+	value := m.model[ix]
+	m.model = append(m.model[:ix], m.model[ix+1:]...)
+	m.clist.Remove(value)
+}
+
+// Check is a method required by the rapid state machine testing library.
+// Check is run after each action and is used to verify that the state of the object,
+// in this case a clist.CList matches the state of the objec.
+func (m *clistModel) Check(t *rapid.T) {
+	require.Equal(t, len(m.model), m.clist.Len())
+	if len(m.model) == 0 {
+		return
+	}
+	require.Equal(t, m.model[0], m.clist.Front())
+	require.Equal(t, m.model[len(m.model)-1], m.clist.Back())
+
+	iter := m.clist.Front()
+	for _, val := range m.model {
+		require.Equal(t, val, iter)
+		iter = iter.Next()
+	}
+}