Difference testing for 'core' protocol using model generated (heuristic) traces #315

danwt · 2022-08-31T12:44:14Z

Overview

Version 3 of a differential testing approach to testing the 'core' aspects of the Interchain Security system.

This PR contains three major components

A 'simibc' testutil directory containing reusable components for testing ibc connected chains in a fine-grained way (here)
A Typescript project containing modelling code and code for generating traces for difference testing (here)
A golang test driver which is called from a unit test, which runs traces read from a json file, and uses them to test the system (here)

All of the included files are necessary for a full understanding, however, some files contain the most information.

Please find a README file which is contained within the Typescript project. This readme file explains the intentions of the work, and gives usage instructions for adapting the model, and generating traces using it.
model.ts contains the majority of the semantic logic used for modelling the system.
main.ts contains the entry point for interacting with the model and generating traces.
properties.ts contains the code used to check some properties of the protocol, most importantly the bond based consumer voting power property.
core_test.go contains the core driver code used to read json traces and execute them against real instances of the system, simulated using ibc-go/testing. The pivotal unit test is here. There is a second unit test here which serves only to check that the driver is written correctly.

I suggest to read the README first, and then decide which to read next based on your interest.

Gathering feedback

All feedback and especially criticism is welcome!

I'm aware of some major issues already but I think now is a sensible time to merge and to leave improvements to future work.

Future work and issue

Code quality

diff-tests/core/setup.go is an absolute monster
semi-duplicated efforts with simibc and the dependency ibc-go/testing
model init state is hardcoded in the typescript and the go code, instead of read into the go code
a few semi-duplicated helper methods between diff-tests/core/core_test.go and diff-tests/core/setup.go
lack of comments

Test capabilities

Testing what happens when assumptions are broken
Other, see this text

testutil/simibc/network_link.go

jtremback · 2022-09-01T00:30:16Z

diff-models/core/__tests__/gen.test.ts

@@ -0,0 +1,12 @@
+import { gen } from '../src/main.js';


Is the stuff in this folder necessary?

The easiest way I know of to check the statement coverage of the trace generation on the model is to use yarn jest --collect-coverage which requires a jest test.
I don't think we should give this up.

jtremback · 2022-09-01T00:50:41Z

diff-models/core/src/common.ts

