Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Replace difftests with model-based testing using Quint #1368

Closed
wants to merge 83 commits into from
Closed

Replace difftests with model-based testing using Quint #1368

wants to merge 83 commits into from

Commits on Aug 17, 2023

  1. Start new attempt on Quint model of ICS

    @p-offtermatt
    p-offtermatt committed Aug 17, 2023
    Configuration menu
    Copy the full SHA
    e2b6407 View commit details
    Browse the repository at this point in the history

Commits on Aug 23, 2023

  1. Advance quint model

    @p-offtermatt
    p-offtermatt committed Aug 23, 2023
    Configuration menu
    Copy the full SHA
    283dc0a View commit details
    Browse the repository at this point in the history

Commits on Aug 24, 2023

  1. Add first finished draft of model

    @p-offtermatt
    p-offtermatt committed Aug 24, 2023
    Configuration menu
    Copy the full SHA
    2155a4f View commit details
    Browse the repository at this point in the history

Commits on Aug 25, 2023

  1. Add test run to model

    @p-offtermatt
    p-offtermatt committed Aug 25, 2023
    Configuration menu
    Copy the full SHA
    6ca6510 View commit details
    Browse the repository at this point in the history

  2. Rename model, add test, use powerset for nondeterminism

    @p-offtermatt
    p-offtermatt committed Aug 25, 2023
    Configuration menu
    Copy the full SHA
    e27e74b View commit details
    Browse the repository at this point in the history

  3. Reintroduce vsc changed tracking variables

    @p-offtermatt
    p-offtermatt committed Aug 25, 2023
    Configuration menu
    Copy the full SHA
    50fae34 View commit details
    Browse the repository at this point in the history

  4. Add text with what expliticly is modelled

    @p-offtermatt
    p-offtermatt authored Aug 25, 2023
    Configuration menu
    Copy the full SHA
    78e890a View commit details
    Browse the repository at this point in the history

  5. Add bluespec to ccv.qnt

    @p-offtermatt
    p-offtermatt authored Aug 25, 2023
    Configuration menu
    Copy the full SHA
    a1d57ef View commit details
    Browse the repository at this point in the history

  6. Add bluespec to expraSpells.qnt

    @p-offtermatt
    p-offtermatt authored Aug 25, 2023
    Configuration menu
    Copy the full SHA
    6c91866 View commit details
    Browse the repository at this point in the history

Commits on Sep 5, 2023

  1. Add docstring to extraSpells module

    @p-offtermatt
    p-offtermatt authored Sep 5, 2023
    Configuration menu
    Copy the full SHA
    2126eac View commit details
    Browse the repository at this point in the history

Commits on Sep 18, 2023

  1. Start rewriting model

    @p-offtermatt
    p-offtermatt committed Sep 18, 2023
    Configuration menu
    Copy the full SHA
    1320b95 View commit details
    Browse the repository at this point in the history

  2. Revert "Start rewriting model" 

    This reverts commit 1320b95.
    @p-offtermatt
    p-offtermatt committed Sep 18, 2023
    Configuration menu
    Copy the full SHA
    5fa449c View commit details
    Browse the repository at this point in the history

  3. Start rewriting quint model

    @p-offtermatt
    p-offtermatt committed Sep 18, 2023
    Configuration menu
    Copy the full SHA
    c05d9e6 View commit details
    Browse the repository at this point in the history

Commits on Sep 19, 2023

  1. Continue seperating logic in Quint model

    @p-offtermatt
    p-offtermatt committed Sep 19, 2023
    Configuration menu
    Copy the full SHA
    4bbe033 View commit details
    Browse the repository at this point in the history

Commits on Sep 20, 2023

  1. Start debugging cryptic error message

    @p-offtermatt
    p-offtermatt committed Sep 20, 2023
    Configuration menu
    Copy the full SHA
    5ebab39 View commit details
    Browse the repository at this point in the history

  2. Start adding endAndBeginBlock defs

    @p-offtermatt
    p-offtermatt committed Sep 20, 2023
    Configuration menu
    Copy the full SHA
    5bca6fc View commit details
    Browse the repository at this point in the history

