Code

Inductive invariant validation.#6

Code

Merged

lemmy merged 24 commits intoheidihoward:mainheidihoward/pbft-tlaplus:mainfrom lemmy:mku-gh05lemmy/pbft-tlaplus:mku-gh05Copy head branch name to clipboardSep 6, 2024

+390-22

Commits

Commits on Aug 19, 2024

• Inductive invariant validation with Apalache.

  Show description for 48316b6
  lemmy

  committed
  48316b6

  Copy full SHA for 48316b6

• Build main/HEAD of Apalache until new official Apalache builds are available.

  Show description for decd45d
  lemmy

  committed
  decd45d

  Copy full SHA for decd45d

• Remove bogus www.` from url that causes a https cert error.

  Show description for b2108a4
  lemmy

  committed
  b2108a4

  Copy full SHA for b2108a4

• Consume newest Apalache release.

  Show description for 01486bb
  lemmy

  committed
  01486bb

  Copy full SHA for 01486bb

• Install TLC nightly build to consume tlaplus/tlaplus@6a1ea00

  Show description for b2bba8f
  lemmy

  committed
  b2bba8f

  Copy full SHA for b2bba8f

• Switch to TLC's generate mode to prevent it from generating an action's complete set of successor states.

  Show description for b295f93
  lemmy

  committed
  b295f93

  Copy full SHA for b295f93

Commits on Sep 2, 2024

• Leave note why Tstamp and Views have to be redefined to be finite sets.

  Show description for a916aa4
  lemmy

  committed
  a916aa4

  Copy full SHA for a916aa4

• Remove unused ConstInit.

  Show description for 6d6ca6e
  lemmy

  committed
  6d6ca6e

  Copy full SHA for 6d6ca6e

• TLAPM does not (yet) support bound tuples (tlaplus/tlapm#140)

  Show description for fda5046
  lemmy

  committed
  fda5046

  Copy full SHA for fda5046

Commits on Sep 3, 2024

• Ignore TLAPS fingerprint cache.

  Show description for a323287
  lemmy

  committed
  a323287

  Copy full SHA for a323287

• Rewrite TypeOK into monstrous universal quantification that avoids constraint explosion.

  Show description for 61e7b5e
  lemmy

  committed
  61e7b5e

  Copy full SHA for 61e7b5e

• Decrease number of generates values to prevent Apalache from exceeding its heap memory.

  Show description for 9a16ecb
  lemmy

  committed
  9a16ecb

  Copy full SHA for 9a16ecb

• mlogs is defined for all replicas (outside of TLA+, one would call it a total function). Without this constraint, Apalache!Gen may generate a function that is not defined for all replicas

  Show description for f3f979e
  lemmy

  committed
  f3f979e

  Copy full SHA for f3f979e

• Remove incomplete leftover.

  Show description for b7b4f4e
  lemmy

  committed
  b7b4f4e

  Copy full SHA for b7b4f4e

• Partial inductive invariant checking with Apalache.

  Show description for da5a4d5
  lemmy

  committed
  da5a4d5

  Copy full SHA for da5a4d5

Commits on Sep 4, 2024

• Push Apalache!Gen into dedicated .tla file to prevent TLC from failing due to missing Apalache.tla import.

  Show description for 779347b
  lemmy

  committed
  779347b

  Copy full SHA for 779347b

• No surprise that SafetyInv is violated if *all* nodes are Byzantine.

  Show description for 1c244a0
  lemmy

  committed
  1c244a0

  Copy full SHA for 1c244a0

• Assume that the number of byzantine replicas is less than what the protocol can tolerate.

  Show description for cefe95f
  lemmy

  committed
  cefe95f

  Copy full SHA for cefe95f

• Generate, simulate, validate, and verify with TLC and Apalache.

  Show description for eb1d4f3
  lemmy

  committed
  eb1d4f3

  Copy full SHA for eb1d4f3

• Mitigate state-space explosion of two byzantine actions to prevent TLC from attempting to generate sets that are too large.

  Show description for 1c1c3a0
  lemmy

  committed
  1c1c3a0

  Copy full SHA for 1c1c3a0

• Do not parse *all* specs because Apalache module is not there.

  Show description for 3f99960
  lemmy

  committed
  3f99960

  Copy full SHA for 3f99960

Commits on Sep 5, 2024

• Finish in reasonable time of approx 10 minutes.

  Show description for bfe1c8a
  lemmy

  committed
  bfe1c8a

  Copy full SHA for bfe1c8a

Commits on Sep 6, 2024

• Bug: Range over constant SeqNums instead of Views.

  Show description for 9477c9f
  lemmy

  committed
  9477c9f

  Copy full SHA for 9477c9f

• Simulation starting at GenInit predicate with Apalache.

  Show description for a6c7b96
  lemmy

  committed
  a6c7b96

  Copy full SHA for a6c7b96