Code

Model-based tests for ICS02#601

Code

Merged

adizere merged 57 commits intomasterinformalsystems/hermes:masterfrom vitor/ics02_mbtinformalsystems/hermes:vitor/ics02_mbtCopy head branch name to clipboardFeb 12, 2021

+937-3

Commits

Commits on Feb 2, 2021

• Add ICS02 model

  vitorenesduarte

  committed
  413d3f4

  Copy full SHA for 413d3f4

• Add MBT test driver

  vitorenesduarte

  committed
  065631e

  Copy full SHA for 065631e

• Add ICS02TestExecutor

  vitorenesduarte

  committed
  b98c7d3

  Copy full SHA for b98c7d3

• Add another apalache counterexample

  vitorenesduarte

  committed
  6685cc1

  Copy full SHA for 6685cc1

• Fix ICS02.tla: client counter starts at 0

  vitorenesduarte

  committed
  f863486

  Copy full SHA for f863486

• Check for errors in MockContext.deliver

  vitorenesduarte

  committed
  cd0d0a6

  Copy full SHA for cd0d0a6

• Handle errors in MBT tests

  vitorenesduarte

  committed
  02c020b

  Copy full SHA for 02c020b

• Remove SyntheticTendermint mock context

  vitorenesduarte

  committed
  a5d06c5

  Copy full SHA for a5d06c5

• More idiomatic check_next_state

  vitorenesduarte

  committed
  356c6d2

  Copy full SHA for 356c6d2

Commits on Feb 3, 2021

• Buffered file reads

  vitorenesduarte

  committed
  6ab8611

  Copy full SHA for 6ab8611

• Make extract_handler_error_kind generic over the IBC handler

  vitorenesduarte

  committed
  490d77b

  Copy full SHA for 490d77b

• Support multiple chains in MBT

  vitorenesduarte

  committed
  92b843c

  Copy full SHA for 92b843c

• Make eyre a dev-dependency

  vitorenesduarte

  committed
  d57cf41

  Copy full SHA for d57cf41

• s/ICS0/IBC on TLA files

  vitorenesduarte

  committed
  f4dbe00

  Copy full SHA for f4dbe00

• Initial support for conn open init

  vitorenesduarte

  committed
  20867a5

  Copy full SHA for 20867a5

• Start connection and channel identifiers at 0

  vitorenesduarte

  committed
  e5e2f7b

  Copy full SHA for e5e2f7b

• Add conn open init to TLA spec

  vitorenesduarte

  committed
  b9ca90a

  Copy full SHA for b9ca90a

• Represent clients with a record in TLA spec

  vitorenesduarte

  committed
  f3cd434

  Copy full SHA for f3cd434

• Finish connection open init

  vitorenesduarte

  committed
  4167d29

  Copy full SHA for 4167d29

• s/state/step

  vitorenesduarte

  committed
  7755fec

  Copy full SHA for 7755fec

Commits on Feb 4, 2021

• Minimize diff

  vitorenesduarte

  committed
  70e70f6

  Copy full SHA for 70e70f6

• Merge branch 'master' into vitor/ics02_mbt

  vitorenesduarte

  committed
  44747d3

  Copy full SHA for 44747d3

• Modularize TLA spec

  vitorenesduarte

  committed
  41d34d3

  Copy full SHA for 41d34d3

• TLA format convention

  vitorenesduarte

  committed
  1f9881c

  Copy full SHA for 1f9881c

• s/Null/None

  vitorenesduarte

  committed
  e2605bb

  Copy full SHA for e2605bb

• Sketch conn open try; Model chain's height

  vitorenesduarte

  committed
  5b98a7e

  Copy full SHA for 5b98a7e

• Bound model space

  vitorenesduarte

  committed
  244efa6

  Copy full SHA for 244efa6

• Only update chain height upon success

  vitorenesduarte

  committed
  7d9202a

  Copy full SHA for 7d9202a

