Skip to content
Merged
Show file tree
Hide file tree
Changes from 4 commits
Commits
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: 0 additions & 16 deletions .config/nextest.toml
Original file line number Diff line number Diff line change
Expand Up @@ -6,12 +6,6 @@
# it's either a production bug or a test bug that must be fixed.
# Do NOT add retries to mask flakiness.

# Test groups for tests that share UDP ports
# These tests must run serially to avoid port conflicts
[test-groups]
# Tests in sessions::p2p, sessions::p2p_enum, and some spectator tests use ports 7777/8888
port-7777 = { max-threads = 1 }

[profile.default]
# Zero retries - tests must pass first time
retries = 0
Expand All @@ -33,16 +27,6 @@ status-level = "pass"
failure-output = "immediate-final" # Show failure output immediately AND at end
success-output = "never" # Hide output for passing tests (reduce noise)

# Serialize tests that use port 7777 (and 8888)
[[profile.default.overrides]]
filter = 'test(sessions::p2p::) | test(sessions::p2p_enum::)'
test-group = 'port-7777'

# Spectator tests using 7777/8888 (test_start_session and test_synchronize_with_host)
[[profile.default.overrides]]
filter = 'test(sessions::spectator::test_start_session) | test(sessions::spectator::test_synchronize_with_host)'
test-group = 'port-7777'

# Multi-process network tests need longer timeouts because they:
# 1. Spawn external peer processes
# 2. Simulate hostile network conditions (high packet loss, burst loss)
Expand Down
8 changes: 4 additions & 4 deletions .devcontainer/README.md
Original file line number Diff line number Diff line change
Expand Up @@ -56,7 +56,7 @@ This devcontainer provides a complete environment for developing, testing, and f
After the container starts, verify all tools:

```bash
./scripts/check-tools.sh
./scripts/ci/check-tools.sh
```

## Build Performance
Expand Down Expand Up @@ -96,19 +96,19 @@ means subsequent rebuilds only reprocess changed layers.
### All Verifiers

```bash
./scripts/verify-all.sh
./scripts/verification/verify-all.sh
```

### TLA+ Only

```bash
./scripts/verify-tla.sh
./scripts/verification/verify-tla.sh
```

### Kani Only

