Difference testing for 'core' protocol using model generated (heurist…

…ic) traces (#315)

* blanket add difftest

* (assum + trace pass) upstream sync setup

* (full pass) shuffle directories

* (all pass) minor tidyup simibc interface

* (all pass) removes extraneous updateClients, deliverAcks

* (pass) del extra UpdateClient in framework deliverAcks

* (pass) tweak docstrings

* (pass) remove chains map from framework

* (pass) rename, doc simibc

* (regression) tweaks

* (pass) tweaks

* (all pass) bump max gass

* Track traces

* Bumps ci configs

* Try fix gosec

* Try fix sonar

* Try fix docker go build for 1.18

* README

* Move diff artifacts to one dir

* Update README

* Update git LFS

* Update sonar properties

* Update README

* Rename NetworkLink -> OrderedLink

* Better docs main.ts

* Docstring matchState

* Removes some hardcoded nums in core_test.go

* Adds couple of comments to core_test.go

* Docstring for Consequence (.ts)

* Update core package.json

* Ensure typechecks enabled

* Prettier on model.ts

* DEL .editorconfig for ts model

* del eslint

* Bump sonar

* Minor tidyup Traces struct go

* Del unused field in properties.ts

* new semantics: model.ts::expired -> willBeProcessedByStakingModule

* Better comment DeliverPackets

* Better comments for model class fields

* Improve model staking class docstrings

* Improve model staking class docstrings

* Fix more_one_third_val_power_change event

* Update testutil/simibc/ordered_link.go comment

Co-authored-by: Shawn Marshall-Spitzbart <[email protected]>

* Adds event.receive_slash_request_unbonded

* Adds event.receive_slash_request_unbonded

* Better docstring BlockHistory

* Adds 4 new events to constants

* Model endblock method split

* Couple more comments model.ts

* Comment model.ts

* New traces

* DEL traces

* CP (debug)

* (debug) offset adjustment

* tentative, fix regression (debug)

* kill prints

* (tentative) property fix

* Fixes BBCVP power provider

* New traces

* Del 2x prints

* Comment property perf

* rn power -> consumerPower in model

* rn power -> consumerPower in driver

* Removes outdated comment

Co-authored-by: Daniel <[email protected]>
Co-authored-by: Jehan <[email protected]>
Co-authored-by: Shawn Marshall-Spitzbart <[email protected]>

.gitattributes

@@ -0,0 +1 @@
+diff-tests/core/driver/traces.json filter=lfs diff=lfs merge=lfs -text

.github/workflows/automated-tests.yml

@@ -6,12 +6,16 @@ jobs:
     steps:
       # Checks-out your repository under $GITHUB_WORKSPACE, so your job can access it
       - uses: actions/checkout@v2
+        with:
+          lfs: true
+      - name: Checkout LFS objects
+        run: git lfs checkout
       - name: Setup Go
         uses: actions/setup-go@v2
         with:
           go-version: "1.18.0" # The Go version to download (if necessary) and use.
 
-      - name: Unit and e2e tests
+      - name: Unit, e2e and difference tests
         run: go test ./...
 
       - name: Integration tests

.github/workflows/build.yml

@@ -12,11 +12,18 @@ jobs:
     steps:
       - uses: actions/checkout@v2
         with:
-          fetch-depth: 0  # Shallow clones should be disabled for a better relevancy of analysis
+          fetch-depth: 0 # Shallow clones should be disabled for a better relevancy of analysis
+          lfs: true
+      - name: Checkout LFS objects
+        run: git lfs checkout
+      - name: Setup Go
+        uses: actions/setup-go@v2
+        with:
+          go-version: "1.18.0" # The Go version to download (if necessary) and use.
       - name: Test with coverage
         run: go test -coverprofile=coverage.out ./...
       - name: SonarCloud Scan
         uses: SonarSource/sonarcloud-github-action@master
         env:
-          GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }}  # Needed to get PR information, if any
+          GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }} # Needed to get PR information, if any
           SONAR_TOKEN: ${{ secrets.SONAR_TOKEN }}

.github/workflows/golangci-lint.yml

@@ -18,7 +18,7 @@ jobs:
     steps:
       - uses: actions/setup-go@v3
         with:
-          go-version: 1.17
+          go-version: 1.18
       - uses: actions/checkout@v3
       - name: golangci-lint
         uses: golangci/golangci-lint-action@v3

.golangci.yml

@@ -0,0 +1,5 @@
+linters-settings:
+  staticcheck:
+    checks:
+      - all
+      - "-SA1019" # cosmosEd25519 allowed in tests

Dockerfile