• Check that chain heights match the ones in the model

  vitorenesduarte

  committed
  28879f0

  Copy full SHA for 28879f0

• Sketch conn open try

  vitorenesduarte

  committed
  a870537

  Copy full SHA for a870537

• Sketch conn open try

  vitorenesduarte

  committed
  a533def

  Copy full SHA for a533def

• Model missing connections and connection mismatches in conn open try

  vitorenesduarte

  committed
  1cdb02a

  Copy full SHA for 1cdb02a

• Trigger bug in conn open try

  vitorenesduarte

  committed
  0186a1c

  Copy full SHA for 0186a1c

• Merge branch 'master' into vitor/ics02_mbt

  vitorenesduarte

  committed
  f777144

  Copy full SHA for f777144

• Go back to previous way of generating connection and channel ids

  vitorenesduarte

  committed
  6b6cd43

  Copy full SHA for 6b6cd43

• Disable failing MBT test

  vitorenesduarte

  committed
  6186bec

  Copy full SHA for 6186bec

Commits on Feb 5, 2021

• Fix panic in conn open try when no connection id is provided

  vitorenesduarte

  committed
  a7b50d7

  Copy full SHA for a7b50d7

• ICS02TestExecutor -> IBCTestExecutor

  vitorenesduarte

  committed
  5b66aac

  Copy full SHA for 5b66aac

• Merge branch 'vitor/conn_open_try' into vitor/ics02_mbt

  vitorenesduarte

  committed
  095433e

  Copy full SHA for 095433e

• Failing MBT test now passes with #615

  vitorenesduarte

  committed
  f2194cf

  Copy full SHA for f2194cf

Commits on Feb 8, 2021

• Add notes on MBT

  vitorenesduarte

  committed
  7bdd3b6

  Copy full SHA for 7bdd3b6

• Remove ICS02

  vitorenesduarte

  committed
  9ee48bd

  Copy full SHA for 9ee48bd

• Add README

  vitorenesduarte

  committed
  035651e

  Copy full SHA for 035651e

• Improve README

  vitorenesduarte

  committed
  b6854ce

  Copy full SHA for b6854ce

• Remove MBT intro

  vitorenesduarte

  committed
  cd484a6

  Copy full SHA for cd484a6

• new lines

  vitorenesduarte

  committed
  d69d15e

  Copy full SHA for d69d15e

Commits on Feb 9, 2021

• Merge branch 'master' into vitor/ics02_mbt

  vitorenesduarte

  committed
  b4aea95

  Copy full SHA for b4aea95

• Make MBT README more easily discoverable

  vitorenesduarte

  committed
  5e9dd63

  Copy full SHA for 5e9dd63

• IBCTestExecutor: Map from ChainId (instead of String) to MockContext

  vitorenesduarte

  committed
  fb20ce0

  Copy full SHA for fb20ce0

• s/epoch/revision

  vitorenesduarte

  committed
  75db6bb

  Copy full SHA for 75db6bb

• Move from eyre to thiserror

  vitorenesduarte

  committed
  a102863

  Copy full SHA for a102863

• Improve README

  vitorenesduarte

  committed
  2e5d6de

  Copy full SHA for 2e5d6de

• Improve README

  vitorenesduarte

  committed
  dfb683d

  Copy full SHA for dfb683d

• Improve arguments order in modelator::test

  vitorenesduarte

  committed
  7e24841

  Copy full SHA for 7e24841

Commits on Feb 10, 2021

• Improve chain identifiers

  vitorenesduarte

  committed
  5d6bf08

  Copy full SHA for 5d6bf08

• Improve README

  vitorenesduarte

  committed
  60e4aba

  Copy full SHA for 60e4aba

Commits on Feb 11, 2021

• Merge branch 'master' into vitor/ics02_mbt

  vitorenesduarte

  committed
  3a991e7

  Copy full SHA for 3a991e7