```bash
./scripts/verify-kani.sh
./scripts/verification/verify-kani.sh
# Or directly:
cargo kani
```
Expand Down
84 changes: 81 additions & 3 deletions .devcontainer/devcontainer.json
Original file line number Diff line number Diff line change
Expand Up @@ -2,7 +2,6 @@
// README at: https://github.com/devcontainers/templates/tree/main/src/rust
{
"name": "Fortress Rollback - Full Verification Environment",

// ===== BUILD OPTIONS (choose one) =====
//
// Option A: Build locally from Dockerfile (first build ~3-5 min, rebuilds use cache)
Expand All @@ -15,7 +14,6 @@
// Local Dockerfile builds remain the default until the registry path is validated across environments.
// Uncomment the line below and comment out the "build" block above to use it.
// "image": "ghcr.io/wallstop/fortress-rollback/devcontainer:latest",

// Additional features (on top of what's in Dockerfile)
"features": {
"ghcr.io/devcontainers/features/powershell:1": {}
Expand All @@ -28,7 +26,7 @@
}
],
// Post-create setup: only workspace-specific tasks (tools are pre-installed in image)
"postCreateCommand": "bash -c '\n set -e\n echo \"=== Setting up Fortress Rollback Development Environment ===\"\n \n # Ensure TLA+ tools are in the workspace\n mkdir -p .tla-tools\n if [ -f /opt/tla/tla2tools.jar ]; then\n cp /opt/tla/tla2tools.jar .tla-tools/\n elif [ ! -f .tla-tools/tla2tools.jar ]; then\n echo \"Downloading TLA+ tools...\"\n curl --proto \"=https\" --tlsv1.2 -fsSL --retry 5 --retry-delay 2 --retry-all-errors --max-time 120 https://github.com/tlaplus/tlaplus/releases/download/v1.8.0/tla2tools.jar -o .tla-tools/tla2tools.jar\n fi\n \n # Sync Vale styles (prose linter)\n if command -v vale >/dev/null 2>&1 && [ -f .vale.ini ]; then\n echo \"Syncing Vale packages...\"\n vale sync || echo \"Vale sync failed, run vale sync manually\"\n fi\n \n # Build project to warm dependency cache\n echo \"Warming dependency cache...\"\n if ! cargo build; then\n echo \"WARNING: Initial cargo build failed. Run cargo build manually to see errors.\"\n fi\n \n echo \"=== Development environment ready! ===\"\n echo \"Run ./scripts/check-tools.sh to verify all tools are installed.\"\n'",
"postCreateCommand": "bash -c '\n set -e\n echo \"=== Setting up Fortress Rollback Development Environment ===\"\n \n # Ensure TLA+ tools are in the workspace\n mkdir -p .tla-tools\n if [ -f /opt/tla/tla2tools.jar ]; then\n cp /opt/tla/tla2tools.jar .tla-tools/\n elif [ ! -f .tla-tools/tla2tools.jar ]; then\n echo \"Downloading TLA+ tools...\"\n curl --proto \"=https\" --tlsv1.2 -fsSL --retry 5 --retry-delay 2 --retry-all-errors --max-time 120 https://github.com/tlaplus/tlaplus/releases/download/v1.8.0/tla2tools.jar -o .tla-tools/tla2tools.jar\n fi\n \n # Sync Vale styles (prose linter)\n if command -v vale >/dev/null 2>&1 && [ -f .vale.ini ]; then\n echo \"Syncing Vale packages...\"\n vale sync || echo \"Vale sync failed, run vale sync manually\"\n fi\n \n # Build project to warm dependency cache\n echo \"Warming dependency cache...\"\n if ! cargo build; then\n echo \"WARNING: Initial cargo build failed. Run cargo build manually to see errors.\"\n fi\n \n echo \"=== Development environment ready! ===\"\n echo \"Run ./scripts/ci/check-tools.sh to verify all tools are installed.\"\n'",
// Environment variables for tools
"containerEnv": {
"TLA_TOOLS_JAR": "${containerWorkspaceFolder}/.tla-tools/tla2tools.jar",
Expand All @@ -53,11 +51,91 @@
"ms-python.vscode-pylance",
"ryanluker.vscode-coverage-gutters",
"streetsidesoftware.code-spell-checker",
"PKief.material-icon-theme",
"GitHub.github-vscode-theme",
"redhat.vscode-yaml",
"markdownlint.markdownlint",
"eamodio.gitlens",
"serayuzgur.crates",
"EditorConfig.EditorConfig",
"yzhang.markdown-all-in-one",
"ms-vscode.hexeditor",
"dracula-theme.theme-dracula",
"enkia.tokyo-night",
"catppuccin.catppuccin-vsc",
"zhuangtongfa.material-theme",
"akamud.vscode-theme-onedark",
"sdras.night-owl",
"teabyii.ayu",
"arcticicestudio.nord-visual-studio-code",
"jdinhlife.gruvbox",
"mvllow.rose-pine",
"whizkydee.material-palenight-theme",
"alexandernanberg.horizon-theme-vscode",
"brittanychiang.halcyon-vscode",
"robbowen.synthwave-vscode",
"pmndrs.pmndrs",
"qufiwefefwoyn.kanagawa",
"azemoh.one-monokai",
"GitHub.copilot",
"GitHub.copilot-chat",
"anthropic.claude-code"
],
"settings": {
"workbench.iconTheme": "material-icon-theme",
"workbench.colorTheme": "GitHub Dark Default",
"workbench.preferredDarkColorTheme": "GitHub Dark Default",
"workbench.preferredLightColorTheme": "GitHub Light Default",
"explorer.excludeGitIgnore": false,
"explorer.compactFolders": false,
"explorer.confirmDelete": false,
"files.exclude": {
"**/.git": true,
"**/.claude": true,
"**/.ruff_cache": true,
"**/.vale": true,
"**/.vscode": true,
"**/target": true,
"**/node_modules": true,
"**/__pycache__": true,
"**/specs/tla/states*": true,
"**/mutants.out": true,
"**/.tmp": true,
"**/.idea": true,
"**/site": true,
"**/states": true,
"loom-tests/target": true,
"progress": true,
"fuzz/corpus": true,
"fuzz/artifacts": true,
"fuzz/coverage": true
},
"files.watcherExclude": {
"**/.git/objects/**": true,
"**/target/**": true,
"**/node_modules/**": true
},
"search.exclude": {
"**/.git": true,
"**/target": true,
"**/node_modules": true,
"**/__pycache__": true,
"**/mutants.out": true
},
"git.autofetch": true,
"scm.diffDecorations": "all",
"editor.bracketPairColorization.enabled": true,
"editor.guides.bracketPairs": true,
"editor.inlineSuggest.enabled": true,
"editor.smoothScrolling": true,
"editor.stickyScroll.enabled": true,
"editor.minimap.enabled": false,
"editor.wordWrap": "on",
"terminal.integrated.defaultProfile.linux": "bash",
"yaml.schemas": {
"https://json.schemastore.org/github-workflow.json": ".github/workflows/*.yml"
},
"markdownlint.run": "onSave",
"rust-analyzer.cargo.features": "all",
"rust-analyzer.check.command": "clippy",
"rust-analyzer.check.allTargets": true,
Expand Down
8 changes: 4 additions & 4 deletions .devcontainer/welcome.sh
Original file line number Diff line number Diff line change
Expand Up @@ -17,13 +17,13 @@ echo ""
echo " TLA+ Model Checker:"
echo " tlc <spec.tla> # Run TLC model checker"
echo " sany <spec.tla> # Parse/check TLA+ spec"
echo " ./scripts/verify-tla.sh # Verify all TLA+ specs"
echo " ./scripts/verification/verify-tla.sh # Verify all TLA+ specs"
echo ""
echo " Kani (Bounded Model Checker for Rust):"
echo " cargo kani # Run all Kani proofs"
echo " cargo kani --harness <name> # Run specific proof"
echo " ./scripts/verify-kani.sh # Verify with helper script"
echo " ./scripts/check-kani-coverage.sh # Validate proof coverage"
echo " ./scripts/verification/verify-kani.sh # Verify with helper script"
echo " ./scripts/verification/check-kani-coverage.sh # Validate proof coverage"
echo ""
echo " Miri (Undefined Behavior Detection):"
echo " cargo +nightly miri test # Run tests under Miri"
Expand Down Expand Up @@ -63,7 +63,7 @@ echo " Profiling:"
echo " cargo flamegraph # Generate flame graphs"
echo ""
echo " All-in-one verification:"
echo " ./scripts/verify-all.sh # Run all verifiers"
echo " ./scripts/verification/verify-all.sh # Run all verifiers"
echo ""
echo " High-Performance CLI Tools (aliased, use instead of standard):"
echo " rg (ripgrep) → grep fd → find"
Expand Down
2 changes: 2 additions & 0 deletions .github/copilot-instructions.md
Original file line number Diff line number Diff line change
@@ -1,3 +1,5 @@
# GitHub Copilot Instructions for Fortress Rollback

**Read and follow [`.llm/context.md`](../.llm/context.md)** — the canonical source of truth for all project context, development policies, testing guidelines, and coding standards. You must read it before making any changes.

When clarifying questions are needed, follow [`.llm/templates/ask-user-question.md`](../.llm/templates/ask-user-question.md) to keep questions concise and actionable.
4 changes: 2 additions & 2 deletions .github/workflows/ci-benchmarks.yml
Original file line number Diff line number Diff line change
Expand Up @@ -59,7 +59,7 @@ jobs:
- name: Verify sccache is working
id: sccache-check
if: steps.sccache.outcome == 'success'
run: ./scripts/verify-sccache.sh
run: ./scripts/ci/verify-sccache.sh
continue-on-error: true

- name: Clear sccache env on failure
Expand Down Expand Up @@ -203,7 +203,7 @@ jobs:
- name: Verify sccache is working
id: sccache-check
if: steps.sccache.outcome == 'success'
run: ./scripts/verify-sccache.sh
run: ./scripts/ci/verify-sccache.sh
continue-on-error: true

- name: Clear sccache env on failure
Expand Down
12 changes: 6 additions & 6 deletions .github/workflows/ci-docs.yml
Original file line number Diff line number Diff line change
Expand Up @@ -157,7 +157,7 @@ jobs:
python-version: '3.12'

- name: Validate wiki consistency
run: python scripts/check-wiki-consistency.py
run: python scripts/docs/check-wiki-consistency.py

# ============================================================================
# SCRIPT TESTS & WIKI DRY-RUN - Run all script tests and validate wiki generation
Expand All @@ -181,10 +181,10 @@ jobs:
run: python -m pytest scripts/tests/ -v

- name: Generate wiki (dry-run)
run: python scripts/sync-wiki.py --dest wiki-test-output
run: python scripts/docs/sync-wiki.py --dest wiki-test-output

- name: Validate generated wiki format
run: python scripts/validate-wiki-output.py --wiki-dir wiki-test-output
run: python scripts/docs/validate-wiki-output.py --wiki-dir wiki-test-output

markdown-lint:
name: Markdown Lint
Expand Down Expand Up @@ -223,7 +223,7 @@ jobs:
echo ""
} >> "$GITHUB_STEP_SUMMARY"

