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

Update example runner + dashboard for lightclient spec #1079

Merged
merged 4 commits into from
Jul 31, 2023
Merged

Update example runner + dashboard for lightclient spec #1079

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
4 commits
Select commit Hold shift + click to select a range
23a7876
Mark parameterized modules as N/A in dashboard
thpani Jul 26, 2023
01f9637
Fix verify args for lightclient spec
thpani Jul 27, 2023
8145fc0
Add instance to Lightclient spec
thpani Jul 28, 2023
a0c92a3
Add --main for Lightclient.qnt
thpani Jul 28, 2023
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
16 changes: 13 additions & 3 deletions examples/.scripts/run-example.sh
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -13,8 +13,16 @@ result () {
local args="$2"
local file="$3"

# Skip tests for parameterized modules
if [[ "$cmd" == "test" && (
"$file" == "cosmos/lightclient/Blockchain.qnt" ||
"$file" == "cosmos/lightclient/LCVerificationApi.qnt" ) ]] ; then
printf "N/A[^parameterized]"; return
fi
# Skip verification for specs that do not define a state machine
if [[ "$cmd" == "verify" && (
"$file" == "cosmos/lightclient/Blockchain.qnt" ||
"$file" == "cosmos/lightclient/LCVerificationApi.qnt" ||
"$file" == "cosmos/lightclient/typedefs.qnt" ||
"$file" =~ ^spells/ ||
"$file" == "solidity/SimpleAuction/SimpleAuction.qnt" ||
Expand Down Expand Up @@ -71,6 +79,8 @@ get_main () {
main="--main=properChannelsTests"
elif [[ "$file" == "cosmos/ics20/ics20.qnt" ]] ; then
main="--main=ics20Test"
elif [[ "$file" == "cosmos/lightclient/Lightclient.qnt" ]] ; then
main="--main=Lightclient_4_3_correct"
elif [[ "$file" == "puzzles/prisoners/prisoners.qnt" ]] ; then
main="--main=prisoners3"
elif [[ "$file" == "solidity/ERC20/erc20.qnt" ]] ; then
Expand All @@ -95,9 +105,9 @@ get_test_args () {
get_verify_args () {
local file="$1"
local args=""
if [[ "$file" == "classic/distributed/LamportMutex/LamportMutex.qnt" ]] ; then
args="--init=Init --step=Next"
elif [[ "$file" == "classic/distributed/ReadersWriters/ReadersWriters.qnt" ]] ; then
if [[ "$file" == "classic/distributed/LamportMutex/LamportMutex.qnt" ||
"$file" == "classic/distributed/ReadersWriters/ReadersWriters.qnt" ||
"$file" == "cosmos/lightclient/Lightclient.qnt" ]] ; then
args="--init=Init --step=Next"
fi
echo "${args}"
Expand Down
1 change: 1 addition & 0 deletions examples/.scripts/run-examples.sh
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -25,3 +25,4 @@ find . -name "*.qnt" | cut -c3- | parallel "${SCRIPT_DIR}/run-example.sh" | env

echo
echo "[^nostatemachine]: This specification does not define a state machine."
echo "[^parameterized]: This specification is parameterized, and instantiated in another module."
5 changes: 3 additions & 2 deletions examples/README.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -60,8 +60,8 @@ listed without any additional command line arguments.
| [cosmos/ics20/denomTrace.qnt](./cosmos/ics20/denomTrace.qnt) | :white_check_mark: | :white_check_mark: | :white_check_mark: | :white_check_mark: |
| [cosmos/ics20/ics20.qnt](./cosmos/ics20/ics20.qnt) | :white_check_mark: | :white_check_mark: | :white_check_mark: | :x:<sup>https://github.com/informalsystems/quint/issues/693</sup> |
| [cosmos/ics23/ics23.qnt](./cosmos/ics23/ics23.qnt) | :white_check_mark: | :white_check_mark: | :white_check_mark: | :x:<sup>https://github.com/informalsystems/quint/issues/693,</sup><sup>https://github.com/informalsystems/quint/pull/975</sup> |
| [cosmos/lightclient/Blockchain.qnt](./cosmos/lightclient/Blockchain.qnt) | :white_check_mark: | :white_check_mark: | :x: | :x: |
| [cosmos/lightclient/LCVerificationApi.qnt](./cosmos/lightclient/LCVerificationApi.qnt) | :white_check_mark: | :white_check_mark: | :x: | :x: |
| [cosmos/lightclient/Blockchain.qnt](./cosmos/lightclient/Blockchain.qnt) | :white_check_mark: | :white_check_mark: | N/A[^parameterized] | N/A[^nostatemachine] |
| [cosmos/lightclient/LCVerificationApi.qnt](./cosmos/lightclient/LCVerificationApi.qnt) | :white_check_mark: | :white_check_mark: | N/A[^parameterized] | N/A[^nostatemachine] |
| [cosmos/lightclient/Lightclient.qnt](./cosmos/lightclient/Lightclient.qnt) | :white_check_mark: | :white_check_mark: | :x: | :x: |
| [cosmos/lightclient/typedefs.qnt](./cosmos/lightclient/typedefs.qnt) | :white_check_mark: | :white_check_mark: | :white_check_mark: | N/A[^nostatemachine] |
| [cosmos/tendermint/TendermintAcc005.qnt](./cosmos/tendermint/TendermintAcc005.qnt) | :white_check_mark: | :white_check_mark: | :x:<sup>https://github.com/informalsystems/quint/pull/1023</sup> | :x:<sup>https://github.com/informalsystems/quint/pull/1023</sup> |
Expand Down Expand Up @@ -95,3 +95,4 @@ listed without any additional command line arguments.
| [verification/defaultOpNames.qnt](./verification/defaultOpNames.qnt) | :white_check_mark: | :white_check_mark: | :white_check_mark: | :white_check_mark: |

[^nostatemachine]: This specification does not define a state machine.
[^parameterized]: This specification is parameterized, and instantiated in another module.
13 changes: 13 additions & 0 deletions examples/cosmos/lightclient/Lightclient.qnt
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -545,3 +545,16 @@ module Lightclient {
the algorithm has indeed terminated there.
*/
}

module Lightclient_4_3_correct {
import Lightclient(
AllNodes = Set("n1", "n2", "n3", "n4"),
TRUSTED_HEIGHT = 1,
TARGET_HEIGHT = 3,
TRUSTING_PERIOD = 1400, // two weeks, one day is 100 time units :-)
CLOCK_DRIFT = 10, // how much we assume the local clock is drifting
REAL_CLOCK_DRIFT = 3, // how much the local clock is actually drifting
IS_PRIMARY_CORRECT = true,
FAULTY_RATIO = (1, 3) // < 1/3 faulty validators
).*
}
Loading