+  invariantSnapshot: InvariantSnapshot;
+}
+
+interface Consequence {


I'd like to know more about what a Consequence is. Is it just the complete model state at any given time? Is it the parts of the model state that you care about checking, minus some "hidden" state?

Good point, this is poorly documented. A consequence is a slice of model state relevant to the action that was last done. It's used for state comparison with the SUT and is helpful for understanding traces when reading through the actions.
Previously I had much more state here, but it's too much and make the jsons huge and any problems really hard to debug.

jtremback · 2022-09-01T00:52:00Z

diff-models/core/jest.config.js

@@ -0,0 +1,24 @@
+export default {


Almost 100% certain this isn't needed. Can you remove all boilerplate files that you don't have a specific purpose for from this folder?

Good point to remove unnecessary files, but this one is very much needed. Jest will not run without this.

jtremback · 2022-09-01T02:16:24Z

diff-tests/core/core_test.go

+		s.Run(fmt.Sprintf("Trace num: %d", i), func() {
+			// Setup a new pair of chains for each trace
+			s.SetupTest()
+			s.traces.CurrentTraceIx = i


This feels really awkward. Can't you just iterate the list and pass the current trace to executeTrace?

It might be possible and I was just lazy. I'll check again. The thing is I want to keep the trace in 'global' state for diagnostics

diff-tests/core/core_test.go

jtremback · 2022-09-01T02:21:30Z

diff-tests/core/core_test.go

+			}()
+			// Record information about the trace, for debugging
+			// diagnostics.
+			s.executeTrace()


Where does the state after the action get checked (the "Consequence")? I see matchState being called in the endAndBeginBlock. Is that it? If it is, it seems odd to have your state being checked by one of your actions.

We only compare committed block state because that's the only thing that matters at the end of the day. Anything that happens inside the block is implementation detail. I.e. as long as the same transactions result in the same committed block state we don't care what the go implementation actually does with those transactions.

We could check after every action but IMO that would bring unnecessary restrictions and make it harder to make the model abstract and to make the implementation efficient

mpoke

Second part of the review (still need to look over properties.ts). In general, the code should be commented better.

diff-tests/core/model/src/model.ts

mpoke

Final part of the review for model.ts and properties.ts. See my comments below.

In general, amazing work @danwt 🚀

diff-tests/core/model/src/properties.ts

diff-tests/core/model/src/model.ts

mpoke · 2022-09-02T13:44:18Z

diff-tests/core/model/src/common.ts

+  h: Record<Chain, number>;
+  t: Record<Chain, number>;
+  tokens: number[];
+  undelegationQ: Undelegation[];
+  delegatorTokens: number;
+  power: (number | undefined)[];


Add comments describing the field. Ditto throughout the model.

Hmm, latest model.ts has all fields commented, did you see?

I'm not sure about also commenting these parts. Tbh there probably a much better way to write the typescript than I have done, I need to study the language a bit more.

diff-tests/core/model/src/properties.ts

diff-tests/core/model/src/common.ts

mpoke · 2022-09-02T14:06:05Z

diff-tests/core/model/src/properties.ts

+  function powerProvider(block: CommittedBlock) {
+    return _.range(NUM_VALIDATORS).map(
+      (i) =>
+        block.invariantSnapshot.tokens[i] +


These are all the tokens of validator i regardless of whether it is bonded, unbonding, or unbonded. For the property, only bonded and unbonding validators are relevant (plus the unbonding undelegations that are captured in the next lines).

Useful catch!

interchain-security/diff-tests/core/model/src/properties.ts

Lines 189 to 208 in 07fa9a8

/**

* @param block to compute validator voting powers for

* @param hp is the earliest height for unbondings to account for

* @returns burnable voting power for each validator on the Provider chain

*/

function powerProvider(block: CommittedBlock, hp: number): number[] {

return _.range(NUM_VALIDATORS).map((i) => {

let x = 0;

if (block.invariantSnapshot.status[i] !== Status.UNBONDED) {

x += block.invariantSnapshot.tokens[i];

}

x += sum(

block.invariantSnapshot.undelegationQ

.filter((e) => e.val === i)

.filter((e) => hp <= e.creationHeight)

.map((e) => e.initialBalance),

);

return x;

});

}

shaspitz · 2022-09-02T21:53:48Z

Could we also add the new files to tests/differential instead of diff-test to be compatible with #325

mpoke

Nice work @danwt.

commit 7e639da Author: Daniel T <30197399+danwt@users.noreply.github.com> Date: Tue Sep 6 11:46:08 2022 +0100 Difference testing for 'core' protocol using model generated (heuristic) 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 <44221603+smarshall-spitzbart@users.noreply.github.com> * 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 <danwtisdall@gmail.com> Co-authored-by: Jehan <jehan.tremback@gmail.com> Co-authored-by: Shawn Marshall-Spitzbart <44221603+smarshall-spitzbart@users.noreply.github.com>

* move to dir * other stuff * revert one change * Update Dockerfile * Squashed commit , with resolutions, of the following: commit 7e639da Author: Daniel T <30197399+danwt@users.noreply.github.com> Date: Tue Sep 6 11:46:08 2022 +0100 Difference testing for 'core' protocol using model generated (heuristic) 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 <44221603+smarshall-spitzbart@users.noreply.github.com> * 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 <danwtisdall@gmail.com> Co-authored-by: Jehan <jehan.tremback@gmail.com> Co-authored-by: Shawn Marshall-Spitzbart <44221603+smarshall-spitzbart@users.noreply.github.com> * DEL extra files Co-authored-by: Daniel <danwtisdall@gmail.com> Co-authored-by: Daniel T <30197399+danwt@users.noreply.github.com>

Daniel added 14 commits August 31, 2022 13:04

blanket add difftest

a0bd801

(assum + trace pass) upstream sync setup

421ec85

(full pass) shuffle directories

e5f3498

(all pass) minor tidyup simibc interface

645a6c2

(all pass) removes extraneous updateClients, deliverAcks

21af28d

(pass) del extra UpdateClient in framework deliverAcks

e33a4f7

(pass) tweak docstrings

213435a

(pass) remove chains map from framework

63f172f

(pass) rename, doc simibc

82b9ee6

(regression) tweaks

ce5e887

(pass) tweaks

9d789f6

(all pass) bump max gass

5656965

Track traces

1308ea1

Bumps ci configs

f87496d

danwt requested review from jtremback, mpoke and sainoe as code owners August 31, 2022 12:44

Try fix gosec

e86826c

danwt requested a review from MSalopek August 31, 2022 12:52

Daniel added 3 commits August 31, 2022 14:08

Try fix sonar

0fd8299

Try fix docker go build for 1.18

6901151

README

a518de4

jtremback reviewed Aug 31, 2022

View reviewed changes

testutil/simibc/network_link.go Outdated Show resolved Hide resolved

jtremback reviewed Sep 1, 2022

View reviewed changes

Merge branch 'main' into danwt/difftest-v3-reb0

35a90af

jtremback reviewed Sep 1, 2022

View reviewed changes

diff-tests/core/core_test.go Outdated Show resolved Hide resolved

jtremback reviewed Sep 1, 2022

View reviewed changes

mpoke reviewed Sep 2, 2022

View reviewed changes

Daniel added 9 commits September 2, 2022 12:20

Adds event.receive_slash_request_unbonded

4967512

Adds event.receive_slash_request_unbonded

d141b8a

Better docstring BlockHistory

189dae0

Adds 4 new events to constants

1c17aea

Model endblock method split

7d917d7

Couple more comments model.ts

1cd81ee

Comment model.ts

4f0c0b3

New traces

3e35ce5

DEL traces

9d4f639

mpoke requested changes Sep 2, 2022

View reviewed changes

Daniel added 8 commits September 2, 2022 17:42

CP (debug)

e562811

(debug) offset adjustment

d0bf519

tentative, fix regression (debug)

777463b

kill prints

2ddd85c

(tentative) property fix

4793687

Fixes BBCVP power provider

d1fe2aa

New traces

49bc590

Del 2x prints

07fa9a8

Daniel and others added 5 commits September 3, 2022 06:23

Comment property perf

0716787

rn power -> consumerPower in model

b409fb2

rn power -> consumerPower in driver

96f01ca

Merge branch 'main' into danwt/difftest-v3-reb0

abeff60

Removes outdated comment

5f0c65d

mpoke approved these changes Sep 6, 2022

View reviewed changes

danwt merged commit 7e639da into main Sep 6, 2022

danwt deleted the danwt/difftest-v3-reb0 branch September 6, 2022 10:46

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Difference testing for 'core' protocol using model generated (heuristic) traces #315

Difference testing for 'core' protocol using model generated (heuristic) traces #315

danwt commented Aug 31, 2022 •

edited

Loading

jtremback Sep 1, 2022

danwt Sep 1, 2022 •

edited

Loading

jtremback Sep 1, 2022

danwt Sep 1, 2022

jtremback Sep 1, 2022 •

edited

Loading

danwt Sep 1, 2022

jtremback Sep 1, 2022

danwt Sep 1, 2022

jtremback Sep 1, 2022

danwt Sep 1, 2022 •

edited

Loading

danwt Sep 1, 2022

mpoke left a comment

mpoke left a comment

mpoke Sep 2, 2022

danwt Sep 2, 2022

mpoke Sep 2, 2022

danwt Sep 2, 2022

shaspitz commented Sep 2, 2022

mpoke left a comment

	/**
	* @param block to compute validator voting powers for
	* @param hp is the earliest height for unbondings to account for
	* @returns burnable voting power for each validator on the Provider chain
	*/
	function powerProvider(block: CommittedBlock, hp: number): number[] {
	return _.range(NUM_VALIDATORS).map((i) => {
	let x = 0;
	if (block.invariantSnapshot.status[i] !== Status.UNBONDED) {
	x += block.invariantSnapshot.tokens[i];
	}
	x += sum(
	block.invariantSnapshot.undelegationQ
	.filter((e) => e.val === i)
	.filter((e) => hp <= e.creationHeight)
	.map((e) => e.initialBalance),
	);
	return x;
	});
	}

Difference testing for 'core' protocol using model generated (heuristic) traces #315

Difference testing for 'core' protocol using model generated (heuristic) traces #315

Conversation

danwt commented Aug 31, 2022 • edited Loading

Overview

Gathering feedback

Future work and issue

Code quality

Test capabilities

Choose a reason for hiding this comment

danwt Sep 1, 2022 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

jtremback Sep 1, 2022 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

danwt Sep 1, 2022 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

mpoke left a comment

Choose a reason for hiding this comment

mpoke left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

shaspitz commented Sep 2, 2022

mpoke left a comment

Choose a reason for hiding this comment

danwt commented Aug 31, 2022 •

edited

Loading

danwt Sep 1, 2022 •

edited

Loading

jtremback Sep 1, 2022 •

edited

Loading

danwt Sep 1, 2022 •

edited

Loading