Commits on Sep 21, 2023

  1. Diagnose Quint parser bug

    @p-offtermatt
    p-offtermatt committed Sep 21, 2023
    Configuration menu
    Copy the full SHA
    4f77d68 View commit details
    Browse the repository at this point in the history

  2. Fix type in Quint

    @p-offtermatt
    p-offtermatt committed Sep 21, 2023
    Configuration menu
    Copy the full SHA
    fa233d6 View commit details
    Browse the repository at this point in the history

  3. Add endBlock actions

    @p-offtermatt
    p-offtermatt committed Sep 21, 2023
    Configuration menu
    Copy the full SHA
    66663bf View commit details
    Browse the repository at this point in the history

Commits on Sep 26, 2023

  1. Start adding state machine module

    @p-offtermatt
    p-offtermatt committed Sep 26, 2023
    Configuration menu
    Copy the full SHA
    7b489fe View commit details
    Browse the repository at this point in the history

  2. Save status with crashing effect checker

    @p-offtermatt
    p-offtermatt committed Sep 26, 2023
    Configuration menu
    Copy the full SHA
    b992f8c View commit details
    Browse the repository at this point in the history

  3. Resolve issue by removing undefined field

    @p-offtermatt
    p-offtermatt committed Sep 26, 2023
    Configuration menu
    Copy the full SHA
    baaddb7 View commit details
    Browse the repository at this point in the history

Commits on Sep 27, 2023

  1. Remove add

    @p-offtermatt
    p-offtermatt committed Sep 27, 2023
    Configuration menu
    Copy the full SHA
    2c1341d View commit details
    Browse the repository at this point in the history

  2. Fix init

    @p-offtermatt
    p-offtermatt committed Sep 27, 2023
    Configuration menu
    Copy the full SHA
    e09968d View commit details
    Browse the repository at this point in the history

Commits on Sep 28, 2023

  1. Snapshot spec with parser crasher

    @p-offtermatt
    p-offtermatt committed Sep 28, 2023
    Configuration menu
    Copy the full SHA
    55ab595 View commit details
    Browse the repository at this point in the history

  2. Snapshot model

    @p-offtermatt
    p-offtermatt committed Sep 28, 2023
    Configuration menu
    Copy the full SHA
    0897e8c View commit details
    Browse the repository at this point in the history

  3. Start debugging tests

    @p-offtermatt
    p-offtermatt committed Sep 28, 2023
    Configuration menu
    Copy the full SHA
    d227aee View commit details
    Browse the repository at this point in the history

  4. Finish test for quint model

    @p-offtermatt
    p-offtermatt committed Sep 28, 2023
    Configuration menu
    Copy the full SHA
    09b1b87 View commit details
    Browse the repository at this point in the history

Commits on Sep 29, 2023

  1. Add README and improve folder structure

    @p-offtermatt
    p-offtermatt committed Sep 29, 2023
    Configuration menu
    Copy the full SHA
    96c101f View commit details
    Browse the repository at this point in the history

  2. Fix import

    @p-offtermatt
    p-offtermatt committed Sep 29, 2023
    Configuration menu
    Copy the full SHA
    aa2989e View commit details
    Browse the repository at this point in the history

  3. Add some invariants

    @p-offtermatt
    p-offtermatt committed Sep 29, 2023
    Configuration menu
    Copy the full SHA
    c291303 View commit details
    Browse the repository at this point in the history

  4. Refactor Consumer advancement

    @p-offtermatt
    p-offtermatt committed Sep 29, 2023
    Configuration menu
    Copy the full SHA
    94a0acb View commit details
    Browse the repository at this point in the history

  5. Snapshot error

    @p-offtermatt
    p-offtermatt committed Sep 29, 2023
    Configuration menu
    Copy the full SHA
    8818531 View commit details
    Browse the repository at this point in the history

  6. Make time module upper case

    @p-offtermatt
    p-offtermatt committed Sep 29, 2023
    Configuration menu
    Copy the full SHA
    633f8bb View commit details
    Browse the repository at this point in the history

  7. Add invariants

    @p-offtermatt
    p-offtermatt committed Sep 29, 2023
    Configuration menu
    Copy the full SHA
    f28d074 View commit details
    Browse the repository at this point in the history

  8. Clean up invariants

    @p-offtermatt
    p-offtermatt committed Sep 29, 2023
    Configuration menu
    Copy the full SHA
    c0363f2 View commit details
    Browse the repository at this point in the history

  9. Add script to run many invariants

    @p-offtermatt
    p-offtermatt committed Sep 29, 2023
    Configuration menu
    Copy the full SHA
    b9d8caf View commit details
    Browse the repository at this point in the history