@@ -7,6 +7,7 @@ RUN apk add --no-cache $PACKAGES
 
 ENV CGO_ENABLED=0
 ENV GOOS=linux
+ENV GOFLAGS="-buildvcs=false"
 
 WORKDIR /downloads
 

diff-tests/core/README.md

@@ -0,0 +1,136 @@
+# Differential testing for Interchain Security 'core' protocol
+
+This directory contains model and trace generation code for the differential approach to testing Interchain Security. In particular, this work is used to test 'core' (normal operation) features of the protocol.
+
+At a high level, the model consists of one Provider chain and one Consumer chain. There is a single delegator account on the Provider, whose actions will change the delegation and thus the tokens and voting power of the validators. The voting power changes are relayed to the Consumer chain. The entire cycle of unbonding operation maturity is captured, because the Consumer will
+send unbonding maturity packets. Moreoever, slashing is modelled, as the Consumer can initiate slashing actions.
+
+## Scope
+
+### Tested (Unchecked means that work is in progress. Checked means the work is complete.)
+
+The following aspects of the system are tested
+
+- [x] Sending VSC packets from provider to one consumer
+- [x] Sending VSC maturities from one consumer to provider
+- [x] Slashing logic (not including actual token burning)
+- [x] Validator power change
+- [x] Validators leaving or joining the active validor set
+- [x] Consumer initiated slashing
+- [x] Delegation operations
+- [x] Undelegation operations
+- [x] Validator unbonding
+- [x] Valiator jailing
+- [x] Validator tombstoning
+- [x] Packet acknowledgements
+- [x] The 'Bond Based Consumer Voting Power' property ([link](https://github.com/cosmos/ibc/blob/main/spec/app/ics-028-cross-chain-validation/system_model_and_properties.md#system-properties))
+- [ ] The 'Validator Set Replication' property ([link](https://github.com/cosmos/ibc/blob/main/spec/app/ics-028-cross-chain-validation/system_model_and_properties.md#system-properties))
+- [ ] The 'Slashable Consumer Misbehavior' property ([link](https://github.com/cosmos/ibc/blob/main/spec/app/ics-028-cross-chain-validation/system_model_and_properties.md#system-properties)) (_maybe_)
+- [ ] PendingVSC when consumer start (_maybe_)
+- [ ] Redelegation operations
+- [ ] Unjailing operations
+
+### NOT Tested
+
+The following aspects of the system are not tested by this work.
+
+- Completing the IBC handshakes
+- Repairing an expired IBC channel through governance
+- Slashing with non-zero slash factors
+- Submitting proposals
+- Executing proposals
+- Adding a new consumer chain
+- Removing a consumer chain for any reason
+- Distribution of rewards
+- Provider Governance
+- Consumer Governance/Democracy
+- Anything to do with cosmwasm
+- Client expiry
+- Packet timeouts
+- Restarting any chain from exported state
+- Any logic that deals with having _more than one consumer chain_
+- Multiple delegator accounts
+
+## Usage
+
+### Overview
+
+This typescript project contains code for
+
+- Modelling the aspects of the system listed under TESTED above
+- Generating and executing actions against a model system based on those aspects, in order to explore various behaviors. The actions are generated using heuristics and randomness.
+- Recording traces of executions to file
+- Choosing a set of traces in a manner convenient for testing the SUT.
+- Replaying a given existing trace against a new model instance, for debugging purposes.
+
+### Usage prerequisities
+
+```bash
+# nodejs version 16 is required.
+node --version
+# yarn package manager is required
+yarn --version
+# setup the project
+yarn install
+```
+
+### Commands
+
+There are several top level yarn project scripts which can be run via
+
+```bash
+yarn <script_name>
+```
+
+as per the `scripts` entry in [package.json](./package.json). The most important of these are
+
+```bash
+# install the project
+yarn install;
+# build in watch mode. Repeatedly build the project when the src changes
+# recommended to run in background process
+yarn build:watch
+# start main.ts - the entry point to the program
+yarn start <args>
+# test - run the tests in __tests__
+yarn test
+```
+
+The actual functionality has entrypoint in [src/main.ts](./src/main.ts). Please see the file for details. The available functionalities are
+
+```bash
+# generate traces for x seconds
+yarn start gen <num seconds>
+# check properties for x seconds
+yarn start properties <num seconds>
+# create a subset of traces
+yarn start subset <output file abs path> <num event instances (optional)>
+# replay a trace from a file (for debugging)
+yarn start replay <filename> <trace index> <num actions>
+```
+
+### Workflow
+
+A workflow of updating the model and generating new traces for testing against the SUT might look like
+
+```bash
+# Generate traces for 30 seconds
+yarn start gen 30
+# Collect and compact a subset of these traces
+yarn start subset </abs/path/to/core/driver/traces.json> 200
+```
+
+### Extending the model
+
+All of the semantic logic of the model that relates to how the system is supposed to work is contained in [src/model.ts](./src/model.ts). All of the logic for generating actions (and thus traces) against the model is contained in [src/main.ts](./src/main.ts). The remaining files are less important.
+
+### Ensuring a consistent Trace format
+
+The golang test driver must be able to parse the traces output by this Typescript project. Several tools exist to generate golang type definitions from json files. I strongly suggest using [gojsonstruct](https://github.com/twpayne/go-jsonstruct) to generate a new golang definition whenever the json trace format changes. The steps to do this are
+
+```bash
+# Pass the content of traces.json to gojsonstruct binary which will output a golang type definition
+gojsonstruct < <traces.json> > trace.go
+```
+
+The `trace.go` file output from the above command should be reconciled with the content in `difftest/trace.go`.

diff-tests/core/driver/.gitignore

@@ -0,0 +1,2 @@
+*.log
+debug.json

diff-tests/core/driver/common.go

@@ -0,0 +1,91 @@
+package core
+
+import (
+	"time"
+
+	sdk "github.com/cosmos/cosmos-sdk/types"
+	stakingtypes "github.com/cosmos/cosmos-sdk/x/staking/types"
+	abci "github.com/tendermint/tendermint/abci/types"
+	tmproto "github.com/tendermint/tendermint/proto/tendermint/types"
+	tmtypes "github.com/tendermint/tendermint/types"
+)
+
+const P = "provider"
+const C = "consumer"
+
+// ValStates represents the total delegation
+// and bond status of a validator
+type ValStates struct {
+	Delegation           []int
+	Tokens               []int
+	ValidatorExtraTokens []int
+	Status               []stakingtypes.BondStatus
+}
+
+type InitState struct {
+	PKSeeds                []string
+	NumValidators          int
+	MaxValidators          int
+	InitialDelegatorTokens int
+	SlashDoublesign        sdk.Dec
+	SlashDowntime          sdk.Dec
+	UnbondingP             time.Duration
+	UnbondingC             time.Duration
+	Trusting               time.Duration
+	MaxClockDrift          time.Duration
+	BlockSeconds           time.Duration
+	ConsensusParams        *abci.ConsensusParams
+	ValStates              ValStates
+	MaxEntries             int
+}
+
+var initState InitState
+
+func init() {
+	//	tokens === power
+	sdk.DefaultPowerReduction = sdk.NewInt(1)
+	initState = InitState{
+		PKSeeds: []string{
+			// Fixed seeds are used to create the private keys for validators.
+			// The seeds are chosen to ensure that the resulting validators are
+			// sorted in descending order by the staking module.
+			"bbaaaababaabbaabababbaabbbbbbaaa",
+			"abbbababbbabaaaaabaaabbbbababaab",
+			"bbabaabaabbbbbabbbaababbbbabbbbb",
+			"aabbbabaaaaababbbabaabaabbbbbbba"},
+		NumValidators:          4,
+		MaxValidators:          2,
+		InitialDelegatorTokens: 10000000000000,
+		SlashDoublesign:        sdk.NewDec(0),
+		SlashDowntime:          sdk.NewDec(0),
+		UnbondingP:             time.Second * 70,
+		UnbondingC:             time.Second * 50,
+		Trusting:               time.Second * 49,
+		MaxClockDrift:          time.Second * 10000,
+		BlockSeconds:           time.Second * 6,
+		ValStates: ValStates{
+			Delegation:           []int{4000, 3000, 2000, 1000},
+			Tokens:               []int{5000, 4000, 3000, 2000},
+			ValidatorExtraTokens: []int{1000, 1000, 1000, 1000},
+			Status: []stakingtypes.BondStatus{stakingtypes.Bonded, stakingtypes.Bonded,
+				stakingtypes.Unbonded, stakingtypes.Unbonded},
+		},
+		MaxEntries: 1000000,
+		ConsensusParams: &abci.ConsensusParams{
+			Block: &abci.BlockParams{
+				MaxBytes: 9223372036854775807,
+				MaxGas:   9223372036854775807,
+			},
+			Evidence: &tmproto.EvidenceParams{
+				MaxAgeNumBlocks: 302400,
+				MaxAgeDuration:  504 * time.Hour, // 3 weeks is the max duration
+				MaxBytes:        10000,
+			},
+			Validator: &tmproto.ValidatorParams{
+				PubKeyTypes: []string{
+					tmtypes.ABCIPubKeyTypeEd25519,
+				},
+			},
+		},
+	}
+}