From 2488377d84750c53046b22661f9557c3596a9d6c Mon Sep 17 00:00:00 2001
From: Philip Offtermatt
Date: Fri, 15 Dec 2023 11:29:55 +0100
Subject: [PATCH] Remove difftest folder
---
tests/difference/core/docs/METHOD.md | 128 ----
tests/difference/core/driver/setup.go | 625 ------------------
tests/difference/core/model/src/common.ts | 244 -------
tests/difference/core/model/src/properties.ts | 359 ----------
4 files changed, 1356 deletions(-)
delete mode 100644 tests/difference/core/docs/METHOD.md
delete mode 100644 tests/difference/core/driver/setup.go
delete mode 100644 tests/difference/core/model/src/common.ts
delete mode 100644 tests/difference/core/model/src/properties.ts
diff --git a/tests/difference/core/docs/METHOD.md b/tests/difference/core/docs/METHOD.md
deleted file mode 100644
index da14a42f9a..0000000000
--- a/tests/difference/core/docs/METHOD.md
+++ /dev/null
@@ -1,128 +0,0 @@
-# Method
-
-Contains information about the differential/difference testing method in general and how it impacts the project.
-
-## Motivation
-
-The goal is to find more, deeper, bugs in the long run life of the project in a more cost effective way than can be done by other testing methods (unit, full node, integration, model based testing).
-
-Each of the traditional methods has draw backs
-
-- unit\
-Finds shallow bugs.
-- full node\
-Expensive to setup and run, hard to debug, slow.
-- integration\
-Limited to isolated parts of system so cannot find logic bugs across systems.
-- model based\
-Exhaustive model checkers do not scale well to large systems. Esoteric languages hard to onboard and maintain.
-
-Diff testing should be
-
-- Able to find deep bugs (and shallow ones)\
-Complicated systems *may* have tricky, deep bugs which are caused by specific interleavings of API calls with specific params. We want a way to try to find these.
-- Maintainable\
-If the requirements change or a major piece of the system API changes it should be possible to modify existing test code to handle the new system, without having to scrap everything.
-- Scalable\
-Everything should run in memory, cheaply. It should be possible to use the debugger to step through failed tests.
-
-Diff testing does not
-
-- Try to find every bug\
-Diff testing is based on randomness and heuristics and these can only get you so far in finding bugs. More on this in [Limitations](#limitations).
-
-## Concepts
-
-Here we use terminology as it is already used in the project, we do **not** use academic parlance.
-
-We have a system under test (SUT) and we want to test that it satisfies all our design properties (e.g. Validator Set Replication). Diff testing works by making a simplified implementation of the business logic of our system, observing executions of the simplified implementation, and then checking that those observations 'match' what is happening in the real system.
-
-![diagram0](./diagrams/diagram0.png)
-
-We have three major components, a model and driver, and the SUT. The creation of each part could go something like
-
-1. Figure out what parts of the system state you need to observe to know that your system is working. E.g. token balances, voting powers.
-2. Figure out which API calls influence that state.
-3. Create the simplest possible implementation of those API calls that results in the correct state. This is the raw model.
-4. Randomly make API calls against your model. You might need some heuristics or bespoke logic to make sure these random calls result in good coverage (see [Limitations](#limitations)).
-5. Record the random API calls made ('actions') and observations of the state made at regular intervals. Together this data forms a trace. Repeated many times from the zero state you obtain *traces*.
-6. Create a 'driver': some code that wraps the API of the SUT and can interpret traces and 'test' those traces against the SUT. For each tested trace, setup the SUT to a suitable zero state, and make each API call as in the trace. For each state observation in the trace, check that the SUT state corresponds.
-
-## Benefits
-
-- You know that the system behavior matches the model behavior.
-- The model should be much simpler and easier to check properties for. It will have clear boundaries.
-- A well written model can be the specification.
-- You can instrument the model with arbitrary code to make sure that your random API calls get good coverage. This can go well beyond statement/branch coverage.
-- Based on my anecdotal experience, the ratio of confidence gained per line of code written and maintained can be much much higher for this kind of testing than for unit tests, integration tests, full node tests.
-- You can find deep bugs because the random exploration will find many cases that humans won't think of.
-
-## Limitations
-
-- You have to maintain a model and all the surrounding framework.
-- If you want to make a major change to your system you will have to change the model and the SUT.\
-NOTE: Change the model first, and THEN change the SUT. This is TDD.
-
-and...
-
-The biggest limitation is that random exploration can be severely limited. This warrants more explanation:
-
-### Random exploration
-
-It's easy to find example programs where random exploration will have very poor results. Consider
-
-```go
-func foo(x uint64) {
- if x = 123456 {
- // BUG
- } else {
- // NO BUG
- }
-}
-```
-
-By testing foo with uniformly randomly chosen x's 80 million times per second you will never find the bug. This is a contrived example, but it illustrates the point that you cannot rely on randomness.
-
-## Influences
-
-In creating diff testing I was influenced ideas from Model Based Testing (see [section](#comparison-to-model-based-testing)). Both methods share the notions of model, driver, and trace but the way the model is written and the traces are generated is different.
-
-## Other
-
-### Random exploration good or bad?
-
-While you shouldn't rely on random exploration for good coverage it proves to be practical and useful in many real life systems. You should definitely measure the coverage of your exploration. With measurements, you can freely experiment with adding heuristic rules to restrict the randomness in particular ways. You can also look at qualities of your particular system and try to make combinatorial or probabilistic arguments for coverage.
-
-### Usage of model as the spec
-
-The model could be the spec, if you want it to be. All the dependencies should be abstracted away behind contract satisfying interfaces, and any implementation detail related to performance or environment boilerplate can be omitted.
-
-### Creating many implementations from a single model
-
-The same model can be used to create drivers for, and test, many different implementations of the system in any language, environment etc
-
-## Comparison to Model Based Testing
-
-Informal Systems uses the term model based testing to refer to, essentially diff testing, with two major differences
-
-- The model is written in a formal specification language with semantics and properties that make it amenable to formal verification and automated reasoning techniques.\
-Example languages: [TLA+](https://en.wikipedia.org/wiki/TLA%2B), [Quint](https://github.com/informalsystems/quint). Example semantic: [Temporal Logic of Actions](https://en.wikipedia.org/wiki/Temporal_logic_of_actions). Example techniques: [SAT Solving](https://en.wikipedia.org/wiki/SAT_solver), [Symbolic Model Checking](https://blog.acolyer.org/2019/11/29/tla-model-checking-made-symbolic/), [State Enumerating Model Checking](https://en.wikipedia.org/wiki/State_space_enumeration). Example tools: [TLC](https://github.com/tlaplus/tlaplus), [Apalache](https://apalache.informal.systems/).
-- The model is explored not by randomness and heuristics but by using a [*model checker*](https://en.wikipedia.org/wiki/Model_checking). Model checkers pull on a massive field of research and they're about applying efficient techniques for exploring program behaviors. While modern model checkers are highly optimized and capable, they are not silver bullets, as they all suffer from the [State Space Explosion Problem](https://en.wikipedia.org/wiki/Combinatorial_explosion). See [this wiki page](https://en.wikipedia.org/wiki/Model_checking#Techniques) for more info.
-
-Why not use model checking? They require expert knowledge which is hard to onboard, the State Space Explosion Problem can be very real in practice, and the tooling e.g TLA+ is generally not industrial strength in terms of maintainability etc.
-
-Note that the Apalache team at Informal is working hard to make MBT a powerful practical tool. They have made leaps and bounds in the last year since diff testing began in April 2022. In particular they have created a new programming language called Quint which should be an industrial strength formal specification language. They have also added powerful exploration capabilities (see [::simulate](https://apalache.informal.systems/docs/apalache/running.html?highlight=simulate#running-the-tool)) which combines random exploration with optimized model checker based exploration.
-
- I recommend checking out [Apalache](https://github.com/informalsystems/apalache) and [Quint](https://github.com/informalsystems/quint) and consulting with Igor.
-
-## Comparison to Property Based Testing
-
-Property Based Testing is a loose term for testing properties of your system. Generally the idea is to make API calls using random heuristics and known tricks, and check that the result satisfies properties. Please see [this page](https://github.com/cosmos/interchain-security/blob/danwt/pbt-prototype/tests/pbt/tutorial.md) for a full tutorial on using a golang PBT library.
-
-~~Why not use property based testing?~~ I suggest using it. See next section.
-
-## Recommendation going forward
-
-In the long run I suggest scrapping the existing model and trace, and using property based testing instead. The existing driver can easily be adapted to take input from a property based testing library like [golang's Rapid](https://github.com/flyingmutant/rapid). The properties from `properties.ts` can easily be written in go and tested in go. A model will not be needed at all, only the action generation heuristics. I think PBT will be able to achieve the same or better results without having to maintain the model.
-
-In the long run I **also** suggest incorporating Informals tools [Apalache](https://github.com/informalsystems/apalache) and [Quint](https://github.com/informalsystems/quint). Please consult with Igor on this.
diff --git a/tests/difference/core/driver/setup.go b/tests/difference/core/driver/setup.go
deleted file mode 100644
index 7114a3b26a..0000000000
--- a/tests/difference/core/driver/setup.go
+++ /dev/null
@@ -1,625 +0,0 @@
-package core
-
-import (
- "bytes"
- cryptoEd25519 "crypto/ed25519"
- "encoding/json"
- "time"
-
- clienttypes "github.com/cosmos/ibc-go/v7/modules/core/02-client/types"
- channeltypes "github.com/cosmos/ibc-go/v7/modules/core/04-channel/types"
- commitmenttypes "github.com/cosmos/ibc-go/v7/modules/core/23-commitment/types"
- ibctmtypes "github.com/cosmos/ibc-go/v7/modules/light-clients/07-tendermint"
- ibctesting "github.com/cosmos/ibc-go/v7/testing"
- "github.com/cosmos/ibc-go/v7/testing/mock"
- "github.com/stretchr/testify/require"
- "github.com/stretchr/testify/suite"
-
- "github.com/cosmos/cosmos-sdk/baseapp"
- codectypes "github.com/cosmos/cosmos-sdk/codec/types"
- cryptocodec "github.com/cosmos/cosmos-sdk/crypto/codec"
- cosmosEd25519 "github.com/cosmos/cosmos-sdk/crypto/keys/ed25519"
- "github.com/cosmos/cosmos-sdk/crypto/keys/secp256k1"
- sdk "github.com/cosmos/cosmos-sdk/types"
- authtypes "github.com/cosmos/cosmos-sdk/x/auth/types"
- banktypes "github.com/cosmos/cosmos-sdk/x/bank/types"
- slashingkeeper "github.com/cosmos/cosmos-sdk/x/slashing/keeper"
- slashingtypes "github.com/cosmos/cosmos-sdk/x/slashing/types"
- stakingkeeper "github.com/cosmos/cosmos-sdk/x/staking/keeper"
- stakingtypes "github.com/cosmos/cosmos-sdk/x/staking/types"
-
- abci "github.com/cometbft/cometbft/abci/types"
- tmproto "github.com/cometbft/cometbft/proto/tendermint/types"
- tmtypes "github.com/cometbft/cometbft/types"
-
- appConsumer "github.com/cosmos/interchain-security/v3/app/consumer"
- appProvider "github.com/cosmos/interchain-security/v3/app/provider"
- icstestingutils "github.com/cosmos/interchain-security/v3/testutil/ibc_testing"
- testutil "github.com/cosmos/interchain-security/v3/testutil/integration"
- simibc "github.com/cosmos/interchain-security/v3/testutil/simibc"
- consumerkeeper "github.com/cosmos/interchain-security/v3/x/ccv/consumer/keeper"
- consumertypes "github.com/cosmos/interchain-security/v3/x/ccv/consumer/types"
- providerkeeper "github.com/cosmos/interchain-security/v3/x/ccv/provider/keeper"
- ccv "github.com/cosmos/interchain-security/v3/x/ccv/types"
-)
-
-type Builder struct {
- suite *suite.Suite
- path *ibctesting.Path
- coordinator *ibctesting.Coordinator
- valAddresses []sdk.ValAddress
- initState InitState
-}
-
-func (b *Builder) provider() *ibctesting.TestChain {
- return b.coordinator.GetChain(ibctesting.GetChainID(0))
-}
-
-func (b *Builder) consumer() *ibctesting.TestChain {
- return b.coordinator.GetChain(ibctesting.GetChainID(1))
-}
-
-func (b *Builder) providerCtx() sdk.Context {
- return b.provider().GetContext()
-}
-
-func (b *Builder) consumerCtx() sdk.Context {
- return b.consumer().GetContext()
-}
-
-func (b *Builder) providerStakingKeeper() stakingkeeper.Keeper {
- return *b.provider().App.(*appProvider.App).StakingKeeper
-}
-
-func (b *Builder) providerSlashingKeeper() slashingkeeper.Keeper {
- return b.provider().App.(*appProvider.App).SlashingKeeper
-}
-
-func (b *Builder) providerKeeper() providerkeeper.Keeper {
- return b.provider().App.(*appProvider.App).ProviderKeeper
-}
-
-func (b *Builder) consumerKeeper() consumerkeeper.Keeper {
- return b.consumer().App.(*appConsumer.App).ConsumerKeeper
-}
-
-func (b *Builder) providerEndpoint() *ibctesting.Endpoint {
- return b.path.EndpointB
-}
-
-func (b *Builder) consumerEndpoint() *ibctesting.Endpoint {
- return b.path.EndpointA
-}
-
-func (b *Builder) validator(i int64) sdk.ValAddress {
- return b.valAddresses[i]
-}
-
-func (b *Builder) consAddr(i int64) sdk.ConsAddress {
- return sdk.ConsAddress(b.validator(i))
-}
-
-// getValidatorPK returns the validator private key using the given seed index
-func (b *Builder) getValidatorPK(seedIx int) mock.PV {
- seed := []byte(b.initState.PKSeeds[seedIx])
- return mock.PV{PrivKey: &cosmosEd25519.PrivKey{Key: cryptoEd25519.NewKeyFromSeed(seed)}} //nolint:staticcheck // SA1019: cosmosEd25519.PrivKey is deprecated: PrivKey defines a ed25519 private key. NOTE: ed25519 keys must not be used in SDK apps except in a tendermint validator context.
-}
-
-func (b *Builder) getAppBytesAndSenders(
- chainID string,
- app ibctesting.TestingApp,
- genesis map[string]json.RawMessage,
- validators *tmtypes.ValidatorSet,
-) ([]byte, []ibctesting.SenderAccount) {
- accounts := []authtypes.GenesisAccount{}
- balances := []banktypes.Balance{}
- senderAccounts := []ibctesting.SenderAccount{}
-
- // Create genesis accounts.
- for i := 0; i < b.initState.MaxValidators; i++ {
- pk := secp256k1.GenPrivKey()
- acc := authtypes.NewBaseAccount(pk.PubKey().Address().Bytes(), pk.PubKey(), uint64(i), 0)
-
- // Give enough funds for many delegations
- // Extra units are to delegate to extra validators created later
- // in order to bond them and still have INITIAL_DELEGATOR_TOKENS remaining
- extra := 0
- for j := 0; j < b.initState.NumValidators; j++ {
- if b.initState.ValStates.Status[j] != stakingtypes.Bonded {
- extra += b.initState.ValStates.Delegation[j]
- }
- }
- amt := uint64(b.initState.InitialDelegatorTokens + extra)
-
- bal := banktypes.Balance{
- Address: acc.GetAddress().String(),
- Coins: sdk.NewCoins(sdk.NewCoin(sdk.DefaultBondDenom, sdk.NewIntFromUint64(amt))),
- }
-
- accounts = append(accounts, acc)
- balances = append(balances, bal)
-
- senderAccount := ibctesting.SenderAccount{
- SenderAccount: acc,
- SenderPrivKey: pk,
- }
-
- senderAccounts = append(senderAccounts, senderAccount)
- }
-
- // set genesis accounts
- genesisAuth := authtypes.NewGenesisState(authtypes.DefaultParams(), accounts)
- genesis[authtypes.ModuleName] = app.AppCodec().MustMarshalJSON(genesisAuth)
-
- stakingValidators := make([]stakingtypes.Validator, 0, len(validators.Validators))
- delegations := make([]stakingtypes.Delegation, 0, len(validators.Validators))
-
- // Sum bonded is needed for BondedPool account
- sumBonded := sdk.NewInt(0)
- initValPowers := []abci.ValidatorUpdate{}
-
- for i, val := range validators.Validators {
- status := b.initState.ValStates.Status[i]
- delegation := b.initState.ValStates.Delegation[i]
- extra := b.initState.ValStates.ValidatorExtraTokens[i]
-
- tokens := sdk.NewInt(int64(delegation + extra))
- b.suite.Require().Equal(status, stakingtypes.Bonded, "All genesis validators should be bonded")
- sumBonded = sumBonded.Add(tokens)
- // delegator account receives delShares shares
- delShares := sdk.NewDec(int64(delegation))
- // validator has additional sumShares due to extra units
- sumShares := sdk.NewDec(int64(delegation + extra))
-
- pk, err := cryptocodec.FromTmPubKeyInterface(val.PubKey)
- require.NoError(b.suite.T(), err)
- pkAny, err := codectypes.NewAnyWithValue(pk)
- require.NoError(b.suite.T(), err)
-
- validator := stakingtypes.Validator{
- OperatorAddress: sdk.ValAddress(val.Address).String(),
- ConsensusPubkey: pkAny,
- Jailed: false,
- Status: status,
- Tokens: tokens,
- DelegatorShares: sumShares,
- Description: stakingtypes.Description{},
- UnbondingHeight: int64(0),
- UnbondingTime: time.Unix(0, 0).UTC(),
- Commission: stakingtypes.NewCommission(sdk.ZeroDec(), sdk.ZeroDec(), sdk.ZeroDec()),
- MinSelfDelegation: sdk.ZeroInt(),
- }
-
- stakingValidators = append(stakingValidators, validator)
-
- // Store delegation from the model delegator account
- delegations = append(delegations, stakingtypes.NewDelegation(accounts[0].GetAddress(), val.Address.Bytes(), delShares))
- // Remaining delegation is from extra account
- delegations = append(delegations, stakingtypes.NewDelegation(accounts[1].GetAddress(), val.Address.Bytes(), sumShares.Sub(delShares)))
-
- // add initial validator powers so consumer InitGenesis runs correctly
- pub, _ := val.ToProto()
- initValPowers = append(initValPowers, abci.ValidatorUpdate{
- Power: val.VotingPower,
- PubKey: pub.PubKey,
- })
- }
-
- bondDenom := sdk.DefaultBondDenom
- genesisStaking := stakingtypes.GenesisState{}
- genesisConsumer := consumertypes.GenesisState{}
-
- if genesis[stakingtypes.ModuleName] != nil {
- // If staking module genesis already exists
- app.AppCodec().MustUnmarshalJSON(genesis[stakingtypes.ModuleName], &genesisStaking)
- bondDenom = genesisStaking.Params.BondDenom
- }
-
- if genesis[consumertypes.ModuleName] != nil {
- app.AppCodec().MustUnmarshalJSON(genesis[consumertypes.ModuleName], &genesisConsumer)
- genesisConsumer.Provider.InitialValSet = initValPowers
- genesisConsumer.Params.Enabled = true
- genesis[consumertypes.ModuleName] = app.AppCodec().MustMarshalJSON(&genesisConsumer)
- }
-
- // Set model parameters
- genesisStaking.Params.MaxEntries = uint32(b.initState.MaxEntries)
- genesisStaking.Params.MaxValidators = uint32(b.initState.MaxValidators)
- genesisStaking.Params.UnbondingTime = b.initState.UnbondingP
- genesisStaking = *stakingtypes.NewGenesisState(genesisStaking.Params, stakingValidators, delegations)
- genesis[stakingtypes.ModuleName] = app.AppCodec().MustMarshalJSON(&genesisStaking)
-
- // add bonded amount to bonded pool module account
- balances = append(balances, banktypes.Balance{
- Address: authtypes.NewModuleAddress(stakingtypes.BondedPoolName).String(),
- Coins: sdk.Coins{sdk.NewCoin(bondDenom, sumBonded)},
- })
-
- // add unbonded amount
- balances = append(balances, banktypes.Balance{
- Address: authtypes.NewModuleAddress(stakingtypes.NotBondedPoolName).String(),
- Coins: sdk.Coins{sdk.NewCoin(bondDenom, sdk.ZeroInt())},
- })
-
- // update total funds supply
- genesisBank := banktypes.NewGenesisState(banktypes.DefaultGenesisState().Params, balances, sdk.NewCoins(), []banktypes.Metadata{}, []banktypes.SendEnabled{})
- genesis[banktypes.ModuleName] = app.AppCodec().MustMarshalJSON(genesisBank)
-
- stateBytes, err := json.MarshalIndent(genesis, "", " ")
- require.NoError(b.suite.T(), err)
-
- return stateBytes, senderAccounts
-}
-
-func (b *Builder) newChain(
- coord *ibctesting.Coordinator,
- appInit icstestingutils.AppIniter,
- chainID string,
- validators *tmtypes.ValidatorSet,
- signers map[string]tmtypes.PrivValidator,
-) *ibctesting.TestChain {
- app, genesis := appInit()
-
- baseapp.SetChainID(chainID)(app.GetBaseApp())
-
- stateBytes, senderAccounts := b.getAppBytesAndSenders(chainID, app, genesis, validators)
-
- app.InitChain(
- abci.RequestInitChain{
- ChainId: chainID,
- Validators: []abci.ValidatorUpdate{},
- ConsensusParams: b.initState.ConsensusParams,
- AppStateBytes: stateBytes,
- },
- )
-
- app.Commit()
-
- app.BeginBlock(
- abci.RequestBeginBlock{
- Header: tmproto.Header{
- ChainID: chainID,
- Height: app.LastBlockHeight() + 1,
- AppHash: app.LastCommitID().Hash,
- ValidatorsHash: validators.Hash(),
- NextValidatorsHash: validators.Hash(),
- },
- },
- )
-
- chain := &ibctesting.TestChain{
- T: b.suite.T(),
- Coordinator: coord,
- ChainID: chainID,
- App: app,
- CurrentHeader: tmproto.Header{
- ChainID: chainID,
- Height: 1,
- Time: coord.CurrentTime.UTC(),
- },
- QueryServer: app.GetIBCKeeper(),
- TxConfig: app.GetTxConfig(),
- Codec: app.AppCodec(),
- Vals: validators,
- NextVals: validators,
- Signers: signers,
- SenderPrivKey: senderAccounts[0].SenderPrivKey,
- SenderAccount: senderAccounts[0].SenderAccount,
- SenderAccounts: senderAccounts,
- }
-
- coord.CommitBlock(chain)
-
- return chain
-}
-
-func (b *Builder) createValidators() (*tmtypes.ValidatorSet, map[string]tmtypes.PrivValidator, []sdk.ValAddress) {
- addresses := []sdk.ValAddress{}
- signers := map[string]tmtypes.PrivValidator{}
- validators := []*tmtypes.Validator{}
-
- for i, power := range b.initState.ValStates.Tokens {
- if b.initState.ValStates.Status[i] != stakingtypes.Bonded {
- continue
- }
- privVal := b.getValidatorPK(i)
-
- pubKey, err := privVal.GetPubKey()
- require.NoError(b.suite.T(), err)
-
- // Compute address
- addr, err := sdk.ValAddressFromHex(pubKey.Address().String())
- require.NoError(b.suite.T(), err)
- addresses = append(addresses, addr)
-
- // Save signer
- signers[pubKey.Address().String()] = privVal
-
- // Save validator with power
- validators = append(validators, tmtypes.NewValidator(pubKey, int64(power)))
- }
-
- return tmtypes.NewValidatorSet(validators), signers, addresses
-}
-
-func (b *Builder) createProviderAndConsumer() {
- coordinator := ibctesting.NewCoordinator(b.suite.T(), 0)
-
- // Create validators
- validators, signers, addresses := b.createValidators()
- // Create provider
- coordinator.Chains[ibctesting.GetChainID(0)] = b.newChain(coordinator, icstestingutils.ProviderAppIniter, ibctesting.GetChainID(0), validators, signers)
- // Create consumer, using the same validators.
- valUpdates := testutil.ToValidatorUpdates(b.suite.T(), validators)
- coordinator.Chains[ibctesting.GetChainID(1)] = b.newChain(coordinator, icstestingutils.ConsumerAppIniter(valUpdates), ibctesting.GetChainID(1), validators, signers)
-
- b.coordinator = coordinator
- b.valAddresses = addresses
-}
-
-// setSigningInfos sets the validator signing info in the provider Slashing module
-func (b *Builder) setSigningInfos() {
- for i := 0; i < b.initState.NumValidators; i++ {
- info := slashingtypes.NewValidatorSigningInfo(
- b.consAddr(int64(i)),
- b.provider().CurrentHeader.GetHeight(),
- 0,
- time.Unix(0, 0),
- false,
- 0,
- )
- b.providerSlashingKeeper().SetValidatorSigningInfo(b.providerCtx(), b.consAddr(int64(i)), info)
- }
-}
-
-// Checks that the lexicographic ordering of validator addresses as computed in
-// the staking module match the ordering of validators in the model.
-func (b *Builder) ensureValidatorLexicographicOrderingMatchesModel() {
- check := func(lesser, greater sdk.ValAddress) {
- lesserV, _ := b.providerStakingKeeper().GetValidator(b.providerCtx(), lesser)
- greaterV, _ := b.providerStakingKeeper().GetValidator(b.providerCtx(), greater)
- lesserKey := stakingtypes.GetValidatorsByPowerIndexKey(lesserV, sdk.DefaultPowerReduction)
- greaterKey := stakingtypes.GetValidatorsByPowerIndexKey(greaterV, sdk.DefaultPowerReduction)
- // The result will be 0 if a==b, -1 if a < b, and +1 if a > b.
- res := bytes.Compare(lesserKey, greaterKey)
- // Confirm that validator precedence is the same in code as in model
- b.suite.Require().Equal(-1, res)
- }
-
- // In order to match the model to the system under test it is necessary
- // to enforce a strict lexicographic ordering on the validators.
- // We must do this because the staking module will break ties when
- // deciding the active validator set by comparing addresses lexicographically.
- // Thus, we assert here that the ordering in the model matches the ordering
- // in the SUT.
- for i := range b.valAddresses[:len(b.valAddresses)-1] {
- // validators are chosen sorted descending in the staking module
- greater := b.valAddresses[i]
- lesser := b.valAddresses[i+1]
- check(lesser, greater)
- }
-}
-
-// delegate is used to delegate tokens to newly created
-// validators in the setup process.
-func (b *Builder) delegate(del int, val sdk.ValAddress, amt int64) {
- d := b.provider().SenderAccounts[del].SenderAccount.GetAddress()
- coins := sdk.NewCoin(sdk.DefaultBondDenom, sdk.NewInt(amt))
- msg := stakingtypes.NewMsgDelegate(d, val, coins)
- providerStaking := b.providerStakingKeeper()
- pskServer := stakingkeeper.NewMsgServerImpl(&providerStaking)
- _, err := pskServer.Delegate(sdk.WrapSDKContext(b.providerCtx()), msg)
- b.suite.Require().NoError(err)
-}
-
-// addValidatorToStakingModule creates an additional validator with zero commission
-// and zero tokens (zero voting power).
-func (b *Builder) addValidatorToStakingModule(privVal mock.PV) {
- coin := sdk.NewCoin(sdk.DefaultBondDenom, sdk.NewInt(0))
-
- pubKey, err := privVal.GetPubKey()
- require.NoError(b.suite.T(), err)
-
- // Compute address
- addr, err := sdk.ValAddressFromHex(pubKey.Address().String())
- require.NoError(b.suite.T(), err)
-
- sdkPK, err := cryptocodec.FromTmPubKeyInterface(pubKey)
- require.NoError(b.suite.T(), err)
-
- msg, err := stakingtypes.NewMsgCreateValidator(
- addr,
- sdkPK,
- coin,
- stakingtypes.Description{},
- stakingtypes.NewCommissionRates(sdk.ZeroDec(), sdk.ZeroDec(), sdk.ZeroDec()),
- sdk.ZeroInt())
- b.suite.Require().NoError(err)
- providerStaking := b.providerStakingKeeper()
- pskServer := stakingkeeper.NewMsgServerImpl(&providerStaking)
- _, _ = pskServer.CreateValidator(sdk.WrapSDKContext(b.providerCtx()), msg)
-}
-
-func (b *Builder) addExtraProviderValidators() {
- for i, status := range b.initState.ValStates.Status {
- if status == stakingtypes.Unbonded {
- privVal := b.getValidatorPK(i)
- b.addValidatorToStakingModule(privVal)
- pubKey, err := privVal.GetPubKey()
- require.NoError(b.suite.T(), err)
-
- addr, err := sdk.ValAddressFromHex(pubKey.Address().String())
- require.NoError(b.suite.T(), err)
-
- b.valAddresses = append(b.valAddresses, addr)
- b.provider().Signers[pubKey.Address().String()] = privVal
- b.consumer().Signers[pubKey.Address().String()] = privVal
- }
- }
-
- b.setSigningInfos()
-
- b.ensureValidatorLexicographicOrderingMatchesModel()
-
- for i := range b.initState.ValStates.Status {
- if b.initState.ValStates.Status[i] == stakingtypes.Unbonded {
- del := b.initState.ValStates.Delegation[i]
- extra := b.initState.ValStates.ValidatorExtraTokens[i]
- b.delegate(0, b.validator(int64(i)), int64(del))
- b.delegate(1, b.validator(int64(i)), int64(extra))
- }
- }
-}
-
-func (b *Builder) setProviderParams() {
- // Set the slash factors on the provider to match the model
- slash := b.providerSlashingKeeper().GetParams(b.providerCtx())
- slash.SlashFractionDoubleSign = b.initState.SlashDoublesign
- slash.SlashFractionDowntime = b.initState.SlashDowntime
- err := b.providerSlashingKeeper().SetParams(b.providerCtx(), slash)
- if err != nil {
- panic(err)
- }
- // Set the throttle factors
- throttle := b.providerKeeper().GetParams(b.providerCtx())
- throttle.SlashMeterReplenishFraction = "1.0"
- throttle.SlashMeterReplenishPeriod = time.Second * 1
- b.providerKeeper().SetParams(b.providerCtx(), throttle)
-}
-
-func (b *Builder) configurePath() {
- b.path = ibctesting.NewPath(b.consumer(), b.provider())
- b.consumerEndpoint().ChannelConfig.PortID = ccv.ConsumerPortID
- b.providerEndpoint().ChannelConfig.PortID = ccv.ProviderPortID
- b.consumerEndpoint().ChannelConfig.Version = ccv.Version
- b.providerEndpoint().ChannelConfig.Version = ccv.Version
- b.consumerEndpoint().ChannelConfig.Order = channeltypes.ORDERED
- b.providerEndpoint().ChannelConfig.Order = channeltypes.ORDERED
-}
-
-func (b *Builder) createProvidersLocalClient() {
- // Configure and create the consumer Client
- tmCfg := b.providerEndpoint().ClientConfig.(*ibctesting.TendermintConfig)
- tmCfg.UnbondingPeriod = b.initState.UnbondingC
- tmCfg.TrustingPeriod = b.initState.Trusting
- tmCfg.MaxClockDrift = b.initState.MaxClockDrift
- err := b.providerEndpoint().CreateClient()
- b.suite.Require().NoError(err)
- // Create the Consumer chain ID mapping in the provider state
- b.providerKeeper().SetConsumerClientId(b.providerCtx(), b.consumer().ChainID, b.providerEndpoint().ClientID)
-}
-
-func (b *Builder) createConsumersLocalClientGenesis() *ibctmtypes.ClientState {
- tmCfg := b.consumerEndpoint().ClientConfig.(*ibctesting.TendermintConfig)
- tmCfg.UnbondingPeriod = b.initState.UnbondingP
- tmCfg.TrustingPeriod = b.initState.Trusting
- tmCfg.MaxClockDrift = b.initState.MaxClockDrift
-
- return ibctmtypes.NewClientState(
- b.provider().ChainID, tmCfg.TrustLevel, tmCfg.TrustingPeriod, tmCfg.UnbondingPeriod, tmCfg.MaxClockDrift,
- b.provider().LastHeader.GetHeight().(clienttypes.Height), commitmenttypes.GetSDKSpecs(),
- []string{"upgrade", "upgradedIBCState"},
- )
-}
-
-func (b *Builder) createConsumerGenesis(client *ibctmtypes.ClientState) *consumertypes.GenesisState {
- providerConsState := b.provider().LastHeader.ConsensusState()
-
- valUpdates := tmtypes.TM2PB.ValidatorUpdates(b.provider().Vals)
- params := ccv.NewParams(
- true,
- 1000, // ignore distribution
- "", // ignore distribution
- "", // ignore distribution
- ccv.DefaultCCVTimeoutPeriod,
- ccv.DefaultTransferTimeoutPeriod,
- ccv.DefaultConsumerRedistributeFrac,
- ccv.DefaultHistoricalEntries,
- b.initState.UnbondingC,
- "0", // disable soft opt-out
- []string{},
- []string{},
- ccv.DefaultRetryDelayPeriod,
- )
- return consumertypes.NewInitialGenesisState(client, providerConsState, valUpdates, params)
-}
-
-// The state of the data returned is equivalent to the state of two chains
-// after a full handshake, but the precise order of steps used to reach the
-// state does not necessarily mimic the order of steps that happen in a
-// live scenario.
-func GetZeroState(
- suite *suite.Suite,
- initState InitState,
-) (path *ibctesting.Path, addrs []sdk.ValAddress, heightLastCommitted, timeLastCommitted int64) {
- b := Builder{initState: initState, suite: suite}
-
- b.createProviderAndConsumer()
-
- b.setProviderParams()
-
- // This is the simplest way to initialize the slash meter
- // after a change to the param value.
- b.providerKeeper().InitializeSlashMeter(b.providerCtx())
-
- b.addExtraProviderValidators()
-
- // Commit the additional validators
- b.coordinator.CommitBlock(b.provider())
-
- b.configurePath()
-
- // Create a client for the provider chain to use, using ibc go testing.
- b.createProvidersLocalClient()
-
- // Manually create a client for the consumer chain to and bootstrap
- // via genesis.
- clientState := b.createConsumersLocalClientGenesis()
-
- consumerGenesis := b.createConsumerGenesis(clientState)
-
- b.consumerKeeper().InitGenesis(b.consumerCtx(), consumerGenesis)
-
- // Client ID is set in InitGenesis and we treat it as a block box. So
- // must query it to use it with the endpoint.
- clientID, _ := b.consumerKeeper().GetProviderClientID(b.consumerCtx())
- b.consumerEndpoint().ClientID = clientID
-
- // Handshake
- b.coordinator.CreateConnections(b.path)
- b.coordinator.CreateChannels(b.path)
-
- // Usually the consumer sets the channel ID when it receives a first VSC packet
- // to the provider. For testing purposes, we can set it here. This is because
- // we model a blank slate: a provider and consumer that have fully established
- // their channel, and are ready for anything to happen.
- b.consumerKeeper().SetProviderChannel(b.consumerCtx(), b.consumerEndpoint().ChannelID)
-
- // Catch up consumer height to provider height. The provider was one ahead
- // from committing additional validators.
- simibc.EndBlock(b.consumer(), func() {})
-
- simibc.BeginBlock(b.consumer(), initState.BlockInterval)
- simibc.BeginBlock(b.provider(), initState.BlockInterval)
-
- // Commit a block on both chains, giving us two committed headers from
- // the same time and height. This is the starting point for all our
- // data driven testing.
- lastProviderHeader, _ := simibc.EndBlock(b.provider(), func() {})
- lastConsumerHeader, _ := simibc.EndBlock(b.consumer(), func() {})
-
- // Want the height and time of last COMMITTED block
- heightLastCommitted = b.provider().CurrentHeader.Height
- timeLastCommitted = b.provider().CurrentHeader.Time.Unix()
-
- // Get ready to update clients.
- simibc.BeginBlock(b.provider(), initState.BlockInterval)
- simibc.BeginBlock(b.consumer(), initState.BlockInterval)
-
- // Update clients to the latest header. Now everything is ready to go!
- // Ignore errors for brevity. Everything is checked in Assumptions test.
- _ = simibc.UpdateReceiverClient(b.consumerEndpoint(), b.providerEndpoint(), lastConsumerHeader)
- _ = simibc.UpdateReceiverClient(b.providerEndpoint(), b.consumerEndpoint(), lastProviderHeader)
-
- return b.path, b.valAddresses, heightLastCommitted, timeLastCommitted
-}
diff --git a/tests/difference/core/model/src/common.ts b/tests/difference/core/model/src/common.ts
deleted file mode 100644
index 1ff002e6fc..0000000000
--- a/tests/difference/core/model/src/common.ts
+++ /dev/null
@@ -1,244 +0,0 @@
-type Chain = 'provider' | 'consumer';
-
-type Validator = number;
-
-enum Status {
- BONDED = 'bonded',
- UNBONDING = 'unbonding',
- UNBONDED = 'unbonded',
-}
-
-/**
- * All the data needed to represent an undelegation occurring
- * in the sdk staking module.
- */
-interface Undelegation {
- val: Validator;
- creationHeight: number;
- completionTime: number;
- balance: number;
- initialBalance: number;
- onHold: boolean;
- opID: number;
- willBeProcessedByStakingModule: boolean;
-}
-
-/**
- * All the data needed to represent an unbonding validator
- * occurring in the sdk staking module.
- */
-interface Unval {
- val: Validator;
- unbondingHeight: number;
- unbondingTime: number;
- onHold: boolean;
- opID: number;
-}
-
-/**
- * A representation of the validator set change data structure
- * sent from the provider to the consumer.
- */
-interface Vsc {
- vscID: number;
- updates: Record;
- downtimeSlashAcks: number[];
-}
-
-/**
- * Validator Set Change Maturity notification data structure
- */
-interface VscMaturity {
- vscID: number;
-}
-
-/**
- * A representation of the packet sent by the consumer to the
- * provider when slashing.
- */
-interface ConsumerInitiatedSlashPacketData {
- val: Validator;
- vscID: number;
- isDowntime: boolean;
-}
-
-type PacketData = Vsc | VscMaturity | ConsumerInitiatedSlashPacketData;
-
-interface Packet {
- data: PacketData;
- // Necessary to deduce a partial order between the provider
- // and consumer chain, as dictated by packet sending and
- // receiving.
- sendHeight: number;
-}
-
-interface Action {
- // A tag to identify the action type
- kind: string;
-}
-
-type Delegate = {
- kind: string;
- val: Validator; // Validator to delegate to
- amt: number; // Amount to delegate
-};
-
-type Undelegate = {
- kind: string;
- val: Validator; // Validator to undelegate from
- amt: number; // Max amount to undelegate
-};
-
-type ConsumerSlash = {
- kind: string;
- val: Validator; // Validator to slash
- infractionHeight: number; // Height of the infraction on consumer
- isDowntime: boolean; // Whether the slash is for downtime (or double sign)
-};
-
-type UpdateClient = {
- kind: string;
- // The chain who will receive the light client header TX
- // (details not modelled explicitly)
- chain: Chain;
-};
-
-type Deliver = {
- kind: string;
- // The chain who will receive packets which have been sent to it
- chain: Chain;
- // The MAX number of packets to deliver, from those available
- numPackets: number;
-};
-
-type EndAndBeginBlock = {
- kind: string;
- // Which chain will end and begin a block?
- chain: Chain;
-};
-
-/**
- * A snapshot of a portion of the model state at the time
- * that a block is committed on one of the chains.
- *
- * The state is exactly the state that is needed to check
- * system properties.
- */
-type PropertiesSystemState = {
- h: Record;
- t: Record;
- tokens: number[];
- status: Status[];
- undelegationQ: Undelegation[];
- delegatorTokens: number;
- consumerPower: (number | null)[];
- vscIDtoH: Record;
- hToVscID: Record;
-};
-
-/**
- * Record a snapshot of both chain states at the height and timestamp
- * of a committed block for a chain.
- */
-interface CommittedBlock {
- chain: Chain;
- propertiesSystemState: PropertiesSystemState;
-}
-
-/**
- * A partial snapshot of model state. It is the state
- * needed to check that the SUT is behaving correctly
- * when compared to the model.
- *
- * NOTE: This is not a complete snapshot of the model state
- * because not all of the data is needed, and the space
- * needed adds up quickly. Also, a concise representation
- * makes traces much more readable and easier to debug
- * by inspection.
- *
- * Fields are optional because not of the state is interesting
- * for all of the possible actions. This could be achieved
- * with a union type.
- */
-interface PartialState {
- h?: number; // Chain local height
- t?: number; // Chain local timestamp
- tokens?: number[];
- delegation?: number[];
- delegatorTokens?: number;
- jailed?: (number | null)[];
- status?: Status[];
- consumerPower?: (number | null)[];
- outstandingDowntime?: boolean[];
-}
-
-interface TraceAction {
- ix: number;
- action: Action;
- partialState: PartialState;
-}
-
-/**
- * The initial state of a new model instances.
- *
- * See model.ts for details of each field.
- */
-type ModelInitState = {
- h: Record;
- t: Record;
- staking: {
- delegation: number[];
- tokens: number[];
- status: Status[];
- undelegationQ: Undelegation[];
- validatorQ: Unval[];
- jailed: (number | null)[];
- delegatorTokens: number;
- opID: number;
- changes: Record;
- lastVals: Validator[];
- lastTokens: number[];
- };
- ccvC: {
- hToVscID: Record;
- pendingChanges: Record[];
- maturingVscs: Map;
- outstandingDowntime: boolean[];
- consumerPower: (number | null)[];
- };
- ccvP: {
- initialHeight: number;
- vscID: number;
- vscIDtoH: Record;
- vscIDtoOpIDs: Map;
- downtimeSlashAcks: number[];
- tombstoned: boolean[];
- matureUnbondingOps: number[];
- queue: (ConsumerInitiatedSlashPacketData | VscMaturity)[];
- };
-};
-
-export {
- ModelInitState,
- PartialState,
- TraceAction,
- CommittedBlock,
- Chain,
- Validator,
- Action,
- Delegate,
- Undelegate,
- ConsumerSlash,
- UpdateClient,
- Deliver,
- EndAndBeginBlock,
- PropertiesSystemState,
- Status,
- Undelegation,
- Unval,
- Vsc,
- VscMaturity,
- ConsumerInitiatedSlashPacketData,
- PacketData,
- Packet,
-};
diff --git a/tests/difference/core/model/src/properties.ts b/tests/difference/core/model/src/properties.ts
deleted file mode 100644
index c7c035d689..0000000000
--- a/tests/difference/core/model/src/properties.ts
+++ /dev/null
@@ -1,359 +0,0 @@
-import { strict as assert } from 'node:assert';
-import _ from 'underscore';
-import {
- P,
- C,
- UNBONDING_SECONDS_C,
- NUM_VALIDATORS,
-} from './constants.js';
-import {
- PropertiesSystemState,
- Chain,
- CommittedBlock,
- Status,
-} from './common.js';
-
-/**
- * Queries and data structures in this file are currently naive
- * and below optimal.
- * Partial order queries and other total order queries in
- * bond-based-consumer-voting-power can be done with binary searches.
- */
-
-/**
- * Data structure used to store a partial order of blocks. The partial order
- * is induced by packet delivery for blocks on different chains, and by height
- * for blocks on the same chain.
- * See https://github.com/cosmos/ibc/blob/main/spec/app/ics-028-cross-chain-validation/system_model_and_properties.md#system-properties
- */
-class PartialOrder {
- // map chain -> block height in chain -> block height in counterparty chain
- greatestPred: Record> = {
- provider: new Map(),
- consumer: new Map(),
- };
- // map chain -> block height in chain -> block height in counterparty chain
- leastSucc: Record> = {
- provider: new Map(),
- consumer: new Map(),
- };
-
- /**
- * Mark the delivery of a packet. Induces a partial order between blocks
- * on different chains.
- * @param receiverChain chain receiving packet
- * @param sendHeight send height on sending chain
- * @param receiveHeight receive height on receiving chain
- */
- deliver = (
- receiverChain: Chain,
- sendHeight: number,
- receiveHeight: number,
- ) => {
- let h = sendHeight;
- if (this.greatestPred[receiverChain].has(receiveHeight)) {
- h = Math.max(
- this.greatestPred[receiverChain].get(receiveHeight) as number,
- h,
- );
- }
- this.greatestPred[receiverChain].set(receiveHeight, h);
- const senderChain = receiverChain === P ? C : P;
- h = receiveHeight;
- if (this.leastSucc[senderChain].has(sendHeight)) {
- h = Math.min(
- this.leastSucc[senderChain].get(sendHeight) as number,
- h,
- );
- }
- this.leastSucc[senderChain].set(sendHeight, h);
- };
-
- /**
- * @param chain chain of block
- * @param height height of block
- * @returns Returns the height greatest predecessor block on the counterparty
- * chain if it exists, else undefined.
- */
- getGreatestPred = (
- chain: Chain,
- height: number,
- ): number | undefined => {
- const it = this.greatestPred[chain].keys();
- let bestH = -1;
- let bestV = -1;
- let result = it.next();
- while (!result.done) {
- const h = result.value;
- if (bestH < h && h <= height) {
- bestH = h;
- bestV = this.greatestPred[chain].get(h) as number;
- }
- result = it.next();
- }
- if (bestV === -1) {
- // No greatest predecessor exists.
- return;
- }
- return bestV;
- };
-
- /**
- *
- * @param chain chain of block
- * @param height height of block
- * @returns Returns the height of the least successor block on the counterparty
- * chain if it exists, else undefined.
- */
- getLeastSucc = (chain: Chain, height: number): number | undefined => {
- const it = this.leastSucc[chain].keys();
- let bestH = 100000000000000; // Infinity
- let bestAnswer = -1;
- let result = it.next();
- while (!result.done) {
- const h = result.value;
- if (h < bestH && height <= h) {
- bestH = h;
- bestAnswer = this.leastSucc[chain].get(h) as number;
- }
- result = it.next();
- }
- if (bestAnswer === -1) {
- // No least successor exists.
- return;
- }
- return bestAnswer;
- };
-}
-
-class BlockHistory {
- partialOrder = new PartialOrder();
- blocks: Record> = {
- provider: new Map(),
- consumer: new Map(),
- };
- /**
- * Mark state as permanently committed to the blockchain.
- * @param chain
- * @param propertiesSystemState
- */
- commitBlock = (chain: Chain, propertiesSystemState: PropertiesSystemState) => {
- const h = propertiesSystemState.h[chain];
- const b: CommittedBlock = {
- chain,
- propertiesSystemState: propertiesSystemState,
- };
- this.blocks[chain].set(h, b);
- };
-}
-
-function sum(arr: number[]): number {
- return arr.reduce((sum: number, x: number) => sum + x, 0);
-}
-
-/**
- * Is the total fund value in the system constant?
- * It only makes sense to check this if slashing with non-zero
- * slash factors never occurs, because slashing with non-zero
- * slash factors burns funds.
- *
- * @param hist A history of blocks.
- * @returns Is the property satisfied?
- */
-function stakingWithoutSlashing(hist: BlockHistory): boolean {
- const blocks = Array.from(hist.blocks[P].entries())
- .sort((a, b) => a[0] - b[0])
- .map((e) => e[1])
- .map((b) => b.propertiesSystemState);
-
- function value(e: PropertiesSystemState) {
- let x = e.delegatorTokens;
- x += sum(e.tokens);
- x += sum(e.undelegationQ.map((e) => e.balance));
- return x;
- }
-
- const v = value(blocks[0]);
- for (let i = 1; i < blocks.length; i++) {
- if (value(blocks[i]) !== v) {
- return false;
- }
- }
- return true;
-}
-
-/**
- * Checks the validator set replication property as defined
- * https://github.com/cosmos/ibc/blob/main/spec/app/ics-028-cross-chain-validation/system_model_and_properties.md#system-properties
- *
- * @param hist A history of blocks.
- * @returns Is the property satisfied?
- */
-function validatorSetReplication(hist: BlockHistory): boolean {
- const blocks = hist.blocks;
- let good = true;
-
- // Each committed block on the consumer chain has a last vscID
- // received that informs the validator set at the NEXT height.
- // Thus, on every received VSCPacket with vscID at height H,
- // the consumer sets hToVscID[H+1] to vscID.
- //
- // The consumer valset is exactly the valset on the provider
- // at the NEXT height after the vscID was sent.
- // Thus, on every sent VSCPacket with vscID at height H,
- // the provider sets vscIDtoH[vscID] to H+1
- //
- // As a result, for every height hC on the consumer, the active
- // valset was last updated by the VSCPacket with ID vscID = hToVscID[hc].
- // This packet was sent by the provider at height hP-1, with hP = vscIDtoH[vscID].
- // This means that the consumer valset at height hC MUST match
- // the provider valset at height hP.
- //
- // We compare these valsets, which are committed in blocks
- // hC-1 and hP-1, respectively (the valset is always used at the NEXT height).
- for (const [hC, b] of blocks[C]) {
- if (hC < 1) {
- // The model starts at consumer height 0, so there is
- // no committed block at height - 1. This means it does
- // not make sense to try to check the property for height 0.
- continue
- }
- const snapshotC = b.propertiesSystemState;
- // Get the vscid of the last update which dictated
- // the consumer valset valsetC committed at hC-1
- const vscid = snapshotC.hToVscID[hC];
- // The VSU packet was sent at height hP-1
- const hP = snapshotC.vscIDtoH[vscid];
- // Compare the validator sets at hC-1 and hP-1
- const valsetC = blocks[C].get(hC - 1)!.propertiesSystemState.consumerPower;
- // The provider set is implicitly defined by the status and tokens (power)
- if (hP < 1) {
- // The model starts at provider height 0, so there is
- // no committed block at height - 1. This means it does not
- // make sense to try to check the property for height 0.
- continue
- }
- const snapshotP = blocks[P].get(hP - 1)!.propertiesSystemState;
- const statusP = snapshotP.status;
- const tokensP = snapshotP.tokens;
- assert(valsetC.length === statusP.length, 'this should never happen.');
- assert(valsetC.length === tokensP.length, 'this should never happen.');
- valsetC.forEach((power, i) => {
- if (power !== null) { // null means the validator is not in the set
- // Check that the consumer power is strictly equal to the provider power
- good = good && (tokensP[i] === power);
- }
- })
- statusP.forEach((status, i) => {
- if (status === Status.BONDED) {
- const power = tokensP[i];
- // Check that the consumer power is strictly equal to the provider power
- good = good && (valsetC[i] === power);
- }
- else {
- // Ensure that the consumer validator set does not contain a non-bonded validator
- good = good && (valsetC[i] === null);
- }
- })
-
- }
- return good;
-}
-
-/**
- * Checks the bond-based consumer voting power property as defined
- * in https://github.com/cosmos/ibc/blob/main/spec/app/ics-028-cross-chain-validation/system_model_and_properties.md#system-properties
- * but modified to account for finite executions and always zero slash factors.
- *
- * @param hist A history of blocks.
- * @returns Is the property satisfied?
- */
-function bondBasedConsumerVotingPower(hist: BlockHistory): boolean {
- const partialOrder = hist.partialOrder;
- const blocks = hist.blocks;
- /**
- * @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.propertiesSystemState.status[i] !== Status.UNBONDED) {
- x += block.propertiesSystemState.tokens[i];
- }
- x += sum(
- block.propertiesSystemState.undelegationQ
- .filter((e) => e.val === i)
- .filter((e) => hp <= e.creationHeight)
- .map((e) => e.initialBalance),
- );
- return x;
- });
- }
- function powerConsumer(block: CommittedBlock) {
- return block.propertiesSystemState.consumerPower;
- }
- function inner(hc: number): boolean {
- const hp = partialOrder.getGreatestPred(C, hc);
- assert(hp !== undefined, 'this should never happen.');
- function getHC_() {
- const tsHC = (blocks[C].get(hc) as CommittedBlock).propertiesSystemState
- .t[C];
- // Get earliest height on consumer
- // that a VSC received at hc could mature
- const heights = Array.from(blocks[C].keys()).sort((a, b) => a - b);
- for (let i = 0; i < heights.length; i++) {
- const hc_ = heights[i];
- if (
- tsHC + UNBONDING_SECONDS_C <=
- (blocks[C].get(hc_) as CommittedBlock).propertiesSystemState.t[C]
- ) {
- return hc_;
- }
- }
- return undefined;
- }
- const hc_ = getHC_();
- let hp_ = undefined;
- if (hc_ !== undefined) {
- hp_ = partialOrder.getLeastSucc(C, hc_);
- }
- let limit = Math.max(...Array.from(blocks[P].keys())) + 1;
- if (hp_ !== undefined) {
- // If provider receives maturation
- // only check property up to and not including
- // the block at which received.
- limit = hp_;
- }
- for (let h = hp; h < limit; h++) {
- for (let i = 0; i < NUM_VALIDATORS; i++) {
- const powerP = powerProvider(
- blocks[P].get(h) as CommittedBlock,
- hp + 1,
- );
- const powerC = powerConsumer(blocks[C].get(hc) as CommittedBlock);
- if (powerC[i] !== null) {
- if (powerP[i] < (powerC[i] as number)) {
- return false;
- }
- }
- }
- }
- return true;
- }
- return _.reduce(
- Array.from(blocks[C].keys()),
- (good, hc) => good && inner(hc),
- true,
- );
-}
-
-export {
- PartialOrder,
- CommittedBlock,
- BlockHistory,
- stakingWithoutSlashing,
- bondBasedConsumerVotingPower,
- validatorSetReplication,
-};