if ./scripts/check-code-fence-syntax.sh docs/ 2>&1 | tee code-fence-output.txt; then
if ./scripts/docs/check-code-fence-syntax.sh docs/ 2>&1 | tee code-fence-output.txt; then
echo "✅ No rustdoc-style code fence attributes found" >> "$GITHUB_STEP_SUMMARY"
else
{
Expand Down Expand Up @@ -272,7 +272,7 @@ jobs:
continue-on-error: true # External links may have rate limits

- name: Check local file links
run: ./scripts/check-links.sh
run: ./scripts/docs/check-links.sh

# ============================================================================
# LYCHEE LINK CHECK - Fast link checking with caching
Expand Down Expand Up @@ -571,7 +571,7 @@ jobs:
} >> "$GITHUB_STEP_SUMMARY"

# Run verification on docs/ directory with fail-fast for CI
if ./scripts/verify-markdown-code.sh --fail-fast docs/ 2>&1 | tee markdown-code-output.txt; then
if ./scripts/docs/verify-markdown-code.sh --fail-fast docs/ 2>&1 | tee markdown-code-output.txt; then
echo "✅ All markdown code samples compile successfully" >> "$GITHUB_STEP_SUMMARY"
else
{
Expand Down
2 changes: 1 addition & 1 deletion .github/workflows/ci-llm-lint.yml
Original file line number Diff line number Diff line change
Expand Up @@ -20,4 +20,4 @@ jobs:
- name: Verify skills index is up-to-date
run: python scripts/hooks/regenerate-skills-index.py --check
- name: Check skill code example quality
run: bash scripts/check-llm-skills.sh
run: bash scripts/docs/check-llm-skills.sh
10 changes: 5 additions & 5 deletions .github/workflows/ci-network.yml
Original file line number Diff line number Diff line change
Expand Up @@ -8,7 +8,7 @@ on:
- '**/Cargo.toml'
- '**/Cargo.lock'
- 'docker/**'
- 'scripts/docker-network-tests.sh'
- 'scripts/ci/docker-network-tests.sh'
- '.github/workflows/ci-network.yml'
pull_request:
branches: [main]
Expand All @@ -17,7 +17,7 @@ on:
- '**/Cargo.toml'
- '**/Cargo.lock'
- 'docker/**'
- 'scripts/docker-network-tests.sh'
- 'scripts/ci/docker-network-tests.sh'
- '.github/workflows/ci-network.yml'
workflow_dispatch:

Expand Down Expand Up @@ -56,14 +56,14 @@ jobs:
- name: Verify sccache is working (Unix)
id: sccache-check-unix
if: steps.sccache.outcome == 'success' && runner.os != 'Windows'
run: ./scripts/verify-sccache.sh
run: ./scripts/ci/verify-sccache.sh
continue-on-error: true

- name: Verify sccache is working (Windows)
id: sccache-check-windows
if: steps.sccache.outcome == 'success' && runner.os == 'Windows'
shell: bash
run: ./scripts/verify-sccache.sh
run: ./scripts/ci/verify-sccache.sh
continue-on-error: true

- name: Set sccache working status
Expand Down Expand Up @@ -131,7 +131,7 @@ jobs:
run: docker compose -f docker/docker-compose.yml build

- name: Run Docker network tests (quick)
run: ./scripts/docker-network-tests.sh --quick
run: ./scripts/ci/docker-network-tests.sh --quick
timeout-minutes: 15

- name: Upload test results
Expand Down
18 changes: 9 additions & 9 deletions .github/workflows/ci-rust.yml
Original file line number Diff line number Diff line change
Expand Up @@ -12,8 +12,8 @@ on:
- 'Cross.toml'
- 'clippy.toml'
- 'rustfmt.toml'
- 'scripts/verify-kani.sh'
- 'scripts/check-kani-coverage.sh'
- 'scripts/verification/verify-kani.sh'
- 'scripts/verification/check-kani-coverage.sh'
- '.github/workflows/ci-rust.yml'
pull_request:
branches: [main]
Expand All @@ -26,8 +26,8 @@ on:
- 'Cross.toml'
- 'clippy.toml'
- 'rustfmt.toml'
- 'scripts/verify-kani.sh'
- 'scripts/check-kani-coverage.sh'
- 'scripts/verification/verify-kani.sh'
- 'scripts/verification/check-kani-coverage.sh'
- '.github/workflows/ci-rust.yml'
workflow_dispatch:

Expand All @@ -45,7 +45,7 @@ jobs:
- uses: actions/checkout@v6

- name: Validate Kani proof coverage
run: ./scripts/check-kani-coverage.sh
run: ./scripts/verification/check-kani-coverage.sh
# Ensures all #[kani::proof] functions are in tier lists in verify-kani.sh

# Primary build and test job (cross-platform matrix)
Expand Down Expand Up @@ -79,14 +79,14 @@ jobs:
- name: Verify sccache is working (Unix)
id: sccache-check-unix
if: steps.sccache.outcome == 'success' && runner.os != 'Windows'
run: ./scripts/verify-sccache.sh
run: ./scripts/ci/verify-sccache.sh
continue-on-error: true

- name: Verify sccache is working (Windows)
id: sccache-check-windows
if: steps.sccache.outcome == 'success' && runner.os == 'Windows'
shell: bash
run: ./scripts/verify-sccache.sh
run: ./scripts/ci/verify-sccache.sh
continue-on-error: true

- name: Set sccache working status
Expand Down Expand Up @@ -433,7 +433,7 @@ jobs:
- name: Verify sccache is working
id: sccache-check
if: steps.sccache.outcome == 'success'
run: ./scripts/verify-sccache.sh
run: ./scripts/ci/verify-sccache.sh
continue-on-error: true

- name: Clear sccache env on failure
Expand Down Expand Up @@ -522,7 +522,7 @@ jobs:
- name: Verify sccache is working
id: sccache-check
if: steps.sccache.outcome == 'success'
run: ./scripts/verify-sccache.sh
run: ./scripts/ci/verify-sccache.sh
continue-on-error: true

- name: Clear sccache env on failure
Expand Down
Loading
Loading