feat(tbtc/signer): mirror FROST/ROAST Rust signer from tBTC monorepo #4005
There are no files selected for viewing
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,81 @@ | ||
| name: tBTC Signer Formal Verification | ||
|
|
||
| on: | ||
| pull_request: | ||
| paths: | ||
| - pkg/tbtc/signer/** | ||
| - .github/workflows/tbtc-signer-formal.yml | ||
| schedule: | ||
| - cron: "23 5 * * *" | ||
| workflow_dispatch: | ||
|
|
||
| permissions: | ||
| contents: read | ||
|
|
||
| concurrency: | ||
| group: tbtc-signer-formal-${{ github.ref }} | ||
| cancel-in-progress: true | ||
|
|
||
| jobs: | ||
| signer-rust-checks: | ||
| name: Signer Rust checks | ||
| runs-on: ubuntu-latest | ||
| timeout-minutes: 30 | ||
| steps: | ||
| - name: Checkout | ||
| uses: actions/checkout@v4 | ||
|
|
||
| - name: Setup Rust | ||
| uses: dtolnay/rust-toolchain@stable | ||
| with: | ||
| components: rustfmt, clippy | ||
|
|
||
| - name: Check formatting | ||
| run: cargo fmt --manifest-path pkg/tbtc/signer/Cargo.toml -- --check | ||
|
|
||
| - name: Run clippy | ||
| run: cargo clippy --manifest-path pkg/tbtc/signer/Cargo.toml --all-targets -- -D warnings | ||
|
|
||
| - name: Run signer tests | ||
| env: | ||
| TBTC_SIGNER_STATE_PATH: /tmp/tbtc-signer-ci-state-${{ github.run_id }}-${{ github.run_attempt }}.json | ||
| run: cargo test --manifest-path pkg/tbtc/signer/Cargo.toml | ||
|
|
||
| signer-formal-invariants: | ||
| name: Signer formal invariants | ||
| runs-on: ubuntu-latest | ||
| timeout-minutes: 30 | ||
| steps: | ||
| - name: Checkout | ||
| uses: actions/checkout@v4 | ||
|
There was a problem hiding this comment. 🧩 Analysis chain🏁 Script executed: #!/bin/bash
set -euo pipefail
for repo in actions/checkout actions/setup-java dtolnay/rust-toolchain; do
echo "=== $repo ==="
git ls-remote "https://github.com/${repo}.git" | head -n 5
echo
doneRepository: threshold-network/keep-core Length of output: 535 🏁 Script executed: #!/bin/bash
set -euo pipefail
# 1) Inspect workflow around the referenced lines
echo "=== Workflow file context ==="
nl -ba .github/workflows/tbtc-signer-formal.yml | sed -n '1,120p'
# 2) Resolve refs to commit SHAs (avoid SIGPIPE by capturing then slicing)
resolve_ref() {
local repo="$1" ref="$2"
local url="https://github.com/${repo}.git"
local tmp="/tmp/lsremote_${repo//\//_}_${ref//\//_}"
git ls-remote "$url" "$ref" > "$tmp" 2>/dev/null || true
echo "--- ${repo} ${ref} ---"
cat "$tmp" || true
echo
rm -f "$tmp" || true
}
echo "=== Resolve action refs to SHAs ==="
resolve_ref "actions/checkout" "refs/tags/v4"
resolve_ref "actions/checkout" "refs/heads/v4"
resolve_ref "actions/setup-java" "refs/tags/v4"
resolve_ref "actions/setup-java" "refs/heads/v4"
resolve_ref "dtolnay/rust-toolchain" "refs/heads/stable"
resolve_ref "dtolnay/rust-toolchain" "refs/tags/stable"Repository: threshold-network/keep-core Length of output: 162 🏁 Script executed: #!/bin/bash
set -euo pipefail
echo "=== Workflow file context (numbered) ==="
python3 - <<'PY'
from pathlib import Path
p = Path(".github/workflows/tbtc-signer-formal.yml")
lines = p.read_text().splitlines()
start, end = 1, min(len(lines), 140)
for i in range(start, end+1):
print(f"{i}\t{lines[i-1]}")
PY
echo
echo "=== Resolve action refs to commit SHAs ==="
resolve_ref() {
local repo="$1" ref="$2"
local url="https://github.com/${repo}.git"
echo "--- ${repo} ${ref} ---"
git ls-remote "$url" "$ref" || true
echo
}
resolve_ref "actions/checkout" "refs/tags/v4"
resolve_ref "actions/checkout" "refs/heads/v4"
resolve_ref "actions/setup-java" "refs/tags/v4"
resolve_ref "actions/setup-java" "refs/heads/v4"
resolve_ref "dtolnay/rust-toolchain" "refs/heads/stable"
resolve_ref "dtolnay/rust-toolchain" "refs/tags/stable"Repository: threshold-network/keep-core Length of output: 2438 🏁 Script executed: #!/bin/bash
set -euo pipefail
echo "Total lines: $(python3 - <<'PY'\nimport pathlib\np=pathlib.Path('.github/workflows/tbtc-signer-formal.yml')\nprint(len(p.read_text().splitlines()))\nPY)"
echo
echo "=== uses: occurrences ==="
rg -n "uses:" .github/workflows/tbtc-signer-formal.yml || true
echo
echo "=== persist-credentials occurrences ==="
rg -n "persist-credentials" .github/workflows/tbtc-signer-formal.yml || trueRepository: threshold-network/keep-core Length of output: 133 🏁 Script executed: #!/bin/bash
set -euo pipefail
echo "Total lines: $(python3 - <<'PY'
import pathlib
p=pathlib.Path('.github/workflows/tbtc-signer-formal.yml')
print(len(p.read_text().splitlines()))
PY)"
echo
echo "=== uses: occurrences ==="
rg -n "uses:" .github/workflows/tbtc-signer-formal.yml || true
echo
echo "=== persist-credentials occurrences ==="
rg -n "persist-credentials" .github/workflows/tbtc-signer-formal.yml || trueRepository: threshold-network/keep-core Length of output: 424 Pin GitHub Actions to commit SHAs and harden checkout credentials.
🧰 Tools🪛 zizmor (1.25.2)[warning] 25-26: credential persistence through GitHub Actions artifacts (artipacked): does not set persist-credentials: false (artipacked) [error] 26-26: unpinned action reference (unpinned-uses): action is not pinned to a hash (required by blanket policy) (unpinned-uses) 🤖 Prompt for AI Agents |
||
|
|
||
| - name: Setup Rust | ||
| uses: dtolnay/rust-toolchain@stable | ||
|
|
||
| - name: Run signer formal invariant tests | ||
| # Filters cargo test by the formal_verification_ prefix so only | ||
| # the formal-invariant test cases run (faster + clearer signal | ||
| # than the full suite). Matches the convention used in the | ||
| # source monorepo's ci-formal-verification.yml. | ||
| run: cargo test --manifest-path pkg/tbtc/signer/Cargo.toml formal_verification_ | ||
|
|
||
| tla-model-checks: | ||
| name: TLA model checks | ||
| runs-on: ubuntu-latest | ||
| timeout-minutes: 20 | ||
| steps: | ||
| - name: Checkout | ||
| uses: actions/checkout@v4 | ||
|
|
||
| - name: Setup Java | ||
| uses: actions/setup-java@v4 | ||
| with: | ||
| distribution: temurin | ||
| java-version: "17" | ||
|
|
||
| - name: Run TLA model checks | ||
| # Iterates over every .cfg under pkg/tbtc/signer/docs/formal/models/ | ||
| # and runs TLC against the matching .tla module. MODELS_PATH defaults | ||
| # to the canonical signer-relative path; override via env var for | ||
| # alternate environments (set in extraction/frost-signer-mirror PR). | ||
| run: pkg/tbtc/signer/scripts/formal/run_tla_models.sh | ||
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1 @@ | ||
| target/ |
Oops, something went wrong.
Oops, something went wrong.
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
🧩 Analysis chain
🏁 Script executed:
Repository: threshold-network/keep-core
Length of output: 272
🏁 Script executed:
Repository: threshold-network/keep-core
Length of output: 272
🏁 Script executed:
Repository: threshold-network/keep-core
Length of output: 2302
Set
persist-credentials: falseon bothactions/checkout@v4stepsThe current workflow checks out without disabling persisted git credentials; add
with: persist-credentials: falseto reduce credential exposure.Suggested patch
- name: Checkout uses: actions/checkout@v4 + with: + persist-credentials: false @@ - name: Checkout uses: actions/checkout@v4 + with: + persist-credentials: false📝 Committable suggestion
🧰 Tools
🪛 zizmor (1.25.2)
[warning] 25-26: credential persistence through GitHub Actions artifacts (artipacked): does not set persist-credentials: false
(artipacked)
[error] 26-26: unpinned action reference (unpinned-uses): action is not pinned to a hash (required by blanket policy)
(unpinned-uses)
🤖 Prompt for AI Agents