------------------------- MODULE LightTests --------------------------- EXTENDS Lightclient_003_draft (* The light client history, which is the function mapping states 0..nprobes to the record with fields: - verified: the latest verified block in the previous state - current: the block that is being checked in the previous state - now: the time point in the previous state - verdict: the light client verdict in the previous state *) VARIABLE \* @type: Int -> [verified: BLOCK, current: BLOCK, now: Int, verdict: Str]; history \* This predicate extends the LightClient Init predicate with history tracking InitTest == /\ Init /\ history = [ n \in {0} |-> [ verified |-> prevVerified, current |-> prevCurrent, now |-> prevNow, verdict |-> prevVerdict ]] \* This predicate extends the LightClient Next predicate with history tracking NextTest == /\ Next /\ history' = [ n \in DOMAIN history \union {nprobes'} |-> IF n = nprobes' THEN [ verified |-> prevVerified', current |-> prevCurrent', now |-> prevNow', verdict |-> prevVerdict' ] ELSE history[n] ] \* Some useful operators for writing tests LightBlock(st) == history[st].current Height(st) == history[st].current.header.height ValSet(st) == LightBlock(st).header.VS ValCommits(st) == LightBlock(st).Commits \* Test an execution that finishes with failure TestFailure == /\ state = "finishedFailure" /\ Cardinality(DOMAIN fetchedLightBlocks) = TARGET_HEIGHT \* Test an execution that finishes with success TestSuccess == /\ state = "finishedSuccess" /\ Cardinality(DOMAIN fetchedLightBlocks) = TARGET_HEIGHT \* This test never produces a counterexample; so the model should be corrected TestFailedTrustingPeriod == \E s \in DOMAIN history : history[s].verdict = "FAILED_TRUSTING_PERIOD" TwoNotEnoughTrust == \E s1, s2 \in DOMAIN history : /\ s1 /= s2 /\ history[s1].verdict = "NOT_ENOUGH_TRUST" /\ history[s2].verdict = "NOT_ENOUGH_TRUST" ThreeNotEnoughTrust == \E s1, s2, s3 \in DOMAIN history : /\ s1 /= s2 /\ s2 /= s3 /\ s1 /= s3 /\ history[s1].verdict = "NOT_ENOUGH_TRUST" /\ history[s2].verdict = "NOT_ENOUGH_TRUST" /\ history[s3].verdict = "NOT_ENOUGH_TRUST" \* Test an execution that finishes with success, and processes two headers with insufficient trust on the way Test2NotEnoughTrustSuccess == /\ state = "finishedSuccess" /\ TwoNotEnoughTrust \* Test an execution that finishes with failure, and processes two headers with insufficient trust on the way Test2NotEnoughTrustFailure == /\ state = "finishedFailure" /\ TwoNotEnoughTrust \* Test an execution that finishes with success, and processes three headers with insufficient trust on the way Test3NotEnoughTrustSuccess == /\ state = "finishedSuccess" /\ ThreeNotEnoughTrust \* Test an execution that finishes with failure, and processes three headers with insufficient trust on the way Test3NotEnoughTrustFailure == /\ state = "finishedFailure" /\ ThreeNotEnoughTrust TestNonMonotonicHeight == /\ \E s \in DOMAIN history : \* this is wrong /\ history[s].current.header.height <= history[s].verified.header.height \* everything else is correct /\ history[s].current.header /= history[s].verified.header /\ history[s].current.header.time > history[s].verified.header.time /\ history[s].current.header.time < history[s].now /\ history[s].verified.header.time + TRUSTING_PERIOD > history[s].now /\ history[s].current.Commits /= {} /\ history[s].current.Commits \subseteq history[s].current.header.VS (* Following three tests have been disabled for now, please refer issue: https://github.com/informalsystems/tendermint-rs/issues/659 TestEmptyCommitEmptyValset == /\ \E s \in DOMAIN history : \* this is wrong /\ history[s].current.Commits = {} /\ ValSet(s) = {} \* everything else is correct /\ history[s].current.header /= history[s].verified.header /\ history[s].current.header.height > history[s].verified.header.height /\ history[s].current.header.time > history[s].verified.header.time /\ history[s].current.header.time < history[s].now /\ history[s].verified.header.time + TRUSTING_PERIOD > history[s].now TestEmptyCommitNonEmptyValset == /\ \E s \in DOMAIN history : \* this is wrong /\ history[s].current.Commits = {} /\ ValSet(s) /= {} \* everything else is correct /\ history[s].current.header /= history[s].verified.header /\ history[s].current.header.height > history[s].verified.header.height /\ history[s].current.header.time > history[s].verified.header.time /\ history[s].current.header.time < history[s].now /\ history[s].verified.header.time + TRUSTING_PERIOD > history[s].now TestLessThanTwoThirdsCommit == /\ \E s \in DOMAIN history : \* this is wrong LET CMS == history[s].current.Commits UVS == history[s].current.header.VS TVS == history[s].verified.header.VS IN /\ history[s].current.header.height > history[s].verified.header.height + 1 /\ CMS /= {} /\ CMS \subseteq UVS /\ 3 * Cardinality(CMS) < 2 * Cardinality(UVS) /\ 3 * Cardinality(CMS \intersect TVS) < Cardinality(TVS) \* everything else is correct /\ history[s].current.header /= history[s].verified.header /\ history[s].current.header.height > history[s].verified.header.height /\ history[s].current.header.time > history[s].verified.header.time /\ history[s].current.header.time < history[s].now /\ history[s].verified.header.time + TRUSTING_PERIOD > history[s].now *) \* Time-related tests \* Test an execution where a header is received from the future TestHeaderFromFuture == /\ \E s \in DOMAIN history : /\ history[s].now < history[s].current.header.time /\ history[s].now < history[s].verified.header.time + TRUSTING_PERIOD \* Test an execution where the untrusted header time is before the trusted header time TestUntrustedBeforeTrusted == /\ \E s \in DOMAIN history : LET CMS == history[s].current.Commits UVS == history[s].current.header.VS IN /\ history[s].current.header.time < history[s].verified.header.time /\ history[s].now < history[s].verified.header.time + TRUSTING_PERIOD /\ CMS /= {} /\ UVS /= {} /\ Cardinality(CMS) < Cardinality(UVS) \* Test an execution where a header is outside the trusting period TestHeaderNotWithinTrustingPeriod == /\ Cardinality(DOMAIN fetchedLightBlocks) = TARGET_HEIGHT /\ \E s \in DOMAIN history : /\ history[s].now > history[s].verified.header.time + TRUSTING_PERIOD /\ history[s].current.header.time < history[s].now \* Validator set tests \* Test an execution where the validator sets differ at each step TestValsetDifferentAllSteps == /\ Cardinality(DOMAIN fetchedLightBlocks) = TARGET_HEIGHT /\ \A s1, s2 \in DOMAIN history : s1 /= s2 => history[s1].current.header.VS /= history[s2].current.header.VS TestHalfValsetChanges == /\ Cardinality(DOMAIN fetchedLightBlocks) = TARGET_HEIGHT /\ \E s1, s2 \in DOMAIN history : /\ s2 = s1 + 1 /\ Cardinality(ValSet(s1)) >= 3 /\ 2 * Cardinality(ValSet(s1) \intersect ValSet(s2)) < Cardinality(ValSet(s1)) TestHalfValsetChangesVerdictSuccess == /\ Cardinality(DOMAIN fetchedLightBlocks) = TARGET_HEIGHT /\ \E s1, s2 \in DOMAIN history : /\ s2 = s1 + 1 /\ history[s2].verdict = "SUCCESS" /\ Cardinality(ValSet(s1)) >= 3 /\ 2 * Cardinality(ValSet(s1) \intersect ValSet(s2)) < Cardinality(ValSet(s1)) TestHalfValsetChangesVerdictNotEnoughTrust == /\ Cardinality(DOMAIN fetchedLightBlocks) = TARGET_HEIGHT /\ \E s1, s2 \in DOMAIN history : /\ s2 = s1 + 1 /\ history[s2].verdict = "NOT_ENOUGH_TRUST" /\ Cardinality(ValSet(s1)) >= 3 /\ 2 * Cardinality(ValSet(s1) \intersect ValSet(s2)) < Cardinality(ValSet(s1)) TestValsetDoubles == /\ Cardinality(DOMAIN fetchedLightBlocks) = TARGET_HEIGHT /\ \E s1, s2 \in DOMAIN history : /\ s2 = s1 + 1 /\ Cardinality(ValSet(s1)) >= 2 /\ Cardinality(ValSet(s2)) = 2 * Cardinality(ValSet(s1)) TestValsetHalves == /\ Cardinality(DOMAIN fetchedLightBlocks) = TARGET_HEIGHT /\ \E s1, s2 \in DOMAIN history : /\ s2 = s1 + 1 /\ Cardinality(ValSet(s1)) >= 4 /\ Cardinality(ValSet(s1)) = 2 * Cardinality(ValSet(s2)) TestValsetChangesFully == /\ Cardinality(DOMAIN fetchedLightBlocks) = TARGET_HEIGHT /\ \E s1, s2 \in DOMAIN history : /\ s2 = s1 + 1 /\ Cardinality(ValSet(s1)) >= 2 /\ ValSet(s1) \intersect ValSet(s2) = {} TestLessThanThirdValsetChanges == /\ Cardinality(DOMAIN fetchedLightBlocks) = TARGET_HEIGHT /\ \E s1, s2 \in DOMAIN history : /\ s2 = s1 + 1 /\ Cardinality(ValSet(s1)) >= 4 /\ ValSet(s2) /= ValSet(s1) /\ 3 * Cardinality(ValSet(s2) \ ValSet(s1)) < Cardinality(ValSet(s1)) TestMoreThanTwoThirdsValsetChanges == /\ Cardinality(DOMAIN fetchedLightBlocks) = TARGET_HEIGHT /\ \E s1, s2 \in DOMAIN history : /\ s2 = s1 + 1 /\ Cardinality(ValSet(s1)) >= 4 /\ 3 * Cardinality(ValSet(s2) \ ValSet(s1)) > 2 * Cardinality(ValSet(s1)) TestOneThirdValsetChanges == /\ Cardinality(DOMAIN fetchedLightBlocks) = TARGET_HEIGHT /\ \E s1, s2 \in DOMAIN history : /\ s2 = s1 + 1 /\ Cardinality(ValSet(s1)) >= 3 /\ 3 * Cardinality(ValSet(s2) \ ValSet(s1)) = Cardinality(ValSet(s1)) TestTwoThirdsValsetChanges == /\ Cardinality(DOMAIN fetchedLightBlocks) = TARGET_HEIGHT /\ \E s1, s2 \in DOMAIN history : /\ s2 = s1 + 1 /\ Cardinality(ValSet(s1)) >= 3 /\ 3 * Cardinality(ValSet(s2) \ ValSet(s1)) = 2 * Cardinality(ValSet(s1)) TestLessThanTwoThirdsSign == /\ Cardinality(DOMAIN fetchedLightBlocks) = TARGET_HEIGHT /\ \E s \in DOMAIN history : /\ history[s].verified.header.time + TRUSTING_PERIOD > history[s].now \* this is wrong /\ \E commits \in SUBSET AllNodes: \E block \in BC!LightBlocks: /\ 3 * Cardinality(commits) < 2 * Cardinality(ValSet(s)) /\ CopyLightBlockFromChain(block, Height(s)) /\ LightBlock(s) = [ block EXCEPT !.Commits = commits] TestMoreThanTwoThirdsSign == /\ Cardinality(DOMAIN fetchedLightBlocks) = TARGET_HEIGHT /\ \E s \in DOMAIN history : 3 * Cardinality(ValCommits(s)) >= 2 * Cardinality(ValSet(s)) ============================================================================ \* When Apalache is fixed to work with operator params, we should rewrite the validator set tests as shown below \* A configurable test for two neighbor valsets TestNeighborValsets(test(_,_)) == /\ Cardinality(DOMAIN fetchedLightBlocks) = TARGET_HEIGHT /\ \E s1, s2 \in DOMAIN history : /\ s2 = s1 + 1 /\ test(ValSet(s1), ValSet(s2)) \* A configurable test for two neighbor valsets and expected verdict TestNeighborValsetsVerdict(test(_,_), want_verdict) == /\ Cardinality(DOMAIN fetchedLightBlocks) = TARGET_HEIGHT /\ \E s1, s2 \in DOMAIN history : /\ s2 = s1 + 1 /\ test(ValSet(s1), ValSet(s2)) /\ history[s2].verdict = want_verdict HalfValsetChanges(vs1, vs2) == /\ Cardinality(vs1) >= 3 /\ 2 * Cardinality(vs1 \intersect vs2) < Cardinality(vs1) TestHalfValsetChanges == TestNeighborValsets(HalfValsetChanges) TestHalfValsetChangesVerdictSuccess == TestNeighborValsetsVerdict(HalfValsetChanges, "SUCCESS") TestHalfValsetChangesVerdictNotEnoughTrust == TestNeighborValsetsVerdict(HalfValsetChanges, "NOT_ENOUGH_TRUST") ValsetDoubles(vs1, vs2) == /\ Cardinality(vs1) >= 2 /\ Cardinality(vs2) = 2 * Cardinality(vs1) TestValsetDoubles == TestNeighborValsets(ValsetDoubles) TestValsetDoublesVerdictSuccess == TestNeighborValsetsVerdict(ValsetDoubles, "SUCCESS") TestValsetDoublesVerdictNotEnoughTrust == TestNeighborValsetsVerdict(ValsetDoubles, "NOT_ENOUGH_TRUST")