DecidePeerSourcing.tla

vim: shiftwidth=2
---- MODULE DecidePeerSourcing ----

UNDEFINED == ""

\* BaseCurrencyNetwork
NetParams(btcMode) ==
  CASE btcMode = "BTC_MAINNET" -> "MainNetParams"
  [] btcMode = "BTC_TESTNET" -> "TestNet3Params"
  [] btcMode = "BTC_REGTEST" -> "RegTestParams"
  [] btcMode = "BTC_DAO_TESTNET" -> "RegTestParams"
  [] btcMode = "BTC_DAO_BETANET" -> "MainNetParams"
  [] btcMode = "BTC_DAO_REGTEST" -> "RegTestParams"
  [] OTHER -> "IMPOSSIBLE"

(* --algorithm algo1

variables
  \* BaseCurrencyNetwork
  btcMode \in {
    "BTC_MAINNET", "BTC_TESTNET", "BTC_REGTEST",
    "BTC_DAO_TESTNET", "BTC_DAO_BETANET", "BTC_DAO_REGTEST"},
  netParams = NetParams(btcMode),

  \* RegTestHost
  regtestHost \in {"NONE", "LOCAL", "REMOTE"},
  regtestHostAddrType = UNDEFINED,
  \* Checked in WalletConfig.setToOnlyUseRegTestHostPeerNode
  isRegtestHostAnOnionAddress \in {TRUE, FALSE},

  \* PreferencesPayload.useTorForBitcoinJ
  \* Either default value (TRUE) or as set by NetworkSettingsView
  prefPayloadUseTorForBitcoinJ \in {TRUE, FALSE},

  \* Preferences.getUseTorForBitcoinJ
  prefUseTorForBitcoinJ = UNDEFINED,

  \* Config.ignoreLocalBtcNode
  toldToIgnoreLocalBtcNode \in {TRUE, FALSE},
  \* LocalBitcoinNode.shouldBeUsed
  shouldUseLocalBitcoinNode = UNDEFINED,
  \* LocalBitcoinNode.isDetected
  localBtcNodeDetected \in {TRUE, FALSE},

  \* Preferences.readPersisted
  configUseTorForBtcOptionSetExplicitly \in {TRUE, FALSE},
  configUseTorForBtcOption \in IF configUseTorForBtcOptionSetExplicitly THEN {TRUE, FALSE} ELSE {UNDEFINED},

  \* Config.useAllProvidedNodes
  useAllProvidedNodes \in {TRUE, FALSE},
  isUseClearNodesWithProxies = UNDEFINED,

  \* Preferences.getBitcoinNodesOptionOrdinal
  bitcoinNodesOption \in {"CUSTOM", "PUBLIC", "PROVIDED"},
  customNodesProvided \in {TRUE, FALSE},

  proxyPassed = UNDEFINED,
  doProposePeers = FALSE,

  warnings = {},
  discoveryType = UNDEFINED,
  peerAddressType = UNDEFINED,
  explicitPeers = UNDEFINED,
  sourcingMethod = UNDEFINED;

\* Any operators in a define block can reference PlusCal variables
define

TypeInv ==
  /\ peerAddressType \in {UNDEFINED, "ONION_AND_PROXIED", "ONION", "CLEAR"}
  /\ explicitPeers \in {UNDEFINED, "LOCALHOST", "REGTESTHOST", "CUSTOM", "PROVIDED"}
  /\ sourcingMethod \in {UNDEFINED, "EXPLICIT_LIST", "DISCOVERY"}
  /\ discoveryType \in {UNDEFINED, "DNS", "SOCKS5MULTI"}
  /\ \A warning \in warnings : warning \in {"PUBLIC_MAINNET", "NO_TOR"}
  /\ netParams /= "IMPOSSIBLE"
  /\ regtestHostAddrType \in {UNDEFINED, "ONION", "INET_FROM_NAME"}

UsingExplicitPeerList == sourcingMethod = "EXPLICIT_LIST"

UsingBisqProvidedPeers ==
  /\ UsingExplicitPeerList
  /\ explicitPeers = "PROVIDED"

UsingCustomPeers ==
  /\ UsingExplicitPeerList
  /\ explicitPeers = "CUSTOM"

UsingOnlyLocalhostPeer ==
  /\ UsingExplicitPeerList
  /\ explicitPeers = "LOCALHOST"

UsingDiscovery == sourcingMethod = "DISCOVERY"

WarningsContain(warning) == warning \in warnings

\* LocalBitcoinNode.shouldBeIgnored
shouldIgnoreLocalBtcNode ==
  \/ toldToIgnoreLocalBtcNode
  \/ btcMode = "BTC_DAO_REGTEST"
  \/ btcMode = "BTC_DAO_TESTNET"
  \* TODO what about BTC_DAO_BETANET?

InDesiredState ==
  /\ bitcoinNodesOption = "CUSTOM" =>
    \/ /\ ~customNodesProvided
       /\ UsingBisqProvidedPeers
    \/ /\ customNodesProvided
       /\ UsingCustomPeers
  /\ shouldUseLocalBitcoinNode =>
    /\ localBtcNodeDetected
    /\ ~shouldIgnoreLocalBtcNode
    /\ UsingOnlyLocalhostPeer
  /\ shouldIgnoreLocalBtcNode =>
    \/ ~UsingExplicitPeerList
    \/ explicitPeers /= "LOCALHOST"
  /\ UsingDiscovery = WarningsContain("PUBLIC_MAINNET")

end define;

begin

\* LocalBitcoinNode.shouldBeUsed
shouldUseLocalBitcoinNode := ~shouldIgnoreLocalBtcNode /\ localBtcNodeDetected;

\* Preferences.readPersisted
if configUseTorForBtcOptionSetExplicitly then
  prefPayloadUseTorForBitcoinJ := configUseTorForBtcOption;
end if;

\* Preferences.getUseTorForBitcoinJ
if (/\ \/ btcMode # "BTC_MAINNET"
       \/ shouldUseLocalBitcoinNode
    /\ ~configUseTorForBtcOptionSetExplicitly) then
  prefUseTorForBitcoinJ := FALSE;
else
  prefUseTorForBitcoinJ := prefPayloadUseTorForBitcoinJ;
end if;

\* WalletsSetup.initialize
proxyPassed := prefUseTorForBitcoinJ;

\* WalletsSetup.setupSourceOfPeers
if netParams = "RegTestParams" then
  \* relevant: BitcoinModule.configure
  if regtestHost = "LOCAL" then
    explicitPeers := "LOCALHOST";
  elsif regtestHost = "REMOTE" then
    explicitPeers := "REGTESTHOST";
    if isRegtestHostAnOnionAddress then
      regtestHostAddrType := "ONION";
    else
      regtestHostAddrType := "INET_FROM_NAME";
    end if;
  else
    doProposePeers := TRUE;
  end if;
elsif shouldUseLocalBitcoinNode then
  explicitPeers := "LOCALHOST";
else
  doProposePeers := TRUE;
end if;

\* doProposePeers represents a substantial layer of complexity
\* that's sometimes bypassed.

\* WalletsSetup.proposePeersFromBtcNodesRepository
if doProposePeers then
  \* BtcNodesSetupPreferences.selectPreferredNodes
  if bitcoinNodesOption = "CUSTOM" then
    if customNodesProvided then
      explicitPeers := "CUSTOM";
    else
      explicitPeers := "PROVIDED";
    end if;
  elsif bitcoinNodesOption = "PUBLIC" then
    explicitPeers := UNDEFINED;
  else
    explicitPeers := "PROVIDED";
  end if;

  \* BtcNodes.getProvidedBtcNodes
  if explicitPeers = "PROVIDED" then
    if btcMode # "BTC_MAINNET" then
      explicitPeers := UNDEFINED;
    end if;
  end if;

  isUseClearNodesWithProxies := useAllProvidedNodes \/ bitcoinNodesOption = "CUSTOM";

  if explicitPeers # UNDEFINED then
    \* BtcNodesRepository.getPeerAddresses
    if proxyPassed then
      if isUseClearNodesWithProxies then
        peerAddressType := "ONION_AND_PROXIED";
      else
        peerAddressType := "ONION";
      end if;
    else
      peerAddressType := "CLEAR";
    end if;
  \* WalletsSetup.proposePeers
  elsif proxyPassed then
    discoveryType := "SOCKS5MULTI";
    warnings := warnings \union {"PUBLIC_MAINNET"};
  elsif btcMode = "BTC_MAINNET" then
    warnings := warnings \union {"PUBLIC_MAINNET", "NO_TOR"};
  end if;
end if;

\* WalletConfig.setupSourceOfPeers
if explicitPeers # UNDEFINED then
  sourcingMethod := "EXPLICIT_LIST";
else
  \* WalletConfig.setupDiscovery
  if netParams # "RegTestParams" then
    sourcingMethod := "DISCOVERY";
    if discoveryType = UNDEFINED then
      discoveryType := "DNS";
    end if;
  end if;
end if;

end algorithm; *)