Commits on Oct 2, 2023

  1. Update model

    @p-offtermatt
    p-offtermatt committed Oct 2, 2023
    Configuration menu
    Copy the full SHA
    e494a09 View commit details
    Browse the repository at this point in the history

  2. Update model for bug reporting]

    @p-offtermatt
    p-offtermatt committed Oct 2, 2023
    Configuration menu
    Copy the full SHA
    289ccad View commit details
    Browse the repository at this point in the history

  3. Remove sanity check script

    @p-offtermatt
    p-offtermatt committed Oct 2, 2023
    Configuration menu
    Copy the full SHA
    45cfc5c View commit details
    Browse the repository at this point in the history

  4. Fix model and randomly run invariant checks

    @p-offtermatt
    p-offtermatt committed Oct 2, 2023
    Configuration menu
    Copy the full SHA
    4fdc2ff View commit details
    Browse the repository at this point in the history

  5. Remove trace

    @p-offtermatt
    p-offtermatt committed Oct 2, 2023
    Configuration menu
    Copy the full SHA
    99744ff View commit details
    Browse the repository at this point in the history

  6. Add model checking to README

    @p-offtermatt
    p-offtermatt committed Oct 2, 2023
    Configuration menu
    Copy the full SHA
    1bc4610 View commit details
    Browse the repository at this point in the history

  7. Add bluespec

    @p-offtermatt
    p-offtermatt committed Oct 2, 2023
    Configuration menu
    Copy the full SHA
    9e4f9c4 View commit details
    Browse the repository at this point in the history

  8. Try fixed bluespec

    @p-offtermatt
    p-offtermatt committed Oct 2, 2023
    Configuration menu
    Copy the full SHA
    ca50ee2 View commit details
    Browse the repository at this point in the history

  9. Fix bluespec definitions

    @p-offtermatt
    p-offtermatt committed Oct 2, 2023
    Configuration menu
    Copy the full SHA
    a80ce70 View commit details
    Browse the repository at this point in the history

Commits on Oct 5, 2023

  1. Update tests/difference/core/quint_model/README.md 

    Co-authored-by: insumity <[email protected]>
    @p-offtermatt @insumity
    p-offtermatt and insumity authored Oct 5, 2023
    Configuration menu
    Copy the full SHA
    918e71a View commit details
    Browse the repository at this point in the history

  2. Update tests/difference/core/quint_model/README.md 

    Co-authored-by: insumity <[email protected]>
    @p-offtermatt @insumity
    p-offtermatt and insumity authored Oct 5, 2023
    Configuration menu
    Copy the full SHA
    8da4cfe View commit details
    Browse the repository at this point in the history

  3. Fix minor issues

    @p-offtermatt
    p-offtermatt committed Oct 5, 2023
    Configuration menu
    Copy the full SHA
    2a68236 View commit details
    Browse the repository at this point in the history

