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

====

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