Done == pc = "Done"

Inv ==
  /\ IF Done THEN InDesiredState ELSE TRUE
  /\ TypeInv

====

This is a TLA+ specification of the algorithm we use for deciding what Bitcoin peers to use (or where to find them). I wrote it because informal reasoning wasn't enough to have a clear understanding of how this process works in Bisq, and because this would be a valuable experience if we ever want to use model checking on more critical parts of the system.

The readability is subpar and there are practically no explaining comments: that's because I wrote this for myself, not intending anyone else to use it (at this point at least). Nonetheless, I thought it would be interesting to other contributors to see what a complicated sequential algorithm looks like in TLA+. Note that the main purpose of TLA+ is checking concurrent algorithms, so this sequential example doesn't play into TLA+ strenghts.

The main part of the file is in gray, because Github doesn't know how to syntax highlight PlusCal code. PlusCal is a sublanguage within TLA+ (that's unfortunately written entirely in a comment).

• The algorithm is described between lines 120-223. That's where Bisq's code for deciding peer sourcing is described. Notice how difficult to understand it is.
• Lines 18-64 describe the variables and their initial state. Those having the form varName \in {A,B,C} are what you'd call inputs. For example, localBtcNodeDetected \in {TRUE, FALSE} means that we'll check if the algorithm is correct both when a local Bitcoin node has been detected and when it hasn't.
• Lines 103-116 (InDesiredState) is where we define what it means for the end state of this algorithm to be correct. At the moment this describes only very few requirements (like being configured to use custom nodes causing custom nodes to be used). This is what I'm working on now: describing what it means for our peer sourcing decisions to be correct.

Started a repo for these: https://github.com/dmos62/bisq-formal-specs