Commits on Oct 6, 2023

  1. Update tests/difference/core/quint_model/README.md 

    Co-authored-by: insumity <[email protected]>
    @p-offtermatt @insumity
    p-offtermatt and insumity authored Oct 6, 2023
    Configuration menu
    Copy the full SHA
    2ad4deb View commit details
    Browse the repository at this point in the history

  2. Update tests/difference/core/quint_model/README.md 

    Co-authored-by: insumity <[email protected]>
    @p-offtermatt @insumity
    p-offtermatt and insumity authored Oct 6, 2023
    Configuration menu
    Copy the full SHA
    9d40842 View commit details
    Browse the repository at this point in the history

  3. Update tests/difference/core/quint_model/README.md 

    Co-authored-by: insumity <[email protected]>
    @p-offtermatt @insumity
    p-offtermatt and insumity authored Oct 6, 2023
    Configuration menu
    Copy the full SHA
    3eeb3fd View commit details
    Browse the repository at this point in the history

  4. Correct verify command by adding \

    @p-offtermatt
    p-offtermatt committed Oct 6, 2023
    Configuration menu
    Copy the full SHA
    2000272 View commit details
    Browse the repository at this point in the history

  5. Add Inv to ValidatorUpdatesArePropagated

    @p-offtermatt
    p-offtermatt committed Oct 6, 2023
    Configuration menu
    Copy the full SHA
    7cd826b View commit details
    Browse the repository at this point in the history

  6. Update tests/difference/core/quint_model/README.md 

    Co-authored-by: insumity <[email protected]>
    @p-offtermatt @insumity
    p-offtermatt and insumity authored Oct 6, 2023
    Configuration menu
    Copy the full SHA
    7df2b1f View commit details
    Browse the repository at this point in the history

Commits on Oct 10, 2023

  1. Apply comments

    @p-offtermatt
    p-offtermatt committed Oct 10, 2023
    Configuration menu
    Copy the full SHA
    3633dc4 View commit details
    Browse the repository at this point in the history

  2. Rename VSC to Vsc

    @p-offtermatt
    p-offtermatt committed Oct 10, 2023
    Configuration menu
    Copy the full SHA
    dc7e687 View commit details
    Browse the repository at this point in the history

  3. Return plain ProtocolState in cases where no error is returned anyways

    @p-offtermatt
    p-offtermatt committed Oct 10, 2023
    Configuration menu
    Copy the full SHA
    728b024 View commit details
    Browse the repository at this point in the history

  4. Remove unused defs

    @p-offtermatt
    p-offtermatt committed Oct 10, 2023
    Configuration menu
    Copy the full SHA
    641d845 View commit details
    Browse the repository at this point in the history

  5. Fix indentation

    @p-offtermatt
    p-offtermatt committed Oct 10, 2023
    Configuration menu
    Copy the full SHA
    c2aa6d0 View commit details
    Browse the repository at this point in the history

  6. Rename to isRunningConsumer

    @p-offtermatt
    p-offtermatt committed Oct 10, 2023
    Configuration menu
    Copy the full SHA
    75b1e11 View commit details
    Browse the repository at this point in the history

  7. Unify naming for extraSpells

    @p-offtermatt
    p-offtermatt committed Oct 10, 2023
    Configuration menu
    Copy the full SHA
    f46554b View commit details
    Browse the repository at this point in the history

  8. Remove HasSubsequence

    @p-offtermatt
    p-offtermatt committed Oct 10, 2023
    Configuration menu
    Copy the full SHA
    3630846 View commit details
    Browse the repository at this point in the history

  9. Run tests before running invariants

    @p-offtermatt
    p-offtermatt committed Oct 10, 2023
    Configuration menu
    Copy the full SHA
    90f6652 View commit details
    Browse the repository at this point in the history

Commits on Oct 11, 2023

  1. Rename modules to have same name as files

    @p-offtermatt
    p-offtermatt committed Oct 11, 2023
    Configuration menu
    Copy the full SHA
    13a32fc View commit details
    Browse the repository at this point in the history

  2. Adjust module name in README and invariant script

    @p-offtermatt
    p-offtermatt committed Oct 11, 2023
    Configuration menu
    Copy the full SHA
    852dac4 View commit details
    Browse the repository at this point in the history

  3. Fix voting power change behaviour around 0

    @p-offtermatt
    p-offtermatt committed Oct 11, 2023
    Configuration menu
    Copy the full SHA
    8aee401 View commit details
    Browse the repository at this point in the history

  4. Adjust error message in test

    @p-offtermatt
    p-offtermatt committed Oct 11, 2023
    Configuration menu
    Copy the full SHA
    d75d5c5 View commit details
    Browse the repository at this point in the history

  5. Remove special treatment of 0 voting power

    @p-offtermatt
    p-offtermatt committed Oct 11, 2023
    Configuration menu
    Copy the full SHA
    f294eec View commit details
    Browse the repository at this point in the history

