From 6ad7bf9de6be4bbebddd53282747d6c51f42e10a Mon Sep 17 00:00:00 2001 From: "Jonathan D.A. Jewell" <6759885+hyperpolymath@users.noreply.github.com> Date: Mon, 5 Oct 2026 17:24:34 +0100 Subject: [PATCH 1/7] feat: echidna integration, prove-result contract, id minting, CI repair - trust: compute levels with ECHIDNA's trust kernel and source axiom scanner (echidna-core-spark, git dep pinned to echidna main b761b3a) instead of the local re-implementation; output-text scan stays as labelled fallback - dispatcher: parse echidna.prove.result/1 (strict schema/status/I-JSON bounds), record trust provenance (receipt vs warrant), minimum-version handshake via /api/provers (MIN_ECHIDNA_VERSION 2.3.0), slug->name resolution from ECHIDNA's own prover list - config: default ECHIDNA endpoint http://127.0.0.1:8081; redacting Debug for forge tokens and webhook secrets - ids: src/ids.rs is the single minting module (UUIDv7 records, UUIDv8 JCS/SHA-256 content ids); all Uuid::new_v4 sites routed through it - ci: drop duplicate `with:` keys that broke cargo-audit, db-checks, publish, release and stress-test on main; refresh actions.lock; pin rust-toolchain 1.99.0; fix otel test needing a Tokio reactor - remove unused crytic/echidna Solidity fuzzing residue (contracts/, echidna/, scripts/echidna-gen.js, echidna-fuzz.yml) - docs: docs/ECHIDNA-INTEGRATION.adoc; 6a2 -> descriptiles wording Co-Authored-By: Claude Opus 5.5 --- .github/workflows/actions.lock | 77 +--- .github/workflows/cargo-audit.yml | 2 - .github/workflows/db-checks.yml | 2 - .github/workflows/echidna-fuzz.yml | 426 ------------------ .github/workflows/publish.yml | 2 - .github/workflows/release.yml | 2 - .github/workflows/stress-test.yml | 2 - .../descriptiles/0-AI-MANIFEST.a2ml | 4 +- .machine_readable/descriptiles/README.adoc | 2 +- Cargo.lock | 42 +- Cargo.toml | 20 +- README.adoc | 2 +- benches/echidnabot_bench.rs | 3 +- config/echidnabot.ncl | 4 +- contracts/Token.sol | 105 ----- contracts/TokenEchidnaTest.sol | 144 ------ docs/ECHIDNA-INTEGRATION.adoc | 151 +++++++ echidna/echidna-assertion.yaml | 44 -- echidna/echidna-ci.yaml | 44 -- echidna/echidna-config.yaml | 76 ---- echidna/echidna-no-flaky-assertion.yaml | 46 -- echidna/echidna-no-flaky.yaml | 75 --- echidnabot.example.toml | 4 +- echidnabot.toml | 4 +- rust-toolchain.toml | 15 + scripts/echidna-gen.js | 338 -------------- src/config.rs | 88 +++- src/dispatcher/echidna_client.rs | 350 ++++++++++++-- src/dispatcher/mod.rs | 35 +- src/dispatcher/prove_result.rs | 188 ++++++++ src/feedback/corpus_delta.rs | 3 +- src/feedback/reranker.rs | 7 +- src/fleet/mod.rs | 10 +- src/ids.rs | 113 +++++ src/lib.rs | 3 +- src/main.rs | 82 +++- src/observability.rs | 7 +- src/result_formatter.rs | 2 + src/scheduler/job_queue.rs | 8 +- src/scheduler/mod.rs | 8 +- src/store/models.rs | 40 +- src/store/sqlite.rs | 6 +- src/trust/axiom_tracker.rs | 162 ++++++- src/trust/confidence.rs | 267 ++++++----- tests/integration_tests.rs | 32 +- tests/lifecycle.rs | 29 +- tests/regressions/mod.rs | 4 +- 47 files changed, 1460 insertions(+), 1620 deletions(-) delete mode 100644 .github/workflows/echidna-fuzz.yml delete mode 100644 contracts/Token.sol delete mode 100644 contracts/TokenEchidnaTest.sol create mode 100644 docs/ECHIDNA-INTEGRATION.adoc delete mode 100644 echidna/echidna-assertion.yaml delete mode 100644 echidna/echidna-ci.yaml delete mode 100644 echidna/echidna-config.yaml delete mode 100644 echidna/echidna-no-flaky-assertion.yaml delete mode 100644 echidna/echidna-no-flaky.yaml create mode 100644 rust-toolchain.toml delete mode 100644 scripts/echidna-gen.js create mode 100644 src/dispatcher/prove_result.rs create mode 100644 src/ids.rs diff --git a/.github/workflows/actions.lock b/.github/workflows/actions.lock index 04c5707..bf554b2 100644 --- a/.github/workflows/actions.lock +++ b/.github/workflows/actions.lock @@ -14,7 +14,7 @@ workflows: - 'actions/configure-pages@v6.0.0' - 'actions/deploy-pages@v5.0.1' - 'actions/upload-pages-artifact@v5.0.0' - - 'haskell-actions/setup@v2.12.0' + - 'haskell-actions/setup@v2.12.1' '.github/workflows/cflite_batch.yml': - 'google/clusterfuzzlite@v1' '.github/workflows/cflite_pr.yml': @@ -26,7 +26,7 @@ workflows: - 'docker/build-push-action@v7.4.0' - 'docker/login-action@v4.6.0' - 'docker/metadata-action@v6.2.0' - - 'docker/setup-buildx-action@v4.4.0' + - 'docker/setup-buildx-action@v4.4.1' '.github/workflows/db-checks.yml': - 'actions/checkout@v7.0.1' - 'dtolnay/rust-toolchain@v1' @@ -38,16 +38,12 @@ workflows: - 'actions/checkout@v7.0.1' - 'actions/deploy-pages@v5.0.1' - 'actions/upload-pages-artifact@v5.0.0' - - 'haskell-actions/setup@v2.12.0' + - 'haskell-actions/setup@v2.12.1' '.github/workflows/dogfood-gate.yml': - 'actions/checkout@v7.0.1' '.github/workflows/e2e.yml': - 'actions/checkout@v7.0.1' - 'swatinem/rust-cache@v2.9.2' - '.github/workflows/echidna-fuzz.yml': - - 'actions/cache@v6.1.0' - - 'actions/checkout@v7.0.1' - - 'actions/upload-artifact@v7.0.1' '.github/workflows/echidnabot.yml': - 'actions/checkout@v7.0.1' '.github/workflows/governance.yml': [] @@ -163,9 +159,9 @@ dependencies: commit: 'sha1-dc802804100637a589fabce1cb79ff13a1411302' owner_id: 5429470 repo_id: 306769011 - 'docker/setup-buildx-action@v4.4.0': - ref: 'v4.4.0' - commit: 'sha1-594f3bf4285d9ea8dc53c9a0c9c4092420091003' + 'docker/setup-buildx-action@v4.4.1': + ref: 'v4.4.1' + commit: 'sha1-f87e5991a6d7451dcb8d9637bfbc97413f497069' owner_id: 5429470 repo_id: 288485773 'dtolnay/rust-toolchain@v1': @@ -183,9 +179,9 @@ dependencies: commit: 'sha1-884713a6c30a92e5e8544c39945cd7cb630abcd1' owner_id: 1342004 repo_id: 400046858 - 'haskell-actions/setup@v2.12.0': - ref: 'v2.12.0' - commit: 'sha1-6037f33647c3f17758a2356c80fc4a53d7e0685d' + 'haskell-actions/setup@v2.12.1': + ref: 'v2.12.1' + commit: 'sha1-0f8e8c99d88aeb3fbfd523f1ef2c6f762d10d64d' owner_id: 75048950 repo_id: 623796603 'softprops/action-gh-release@v3.0.3': @@ -198,58 +194,3 @@ dependencies: commit: 'sha1-6323deb102c322ba6fcbdcafc7e3dddab59af2b6' owner_id: 580492 repo_id: 298565987 - 'Swatinem/rust-cache@c19371144df3bb44fab255c43d04cbc2ab54d1c4': - ref: 'v2' - commit: 'sha1-c19371144df3bb44fab255c43d04cbc2ab54d1c4' - owner_id: 580492 - repo_id: 298565987 - 'actions/cache@55cc8345863c7cc4c66a329aec7e433d2d1c52a9': - ref: 'v6.1.0' - commit: 'sha1-55cc8345863c7cc4c66a329aec7e433d2d1c52a9' - owner_id: 44036562 - repo_id: 215566462 - 'actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1': - ref: 'v7.0.1' - commit: 'sha1-3d3c42e5aac5ba805825da76410c181273ba90b1' - owner_id: 44036562 - repo_id: 197814629 - 'actions/checkout@9c091bb21b7c1c1d1991bb908d89e4e9dddfe3e0': - ref: 'v7.0.0' - commit: 'sha1-9c091bb21b7c1c1d1991bb908d89e4e9dddfe3e0' - owner_id: 44036562 - repo_id: 197814629 - 'actions/upload-artifact@043fb46d1a93c77aae656e7c1c64a875d1fc6a0a': - ref: 'v7.0.1' - commit: 'sha1-043fb46d1a93c77aae656e7c1c64a875d1fc6a0a' - owner_id: 44036562 - repo_id: 192625955 - 'codecov/codecov-action@fb8b3582c8e4def4969c97caa2f19720cb33a72f': - ref: 'v7.0.0' - commit: 'sha1-fb8b3582c8e4def4969c97caa2f19720cb33a72f' - owner_id: 8226205 - repo_id: 200299178 - 'dtolnay/rust-toolchain@67ef31d5b988238dd797d409d6f9574278e20537': - ref: 'stable' - commit: 'sha1-67ef31d5b988238dd797d409d6f9574278e20537' - owner_id: 1940490 - repo_id: 260749683 - 'editorconfig-checker/action-editorconfig-checker@840e866d93b8e032123c23bac69dece044d4d84c': - ref: 'v2.2.0' - commit: 'sha1-840e866d93b8e032123c23bac69dece044d4d84c' - owner_id: 26415196 - repo_id: 297874902 - 'erlef/setup-beam@54075bcc5e249e4758d363f27d099f55d843f124': - ref: 'v1.24.1' - commit: 'sha1-54075bcc5e249e4758d363f27d099f55d843f124' - owner_id: 47606891 - repo_id: 331103973 - 'ossf/scorecard-action@4eaacf0543bb3f2c246792bd56e8cdeffafb205a': - ref: 'v2.4.3' - commit: 'sha1-4eaacf0543bb3f2c246792bd56e8cdeffafb205a' - owner_id: 67707773 - repo_id: 421101922 - 'webfactory/ssh-agent@e83874834305fe9a4a2997156cb26c5de65a8555': - ref: 'v0.10.0' - commit: 'sha1-e83874834305fe9a4a2997156cb26c5de65a8555' - owner_id: 135788 - repo_id: 208510314 diff --git a/.github/workflows/cargo-audit.yml b/.github/workflows/cargo-audit.yml index 7b488ac..505cc60 100644 --- a/.github/workflows/cargo-audit.yml +++ b/.github/workflows/cargo-audit.yml @@ -29,8 +29,6 @@ jobs: # the note in stress-test.yml. This SHA currently tolerates its absence; # stating it explicitly keeps the step working across future re-pins. uses: dtolnay/rust-toolchain@v1 - with: - toolchain: master with: toolchain: stable - name: Install cargo-audit diff --git a/.github/workflows/db-checks.yml b/.github/workflows/db-checks.yml index 5ffd95a..46960e4 100644 --- a/.github/workflows/db-checks.yml +++ b/.github/workflows/db-checks.yml @@ -45,8 +45,6 @@ jobs: # the note in stress-test.yml. This SHA currently tolerates its absence; # stating it explicitly keeps the step working across future re-pins. uses: dtolnay/rust-toolchain@v1 - with: - toolchain: master with: toolchain: stable diff --git a/.github/workflows/echidna-fuzz.yml b/.github/workflows/echidna-fuzz.yml deleted file mode 100644 index 6b55d5d..0000000 --- a/.github/workflows/echidna-fuzz.yml +++ /dev/null @@ -1,426 +0,0 @@ -# This workflow is managed by gh actions-lock. -# SPDX-License-Identifier: MPL-2.0 -# This workflow is managed by gh actions-lock. -name: Echidna Smart Contract Fuzzing -permissions: - contents: read - checks: write - pull-requests: write -# ═══════════════════════════════════════════════════════════════════════════════ -# RATE LIMITING: Only one fuzzing run per PR/branch at a time -# New pushes cancel in-progress runs to save resources -# ═══════════════════════════════════════════════════════════════════════════════ -concurrency: - group: echidna-fuzz-${{ github.workflow }}-${{ github.event.pull_request.number || github.ref }} - cancel-in-progress: true -on: - push: - branches: [main] - paths: - - 'contracts/**/*.sol' - - 'echidna/**' - - '.github/workflows/echidna-fuzz.yml' - pull_request: - paths: - - 'contracts/**/*.sol' - - 'echidna/**' - - '.github/workflows/echidna-fuzz.yml' - workflow_dispatch: - inputs: - contract: - description: 'Contract to test (e.g., TokenEchidnaTest)' - required: false - default: '' - type: string - test_limit: - description: 'Number of test iterations' - required: false - default: '10000' - type: string - test_mode: - description: 'Echidna test mode' - required: false - default: 'property' - type: choice - options: - - property - - assertion - - optimization - - overflow - - exploration - no_flaky: - description: 'Enable no-flaky-tests mode (deterministic, multi-pass verification)' - required: false - default: false - type: boolean - seed: - description: 'Fixed seed for reproducibility (0 = random)' - required: false - default: '0' - type: string -env: - SOLC_VERSION: "0.8.19" - ECHIDNA_VERSION: "2.2.3" - # Rate limit: Maximum contracts to test in parallel - MAX_PARALLEL_CONTRACTS: 3 - # Timeout for individual test runs (seconds) - TEST_TIMEOUT: 600 - # No-flaky mode: Number of verification passes required - VERIFICATION_PASSES: 3 -jobs: - # ═══════════════════════════════════════════════════════════════════════════ - # RATE LIMIT CHECK: Prevent abuse and resource exhaustion - # ═══════════════════════════════════════════════════════════════════════════ - rate-limit-check: - name: Rate Limit Check - runs-on: ubuntu-latest - timeout-minutes: 5 - outputs: - allowed: ${{ steps.check.outputs.allowed }} - reason: ${{ steps.check.outputs.reason }} - steps: - - name: Check rate limits - id: check - run: | - # Check if this is a scheduled/automated run vs manual - if [ "${{ github.event_name }}" = "schedule" ]; then - echo "allowed=true" >> $GITHUB_OUTPUT - echo "reason=scheduled" >> $GITHUB_OUTPUT - exit 0 - fi - - # For PRs, check if the author has permission - if [ "${{ github.event_name }}" = "pull_request" ]; then - AUTHOR="${{ github.event.pull_request.user.login }}" - # Allow all PR authors but log for monitoring - echo "::notice::Fuzzing triggered by PR author: $AUTHOR" - fi - - # Check workflow run count in last hour (basic rate limiting) - # In production, this would query GitHub API for recent workflow runs - echo "allowed=true" >> $GITHUB_OUTPUT - echo "reason=within_limits" >> $GITHUB_OUTPUT - detect-contracts: - name: Detect Solidity contracts - needs: rate-limit-check - if: needs.rate-limit-check.outputs.allowed == 'true' - runs-on: ubuntu-latest - timeout-minutes: 5 - outputs: - has_contracts: ${{ steps.detect.outputs.has_contracts }} - has_echidna_tests: ${{ steps.detect.outputs.has_echidna_tests }} - contracts: ${{ steps.detect.outputs.contracts }} - contract_count: ${{ steps.detect.outputs.contract_count }} - steps: - - uses: actions/checkout@v7.0.1 - - name: Detect contract files - id: detect - run: | - # Find all Solidity files - contract_count=$(find contracts -name "*.sol" -type f 2>/dev/null | wc -l) - - # Find Echidna test contracts (contain "echidna_" functions) - echidna_tests=$(grep -rl "echidna_" contracts/*.sol 2>/dev/null | xargs -I{} basename {} .sol | tr '\n' ',' | sed 's/,$//' || echo "") - - # Count test contracts for rate limiting - test_count=$(echo "$echidna_tests" | tr ',' '\n' | grep -c . || echo 0) - - # Rate limit: Cap number of contracts - if [ "$test_count" -gt "${{ env.MAX_PARALLEL_CONTRACTS }}" ]; then - echo "::warning::Found $test_count test contracts, limiting to ${{ env.MAX_PARALLEL_CONTRACTS }}" - echidna_tests=$(echo "$echidna_tests" | tr ',' '\n' | head -${{ env.MAX_PARALLEL_CONTRACTS }} | tr '\n' ',' | sed 's/,$//') - fi - - echo "has_contracts=$([[ $contract_count -gt 0 ]] && echo true || echo false)" >> $GITHUB_OUTPUT - echo "has_echidna_tests=$([[ -n "$echidna_tests" ]] && echo true || echo false)" >> $GITHUB_OUTPUT - contracts_json=$(printf '%s' "$echidna_tests" | jq -Rc 'split(",") | map(select(length > 0))') - echo "contracts=$contracts_json" >> "$GITHUB_OUTPUT" - echo "contract_count=$test_count" >> $GITHUB_OUTPUT - - echo "::notice::Found $contract_count Solidity files, Echidna tests: $echidna_tests (limited to ${{ env.MAX_PARALLEL_CONTRACTS }} max)" - # ═══════════════════════════════════════════════════════════════════════════ - # PROPERTY TESTING with safeguards - # ═══════════════════════════════════════════════════════════════════════════ - echidna-property-test: - name: Echidna Property Testing - needs: detect-contracts - if: needs.detect-contracts.outputs.has_echidna_tests == 'true' - runs-on: ubuntu-latest - timeout-minutes: 30 - strategy: - fail-fast: false - max-parallel: 2 # Rate limit: max 2 concurrent test jobs - matrix: - contract: ${{ fromJson(needs.detect-contracts.outputs.contracts) }} - steps: - - uses: actions/checkout@v7.0.1 - - name: Restore Echidna corpus cache - uses: actions/cache@v6.1.0 - with: - path: echidna-corpus - key: echidna-corpus-${{ matrix.contract }}-${{ hashFiles(format('contracts/{0}.sol', matrix.contract)) }} - restore-keys: | - echidna-corpus-${{ matrix.contract }}- - - name: Install pinned Solidity and Echidna binaries - run: | - set -euo pipefail - install_dir="${RUNNER_TEMP}/solidity-fuzz-tools" - mkdir -p "$install_dir" - curl -fL --retry 3 -o "$install_dir/solc" "https://github.com/ethereum/solidity/releases/download/v${SOLC_VERSION}/solc-static-linux" - echo "7a5c1d3dc9a8eba62bb2ec37192c9178ae5fe8a54a56e5573fd3c9c17cd9eb48 $install_dir/solc" | sha256sum --check - curl -fL --retry 3 -o "$install_dir/echidna.tar.gz" "https://github.com/crytic/echidna/releases/download/v${ECHIDNA_VERSION}/echidna-${ECHIDNA_VERSION}-x86_64-linux.tar.gz" - echo "d33c0451bb3bb65c76445d2dbfcd1102dab7a27a8d450197dabd3f06bed76067 $install_dir/echidna.tar.gz" | sha256sum --check - tar -xzf "$install_dir/echidna.tar.gz" -C "$install_dir" echidna - chmod +x "$install_dir/solc" "$install_dir/echidna" - echo "$install_dir" >> "$GITHUB_PATH" - "$install_dir/solc" --version - "$install_dir/echidna" --version - - name: Install pinned Solidity compiler adapter - run: | - python3 -m venv "${RUNNER_TEMP}/crytic-compile" - "${RUNNER_TEMP}/crytic-compile/bin/pip" install 'crytic-compile==0.4.2' - echo "${RUNNER_TEMP}/crytic-compile/bin" >> "$GITHUB_PATH" - - name: Run Echidna property tests - id: echidna - run: | - # The adapter installs a solc-select shim; prefer the checksum-pinned compiler. - export PATH="${RUNNER_TEMP}/solidity-fuzz-tools:$PATH" - test "$(command -v solc)" = "${RUNNER_TEMP}/solidity-fuzz-tools/solc" - echo "::group::Echidna Property Testing - ${{ matrix.contract }}" - - CONTRACT_FILE="contracts/${{ matrix.contract }}.sol" - NO_FLAKY="${{ github.event.inputs.no_flaky || 'false' }}" - SEED="${{ github.event.inputs.seed || '0' }}" - - # Select config based on mode - if [ "$NO_FLAKY" = "true" ]; then - CONFIG_FILE="echidna/echidna-no-flaky.yaml" - echo "::notice::Running in NO-FLAKY mode with deterministic settings" - else - CONFIG_FILE="echidna/echidna-ci.yaml" - fi - - if [ ! -f "$CONTRACT_FILE" ]; then - echo "::error::Contract file not found: $CONTRACT_FILE" - exit 1 - fi - - mkdir -p echidna-results - - # Build Echidna command - ECHIDNA_CMD="echidna $CONTRACT_FILE --contract ${{ matrix.contract }} --config $CONFIG_FILE --format json" - - # Add fixed seed if specified (for reproducibility) - if [ "$SEED" != "0" ]; then - ECHIDNA_CMD="$ECHIDNA_CMD --seed $SEED" - echo "::notice::Using fixed seed: $SEED" - fi - - # NO-FLAKY MODE: Run multiple passes and require all to agree - if [ "$NO_FLAKY" = "true" ]; then - echo "Running ${{ env.VERIFICATION_PASSES }} verification passes..." - PASS_COUNT=0 - FAIL_COUNT=0 - - for i in $(seq 1 ${{ env.VERIFICATION_PASSES }}); do - echo "=== Pass $i/${{ env.VERIFICATION_PASSES }} ===" - - # Use consistent seed across passes if not specified - if [ "$SEED" = "0" ]; then - PASS_SEED=$((42 + i)) - PASS_CMD="$ECHIDNA_CMD --seed $PASS_SEED" - else - PASS_CMD="$ECHIDNA_CMD" - fi - - set +e - timeout ${{ env.TEST_TIMEOUT }} $PASS_CMD 2>&1 | tee "echidna-results/pass-$i.json" - PASS_EXIT=${PIPESTATUS[0]} - set -e - - if [ $PASS_EXIT -eq 0 ]; then - PASS_COUNT=$((PASS_COUNT + 1)) - echo "Pass $i: SUCCESS" - else - FAIL_COUNT=$((FAIL_COUNT + 1)) - echo "Pass $i: FAILURE" - fi - done - - echo "" - echo "=== Verification Summary ===" - echo "Passed: $PASS_COUNT / ${{ env.VERIFICATION_PASSES }}" - echo "Failed: $FAIL_COUNT / ${{ env.VERIFICATION_PASSES }}" - - # Require ALL passes to succeed in no-flaky mode - if [ $FAIL_COUNT -gt 0 ]; then - echo "result=flaky" >> $GITHUB_OUTPUT - echo "passes=$PASS_COUNT" >> $GITHUB_OUTPUT - echo "::error::Test is FLAKY - failed $FAIL_COUNT of ${{ env.VERIFICATION_PASSES }} passes" - exit 1 - else - echo "result=stable" >> $GITHUB_OUTPUT - echo "passes=$PASS_COUNT" >> $GITHUB_OUTPUT - echo "::notice::Test is STABLE - passed all ${{ env.VERIFICATION_PASSES }} verification passes" - fi - else - # Standard single-pass mode with timeout - set +e - timeout ${{ env.TEST_TIMEOUT }} $ECHIDNA_CMD 2>&1 | tee echidna-results/property-test.json - ECHIDNA_EXIT=${PIPESTATUS[0]} - set -e - - echo "::endgroup::" - - if [ $ECHIDNA_EXIT -eq 124 ]; then - echo "result=timeout" >> $GITHUB_OUTPUT - echo "::error::Echidna test timed out after ${{ env.TEST_TIMEOUT }} seconds" - exit 1 - elif [ $ECHIDNA_EXIT -eq 0 ]; then - echo "result=success" >> $GITHUB_OUTPUT - echo "::notice::All property tests passed!" - else - echo "result=failure" >> $GITHUB_OUTPUT - echo "::error::Echidna run failed; inspect output for compiler errors or counterexamples" - exit $ECHIDNA_EXIT - fi - fi - - name: Save corpus cache - if: always() - uses: actions/cache/save@v6.1.0 - with: - path: echidna-corpus - key: echidna-corpus-${{ matrix.contract }}-${{ hashFiles(format('contracts/{0}.sol', matrix.contract)) }} - - name: Upload Echidna results - if: always() - uses: actions/upload-artifact@v7.0.1 - with: - name: echidna-property-results-${{ matrix.contract }} - path: echidna-results/ - retention-days: 30 - # ═══════════════════════════════════════════════════════════════════════════ - # ASSERTION TESTING with safeguards - # ═══════════════════════════════════════════════════════════════════════════ - echidna-assertion-test: - name: Echidna Assertion Testing - needs: detect-contracts - if: needs.detect-contracts.outputs.has_echidna_tests == 'true' - runs-on: ubuntu-latest - timeout-minutes: 30 - strategy: - fail-fast: false - max-parallel: 2 - matrix: - contract: ${{ fromJson(needs.detect-contracts.outputs.contracts) }} - steps: - - uses: actions/checkout@v7.0.1 - - name: Restore Echidna corpus cache - uses: actions/cache@v6.1.0 - with: - path: echidna-corpus-assertion - key: echidna-corpus-assertion-${{ matrix.contract }}-${{ hashFiles(format('contracts/{0}.sol', matrix.contract)) }} - restore-keys: | - echidna-corpus-assertion-${{ matrix.contract }}- - - name: Install pinned Solidity and Echidna binaries - run: | - set -euo pipefail - install_dir="${RUNNER_TEMP}/solidity-fuzz-tools" - mkdir -p "$install_dir" - curl -fL --retry 3 -o "$install_dir/solc" "https://github.com/ethereum/solidity/releases/download/v${SOLC_VERSION}/solc-static-linux" - echo "7a5c1d3dc9a8eba62bb2ec37192c9178ae5fe8a54a56e5573fd3c9c17cd9eb48 $install_dir/solc" | sha256sum --check - curl -fL --retry 3 -o "$install_dir/echidna.tar.gz" "https://github.com/crytic/echidna/releases/download/v${ECHIDNA_VERSION}/echidna-${ECHIDNA_VERSION}-x86_64-linux.tar.gz" - echo "d33c0451bb3bb65c76445d2dbfcd1102dab7a27a8d450197dabd3f06bed76067 $install_dir/echidna.tar.gz" | sha256sum --check - tar -xzf "$install_dir/echidna.tar.gz" -C "$install_dir" echidna - chmod +x "$install_dir/solc" "$install_dir/echidna" - echo "$install_dir" >> "$GITHUB_PATH" - "$install_dir/solc" --version - "$install_dir/echidna" --version - - name: Install pinned Solidity compiler adapter - run: | - python3 -m venv "${RUNNER_TEMP}/crytic-compile" - "${RUNNER_TEMP}/crytic-compile/bin/pip" install 'crytic-compile==0.4.2' - echo "${RUNNER_TEMP}/crytic-compile/bin" >> "$GITHUB_PATH" - - name: Run Echidna assertion tests - id: echidna - run: | - export PATH="${RUNNER_TEMP}/solidity-fuzz-tools:$PATH" - test "$(command -v solc)" = "${RUNNER_TEMP}/solidity-fuzz-tools/solc" - echo "::group::Echidna Assertion Testing - ${{ matrix.contract }}" - - CONTRACT_FILE="contracts/${{ matrix.contract }}.sol" - NO_FLAKY="${{ github.event.inputs.no_flaky || 'false' }}" - - if [ "$NO_FLAKY" = "true" ]; then - CONFIG_FILE="echidna/echidna-no-flaky-assertion.yaml" - else - CONFIG_FILE="echidna/echidna-assertion.yaml" - fi - - mkdir -p echidna-results - - set +e - timeout ${{ env.TEST_TIMEOUT }} echidna "$CONTRACT_FILE" \ - --contract "${{ matrix.contract }}" \ - --config "$CONFIG_FILE" \ - --format text \ - 2>&1 | tee echidna-results/assertion-test.txt - - ECHIDNA_EXIT=${PIPESTATUS[0]} - set -e - - echo "::endgroup::" - - if [ $ECHIDNA_EXIT -eq 124 ]; then - echo "::error::Assertion test timed out after ${{ env.TEST_TIMEOUT }} seconds" - exit 1 - elif [ $ECHIDNA_EXIT -eq 0 ]; then - echo "::notice::All assertion tests passed!" - else - echo "::error::Echidna assertion run failed; inspect output for compiler errors or counterexamples" - exit "$ECHIDNA_EXIT" - fi - - name: Upload Echidna results - if: always() - uses: actions/upload-artifact@v7.0.1 - with: - name: echidna-assertion-results-${{ matrix.contract }} - path: echidna-results/ - retention-days: 30 - summary: - name: Fuzzing Summary - needs: [detect-contracts, echidna-property-test, echidna-assertion-test] - if: always() && needs.detect-contracts.outputs.has_echidna_tests == 'true' - runs-on: ubuntu-latest - timeout-minutes: 5 - steps: - - name: Generate summary - run: | - NO_FLAKY="${{ github.event.inputs.no_flaky || 'false' }}" - - echo "## Echidna Smart Contract Fuzzing Summary" >> $GITHUB_STEP_SUMMARY - echo "" >> $GITHUB_STEP_SUMMARY - - # Show safeguard status - echo "### Safeguards" >> $GITHUB_STEP_SUMMARY - echo "| Setting | Value |" >> $GITHUB_STEP_SUMMARY - echo "|---------|-------|" >> $GITHUB_STEP_SUMMARY - echo "| Rate Limit (max parallel) | ${{ env.MAX_PARALLEL_CONTRACTS }} contracts |" >> $GITHUB_STEP_SUMMARY - echo "| Test Timeout | ${{ env.TEST_TIMEOUT }}s |" >> $GITHUB_STEP_SUMMARY - echo "| No-Flaky Mode | $NO_FLAKY |" >> $GITHUB_STEP_SUMMARY - if [ "$NO_FLAKY" = "true" ]; then - echo "| Verification Passes | ${{ env.VERIFICATION_PASSES }} |" >> $GITHUB_STEP_SUMMARY - fi - echo "" >> $GITHUB_STEP_SUMMARY - - echo "### Test Results" >> $GITHUB_STEP_SUMMARY - echo "| Test Type | Contract | Status |" >> $GITHUB_STEP_SUMMARY - echo "|-----------|----------|--------|" >> $GITHUB_STEP_SUMMARY - echo "| Property Tests | ${{ needs.detect-contracts.outputs.contracts }} | ${{ needs.echidna-property-test.result }} |" >> $GITHUB_STEP_SUMMARY - echo "| Assertion Tests | ${{ needs.detect-contracts.outputs.contracts }} | ${{ needs.echidna-assertion-test.result }} |" >> $GITHUB_STEP_SUMMARY - echo "" >> $GITHUB_STEP_SUMMARY - echo "### Configuration" >> $GITHUB_STEP_SUMMARY - echo "- Solidity Version: ${{ env.SOLC_VERSION }}" >> $GITHUB_STEP_SUMMARY - echo "- Echidna Version: ${{ env.ECHIDNA_VERSION }}" >> $GITHUB_STEP_SUMMARY - echo "- Contracts Tested: ${{ needs.detect-contracts.outputs.contract_count }}" >> $GITHUB_STEP_SUMMARY - echo "" >> $GITHUB_STEP_SUMMARY - echo "_Fuzzed by [echidnabot](https://github.com/hyperpolymath/echidnabot)_" >> $GITHUB_STEP_SUMMARY diff --git a/.github/workflows/publish.yml b/.github/workflows/publish.yml index 8ea3348..8731264 100644 --- a/.github/workflows/publish.yml +++ b/.github/workflows/publish.yml @@ -36,8 +36,6 @@ jobs: uses: actions/checkout@v7.0.1 - name: Install Rust toolchain uses: dtolnay/rust-toolchain@v1 - with: - toolchain: master with: toolchain: stable - name: Cache cargo diff --git a/.github/workflows/release.yml b/.github/workflows/release.yml index 53487fa..3ea73c0 100644 --- a/.github/workflows/release.yml +++ b/.github/workflows/release.yml @@ -52,8 +52,6 @@ jobs: # the note in stress-test.yml. Supplying `targets:` alone does not # satisfy it. uses: dtolnay/rust-toolchain@v1 - with: - toolchain: master with: toolchain: stable targets: ${{ matrix.target }} diff --git a/.github/workflows/stress-test.yml b/.github/workflows/stress-test.yml index 58361ff..8c34a3c 100644 --- a/.github/workflows/stress-test.yml +++ b/.github/workflows/stress-test.yml @@ -19,8 +19,6 @@ jobs: # "stable"), and a SHA carries no such name. Without it the action fails # with `error: invalid toolchain name ''`. uses: dtolnay/rust-toolchain@v1 - with: - toolchain: master with: toolchain: stable diff --git a/.machine_readable/descriptiles/0-AI-MANIFEST.a2ml b/.machine_readable/descriptiles/0-AI-MANIFEST.a2ml index 6bf1f8c..8a68487 100644 --- a/.machine_readable/descriptiles/0-AI-MANIFEST.a2ml +++ b/.machine_readable/descriptiles/0-AI-MANIFEST.a2ml @@ -1,8 +1,8 @@ -# AI Manifest for 6a2 Directory +# AI Manifest for the descriptiles Directory ## Purpose -This manifest declares the AI-assistant context for the 6a2 machine-readable metadata directory. +This manifest declares the AI-assistant context for the descriptiles machine-readable metadata directory. ## Canonical Locations diff --git a/.machine_readable/descriptiles/README.adoc b/.machine_readable/descriptiles/README.adoc index 916a702..a565c83 100644 --- a/.machine_readable/descriptiles/README.adoc +++ b/.machine_readable/descriptiles/README.adoc @@ -1,6 +1,6 @@ // SPDX-License-Identifier: CC-BY-SA-4.0 // Copyright (c) Jonathan D.A. Jewell -# A2ML 6a2 Directory +# A2ML descriptiles Directory (formerly `6a2/`, retired estate-wide) This directory contains the 6 core A2ML machine-readable metadata files for this repository. diff --git a/Cargo.lock b/Cargo.lock index 7743221..d24802f 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -247,13 +247,13 @@ dependencies = [ [[package]] name = "async-trait" -version = "0.1.89" +version = "0.1.92" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "9035ad2d096bed7955a320ee7e2230574d28fd3c3a0f186cbea1ff3c7eed5dbb" +checksum = "82f6aeea286b8eb4dd3431a1be1b59d290ace00f5bfd8e2a159bc2a05e2c1667" dependencies = [ "proc-macro2", "quote", - "syn 2.0.117", + "syn 3.0.3", ] [[package]] @@ -1108,6 +1108,14 @@ version = "1.0.5" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "92773504d58c093f6de2459af4af33faa518c13451eb8f2b5698ed3d36e7c813" +[[package]] +name = "echidna-core-spark" +version = "0.1.0" +source = "git+https://github.com/hyperpolymath/echidna?rev=b761b3a832981be51d4e88076ef1b90fe5037e9c#b761b3a832981be51d4e88076ef1b90fe5037e9c" +dependencies = [ + "serde", +] + [[package]] name = "echidnabot" version = "0.1.0" @@ -1122,6 +1130,7 @@ dependencies = [ "clap", "config", "criterion", + "echidna-core-spark", "gitbot-shared-context", "hex", "hmac 0.13.0", @@ -1133,8 +1142,10 @@ dependencies = [ "proptest", "rand 0.10.2", "reqwest 0.12.28", + "semver", "serde", "serde_json", + "serde_json_canonicalizer", "sha2 0.11.0", "sqlx", "tempfile", @@ -3443,9 +3454,9 @@ dependencies = [ [[package]] name = "rustls" -version = "0.23.40" +version = "0.23.45" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "ef86cd5876211988985292b91c96a8f2d298df24e75989a43a3c73f2d4d8168b" +checksum = "0d41d731c7d2f962d1ccc364cec258de3c0e93b38c2fb3ba97ac74513048d634" dependencies = [ "log", "once_cell", @@ -3480,9 +3491,9 @@ dependencies = [ [[package]] name = "rustls-webpki" -version = "0.103.13" +version = "0.103.15" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "61c429a8649f110dddef65e2a5ad240f747e85f7758a6bccc7e5777bd33f756e" +checksum = "f3c3cf1d8b1e7d4927e2d154c3fcb02979afb9939629c62cd9048d4f07b60ac2" dependencies = [ "ring", "rustls-pki-types", @@ -3513,6 +3524,12 @@ version = "1.0.23" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "9774ba4a74de5f7b1c1451ed6cd5285a32eddb5cccb8cc655a4e50009e06477f" +[[package]] +name = "ryu-js" +version = "1.0.3" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "04d056b875a9d2e6cb9a61d127afee9ac5999b9f87bcb32079d1318e505be714" + [[package]] name = "same-file" version = "1.0.6" @@ -3634,6 +3651,17 @@ dependencies = [ "zmij", ] +[[package]] +name = "serde_json_canonicalizer" +version = "0.3.2" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "fe52319a927259afbfa5180c5157cd8167edfd3e8c254f9558c7fef44c5649f2" +dependencies = [ + "ryu-js", + "serde", + "serde_json", +] + [[package]] name = "serde_path_to_error" version = "0.1.20" diff --git a/Cargo.toml b/Cargo.toml index 902523a..4a9ac68 100644 --- a/Cargo.toml +++ b/Cargo.toml @@ -28,6 +28,19 @@ path = "src/main.rs" # Fleet coordination gitbot-shared-context = { version = "0.1.0", git = "https://github.com/hyperpolymath/gitbot-fleet", rev = "40ef6bf1a43813948476d33c764e3405adc950c2" } +# ECHIDNA trust kernel. Canonical trust-level algorithm and source-level +# axiom scanner, shared with ECHIDNA so echidnabot no longer re-implements +# them. Pinned by full rev (immutable). At this rev the crate is still named +# `echidna-core-spark`; it is being renamed `echidna-core-creusot` upstream, +# and the trust types are meant to move into `echidna-core` proper. Follow-up: +# re-point this line once that lands on echidna `main` (see +# docs/ECHIDNA-INTEGRATION.adoc). +echidna-core-spark = { git = "https://github.com/hyperpolymath/echidna", rev = "b761b3a832981be51d4e88076ef1b90fe5037e9c" } + +# Minimum-version handshake with the ECHIDNA server. +semver = "1" + + # Async runtime tokio = { version = "1", features = ["full"] } @@ -70,7 +83,12 @@ reqwest = { version = "0.12", default-features = false, features = ["json", "rus # Utilities async-trait = "0.1" -uuid = { version = "1", features = ["v4", "serde"] } +# v7 for records, v8 for content ids; minted only in src/ids.rs. +uuid = { version = "1.10", features = ["v7", "v8", "serde"] } +# RFC 8785 (JCS) canonical bytes for src/ids.rs content ids. The estate +# crate hyperpolymath/ijson-jcs is not public, so a public build cannot +# depend on it; swap once it is (docs/ECHIDNA-INTEGRATION.adoc). +serde_json_canonicalizer = "0.3" chrono = { version = "0.4", features = ["serde"] } thiserror = "2" anyhow = "1" diff --git a/README.adoc b/README.adoc index 8ec330c..edd52bd 100644 --- a/README.adoc +++ b/README.adoc @@ -72,7 +72,7 @@ echidnabot init-db # Start the webhook server export DATABASE_URL=sqlite:echidnabot.db -export ECHIDNA_URL=http://localhost:8080 +export ECHIDNA_URL=http://127.0.0.1:8081 echidnabot serve --port 8080 ---- diff --git a/benches/echidnabot_bench.rs b/benches/echidnabot_bench.rs index 4605a68..7f84d71 100644 --- a/benches/echidnabot_bench.rs +++ b/benches/echidnabot_bench.rs @@ -24,7 +24,6 @@ use sha2::Sha256; // one; CI runs clippy with `-D warnings`, so the re-export is an error here. use std::hint::black_box; use std::net::{IpAddr, Ipv4Addr}; -use uuid::Uuid; // ────────────────────────────────────────────────────────────────────────────── // HMAC-SHA256 webhook signature verification @@ -158,7 +157,7 @@ fn bench_goal_fingerprint(c: &mut Criterion) { // ────────────────────────────────────────────────────────────────────────────── fn bench_proof_job_new(c: &mut Criterion) { - let repo = Uuid::new_v4(); + let repo = echidnabot::ids::new_record_id(); let prover = ProverKind::new("coq"); let files = vec![ "theories/Main.v".to_string(), diff --git a/config/echidnabot.ncl b/config/echidnabot.ncl index f31ac6e..6de5ba9 100644 --- a/config/echidnabot.ncl +++ b/config/echidnabot.ncl @@ -91,8 +91,8 @@ let Config = { max_connections = 5, }, echidna = { - endpoint = "http://localhost:8080/graphql", - rest_endpoint = "http://localhost:8080", + endpoint = "http://127.0.0.1:8081/graphql", + rest_endpoint = "http://127.0.0.1:8081", mode = 'auto, timeout_seconds = 120, }, diff --git a/contracts/Token.sol b/contracts/Token.sol deleted file mode 100644 index e460d87..0000000 --- a/contracts/Token.sol +++ /dev/null @@ -1,105 +0,0 @@ -// SPDX-License-Identifier: MPL-2.0 -// Copyright (C) 2024 Jonathan D.A. Jewell / Hyperpolymath - -pragma solidity ^0.8.19; - -/// @title Token - A simple ERC20-like token for Echidna testing demonstration -/// @notice This contract demonstrates common patterns that Echidna can fuzz test -contract Token { - string public name = "TestToken"; - string public symbol = "TST"; - uint8 public constant decimals = 18; - uint256 public totalSupply; - - mapping(address => uint256) public balanceOf; - mapping(address => mapping(address => uint256)) public allowance; - - address public owner; - bool public paused; - - event Transfer(address indexed from, address indexed to, uint256 value); - event Approval(address indexed owner, address indexed spender, uint256 value); - event Paused(address account); - event Unpaused(address account); - - modifier onlyOwner() { - require(msg.sender == owner, "Token: caller is not the owner"); - _; - } - - modifier whenNotPaused() { - require(!paused, "Token: paused"); - _; - } - - constructor(uint256 initialSupply) { - owner = msg.sender; - totalSupply = initialSupply; - balanceOf[msg.sender] = initialSupply; - } - - function transfer(address to, uint256 amount) public whenNotPaused returns (bool) { - require(to != address(0), "Token: transfer to zero address"); - require(balanceOf[msg.sender] >= amount, "Token: insufficient balance"); - - balanceOf[msg.sender] -= amount; - balanceOf[to] += amount; - - emit Transfer(msg.sender, to, amount); - return true; - } - - function approve(address spender, uint256 amount) public whenNotPaused returns (bool) { - require(spender != address(0), "Token: approve to zero address"); - - allowance[msg.sender][spender] = amount; - emit Approval(msg.sender, spender, amount); - return true; - } - - function transferFrom( - address from, - address to, - uint256 amount - ) public whenNotPaused returns (bool) { - require(from != address(0), "Token: transfer from zero address"); - require(to != address(0), "Token: transfer to zero address"); - require(balanceOf[from] >= amount, "Token: insufficient balance"); - require(allowance[from][msg.sender] >= amount, "Token: insufficient allowance"); - - allowance[from][msg.sender] -= amount; - balanceOf[from] -= amount; - balanceOf[to] += amount; - - emit Transfer(from, to, amount); - return true; - } - - function mint(address to, uint256 amount) public onlyOwner whenNotPaused { - require(to != address(0), "Token: mint to zero address"); - - totalSupply += amount; - balanceOf[to] += amount; - - emit Transfer(address(0), to, amount); - } - - function burn(uint256 amount) public whenNotPaused { - require(balanceOf[msg.sender] >= amount, "Token: burn exceeds balance"); - - balanceOf[msg.sender] -= amount; - totalSupply -= amount; - - emit Transfer(msg.sender, address(0), amount); - } - - function pause() public onlyOwner { - paused = true; - emit Paused(msg.sender); - } - - function unpause() public onlyOwner { - paused = false; - emit Unpaused(msg.sender); - } -} diff --git a/contracts/TokenEchidnaTest.sol b/contracts/TokenEchidnaTest.sol deleted file mode 100644 index e15448d..0000000 --- a/contracts/TokenEchidnaTest.sol +++ /dev/null @@ -1,144 +0,0 @@ -// SPDX-License-Identifier: MPL-2.0 -// Copyright (C) 2024 Jonathan D.A. Jewell / Hyperpolymath - -pragma solidity ^0.8.19; - -import "./Token.sol"; - -/// @title TokenEchidnaTest - Echidna fuzz testing properties for Token contract -/// @notice This contract defines invariants and properties that Echidna will attempt to break -/// @dev All functions starting with "echidna_" are treated as invariant tests -/// All functions starting with "test_" can be used for property exploration -contract TokenEchidnaTest is Token { - // Track initial state for invariant checking - uint256 private initialTotalSupply; - address private constant ECHIDNA_SENDER = address(0x10000); - address private constant ECHIDNA_RECEIVER = address(0x20000); - - constructor() Token(1_000_000 * 10 ** 18) { - initialTotalSupply = totalSupply; - // Give Echidna addresses some tokens to work with - balanceOf[msg.sender] -= 100_000 * 10 ** 18; - balanceOf[ECHIDNA_SENDER] = 50_000 * 10 ** 18; - balanceOf[ECHIDNA_RECEIVER] = 50_000 * 10 ** 18; - } - - // ========== INVARIANT PROPERTIES ========== - // These must ALWAYS return true. Echidna tries to break them. - - /// @notice Total supply should never be negative (always >= 0) - /// @dev This invariant verifies the supply never underflows - function echidna_total_supply_not_negative() public view returns (bool) { - return totalSupply >= 0; - } - - /// @notice User balance should never exceed total supply - /// @dev Prevents inflation bugs - function echidna_balance_never_exceeds_supply() public view returns (bool) { - return balanceOf[msg.sender] <= totalSupply; - } - - /// @notice Transfer should not create tokens (conservation of value) - /// @dev Sum of balances should remain constant after transfers - function echidna_transfer_preserves_total() public returns (bool) { - if (paused) return true; - uint256 supplyBefore = totalSupply; - address recipient = msg.sender == ECHIDNA_RECEIVER ? ECHIDNA_SENDER : ECHIDNA_RECEIVER; - transfer(recipient, balanceOf[msg.sender] / 2); - return totalSupply == supplyBefore; - } - - /// @notice Zero address should never have a balance - /// @dev Tokens sent to zero address should be burned - function echidna_zero_address_no_balance() public view returns (bool) { - return balanceOf[address(0)] == 0; - } - - /// @notice Self-transfer should not change balance - /// @dev Sending tokens to yourself shouldn't create or destroy tokens - function echidna_self_transfer_neutral() public returns (bool) { - uint256 balanceBefore = balanceOf[msg.sender]; - if (balanceBefore > 0 && !paused) { - transfer(msg.sender, balanceBefore / 2); - return balanceOf[msg.sender] == balanceBefore; - } - return true; - } - - /// @notice Owner should always be set - /// @dev Owner address should never be zero after construction - function echidna_owner_always_set() public view returns (bool) { - return owner != address(0); - } - - // ========== ASSERTION-BASED TESTS ========== - // These test specific behaviors with assertions - - /// @notice Test that transfer reduces sender balance correctly - function test_transfer_reduces_balance(address to, uint256 amount) public { - // Skip invalid inputs - if (to == address(0) || to == msg.sender || paused) return; - if (amount == 0 || amount > balanceOf[msg.sender]) return; - - uint256 balanceBefore = balanceOf[msg.sender]; - transfer(to, amount); - uint256 balanceAfter = balanceOf[msg.sender]; - - assert(balanceAfter == balanceBefore - amount); - } - - /// @notice Test that transfer increases receiver balance correctly - function test_transfer_increases_balance(address to, uint256 amount) public { - // Skip invalid inputs - if (to == address(0) || to == msg.sender || paused) return; - if (amount == 0 || amount > balanceOf[msg.sender]) return; - - uint256 receiverBefore = balanceOf[to]; - transfer(to, amount); - uint256 receiverAfter = balanceOf[to]; - - assert(receiverAfter == receiverBefore + amount); - } - - /// @notice Test approve and transferFrom flow - function test_approve_transferFrom( - address spender, - uint256 approveAmount, - uint256 transferAmount - ) public { - if (spender == address(0) || spender == msg.sender || paused) return; - if (approveAmount == 0 || transferAmount == 0) return; - if (transferAmount > approveAmount) return; - if (approveAmount > balanceOf[msg.sender]) return; - - approve(spender, approveAmount); - assert(allowance[msg.sender][spender] == approveAmount); - } - - /// @notice Test that burn reduces total supply - function test_burn_reduces_supply(uint256 amount) public { - if (amount == 0 || amount > balanceOf[msg.sender] || paused) return; - - uint256 supplyBefore = totalSupply; - burn(amount); - uint256 supplyAfter = totalSupply; - - assert(supplyAfter == supplyBefore - amount); - } - - // ========== HELPER FUNCTIONS FOR ECHIDNA ========== - - /// @notice Allow Echidna to trigger pause (simulating owner action) - function try_pause() public { - if (msg.sender == owner) { - pause(); - } - } - - /// @notice Allow Echidna to trigger unpause - function try_unpause() public { - if (msg.sender == owner) { - unpause(); - } - } -} diff --git a/docs/ECHIDNA-INTEGRATION.adoc b/docs/ECHIDNA-INTEGRATION.adoc new file mode 100644 index 0000000..640b9a4 --- /dev/null +++ b/docs/ECHIDNA-INTEGRATION.adoc @@ -0,0 +1,151 @@ +// SPDX-License-Identifier: CC-BY-SA-4.0 +// Copyright (c) Jonathan D.A. Jewell += echidnabot ⇄ ECHIDNA integration +:toc: + +This page records how echidnabot depends on `hyperpolymath/echidna`, which +parts are shared code and which are local, and the follow-ups still open. +Status words follow AGENTS.md §6: _implemented_, _tested_, _wired_ and +_proved_ mean different things and none implies the next. + +== Trust kernel (shared, not re-implemented) + +`src/trust/confidence.rs` and `src/trust/axiom_tracker.rs` no longer carry +their own algorithms. + +* The trust *level* comes from `echidna_core_spark::compute_trust_level` + (ECHIDNA's trust kernel). echidnabot only maps its inputs onto ECHIDNA's + `TrustFactors`. `certificate_verified` is always `false`, because echidnabot + never checks a certificate itself. +* The proof-*source* axiom scan is ECHIDNA's + `echidna_core_spark::axiom_tracker::AxiomTracker`, called through + `AxiomTracker::scan_source`. +* The prover-*output* text scan (`AxiomTracker::scan`, for example Lean's + "declaration uses 'sorry'") stays local. ECHIDNA has no equivalent. + +The dependency is a git dependency pinned by full rev +(`b761b3a832981be51d4e88076ef1b90fe5037e9c`, on echidna `main`). A path +dependency would break standalone builds. + +Status: implemented and tested (unit tests in both modules). The kernel's +Creusot annotations are ECHIDNA's. echidnabot does not claim they are +proved. + +=== Follow-up: crate rename + +At the pinned rev the crate is named `echidna-core-spark`. It is not SPARK. +Upstream intends to rename it (`echidna-core-creusot`) and to move the trust +types into `echidna-core`. When either change lands on echidna `main`, update +the `Cargo.toml` line and the `use` paths. Do not pin to an unmerged branch. + +== Prover identifiers + +`ProverKind` was already a string slug (`ProverKind::new("lean")`) and is no +longer a 12-variant enum. echidnabot no longer keeps a static table of +ECHIDNA's names either. The start-up handshake (below) reads ECHIDNA's own +list from `/api/provers`. `EchidnaClient::echidna_name` matches a slug +against that list, ignoring case, `-` and `_`. The static mapping is used +only for the classic provers, and only when no list is available. + +Not done: depending on `echidna-core`'s `ProverKind` enum directly. That +would tie echidnabot's release cadence to every backend ECHIDNA adds, which +is the drift the slug type exists to avoid. Revisit if ECHIDNA publishes a +small, stable identifiers crate. + +== Minimum-version handshake + +`EchidnaClient::handshake` calls `GET /api/provers`, which also confirms +that the REST surface is up. It reads the server version from the +`version` or `echidna_version` field of that response, or from +`/api/health` if neither is present. It then enforces `MIN_ECHIDNA_VERSION` +(`2.3.0`). + +* At `serve` start-up, an ECHIDNA that is reachable but too old (or reports + a non-semver version) stops the process. An unreachable ECHIDNA only + logs a warning. +* Every job runs `ensure_handshake` before it dispatches, unless local + isolation is on. + +Status: implemented and unit-tested (version gate, name resolution). It is +wired into `serve` and `process_job`. No end-to-end test against a live +ECHIDNA was run. + +== Default endpoint + +`echidna server` listens on `127.0.0.1:8081`. The defaults are now +`http://127.0.0.1:8081` (REST) and `http://127.0.0.1:8081/graphql`, in +`src/config.rs`, `echidnabot.toml`, `echidnabot.example.toml` and +`config/echidnabot.ncl`. + +== `echidna.prove.result/1` + +`src/dispatcher/prove_result.rs` parses and validates the shared contract +object: + +[source,json] +---- +{"duration_ms":12,"echidna_version":"2.3.0","goal":"t","message":"ok","prover":"Lean","schema":"echidna.prove.result/1","status":"verified","trust":{"axioms":[],"confidence":null}} +---- + +A REST `/api/verify` body that carries the schema tag is read in this +shape. Any other body goes through the legacy path (`valid`, plus the typed +`outcome` when present). + +* Validation is strict about the schema tag, the status vocabulary, unknown + fields, the I-JSON integer bound on `duration_ms` (≤ 2^53−1) and a finite + `confidence`. +* Key order is not enforced. A valid object that is not JCS-canonical is + still accepted, because echidnabot is a consumer. + +=== Receipt vs warrant (pattern from epistemic-types) + +`ProofResult.trust_source` / `JobResult.trust_source` record where the trust +data came from: + +* `echidna`: ECHIDNA reported `trust.axioms` itself. echidnabot passes them + on unchanged (a _receipt_). +* `local-fallback`: echidnabot derived the axioms from the source and + output (a _warrant_). + +This is a plain enum that copies the distinction drawn by +`hyperpolymath/epistemic-types`. It is not a dependency, because that +library has no Rust port. + +== Identifiers + +`src/ids.rs` is the only module that mints identifiers: + +* `new_record_id()` returns a UUIDv7 for records and events: jobs, + repositories, result records and fleet findings. +* `content_id(value)` returns a UUIDv8 per RFC 9562 Appendix B.2. It takes + SHA-256 over the RFC 8785 (JCS) bytes of the value, keeps the first 16 + bytes, and sets version `8` and variant `10`. Use it for proof goals and + prove results. `goal_content_id(text)` is the string form. + +ECHIDNA and proof-burrower use the same construction, so all three agree on +a content id. JCS bytes come from the `serde_json_canonicalizer` crate, +because the estate crate `hyperpolymath/ijson-jcs` is private and a public +build cannot depend on it. Swap it in once it is public. + +Minting sites routed through `ids::new_record_id` (previously +`Uuid::new_v4`): + +* `src/scheduler/mod.rs` `JobId::new` +* `src/store/models.rs`: `Repository::new`, `ProofResultRecord::new`, + `TacticOutcomeRecord::new` +* tests and benches only: `src/fleet/mod.rs` (×3), + `src/feedback/corpus_delta.rs`, `src/feedback/reranker.rs`, + `src/scheduler/job_queue.rs`, `src/store/sqlite.rs`, + `tests/integration_tests.rs`, `tests/lifecycle.rs`, `tests/regressions/mod.rs`, + `benches/echidnabot_bench.rs` + +== Secrets in logs (pattern from the types fit map) + +`GitHubConfig`, `GitLabConfig`, `CodebergConfig` and `store::Repository` now +have hand-written `Debug` impls that print `` / `` in place +of tokens and webhook secrets. This is not `secret-types`, which is still an +empty template upstream. + +Still open: webhook secrets are stored in plaintext in SQLite +(`store/sqlite.rs`). At-rest protection would need januskey's `KeyManager` +split out into a library crate. diff --git a/echidna/echidna-assertion.yaml b/echidna/echidna-assertion.yaml deleted file mode 100644 index 542e5e2..0000000 --- a/echidna/echidna-assertion.yaml +++ /dev/null @@ -1,44 +0,0 @@ -# SPDX-License-Identifier: MPL-2.0 -# Owner: Jonathan D.A. Jewell -# Echidna Assertion Mode Configuration -# Tests functions with assert() statements - -# Assertion-based testing mode -testMode: "assertion" - -# Test iterations -testLimit: 30000 - -# Sequence length -seqLen: 75 - -# Shrinking for minimal reproduction -shrinkLimit: 3000 - -# Sender addresses -sender: - - "0x10000" - - "0x20000" - - "0x30000" - -deployer: "0x30000" - -# Keep property names distinct from argument-taking transaction functions. -# Assertion mode still exercises assertions in all transaction functions. -prefix: "echidna_" - -# Enable coverage -coverage: true - -# Text output for readability -format: "text" - -# Transaction timeout -timeout: 180 - -workers: 1 - -corpusDir: "echidna-corpus-assertion" - -maxValue: 100000000000000000000 -maxGas: 12500000 diff --git a/echidna/echidna-ci.yaml b/echidna/echidna-ci.yaml deleted file mode 100644 index 9a2677e..0000000 --- a/echidna/echidna-ci.yaml +++ /dev/null @@ -1,44 +0,0 @@ -# SPDX-License-Identifier: MPL-2.0 -# Owner: Jonathan D.A. Jewell -# Echidna CI Configuration - Faster settings for continuous integration - -# Property-based testing mode -testMode: "property" - -# Reduced test limit for CI (faster feedback) -testLimit: 10000 - -# Shorter sequences for quick runs -seqLen: 50 - -# Faster shrinking -shrinkLimit: 1000 - -# Sender addresses -sender: - - "0x10000" - - "0x20000" - - "0x30000" - -deployer: "0x30000" - -# Invariant test prefix -prefix: "echidna_" - -# Enable coverage -coverage: true - -# JSON output for parsing in CI -format: "json" - -# Shorter timeout for CI -timeout: 120 - -# Single worker for reproducibility -workers: 1 - -# Corpus for reproducible fuzzing -corpusDir: "echidna-corpus" - -maxValue: 100000000000000000000 -maxGas: 12500000 diff --git a/echidna/echidna-config.yaml b/echidna/echidna-config.yaml deleted file mode 100644 index c0e4dc0..0000000 --- a/echidna/echidna-config.yaml +++ /dev/null @@ -1,76 +0,0 @@ -# SPDX-License-Identifier: MPL-2.0 -# Owner: Jonathan D.A. Jewell -# Echidna Configuration for Smart Contract Fuzzing -# https://github.com/crytic/echidna - -# Test mode: property (default), assertion, optimization, overflow, exploration -testMode: "property" - -# Number of test sequences to run (higher = more thorough but slower) -testLimit: 50000 - -# Maximum length of a single test sequence -seqLen: 100 - -# Shrink failing test cases to minimal reproduction -shrinkLimit: 5000 - -# Contract deployment configuration -deployContracts: [] -deployBytecodes: [] - -# Sender addresses Echidna will use -sender: - - "0x10000" - - "0x20000" - - "0x30000" - -# Deploy the test contract from this address -deployer: "0x30000" - -# Property test prefix (functions starting with this are invariant tests) -prefix: "echidna_" - -# Enable coverage-guided fuzzing -coverage: true - -# Output format: text, json, none -format: "text" - -# Solidity compiler settings -solcArgs: "" - -# Timeout for individual transactions (in seconds) -timeout: 300 - -# Number of workers (parallel fuzzing) -workers: 1 - -# Corpus directory for saving interesting inputs -corpusDir: "echidna-corpus" - -# Dictionary of values to guide fuzzing -dictionary: [] - -# Filter functions to test (empty = all functions) -filterFunctions: [] - -# Filter blacklisted functions -filterBlacklist: false - -# Maximum value for msg.value in transactions -maxValue: 100000000000000000000 - -# Maximum gas for transactions -maxGas: 12500000 - -# Enable balance checking -balanceContract: 0 - -# RPC settings for forking (optional) -# rpcUrl: "https://eth-mainnet.g.alchemy.com/v2/YOUR_KEY" -# rpcBlock: 18000000 - -# Symbolic execution backend (optional) -# symExec: false -# symExecTimeout: 30 diff --git a/echidna/echidna-no-flaky-assertion.yaml b/echidna/echidna-no-flaky-assertion.yaml deleted file mode 100644 index ab13343..0000000 --- a/echidna/echidna-no-flaky-assertion.yaml +++ /dev/null @@ -1,46 +0,0 @@ -# SPDX-License-Identifier: MPL-2.0 -# Owner: Jonathan D.A. Jewell -# Echidna No-Flaky Assertion Mode Configuration -# Deterministic settings for stable assertion-based testing - -# Assertion-based testing mode -testMode: "assertion" - -# Higher test limit for thorough coverage -testLimit: 25000 - -# Longer sequences -seqLen: 100 - -# Aggressive shrinking -shrinkLimit: 10000 - -# Fixed sender addresses -sender: - - "0x10000" - - "0x20000" - - "0x30000" - -deployer: "0x30000" - -# No prefix filter in assertion mode -prefix: "echidna_" - -# Enable coverage -coverage: true - -# Text output for readability -format: "text" - -# Longer timeout -timeout: 300 - -# Single worker for determinism -workers: 1 - -# Persistent corpus -corpusDir: "echidna-corpus-assertion" - -# Fixed values -maxValue: 100000000000000000000 -maxGas: 12500000 diff --git a/echidna/echidna-no-flaky.yaml b/echidna/echidna-no-flaky.yaml deleted file mode 100644 index 5988795..0000000 --- a/echidna/echidna-no-flaky.yaml +++ /dev/null @@ -1,75 +0,0 @@ -# SPDX-License-Identifier: MPL-2.0 -# Owner: Jonathan D.A. Jewell -# Echidna No-Flaky Mode Configuration -# Deterministic settings for reproducible, stable test results -# -# This configuration prioritizes: -# 1. Reproducibility - same inputs produce same outputs -# 2. Stability - tests don't randomly pass/fail -# 3. Thoroughness - comprehensive coverage to catch edge cases - -# Property-based testing mode -testMode: "property" - -# Higher test limit for thorough coverage (reduces flakiness) -testLimit: 25000 - -# Longer sequences to explore deeper state space -seqLen: 100 - -# Aggressive shrinking for minimal reproduction -shrinkLimit: 10000 - -# Fixed sender addresses for determinism -sender: - - "0x10000" - - "0x20000" - - "0x30000" - -# Fixed deployer -deployer: "0x30000" - -# Invariant test prefix -prefix: "echidna_" - -# Enable coverage for guided fuzzing -coverage: true - -# JSON output for CI parsing -format: "json" - -# Longer timeout for thorough testing -timeout: 300 - -# Single worker for deterministic execution order -workers: 1 - -# Persistent corpus for reproducibility -corpusDir: "echidna-corpus" - -# No dictionary randomization -dictionary: [] - -# Test all functions -filterFunctions: [] -filterBlacklist: false - -# Fixed transaction values -maxValue: 100000000000000000000 -maxGas: 12500000 - -# ═══════════════════════════════════════════════════════════════════════════════ -# NO-FLAKY SPECIFIC SETTINGS -# ═══════════════════════════════════════════════════════════════════════════════ - -# Disable mutation-based exploration (more deterministic) -# Note: This reduces coverage but increases reproducibility -# mutConsts: [] - -# Use fixed block parameters -# timestamp: 1704067200 # 2024-01-01 00:00:00 UTC -# blockNumber: 1 - -# Retry failed property checks to confirm failure -# (prevents false positives from transient issues) -# retryLimit: 3 diff --git a/echidnabot.example.toml b/echidnabot.example.toml index 774bbbb..dbea1d6 100644 --- a/echidnabot.example.toml +++ b/echidnabot.example.toml @@ -17,9 +17,9 @@ max_connections = 5 [echidna] # ECHIDNA Core GraphQL endpoint -endpoint = "http://localhost:8080/graphql" +endpoint = "http://127.0.0.1:8081/graphql" # ECHIDNA Core REST endpoint -rest_endpoint = "http://localhost:8080" +rest_endpoint = "http://127.0.0.1:8081" # API mode: auto, graphql, rest mode = "auto" # Timeout for proof verification (seconds) diff --git a/echidnabot.toml b/echidnabot.toml index 4053fbd..1c830f6 100644 --- a/echidnabot.toml +++ b/echidnabot.toml @@ -17,9 +17,9 @@ max_connections = 5 [echidna] # ECHIDNA Core GraphQL endpoint -endpoint = "http://localhost:8080/graphql" +endpoint = "http://127.0.0.1:8081/graphql" # ECHIDNA Core REST endpoint -rest_endpoint = "http://localhost:8080" +rest_endpoint = "http://127.0.0.1:8081" # API mode: auto, graphql, rest mode = "auto" # Timeout for proof verification (seconds) diff --git a/rust-toolchain.toml b/rust-toolchain.toml new file mode 100644 index 0000000..e3636ad --- /dev/null +++ b/rust-toolchain.toml @@ -0,0 +1,15 @@ +# SPDX-License-Identifier: MPL-2.0 +# +# Repo-local toolchain pin (AGENTS §1a: a repo's own pins stay in the repo so +# it builds standalone). CI's reusable workflow installs floating `stable`; +# this file overrides it inside the checkout, so a new clippy release can no +# longer turn `main` red without a commit. 2026-10-02: stable moved to 1.99.0 +# and its clippy flagged `double_must_use` on the `#[async_trait]` adapter +# trait, which is exactly that failure mode. +# +# Bump deliberately: change `channel`, run `cargo clippy --all-targets -- -D +# warnings` and `cargo test`, commit both together. +[toolchain] +channel = "1.99.0" +components = ["clippy", "rustfmt"] +profile = "minimal" diff --git a/scripts/echidna-gen.js b/scripts/echidna-gen.js deleted file mode 100644 index 98eeff0..0000000 --- a/scripts/echidna-gen.js +++ /dev/null @@ -1,338 +0,0 @@ -// SPDX-License-Identifier: MPL-2.0 -// Copyright (c) Jonathan D.A. Jewell -#!/usr/bin/env -S deno run --allow-read --allow-write -// Echidna Test Property Generator -// Generates Echidna test contracts from Solidity source files -// -// Usage: deno run --allow-read --allow-write scripts/echidna-gen.js - -const SPDX_HEADER = `// SPDX-License-Identifier: MPL-2.0 -// Generated by echidnabot - Echidna Test Generator -// https://github.com/hyperpolymath/echidnabot -`; - -/** - * Parse a Solidity contract and extract key information - * @param {string} source - Solidity source code - * @returns {object} Parsed contract info - */ -function parseContract(source) { - const contractMatch = source.match(/contract\s+(\w+)(?:\s+is\s+([^{]+))?\s*\{/); - if (!contractMatch) { - throw new Error("No contract found in source file"); - } - - const name = contractMatch[1]; - const inheritance = contractMatch[2]?.split(",").map((s) => s.trim()) || []; - - // Extract state variables - const stateVars = []; - const stateVarRegex = - /^\s*(uint256|uint128|uint64|uint32|uint16|uint8|int256|int128|int64|int32|int16|int8|address|bool|string|bytes32|bytes)\s+(public\s+|private\s+|internal\s+)?(\w+)/gm; - let match; - while ((match = stateVarRegex.exec(source)) !== null) { - stateVars.push({ - type: match[1], - visibility: match[2]?.trim() || "internal", - name: match[3], - }); - } - - // Extract mappings - const mappings = []; - const mappingRegex = - /mapping\s*\(\s*(\w+)\s*=>\s*(\w+)\s*\)\s+(public\s+|private\s+|internal\s+)?(\w+)/g; - while ((match = mappingRegex.exec(source)) !== null) { - mappings.push({ - keyType: match[1], - valueType: match[2], - visibility: match[3]?.trim() || "internal", - name: match[4], - }); - } - - // Extract functions - const functions = []; - const funcRegex = - /function\s+(\w+)\s*\(([^)]*)\)\s+(public|external|internal|private)?[^{]*\{/g; - while ((match = funcRegex.exec(source)) !== null) { - functions.push({ - name: match[1], - params: match[2], - visibility: match[3] || "public", - }); - } - - // Extract pragma version - const pragmaMatch = source.match(/pragma\s+solidity\s+([^;]+);/); - const pragmaVersion = pragmaMatch ? pragmaMatch[1] : "^0.8.19"; - - return { - name, - inheritance, - stateVars, - mappings, - functions, - pragmaVersion, - }; -} - -/** - * Generate invariant properties based on contract analysis - * @param {object} contract - Parsed contract info - * @returns {string[]} Array of invariant function strings - */ -function generateInvariants(contract) { - const invariants = []; - - // Generate balance invariants for uint state variables - for (const v of contract.stateVars) { - if (v.type.startsWith("uint")) { - invariants.push(` - /// @notice ${v.name} should maintain valid bounds - function echidna_${v.name}_valid() public view returns (bool) { - return ${v.name} >= 0; - }`); - } - - if (v.type === "address" && v.name !== "owner") { - invariants.push(` - /// @notice ${v.name} address validation - function echidna_${v.name}_not_zero() public view returns (bool) { - // Allow zero address if intentionally set - return true; - }`); - } - } - - // Generate mapping invariants - for (const m of contract.mappings) { - if (m.valueType.startsWith("uint")) { - invariants.push(` - /// @notice Mapping ${m.name} values should be valid - function echidna_${m.name}_valid(${m.keyType} key) public view returns (bool) { - return ${m.name}[key] >= 0; - }`); - } - } - - // Check for common patterns - const hasOwner = contract.stateVars.some((v) => v.name === "owner"); - if (hasOwner) { - invariants.push(` - /// @notice Owner should always be set after construction - function echidna_owner_set() public view returns (bool) { - return owner != address(0); - }`); - } - - const hasTotalSupply = contract.stateVars.some( - (v) => v.name === "totalSupply" - ); - const hasBalanceOf = contract.mappings.some((m) => m.name === "balanceOf"); - if (hasTotalSupply && hasBalanceOf) { - invariants.push(` - /// @notice User balance should never exceed total supply - function echidna_balance_bounded() public view returns (bool) { - return balanceOf[msg.sender] <= totalSupply; - }`); - } - - const hasPaused = contract.stateVars.some((v) => v.name === "paused"); - if (hasPaused) { - invariants.push(` - /// @notice Paused state consistency check - function echidna_pause_consistent() public view returns (bool) { - return paused == true || paused == false; // Always true, but demonstrates state tracking - }`); - } - - return invariants; -} - -/** - * Generate assertion-based test functions - * @param {object} contract - Parsed contract info - * @returns {string[]} Array of test function strings - */ -function generateAssertionTests(contract) { - const tests = []; - - // Generate tests for transfer-like functions - const transferFuncs = contract.functions.filter( - (f) => - f.name.toLowerCase().includes("transfer") || - f.name.toLowerCase().includes("send") - ); - - for (const func of transferFuncs) { - tests.push(` - /// @notice Test ${func.name} balance accounting - function test_${func.name}_accounting(address to, uint256 amount) public { - if (to == address(0) || to == msg.sender) return; - if (amount == 0 || amount > balanceOf[msg.sender]) return; - - uint256 senderBefore = balanceOf[msg.sender]; - uint256 receiverBefore = balanceOf[to]; - - try this.${func.name}(to, amount) { - assert(balanceOf[msg.sender] == senderBefore - amount); - assert(balanceOf[to] == receiverBefore + amount); - } catch { - // Transfer failed, balances should be unchanged - assert(balanceOf[msg.sender] == senderBefore); - assert(balanceOf[to] == receiverBefore); - } - }`); - } - - // Generate tests for mint-like functions - const mintFuncs = contract.functions.filter((f) => - f.name.toLowerCase().includes("mint") - ); - - for (const func of mintFuncs) { - tests.push(` - /// @notice Test ${func.name} supply increase - function test_${func.name}_supply(address to, uint256 amount) public { - if (to == address(0) || amount == 0) return; - - uint256 supplyBefore = totalSupply; - - try this.${func.name}(to, amount) { - assert(totalSupply == supplyBefore + amount); - } catch { - assert(totalSupply == supplyBefore); - } - }`); - } - - // Generate tests for burn-like functions - const burnFuncs = contract.functions.filter((f) => - f.name.toLowerCase().includes("burn") - ); - - for (const func of burnFuncs) { - tests.push(` - /// @notice Test ${func.name} supply decrease - function test_${func.name}_supply(uint256 amount) public { - if (amount == 0 || amount > balanceOf[msg.sender]) return; - - uint256 supplyBefore = totalSupply; - - try this.${func.name}(amount) { - assert(totalSupply == supplyBefore - amount); - } catch { - assert(totalSupply == supplyBefore); - } - }`); - } - - return tests; -} - -/** - * Generate the complete Echidna test contract - * @param {object} contract - Parsed contract info - * @param {string} importPath - Relative import path - * @returns {string} Complete test contract source - */ -function generateTestContract(contract, importPath) { - const invariants = generateInvariants(contract); - const assertionTests = generateAssertionTests(contract); - - const testContractName = `${contract.name}EchidnaTest`; - - return `${SPDX_HEADER} -pragma solidity ${contract.pragmaVersion}; - -import "${importPath}"; - -/// @title ${testContractName} - Auto-generated Echidna fuzz testing contract -/// @notice Property-based tests for ${contract.name} -/// @dev Generated invariants and assertion tests for fuzzing -contract ${testContractName} is ${contract.name} { - // ========== TEST CONFIGURATION ========== - - address private constant ECHIDNA_SENDER = address(0x10000); - address private constant ECHIDNA_RECEIVER = address(0x20000); - - // ========== CONSTRUCTOR ========== - - constructor() ${contract.name}(${contract.name === "Token" ? "1_000_000 * 10 ** 18" : ""}) { - // Initial test setup - } - - // ========== INVARIANT PROPERTIES ========== - // These must ALWAYS return true. Echidna tries to break them. -${invariants.join("\n")} - - // ========== ASSERTION-BASED TESTS ========== - // These use assert() to verify specific behaviors -${assertionTests.join("\n")} -} -`; -} - -/** - * Main CLI handler - */ -async function main() { - const args = Deno.args; - - if (args.length < 1) { - console.log(` -Echidna Test Generator - Generate fuzz tests for Solidity contracts - -Usage: - deno run --allow-read --allow-write scripts/echidna-gen.js [output.sol] - -Arguments: - Path to the Solidity contract to analyze - [output.sol] Optional output path (default: EchidnaTest.sol) - -Examples: - deno run --allow-read --allow-write scripts/echidna-gen.js contracts/Token.sol - deno run --allow-read --allow-write scripts/echidna-gen.js contracts/Vault.sol contracts/VaultTest.sol -`); - Deno.exit(1); - } - - const inputPath = args[0]; - const source = await Deno.readTextFile(inputPath); - - console.log(`Analyzing ${inputPath}...`); - - const contract = parseContract(source); - - console.log(`Found contract: ${contract.name}`); - console.log(` State variables: ${contract.stateVars.length}`); - console.log(` Mappings: ${contract.mappings.length}`); - console.log(` Functions: ${contract.functions.length}`); - - // Calculate import path - const inputDir = inputPath.split("/").slice(0, -1).join("/"); - const inputFile = inputPath.split("/").pop(); - const importPath = `./${inputFile}`; - - // Generate test contract - const testSource = generateTestContract(contract, importPath); - - // Determine output path - const outputPath = args[1] || inputPath.replace(".sol", "EchidnaTest.sol"); - - await Deno.writeTextFile(outputPath, testSource); - - console.log(`\nGenerated Echidna test contract: ${outputPath}`); - console.log(` -Next steps: - 1. Review and customize the generated tests - 2. Run Echidna: - echidna ${outputPath} --contract ${contract.name}EchidnaTest --config echidna/echidna-config.yaml -`); -} - -main().catch((err) => { - console.error(`Error: ${err.message}`); - Deno.exit(1); -}); diff --git a/src/config.rs b/src/config.rs index 33d57fe..4626dbf 100644 --- a/src/config.rs +++ b/src/config.rs @@ -374,12 +374,14 @@ impl Default for EchidnaConfig { } } +/// Default ECHIDNA GraphQL endpoint: `echidna server` listens on 127.0.0.1:8081. fn default_echidna_endpoint() -> String { - "http://localhost:8080/graphql".to_string() + "http://127.0.0.1:8081/graphql".to_string() } +/// Default ECHIDNA REST base URL (same `echidna server`, port 8081). fn default_echidna_rest_endpoint() -> String { - "http://localhost:8080".to_string() + "http://127.0.0.1:8081".to_string() } fn default_echidna_mode() -> EchidnaApiMode { @@ -390,7 +392,7 @@ fn default_timeout() -> u64 { 300 // 5 minutes } -#[derive(Debug, Deserialize, Clone)] +#[derive(Deserialize, Clone)] pub struct GitHubConfig { /// GitHub App ID pub app_id: Option, @@ -405,7 +407,7 @@ pub struct GitHubConfig { pub webhook_secret: Option, } -#[derive(Debug, Deserialize, Clone)] +#[derive(Deserialize, Clone)] pub struct GitLabConfig { /// GitLab instance URL pub url: String, @@ -435,7 +437,7 @@ pub struct GitLabConfig { /// (statuses, comments, issues) require a token; the adapter /// returns `Error::Config("CODEBERG_TOKEN not set")` when missing. /// The `CODEBERG_TOKEN` env var also works as a fallback. -#[derive(Debug, Deserialize, Clone)] +#[derive(Deserialize, Clone)] pub struct CodebergConfig { /// Codeberg / Forgejo / Gitea instance URL. pub url: String, @@ -499,3 +501,79 @@ impl Config { Ok(parsed) } } + +/// Render a secret-bearing field for `Debug` without its value. +/// +/// Pattern from the types fit map (secret-types is not yet a usable +/// library): tokens and webhook secrets never reach logs through `{:?}`. +pub fn redacted(value: &Option) -> &'static str { + if value.is_some() { + "" + } else { + "" + } +} + +impl std::fmt::Debug for GitHubConfig { + /// Debug output with `token` and `webhook_secret` redacted. + fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result { + f.debug_struct("GitHubConfig") + .field("app_id", &self.app_id) + .field("private_key_path", &self.private_key_path) + .field("token", &redacted(&self.token)) + .field("webhook_secret", &redacted(&self.webhook_secret)) + .finish() + } +} + +impl std::fmt::Debug for GitLabConfig { + /// Debug output with `token` and `webhook_secret` redacted. + fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result { + f.debug_struct("GitLabConfig") + .field("url", &self.url) + .field("token", &"") + .field("webhook_secret", &redacted(&self.webhook_secret)) + .finish() + } +} + +impl std::fmt::Debug for CodebergConfig { + /// Debug output with `token` and `webhook_secret` redacted. + fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result { + f.debug_struct("CodebergConfig") + .field("url", &self.url) + .field("token", &redacted(&self.token)) + .field("webhook_secret", &redacted(&self.webhook_secret)) + .finish() + } +} + +#[cfg(test)] +mod redaction_tests { + use super::*; + + /// Secrets never appear in `Debug` output; their presence still does. + #[test] + fn forge_configs_redact_secrets_in_debug() { + let gh = GitHubConfig { + app_id: Some(1), + private_key_path: None, + token: Some("ghp_SECRET".into()), + webhook_secret: Some("whsec_SECRET".into()), + }; + let gl = GitLabConfig { + url: "https://gitlab.com".into(), + token: "glpat_SECRET".into(), + webhook_secret: None, + }; + let cb = CodebergConfig { + url: "https://codeberg.org".into(), + token: Some("cb_SECRET".into()), + webhook_secret: Some("cbwh_SECRET".into()), + }; + for out in [format!("{gh:?}"), format!("{gl:?}"), format!("{cb:?}")] { + assert!(!out.contains("SECRET"), "{out}"); + assert!(out.contains(""), "{out}"); + } + } +} diff --git a/src/dispatcher/echidna_client.rs b/src/dispatcher/echidna_client.rs index 096626e..391051f 100644 --- a/src/dispatcher/echidna_client.rs +++ b/src/dispatcher/echidna_client.rs @@ -5,14 +5,33 @@ use reqwest::Client; use serde::{Deserialize, Serialize}; +use std::sync::RwLock; use std::time::Duration; -use super::{ProofResult, ProofStatus, ProverKind, TacticSuggestion}; +use super::prove_result::ProveResult; +use super::{ProofResult, ProofStatus, ProverKind, TacticSuggestion, TrustSource}; use crate::config::{EchidnaApiMode, EchidnaConfig}; use crate::error::{Error, Result}; -use crate::trust::{axiom_tracker::AxiomTracker, confidence::assess_confidence}; +use crate::trust::axiom_tracker::{AxiomFlag, AxiomReport, AxiomTracker}; +use crate::trust::confidence::assess_confidence_with_axioms; use tracing::warn; +/// Oldest ECHIDNA server release echidnabot talks to. +/// +/// 2.3.0 is the first tagged release whose REST `/api/verify` returns the +/// typed `outcome` field and whose `/api/health` reports `version`. +pub const MIN_ECHIDNA_VERSION: &str = "2.3.0"; + +/// What the start-up handshake learned about the ECHIDNA server. +#[derive(Debug, Clone, PartialEq, Eq)] +pub struct EchidnaHandshake { + /// Server version, from `/api/provers` if it reports one, else + /// `/api/health`. + pub version: semver::Version, + /// ECHIDNA's own prover identifiers, as listed by `/api/provers`. + pub provers: Vec, +} + /// Client for ECHIDNA Core GraphQL API pub struct EchidnaClient { client: Client, @@ -20,6 +39,9 @@ pub struct EchidnaClient { rest_endpoint: String, timeout: Duration, mode: EchidnaApiMode, + /// Result of the last successful [`EchidnaClient::handshake`]; its + /// prover list maps echidnabot slugs onto ECHIDNA's names. + handshake: RwLock>, } impl EchidnaClient { @@ -36,9 +58,89 @@ impl EchidnaClient { rest_endpoint: config.rest_endpoint.clone(), timeout: Duration::from_secs(config.timeout_secs), mode: config.mode, + handshake: RwLock::new(None), } } + /// Minimum-version handshake with the ECHIDNA server. + /// + /// Lists `/api/provers` (which also proves the REST surface is there) and + /// reads the version from that response if present, otherwise from + /// `/api/health`. Fails with [`Error::Echidna`] if the server is older + /// than [`MIN_ECHIDNA_VERSION`] or reports an unparseable version. On + /// success the prover list is remembered for slug → name resolution. + pub async fn handshake(&self) -> Result { + let response = self + .client + .get(self.rest_url("/api/provers")) + .timeout(Duration::from_secs(10)) + .send() + .await + .map_err(Error::Http)?; + if !response.status().is_success() { + return Err(Error::Echidna(format!( + "ECHIDNA /api/provers returned status {}", + response.status() + ))); + } + let provers: RestProversResponse = response.json().await.map_err(Error::Http)?; + + let raw_version = match provers.version.clone().or(provers.echidna_version.clone()) { + Some(v) => v, + None => { + let health = self + .client + .get(self.rest_url("/api/health")) + .timeout(Duration::from_secs(5)) + .send() + .await + .map_err(Error::Http)?; + if !health.status().is_success() { + return Err(Error::Echidna(format!( + "ECHIDNA /api/health returned status {}", + health.status() + ))); + } + let health: RestHealthResponse = health.json().await.map_err(Error::Http)?; + health.version + } + }; + + let version = check_min_version(&raw_version)?; + let handshake = EchidnaHandshake { + version, + provers: provers.provers.into_iter().map(|p| p.name).collect(), + }; + if let Ok(mut slot) = self.handshake.write() { + *slot = Some(handshake.clone()); + } + Ok(handshake) + } + + /// Run [`EchidnaClient::handshake`] unless one has already succeeded. + pub async fn ensure_handshake(&self) -> Result { + let cached = self.handshake.read().ok().and_then(|slot| slot.clone()); + match cached { + Some(done) => Ok(done), + None => self.handshake().await, + } + } + + /// ECHIDNA's identifier for an echidnabot prover slug. + /// + /// Uses the list learned by [`EchidnaClient::handshake`] when one is + /// available (case-, `-`- and `_`-insensitive match), and otherwise the + /// static mapping for the classic provers. + pub fn echidna_name(&self, prover: &ProverKind) -> String { + let known = self + .handshake + .read() + .ok() + .and_then(|slot| slot.as_ref().map(|h| h.provers.clone())) + .unwrap_or_default(); + resolve_echidna_name(prover, &known) + } + /// Verify a proof using ECHIDNA Core #[tracing::instrument( name = "echidna.verify", @@ -207,8 +309,10 @@ impl EchidnaClient { || a.ends_with(".drat") || a.ends_with(".tstp") }); - let axioms = AxiomTracker::scan(prover, &prover_output); - let confidence = assess_confidence(prover, status, has_cert, 1); + let axioms = AxiomTracker::scan_source(prover, content) + .merge(AxiomTracker::scan(prover, &prover_output)); + let confidence = + assess_confidence_with_axioms(prover, status, has_cert, 1, axioms.worst_danger); Ok(ProofResult { status, message: data.verify_proof.message, @@ -217,6 +321,7 @@ impl EchidnaClient { artifacts, confidence: Some(confidence), axioms: Some(axioms), + trust_source: TrustSource::LocalFallback, }) } @@ -349,7 +454,7 @@ impl EchidnaClient { async fn verify_proof_rest(&self, prover: &ProverKind, content: &str) -> Result { let request = RestVerifyRequest { - prover: prover_to_echidna_name(prover), + prover: self.echidna_name(prover), content: content.to_string(), }; @@ -369,29 +474,8 @@ impl EchidnaClient { ))); } - let data: RestVerifyResponse = response.json().await.map_err(Error::Http)?; - let status = if data.valid { - ProofStatus::Verified - } else { - ProofStatus::Failed - }; - // REST endpoint returns no raw output; axiom scan over empty string = clean. - let prover_output = String::new(); - let axioms = AxiomTracker::scan(prover, &prover_output); - let confidence = assess_confidence(prover, status, false, 1); - Ok(ProofResult { - status, - message: if data.valid { - "Proof verified successfully".to_string() - } else { - "Proof verification failed".to_string() - }, - prover_output, - duration_ms: 0, - artifacts: Vec::new(), - confidence: Some(confidence), - axioms: Some(axioms), - }) + let body: serde_json::Value = response.json().await.map_err(Error::Http)?; + rest_verify_result(prover, content, body) } async fn suggest_tactics_rest( @@ -407,7 +491,7 @@ impl EchidnaClient { }; let request = RestSuggestRequest { - prover: prover_to_echidna_name(prover), + prover: self.echidna_name(prover), content, limit: Some(5), }; @@ -468,11 +552,11 @@ impl EchidnaClient { } let data: RestProversResponse = response.json().await.map_err(Error::Http)?; - let target = prover_to_echidna_name(prover).to_lowercase(); - let available = data - .provers - .into_iter() - .any(|info| info.name.to_lowercase() == target); + let names: Vec = data.provers.into_iter().map(|info| info.name).collect(); + let target = normalise_prover_name(&resolve_echidna_name(prover, &names)); + let available = names + .iter() + .any(|name| normalise_prover_name(name) == target); Ok(if available { ProverStatus::Available @@ -492,15 +576,120 @@ struct RestVerifyRequest { content: String, } +/// Legacy REST `/api/verify` body (ECHIDNA ≤ 2.3 shape). #[derive(Deserialize)] struct RestVerifyResponse { valid: bool, + /// Typed outcome (`PROVED`, `NO_PROOF_FOUND`, `TIMEOUT`, ...); absent on + /// very old servers. + #[serde(default)] + outcome: Option, #[allow(dead_code)] + #[serde(default)] goals_remaining: usize, #[allow(dead_code)] + #[serde(default)] tactics_used: usize, } +/// Build a [`ProofResult`] from a REST `/api/verify` body. +/// +/// An `echidna.prove.result/1` body is read as that contract and its `trust` +/// object is transported ([`TrustSource::Echidna`]). Any other body is read +/// as the legacy shape and trust is derived locally from the proof source. +fn rest_verify_result( + prover: &ProverKind, + content: &str, + body: serde_json::Value, +) -> Result { + if ProveResult::is_prove_result(&body) { + let result = ProveResult::from_value(body)?; + let status = ProofStatus::from(result.status); + let reported = AxiomReport::from_reported( + prover.clone(), + result + .trust + .axioms + .iter() + .map(|a| AxiomFlag::Other(a.clone())), + ); + // ECHIDNA's list is the receipt; the canonical source scan still runs + // so a hole ECHIDNA did not name cannot raise the level. + let axioms = reported.merge(AxiomTracker::scan_source(prover, content)); + let confidence = + assess_confidence_with_axioms(prover, status, false, 1, axioms.worst_danger); + return Ok(ProofResult { + status, + message: result.message, + prover_output: String::new(), + duration_ms: result.duration_ms, + artifacts: Vec::new(), + confidence: Some(confidence), + axioms: Some(axioms), + trust_source: TrustSource::Echidna, + }); + } + + let data: RestVerifyResponse = serde_json::from_value(body)?; + let status = match data.outcome.as_deref() { + Some(outcome) => parse_rest_outcome(outcome, data.valid), + None if data.valid => ProofStatus::Verified, + None => ProofStatus::Failed, + }; + // The legacy REST body carries no prover output, so the only axiom + // signal is the source scan. + let axioms = AxiomTracker::scan_source(prover, content); + let confidence = assess_confidence_with_axioms(prover, status, false, 1, axioms.worst_danger); + Ok(ProofResult { + status, + message: match status { + ProofStatus::Verified => "Proof verified successfully".to_string(), + ProofStatus::Timeout => "Proof verification timed out".to_string(), + ProofStatus::Error => "ECHIDNA reported an error".to_string(), + _ => "Proof verification failed".to_string(), + }, + prover_output: String::new(), + duration_ms: 0, + artifacts: Vec::new(), + confidence: Some(confidence), + axioms: Some(axioms), + trust_source: TrustSource::LocalFallback, + }) +} + +/// Map ECHIDNA's typed REST outcome onto [`ProofStatus`]. +fn parse_rest_outcome(outcome: &str, valid: bool) -> ProofStatus { + match outcome.to_ascii_uppercase().as_str() { + "PROVED" => ProofStatus::Verified, + "NO_PROOF_FOUND" | "INVALID_INPUT" | "INCONSISTENT_PREMISES" => ProofStatus::Failed, + "TIMEOUT" => ProofStatus::Timeout, + "UNSUPPORTED_FEATURE" | "PROVER_ERROR" | "SYSTEM_ERROR" => ProofStatus::Error, + _ if valid => ProofStatus::Verified, + _ => ProofStatus::Unknown, + } +} + +#[derive(Deserialize)] +struct RestHealthResponse { + version: String, +} + +/// Parse a reported ECHIDNA version and enforce [`MIN_ECHIDNA_VERSION`]. +pub fn check_min_version(raw: &str) -> Result { + let trimmed = raw.trim().trim_start_matches('v'); + let version = semver::Version::parse(trimmed).map_err(|e| { + Error::Echidna(format!("ECHIDNA reported unparseable version {raw:?}: {e}")) + })?; + let minimum = semver::Version::parse(MIN_ECHIDNA_VERSION) + .map_err(|e| Error::Internal(format!("MIN_ECHIDNA_VERSION is not semver: {e}")))?; + if version < minimum { + return Err(Error::Echidna(format!( + "ECHIDNA {version} is older than the minimum supported {minimum}" + ))); + } + Ok(version) +} + #[derive(Serialize)] struct RestSuggestRequest { prover: String, @@ -516,21 +705,46 @@ struct RestSuggestResponse { #[derive(Deserialize)] struct RestProversResponse { provers: Vec, + /// Not sent by ECHIDNA 2.3; accepted if a later server adds it. + #[serde(default)] + version: Option, + /// Alternative spelling, matching the prove-result contract. + #[serde(default)] + echidna_version: Option, } #[derive(Deserialize)] struct RestProverInfo { name: String, #[allow(dead_code)] + #[serde(default)] tier: u8, #[allow(dead_code)] + #[serde(default)] complexity: u8, } -fn prover_to_echidna_name(prover: &ProverKind) -> String { - // These are ECHIDNA's serde enum names, not presentation labels. +/// Lower-case a prover name and drop `-`, `_`, spaces and `/` for matching. +fn normalise_prover_name(name: &str) -> String { + name.chars() + .filter(|c| !matches!(c, '-' | '_' | ' ' | '/')) + .flat_map(char::to_lowercase) + .collect() +} + +/// Map an echidnabot slug onto ECHIDNA's identifier. +/// +/// With a non-empty `known` list (from `/api/provers`) the first normalised +/// match wins. Without one, or with no match, the static mapping for the +/// classic provers applies; these are ECHIDNA's serde enum names, not +/// presentation labels. +fn resolve_echidna_name(prover: &ProverKind, known: &[String]) -> String { + let wanted = normalise_prover_name(prover.as_str()); + if let Some(hit) = known.iter().find(|k| normalise_prover_name(k) == wanted) { + return hit.clone(); + } match prover.as_str() { - "lean" => "Lean", + "lean" | "lean4" => "Lean", "isabelle" => "Isabelle", "hol-light" => "HOLLight", _ => prover.display_name(), @@ -653,4 +867,66 @@ mod tests { assert_eq!(ProverKind::new("lean").tier(), 1); assert_eq!(ProverKind::new("hol4").tier(), 3); } + + #[test] + fn test_min_version_gate() { + assert!(check_min_version("2.3.0").is_ok()); + assert!(check_min_version("v2.4.1").is_ok()); + assert!(check_min_version("2.2.9").is_err()); + assert!(check_min_version("not-a-version").is_err()); + } + + #[test] + fn test_resolve_name_prefers_handshake_list() { + let known = vec!["HOLLight".to_string(), "Idris2".to_string()]; + assert_eq!( + resolve_echidna_name(&ProverKind::new("hol-light"), &known), + "HOLLight" + ); + assert_eq!( + resolve_echidna_name(&ProverKind::new("idris2"), &known), + "Idris2" + ); + // Falls back to the static classic mapping without a list. + assert_eq!(resolve_echidna_name(&ProverKind::new("lean"), &[]), "Lean"); + } + + #[test] + fn test_rest_body_in_prove_result_shape_is_transported() { + let body = serde_json::json!({ + "schema": "echidna.prove.result/1", + "status": "verified", + "prover": "Lean", + "goal": "t", + "duration_ms": 7, + "message": "ok", + "trust": {"confidence": null, "axioms": ["propext"]}, + "echidna_version": "2.4.0" + }); + let r = rest_verify_result( + &ProverKind::new("lean"), + "theorem t : True := trivial", + body, + ) + .unwrap(); + assert_eq!(r.status, ProofStatus::Verified); + assert_eq!(r.trust_source, TrustSource::Echidna); + assert_eq!(r.duration_ms, 7); + assert!(r + .axioms + .unwrap() + .flags + .contains(&AxiomFlag::Other("propext".to_string()))); + } + + #[test] + fn test_legacy_rest_body_uses_outcome_and_source_scan() { + let body = serde_json::json!({ + "valid": false, "outcome": "TIMEOUT", "goals_remaining": 1, "tactics_used": 0 + }); + let r = rest_verify_result(&ProverKind::new("lean"), " sorry\n", body).unwrap(); + assert_eq!(r.status, ProofStatus::Timeout); + assert_eq!(r.trust_source, TrustSource::LocalFallback); + assert!(r.axioms.unwrap().has_unsound()); + } } diff --git a/src/dispatcher/mod.rs b/src/dispatcher/mod.rs index b37912b..4b48a47 100644 --- a/src/dispatcher/mod.rs +++ b/src/dispatcher/mod.rs @@ -4,8 +4,10 @@ //! Prover dispatcher - communicates with ECHIDNA Core pub mod echidna_client; +pub mod prove_result; -pub use echidna_client::EchidnaClient; +pub use echidna_client::{EchidnaClient, EchidnaHandshake, MIN_ECHIDNA_VERSION}; +pub use prove_result::{ProveResult, PROVE_RESULT_SCHEMA}; use serde::{Deserialize, Serialize}; @@ -27,6 +29,37 @@ pub struct ProofResult { /// Axiom usage flags scanned from prover output. #[serde(default)] pub axioms: Option, + /// Where `confidence` and `axioms` came from. Results stored before this + /// field existed deserialise as [`TrustSource::LocalFallback`]. + #[serde(default)] + pub trust_source: TrustSource, +} + +/// Provenance of the trust data attached to a [`ProofResult`]. +/// +/// Pattern from `hyperpolymath/epistemic-types` (receipt vs warrant), adopted +/// as a plain enum; there is no Rust port of those types to depend on. +#[derive(Debug, Clone, Copy, PartialEq, Eq, Default, Serialize, Deserialize)] +#[serde(rename_all = "kebab-case")] +pub enum TrustSource { + /// ECHIDNA reported the axiom data itself (an `echidna.prove.result/1` + /// `trust` object). echidnabot transports it unchanged (a receipt); the + /// level is still computed by ECHIDNA's trust kernel, linked in. + Echidna, + /// echidnabot computed the trust data from what ECHIDNA returned, using + /// ECHIDNA's trust kernel and source scanner: a warrant, not a receipt. + #[default] + LocalFallback, +} + +impl TrustSource { + /// Short label used in check-run summaries and PR comments. + pub fn label(&self) -> &'static str { + match self { + Self::Echidna => "axioms reported by ECHIDNA", + Self::LocalFallback => "derived locally by echidnabot (ECHIDNA did not report trust)", + } + } } /// Proof verification status diff --git a/src/dispatcher/prove_result.rs b/src/dispatcher/prove_result.rs new file mode 100644 index 0000000..81e4714 --- /dev/null +++ b/src/dispatcher/prove_result.rs @@ -0,0 +1,188 @@ +// SPDX-License-Identifier: MPL-2.0 +// Copyright (c) Jonathan D.A. Jewell +//! Consumer side of the shared `echidna.prove.result/1` contract. +//! +//! ECHIDNA's `echidna prove ... --output json` prints exactly one +//! JCS-canonical (RFC 8785) I-JSON (RFC 7493) object: +//! +//! ```json +//! {"duration_ms":12,"echidna_version":"2.3.0","goal":"t","message":"...", +//! "prover":"Lean","schema":"echidna.prove.result/1","status":"verified", +//! "trust":{"axioms":[],"confidence":null}} +//! ``` +//! +//! echidnabot accepts that object wherever it consumes a result: a REST +//! `/api/verify` body that carries `"schema":"echidna.prove.result/1"` is read +//! as this shape, and anything else falls back to the legacy REST shape. +//! +//! The `trust` object is ECHIDNA's own judgement (a *receipt*, in the +//! vocabulary of `hyperpolymath/epistemic-types`). echidnabot transports it +//! instead of re-deriving a score; see [`super::TrustSource`]. +//! +//! Validation here is deliberately strict about the parts a consumer depends +//! on (schema tag, status vocabulary, the I-JSON integer bound on +//! `duration_ms`, finite `confidence`) and liberal about key order, so a +//! non-canonical but otherwise valid object is still accepted. + +use serde::{Deserialize, Serialize}; + +use super::ProofStatus; +use crate::error::{Error, Result}; + +/// The schema tag every `echidna.prove.result/1` object carries. +pub const PROVE_RESULT_SCHEMA: &str = "echidna.prove.result/1"; + +/// Largest integer I-JSON (RFC 7493 §2.2) guarantees to round-trip: 2^53 − 1. +pub const IJSON_MAX_SAFE_INTEGER: u64 = (1 << 53) - 1; + +/// Status vocabulary of `echidna.prove.result/1`. +#[derive(Debug, Clone, Copy, PartialEq, Eq, Serialize, Deserialize)] +#[serde(rename_all = "lowercase")] +pub enum ProveStatus { + /// The prover accepted the proof. + Verified, + /// The prover rejected the proof. + Failed, + /// ECHIDNA or the backend failed before producing a verdict. + Error, + /// The backend ran out of time. + Timeout, + /// No verdict either way. + Unknown, +} + +impl From for ProofStatus { + /// Map the contract's status onto echidnabot's own status enum. + fn from(status: ProveStatus) -> Self { + match status { + ProveStatus::Verified => ProofStatus::Verified, + ProveStatus::Failed => ProofStatus::Failed, + ProveStatus::Error => ProofStatus::Error, + ProveStatus::Timeout => ProofStatus::Timeout, + ProveStatus::Unknown => ProofStatus::Unknown, + } + } +} + +/// ECHIDNA's trust judgement for one result. +#[derive(Debug, Clone, PartialEq, Serialize, Deserialize)] +pub struct ProveTrust { + /// ECHIDNA's confidence, or `null` when no receipt-backed computation + /// produced one. + pub confidence: Option, + /// Axioms / holes ECHIDNA found in the proof. + pub axioms: Vec, +} + +/// One `echidna.prove.result/1` object. +#[derive(Debug, Clone, PartialEq, Serialize, Deserialize)] +#[serde(deny_unknown_fields)] +pub struct ProveResult { + /// Always [`PROVE_RESULT_SCHEMA`]. + pub schema: String, + /// Verdict. + pub status: ProveStatus, + /// ECHIDNA's prover identifier. + pub prover: String, + /// The goal or theorem name. + pub goal: String, + /// Wall-clock duration; bounded by [`IJSON_MAX_SAFE_INTEGER`]. + pub duration_ms: u64, + /// Human-readable message. + pub message: String, + /// ECHIDNA's trust judgement. + pub trust: ProveTrust, + /// Version of the ECHIDNA that produced the object. + pub echidna_version: String, +} + +impl ProveResult { + /// Parse and validate one `echidna.prove.result/1` object from text. + pub fn parse(text: &str) -> Result { + let value: serde_json::Value = serde_json::from_str(text.trim())?; + Self::from_value(value) + } + + /// Validate an already-parsed JSON value as `echidna.prove.result/1`. + pub fn from_value(value: serde_json::Value) -> Result { + if !Self::is_prove_result(&value) { + return Err(Error::Echidna(format!( + "not an {PROVE_RESULT_SCHEMA} object (schema tag missing or different)" + ))); + } + if let Some(d) = value.get("duration_ms") { + match d.as_u64() { + Some(n) if n <= IJSON_MAX_SAFE_INTEGER => {} + _ => { + return Err(Error::Echidna(format!( + "duration_ms must be a non-negative integer <= 2^53-1 (I-JSON), got {d}" + ))) + } + } + } + let parsed: ProveResult = serde_json::from_value(value)?; + if let Some(c) = parsed.trust.confidence { + if !c.is_finite() { + return Err(Error::Echidna( + "trust.confidence must be a finite number or null".to_string(), + )); + } + } + Ok(parsed) + } + + /// Whether a JSON value carries the `echidna.prove.result/1` schema tag. + pub fn is_prove_result(value: &serde_json::Value) -> bool { + value.get("schema").and_then(|s| s.as_str()) == Some(PROVE_RESULT_SCHEMA) + } +} + +#[cfg(test)] +mod tests { + use super::*; + + const CANONICAL: &str = r#"{"duration_ms":12,"echidna_version":"2.3.0","goal":"t","message":"ok","prover":"Lean","schema":"echidna.prove.result/1","status":"verified","trust":{"axioms":[],"confidence":null}}"#; + + #[test] + fn parses_canonical_object() { + let r = ProveResult::parse(CANONICAL).unwrap(); + assert_eq!(r.status, ProveStatus::Verified); + assert_eq!(ProofStatus::from(r.status), ProofStatus::Verified); + assert_eq!(r.trust.confidence, None); + assert_eq!(r.duration_ms, 12); + } + + #[test] + fn accepts_non_canonical_key_order() { + let text = r#"{"schema":"echidna.prove.result/1","status":"timeout","prover":"Z3","goal":"g","duration_ms":5,"message":"","trust":{"confidence":0.5,"axioms":["classical"]},"echidna_version":"2.4.0"}"#; + let r = ProveResult::parse(text).unwrap(); + assert_eq!(ProofStatus::from(r.status), ProofStatus::Timeout); + assert_eq!(r.trust.axioms, vec!["classical".to_string()]); + } + + #[test] + fn rejects_wrong_schema_tag() { + let text = CANONICAL.replace("echidna.prove.result/1", "echidna.prove.result/2"); + assert!(ProveResult::parse(&text).is_err()); + } + + #[test] + fn rejects_unknown_status() { + let text = CANONICAL.replace("\"verified\"", "\"proved\""); + assert!(ProveResult::parse(&text).is_err()); + } + + #[test] + fn rejects_duration_outside_ijson_range() { + let text = CANONICAL.replace("\"duration_ms\":12", "\"duration_ms\":9007199254740992"); + assert!(ProveResult::parse(&text).is_err()); + let text = CANONICAL.replace("\"duration_ms\":12", "\"duration_ms\":9007199254740991"); + assert!(ProveResult::parse(&text).is_ok()); + } + + #[test] + fn rejects_unknown_fields() { + let text = CANONICAL.replace("\"goal\":\"t\"", "\"goal\":\"t\",\"extra\":1"); + assert!(ProveResult::parse(&text).is_err()); + } +} diff --git a/src/feedback/corpus_delta.rs b/src/feedback/corpus_delta.rs index 3b43c0c..0998857 100644 --- a/src/feedback/corpus_delta.rs +++ b/src/feedback/corpus_delta.rs @@ -333,10 +333,9 @@ pub struct RefreshStatus { mod tests { use super::*; use tokio::io::AsyncReadExt; - use uuid::Uuid; fn tmp_dir() -> PathBuf { - std::env::temp_dir().join(format!("echidnabot-corpus-{}", Uuid::new_v4())) + std::env::temp_dir().join(format!("echidnabot-corpus-{}", crate::ids::new_record_id())) } fn sample_row(succeeded: bool) -> DeltaRow { diff --git a/src/feedback/reranker.rs b/src/feedback/reranker.rs index cd1222c..635dd37 100644 --- a/src/feedback/reranker.rs +++ b/src/feedback/reranker.rs @@ -141,11 +141,12 @@ impl Reranker { mod tests { use super::*; use crate::store::SqliteStore; - use uuid::Uuid; async fn fresh_store() -> (Arc, std::path::PathBuf) { - let path = - std::env::temp_dir().join(format!("echidnabot-rerank-test-{}.db", Uuid::new_v4())); + let path = std::env::temp_dir().join(format!( + "echidnabot-rerank-test-{}.db", + crate::ids::new_record_id() + )); let url = format!("sqlite://{}?mode=rwc", path.display()); let store = SqliteStore::new(&url).await.unwrap(); (Arc::new(store) as Arc, path) diff --git a/src/fleet/mod.rs b/src/fleet/mod.rs index f870621..540d0b2 100644 --- a/src/fleet/mod.rs +++ b/src/fleet/mod.rs @@ -171,7 +171,6 @@ mod tests { use crate::dispatcher::ProverKind; use crate::scheduler::JobId; use chrono::Utc; - use uuid::Uuid; #[test] fn test_fleet_coordinator_lifecycle() { @@ -195,7 +194,7 @@ mod tests { let job = ProofJob { id: JobId::new(), - repo_id: Uuid::new_v4(), + repo_id: crate::ids::new_record_id(), commit_sha: "abc123".to_string(), prover: ProverKind::new("coq"), file_paths: vec!["test.v".to_string()], @@ -218,6 +217,7 @@ mod tests { failed_files: vec![], confidence: None, axioms: None, + trust_source: Default::default(), }; coordinator.publish_finding(&job, &result).unwrap(); @@ -235,7 +235,7 @@ mod tests { let job = ProofJob { id: JobId::new(), - repo_id: Uuid::new_v4(), + repo_id: crate::ids::new_record_id(), commit_sha: "abc123".to_string(), prover: ProverKind::new("lean"), file_paths: vec!["test.lean".to_string()], @@ -258,6 +258,7 @@ mod tests { failed_files: vec!["test.lean".to_string()], confidence: None, axioms: None, + trust_source: Default::default(), }; coordinator.publish_finding(&job, &result).unwrap(); @@ -274,7 +275,7 @@ mod tests { let job = ProofJob { id: JobId::new(), - repo_id: Uuid::new_v4(), + repo_id: crate::ids::new_record_id(), commit_sha: "abc123".to_string(), prover: ProverKind::new("z3"), file_paths: vec!["test.smt2".to_string()], @@ -297,6 +298,7 @@ mod tests { failed_files: vec![], confidence: None, axioms: None, + trust_source: Default::default(), }; // Should not error when not connected diff --git a/src/ids.rs b/src/ids.rs new file mode 100644 index 0000000..32e8130 --- /dev/null +++ b/src/ids.rs @@ -0,0 +1,113 @@ +// SPDX-License-Identifier: MPL-2.0 +// Copyright (c) Jonathan D.A. Jewell +//! # Identifier minting — the only place echidnabot mints ids +//! +//! Two kinds of identifier, and nothing else in the crate mints one: +//! +//! * [`new_record_id`] — a **UUIDv7** (RFC 9562 §5.7) for *events and +//! records*: jobs, repositories, proof-result records, fleet findings. +//! Time-ordered, minted from the `uuid` crate's library API as +//! `standards/docs/UUID-V7-ESTATE-STANDARD.adoc` requires (no hand-set +//! version bits). +//! * [`content_id`] — a **UUIDv8** (RFC 9562 §5.8, Appendix B.2 style) for +//! *content*: proof goals and `echidna.prove.result/1` objects. It is +//! SHA-256 over the RFC 8785 (JCS) canonical bytes of the value, truncated +//! to the first 16 bytes, with the version nibble set to `8` and the +//! variant bits set to `10`. The same JSON content always yields the same +//! id, whatever key order or whitespace it arrived in. +//! +//! The v7/v8 split is the owner's delegated policy of 2026-10-05: v7 for +//! things that *happened*, v8 for things that *are* (content addressing). +//! The same split, with the same construction, is implemented in +//! `hyperpolymath/echidna` (`src/rust/ids.rs`) and +//! `hyperpolymath/proof-burrower` (`burrower-core/src/ids.rs`), so a content +//! id computed by any of the three agrees. See +//! `docs/ECHIDNA-INTEGRATION.adoc` § Identifiers. +//! +//! IDs that arrive from outside (a forge's repository id, an ECHIDNA job id) +//! keep whatever format they came with; this module only mints our own. + +use sha2::{Digest, Sha256}; +use uuid::Uuid; + +/// Mint a fresh time-ordered record id (UUIDv7). +/// +/// Use for events and records: jobs, repositories, result records, fleet +/// findings. Within one process successive ids sort in minting order (the +/// `uuid` crate keeps a monotonic counter inside the millisecond). +pub fn new_record_id() -> Uuid { + Uuid::now_v7() +} + +/// Content id of a JSON value: UUIDv8 over SHA-256 of its JCS bytes. +/// +/// Use for proof goals and prove results. Fails only if the value cannot be +/// canonicalised (RFC 8785 rejects non-finite numbers, which +/// `serde_json::Value` cannot hold anyway, so this is defensive). +pub fn content_id(value: &serde_json::Value) -> Result { + let canonical = serde_json_canonicalizer::to_vec(value)?; + let digest = Sha256::digest(&canonical); + let mut first16 = [0u8; 16]; + first16.copy_from_slice(&digest[..16]); + // `new_v8` overwrites the version nibble with 8 and the variant bits + // with RFC 9562's `10`; the other 122 bits are the hash prefix. + Ok(Uuid::new_v8(first16)) +} + +/// Content id of a proof goal's text (a JSON string). +/// +/// Infallible: a JSON string always canonicalises. +pub fn goal_content_id(goal_text: &str) -> Uuid { + content_id(&serde_json::Value::String(goal_text.to_string())).unwrap_or_else(|_| Uuid::nil()) +} + +#[cfg(test)] +mod tests { + use super::*; + use serde_json::json; + + /// Same JCS content gives the same v8 id regardless of key order and spacing. + #[test] + fn same_canonical_content_same_v8_id() { + let a: serde_json::Value = serde_json::from_str(r#"{"b":1,"a":[true,null]}"#).unwrap(); + let b: serde_json::Value = + serde_json::from_str("{ \"a\" : [ true , null ] , \"b\" : 1 }").unwrap(); + assert_eq!(content_id(&a).unwrap(), content_id(&b).unwrap()); + assert_ne!( + content_id(&a).unwrap(), + content_id(&json!({"a":[true,null],"b":2})).unwrap() + ); + } + + /// The v8 id is exactly the SHA-256 prefix with version/variant bits applied. + #[test] + fn v8_bits_and_hash_prefix() { + let id = content_id(&json!("lemma foo: x = y")).unwrap(); + assert_eq!(id.get_version_num(), 8); + assert_eq!(id.get_variant(), uuid::Variant::RFC4122); + let bytes = id.as_bytes(); + assert_eq!(bytes[6] >> 4, 0x8); + assert_eq!(bytes[8] >> 6, 0b10); + let digest = Sha256::digest(br#""lemma foo: x = y""#); + for (i, byte) in bytes.iter().enumerate() { + let mask = match i { + 6 => 0x0f, + 8 => 0x3f, + _ => 0xff, + }; + assert_eq!(byte & mask, digest[i] & mask, "byte {i}"); + } + assert_eq!(goal_content_id("lemma foo: x = y"), id); + } + + /// v7 record ids carry version 7 and sort in minting order. + #[test] + fn v7_record_ids_are_versioned_and_monotonic() { + let ids: Vec = (0..1000).map(|_| new_record_id()).collect(); + for w in ids.windows(2) { + assert!(w[0] < w[1], "{} !< {}", w[0], w[1]); + } + assert_eq!(ids[0].get_version_num(), 7); + assert_eq!(ids[0].get_variant(), uuid::Variant::RFC4122); + } +} diff --git a/src/lib.rs b/src/lib.rs index e9d17fe..993c616 100644 --- a/src/lib.rs +++ b/src/lib.rs @@ -21,7 +21,8 @@ pub mod dispatcher; pub mod error; pub mod executor; // Container isolation for secure prover execution pub mod feedback; // Double-loop: proof-history reranker + corpus delta (Package 7b) -pub mod fleet; // gitbot-fleet coordination layer +pub mod fleet; +pub mod ids; // The single ID-minting module (UUIDv7 records, UUIDv8 content ids) // gitbot-fleet coordination layer pub mod llm; // BoJ-mediated LLM client (Consultant-mode Q&A) pub mod modes; // Bot operating modes (Verifier/Advisor/Consultant/Regulator) pub mod observability; // Structured logging + OpenTelemetry distributed tracing (OTLP) diff --git a/src/main.rs b/src/main.rs index e0f62eb..d5d1f9b 100644 --- a/src/main.rs +++ b/src/main.rs @@ -288,6 +288,7 @@ async fn serve( config.scheduler.queue_size, )); let echidna = Arc::new(EchidnaClient::new(&config.echidna)); + startup_handshake(&echidna).await?; let graphql_state = GraphQLState { store: store.clone(), @@ -751,6 +752,7 @@ async fn run_scheduler_loop( failed_files: vec![], confidence: None, axioms: None, + trust_source: echidnabot::dispatcher::TrustSource::LocalFallback, } } }; @@ -852,6 +854,7 @@ async fn report_to_platform( artifacts: vec![], confidence: job_result.confidence.clone(), axioms: job_result.axioms.clone(), + trust_source: job_result.trust_source, }; // Tactic suggestions for Advisor / Consultant / Regulator. Verifier @@ -1177,6 +1180,37 @@ async fn record_feedback( } } +/// Minimum-version handshake at start-up. +/// +/// An ECHIDNA that answers but is too old (or reports a non-semver version) +/// stops start-up: every result it produced would be read with the wrong +/// contract. An ECHIDNA that is not reachable yet only warns; each job runs +/// the handshake again before it dispatches (see `process_job`). +async fn startup_handshake(echidna: &EchidnaClient) -> Result<()> { + match echidna.handshake().await { + Ok(h) => { + tracing::info!( + "ECHIDNA {} handshake ok ({} provers listed; minimum {})", + h.version, + h.provers.len(), + echidnabot::dispatcher::MIN_ECHIDNA_VERSION + ); + Ok(()) + } + Err(echidnabot::Error::Echidna(msg)) => Err(echidnabot::Error::Echidna(format!( + "ECHIDNA handshake failed: {msg}" + ))), + Err(other) => { + tracing::warn!( + "ECHIDNA not reachable at start-up ({other}); jobs will retry the handshake" + ); + Ok(()) + } + } +} + +/// Run one proof job: check ECHIDNA (health + version handshake), find the +/// proof files, verify each one, and aggregate status, axioms and trust. async fn process_job( job: &ProofJob, store: &dyn Store, @@ -1190,6 +1224,9 @@ async fn process_job( "ECHIDNA core reported unhealthy status".to_string(), )); } + if !config.executor.local_isolation { + echidna.ensure_handshake().await?; + } let status = echidna.prover_status(&job.prover).await?; if status != ProverStatus::Available { @@ -1243,6 +1280,7 @@ async fn process_job( failed_files: vec![], confidence: None, axioms: None, + trust_source: echidnabot::dispatcher::TrustSource::LocalFallback, }); } @@ -1251,6 +1289,11 @@ async fn process_job( let mut verified = Vec::new(); let mut failed = Vec::new(); let mut prover_output = String::new(); + // Source-level axiom scan (ECHIDNA's canonical scanner) over every file, + // merged with whatever ECHIDNA itself reported per file. + let mut source_axioms: Option = None; + // `Echidna` only if ECHIDNA reported trust for every file it verified. + let mut all_trust_from_echidna = true; // Build the local sandboxed executor once (only when configured). // When `executor.local_isolation = false` (default), proofs delegate @@ -1297,6 +1340,12 @@ async fn process_job( repo_path.join(path) }; let content = fs::read_to_string(&full_path).await?; + let file_axioms = + echidnabot::trust::axiom_tracker::AxiomTracker::scan_source(&job.prover, &content); + source_axioms = Some(match source_axioms.take() { + Some(acc) => acc.merge(file_axioms), + None => file_axioms, + }); let (verified_ok, output_chunk) = if let Some(ref ex) = local_executor { // Local sandboxed path. ExecutionResult is success on @@ -1318,6 +1367,15 @@ async fn process_job( } else { // ECHIDNA-delegated path (default). let result = echidna.verify_proof(&job.prover, &content).await?; + if result.trust_source != echidnabot::dispatcher::TrustSource::Echidna { + all_trust_from_echidna = false; + } + if let Some(reported) = result.axioms { + source_axioms = Some(match source_axioms.take() { + Some(acc) => acc.merge(reported), + None => reported, + }); + } ( result.status == echidnabot::dispatcher::ProofStatus::Verified, result.prover_output, @@ -1349,9 +1407,26 @@ async fn process_job( } else { echidnabot::dispatcher::ProofStatus::Failed }; - let axioms = echidnabot::trust::axiom_tracker::AxiomTracker::scan(&job.prover, &prover_output); - let confidence = - echidnabot::trust::confidence::assess_confidence(&job.prover, final_status, false, 1); + let output_axioms = + echidnabot::trust::axiom_tracker::AxiomTracker::scan(&job.prover, &prover_output); + let axioms = match source_axioms { + Some(src) => src.merge(output_axioms), + None => output_axioms, + }; + let confidence = echidnabot::trust::confidence::assess_confidence_with_axioms( + &job.prover, + final_status, + false, + 1, + axioms.worst_danger, + ); + // The level is always computed by ECHIDNA's trust kernel (linked in); + // `Echidna` here means every file's axiom data was reported by ECHIDNA. + let trust_source = if local_executor.is_none() && all_trust_from_echidna { + echidnabot::dispatcher::TrustSource::Echidna + } else { + echidnabot::dispatcher::TrustSource::LocalFallback + }; Ok(echidnabot::scheduler::JobResult { success, message, @@ -1361,6 +1436,7 @@ async fn process_job( failed_files: failed, confidence: Some(confidence), axioms: Some(axioms), + trust_source, }) } diff --git a/src/observability.rs b/src/observability.rs index adc8f01..8c8eb9f 100644 --- a/src/observability.rs +++ b/src/observability.rs @@ -420,8 +420,11 @@ mod tests { hook().await; } - #[test] - fn into_coordinator_hook_drains_provider_idempotent_with_shutdown() { + /// After `into_coordinator_hook` takes the provider, `shutdown` is a no-op. + /// Runs inside a Tokio runtime: building the tonic exporter needs a + /// reactor since the hyper-util 0.1.20 / tracing-opentelemetry 0.34 bump. + #[tokio::test] + async fn into_coordinator_hook_drains_provider_idempotent_with_shutdown() { // Idempotency contract: after into_coordinator_hook() has taken // the provider, calling shutdown() consumes self without // touching anything (provider is None, branch elided). diff --git a/src/result_formatter.rs b/src/result_formatter.rs index 3167ea3..dd3ac56 100644 --- a/src/result_formatter.rs +++ b/src/result_formatter.rs @@ -153,6 +153,7 @@ mod tests { artifacts: vec![], confidence: None, axioms: None, + trust_source: Default::default(), } } @@ -165,6 +166,7 @@ mod tests { artifacts: vec![], confidence: None, axioms: None, + trust_source: Default::default(), } } diff --git a/src/scheduler/job_queue.rs b/src/scheduler/job_queue.rs index 570f993..28cb505 100644 --- a/src/scheduler/job_queue.rs +++ b/src/scheduler/job_queue.rs @@ -282,14 +282,14 @@ mod tests { let scheduler = JobScheduler::new(2, 10); let job1 = ProofJob::new( - Uuid::new_v4(), + crate::ids::new_record_id(), "abc123".to_string(), ProverKind::new("metamath"), vec!["test.mm".to_string()], ); let job2 = ProofJob::new( - Uuid::new_v4(), + crate::ids::new_record_id(), "def456".to_string(), ProverKind::new("metamath"), vec!["test2.mm".to_string()], @@ -313,7 +313,7 @@ mod tests { #[tokio::test] async fn test_duplicate_detection() { let scheduler = JobScheduler::new(2, 10); - let repo_id = Uuid::new_v4(); + let repo_id = crate::ids::new_record_id(); let job1 = ProofJob::new( repo_id, @@ -339,7 +339,7 @@ mod tests { #[tokio::test] async fn test_priority_ordering() { let scheduler = JobScheduler::new(1, 10); - let repo_id = Uuid::new_v4(); + let repo_id = crate::ids::new_record_id(); let low_priority = ProofJob::new( repo_id, diff --git a/src/scheduler/mod.rs b/src/scheduler/mod.rs index d4485d0..ff85372 100644 --- a/src/scheduler/mod.rs +++ b/src/scheduler/mod.rs @@ -25,8 +25,9 @@ use crate::trust::{axiom_tracker::AxiomReport, confidence::ConfidenceReport}; pub struct JobId(pub Uuid); impl JobId { + /// Mint a fresh job id (UUIDv7 via [`crate::ids::new_record_id`]). pub fn new() -> Self { - Self(Uuid::new_v4()) + Self(crate::ids::new_record_id()) } } @@ -167,7 +168,10 @@ pub struct JobResult { /// Confidence level assessed over the aggregated prover output. #[serde(default)] pub confidence: Option, - /// Axiom usage flags found in the aggregated prover output. + /// Axiom usage flags found in the proof sources and prover output. #[serde(default)] pub axioms: Option, + /// Provenance of `confidence` / `axioms`. + #[serde(default)] + pub trust_source: crate::dispatcher::TrustSource, } diff --git a/src/store/models.rs b/src/store/models.rs index e67475f..6164316 100644 --- a/src/store/models.rs +++ b/src/store/models.rs @@ -13,7 +13,7 @@ use crate::modes::BotMode; use crate::scheduler::{JobId, JobPriority, JobStatus}; /// Repository record -#[derive(Debug, Clone, Serialize, Deserialize)] +#[derive(Clone, Serialize, Deserialize)] pub struct Repository { pub id: Uuid, pub platform: Platform, @@ -43,15 +43,45 @@ pub struct Repository { pub regulator_coverage_threshold: u8, } +impl std::fmt::Debug for Repository { + /// Debug output with `webhook_secret` redacted (log-leak guard). + fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result { + f.debug_struct("Repository") + .field("id", &self.id) + .field("platform", &self.platform) + .field("owner", &self.owner) + .field("name", &self.name) + .field( + "webhook_secret", + &crate::config::redacted(&self.webhook_secret), + ) + .field("enabled_provers", &self.enabled_provers) + .field("check_on_push", &self.check_on_push) + .field("check_on_pr", &self.check_on_pr) + .field("auto_comment", &self.auto_comment) + .field("enabled", &self.enabled) + .field("last_checked_commit", &self.last_checked_commit) + .field("created_at", &self.created_at) + .field("updated_at", &self.updated_at) + .field("mode", &self.mode) + .field( + "regulator_coverage_threshold", + &self.regulator_coverage_threshold, + ) + .finish() + } +} + fn default_regulator_threshold() -> u8 { 100 } impl Repository { + /// New repository record with defaults and a fresh UUIDv7 id. pub fn new(platform: Platform, owner: String, name: String) -> Self { let now = Utc::now(); Self { - id: Uuid::new_v4(), + id: crate::ids::new_record_id(), platform, owner, name, @@ -136,9 +166,10 @@ pub struct ProofResultRecord { } impl ProofResultRecord { + /// Persistable record of a job result, with a fresh UUIDv7 id. pub fn new(job_id: JobId, result: &crate::scheduler::JobResult) -> Self { Self { - id: Uuid::new_v4(), + id: crate::ids::new_record_id(), job_id: job_id.0, success: result.success, message: result.message.clone(), @@ -180,6 +211,7 @@ pub struct TacticOutcomeRecord { } impl TacticOutcomeRecord { + /// Record of one tactic attempt, with a fresh UUIDv7 id. pub fn new( job_id: Option, prover: ProverKind, @@ -189,7 +221,7 @@ impl TacticOutcomeRecord { duration_ms: i64, ) -> Self { Self { - id: Uuid::new_v4(), + id: crate::ids::new_record_id(), job_id, prover, goal_fingerprint, diff --git a/src/store/sqlite.rs b/src/store/sqlite.rs index 9821bcc..946f017 100644 --- a/src/store/sqlite.rs +++ b/src/store/sqlite.rs @@ -802,8 +802,10 @@ mod tests { use crate::store::models::{goal_fingerprint, TacticOutcomeRecord}; async fn fresh_store() -> (SqliteStore, std::path::PathBuf) { - let path = - std::env::temp_dir().join(format!("echidnabot-store-test-{}.db", Uuid::new_v4())); + let path = std::env::temp_dir().join(format!( + "echidnabot-store-test-{}.db", + crate::ids::new_record_id() + )); let url = format!("sqlite://{}?mode=rwc", path.display()); let store = SqliteStore::new(&url).await.expect("open store"); (store, path) diff --git a/src/trust/axiom_tracker.rs b/src/trust/axiom_tracker.rs index 43657d9..e81b90d 100644 --- a/src/trust/axiom_tracker.rs +++ b/src/trust/axiom_tracker.rs @@ -15,7 +15,20 @@ //! - `axiom` (Lean4) -- user-declared axiom //! - `assume` (Metamath) -- hypothesis without proof //! - Classical logic axioms (excluded middle, double negation elimination) - +//! +//! Two scanners live here and they read different things: +//! +//! - [`AxiomTracker::scan_source`] reads the **proof source** and delegates to +//! ECHIDNA's canonical scanner (`echidna_core_spark::axiom_tracker`), which +//! skips comment lines and ECHIDNA's own scaffold markers. This is the +//! primary signal and is shared with ECHIDNA, not re-implemented. +//! - [`AxiomTracker::scan`] reads the **prover's output text** (for example +//! Lean's "declaration uses 'sorry'"). ECHIDNA has no equivalent, so this +//! stays local, as a fallback for when the source is unavailable. + +use echidna_core_spark::axiom_tracker::{ + AxiomTracker as EchidnaAxiomTracker, AxiomUsage, DangerLevel, +}; use serde::{Deserialize, Serialize}; use crate::dispatcher::ProverKind; @@ -79,6 +92,33 @@ impl AxiomFlag { pub fn is_unsound(&self) -> bool { self.severity() >= 3 } + + /// The ECHIDNA danger level this flag corresponds to. + /// + /// `--type-in-type` can manufacture false theorems, so it is `Reject`; + /// the other unsound holes are `Warning` (ECHIDNA's level for `sorry`, + /// `Admitted` and `oops`); everything else is `Noted`. + pub fn danger_level(&self) -> DangerLevel { + match self { + Self::TypeInType => DangerLevel::Reject, + Self::Sorry | Self::Admitted | Self::Oops | Self::Postulate => DangerLevel::Warning, + _ => DangerLevel::Noted, + } + } + + /// Map one ECHIDNA source-scan finding onto the local flag vocabulary. + fn from_usage(usage: &AxiomUsage) -> Self { + match usage.construct.trim() { + "sorry" => Self::Sorry, + "Admitted" | "admit" => Self::Admitted, + "postulate" | "{!!}" => Self::Postulate, + "--type-in-type" | "OPTIONS --type-in-type" => Self::TypeInType, + "oops" => Self::Oops, + "axiom" | "Axiom" => Self::UserAxiom, + "assume" => Self::UndischargedAssumption, + other => Self::Other(other.to_string()), + } + } } impl std::fmt::Display for AxiomFlag { @@ -100,6 +140,15 @@ pub struct AxiomReport { pub warning_count: usize, /// Overall assessment pub clean: bool, + /// Worst ECHIDNA danger level found, the input to the trust kernel. + /// Older stored reports lack the field and deserialise as `Safe`. + #[serde(default = "safe")] + pub worst_danger: DangerLevel, +} + +/// Serde default for [`AxiomReport::worst_danger`]. +fn safe() -> DangerLevel { + DangerLevel::Safe } impl AxiomReport { @@ -116,6 +165,43 @@ impl AxiomReport { .collect() } + /// Combine two reports on the same proof (for example a source scan and + /// an output scan): the union of the flags and the worse danger level. + pub fn merge(mut self, other: AxiomReport) -> AxiomReport { + let worst = DangerLevel::max_danger(self.worst_danger, other.worst_danger); + self.flags.extend(other.flags); + let mut report = AxiomReport::from_flags(self.prover, self.flags); + report.worst_danger = DangerLevel::max_danger(report.worst_danger, worst); + report + } + + /// Build a report from axiom names ECHIDNA reported (the + /// `echidna.prove.result/1` `trust.axioms` list). + pub fn from_reported(prover: ProverKind, flags: impl IntoIterator) -> Self { + AxiomReport::from_flags(prover, flags.into_iter().collect()) + } + + /// Build a report from raw flags, deduplicating and counting them. + fn from_flags(prover: ProverKind, mut flags: Vec) -> AxiomReport { + flags.sort_by_key(|f| std::cmp::Reverse(f.severity())); + flags.dedup(); + let unsound_count = flags.iter().filter(|f| f.severity() >= 3).count(); + let warning_count = flags.iter().filter(|f| f.severity() == 2).count(); + let clean = flags.is_empty(); + let worst_danger = flags + .iter() + .map(AxiomFlag::danger_level) + .fold(DangerLevel::Safe, DangerLevel::max_danger); + AxiomReport { + prover, + flags, + unsound_count, + warning_count, + clean, + worst_danger, + } + } + /// Format as a human-readable summary pub fn summary(&self) -> String { if self.clean { @@ -166,21 +252,34 @@ impl AxiomTracker { // Universal patterns (apply to all provers) scan_universal(&output_lower, &mut flags); - // Deduplicate flags - flags.sort_by_key(|f| std::cmp::Reverse(f.severity())); - flags.dedup(); + AxiomReport::from_flags(prover.clone(), flags) + } - let unsound_count = flags.iter().filter(|f| f.severity() >= 3).count(); - let warning_count = flags.iter().filter(|f| f.severity() == 2).count(); - let clean = flags.is_empty(); + /// Scan proof **source** with ECHIDNA's canonical axiom scanner. + /// + /// Provers ECHIDNA has no pattern table for yield a clean report; the + /// slug is normalised (`hol-light` → `hollight`, `lean4` → `lean`) to + /// ECHIDNA's keys first. + pub fn scan_source(prover: &ProverKind, source: &str) -> AxiomReport { + let usages = EchidnaAxiomTracker::new().scan(&echidna_scanner_key(prover), source); + let flags = usages.iter().map(AxiomFlag::from_usage).collect(); + let mut report = AxiomReport::from_flags(prover.clone(), flags); + report.worst_danger = usages + .iter() + .map(|u| u.danger_level) + .fold(report.worst_danger, DangerLevel::max_danger); + report + } +} - AxiomReport { - prover: prover.clone(), - flags, - unsound_count, - warning_count, - clean, - } +/// ECHIDNA's scanner-table key for an echidnabot prover slug. +fn echidna_scanner_key(prover: &ProverKind) -> String { + match prover.as_str() { + "lean4" => "lean".to_string(), + "rocq" => "coq".to_string(), + "idris" => "idris2".to_string(), + "f*" | "f-star" => "fstar".to_string(), + other => other.replace(['-', '_'], ""), } } @@ -408,4 +507,39 @@ mod tests { let warnings = report.flags_at_severity(2); assert!(warnings.len() >= 2); // sorry + axiom } + + #[test] + fn test_source_scan_uses_echidna_patterns() { + let report = AxiomTracker::scan_source( + &ProverKind::new("lean"), + "theorem t : 1 = 1 := by\n sorry\n", + ); + assert!(report.flags.contains(&AxiomFlag::Sorry)); + assert_eq!(report.worst_danger, DangerLevel::Warning); + } + + #[test] + fn test_source_scan_skips_comments_and_scaffold() { + let report = AxiomTracker::scan_source( + &ProverKind::new("lean"), + "-- sorry in a comment is documentation\ntheorem t : True := trivial\n", + ); + assert!(report.clean, "{:?}", report.flags); + assert_eq!(report.worst_danger, DangerLevel::Safe); + } + + #[test] + fn test_source_scan_idris_believe_me_is_reject() { + let report = AxiomTracker::scan_source(&ProverKind::new("idris2"), "f = believe_me x\n"); + assert_eq!(report.worst_danger, DangerLevel::Reject); + } + + #[test] + fn test_merge_keeps_worst_danger() { + let output = AxiomTracker::scan(&ProverKind::new("lean"), "All goals discharged"); + let source = AxiomTracker::scan_source(&ProverKind::new("lean"), " sorry\n"); + let merged = output.merge(source); + assert!(merged.has_unsound()); + assert_eq!(merged.worst_danger, DangerLevel::Warning); + } } diff --git a/src/trust/confidence.rs b/src/trust/confidence.rs index 8986441..a96f681 100644 --- a/src/trust/confidence.rs +++ b/src/trust/confidence.rs @@ -3,30 +3,40 @@ // SPDX-FileCopyrightText: 2025 Jonathan D.A. Jewell //! Proof confidence level assessment //! -//! Maps ECHIDNA verification results to a 5-level trust scale based on: -//! - Prover kernel size (small-kernel = higher trust) -//! - Number of independent checkers used -//! - Presence of proof certificates -//! - Prover tier within ECHIDNA - +//! The trust-level *algorithm* is ECHIDNA's, not echidnabot's: every call +//! goes through [`echidna_core_spark::compute_trust_level`] (the Creusot- +//! annotated kernel shared with ECHIDNA). This module only translates +//! echidnabot's inputs (prover slug, status, artefacts, axiom scan) into +//! ECHIDNA's [`TrustFactors`] and wraps the answer in a report. +//! +//! Epistemic note (pattern from `hyperpolymath/epistemic-types`, not a +//! dependency): a level computed here is a *warrant* — echidnabot's own +//! reading of ECHIDNA's output. When ECHIDNA itself supplies trust data in an +//! `echidna.prove.result/1` object, that is the *receipt* and is preferred; +//! see [`crate::dispatcher::TrustSource`]. + +use echidna_core_spark::axiom_tracker::DangerLevel; +use echidna_core_spark::{compute_trust_level, ProverClass, TrustFactors, TrustLevel}; use serde::{Deserialize, Serialize}; use crate::dispatcher::{ProofStatus, ProverKind}; /// Confidence level for a proof verification result. /// -/// Higher levels indicate stronger trust in the result. +/// Mirrors ECHIDNA's [`TrustLevel`] one-to-one (see the `From` impls); it is +/// kept as a local type only so echidnabot can attach presentation methods +/// (`label`, `Display`) to it. #[derive(Debug, Clone, Copy, PartialEq, Eq, PartialOrd, Ord, Hash, Serialize, Deserialize)] pub enum ConfidenceLevel { - /// Large-TCB system or unchecked result + /// Large-TCB system, unchecked result, or dangerous axioms present Level1 = 1, - /// Single prover result without certificate + /// Single prover result without a verified certificate Level2 = 2, - /// Single prover with proof certificate (Alethe, DRAT/LRAT) + /// Verified certificate, or cross-checked by 2+ provers Level3 = 3, - /// Checked by small-kernel system (Lean4, Coq, Isabelle) with certificate + /// Small-kernel system with a verified certificate Level4 = 4, - /// Cross-checked by 2+ independent small-kernel systems + /// Cross-checked by 2+ small-kernel systems with verified certificates Level5 = 5, } @@ -39,11 +49,11 @@ impl ConfidenceLevel { /// Human-readable label pub fn label(&self) -> &'static str { match self { - Self::Level1 => "Minimal (large-TCB / unchecked)", - Self::Level2 => "Low (single prover, no certificate)", - Self::Level3 => "Moderate (single prover + certificate)", - Self::Level4 => "High (small-kernel + certificate)", - Self::Level5 => "Maximum (cross-checked by 2+ systems)", + Self::Level1 => "Minimal (large-TCB / unchecked / dangerous axioms)", + Self::Level2 => "Low (single prover, no verified certificate)", + Self::Level3 => "Moderate (verified certificate or cross-checked)", + Self::Level4 => "High (small-kernel + verified certificate)", + Self::Level5 => "Maximum (cross-checked by 2+ small-kernel systems)", } } @@ -53,7 +63,34 @@ impl ConfidenceLevel { } } +impl From for ConfidenceLevel { + /// Translate ECHIDNA's trust level into the local presentation type. + fn from(level: TrustLevel) -> Self { + match level { + TrustLevel::Level1 => Self::Level1, + TrustLevel::Level2 => Self::Level2, + TrustLevel::Level3 => Self::Level3, + TrustLevel::Level4 => Self::Level4, + TrustLevel::Level5 => Self::Level5, + } + } +} + +impl From for TrustLevel { + /// Translate the local presentation type back into ECHIDNA's trust level. + fn from(level: ConfidenceLevel) -> Self { + match level { + ConfidenceLevel::Level1 => Self::Level1, + ConfidenceLevel::Level2 => Self::Level2, + ConfidenceLevel::Level3 => Self::Level3, + ConfidenceLevel::Level4 => Self::Level4, + ConfidenceLevel::Level5 => Self::Level5, + } + } +} + impl std::fmt::Display for ConfidenceLevel { + /// Render as `Level N (label)`. fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result { write!(f, "Level {} ({})", self.value(), self.label()) } @@ -76,7 +113,10 @@ pub struct ConfidenceReport { pub justification: String, } -/// Assess the confidence level of a proof verification result. +/// Assess the confidence level of a proof verification result with no +/// axiom information (treated as no dangerous axioms found). +/// +/// Prefer [`assess_confidence_with_axioms`] whenever an axiom scan exists. /// /// # Arguments /// * `prover` - Which prover produced the result @@ -89,6 +129,31 @@ pub fn assess_confidence( has_certificate: bool, checker_count: usize, ) -> ConfidenceReport { + assess_confidence_with_axioms( + prover, + status, + has_certificate, + checker_count, + DangerLevel::Safe, + ) +} + +/// Assess the confidence level of a proof result using ECHIDNA's canonical +/// trust algorithm. +/// +/// echidnabot never verifies certificates itself, so `certificate_verified` +/// is always passed as `false`: a certificate artefact raises nothing above +/// Level 2 on its own. Solver integrity is checked elsewhere +/// ([`crate::trust::SolverIntegrity`]) and is assumed here. +pub fn assess_confidence_with_axioms( + prover: &ProverKind, + status: ProofStatus, + has_certificate: bool, + checker_count: usize, + worst_axiom_danger: DangerLevel, +) -> ConfidenceReport { + let small_kernel = is_small_kernel(prover); + // Only verified proofs get meaningful confidence levels if status != ProofStatus::Verified { return ConfidenceReport { @@ -96,7 +161,7 @@ pub fn assess_confidence( prover: prover.clone(), has_certificate: false, checker_count: 0, - small_kernel: is_small_kernel(prover), + small_kernel, justification: format!( "Proof status is {:?} (not Verified) -- confidence is minimal", status @@ -104,83 +169,48 @@ pub fn assess_confidence( }; } - let small_kernel = is_small_kernel(prover); - - // Level 5: Cross-checked by 2+ independent small-kernel systems - if checker_count >= 2 && small_kernel { - return ConfidenceReport { - level: ConfidenceLevel::Level5, - prover: prover.clone(), - has_certificate, - checker_count, - small_kernel, - justification: format!( - "Cross-checked by {} independent small-kernel systems ({})", - checker_count, - prover.display_name() - ), - }; - } + let factors = TrustFactors { + prover_class: prover_class(prover), + confirming_provers: u32::try_from(checker_count).unwrap_or(u32::MAX), + has_certificate, + certificate_verified: false, + worst_axiom_danger, + solver_integrity_ok: true, + }; + let level = ConfidenceLevel::from(compute_trust_level(&factors)); - // Level 4: Small-kernel system with certificate - if small_kernel && has_certificate { - return ConfidenceReport { - level: ConfidenceLevel::Level4, - prover: prover.clone(), - has_certificate, - checker_count, - small_kernel, - justification: format!( - "Verified by small-kernel system ({}) with proof certificate", - prover.display_name() - ), - }; - } - - // Level 3: Single prover with proof certificate (e.g., Z3 with DRAT/LRAT) - if has_certificate { - return ConfidenceReport { - level: ConfidenceLevel::Level3, - prover: prover.clone(), - has_certificate, - checker_count, - small_kernel, - justification: format!( - "Verified by {} with proof certificate", - prover.display_name() - ), - }; - } - - // Level 2: Single prover without certificate but with small kernel - if small_kernel { - return ConfidenceReport { - level: ConfidenceLevel::Level2, - prover: prover.clone(), - has_certificate, - checker_count, - small_kernel, - justification: format!( - "Verified by small-kernel system ({}) without proof certificate", - prover.display_name() - ), - }; - } - - // Level 1: Large-TCB or stub prover ConfidenceReport { - level: ConfidenceLevel::Level1, + level, prover: prover.clone(), - has_certificate: false, + has_certificate, checker_count, - small_kernel: false, + small_kernel, justification: format!( - "Verified by large-TCB system ({}) -- consider cross-checking", - prover.display_name() + "ECHIDNA trust kernel: {} ({}, {} checker(s), certificate {}, worst axiom danger {})", + TrustLevel::from(level).description(), + prover.display_name(), + checker_count, + if has_certificate { + "present but not independently verified" + } else { + "absent" + }, + worst_axiom_danger ), } } +/// Classify a prover slug into ECHIDNA's coarse [`ProverClass`]. +pub fn prover_class(prover: &ProverKind) -> ProverClass { + if is_small_kernel(prover) { + return ProverClass::SmallKernel; + } + match prover.as_str() { + "z3" | "cvc5" | "alt-ergo" | "vampire" | "eprover" | "spass" => ProverClass::SmtOrAtp, + _ => ProverClass::Other, + } +} + /// Determine if a prover uses a small, trusted kernel. /// /// Small-kernel provers have a minimal trusted code base for proof checking, @@ -278,45 +308,58 @@ mod tests { } #[test] - fn test_assess_level5_cross_checked() { - let report = assess_confidence( - &ProverKind::new("lean"), - ProofStatus::Verified, - true, - 3, // 3 independent checkers - ); - assert_eq!(report.level, ConfidenceLevel::Level5); + fn test_assess_cross_checked_without_verified_cert_is_level3() { + // ECHIDNA's kernel needs a *verified* certificate for Level 5; two or + // more agreeing provers without one earn Level 3. + let report = assess_confidence(&ProverKind::new("lean"), ProofStatus::Verified, true, 3); + assert_eq!(report.level, ConfidenceLevel::Level3); assert!(report.small_kernel); assert_eq!(report.checker_count, 3); } #[test] - fn test_assess_level4_small_kernel_with_cert() { - let report = assess_confidence(&ProverKind::new("coq"), ProofStatus::Verified, true, 1); - assert_eq!(report.level, ConfidenceLevel::Level4); + fn test_assess_single_prover_with_unverified_cert_is_level2() { + // echidnabot never verifies certificates, so a cert artefact alone + // does not lift a single result above Level 2. + for slug in ["coq", "z3"] { + let report = assess_confidence(&ProverKind::new(slug), ProofStatus::Verified, true, 1); + assert_eq!(report.level, ConfidenceLevel::Level2, "{slug}"); + } } #[test] - fn test_assess_level3_cert_no_small_kernel() { - let report = assess_confidence( - &ProverKind::new("z3"), - ProofStatus::Verified, - true, // Has DRAT/LRAT certificate - 1, - ); - assert_eq!(report.level, ConfidenceLevel::Level3); + fn test_assess_single_prover_no_cert_is_level2() { + for slug in ["lean", "pvs"] { + let report = assess_confidence(&ProverKind::new(slug), ProofStatus::Verified, false, 1); + assert_eq!(report.level, ConfidenceLevel::Level2, "{slug}"); + } } #[test] - fn test_assess_level2_small_kernel_no_cert() { - let report = assess_confidence(&ProverKind::new("lean"), ProofStatus::Verified, false, 1); - assert_eq!(report.level, ConfidenceLevel::Level2); + fn test_assess_dangerous_axioms_cap_at_level1() { + for danger in [DangerLevel::Warning, DangerLevel::Reject] { + let report = assess_confidence_with_axioms( + &ProverKind::new("lean"), + ProofStatus::Verified, + true, + 3, + danger, + ); + assert_eq!(report.level, ConfidenceLevel::Level1); + } } #[test] - fn test_assess_level1_large_tcb() { - let report = assess_confidence(&ProverKind::new("pvs"), ProofStatus::Verified, false, 1); - assert_eq!(report.level, ConfidenceLevel::Level1); + fn test_level_round_trips_through_echidna() { + for level in [ + ConfidenceLevel::Level1, + ConfidenceLevel::Level2, + ConfidenceLevel::Level3, + ConfidenceLevel::Level4, + ConfidenceLevel::Level5, + ] { + assert_eq!(ConfidenceLevel::from(TrustLevel::from(level)), level); + } } #[test] diff --git a/tests/integration_tests.rs b/tests/integration_tests.rs index b9a33aa..8309063 100644 --- a/tests/integration_tests.rs +++ b/tests/integration_tests.rs @@ -29,7 +29,6 @@ use axum::http::HeaderMap; use hmac::{Hmac, KeyInit, Mac}; use sha2::Sha256; use std::time::Duration; -use uuid::Uuid; // ============================================================================= // Webhook Signature Verification Tests @@ -146,6 +145,7 @@ fn test_proof_result_parsing() { artifacts: vec!["proof.cert".to_string()], confidence: None, axioms: None, + trust_source: Default::default(), }; assert_eq!(result.status, ProofStatus::Verified); @@ -214,6 +214,7 @@ fn test_result_formatter_truncates_long_output() { artifacts: vec![], confidence: None, axioms: None, + trust_source: Default::default(), }; let formatted = format_proof_result( @@ -264,7 +265,7 @@ fn test_check_run_conclusion_values() { #[test] fn test_job_creation() { - let repo_id = Uuid::new_v4(); + let repo_id = echidnabot::ids::new_record_id(); let job = ProofJob::new( repo_id, "abc123def".to_string(), @@ -284,7 +285,7 @@ fn test_job_creation() { #[test] fn test_job_start_sets_running() { let mut job = ProofJob::new( - Uuid::new_v4(), + echidnabot::ids::new_record_id(), "abc123".to_string(), ProverKind::new("coq"), vec![], @@ -298,7 +299,7 @@ fn test_job_start_sets_running() { #[test] fn test_job_complete_success() { let mut job = ProofJob::new( - Uuid::new_v4(), + echidnabot::ids::new_record_id(), "abc123".to_string(), ProverKind::new("z3"), vec![], @@ -314,6 +315,7 @@ fn test_job_complete_success() { failed_files: vec![], confidence: None, axioms: None, + trust_source: Default::default(), }; job.complete(result); @@ -325,7 +327,7 @@ fn test_job_complete_success() { #[test] fn test_job_complete_failure() { let mut job = ProofJob::new( - Uuid::new_v4(), + echidnabot::ids::new_record_id(), "abc123".to_string(), ProverKind::new("lean"), vec![], @@ -341,6 +343,7 @@ fn test_job_complete_failure() { failed_files: vec!["test.lean".to_string()], confidence: None, axioms: None, + trust_source: Default::default(), }; job.complete(result); @@ -350,7 +353,7 @@ fn test_job_complete_failure() { #[test] fn test_job_cancel() { let mut job = ProofJob::new( - Uuid::new_v4(), + echidnabot::ids::new_record_id(), "abc123".to_string(), ProverKind::new("agda"), vec![], @@ -388,7 +391,7 @@ fn test_repository_model() { #[test] fn test_proof_job_record_from_job() { let job = ProofJob::new( - Uuid::new_v4(), + echidnabot::ids::new_record_id(), "sha256hash".to_string(), ProverKind::new("metamath"), vec!["proof.mm".to_string()], @@ -413,6 +416,7 @@ fn test_proof_result_record() { failed_files: vec![], confidence: None, axioms: None, + trust_source: Default::default(), }; let record = ProofResultRecord::new(job_id, &result); @@ -480,7 +484,7 @@ async fn test_executor_no_backend_refuses_proofs() { #[tokio::test] async fn test_scheduler_enqueue_dequeue_cycle() { let scheduler = JobScheduler::new(2, 10); - let repo_id = Uuid::new_v4(); + let repo_id = echidnabot::ids::new_record_id(); // Enqueue a job let job = ProofJob::new( @@ -511,6 +515,7 @@ async fn test_scheduler_enqueue_dequeue_cycle() { failed_files: vec![], confidence: None, axioms: None, + trust_source: Default::default(), }; scheduler.complete_job(job_id, result).await; @@ -530,7 +535,10 @@ async fn test_tactic_outcome_roundtrip_via_store() { use echidnabot::store::models::{goal_fingerprint, TacticOutcomeRecord}; use echidnabot::store::{SqliteStore, Store}; - let path = std::env::temp_dir().join(format!("echidnabot-test-outcomes-{}.db", Uuid::new_v4())); + let path = std::env::temp_dir().join(format!( + "echidnabot-test-outcomes-{}.db", + echidnabot::ids::new_record_id() + )); let url = format!("sqlite://{}?mode=rwc", path.display()); let store = SqliteStore::new(&url).await.unwrap(); @@ -574,7 +582,7 @@ async fn test_scheduler_metrics_methods() { assert_eq!(scheduler.queue_depth(), 0); // Enqueue some jobs and verify they become visible via stats - let repo_id = Uuid::new_v4(); + let repo_id = echidnabot::ids::new_record_id(); for i in 0..3 { let job = ProofJob::new( repo_id, @@ -594,13 +602,13 @@ async fn test_scheduler_respects_max_concurrent() { // Enqueue two jobs let job1 = ProofJob::new( - Uuid::new_v4(), + echidnabot::ids::new_record_id(), "commit1".to_string(), ProverKind::new("coq"), vec![], ); let job2 = ProofJob::new( - Uuid::new_v4(), + echidnabot::ids::new_record_id(), "commit2".to_string(), ProverKind::new("lean"), vec![], diff --git a/tests/lifecycle.rs b/tests/lifecycle.rs index 23f2089..6eec638 100644 --- a/tests/lifecycle.rs +++ b/tests/lifecycle.rs @@ -50,6 +50,7 @@ fn make_job_result(success: bool) -> JobResult { }, confidence: None, axioms: None, + trust_source: Default::default(), } } @@ -68,7 +69,7 @@ fn make_job(repo: Uuid, commit: &str, prover: &str) -> ProofJob { #[test] fn lifecycle_job_starts_queued() { - let job = make_job(Uuid::new_v4(), "abc123", "coq"); + let job = make_job(echidnabot::ids::new_record_id(), "abc123", "coq"); assert_eq!(job.status, JobStatus::Queued); assert!(job.started_at.is_none()); assert!(job.completed_at.is_none()); @@ -76,7 +77,7 @@ fn lifecycle_job_starts_queued() { #[test] fn lifecycle_job_transitions_queued_to_running() { - let mut job = make_job(Uuid::new_v4(), "abc123", "lean"); + let mut job = make_job(echidnabot::ids::new_record_id(), "abc123", "lean"); job.start(); assert_eq!(job.status, JobStatus::Running); assert!( @@ -87,7 +88,7 @@ fn lifecycle_job_transitions_queued_to_running() { #[test] fn lifecycle_job_transitions_running_to_completed() { - let mut job = make_job(Uuid::new_v4(), "def456", "coq"); + let mut job = make_job(echidnabot::ids::new_record_id(), "def456", "coq"); job.start(); job.complete(make_job_result(true)); assert_eq!(job.status, JobStatus::Completed); @@ -99,7 +100,7 @@ fn lifecycle_job_transitions_running_to_completed() { #[test] fn lifecycle_job_transitions_running_to_failed() { - let mut job = make_job(Uuid::new_v4(), "fail001", "lean"); + let mut job = make_job(echidnabot::ids::new_record_id(), "fail001", "lean"); job.start(); job.complete(make_job_result(false)); assert_eq!(job.status, JobStatus::Failed); @@ -107,14 +108,14 @@ fn lifecycle_job_transitions_running_to_failed() { #[test] fn lifecycle_job_cancel_from_queued() { - let mut job = make_job(Uuid::new_v4(), "ghi789", "metamath"); + let mut job = make_job(echidnabot::ids::new_record_id(), "ghi789", "metamath"); job.cancel(); assert_eq!(job.status, JobStatus::Cancelled); } #[test] fn lifecycle_job_duration_ms_after_completion() { - let mut job = make_job(Uuid::new_v4(), "abc", "lean"); + let mut job = make_job(echidnabot::ids::new_record_id(), "abc", "lean"); job.start(); job.complete(make_job_result(true)); let dur = job.duration_ms(); @@ -123,7 +124,7 @@ fn lifecycle_job_duration_ms_after_completion() { #[test] fn lifecycle_job_result_attached_after_completion() { - let mut job = make_job(Uuid::new_v4(), "res_check", "coq"); + let mut job = make_job(echidnabot::ids::new_record_id(), "res_check", "coq"); job.start(); job.complete(make_job_result(true)); assert!( @@ -150,7 +151,7 @@ async fn lifecycle_scheduler_empty_at_start() { #[tokio::test] async fn lifecycle_scheduler_full_job_cycle() { let sched = JobScheduler::new(2, 10); - let repo = Uuid::new_v4(); + let repo = echidnabot::ids::new_record_id(); let job = make_job(repo, "sha001", "coq"); let job_id = sched @@ -178,7 +179,7 @@ async fn lifecycle_scheduler_full_job_cycle() { #[tokio::test] async fn lifecycle_scheduler_cancel_queued_job() { let sched = JobScheduler::new(1, 10); - let repo = Uuid::new_v4(); + let repo = echidnabot::ids::new_record_id(); // Fill the single concurrent slot let blocker = make_job(repo, "sha_blocker", "lean"); @@ -201,7 +202,7 @@ async fn lifecycle_scheduler_cancel_queued_job() { #[tokio::test] async fn lifecycle_scheduler_max_concurrent_enforced() { let sched = JobScheduler::new(1, 10); - let repo = Uuid::new_v4(); + let repo = echidnabot::ids::new_record_id(); sched.enqueue(make_job(repo, "sha1", "coq")).await.unwrap(); sched.enqueue(make_job(repo, "sha2", "lean")).await.unwrap(); @@ -217,7 +218,7 @@ async fn lifecycle_scheduler_max_concurrent_enforced() { #[tokio::test] async fn lifecycle_scheduler_get_job_by_id() { let sched = JobScheduler::new(2, 10); - let job = make_job(Uuid::new_v4(), "get_me", "z3"); + let job = make_job(echidnabot::ids::new_record_id(), "get_me", "z3"); let job_id = sched.enqueue(job).await.unwrap().unwrap(); let found = sched.get_job(job_id).await; @@ -232,8 +233,8 @@ async fn lifecycle_scheduler_get_job_by_id() { #[tokio::test] async fn lifecycle_scheduler_jobs_for_repo() { let sched = JobScheduler::new(4, 20); - let repo_a = Uuid::new_v4(); - let repo_b = Uuid::new_v4(); + let repo_a = echidnabot::ids::new_record_id(); + let repo_b = echidnabot::ids::new_record_id(); sched.enqueue(make_job(repo_a, "a1", "coq")).await.unwrap(); sched.enqueue(make_job(repo_a, "a2", "lean")).await.unwrap(); @@ -423,7 +424,7 @@ async fn lifecycle_shutdown_timeout_fires_with_warning_when_drain_exceeds_deadli // active_count; do that via the normal enqueue+try_start_next flow. let sched = Arc::new(JobScheduler::new(2, 10)); let job = ProofJob::new( - Uuid::new_v4(), + echidnabot::ids::new_record_id(), "deadlock_sha".to_string(), ProverKind::new("coq"), vec!["slow.v".to_string()], diff --git a/tests/regressions/mod.rs b/tests/regressions/mod.rs index c855baa..8733ada 100644 --- a/tests/regressions/mod.rs +++ b/tests/regressions/mod.rs @@ -42,7 +42,7 @@ fn regression_prover_key_debug_format_bug_42e7bde() { #[tokio::test] async fn regression_duplicate_detection_respects_prover() { let sched = JobScheduler::new(4, 20); - let repo = Uuid::new_v4(); + let repo = echidnabot::ids::new_record_id(); let j1 = ProofJob::new(repo, "sha_dup".to_string(), ProverKind::new("coq"), vec![]); let j2 = ProofJob::new(repo, "sha_dup".to_string(), ProverKind::new("lean"), vec![]); // diff prover @@ -71,7 +71,7 @@ fn regression_goal_fingerprint_always_64_chars() { #[tokio::test] async fn regression_priority_queue_ordering() { let sched = JobScheduler::new(1, 10); - let repo = Uuid::new_v4(); + let repo = echidnabot::ids::new_record_id(); let low = ProofJob::new(repo, "low_sha".to_string(), ProverKind::new("coq"), vec![]) .with_priority(JobPriority::Low); From 5b023985149e73a643521805ea2d1e5385ee47ac Mon Sep 17 00:00:00 2001 From: "Jonathan D.A. Jewell" <6759885+hyperpolymath@users.noreply.github.com> Date: Mon, 5 Oct 2026 17:25:55 +0100 Subject: [PATCH 2/7] docs(wiki): ECHIDNA integration page; local 8081 default and version handshake Co-Authored-By: Claude Opus 5.5 --- wiki/ECHIDNA-Integration.md | 37 +++++++++++++++++++++++++++++++++++++ wiki/Getting-Started.md | 6 ++++-- wiki/Home.md | 2 +- 3 files changed, 42 insertions(+), 3 deletions(-) create mode 100644 wiki/ECHIDNA-Integration.md diff --git a/wiki/ECHIDNA-Integration.md b/wiki/ECHIDNA-Integration.md new file mode 100644 index 0000000..6eea287 --- /dev/null +++ b/wiki/ECHIDNA-Integration.md @@ -0,0 +1,37 @@ + +# ECHIDNA Integration + +echidnabot orchestrates; [ECHIDNA](https://github.com/hyperpolymath/echidna) proves. This page is the user-facing summary of `docs/ECHIDNA-INTEGRATION.adoc` in the repository, which is the authoritative record. + +## Connecting + +- Default endpoints: `http://127.0.0.1:8081` (REST) and `http://127.0.0.1:8081/graphql`, the address `echidna server` listens on. +- **Version handshake:** on start-up echidnabot reads `GET /api/provers` (and `/api/health` if needed) and refuses to run against an ECHIDNA older than **2.3.0**. An unreachable ECHIDNA only logs a warning; every job retries the handshake before dispatching. +- Prover names are taken from ECHIDNA's own `/api/provers` list, so new ECHIDNA backends need no echidnabot change. + +## Trust levels + +The 5-level confidence shown in check runs and PR comments is computed by **ECHIDNA's trust kernel** (linked as a library), not by an echidnabot copy. Axioms and holes (`sorry`, `Admitted`, `postulate`, `believe_me`, ...) are found by ECHIDNA's source scanner, plus a scan of the prover's output text. + +echidnabot never verifies proof certificates itself, so a certificate artefact on its own does not raise a single result above Level 2. + +Each result says where its trust data came from: + +| Source | Meaning | +|---|---| +| `echidna` | ECHIDNA reported the axioms itself (`echidna.prove.result/1` `trust` object), passed on unchanged | +| `local-fallback` | echidnabot derived the axioms from the proof source and prover output | + +## The `echidna.prove.result/1` contract + +When ECHIDNA answers in the shared contract shape, echidnabot reads it directly: + +```json +{"duration_ms":12,"echidna_version":"2.3.0","goal":"t","message":"ok","prover":"Lean","schema":"echidna.prove.result/1","status":"verified","trust":{"axioms":[],"confidence":null}} +``` + +`status` is one of `verified`, `failed`, `error`, `timeout`, `unknown`. Older ECHIDNA response bodies are still accepted. + +## Identifiers + +echidnabot mints UUIDv7 ids for jobs and records. For content (proof goals, prove results) it uses UUIDv8 content ids: SHA-256 over the RFC 8785 canonical JSON, the same construction ECHIDNA and proof-burrower use. diff --git a/wiki/Getting-Started.md b/wiki/Getting-Started.md index f7b013b..7c1ca3c 100644 --- a/wiki/Getting-Started.md +++ b/wiki/Getting-Started.md @@ -60,8 +60,10 @@ name = "your-repo" enabled = ["coq", "lean4"] [echidna] -# Use public instance or self-host -endpoint = "https://echidna.hyperpolymath.dev/graphql" +# Default: a local `echidna server` on port 8081 (REST + GraphQL). +# echidnabot checks the server is ECHIDNA >= 2.3.0 at start-up. +endpoint = "http://127.0.0.1:8081/graphql" +rest_endpoint = "http://127.0.0.1:8081" ``` ### 2. Set Up Webhook diff --git a/wiki/Home.md b/wiki/Home.md index 15f80bc..3652e5b 100644 --- a/wiki/Home.md +++ b/wiki/Home.md @@ -72,7 +72,7 @@ Every commit with proof files gets verified. Broken proofs block merges (in `reg | **4 Bot Modes** | Verifier, Advisor, Consultant, Regulator | | **ML Suggestions** | Tactic suggestions via ECHIDNA's Julia ML backend | | **Container Isolation**| podman rootless + bwrap fallback; fail-safe (refuses unsandboxed) | -| **Trust Bridge** | 5-level confidence, SHA-256 solver integrity, axiom tracking | +| **Trust Bridge** | 5-level confidence from ECHIDNA's own trust kernel, SHA-256 solver integrity, axiom tracking ([[ECHIDNA Integration]]) | | **GraphQL API** | Query and control programmatically | | **Self-Hosting** | Run your own instance; Containerfile + Guix supplied | From d124047b85be263c3707dbd487517f4d3b67ba74 Mon Sep 17 00:00:00 2001 From: "Jonathan D.A. Jewell" <6759885+hyperpolymath@users.noreply.github.com> Date: Mon, 5 Oct 2026 18:11:12 +0100 Subject: [PATCH 3/7] ci(workflow-linter): accept SPDX anywhere in the leading comment block gh actions-lock owns line 1 of each managed workflow, so the head -1 check failed all 29 workflows. Adopt the rsr-template-repo awk form. Co-Authored-By: Claude Opus 5.5 --- .github/workflows/workflow-linter.yml | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/.github/workflows/workflow-linter.yml b/.github/workflows/workflow-linter.yml index 80dab63..13d0b78 100644 --- a/.github/workflows/workflow-linter.yml +++ b/.github/workflows/workflow-linter.yml @@ -22,7 +22,10 @@ jobs: errors=0 for f in .github/workflows/*.yml .github/workflows/*.yaml; do [ -f "$f" ] || continue - if ! head -1 "$f" | grep -q "SPDX-License-Identifier"; then + # gh actions-lock owns line 1 of every workflow it manages, so + # accept the licence anywhere in the leading comment block (the + # rsr-template-repo form). + if ! awk '/^# SPDX-License-Identifier:/ { found=1 } /^[^#[:space:]]/ { exit } END { exit !found }' "$f"; then echo "ERROR: $f missing SPDX header" errors=$((errors + 1)) fi From c5416a470e12a404567358fa4db21815da5dead7 Mon Sep 17 00:00:00 2001 From: "Jonathan D.A. Jewell" <6759885+hyperpolymath@users.noreply.github.com> Date: Mon, 5 Oct 2026 18:16:00 +0100 Subject: [PATCH 4/7] =?UTF-8?q?fix(dispatcher):=20act=20on=20review=20?= =?UTF-8?q?=E2=80=94=20handshake=20classification,=20graphql=20skip,=20rep?= =?UTF-8?q?orted=20axiom=20names?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit - EchidnaIncompatible (fatal at start-up) vs unreachable/5xx (warn, retried); missing /api/health version is incompatible, not 'unreachable' - skip the REST handshake in graphql mode (start-up and per job) - map ECHIDNA-reported axiom names via AxiomFlag::from_name (sorryAx, believe_me, propext, ...) so a named hole caps the level at 1 - dedup flags by identity, not only adjacency - wiki/docs: content_id is available but not yet used Co-Authored-By: Claude Opus 5.5 --- docs/ECHIDNA-INTEGRATION.adoc | 16 +++- src/dispatcher/echidna_client.rs | 125 +++++++++++++++++++++++-------- src/error.rs | 5 ++ src/main.rs | 22 ++++-- src/trust/axiom_tracker.rs | 54 +++++++++++-- wiki/ECHIDNA-Integration.md | 6 +- 6 files changed, 180 insertions(+), 48 deletions(-) diff --git a/docs/ECHIDNA-INTEGRATION.adoc b/docs/ECHIDNA-INTEGRATION.adoc index 640b9a4..7eb293e 100644 --- a/docs/ECHIDNA-INTEGRATION.adoc +++ b/docs/ECHIDNA-INTEGRATION.adoc @@ -60,11 +60,15 @@ that the REST surface is up. It reads the server version from the `/api/health` if neither is present. It then enforces `MIN_ECHIDNA_VERSION` (`2.3.0`). -* At `serve` start-up, an ECHIDNA that is reachable but too old (or reports - a non-semver version) stops the process. An unreachable ECHIDNA only - logs a warning. +* At `serve` start-up, an ECHIDNA that answers but is incompatible stops + the process (`Error::EchidnaIncompatible`). Incompatible means one of: + too old, no version reported, a non-semver version, a 4xx on the + handshake paths, or a body that cannot be parsed. An unreachable ECHIDNA, + or one returning 5xx while it warms up, only logs a warning. * Every job runs `ensure_handshake` before it dispatches, unless local isolation is on. +* With `mode = "graphql"` there is no REST surface, so the handshake is + skipped. A GraphQL version query is a follow-up. Status: implemented and unit-tested (version gate, name resolution). It is wired into `serve` and `process_job`. No end-to-end test against a live @@ -99,6 +103,12 @@ shape. Any other body goes through the legacy path (`valid`, plus the typed === Receipt vs warrant (pattern from epistemic-types) +Axiom names that ECHIDNA reports are mapped with `AxiomFlag::from_name`. +Kernel names such as Lean's `sorryAx` and Idris's `believe_me` are +included. A hole that ECHIDNA names therefore caps the level at 1, even +when the local source looks clean (for example, a hole in an imported +module). + `ProofResult.trust_source` / `JobResult.trust_source` record where the trust data came from: diff --git a/src/dispatcher/echidna_client.rs b/src/dispatcher/echidna_client.rs index 391051f..f84d5cb 100644 --- a/src/dispatcher/echidna_client.rs +++ b/src/dispatcher/echidna_client.rs @@ -77,13 +77,10 @@ impl EchidnaClient { .send() .await .map_err(Error::Http)?; - if !response.status().is_success() { - return Err(Error::Echidna(format!( - "ECHIDNA /api/provers returned status {}", - response.status() - ))); - } - let provers: RestProversResponse = response.json().await.map_err(Error::Http)?; + check_handshake_status("/api/provers", response.status())?; + let provers: RestProversResponse = response.json().await.map_err(|e| { + Error::EchidnaIncompatible(format!("/api/provers body not understood: {e}")) + })?; let raw_version = match provers.version.clone().or(provers.echidna_version.clone()) { Some(v) => v, @@ -95,14 +92,15 @@ impl EchidnaClient { .send() .await .map_err(Error::Http)?; - if !health.status().is_success() { - return Err(Error::Echidna(format!( - "ECHIDNA /api/health returned status {}", - health.status() - ))); - } - let health: RestHealthResponse = health.json().await.map_err(Error::Http)?; - health.version + check_handshake_status("/api/health", health.status())?; + let health: RestHealthResponse = health.json().await.map_err(|e| { + Error::EchidnaIncompatible(format!("/api/health body not understood: {e}")) + })?; + health.version.ok_or_else(|| { + Error::EchidnaIncompatible(format!( + "ECHIDNA did not report a version; {MIN_ECHIDNA_VERSION} or newer is required" + )) + })? } }; @@ -117,6 +115,13 @@ impl EchidnaClient { Ok(handshake) } + /// Whether this client talks REST at all (and so can run the handshake). + /// + /// GraphQL-only deployments have no `/api/provers`; they skip it. + pub fn uses_rest(&self) -> bool { + !matches!(self.mode, EchidnaApiMode::Graphql) + } + /// Run [`EchidnaClient::handshake`] unless one has already succeeded. pub async fn ensure_handshake(&self) -> Result { let cached = self.handshake.read().ok().and_then(|slot| slot.clone()); @@ -607,14 +612,12 @@ fn rest_verify_result( let status = ProofStatus::from(result.status); let reported = AxiomReport::from_reported( prover.clone(), - result - .trust - .axioms - .iter() - .map(|a| AxiomFlag::Other(a.clone())), + result.trust.axioms.iter().map(|a| AxiomFlag::from_name(a)), ); - // ECHIDNA's list is the receipt; the canonical source scan still runs - // so a hole ECHIDNA did not name cannot raise the level. + // ECHIDNA's list is the receipt and counts at full severity (a named + // `sorry` caps the level even if the source looks clean, e.g. a hole + // in an imported module). The source scan is merged in as well, so a + // hole ECHIDNA did not name still counts. let axioms = reported.merge(AxiomTracker::scan_source(prover, content)); let confidence = assess_confidence_with_axioms(prover, status, false, 1, axioms.worst_danger); @@ -671,19 +674,41 @@ fn parse_rest_outcome(outcome: &str, valid: bool) -> ProofStatus { #[derive(Deserialize)] struct RestHealthResponse { - version: String, + /// Absent on servers older than 2.3.0. + #[serde(default)] + version: Option, +} + +/// Classify a non-success handshake status. +/// +/// 5xx means the server is up but not ready (transient: the message says +/// "unavailable", which [`crate::scheduler::retry::is_transient_error`] +/// retries). Any other non-success status means this is not an ECHIDNA +/// echidnabot can use. +fn check_handshake_status(path: &str, status: reqwest::StatusCode) -> Result<()> { + if status.is_success() { + Ok(()) + } else if status.is_server_error() { + Err(Error::Echidna(format!( + "ECHIDNA {path} unavailable (status {status})" + ))) + } else { + Err(Error::EchidnaIncompatible(format!( + "ECHIDNA {path} returned status {status}" + ))) + } } /// Parse a reported ECHIDNA version and enforce [`MIN_ECHIDNA_VERSION`]. pub fn check_min_version(raw: &str) -> Result { let trimmed = raw.trim().trim_start_matches('v'); let version = semver::Version::parse(trimmed).map_err(|e| { - Error::Echidna(format!("ECHIDNA reported unparseable version {raw:?}: {e}")) + Error::EchidnaIncompatible(format!("ECHIDNA reported unparseable version {raw:?}: {e}")) })?; let minimum = semver::Version::parse(MIN_ECHIDNA_VERSION) .map_err(|e| Error::Internal(format!("MIN_ECHIDNA_VERSION is not semver: {e}")))?; if version < minimum { - return Err(Error::Echidna(format!( + return Err(Error::EchidnaIncompatible(format!( "ECHIDNA {version} is older than the minimum supported {minimum}" ))); } @@ -912,11 +937,51 @@ mod tests { assert_eq!(r.status, ProofStatus::Verified); assert_eq!(r.trust_source, TrustSource::Echidna); assert_eq!(r.duration_ms, 7); - assert!(r - .axioms - .unwrap() - .flags - .contains(&AxiomFlag::Other("propext".to_string()))); + assert!(r.axioms.unwrap().flags.contains(&AxiomFlag::ClassicalAxiom)); + } + + #[test] + fn test_reported_sorry_caps_level_even_with_clean_source() { + let body = serde_json::json!({ + "schema": "echidna.prove.result/1", + "status": "verified", + "prover": "Lean", + "goal": "t", + "duration_ms": 1, + "message": "ok", + "trust": {"confidence": null, "axioms": ["sorryAx"]}, + "echidna_version": "2.4.0" + }); + let r = rest_verify_result( + &ProverKind::new("lean"), + "theorem t : True := trivial", + body, + ) + .unwrap(); + assert!(r.axioms.as_ref().unwrap().has_unsound()); + assert_eq!( + r.confidence.unwrap().level, + crate::trust::confidence::ConfidenceLevel::Level1 + ); + } + + #[test] + fn test_handshake_status_classification() { + use reqwest::StatusCode; + assert!(check_handshake_status("/api/provers", StatusCode::OK).is_ok()); + let warmup = check_handshake_status("/api/provers", StatusCode::SERVICE_UNAVAILABLE); + assert!(matches!(warmup, Err(Error::Echidna(_)))); + assert!(crate::scheduler::retry::is_transient_error( + &warmup.unwrap_err() + )); + assert!(matches!( + check_handshake_status("/api/provers", StatusCode::NOT_FOUND), + Err(Error::EchidnaIncompatible(_)) + )); + assert!(matches!( + check_min_version("2.2.0"), + Err(Error::EchidnaIncompatible(_)) + )); } #[test] diff --git a/src/error.rs b/src/error.rs index 018285b..c94a5d5 100644 --- a/src/error.rs +++ b/src/error.rs @@ -41,6 +41,11 @@ pub enum Error { #[error("ECHIDNA communication error: {0}")] Echidna(String), + /// The ECHIDNA server answered but is not one echidnabot can talk to + /// (too old, no version, or an unexpected REST shape). Never transient. + #[error("ECHIDNA server incompatible: {0}")] + EchidnaIncompatible(String), + #[error("Webhook verification failed: {0}")] WebhookVerification(String), diff --git a/src/main.rs b/src/main.rs index d5d1f9b..bf97d15 100644 --- a/src/main.rs +++ b/src/main.rs @@ -1182,11 +1182,17 @@ async fn record_feedback( /// Minimum-version handshake at start-up. /// -/// An ECHIDNA that answers but is too old (or reports a non-semver version) -/// stops start-up: every result it produced would be read with the wrong -/// contract. An ECHIDNA that is not reachable yet only warns; each job runs -/// the handshake again before it dispatches (see `process_job`). +/// An ECHIDNA that answers but is incompatible (too old, no or non-semver +/// version, or an unexpected REST shape) stops start-up: every result it +/// produced would be read with the wrong contract. An ECHIDNA that is not +/// reachable yet, or answers 5xx while warming up, only warns; each job runs +/// the handshake again before it dispatches (see `process_job`). GraphQL-only +/// deployments skip the REST handshake. async fn startup_handshake(echidna: &EchidnaClient) -> Result<()> { + if !echidna.uses_rest() { + tracing::info!("ECHIDNA mode is graphql: REST version handshake skipped"); + return Ok(()); + } match echidna.handshake().await { Ok(h) => { tracing::info!( @@ -1197,9 +1203,9 @@ async fn startup_handshake(echidna: &EchidnaClient) -> Result<()> { ); Ok(()) } - Err(echidnabot::Error::Echidna(msg)) => Err(echidnabot::Error::Echidna(format!( - "ECHIDNA handshake failed: {msg}" - ))), + Err(echidnabot::Error::EchidnaIncompatible(msg)) => Err( + echidnabot::Error::EchidnaIncompatible(format!("ECHIDNA handshake failed: {msg}")), + ), Err(other) => { tracing::warn!( "ECHIDNA not reachable at start-up ({other}); jobs will retry the handshake" @@ -1224,7 +1230,7 @@ async fn process_job( "ECHIDNA core reported unhealthy status".to_string(), )); } - if !config.executor.local_isolation { + if !config.executor.local_isolation && echidna.uses_rest() { echidna.ensure_handshake().await?; } diff --git a/src/trust/axiom_tracker.rs b/src/trust/axiom_tracker.rs index e81b90d..74d921e 100644 --- a/src/trust/axiom_tracker.rs +++ b/src/trust/axiom_tracker.rs @@ -108,14 +108,26 @@ impl AxiomFlag { /// Map one ECHIDNA source-scan finding onto the local flag vocabulary. fn from_usage(usage: &AxiomUsage) -> Self { - match usage.construct.trim() { - "sorry" => Self::Sorry, - "Admitted" | "admit" => Self::Admitted, + Self::from_name(&usage.construct) + } + + /// Map an axiom / construct name onto the local flag vocabulary. + /// + /// Used for both ECHIDNA source-scan findings and the names ECHIDNA + /// reports in `echidna.prove.result/1` `trust.axioms` (which may use the + /// kernel names, e.g. Lean's `sorryAx` from `#print axioms`). + pub fn from_name(name: &str) -> Self { + match name.trim() { + "sorry" | "sorryAx" => Self::Sorry, + "Admitted" | "admit" | "admitted" => Self::Admitted, "postulate" | "{!!}" => Self::Postulate, - "--type-in-type" | "OPTIONS --type-in-type" => Self::TypeInType, + "believe_me" | "assert_total" | "idris_crash" => Self::Postulate, + "--type-in-type" | "OPTIONS --type-in-type" | "type-in-type" => Self::TypeInType, "oops" => Self::Oops, "axiom" | "Axiom" => Self::UserAxiom, "assume" => Self::UndischargedAssumption, + "Classical.choice" | "choice" => Self::AxiomOfChoice, + "Classical.em" | "propext" | "Quot.sound" | "excluded_middle" => Self::ClassicalAxiom, other => Self::Other(other.to_string()), } } @@ -183,7 +195,13 @@ impl AxiomReport { /// Build a report from raw flags, deduplicating and counting them. fn from_flags(prover: ProverKind, mut flags: Vec) -> AxiomReport { - flags.sort_by_key(|f| std::cmp::Reverse(f.severity())); + // Sort by severity, then by identity, so equal flags are adjacent and + // `dedup` removes every duplicate (not only neighbouring ones). + flags.sort_by(|a, b| { + b.severity() + .cmp(&a.severity()) + .then_with(|| a.description().cmp(&b.description())) + }); flags.dedup(); let unsound_count = flags.iter().filter(|f| f.severity() >= 3).count(); let warning_count = flags.iter().filter(|f| f.severity() == 2).count(); @@ -534,6 +552,32 @@ mod tests { assert_eq!(report.worst_danger, DangerLevel::Reject); } + #[test] + fn test_from_flags_dedups_non_adjacent_duplicates() { + let report = AxiomReport::from_reported( + ProverKind::new("lean"), + [ + AxiomFlag::Sorry, + AxiomFlag::Admitted, + AxiomFlag::Sorry, + AxiomFlag::Other("x".into()), + AxiomFlag::AxiomOfChoice, + AxiomFlag::Other("x".into()), + ], + ); + assert_eq!(report.flags.len(), 4, "{:?}", report.flags); + } + + #[test] + fn test_from_name_maps_kernel_names() { + assert_eq!(AxiomFlag::from_name("sorryAx"), AxiomFlag::Sorry); + assert_eq!( + AxiomFlag::from_name("believe_me").danger_level(), + DangerLevel::Warning + ); + assert_eq!(AxiomFlag::from_name("propext"), AxiomFlag::ClassicalAxiom); + } + #[test] fn test_merge_keeps_worst_danger() { let output = AxiomTracker::scan(&ProverKind::new("lean"), "All goals discharged"); diff --git a/wiki/ECHIDNA-Integration.md b/wiki/ECHIDNA-Integration.md index 6eea287..ef9a830 100644 --- a/wiki/ECHIDNA-Integration.md +++ b/wiki/ECHIDNA-Integration.md @@ -6,13 +6,15 @@ echidnabot orchestrates; [ECHIDNA](https://github.com/hyperpolymath/echidna) pro ## Connecting - Default endpoints: `http://127.0.0.1:8081` (REST) and `http://127.0.0.1:8081/graphql`, the address `echidna server` listens on. -- **Version handshake:** on start-up echidnabot reads `GET /api/provers` (and `/api/health` if needed) and refuses to run against an ECHIDNA older than **2.3.0**. An unreachable ECHIDNA only logs a warning; every job retries the handshake before dispatching. +- **Version handshake:** on start-up echidnabot reads `GET /api/provers` (and `/api/health` if needed). It refuses to run against an ECHIDNA older than **2.3.0**, or one that reports no version. An unreachable or warming-up (5xx) ECHIDNA only logs a warning, and every job retries the handshake before dispatching. GraphQL-only mode skips this REST check. - Prover names are taken from ECHIDNA's own `/api/provers` list, so new ECHIDNA backends need no echidnabot change. ## Trust levels The 5-level confidence shown in check runs and PR comments is computed by **ECHIDNA's trust kernel** (linked as a library), not by an echidnabot copy. Axioms and holes (`sorry`, `Admitted`, `postulate`, `believe_me`, ...) are found by ECHIDNA's source scanner, plus a scan of the prover's output text. +An axiom that ECHIDNA names (for example `sorryAx`) counts at full severity, even if echidnabot's own scan of the source finds nothing. + echidnabot never verifies proof certificates itself, so a certificate artefact on its own does not raise a single result above Level 2. Each result says where its trust data came from: @@ -34,4 +36,4 @@ When ECHIDNA answers in the shared contract shape, echidnabot reads it directly: ## Identifiers -echidnabot mints UUIDv7 ids for jobs and records. For content (proof goals, prove results) it uses UUIDv8 content ids: SHA-256 over the RFC 8785 canonical JSON, the same construction ECHIDNA and proof-burrower use. +echidnabot mints UUIDv7 ids for jobs and records. A UUIDv8 content-id helper (SHA-256 over RFC 8785 canonical JSON, the same construction ECHIDNA and proof-burrower use) is available in `src/ids.rs`. Nothing uses it yet for proof goals or results. From 715632be9d7a1717df56830dc7e1a97bb53c076c Mon Sep 17 00:00:00 2001 From: "Jonathan D.A. Jewell" <6759885+hyperpolymath@users.noreply.github.com> Date: Mon, 5 Oct 2026 20:17:08 +0100 Subject: [PATCH 5/7] fix(config): GraphQL default endpoint is echidna-graphql's `/`; add live echidna trace tests `echidna server` serves REST only. GraphQL is the separate `echidna-graphql` binary, which serves at `/` (not `/graphql`) and is hard-coded to 127.0.0.1:8081. The old default `/graphql` returned 404, so auto mode against echidna-graphql failed both legs. Traced live against echidna a71aa2c: the old default fails (planted control), the new one verifies a true Z3 goal and rejects a false one against either binary. tests/live_echidna.rs drives the real client against a running echidna (skipped unless ECHIDNABOT_LIVE_ECHIDNA_URL / _GRAPHQL_URL / _DEFAULTS are set): handshake, REST Z3 and Coq true/false goals, Admitted flagged by the axiom scan, GraphQL Z3 true/false, default config. Co-Authored-By: Claude Opus 5.5 --- config/echidnabot.ncl | 2 +- docs/ECHIDNA-INTEGRATION.adoc | 18 +++- echidnabot.example.toml | 2 +- echidnabot.toml | 2 +- src/config.rs | 6 +- tests/live_echidna.rs | 165 ++++++++++++++++++++++++++++++++++ wiki/ECHIDNA-Integration.md | 2 +- wiki/Getting-Started.md | 6 +- 8 files changed, 191 insertions(+), 12 deletions(-) create mode 100644 tests/live_echidna.rs diff --git a/config/echidnabot.ncl b/config/echidnabot.ncl index 6de5ba9..f95fb17 100644 --- a/config/echidnabot.ncl +++ b/config/echidnabot.ncl @@ -91,7 +91,7 @@ let Config = { max_connections = 5, }, echidna = { - endpoint = "http://127.0.0.1:8081/graphql", + endpoint = "http://127.0.0.1:8081/", rest_endpoint = "http://127.0.0.1:8081", mode = 'auto, timeout_seconds = 120, diff --git a/docs/ECHIDNA-INTEGRATION.adoc b/docs/ECHIDNA-INTEGRATION.adoc index 7eb293e..cea8ecd 100644 --- a/docs/ECHIDNA-INTEGRATION.adoc +++ b/docs/ECHIDNA-INTEGRATION.adoc @@ -76,10 +76,20 @@ ECHIDNA was run. == Default endpoint -`echidna server` listens on `127.0.0.1:8081`. The defaults are now -`http://127.0.0.1:8081` (REST) and `http://127.0.0.1:8081/graphql`, in -`src/config.rs`, `echidnabot.toml`, `echidnabot.example.toml` and -`config/echidnabot.ncl`. +`echidna server` listens on `127.0.0.1:8081` and serves REST only. GraphQL +is the separate `echidna-graphql` binary, which serves at `/` and is also +hard-coded to `127.0.0.1:8081`, so only one of the two can run on a host at +a time. The defaults are `http://127.0.0.1:8081` (REST) and +`http://127.0.0.1:8081/` (GraphQL), in `src/config.rs`, `echidnabot.toml`, +`echidnabot.example.toml` and `config/echidnabot.ncl`. In `auto` mode +echidnabot tries GraphQL first and falls back to REST, so either binary +works with the defaults. + +Traced live on 2026-10-05 against echidna `a71aa2c` (z3 and coqc on +PATH): REST through `echidna server`, and GraphQL through +`echidna-graphql`, each with a planted false goal that must not verify. +Before this change the GraphQL default was `/graphql`, which returns 404 +from `echidna-graphql`. See `tests/live_echidna.rs`. == `echidna.prove.result/1` diff --git a/echidnabot.example.toml b/echidnabot.example.toml index dbea1d6..77dbfcc 100644 --- a/echidnabot.example.toml +++ b/echidnabot.example.toml @@ -17,7 +17,7 @@ max_connections = 5 [echidna] # ECHIDNA Core GraphQL endpoint -endpoint = "http://127.0.0.1:8081/graphql" +endpoint = "http://127.0.0.1:8081/" # ECHIDNA Core REST endpoint rest_endpoint = "http://127.0.0.1:8081" # API mode: auto, graphql, rest diff --git a/echidnabot.toml b/echidnabot.toml index 1c830f6..369f616 100644 --- a/echidnabot.toml +++ b/echidnabot.toml @@ -17,7 +17,7 @@ max_connections = 5 [echidna] # ECHIDNA Core GraphQL endpoint -endpoint = "http://127.0.0.1:8081/graphql" +endpoint = "http://127.0.0.1:8081/" # ECHIDNA Core REST endpoint rest_endpoint = "http://127.0.0.1:8081" # API mode: auto, graphql, rest diff --git a/src/config.rs b/src/config.rs index 4626dbf..a2af5a2 100644 --- a/src/config.rs +++ b/src/config.rs @@ -374,9 +374,11 @@ impl Default for EchidnaConfig { } } -/// Default ECHIDNA GraphQL endpoint: `echidna server` listens on 127.0.0.1:8081. +/// Default ECHIDNA GraphQL endpoint: the separate `echidna-graphql` binary, +/// which serves GraphQL at `/` on 127.0.0.1:8081 (`echidna server` has no +/// GraphQL route; in `auto` mode the REST fallback reaches it instead). fn default_echidna_endpoint() -> String { - "http://127.0.0.1:8081/graphql".to_string() + "http://127.0.0.1:8081/".to_string() } /// Default ECHIDNA REST base URL (same `echidna server`, port 8081). diff --git a/tests/live_echidna.rs b/tests/live_echidna.rs new file mode 100644 index 0000000..70790a9 --- /dev/null +++ b/tests/live_echidna.rs @@ -0,0 +1,165 @@ +// SPDX-License-Identifier: MPL-2.0 +//! Live trace: echidnabot's ECHIDNA client against a real `echidna server`. +//! +//! Skipped unless `ECHIDNABOT_LIVE_ECHIDNA_URL` names a running server +//! (e.g. `http://127.0.0.1:8081`, the `echidna server` default). Each check +//! pairs a positive case with a planted negative control, so a client that +//! always answered "verified" would fail here. +//! +//! Run: `ECHIDNABOT_LIVE_ECHIDNA_URL=http://127.0.0.1:8081 cargo test --test live_echidna` + +use echidna_core_spark::axiom_tracker::DangerLevel; +use echidnabot::config::{EchidnaApiMode, EchidnaConfig}; +use echidnabot::dispatcher::echidna_client::{EchidnaClient, MIN_ECHIDNA_VERSION}; +use echidnabot::dispatcher::{ProofStatus, ProverKind}; + +/// Client for the live server named by the environment, or `None` to skip. +fn live_client() -> Option { + let url = std::env::var("ECHIDNABOT_LIVE_ECHIDNA_URL").ok()?; + let config = EchidnaConfig { + endpoint: format!("{url}/"), + rest_endpoint: url, + mode: EchidnaApiMode::Rest, + timeout_secs: 120, + }; + Some(EchidnaClient::new(&config)) +} + +/// Whether `bin` resolves on `PATH`. +fn on_path(bin: &str) -> bool { + std::env::var_os("PATH") + .map(|p| std::env::split_paths(&p).any(|d| d.join(bin).is_file())) + .unwrap_or(false) +} + +/// The REST handshake reads a version >= the minimum and ECHIDNA's prover names. +#[tokio::test] +async fn live_handshake_reads_version_and_prover_list() { + let Some(client) = live_client() else { + eprintln!("skipped: ECHIDNABOT_LIVE_ECHIDNA_URL not set"); + return; + }; + let hs = client + .handshake() + .await + .expect("handshake against live echidna"); + let min = semver::Version::parse(MIN_ECHIDNA_VERSION).unwrap(); + assert!(hs.version >= min, "version {} below {}", hs.version, min); + assert!( + hs.provers.iter().any(|p| p == "Z3"), + "Z3 missing: {:?}", + hs.provers + ); + // Name resolution must use the server's spelling, not the slug. + assert_eq!(client.echidna_name(&ProverKind::new("z3")), "Z3"); + assert_eq!(client.echidna_name(&ProverKind::new("cvc5")), "CVC5"); +} + +/// REST verify: a true Z3 obligation verifies; a planted false one fails. +#[tokio::test] +async fn live_verify_z3_true_goal_and_planted_false_goal() { + let Some(client) = live_client() else { + eprintln!("skipped: ECHIDNABOT_LIVE_ECHIDNA_URL not set"); + return; + }; + if !on_path("z3") { + eprintln!("skipped: z3 not on PATH"); + return; + } + client.ensure_handshake().await.expect("handshake"); + let z3 = ProverKind::new("z3"); + + // Negated obligation x+0=x is unsat -> discharged. + let good = "(declare-const x Int)\n(assert (not (= (+ x 0) x)))\n(check-sat)\n"; + let r = client.verify_proof(&z3, good).await.expect("verify good"); + assert_eq!(r.status, ProofStatus::Verified, "{r:?}"); + + // Planted control: negated x+1=x is sat -> must NOT verify. + let bad = "(declare-const x Int)\n(assert (not (= (+ x 1) x)))\n(check-sat)\n"; + let r = client.verify_proof(&z3, bad).await.expect("verify bad"); + assert_eq!(r.status, ProofStatus::Failed, "{r:?}"); +} + +/// REST verify: a true Coq proof verifies, a false one does not, and an +/// `Admitted` proof is flagged by the axiom scan. +#[tokio::test] +async fn live_verify_coq_true_goal_and_planted_false_goal() { + let Some(client) = live_client() else { + eprintln!("skipped: ECHIDNABOT_LIVE_ECHIDNA_URL not set"); + return; + }; + if !on_path("coqc") { + eprintln!("skipped: coqc not on PATH"); + return; + } + client.ensure_handshake().await.expect("handshake"); + let coq = ProverKind::new("coq"); + + let good = "Theorem t : True. Proof. exact I. Qed."; + let r = client.verify_proof(&coq, good).await.expect("verify good"); + assert_eq!(r.status, ProofStatus::Verified, "{r:?}"); + + let bad = "Theorem t : 1 = 2. Proof. reflexivity. Qed."; + let r = client.verify_proof(&coq, bad).await.expect("verify bad"); + assert_ne!(r.status, ProofStatus::Verified, "{r:?}"); + + // `Admitted` is reported PROVED by echidna's /api/verify (upstream gap); + // echidnabot's source scan must still flag it so trust is capped. + let admitted = "Lemma l : False. Admitted."; + let r = client + .verify_proof(&coq, admitted) + .await + .expect("verify admitted"); + let axioms = r.axioms.expect("axiom report"); + assert_ne!( + axioms.worst_danger, + DangerLevel::Safe, + "Admitted not flagged: {axioms:?}" + ); +} + +/// GraphQL verify against `echidna-graphql`: true goal verifies, false fails. +#[tokio::test] +async fn live_graphql_verify_z3_true_goal_and_planted_false_goal() { + // GraphQL is the separate `echidna-graphql` binary (serves at `/`). + let Ok(url) = std::env::var("ECHIDNABOT_LIVE_ECHIDNA_GRAPHQL_URL") else { + eprintln!("skipped: ECHIDNABOT_LIVE_ECHIDNA_GRAPHQL_URL not set"); + return; + }; + if !on_path("z3") { + eprintln!("skipped: z3 not on PATH"); + return; + } + let client = EchidnaClient::new(&EchidnaConfig { + endpoint: url, + rest_endpoint: "http://127.0.0.1:9".to_string(), + mode: EchidnaApiMode::Graphql, + timeout_secs: 120, + }); + let z3 = ProverKind::new("z3"); + let good = "(declare-const x Int)\n(assert (not (= (+ x 0) x)))\n(check-sat)\n"; + let r = client.verify_proof(&z3, good).await.expect("graphql good"); + assert_eq!(r.status, ProofStatus::Verified, "{r:?}"); + let bad = "(declare-const x Int)\n(assert (not (= (+ x 1) x)))\n(check-sat)\n"; + let r = client.verify_proof(&z3, bad).await.expect("graphql bad"); + assert_eq!(r.status, ProofStatus::Failed, "{r:?}"); +} + +/// The default config (auto mode) reaches whichever ECHIDNA binary is on 8081. +#[tokio::test] +async fn live_default_config_reaches_whichever_echidna_runs_on_8081() { + // Set ECHIDNABOT_LIVE_DEFAULTS=1 with either `echidna server` or + // `echidna-graphql` running on its default port. + if std::env::var("ECHIDNABOT_LIVE_DEFAULTS").is_err() || !on_path("z3") { + eprintln!("skipped: ECHIDNABOT_LIVE_DEFAULTS not set or z3 missing"); + return; + } + let client = EchidnaClient::new(&EchidnaConfig::default()); + let z3 = ProverKind::new("z3"); + let good = "(declare-const x Int)\n(assert (not (= (+ x 0) x)))\n(check-sat)\n"; + let r = client.verify_proof(&z3, good).await.expect("default good"); + assert_eq!(r.status, ProofStatus::Verified, "{r:?}"); + let bad = "(declare-const x Int)\n(assert (not (= (+ x 1) x)))\n(check-sat)\n"; + let r = client.verify_proof(&z3, bad).await.expect("default bad"); + assert_eq!(r.status, ProofStatus::Failed, "{r:?}"); +} diff --git a/wiki/ECHIDNA-Integration.md b/wiki/ECHIDNA-Integration.md index ef9a830..a714688 100644 --- a/wiki/ECHIDNA-Integration.md +++ b/wiki/ECHIDNA-Integration.md @@ -5,7 +5,7 @@ echidnabot orchestrates; [ECHIDNA](https://github.com/hyperpolymath/echidna) pro ## Connecting -- Default endpoints: `http://127.0.0.1:8081` (REST) and `http://127.0.0.1:8081/graphql`, the address `echidna server` listens on. +- Default endpoints: `http://127.0.0.1:8081` (REST, `echidna server`) and `http://127.0.0.1:8081/` (GraphQL, the separate `echidna-graphql` binary, which serves at `/`). Both ECHIDNA binaries default to port 8081, so run one or the other; `auto` mode tries GraphQL and falls back to REST. - **Version handshake:** on start-up echidnabot reads `GET /api/provers` (and `/api/health` if needed). It refuses to run against an ECHIDNA older than **2.3.0**, or one that reports no version. An unreachable or warming-up (5xx) ECHIDNA only logs a warning, and every job retries the handshake before dispatching. GraphQL-only mode skips this REST check. - Prover names are taken from ECHIDNA's own `/api/provers` list, so new ECHIDNA backends need no echidnabot change. diff --git a/wiki/Getting-Started.md b/wiki/Getting-Started.md index 7c1ca3c..5311114 100644 --- a/wiki/Getting-Started.md +++ b/wiki/Getting-Started.md @@ -60,9 +60,11 @@ name = "your-repo" enabled = ["coq", "lean4"] [echidna] -# Default: a local `echidna server` on port 8081 (REST + GraphQL). +# Default: a local `echidna server` (REST) on port 8081. GraphQL is the +# separate `echidna-graphql` binary, served at `/` on the same port 8081; +# run one or the other. `mode = "auto"` tries GraphQL, then falls back to REST. # echidnabot checks the server is ECHIDNA >= 2.3.0 at start-up. -endpoint = "http://127.0.0.1:8081/graphql" +endpoint = "http://127.0.0.1:8081/" rest_endpoint = "http://127.0.0.1:8081" ``` From 9d56550ed3cb7c55ebd49b30c9885c70b9d70586 Mon Sep 17 00:00:00 2001 From: "Jonathan D.A. Jewell" <6759885+hyperpolymath@users.noreply.github.com> Date: Mon, 5 Oct 2026 20:51:13 +0100 Subject: [PATCH 6/7] fix(ci): stop SPDX header scan at indented workflow content Co-Authored-By: Claude Opus 5.5 --- .github/workflows/workflow-linter.yml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/.github/workflows/workflow-linter.yml b/.github/workflows/workflow-linter.yml index 13d0b78..307d73e 100644 --- a/.github/workflows/workflow-linter.yml +++ b/.github/workflows/workflow-linter.yml @@ -25,7 +25,7 @@ jobs: # gh actions-lock owns line 1 of every workflow it manages, so # accept the licence anywhere in the leading comment block (the # rsr-template-repo form). - if ! awk '/^# SPDX-License-Identifier:/ { found=1 } /^[^#[:space:]]/ { exit } END { exit !found }' "$f"; then + if ! awk '/^# SPDX-License-Identifier:/ { found=1 } /^[[:space:]]*[^#[:space:]]/ { exit } END { exit !found }' "$f"; then echo "ERROR: $f missing SPDX header" errors=$((errors + 1)) fi From 7f9552c8e24fd5fe04e0ed746427c85111463d8a Mon Sep 17 00:00:00 2001 From: "coderabbitai[bot]" <136622811+coderabbitai[bot]@users.noreply.github.com> Date: Mon, 5 Oct 2026 20:20:49 +0000 Subject: [PATCH 7/7] docs(rust): clarify proof processing, ECHIDNA client errors, and trust assessment behavior --- src/config.rs | 1 + src/dispatcher/echidna_client.rs | 72 ++++++++++++++++++++++++++------ src/dispatcher/prove_result.rs | 11 +++++ src/ids.rs | 3 +- src/main.rs | 50 +++++++++++++++------- src/trust/axiom_tracker.rs | 7 +++- src/trust/confidence.rs | 6 +++ 7 files changed, 120 insertions(+), 30 deletions(-) diff --git a/src/config.rs b/src/config.rs index a2af5a2..b062bc0 100644 --- a/src/config.rs +++ b/src/config.rs @@ -505,6 +505,7 @@ impl Config { } /// Render a secret-bearing field for `Debug` without its value. +/// Returns `""` for `Some` and `""` for `None`. /// /// Pattern from the types fit map (secret-types is not yet a usable /// library): tokens and webhook secrets never reach logs through `{:?}`. diff --git a/src/dispatcher/echidna_client.rs b/src/dispatcher/echidna_client.rs index f84d5cb..cf4a288 100644 --- a/src/dispatcher/echidna_client.rs +++ b/src/dispatcher/echidna_client.rs @@ -46,6 +46,9 @@ pub struct EchidnaClient { impl EchidnaClient { /// Create a new ECHIDNA client + /// + /// # Panics + /// Panics if the HTTP client cannot be initialised. pub fn new(config: &EchidnaConfig) -> Self { let client = Client::builder() .timeout(Duration::from_secs(config.timeout_secs)) @@ -66,9 +69,14 @@ impl EchidnaClient { /// /// Lists `/api/provers` (which also proves the REST surface is there) and /// reads the version from that response if present, otherwise from - /// `/api/health`. Fails with [`Error::Echidna`] if the server is older - /// than [`MIN_ECHIDNA_VERSION`] or reports an unparseable version. On - /// success the prover list is remembered for slug → name resolution. + /// `/api/health`. Returns the version and prover names, caching them for + /// slug resolution unless the cache lock is poisoned. + /// + /// # Errors + /// Returns [`Error::Http`] for request failures, [`Error::Echidna`] for + /// 5xx responses, and [`Error::EchidnaIncompatible`] for other unsuccessful + /// statuses, unreadable response bodies, or a missing, unparseable or + /// older-than-[`MIN_ECHIDNA_VERSION`] version. pub async fn handshake(&self) -> Result { let response = self .client @@ -123,6 +131,9 @@ impl EchidnaClient { } /// Run [`EchidnaClient::handshake`] unless one has already succeeded. + /// + /// Returns the cached result without rechecking the server. If the cache + /// is empty or unreadable, performs the handshake and propagates its errors. pub async fn ensure_handshake(&self) -> Result { let cached = self.handshake.read().ok().and_then(|slot| slot.clone()); match cached { @@ -134,8 +145,8 @@ impl EchidnaClient { /// ECHIDNA's identifier for an echidnabot prover slug. /// /// Uses the list learned by [`EchidnaClient::handshake`] when one is - /// available (case-, `-`- and `_`-insensitive match), and otherwise the - /// static mapping for the classic provers. + /// available, ignoring case, `-`, `_`, spaces and `/`. With no match, + /// uses the classic prover mapping or the prover's display name. pub fn echidna_name(&self, prover: &ProverKind) -> String { let known = self .handshake @@ -248,6 +259,12 @@ impl EchidnaClient { format!("{}{}", base, path) } + /// Submit proof source through GraphQL and derive confidence locally from + /// its source, prover output and certificate artefact names. + /// + /// Returns [`Error::Http`] for request or response-decoding failures and + /// [`Error::Echidna`] for unsuccessful HTTP statuses, GraphQL errors or + /// missing response data. async fn verify_proof_graphql( &self, prover: &ProverKind, @@ -457,6 +474,11 @@ impl EchidnaClient { } } + /// Submit proof source to `/api/verify` using the resolved prover name. + /// + /// Returns [`Error::Http`] for request or JSON-decoding failures and + /// [`Error::Echidna`] for unsuccessful HTTP statuses. Result validation + /// errors from [`rest_verify_result`] are propagated. async fn verify_proof_rest(&self, prover: &ProverKind, content: &str) -> Result { let request = RestVerifyRequest { prover: self.echidna_name(prover), @@ -483,6 +505,12 @@ impl EchidnaClient { rest_verify_result(prover, content, body) } + /// Request up to five tactics for `goal_state`, or for `context` when the + /// goal state is blank. Each returned tactic receives confidence `0.5` + /// and a heuristic explanation. + /// + /// Returns [`Error::Http`] for request or response-decoding failures and + /// [`Error::Echidna`] for unsuccessful HTTP statuses. async fn suggest_tactics_rest( &self, prover: &ProverKind, @@ -543,6 +571,10 @@ impl EchidnaClient { } } + /// Check whether `/api/provers` lists a matching normalised prover name. + /// + /// An absent name yields `Unavailable`; unsuccessful HTTP statuses yield + /// `Unknown`. Request and response-decoding failures return [`Error::Http`]. async fn prover_status_rest(&self, prover: &ProverKind) -> Result { let response = self .client @@ -599,9 +631,17 @@ struct RestVerifyResponse { /// Build a [`ProofResult`] from a REST `/api/verify` body. /// -/// An `echidna.prove.result/1` body is read as that contract and its `trust` -/// object is transported ([`TrustSource::Echidna`]). Any other body is read -/// as the legacy shape and trust is derived locally from the proof source. +/// An `echidna.prove.result/1` body supplies status, message, duration in +/// milliseconds and reported axioms ([`TrustSource::Echidna`]). Its axioms +/// are merged with a scan of `content`; confidence is recalculated locally, +/// ignoring the reported confidence. Other bodies use the legacy shape, +/// source-only axiom scanning and a zero duration. Both return empty prover +/// output and artefact lists. +/// +/// # Errors +/// Propagates [`ProveResult::from_value`] validation errors for tagged bodies +/// without trying the legacy shape. Legacy deserialisation errors return +/// [`Error::Json`]. fn rest_verify_result( prover: &ProverKind, content: &str, @@ -661,6 +701,9 @@ fn rest_verify_result( } /// Map ECHIDNA's typed REST outcome onto [`ProofStatus`]. +/// +/// Matching ignores ASCII case. Unknown outcomes yield `Verified` when +/// `valid` is true and `Unknown` otherwise; recognised outcomes ignore `valid`. fn parse_rest_outcome(outcome: &str, valid: bool) -> ProofStatus { match outcome.to_ascii_uppercase().as_str() { "PROVED" => ProofStatus::Verified, @@ -679,12 +722,11 @@ struct RestHealthResponse { version: Option, } -/// Classify a non-success handshake status. +/// Accept successful handshake statuses and classify failures. /// -/// 5xx means the server is up but not ready (transient: the message says -/// "unavailable", which [`crate::scheduler::retry::is_transient_error`] -/// retries). Any other non-success status means this is not an ECHIDNA -/// echidnabot can use. +/// Returns [`Error::Echidna`] for 5xx responses, classified as transient by +/// [`crate::scheduler::retry::is_transient_error`]. Other unsuccessful statuses +/// return [`Error::EchidnaIncompatible`]. `path` identifies the failing endpoint. fn check_handshake_status(path: &str, status: reqwest::StatusCode) -> Result<()> { if status.is_success() { Ok(()) @@ -700,6 +742,10 @@ fn check_handshake_status(path: &str, status: reqwest::StatusCode) -> Result<()> } /// Parse a reported ECHIDNA version and enforce [`MIN_ECHIDNA_VERSION`]. +/// +/// Surrounding whitespace and leading lowercase `v` characters are ignored. +/// Returns [`Error::EchidnaIncompatible`] if parsing fails or the version is +/// below the minimum, using semantic-version ordering. pub fn check_min_version(raw: &str) -> Result { let trimmed = raw.trim().trim_start_matches('v'); let version = semver::Version::parse(trimmed).map_err(|e| { diff --git a/src/dispatcher/prove_result.rs b/src/dispatcher/prove_result.rs index 81e4714..2d25794 100644 --- a/src/dispatcher/prove_result.rs +++ b/src/dispatcher/prove_result.rs @@ -98,12 +98,23 @@ pub struct ProveResult { impl ProveResult { /// Parse and validate one `echidna.prove.result/1` object from text. + /// + /// Accepts surrounding whitespace and non-canonical key order. Invalid + /// JSON returns [`Error::Json`]; validation errors from [`Self::from_value`] + /// are propagated. pub fn parse(text: &str) -> Result { let value: serde_json::Value = serde_json::from_str(text.trim())?; Self::from_value(value) } /// Validate an already-parsed JSON value as `echidna.prove.result/1`. + /// + /// # Errors + /// Returns [`Error::Echidna`] for a missing or different schema tag, a + /// supplied duration outside the integer range `0..=2^53-1` milliseconds, + /// or non-finite confidence. Returns [`Error::Json`] for deserialisation + /// failures, including missing required fields, unknown top-level fields + /// and unknown statuses. Unknown fields within `trust` are ignored. pub fn from_value(value: serde_json::Value) -> Result { if !Self::is_prove_result(&value) { return Err(Error::Echidna(format!( diff --git a/src/ids.rs b/src/ids.rs index 32e8130..f8d506e 100644 --- a/src/ids.rs +++ b/src/ids.rs @@ -56,7 +56,8 @@ pub fn content_id(value: &serde_json::Value) -> Result /// Content id of a proof goal's text (a JSON string). /// -/// Infallible: a JSON string always canonicalises. +/// Hashes the exact text as a JSON string, without trimming or normalisation. +/// Returns the nil UUID if canonicalisation fails instead of propagating an error. pub fn goal_content_id(goal_text: &str) -> Uuid { content_id(&serde_json::Value::String(goal_text.to_string())).unwrap_or_else(|_| Uuid::nil()) } diff --git a/src/main.rs b/src/main.rs index bf97d15..34b90c7 100644 --- a/src/main.rs +++ b/src/main.rs @@ -238,6 +238,13 @@ type TracerFlushHook = Box< + 'static, >; +/// Initialise storage and the scheduler, then serve HTTP on `host:port`. +/// On shutdown, drain jobs within the configured timeout, close storage and +/// run `tracer_hook` if supplied. +/// +/// Propagates storage initialisation, incompatible ECHIDNA handshake and +/// listener-binding errors. HTTP serving errors trigger shutdown and are +/// consumed; other handshake failures allow start-up to continue. async fn serve( config: &Config, host: &str, @@ -718,6 +725,11 @@ async fn init_db(config: &Config) -> Result<()> { Ok(()) } +/// Process queued jobs sequentially, persist outcomes and report them to the +/// originating platform. Job errors become unsuccessful results; persistence, +/// feedback and reporting failures do not stop the loop. +/// +/// Checks `shutdown` while waiting for work, without interrupting an active job. async fn run_scheduler_loop( scheduler: Arc, store: Arc, @@ -798,17 +810,18 @@ async fn run_scheduler_loop( /// /// Cascade: /// 1. Look up the repository row to recover platform + bot mode. -/// 2. Resolve the effective mode via `modes::resolve_mode` (directive -/// content is None until the executor lands a clone-and-read step). +/// 2. Resolve the effective mode from the fetched repository directive, +/// repository settings and daemon default. /// 3. Build the platform-appropriate adapter. /// 4. Translate the `JobResult` into a `ProofResult` for the formatter, /// then format per-mode. -/// 5. Always create a check run; comment on the originating PR for +/// 5. Attempt a check run; comment on the originating PR for /// modes that opt in (Advisor / Consultant / Regulator). /// -/// All steps are best-effort. Errors are surfaced to the caller (which -/// logs but does not propagate them), so a 503 from GitHub or a missing -/// token never blocks the scheduler. +/// A missing repository is a no-op. Repository lookup and final adapter +/// construction errors reach the caller. Directive, suggestion, reranking, +/// coverage lookup and posting failures are handled locally. Failed inline +/// review comments fall back to general PR comments. async fn report_to_platform( store: Arc, echidna: &EchidnaClient, @@ -1182,12 +1195,10 @@ async fn record_feedback( /// Minimum-version handshake at start-up. /// -/// An ECHIDNA that answers but is incompatible (too old, no or non-semver -/// version, or an unexpected REST shape) stops start-up: every result it -/// produced would be read with the wrong contract. An ECHIDNA that is not -/// reachable yet, or answers 5xx while warming up, only warns; each job runs -/// the handshake again before it dispatches (see `process_job`). GraphQL-only -/// deployments skip the REST handshake. +/// Propagates `Error::EchidnaIncompatible` and converts all other handshake +/// errors to success, allowing start-up to continue. Delegated REST jobs +/// retry when no successful handshake is cached (see `process_job`). +/// GraphQL-only deployments skip the REST handshake. async fn startup_handshake(echidna: &EchidnaClient) -> Result<()> { if !echidna.uses_rest() { tracing::info!("ECHIDNA mode is graphql: REST version handshake skipped"); @@ -1215,8 +1226,19 @@ async fn startup_handshake(echidna: &EchidnaClient) -> Result<()> { } } -/// Run one proof job: check ECHIDNA (health + version handshake), find the -/// proof files, verify each one, and aggregate status, axioms and trust. +/// Run one proof job and aggregate file verdicts, axioms and confidence. +/// +/// Checks ECHIDNA health and prover availability even for local execution; +/// delegated REST jobs also ensure a cached version handshake. Clones the +/// requested revision, discovers proof files when none were supplied and +/// stores the discovered paths. Duration includes these steps, in milliseconds. +/// No proof files yields an unsuccessful result without trust data. +/// +/// Propagates database, checkout, file-reading and ECHIDNA errors, and returns +/// a configuration error if local isolation has no available backend. Local +/// execution errors become failed file verdicts. File-discovery task failures +/// become an empty file list. Confidence is computed locally; trust provenance +/// is `Echidna` only when every delegated result reports that provenance. async fn process_job( job: &ProofJob, store: &dyn Store, diff --git a/src/trust/axiom_tracker.rs b/src/trust/axiom_tracker.rs index 74d921e..92de012 100644 --- a/src/trust/axiom_tracker.rs +++ b/src/trust/axiom_tracker.rs @@ -96,8 +96,8 @@ impl AxiomFlag { /// The ECHIDNA danger level this flag corresponds to. /// /// `--type-in-type` can manufacture false theorems, so it is `Reject`; - /// the other unsound holes are `Warning` (ECHIDNA's level for `sorry`, - /// `Admitted` and `oops`); everything else is `Noted`. + /// `Sorry`, `Admitted`, `Oops` and `Postulate` are `Warning`; + /// everything else is `Noted`. pub fn danger_level(&self) -> DangerLevel { match self { Self::TypeInType => DangerLevel::Reject, @@ -116,6 +116,7 @@ impl AxiomFlag { /// Used for both ECHIDNA source-scan findings and the names ECHIDNA /// reports in `echidna.prove.result/1` `trust.axioms` (which may use the /// kernel names, e.g. Lean's `sorryAx` from `#print axioms`). + /// Surrounding whitespace is trimmed; unrecognised names become `Other`. pub fn from_name(name: &str) -> Self { match name.trim() { "sorry" | "sorryAx" => Self::Sorry, @@ -179,6 +180,8 @@ impl AxiomReport { /// Combine two reports on the same proof (for example a source scan and /// an output scan): the union of the flags and the worse danger level. + /// Retains this report's prover without checking that the other matches, + /// deduplicates flags and recalculates counts. pub fn merge(mut self, other: AxiomReport) -> AxiomReport { let worst = DangerLevel::max_danger(self.worst_danger, other.worst_danger); self.flags.extend(other.flags); diff --git a/src/trust/confidence.rs b/src/trust/confidence.rs index a96f681..5b350f0 100644 --- a/src/trust/confidence.rs +++ b/src/trust/confidence.rs @@ -145,6 +145,12 @@ pub fn assess_confidence( /// is always passed as `false`: a certificate artefact raises nothing above /// Level 2 on its own. Solver integrity is checked elsewhere /// ([`crate::trust::SolverIntegrity`]) and is assumed here. +/// +/// `checker_count` is the number of independent checkers that confirmed the +/// result; values above `u32::MAX` are capped for assessment but retained in +/// the report. `worst_axiom_danger` is the highest danger found in the proof. +/// A status other than `Verified` returns Level 1 with no certificate and +/// zero checkers, regardless of the supplied values. pub fn assess_confidence_with_axioms( prover: &ProverKind, status: ProofStatus,