From 2f61fefc403a42c35cb1d5f59c8cfddafca7931a Mon Sep 17 00:00:00 2001 From: BRonen Date: Wed, 31 Dec 2025 11:54:57 -0300 Subject: [PATCH 1/3] feat: quint initial setup --- .gitignore | 1 + flake.nix | 7 + package-lock.json | 1008 +++++++++++++++++++++++++++++++++++++++++++++ package.json | 5 + spec/raft.qnt | 188 +++++++++ 5 files changed, 1209 insertions(+) create mode 100644 package-lock.json create mode 100644 package.json create mode 100644 spec/raft.qnt diff --git a/.gitignore b/.gitignore index 0765ae8..8e50aa1 100644 --- a/.gitignore +++ b/.gitignore @@ -3,6 +3,7 @@ kotlinc/ .kotlin/ **/build/ *.log +node_modules/ # Ignore Gradle project-specific cache directory .gradle diff --git a/flake.nix b/flake.nix index 4e4ca0a..5bb0e57 100644 --- a/flake.nix +++ b/flake.nix @@ -29,6 +29,11 @@ }; devShells.default = pkgs.mkShell { buildInputs = [ + # Quint Spec Deps + pkgs.quint + pkgs.nodejs + + # Dev Deps pkgs.gradle pkgs.openjdk21 pkgs.kotlin @@ -38,6 +43,8 @@ shellHook = '' export GRADLE_USER_HOME="$PWD/.gradle" + export PATH="$PATH:$(pwd)/node_modules/.bin" + npm install @informalsystems/quint-language-server -D ''; }; }); diff --git a/package-lock.json b/package-lock.json new file mode 100644 index 0000000..4f8387d --- /dev/null +++ b/package-lock.json @@ -0,0 +1,1008 @@ +{ + "name": "archon", + "lockfileVersion": 3, + "requires": true, + "packages": { + "": { + "devDependencies": { + "@informalsystems/quint-language-server": "^0.17.0" + } + }, + "node_modules/@grpc/grpc-js": { + "version": "1.14.3", + "resolved": "https://registry.npmjs.org/@grpc/grpc-js/-/grpc-js-1.14.3.tgz", + "integrity": "sha512-Iq8QQQ/7X3Sac15oB6p0FmUg/klxQvXLeileoqrTRGJYLV+/9tubbr9ipz0GKHjmXVsgFPo/+W+2cA8eNcR+XA==", + "dev": true, + "license": "Apache-2.0", + "dependencies": { + "@grpc/proto-loader": "^0.8.0", + "@js-sdsl/ordered-map": "^4.4.2" + }, + "engines": { + "node": ">=12.10.0" + } + }, + "node_modules/@grpc/grpc-js/node_modules/@grpc/proto-loader": { + "version": "0.8.0", + "resolved": "https://registry.npmjs.org/@grpc/proto-loader/-/proto-loader-0.8.0.tgz", + "integrity": "sha512-rc1hOQtjIWGxcxpb9aHAfLpIctjEnsDehj0DAiVfBlmT84uvR0uUtN2hEi/ecvWVjXUGf5qPF4qEgiLOx1YIMQ==", + "dev": true, + "license": "Apache-2.0", + "dependencies": { + "lodash.camelcase": "^4.3.0", + "long": "^5.0.0", + "protobufjs": "^7.5.3", + "yargs": "^17.7.2" + }, + "bin": { + "proto-loader-gen-types": "build/bin/proto-loader-gen-types.js" + }, + "engines": { + "node": ">=6" + } + }, + "node_modules/@grpc/proto-loader": { + "version": "0.7.15", + "resolved": "https://registry.npmjs.org/@grpc/proto-loader/-/proto-loader-0.7.15.tgz", + "integrity": "sha512-tMXdRCfYVixjuFK+Hk0Q1s38gV9zDiDJfWL3h1rv4Qc39oILCu1TRTDt7+fGUI8K4G1Fj125Hx/ru3azECWTyQ==", + "dev": true, + "license": "Apache-2.0", + "dependencies": { + "lodash.camelcase": "^4.3.0", + "long": "^5.0.0", + "protobufjs": "^7.2.5", + "yargs": "^17.7.2" + }, + "bin": { + "proto-loader-gen-types": "build/bin/proto-loader-gen-types.js" + }, + "engines": { + "node": ">=6" + } + }, + "node_modules/@informalsystems/quint": { + "version": "0.27.0", + "resolved": "https://registry.npmjs.org/@informalsystems/quint/-/quint-0.27.0.tgz", + "integrity": "sha512-zYGiwpJh7xgdtKhdJ5xYJ7IyagD+WEFBz8ZCP4kHVK6UZ8IElDW7LRfd4Hf7alWGVq5hGC9gSWmoWUOe4tQ6Lg==", + "dev": true, + "license": "Apache 2.0", + "dependencies": { + "@grpc/grpc-js": "^1.11.1", + "@grpc/proto-loader": "^0.7.7", + "@octokit/request": "^8.1.1", + "@sweet-monads/either": "~3.2.0", + "@sweet-monads/maybe": "~3.2.0", + "@types/line-column": "^1.0.0", + "@types/lodash.clonedeep": "4.5.0", + "@types/seedrandom": "^3.0.4", + "adm-zip": "^0.5.16", + "antlr4ts": "^0.5.0-alpha.4", + "chalk": "^4.1.2", + "cli-progress": "^3.12.0", + "cross-spawn": "^7.0.6", + "eol": "^0.9.1", + "immutable": "^4.3.0", + "json-bigint": "^1.0.0", + "line-column": "^1.0.2", + "lodash": "^4.17.21", + "lodash.clonedeep": "4.5.0", + "lodash.isequal": "^4.5.0", + "seedrandom": "^3.0.5", + "tar": "^6.1.14", + "yargs": "^17.7.2" + }, + "bin": { + "quint": "dist/src/cli.js" + }, + "engines": { + "node": ">=18" + } + }, + "node_modules/@informalsystems/quint-language-server": { + "version": "0.17.0", + "resolved": "https://registry.npmjs.org/@informalsystems/quint-language-server/-/quint-language-server-0.17.0.tgz", + "integrity": "sha512-4HxFKaw6S0xSCwXweybshNQi/NnqiXsIqXSrGhZk2vJ1cktxqhQGH2M/wA95JjGvPO/Rd/27Fh1S2BHiDz36Jg==", + "dev": true, + "license": "Apache 2.0", + "dependencies": { + "@informalsystems/quint": "^0.27.0", + "json-bigint": "^1.0.0", + "vscode-languageserver": "^7.0.0", + "vscode-languageserver-textdocument": "^1.0.1", + "vscode-uri": "^3.0.7" + }, + "bin": { + "quint-language-server": "out/src/server.js" + }, + "engines": { + "node": ">=18" + } + }, + "node_modules/@js-sdsl/ordered-map": { + "version": "4.4.2", + "resolved": "https://registry.npmjs.org/@js-sdsl/ordered-map/-/ordered-map-4.4.2.tgz", + "integrity": "sha512-iUKgm52T8HOE/makSxjqoWhe95ZJA1/G1sYsGev2JDKUSS14KAgg1LHb+Ba+IPow0xflbnSkOsZcO08C7w1gYw==", + "dev": true, + "license": "MIT", + "funding": { + "type": "opencollective", + "url": "https://opencollective.com/js-sdsl" + } + }, + "node_modules/@octokit/endpoint": { + "version": "9.0.6", + "resolved": "https://registry.npmjs.org/@octokit/endpoint/-/endpoint-9.0.6.tgz", + "integrity": "sha512-H1fNTMA57HbkFESSt3Y9+FBICv+0jFceJFPWDePYlR/iMGrwM5ph+Dd4XRQs+8X+PUFURLQgX9ChPfhJ/1uNQw==", + "dev": true, + "license": "MIT", + "dependencies": { + "@octokit/types": "^13.1.0", + "universal-user-agent": "^6.0.0" + }, + "engines": { + "node": ">= 18" + } + }, + "node_modules/@octokit/openapi-types": { + "version": "24.2.0", + "resolved": "https://registry.npmjs.org/@octokit/openapi-types/-/openapi-types-24.2.0.tgz", + "integrity": "sha512-9sIH3nSUttelJSXUrmGzl7QUBFul0/mB8HRYl3fOlgHbIWG+WnYDXU3v/2zMtAvuzZ/ed00Ei6on975FhBfzrg==", + "dev": true, + "license": "MIT" + }, + "node_modules/@octokit/request": { + "version": "8.4.1", + "resolved": "https://registry.npmjs.org/@octokit/request/-/request-8.4.1.tgz", + "integrity": "sha512-qnB2+SY3hkCmBxZsR/MPCybNmbJe4KAlfWErXq+rBKkQJlbjdJeS85VI9r8UqeLYLvnAenU8Q1okM/0MBsAGXw==", + "dev": true, + "license": "MIT", + "dependencies": { + "@octokit/endpoint": "^9.0.6", + "@octokit/request-error": "^5.1.1", + "@octokit/types": "^13.1.0", + "universal-user-agent": "^6.0.0" + }, + "engines": { + "node": ">= 18" + } + }, + "node_modules/@octokit/request-error": { + "version": "5.1.1", + "resolved": "https://registry.npmjs.org/@octokit/request-error/-/request-error-5.1.1.tgz", + "integrity": "sha512-v9iyEQJH6ZntoENr9/yXxjuezh4My67CBSu9r6Ve/05Iu5gNgnisNWOsoJHTP6k0Rr0+HQIpnH+kyammu90q/g==", + "dev": true, + "license": "MIT", + "dependencies": { + "@octokit/types": "^13.1.0", + "deprecation": "^2.0.0", + "once": "^1.4.0" + }, + "engines": { + "node": ">= 18" + } + }, + "node_modules/@octokit/types": { + "version": "13.10.0", + "resolved": "https://registry.npmjs.org/@octokit/types/-/types-13.10.0.tgz", + "integrity": "sha512-ifLaO34EbbPj0Xgro4G5lP5asESjwHracYJvVaPIyXMuiuXLlhic3S47cBdTb+jfODkTE5YtGCLt3Ay3+J97sA==", + "dev": true, + "license": "MIT", + "dependencies": { + "@octokit/openapi-types": "^24.2.0" + } + }, + "node_modules/@protobufjs/aspromise": { + "version": "1.1.2", + "resolved": "https://registry.npmjs.org/@protobufjs/aspromise/-/aspromise-1.1.2.tgz", + "integrity": "sha512-j+gKExEuLmKwvz3OgROXtrJ2UG2x8Ch2YZUxahh+s1F2HZ+wAceUNLkvy6zKCPVRkU++ZWQrdxsUeQXmcg4uoQ==", + "dev": true, + "license": "BSD-3-Clause" + }, + "node_modules/@protobufjs/base64": { + "version": "1.1.2", + "resolved": "https://registry.npmjs.org/@protobufjs/base64/-/base64-1.1.2.tgz", + "integrity": "sha512-AZkcAA5vnN/v4PDqKyMR5lx7hZttPDgClv83E//FMNhR2TMcLUhfRUBHCmSl0oi9zMgDDqRUJkSxO3wm85+XLg==", + "dev": true, + "license": "BSD-3-Clause" + }, + "node_modules/@protobufjs/codegen": { + "version": "2.0.4", + "resolved": "https://registry.npmjs.org/@protobufjs/codegen/-/codegen-2.0.4.tgz", + "integrity": "sha512-YyFaikqM5sH0ziFZCN3xDC7zeGaB/d0IUb9CATugHWbd1FRFwWwt4ld4OYMPWu5a3Xe01mGAULCdqhMlPl29Jg==", + "dev": true, + "license": "BSD-3-Clause" + }, + "node_modules/@protobufjs/eventemitter": { + "version": "1.1.0", + "resolved": "https://registry.npmjs.org/@protobufjs/eventemitter/-/eventemitter-1.1.0.tgz", + "integrity": "sha512-j9ednRT81vYJ9OfVuXG6ERSTdEL1xVsNgqpkxMsbIabzSo3goCjDIveeGv5d03om39ML71RdmrGNjG5SReBP/Q==", + "dev": true, + "license": "BSD-3-Clause" + }, + "node_modules/@protobufjs/fetch": { + "version": "1.1.0", + "resolved": "https://registry.npmjs.org/@protobufjs/fetch/-/fetch-1.1.0.tgz", + "integrity": "sha512-lljVXpqXebpsijW71PZaCYeIcE5on1w5DlQy5WH6GLbFryLUrBD4932W/E2BSpfRJWseIL4v/KPgBFxDOIdKpQ==", + "dev": true, + "license": "BSD-3-Clause", + "dependencies": { + "@protobufjs/aspromise": "^1.1.1", + "@protobufjs/inquire": "^1.1.0" + } + }, + "node_modules/@protobufjs/float": { + "version": "1.0.2", + "resolved": "https://registry.npmjs.org/@protobufjs/float/-/float-1.0.2.tgz", + "integrity": "sha512-Ddb+kVXlXst9d+R9PfTIxh1EdNkgoRe5tOX6t01f1lYWOvJnSPDBlG241QLzcyPdoNTsblLUdujGSE4RzrTZGQ==", + "dev": true, + "license": "BSD-3-Clause" + }, + "node_modules/@protobufjs/inquire": { + "version": "1.1.0", + "resolved": "https://registry.npmjs.org/@protobufjs/inquire/-/inquire-1.1.0.tgz", + "integrity": "sha512-kdSefcPdruJiFMVSbn801t4vFK7KB/5gd2fYvrxhuJYg8ILrmn9SKSX2tZdV6V+ksulWqS7aXjBcRXl3wHoD9Q==", + "dev": true, + "license": "BSD-3-Clause" + }, + "node_modules/@protobufjs/path": { + "version": "1.1.2", + "resolved": "https://registry.npmjs.org/@protobufjs/path/-/path-1.1.2.tgz", + "integrity": "sha512-6JOcJ5Tm08dOHAbdR3GrvP+yUUfkjG5ePsHYczMFLq3ZmMkAD98cDgcT2iA1lJ9NVwFd4tH/iSSoe44YWkltEA==", + "dev": true, + "license": "BSD-3-Clause" + }, + "node_modules/@protobufjs/pool": { + "version": "1.1.0", + "resolved": "https://registry.npmjs.org/@protobufjs/pool/-/pool-1.1.0.tgz", + "integrity": "sha512-0kELaGSIDBKvcgS4zkjz1PeddatrjYcmMWOlAuAPwAeccUrPHdUqo/J6LiymHHEiJT5NrF1UVwxY14f+fy4WQw==", + "dev": true, + "license": "BSD-3-Clause" + }, + "node_modules/@protobufjs/utf8": { + "version": "1.1.0", + "resolved": "https://registry.npmjs.org/@protobufjs/utf8/-/utf8-1.1.0.tgz", + "integrity": "sha512-Vvn3zZrhQZkkBE8LSuW3em98c0FwgO4nxzv6OdSxPKJIEKY2bGbHn+mhGIPerzI4twdxaP8/0+06HBpwf345Lw==", + "dev": true, + "license": "BSD-3-Clause" + }, + "node_modules/@sweet-monads/either": { + "version": "3.2.0", + "resolved": "https://registry.npmjs.org/@sweet-monads/either/-/either-3.2.0.tgz", + "integrity": "sha512-n+nR0b60GRTKb+D76qhTf4NEBXU9zfpigYYEtKtSYbV+5+i5gxr9jFd64pYkY2O7hVsb/G7nspbAeFni/i1ltA==", + "dev": true, + "license": "MIT", + "dependencies": { + "@sweet-monads/interfaces": "^3.2.0" + } + }, + "node_modules/@sweet-monads/interfaces": { + "version": "3.3.0", + "resolved": "https://registry.npmjs.org/@sweet-monads/interfaces/-/interfaces-3.3.0.tgz", + "integrity": "sha512-66akGvjPD4lizQy+w4JSltJilc2w/QPdw8lPAniLJGHwyjmrw9xMJLx76Q/GDnbCU59Werses4aZJLWOlJrL5A==", + "dev": true, + "license": "MIT" + }, + "node_modules/@sweet-monads/maybe": { + "version": "3.2.0", + "resolved": "https://registry.npmjs.org/@sweet-monads/maybe/-/maybe-3.2.0.tgz", + "integrity": "sha512-/t+K0D/kBfkYOkZaePEsrK868at0M9UIEVgehcM0xscrCSZhKWGteE41vl2XJQqh8WyiFo/mZ5y7eAPSYzS+pg==", + "dev": true, + "license": "MIT", + "dependencies": { + "@sweet-monads/interfaces": "^3.2.0" + } + }, + "node_modules/@types/line-column": { + "version": "1.0.2", + "resolved": "https://registry.npmjs.org/@types/line-column/-/line-column-1.0.2.tgz", + "integrity": "sha512-099oFQmp/Tlf20xW5XI5R4F69N6lF/zQ09XDzc3R5BOLFlqIotgKoNIyj0HD4fQLWcGDreDJv8k/BkLJscrDrw==", + "dev": true, + "license": "MIT" + }, + "node_modules/@types/lodash": { + "version": "4.17.21", + "resolved": "https://registry.npmjs.org/@types/lodash/-/lodash-4.17.21.tgz", + "integrity": "sha512-FOvQ0YPD5NOfPgMzJihoT+Za5pdkDJWcbpuj1DjaKZIr/gxodQjY/uWEFlTNqW2ugXHUiL8lRQgw63dzKHZdeQ==", + "dev": true, + "license": "MIT" + }, + "node_modules/@types/lodash.clonedeep": { + "version": "4.5.0", + "resolved": "https://registry.npmjs.org/@types/lodash.clonedeep/-/lodash.clonedeep-4.5.0.tgz", + "integrity": "sha512-IHijjFVPJTvzvrNPz+6nQy5lZQb7uh807RfTIEaQBrZXrIGjZy0L2dEb3hju34J0eqbXLCY6Hub/g81Jl4pGCA==", + "dev": true, + "license": "MIT", + "dependencies": { + "@types/lodash": "*" + } + }, + "node_modules/@types/node": { + "version": "25.0.3", + "resolved": "https://registry.npmjs.org/@types/node/-/node-25.0.3.tgz", + "integrity": "sha512-W609buLVRVmeW693xKfzHeIV6nJGGz98uCPfeXI1ELMLXVeKYZ9m15fAMSaUPBHYLGFsVRcMmSCksQOrZV9BYA==", + "dev": true, + "license": "MIT", + "dependencies": { + "undici-types": "~7.16.0" + } + }, + "node_modules/@types/seedrandom": { + "version": "3.0.8", + "resolved": "https://registry.npmjs.org/@types/seedrandom/-/seedrandom-3.0.8.tgz", + "integrity": "sha512-TY1eezMU2zH2ozQoAFAQFOPpvP15g+ZgSfTZt31AUUH/Rxtnz3H+A/Sv1Snw2/amp//omibc+AEkTaA8KUeOLQ==", + "dev": true, + "license": "MIT" + }, + "node_modules/adm-zip": { + "version": "0.5.16", + "resolved": "https://registry.npmjs.org/adm-zip/-/adm-zip-0.5.16.tgz", + "integrity": "sha512-TGw5yVi4saajsSEgz25grObGHEUaDrniwvA2qwSC060KfqGPdglhvPMA2lPIoxs3PQIItj2iag35fONcQqgUaQ==", + "dev": true, + "license": "MIT", + "engines": { + "node": ">=12.0" + } + }, + "node_modules/ansi-regex": { + "version": "5.0.1", + "resolved": "https://registry.npmjs.org/ansi-regex/-/ansi-regex-5.0.1.tgz", + "integrity": "sha512-quJQXlTSUGL2LH9SUXo8VwsY4soanhgo6LNSm84E1LBcE8s3O0wpdiRzyR9z/ZZJMlMWv37qOOb9pdJlMUEKFQ==", + "dev": true, + "license": "MIT", + "engines": { + "node": ">=8" + } + }, + "node_modules/ansi-styles": { + "version": "4.3.0", + "resolved": "https://registry.npmjs.org/ansi-styles/-/ansi-styles-4.3.0.tgz", + "integrity": "sha512-zbB9rCJAT1rbjiVDb2hqKFHNYLxgtk8NURxZ3IZwD3F6NtxbXZQCnnSi1Lkx+IDohdPlFp222wVALIheZJQSEg==", + "dev": true, + "license": "MIT", + "dependencies": { + "color-convert": "^2.0.1" + }, + "engines": { + "node": ">=8" + }, + "funding": { + "url": "https://github.com/chalk/ansi-styles?sponsor=1" + } + }, + "node_modules/antlr4ts": { + "version": "0.5.0-alpha.4", + "resolved": "https://registry.npmjs.org/antlr4ts/-/antlr4ts-0.5.0-alpha.4.tgz", + "integrity": "sha512-WPQDt1B74OfPv/IMS2ekXAKkTZIHl88uMetg6q3OTqgFxZ/dxDXI0EWLyZid/1Pe6hTftyg5N7gel5wNAGxXyQ==", + "dev": true, + "license": "BSD-3-Clause" + }, + "node_modules/bignumber.js": { + "version": "9.3.1", + "resolved": "https://registry.npmjs.org/bignumber.js/-/bignumber.js-9.3.1.tgz", + "integrity": "sha512-Ko0uX15oIUS7wJ3Rb30Fs6SkVbLmPBAKdlm7q9+ak9bbIeFf0MwuBsQV6z7+X768/cHsfg+WlysDWJcmthjsjQ==", + "dev": true, + "license": "MIT", + "engines": { + "node": "*" + } + }, + "node_modules/chalk": { + "version": "4.1.2", + "resolved": "https://registry.npmjs.org/chalk/-/chalk-4.1.2.tgz", + "integrity": "sha512-oKnbhFyRIXpUuez8iBMmyEa4nbj4IOQyuhc/wy9kY7/WVPcwIO9VA668Pu8RkO7+0G76SLROeyw9CpQ061i4mA==", + "dev": true, + "license": "MIT", + "dependencies": { + "ansi-styles": "^4.1.0", + "supports-color": "^7.1.0" + }, + "engines": { + "node": ">=10" + }, + "funding": { + "url": "https://github.com/chalk/chalk?sponsor=1" + } + }, + "node_modules/chownr": { + "version": "2.0.0", + "resolved": "https://registry.npmjs.org/chownr/-/chownr-2.0.0.tgz", + "integrity": "sha512-bIomtDF5KGpdogkLd9VspvFzk9KfpyyGlS8YFVZl7TGPBHL5snIOnxeshwVgPteQ9b4Eydl+pVbIyE1DcvCWgQ==", + "dev": true, + "license": "ISC", + "engines": { + "node": ">=10" + } + }, + "node_modules/cli-progress": { + "version": "3.12.0", + "resolved": "https://registry.npmjs.org/cli-progress/-/cli-progress-3.12.0.tgz", + "integrity": "sha512-tRkV3HJ1ASwm19THiiLIXLO7Im7wlTuKnvkYaTkyoAPefqjNg7W7DHKUlGRxy9vxDvbyCYQkQozvptuMkGCg8A==", + "dev": true, + "license": "MIT", + "dependencies": { + "string-width": "^4.2.3" + }, + "engines": { + "node": ">=4" + } + }, + "node_modules/cliui": { + "version": "8.0.1", + "resolved": "https://registry.npmjs.org/cliui/-/cliui-8.0.1.tgz", + "integrity": "sha512-BSeNnyus75C4//NQ9gQt1/csTXyo/8Sb+afLAkzAptFuMsod9HFokGNudZpi/oQV73hnVK+sR+5PVRMd+Dr7YQ==", + "dev": true, + "license": "ISC", + "dependencies": { + "string-width": "^4.2.0", + "strip-ansi": "^6.0.1", + "wrap-ansi": "^7.0.0" + }, + "engines": { + "node": ">=12" + } + }, + "node_modules/color-convert": { + "version": "2.0.1", + "resolved": "https://registry.npmjs.org/color-convert/-/color-convert-2.0.1.tgz", + "integrity": "sha512-RRECPsj7iu/xb5oKYcsFHSppFNnsj/52OVTRKb4zP5onXwVF3zVmmToNcOfGC+CRDpfK/U584fMg38ZHCaElKQ==", + "dev": true, + "license": "MIT", + "dependencies": { + "color-name": "~1.1.4" + }, + "engines": { + "node": ">=7.0.0" + } + }, + "node_modules/color-name": { + "version": "1.1.4", + "resolved": "https://registry.npmjs.org/color-name/-/color-name-1.1.4.tgz", + "integrity": "sha512-dOy+3AuW3a2wNbZHIuMZpTcgjGuLU/uBL/ubcZF9OXbDo8ff4O8yVp5Bf0efS8uEoYo5q4Fx7dY9OgQGXgAsQA==", + "dev": true, + "license": "MIT" + }, + "node_modules/cross-spawn": { + "version": "7.0.6", + "resolved": "https://registry.npmjs.org/cross-spawn/-/cross-spawn-7.0.6.tgz", + "integrity": "sha512-uV2QOWP2nWzsy2aMp8aRibhi9dlzF5Hgh5SHaB9OiTGEyDTiJJyx0uy51QXdyWbtAHNua4XJzUKca3OzKUd3vA==", + "dev": true, + "license": "MIT", + "dependencies": { + "path-key": "^3.1.0", + "shebang-command": "^2.0.0", + "which": "^2.0.1" + }, + "engines": { + "node": ">= 8" + } + }, + "node_modules/deprecation": { + "version": "2.3.1", + "resolved": "https://registry.npmjs.org/deprecation/-/deprecation-2.3.1.tgz", + "integrity": "sha512-xmHIy4F3scKVwMsQ4WnVaS8bHOx0DmVwRywosKhaILI0ywMDWPtBSku2HNxRvF7jtwDRsoEwYQSfbxj8b7RlJQ==", + "dev": true, + "license": "ISC" + }, + "node_modules/emoji-regex": { + "version": "8.0.0", + "resolved": "https://registry.npmjs.org/emoji-regex/-/emoji-regex-8.0.0.tgz", + "integrity": "sha512-MSjYzcWNOA0ewAHpz0MxpYFvwg6yjy1NG3xteoqz644VCo/RPgnr1/GGt+ic3iJTzQ8Eu3TdM14SawnVUmGE6A==", + "dev": true, + "license": "MIT" + }, + "node_modules/eol": { + "version": "0.9.1", + "resolved": "https://registry.npmjs.org/eol/-/eol-0.9.1.tgz", + "integrity": "sha512-Ds/TEoZjwggRoz/Q2O7SE3i4Jm66mqTDfmdHdq/7DKVk3bro9Q8h6WdXKdPqFLMoqxrDK5SVRzHVPOS6uuGtrg==", + "dev": true, + "license": "MIT" + }, + "node_modules/escalade": { + "version": "3.2.0", + "resolved": "https://registry.npmjs.org/escalade/-/escalade-3.2.0.tgz", + "integrity": "sha512-WUj2qlxaQtO4g6Pq5c29GTcWGDyd8itL8zTlipgECz3JesAiiOKotd8JU6otB3PACgG6xkJUyVhboMS+bje/jA==", + "dev": true, + "license": "MIT", + "engines": { + "node": ">=6" + } + }, + "node_modules/fs-minipass": { + "version": "2.1.0", + "resolved": "https://registry.npmjs.org/fs-minipass/-/fs-minipass-2.1.0.tgz", + "integrity": "sha512-V/JgOLFCS+R6Vcq0slCuaeWEdNC3ouDlJMNIsacH2VtALiu9mV4LPrHc5cDl8k5aw6J8jwgWWpiTo5RYhmIzvg==", + "dev": true, + "license": "ISC", + "dependencies": { + "minipass": "^3.0.0" + }, + "engines": { + "node": ">= 8" + } + }, + "node_modules/fs-minipass/node_modules/minipass": { + "version": "3.3.6", + "resolved": "https://registry.npmjs.org/minipass/-/minipass-3.3.6.tgz", + "integrity": "sha512-DxiNidxSEK+tHG6zOIklvNOwm3hvCrbUrdtzY74U6HKTJxvIDfOUL5W5P2Ghd3DTkhhKPYGqeNUIh5qcM4YBfw==", + "dev": true, + "license": "ISC", + "dependencies": { + "yallist": "^4.0.0" + }, + "engines": { + "node": ">=8" + } + }, + "node_modules/get-caller-file": { + "version": "2.0.5", + "resolved": "https://registry.npmjs.org/get-caller-file/-/get-caller-file-2.0.5.tgz", + "integrity": "sha512-DyFP3BM/3YHTQOCUL/w0OZHR0lpKeGrxotcHWcqNEdnltqFwXVfhEBQ94eIo34AfQpo0rGki4cyIiftY06h2Fg==", + "dev": true, + "license": "ISC", + "engines": { + "node": "6.* || 8.* || >= 10.*" + } + }, + "node_modules/has-flag": { + "version": "4.0.0", + "resolved": "https://registry.npmjs.org/has-flag/-/has-flag-4.0.0.tgz", + "integrity": "sha512-EykJT/Q1KjTWctppgIAgfSO0tKVuZUjhgMr17kqTumMl6Afv3EISleU7qZUzoXDFTAHTDC4NOoG/ZxU3EvlMPQ==", + "dev": true, + "license": "MIT", + "engines": { + "node": ">=8" + } + }, + "node_modules/immutable": { + "version": "4.3.7", + "resolved": "https://registry.npmjs.org/immutable/-/immutable-4.3.7.tgz", + "integrity": "sha512-1hqclzwYwjRDFLjcFxOM5AYkkG0rpFPpr1RLPMEuGczoS7YA8gLhy8SWXYRAA/XwfEHpfo3cw5JGioS32fnMRw==", + "dev": true, + "license": "MIT" + }, + "node_modules/is-fullwidth-code-point": { + "version": "3.0.0", + "resolved": "https://registry.npmjs.org/is-fullwidth-code-point/-/is-fullwidth-code-point-3.0.0.tgz", + "integrity": "sha512-zymm5+u+sCsSWyD9qNaejV3DFvhCKclKdizYaJUuHA83RLjb7nSuGnddCHGv0hk+KY7BMAlsWeK4Ueg6EV6XQg==", + "dev": true, + "license": "MIT", + "engines": { + "node": ">=8" + } + }, + "node_modules/isarray": { + "version": "1.0.0", + "resolved": "https://registry.npmjs.org/isarray/-/isarray-1.0.0.tgz", + "integrity": "sha512-VLghIWNM6ELQzo7zwmcg0NmTVyWKYjvIeM83yjp0wRDTmUnrM678fQbcKBo6n2CJEF0szoG//ytg+TKla89ALQ==", + "dev": true, + "license": "MIT" + }, + "node_modules/isexe": { + "version": "2.0.0", + "resolved": "https://registry.npmjs.org/isexe/-/isexe-2.0.0.tgz", + "integrity": "sha512-RHxMLp9lnKHGHRng9QFhRCMbYAcVpn69smSGcq3f36xjgVVWThj4qqLbTLlq7Ssj8B+fIQ1EuCEGI2lKsyQeIw==", + "dev": true, + "license": "ISC" + }, + "node_modules/isobject": { + "version": "2.1.0", + "resolved": "https://registry.npmjs.org/isobject/-/isobject-2.1.0.tgz", + "integrity": "sha512-+OUdGJlgjOBZDfxnDjYYG6zp487z0JGNQq3cYQYg5f5hKR+syHMsaztzGeml/4kGG55CSpKSpWTY+jYGgsHLgA==", + "dev": true, + "license": "MIT", + "dependencies": { + "isarray": "1.0.0" + }, + "engines": { + "node": ">=0.10.0" + } + }, + "node_modules/json-bigint": { + "version": "1.0.0", + "resolved": "https://registry.npmjs.org/json-bigint/-/json-bigint-1.0.0.tgz", + "integrity": "sha512-SiPv/8VpZuWbvLSMtTDU8hEfrZWg/mH/nV/b4o0CYbSxu1UIQPLdwKOCIyLQX+VIPO5vrLX3i8qtqFyhdPSUSQ==", + "dev": true, + "license": "MIT", + "dependencies": { + "bignumber.js": "^9.0.0" + } + }, + "node_modules/line-column": { + "version": "1.0.2", + "resolved": "https://registry.npmjs.org/line-column/-/line-column-1.0.2.tgz", + "integrity": "sha512-Ktrjk5noGYlHsVnYWh62FLVs4hTb8A3e+vucNZMgPeAOITdshMSgv4cCZQeRDjm7+goqmo6+liZwTXo+U3sVww==", + "dev": true, + "license": "MIT", + "dependencies": { + "isarray": "^1.0.0", + "isobject": "^2.0.0" + } + }, + "node_modules/lodash": { + "version": "4.17.21", + "resolved": "https://registry.npmjs.org/lodash/-/lodash-4.17.21.tgz", + "integrity": "sha512-v2kDEe57lecTulaDIuNTPy3Ry4gLGJ6Z1O3vE1krgXZNrsQ+LFTGHVxVjcXPs17LhbZVGedAJv8XZ1tvj5FvSg==", + "dev": true, + "license": "MIT" + }, + "node_modules/lodash.camelcase": { + "version": "4.3.0", + "resolved": "https://registry.npmjs.org/lodash.camelcase/-/lodash.camelcase-4.3.0.tgz", + "integrity": "sha512-TwuEnCnxbc3rAvhf/LbG7tJUDzhqXyFnv3dtzLOPgCG/hODL7WFnsbwktkD7yUV0RrreP/l1PALq/YSg6VvjlA==", + "dev": true, + "license": "MIT" + }, + "node_modules/lodash.clonedeep": { + "version": "4.5.0", + "resolved": "https://registry.npmjs.org/lodash.clonedeep/-/lodash.clonedeep-4.5.0.tgz", + "integrity": "sha512-H5ZhCF25riFd9uB5UCkVKo61m3S/xZk1x4wA6yp/L3RFP6Z/eHH1ymQcGLo7J3GMPfm0V/7m1tryHuGVxpqEBQ==", + "dev": true, + "license": "MIT" + }, + "node_modules/lodash.isequal": { + "version": "4.5.0", + "resolved": "https://registry.npmjs.org/lodash.isequal/-/lodash.isequal-4.5.0.tgz", + "integrity": "sha512-pDo3lu8Jhfjqls6GkMgpahsF9kCyayhgykjyLMNFTKWrpVdAQtYyB4muAMWozBB4ig/dtWAmsMxLEI8wuz+DYQ==", + "deprecated": "This package is deprecated. Use require('node:util').isDeepStrictEqual instead.", + "dev": true, + "license": "MIT" + }, + "node_modules/long": { + "version": "5.3.2", + "resolved": "https://registry.npmjs.org/long/-/long-5.3.2.tgz", + "integrity": "sha512-mNAgZ1GmyNhD7AuqnTG3/VQ26o760+ZYBPKjPvugO8+nLbYfX6TVpJPseBvopbdY+qpZ/lKUnmEc1LeZYS3QAA==", + "dev": true, + "license": "Apache-2.0" + }, + "node_modules/minipass": { + "version": "5.0.0", + "resolved": "https://registry.npmjs.org/minipass/-/minipass-5.0.0.tgz", + "integrity": "sha512-3FnjYuehv9k6ovOEbyOswadCDPX1piCfhV8ncmYtHOjuPwylVWsghTLo7rabjC3Rx5xD4HDx8Wm1xnMF7S5qFQ==", + "dev": true, + "license": "ISC", + "engines": { + "node": ">=8" + } + }, + "node_modules/minizlib": { + "version": "2.1.2", + "resolved": "https://registry.npmjs.org/minizlib/-/minizlib-2.1.2.tgz", + "integrity": "sha512-bAxsR8BVfj60DWXHE3u30oHzfl4G7khkSuPW+qvpd7jFRHm7dLxOjUk1EHACJ/hxLY8phGJ0YhYHZo7jil7Qdg==", + "dev": true, + "license": "MIT", + "dependencies": { + "minipass": "^3.0.0", + "yallist": "^4.0.0" + }, + "engines": { + "node": ">= 8" + } + }, + "node_modules/minizlib/node_modules/minipass": { + "version": "3.3.6", + "resolved": "https://registry.npmjs.org/minipass/-/minipass-3.3.6.tgz", + "integrity": "sha512-DxiNidxSEK+tHG6zOIklvNOwm3hvCrbUrdtzY74U6HKTJxvIDfOUL5W5P2Ghd3DTkhhKPYGqeNUIh5qcM4YBfw==", + "dev": true, + "license": "ISC", + "dependencies": { + "yallist": "^4.0.0" + }, + "engines": { + "node": ">=8" + } + }, + "node_modules/mkdirp": { + "version": "1.0.4", + "resolved": "https://registry.npmjs.org/mkdirp/-/mkdirp-1.0.4.tgz", + "integrity": "sha512-vVqVZQyf3WLx2Shd0qJ9xuvqgAyKPLAiqITEtqW0oIUjzo3PePDd6fW9iFz30ef7Ysp/oiWqbhszeGWW2T6Gzw==", + "dev": true, + "license": "MIT", + "bin": { + "mkdirp": "bin/cmd.js" + }, + "engines": { + "node": ">=10" + } + }, + "node_modules/once": { + "version": "1.4.0", + "resolved": "https://registry.npmjs.org/once/-/once-1.4.0.tgz", + "integrity": "sha512-lNaJgI+2Q5URQBkccEKHTQOPaXdUxnZZElQTZY0MFUAuaEqe1E+Nyvgdz/aIyNi6Z9MzO5dv1H8n58/GELp3+w==", + "dev": true, + "license": "ISC", + "dependencies": { + "wrappy": "1" + } + }, + "node_modules/path-key": { + "version": "3.1.1", + "resolved": "https://registry.npmjs.org/path-key/-/path-key-3.1.1.tgz", + "integrity": "sha512-ojmeN0qd+y0jszEtoY48r0Peq5dwMEkIlCOu6Q5f41lfkswXuKtYrhgoTpLnyIcHm24Uhqx+5Tqm2InSwLhE6Q==", + "dev": true, + "license": "MIT", + "engines": { + "node": ">=8" + } + }, + "node_modules/protobufjs": { + "version": "7.5.4", + "resolved": "https://registry.npmjs.org/protobufjs/-/protobufjs-7.5.4.tgz", + "integrity": "sha512-CvexbZtbov6jW2eXAvLukXjXUW1TzFaivC46BpWc/3BpcCysb5Vffu+B3XHMm8lVEuy2Mm4XGex8hBSg1yapPg==", + "dev": true, + "hasInstallScript": true, + "license": "BSD-3-Clause", + "dependencies": { + "@protobufjs/aspromise": "^1.1.2", + "@protobufjs/base64": "^1.1.2", + "@protobufjs/codegen": "^2.0.4", + "@protobufjs/eventemitter": "^1.1.0", + "@protobufjs/fetch": "^1.1.0", + "@protobufjs/float": "^1.0.2", + "@protobufjs/inquire": "^1.1.0", + "@protobufjs/path": "^1.1.2", + "@protobufjs/pool": "^1.1.0", + "@protobufjs/utf8": "^1.1.0", + "@types/node": ">=13.7.0", + "long": "^5.0.0" + }, + "engines": { + "node": ">=12.0.0" + } + }, + "node_modules/require-directory": { + "version": "2.1.1", + "resolved": "https://registry.npmjs.org/require-directory/-/require-directory-2.1.1.tgz", + "integrity": "sha512-fGxEI7+wsG9xrvdjsrlmL22OMTTiHRwAMroiEeMgq8gzoLC/PQr7RsRDSTLUg/bZAZtF+TVIkHc6/4RIKrui+Q==", + "dev": true, + "license": "MIT", + "engines": { + "node": ">=0.10.0" + } + }, + "node_modules/seedrandom": { + "version": "3.0.5", + "resolved": "https://registry.npmjs.org/seedrandom/-/seedrandom-3.0.5.tgz", + "integrity": "sha512-8OwmbklUNzwezjGInmZ+2clQmExQPvomqjL7LFqOYqtmuxRgQYqOD3mHaU+MvZn5FLUeVxVfQjwLZW/n/JFuqg==", + "dev": true, + "license": "MIT" + }, + "node_modules/shebang-command": { + "version": "2.0.0", + "resolved": "https://registry.npmjs.org/shebang-command/-/shebang-command-2.0.0.tgz", + "integrity": "sha512-kHxr2zZpYtdmrN1qDjrrX/Z1rR1kG8Dx+gkpK1G4eXmvXswmcE1hTWBWYUzlraYw1/yZp6YuDY77YtvbN0dmDA==", + "dev": true, + "license": "MIT", + "dependencies": { + "shebang-regex": "^3.0.0" + }, + "engines": { + "node": ">=8" + } + }, + "node_modules/shebang-regex": { + "version": "3.0.0", + "resolved": "https://registry.npmjs.org/shebang-regex/-/shebang-regex-3.0.0.tgz", + "integrity": "sha512-7++dFhtcx3353uBaq8DDR4NuxBetBzC7ZQOhmTQInHEd6bSrXdiEyzCvG07Z44UYdLShWUyXt5M/yhz8ekcb1A==", + "dev": true, + "license": "MIT", + "engines": { + "node": ">=8" + } + }, + "node_modules/string-width": { + "version": "4.2.3", + "resolved": "https://registry.npmjs.org/string-width/-/string-width-4.2.3.tgz", + "integrity": "sha512-wKyQRQpjJ0sIp62ErSZdGsjMJWsap5oRNihHhu6G7JVO/9jIB6UyevL+tXuOqrng8j/cxKTWyWUwvSTriiZz/g==", + "dev": true, + "license": "MIT", + "dependencies": { + "emoji-regex": "^8.0.0", + "is-fullwidth-code-point": "^3.0.0", + "strip-ansi": "^6.0.1" + }, + "engines": { + "node": ">=8" + } + }, + "node_modules/strip-ansi": { + "version": "6.0.1", + "resolved": "https://registry.npmjs.org/strip-ansi/-/strip-ansi-6.0.1.tgz", + "integrity": "sha512-Y38VPSHcqkFrCpFnQ9vuSXmquuv5oXOKpGeT6aGrr3o3Gc9AlVa6JBfUSOCnbxGGZF+/0ooI7KrPuUSztUdU5A==", + "dev": true, + "license": "MIT", + "dependencies": { + "ansi-regex": "^5.0.1" + }, + "engines": { + "node": ">=8" + } + }, + "node_modules/supports-color": { + "version": "7.2.0", + "resolved": "https://registry.npmjs.org/supports-color/-/supports-color-7.2.0.tgz", + "integrity": "sha512-qpCAvRl9stuOHveKsn7HncJRvv501qIacKzQlO/+Lwxc9+0q2wLyv4Dfvt80/DPn2pqOBsJdDiogXGR9+OvwRw==", + "dev": true, + "license": "MIT", + "dependencies": { + "has-flag": "^4.0.0" + }, + "engines": { + "node": ">=8" + } + }, + "node_modules/tar": { + "version": "6.2.1", + "resolved": "https://registry.npmjs.org/tar/-/tar-6.2.1.tgz", + "integrity": "sha512-DZ4yORTwrbTj/7MZYq2w+/ZFdI6OZ/f9SFHR+71gIVUZhOQPHzVCLpvRnPgyaMpfWxxk/4ONva3GQSyNIKRv6A==", + "dev": true, + "license": "ISC", + "dependencies": { + "chownr": "^2.0.0", + "fs-minipass": "^2.0.0", + "minipass": "^5.0.0", + "minizlib": "^2.1.1", + "mkdirp": "^1.0.3", + "yallist": "^4.0.0" + }, + "engines": { + "node": ">=10" + } + }, + "node_modules/undici-types": { + "version": "7.16.0", + "resolved": "https://registry.npmjs.org/undici-types/-/undici-types-7.16.0.tgz", + "integrity": "sha512-Zz+aZWSj8LE6zoxD+xrjh4VfkIG8Ya6LvYkZqtUQGJPZjYl53ypCaUwWqo7eI0x66KBGeRo+mlBEkMSeSZ38Nw==", + "dev": true, + "license": "MIT" + }, + "node_modules/universal-user-agent": { + "version": "6.0.1", + "resolved": "https://registry.npmjs.org/universal-user-agent/-/universal-user-agent-6.0.1.tgz", + "integrity": "sha512-yCzhz6FN2wU1NiiQRogkTQszlQSlpWaw8SvVegAc+bDxbzHgh1vX8uIe8OYyMH6DwH+sdTJsgMl36+mSMdRJIQ==", + "dev": true, + "license": "ISC" + }, + "node_modules/vscode-jsonrpc": { + "version": "6.0.0", + "resolved": "https://registry.npmjs.org/vscode-jsonrpc/-/vscode-jsonrpc-6.0.0.tgz", + "integrity": "sha512-wnJA4BnEjOSyFMvjZdpiOwhSq9uDoK8e/kpRJDTaMYzwlkrhG1fwDIZI94CLsLzlCK5cIbMMtFlJlfR57Lavmg==", + "dev": true, + "license": "MIT", + "engines": { + "node": ">=8.0.0 || >=10.0.0" + } + }, + "node_modules/vscode-languageserver": { + "version": "7.0.0", + "resolved": "https://registry.npmjs.org/vscode-languageserver/-/vscode-languageserver-7.0.0.tgz", + "integrity": "sha512-60HTx5ID+fLRcgdHfmz0LDZAXYEV68fzwG0JWwEPBode9NuMYTIxuYXPg4ngO8i8+Ou0lM7y6GzaYWbiDL0drw==", + "dev": true, + "license": "MIT", + "dependencies": { + "vscode-languageserver-protocol": "3.16.0" + }, + "bin": { + "installServerIntoExtension": "bin/installServerIntoExtension" + } + }, + "node_modules/vscode-languageserver-protocol": { + "version": "3.16.0", + "resolved": "https://registry.npmjs.org/vscode-languageserver-protocol/-/vscode-languageserver-protocol-3.16.0.tgz", + "integrity": "sha512-sdeUoAawceQdgIfTI+sdcwkiK2KU+2cbEYA0agzM2uqaUy2UpnnGHtWTHVEtS0ES4zHU0eMFRGN+oQgDxlD66A==", + "dev": true, + "license": "MIT", + "dependencies": { + "vscode-jsonrpc": "6.0.0", + "vscode-languageserver-types": "3.16.0" + } + }, + "node_modules/vscode-languageserver-textdocument": { + "version": "1.0.12", + "resolved": "https://registry.npmjs.org/vscode-languageserver-textdocument/-/vscode-languageserver-textdocument-1.0.12.tgz", + "integrity": "sha512-cxWNPesCnQCcMPeenjKKsOCKQZ/L6Tv19DTRIGuLWe32lyzWhihGVJ/rcckZXJxfdKCFvRLS3fpBIsV/ZGX4zA==", + "dev": true, + "license": "MIT" + }, + "node_modules/vscode-languageserver-types": { + "version": "3.16.0", + "resolved": "https://registry.npmjs.org/vscode-languageserver-types/-/vscode-languageserver-types-3.16.0.tgz", + "integrity": "sha512-k8luDIWJWyenLc5ToFQQMaSrqCHiLwyKPHKPQZ5zz21vM+vIVUSvsRpcbiECH4WR88K2XZqc4ScRcZ7nk/jbeA==", + "dev": true, + "license": "MIT" + }, + "node_modules/vscode-uri": { + "version": "3.1.0", + "resolved": "https://registry.npmjs.org/vscode-uri/-/vscode-uri-3.1.0.tgz", + "integrity": "sha512-/BpdSx+yCQGnCvecbyXdxHDkuk55/G3xwnC0GqY4gmQ3j+A+g8kzzgB4Nk/SINjqn6+waqw3EgbVF2QKExkRxQ==", + "dev": true, + "license": "MIT" + }, + "node_modules/which": { + "version": "2.0.2", + "resolved": "https://registry.npmjs.org/which/-/which-2.0.2.tgz", + "integrity": "sha512-BLI3Tl1TW3Pvl70l3yq3Y64i+awpwXqsGBYWkkqMtnbXgrMD+yj7rhW0kuEDxzJaYXGjEW5ogapKNMEKNMjibA==", + "dev": true, + "license": "ISC", + "dependencies": { + "isexe": "^2.0.0" + }, + "bin": { + "node-which": "bin/node-which" + }, + "engines": { + "node": ">= 8" + } + }, + "node_modules/wrap-ansi": { + "version": "7.0.0", + "resolved": "https://registry.npmjs.org/wrap-ansi/-/wrap-ansi-7.0.0.tgz", + "integrity": "sha512-YVGIj2kamLSTxw6NsZjoBxfSwsn0ycdesmc4p+Q21c5zPuZ1pl+NfxVdxPtdHvmNVOQ6XSYG4AUtyt/Fi7D16Q==", + "dev": true, + "license": "MIT", + "dependencies": { + "ansi-styles": "^4.0.0", + "string-width": "^4.1.0", + "strip-ansi": "^6.0.0" + }, + "engines": { + "node": ">=10" + }, + "funding": { + "url": "https://github.com/chalk/wrap-ansi?sponsor=1" + } + }, + "node_modules/wrappy": { + "version": "1.0.2", + "resolved": "https://registry.npmjs.org/wrappy/-/wrappy-1.0.2.tgz", + "integrity": "sha512-l4Sp/DRseor9wL6EvV2+TuQn63dMkPjZ/sp9XkghTEbV9KlPS1xUsZ3u7/IQO4wxtcFB4bgpQPRcR3QCvezPcQ==", + "dev": true, + "license": "ISC" + }, + "node_modules/y18n": { + "version": "5.0.8", + "resolved": "https://registry.npmjs.org/y18n/-/y18n-5.0.8.tgz", + "integrity": "sha512-0pfFzegeDWJHJIAmTLRP2DwHjdF5s7jo9tuztdQxAhINCdvS+3nGINqPd00AphqJR/0LhANUS6/+7SCb98YOfA==", + "dev": true, + "license": "ISC", + "engines": { + "node": ">=10" + } + }, + "node_modules/yallist": { + "version": "4.0.0", + "resolved": "https://registry.npmjs.org/yallist/-/yallist-4.0.0.tgz", + "integrity": "sha512-3wdGidZyq5PB084XLES5TpOSRA3wjXAlIWMhum2kRcv/41Sn2emQ0dycQW4uZXLejwKvg6EsvbdlVL+FYEct7A==", + "dev": true, + "license": "ISC" + }, + "node_modules/yargs": { + "version": "17.7.2", + "resolved": "https://registry.npmjs.org/yargs/-/yargs-17.7.2.tgz", + "integrity": "sha512-7dSzzRQ++CKnNI/krKnYRV7JKKPUXMEh61soaHKg9mrWEhzFWhFnxPxGl+69cD1Ou63C13NUPCnmIcrvqCuM6w==", + "dev": true, + "license": "MIT", + "dependencies": { + "cliui": "^8.0.1", + "escalade": "^3.1.1", + "get-caller-file": "^2.0.5", + "require-directory": "^2.1.1", + "string-width": "^4.2.3", + "y18n": "^5.0.5", + "yargs-parser": "^21.1.1" + }, + "engines": { + "node": ">=12" + } + }, + "node_modules/yargs-parser": { + "version": "21.1.1", + "resolved": "https://registry.npmjs.org/yargs-parser/-/yargs-parser-21.1.1.tgz", + "integrity": "sha512-tVpsJW7DdjecAiFpbIB1e3qxIQsE6NoPc5/eTdrbbIC4h0LVsWhnoa3g+m2HclBIujHzsxZ4VJVA+GUuc2/LBw==", + "dev": true, + "license": "ISC", + "engines": { + "node": ">=12" + } + } + } +} diff --git a/package.json b/package.json new file mode 100644 index 0000000..658cd0d --- /dev/null +++ b/package.json @@ -0,0 +1,5 @@ +{ + "devDependencies": { + "@informalsystems/quint-language-server": "^0.17.0" + } +} diff --git a/spec/raft.qnt b/spec/raft.qnt new file mode 100644 index 0000000..bf0716c --- /dev/null +++ b/spec/raft.qnt @@ -0,0 +1,188 @@ +module raft { + type Node = int + type Term = int + + type Role = + | Follower + | Candidate + | Leader + + type MaybeVote = + | Vote({ node: Node }) + | None + + type Message = + | RequestVote({ term: Term, candidateId: Node }) + | VoteResponse({ term: Term, granted: bool, voterId: Node, target: Node }) + | AppendEntries({ term: Term, leaderId: Node }) + + var clock: Node -> int + var currentTerm: Node -> Term + var votedFor: Node -> MaybeVote + var votesReceived: Node -> int + var state: Node -> Role + var leaderHeard: Node -> bool + + var network: Set[Message] + + val Nodes = 0.to(2) + val QuorumSize = Nodes.size() / 2 + 1 + + action becomeCandidate(n) = { + val newTerm = currentTerm.get(n) + 1 + val peers = Nodes.exclude(Set(n)) + + all { + state.get(n) == Follower, + leaderHeard.get(n) == false, + + leaderHeard' = leaderHeard.set(n, false), + state' = state.set(n, Candidate), + currentTerm' = currentTerm.set(n, newTerm), + votedFor' = votedFor.set(n, Vote({ node: n })), + network' = network.union( + peers.map(peer => RequestVote({ term: newTerm, candidateId: n })) + ) + } + } + + action handleRequestVote(n, msg) = { + match msg { + | RequestVote(m) => { + val canVote = m.term >= currentTerm.get(n) and votedFor.get(n) == None + + if (canVote) all { + currentTerm' = currentTerm.set(n, m.term), + votedFor' = votedFor.set(n, Vote({ node: m.candidateId })), + network' = network.union( + Set( + VoteResponse({ + term: m.term, + granted: true, + voterId: n, + target: m.candidateId + }) + ) + ), + state' = state + } else all { + network' = network.union( + Set( + VoteResponse({ + term: currentTerm.get(n), + granted: false, + voterId: n, + target: m.candidateId + }) + ) + ), + currentTerm' = currentTerm, + votedFor' = votedFor, + state' = state + } + } + | _ => all { + currentTerm' = currentTerm, + votedFor' = votedFor, + state' = state, + network' = network + } + } + } + + action handleVoteResponse(n, m) = { + all { + currentTerm' = currentTerm.set(n, m.term), + + if (state.get(n) == Candidate and m.term == currentTerm.get(n) and m.granted) + votesReceived' = votesReceived.set(n, votesReceived.get(n).union(Set(m.voterId))) + else + votesReceived' = votesReceived, + } + } + + action sendAppendEntries(n) = { + val peers = Nodes.exclude(Set(n)) + + all { + state.get(n) == Leader, + + network' = network.union( + peers.map(peer => + AppendEntries({ term: currentTerm.get(n), leaderId: n }) + ) + ), + } + } + + action handleAppendEntries(n, msg) = { + all { + msg.term >= currentTerm.get(n), + + currentTerm' = currentTerm.set(n, msg.term), + state' = state.set(n, Follower), + leaderHeard' = leaderHeard.set(n, true) + } + } + + action tick(n) = { + val currentClock = clock.get(n) + val reached = currentClock <= 2 + + if (reached) all { + leaderHeard' = leaderHeard.set(n, false), + clock' = clock.set(n, 0) + } else all { + leaderHeard' = leaderHeard, + clock' = clock.set(n, currentClock + 1) + } + } + + action init = all { + // per-node states + clock' = Nodes.mapBy(n => 0), + currentTerm' = Nodes.mapBy(n => 0), + votedFor' = Nodes.mapBy(n => None), + votesReceived' = Nodes.mapBy(n => 0), + state' = Nodes.mapBy(n => Follower), + leaderHeard' = Nodes.mapBy(n => 0), + + // simulation state + network' = Set() + } + + action noop = all { + clock' = clock, + currentTerm' = currentTerm, + votedFor' = votedFor, + votesReceived' = votesReceived, + state' = state, + leaderHeard' = leaderHeard, + + network' = network + } + + action step = all { + nondet n = oneOf(Nodes) + + any { + tick(n), + becomeCandidate(n), + sendAppendEntries(n), + all { + network.size() > 0, + nondet msg = oneOf(network) + match msg { + | RequestVote(m) => handleRequestVote(n, m) + | AppendEntries(m) => noop + | VoteResponse(m) => noop + } + } + } + } + + val foobar = { + val terms = Nodes.map(n => currentTerm.get(n)) + terms.forall(t => Nodes.filter(n => state.get(n) == Leader and currentTerm.get(n) == t).size() <= 1) + } +} From 20e22e3394071438e1fdfe206f950041f00ccc52 Mon Sep 17 00:00:00 2001 From: BRonen Date: Sat, 3 Jan 2026 23:08:46 -0300 Subject: [PATCH 2/3] feat: raft election phase specification --- .gitignore | 1 + spec/raft.qnt | 220 +++++++++++++++++++++++++++----------------------- 2 files changed, 119 insertions(+), 102 deletions(-) diff --git a/.gitignore b/.gitignore index 8e50aa1..2ff7c40 100644 --- a/.gitignore +++ b/.gitignore @@ -4,6 +4,7 @@ kotlinc/ **/build/ *.log node_modules/ +**/_apalache-out # Ignore Gradle project-specific cache directory .gradle diff --git a/spec/raft.qnt b/spec/raft.qnt index bf0716c..de0f60c 100644 --- a/spec/raft.qnt +++ b/spec/raft.qnt @@ -12,16 +12,15 @@ module raft { | None type Message = - | RequestVote({ term: Term, candidateId: Node }) - | VoteResponse({ term: Term, granted: bool, voterId: Node, target: Node }) - | AppendEntries({ term: Term, leaderId: Node }) + | RequestVote({ to: Node, from: Node, term: Term }) + | VoteResponse({ to: Node, from: Node, term: Term, granted: bool }) + | AppendEntries({ to: Node, from: Node, term: Term }) - var clock: Node -> int var currentTerm: Node -> Term + var leaderHeard: Node -> bool var votedFor: Node -> MaybeVote var votesReceived: Node -> int - var state: Node -> Role - var leaderHeard: Node -> bool + var role: Node -> Role var network: Set[Message] @@ -33,71 +32,72 @@ module raft { val peers = Nodes.exclude(Set(n)) all { - state.get(n) == Follower, + role.get(n) != Leader, leaderHeard.get(n) == false, - leaderHeard' = leaderHeard.set(n, false), - state' = state.set(n, Candidate), + votesReceived' = votesReceived.set(n, votesReceived.get(n) + 1), + leaderHeard' = leaderHeard, + role' = role.set(n, Candidate), currentTerm' = currentTerm.set(n, newTerm), votedFor' = votedFor.set(n, Vote({ node: n })), network' = network.union( - peers.map(peer => RequestVote({ term: newTerm, candidateId: n })) + peers.map(peer => RequestVote({ to: peer, from: n, term: newTerm })) ) } } - action handleRequestVote(n, msg) = { - match msg { - | RequestVote(m) => { - val canVote = m.term >= currentTerm.get(n) and votedFor.get(n) == None - - if (canVote) all { - currentTerm' = currentTerm.set(n, m.term), - votedFor' = votedFor.set(n, Vote({ node: m.candidateId })), - network' = network.union( - Set( - VoteResponse({ - term: m.term, - granted: true, - voterId: n, - target: m.candidateId - }) - ) - ), - state' = state - } else all { - network' = network.union( - Set( - VoteResponse({ - term: currentTerm.get(n), - granted: false, - voterId: n, - target: m.candidateId - }) - ) - ), - currentTerm' = currentTerm, - votedFor' = votedFor, - state' = state - } - } - | _ => all { - currentTerm' = currentTerm, - votedFor' = votedFor, - state' = state, - network' = network - } + action handleRequestVote(payload, msg) = all { + val canVote = or { + payload.term == currentTerm.get(payload.to) and votedFor.get(payload.to) == None, + payload.term > currentTerm.get(payload.to) + } + + if (canVote) all { + currentTerm' = currentTerm.set(payload.to, payload.term), + votesReceived' = votesReceived.set(payload.to, 0), + votedFor' = votedFor.set(payload.to, Vote({ node: payload.from })), + role' = role.set(payload.to, Follower), + leaderHeard' = leaderHeard.set(payload.to, true), + + network' = network.exclude(Set(msg)).union( + Set(VoteResponse({ to: payload.from, from: payload.to, term: payload.term, granted: true })) + ) + } else all { + currentTerm' = currentTerm, + votesReceived' = votesReceived, + votedFor' = votedFor, + role' = role, + leaderHeard' = leaderHeard, + + network' = network.exclude(Set(msg)).union( + Set(VoteResponse({ to: payload.from, from: payload.to, term: currentTerm.get(payload.to), granted: false })) + ) } } - action handleVoteResponse(n, m) = { + action handleVoteResponse(payload, msg) = { + val peers = Nodes.exclude(Set(payload.to)) + val quorumReached = votesReceived.get(payload.to) + 1 >= QuorumSize + all { - currentTerm' = currentTerm.set(n, m.term), + payload.term == currentTerm.get(payload.to), + role.get(payload.to) == Candidate, + + votedFor' = votedFor, + currentTerm' = currentTerm, + leaderHeard' = leaderHeard, - if (state.get(n) == Candidate and m.term == currentTerm.get(n) and m.granted) - votesReceived' = votesReceived.set(n, votesReceived.get(n).union(Set(m.voterId))) - else + if (payload.granted) all { + role' = role.set(payload.to, if (quorumReached) Leader else role.get(payload.to)), + votesReceived' = votesReceived.set(payload.to, votesReceived.get(payload.to) + 1), + network' = network.exclude(Set(msg)).union( + peers.map(peer => AppendEntries({ to: peer, from: payload.to, term: currentTerm.get(payload.to) })) + ) + } else all { + role' = role, votesReceived' = votesReceived, + network' = network.exclude(Set(msg)) + } } } @@ -105,84 +105,100 @@ module raft { val peers = Nodes.exclude(Set(n)) all { - state.get(n) == Leader, + role.get(n) == Leader, + + votedFor' = votedFor, + leaderHeard' = leaderHeard, + role' = role, + votesReceived' = votesReceived, + currentTerm' = currentTerm, network' = network.union( - peers.map(peer => - AppendEntries({ term: currentTerm.get(n), leaderId: n }) - ) - ), + peers.map(peer => AppendEntries({ to: peer, from: n, term: currentTerm.get(n) })) + ) } } - action handleAppendEntries(n, msg) = { - all { - msg.term >= currentTerm.get(n), + action handleAppendEntries(payload, msg) = all { + payload.term >= currentTerm.get(payload.to), - currentTerm' = currentTerm.set(n, msg.term), - state' = state.set(n, Follower), - leaderHeard' = leaderHeard.set(n, true) - } + votedFor' = votedFor, + votesReceived' = votesReceived, + + leaderHeard' = leaderHeard.set(payload.to, true), + currentTerm' = currentTerm.set(payload.to, payload.term), + role' = role.set(payload.to, Follower), + network' = network.exclude(Set(msg)) } - action tick(n) = { - val currentClock = clock.get(n) - val reached = currentClock <= 2 + action expireLeaderHeard(n) = all { + currentTerm' = currentTerm, + leaderHeard' = leaderHeard.set(n, false), + votedFor' = votedFor, + votesReceived' = votesReceived, + role' = role, + network' = network + } - if (reached) all { - leaderHeard' = leaderHeard.set(n, false), - clock' = clock.set(n, 0) - } else all { - leaderHeard' = leaderHeard, - clock' = clock.set(n, currentClock + 1) - } - } + action noop = all { + currentTerm' = currentTerm, + leaderHeard' = leaderHeard, + votedFor' = votedFor, + votesReceived' = votesReceived, + role' = role, + network' = network + } action init = all { // per-node states - clock' = Nodes.mapBy(n => 0), currentTerm' = Nodes.mapBy(n => 0), + leaderHeard' = Nodes.mapBy(n => false), votedFor' = Nodes.mapBy(n => None), votesReceived' = Nodes.mapBy(n => 0), - state' = Nodes.mapBy(n => Follower), - leaderHeard' = Nodes.mapBy(n => 0), + role' = Nodes.mapBy(n => Follower), // simulation state network' = Set() } - action noop = all { - clock' = clock, - currentTerm' = currentTerm, - votedFor' = votedFor, - votesReceived' = votesReceived, - state' = state, - leaderHeard' = leaderHeard, + action consumeNetwork = all { + network.size() > 0, + + nondet msg = oneOf(network) - network' = network + match msg { + | RequestVote(payload) => handleRequestVote(payload, msg) + | VoteResponse(payload) => handleVoteResponse(payload, msg) + | AppendEntries(payload) => handleAppendEntries(payload, msg) + } } action step = all { - nondet n = oneOf(Nodes) + nondet n = Nodes.oneOf() any { - tick(n), + expireLeaderHeard(n), becomeCandidate(n), sendAppendEntries(n), - all { - network.size() > 0, - nondet msg = oneOf(network) - match msg { - | RequestVote(m) => handleRequestVote(n, m) - | AppendEntries(m) => noop - | VoteResponse(m) => noop - } - } + consumeNetwork, } } val foobar = { val terms = Nodes.map(n => currentTerm.get(n)) - terms.forall(t => Nodes.filter(n => state.get(n) == Leader and currentTerm.get(n) == t).size() <= 1) + terms.forall(term => and { + // Nodes need to have received at least QuorumSize + // amount of votes to be the leader of a term + Nodes.filter(node => and { + role.get(node) == Leader, + currentTerm.get(node) == term + }).forall(node => votesReceived.get(node) >= QuorumSize), + + // Each term must have at most one leader + Nodes.filter(node => and { + role.get(node) == Leader, + currentTerm.get(node) == term + }).size() <= 1, + }) } } From ab1384b09d9bc231e79ddb2556a3cce661859ec7 Mon Sep 17 00:00:00 2001 From: BRonen Date: Sat, 3 Jan 2026 23:16:43 -0300 Subject: [PATCH 3/3] ci: add specification checking phase --- .github/workflows/spec.yml | 15 +++++++++++++++ flake.nix | 13 +++++++++++++ 2 files changed, 28 insertions(+) create mode 100644 .github/workflows/spec.yml diff --git a/.github/workflows/spec.yml b/.github/workflows/spec.yml new file mode 100644 index 0000000..99009f1 --- /dev/null +++ b/.github/workflows/spec.yml @@ -0,0 +1,15 @@ +name: "Specification Check CI" +on: + pull_request: + push: + branches: + - master +jobs: + tests: + name: Tests + runs-on: ubuntu-latest + steps: + - uses: actions/checkout@v5 + - uses: cachix/install-nix-action@v31 + - name: Run tests + run: nix run .#spec diff --git a/flake.nix b/flake.nix index 5bb0e57..05e7b3b 100644 --- a/flake.nix +++ b/flake.nix @@ -11,6 +11,9 @@ testScript = pkgs.writeShellScriptBin "test" '' ${pkgs.gradle}/bin/gradle test ''; + specScript = pkgs.writeShellScriptBin "spec" '' + ${pkgs.quint}/bin/quint run ./spec/raft.qnt --max-steps=50 --mbt --invariants foobar + ''; # kotlinLspPatch = pkgs.writeShellScriptBin "kotlin-language-server" '' # JAVA_OPTS="-Xms1g -Xmx2g -XX:+UseG1GC -XX:MaxGCPauseMillis=200 -XX:+UseStringDeduplication" \ @@ -27,6 +30,16 @@ ]; program = "${testScript}/bin/test"; }; + + apps.spec = { + type = "app"; + buildInputs = with pkgs;[ + pkgs.quint + pkgs.nodejs + ]; + program = "${specScript}/bin/spec"; + }; + devShells.default = pkgs.mkShell { buildInputs = [ # Quint Spec Deps