mukan-consensus/spec/light-client/attacks/MC_5_3.tla
Mukan Erkin Törük ef24c0b67e
Some checks are pending
docker-build-cometbft / vars (push) Waiting to run
docker-build-cometbft / build-images (amd64, ubuntu-24.04) (push) Blocked by required conditions
docker-build-cometbft / build-images (arm64, ubuntu-24.04-arm) (push) Blocked by required conditions
docker-build-cometbft / merge-images (push) Blocked by required conditions
docker-build-e2e-node / vars (push) Waiting to run
docker-build-e2e-node / build-images (amd64, ubuntu-24.04) (push) Blocked by required conditions
docker-build-e2e-node / build-images (arm64, ubuntu-24.04-arm) (push) Blocked by required conditions
docker-build-e2e-node / merge-images (push) Blocked by required conditions
initial: sovereign Mukan Network fork
2026-05-11 03:18:27 +03:00

18 lines
745 B
Text

------------------------- MODULE MC_5_3 -------------------------------------
AllNodes == {"n1", "n2", "n3", "n4", "n5"}
COMMON_HEIGHT == 1
CONFLICT_HEIGHT == 3
TRUSTING_PERIOD == 1400 \* two weeks, one day is 100 time units :-)
FAULTY_RATIO == <<1, 2>> \* < 1 / 2 faulty validators
VARIABLES
blockchain, \* the reference blockchain
refClock, \* current time in the reference blockchain
Faulty, \* the set of faulty validators
state, \* the state of the light client detector
conflictingBlock, \* an evidence that two peers reported conflicting blocks
attackers
INSTANCE Isolation_001_draft
============================================================================