Commits on Oct 12, 2023

  1. Rename sentVscPackets to sentVscPacketsToConsumer

    @p-offtermatt
    p-offtermatt committed Oct 12, 2023
    Configuration menu
    Copy the full SHA
    4d87372 View commit details
    Browse the repository at this point in the history

  2. Update tests/difference/core/quint_model/README.md 

    Co-authored-by: insumity <[email protected]>
    @p-offtermatt @insumity
    p-offtermatt and insumity authored Oct 12, 2023
    Configuration menu
    Copy the full SHA
    53d5bff View commit details
    Browse the repository at this point in the history

  3. Resolve comments

    @p-offtermatt
    p-offtermatt committed Oct 12, 2023
    Configuration menu
    Copy the full SHA
    738a347 View commit details
    Browse the repository at this point in the history

  4. Merge branch 'ph/quint-model-v2' of https://github.com/cosmos/interch… 

    …ain-security into ph/quint-model-v2
    @p-offtermatt
    p-offtermatt committed Oct 12, 2023
    Configuration menu
    Copy the full SHA
    c7fe7c5 View commit details
    Browse the repository at this point in the history

  5. Adjust comment to fit actual time advancement

    @p-offtermatt
    p-offtermatt committed Oct 12, 2023
    Configuration menu
    Copy the full SHA
    3a03fcd View commit details
    Browse the repository at this point in the history

Commits on Oct 13, 2023

  1. Remove hasError field and make it a function

    @p-offtermatt
    p-offtermatt committed Oct 13, 2023
    Configuration menu
    Copy the full SHA
    d71dad3 View commit details
    Browse the repository at this point in the history

  2. Adjust docstring

    @p-offtermatt
    p-offtermatt committed Oct 13, 2023
    Configuration menu
    Copy the full SHA
    455696a View commit details
    Browse the repository at this point in the history

  3. Remove unused timedout val

    @p-offtermatt
    p-offtermatt committed Oct 13, 2023
    Configuration menu
    Copy the full SHA
    d422cb4 View commit details
    Browse the repository at this point in the history

  4. Update doc

    @p-offtermatt
    p-offtermatt committed Oct 13, 2023
    Configuration menu
    Copy the full SHA
    6ed82c8 View commit details
    Browse the repository at this point in the history

Commits on Oct 16, 2023

  1. Rename statemachine to model

    @p-offtermatt
    p-offtermatt committed Oct 16, 2023
    Configuration menu
    Copy the full SHA
    b817f43 View commit details
    Browse the repository at this point in the history

  2. Use ... syntax

    @p-offtermatt
    p-offtermatt committed Oct 16, 2023
    Configuration menu
    Copy the full SHA
    70cd774 View commit details
    Browse the repository at this point in the history

  3. Change Error type to string

    @p-offtermatt
    p-offtermatt committed Oct 16, 2023
    Configuration menu
    Copy the full SHA
    86324b7 View commit details
    Browse the repository at this point in the history

Commits on Oct 19, 2023

  1. Start adding mbt using Quint model

    @p-offtermatt
    p-offtermatt committed Oct 19, 2023
    Configuration menu
    Copy the full SHA
    b856081 View commit details
    Browse the repository at this point in the history

  2. Merge branch 'main' into ph/mbt

    @p-offtermatt
    p-offtermatt committed Oct 19, 2023
    Configuration menu
    Copy the full SHA
    234a89e View commit details
    Browse the repository at this point in the history