diff --git a/.github/workflows/dogfood-gate.yml b/.github/workflows/dogfood-gate.yml index 0729c2be..29bd304e 100644 --- a/.github/workflows/dogfood-gate.yml +++ b/.github/workflows/dogfood-gate.yml @@ -57,6 +57,8 @@ jobs: run: | bash scripts/ci/test-manifest-validator-regressions.sh bash .github/hooks/validate-a2ml.sh + - name: Check prover integration inventory + run: bash scripts/check-verification-integrations.sh - name: Write summary run: | A2ML_COUNT="${{ steps.detect.outputs.count }}" diff --git a/.machine_readable/provers.a2ml b/.machine_readable/provers.a2ml index dc27c06f..18952ef7 100644 --- a/.machine_readable/provers.a2ml +++ b/.machine_readable/provers.a2ml @@ -3,23 +3,23 @@ # # provers.a2ml — Authoritative enumeration of ECHIDNA prover backends. # -# Generated from src/rust/provers/mod.rs::ProverKind. One section per +# Generated from crates/echidna-core/src/prover_kind.rs::ProverKind. One section per # variant, keyed by the variant's PascalCase name for stability against # slug-format drift. `slug` is the snake_case identifier used on the # wire (matches serde's rename_all = "snake_case" default). # -# Downstream consumers: -# - .github/workflows/backend-matrix.yml (vcl-ut) reads this file to -# build its matrix strategy, one job per prover. -# - Future sync check fails CI if this file drifts from ProverKind::all(). +# This is a declaration inventory, not a claim that each variant has a +# runnable backend or a successful proof. See verification-integrations.a2ml +# for the assessed roles of selected tools outside and within this enum. # -# SYNC SOURCE-OF-TRUTH: `pub enum ProverKind` in src/rust/provers/mod.rs. +# SYNC SOURCE-OF-TRUTH: `pub enum ProverKind` in +# crates/echidna-core/src/prover_kind.rs. # If that enum changes, regenerate with scripts/gen-provers-a2ml.sh. [metadata] version = "1.0.0" -source = "src/rust/provers/mod.rs::ProverKind" -date = "2026-09-25" +source = "crates/echidna-core/src/prover_kind.rs::ProverKind" +date = "2026-11-07" count = 141 [prover.ABC] diff --git a/.machine_readable/verification-integrations.a2ml b/.machine_readable/verification-integrations.a2ml new file mode 100644 index 00000000..c2bfb286 --- /dev/null +++ b/.machine_readable/verification-integrations.a2ml @@ -0,0 +1,79 @@ +# SPDX-License-Identifier: MPL-2.0 +# Selected verification-tool roles at the ECHIDNA boundary. +# This complements provers.a2ml: every enum variant not listed below defaults +# to declared_unverified. A source file or enum variant is not a successful run. +# This ledger records source integration, not proof validity or tool health. + +[metadata] +schema = "verification-integrations/1" +reviewed = "2026-11-07" +enum_source = "crates/echidna-core/src/prover_kind.rs" +enum_registry = ".machine_readable/provers.a2ml" +enum_default = "declared_unverified" + +# backend_declared: enum variant and backend source exist; runtime unverified. +# partial_non_backend: ECHIDNA has corpus/internal code, not a prover backend. +# via_parent: a language/family served by the named tool, not its own backend. +# not_integrated: a verifier with no ECHIDNA backend at this review. +# not_a_prover: language or compute substrate, not a prover integration. + +[tool.Idris2] +status = "backend_declared" +role = "dependent-type checker" +prover_kind = "Idris2" +local_paths = ["src/rust/provers/idris2.rs"] + +[tool.GNATprove] +status = "backend_declared" +role = "SPARK/Ada verifier" +prover_kind = "GNATprove" +local_paths = ["src/rust/provers/gnatprove.rs"] + +[tool.SPARK] +status = "via_parent" +role = "Ada verification language and toolchain" +parent_tool = "GNATprove" + +[tool.Creusot] +status = "partial_non_backend" +role = "Rust deductive verification" +local_paths = ["src/rust/corpus/creusot.rs", "crates/echidna-core-creusot/src/lib.rs"] +upstream = "https://github.com/creusot-rs/creusot" + +[tool.Pearlite] +status = "via_parent" +role = "Creusot specification language" +parent_tool = "Creusot" + +[tool.Verus] +status = "not_integrated" +role = "Rust verification" +upstream = "https://github.com/verus-lang/verus" + +[tool.Kani] +status = "not_integrated" +role = "Rust model checking" +upstream = "https://github.com/model-checking/kani" + +[tool.Aeneas] +status = "not_integrated" +role = "Rust-to-proof translation" +upstream = "https://github.com/AeneasVerif/aeneas" + +[tool.Atoma] +status = "not_integrated" +role = "estate Zig verification research prototype" +upstream = "https://github.com/hyperpolymath/atoma" + +[tool.Chapel] +status = "not_a_prover" +role = "parallel proof-search compute substrate" +local_paths = ["src/chapel/parallel_proof_search.chpl"] + +[tool.ATS2] +status = "not_a_prover" +role = "programming language and type system" + +[tool.Zig] +status = "not_a_prover" +role = "implementation and FFI language" diff --git a/docs/PROVER_COUNT.adoc b/docs/PROVER_COUNT.adoc index 8f6a2f80..5fbd0cb8 100644 --- a/docs/PROVER_COUNT.adoc +++ b/docs/PROVER_COUNT.adoc @@ -18,10 +18,16 @@ ____ === TL;DR +Counts describe declarations and source files, not successful tool runs. +The machine-readable link:../.machine_readable/verification-integrations.a2ml[verification integration ledger] +distinguishes selected backend, corpus, internal-proof, and non-prover roles. +Run `bash scripts/check-verification-integrations.sh` to check its source +references and the full 141-variant declaration inventory. + [width="100%",cols="34%,33%,33%",options="header",] |=== |Question |Answer |Command -|Total `+ProverKind+` variants in `+src/rust/provers/mod.rs+` |*141* +|Total `+ProverKind+` variants in `+crates/echidna-core/src/prover_kind.rs+` |*141* |`+V+` below |Backend implementation files in `+src/rust/provers/+` |*105* |`+F+` @@ -309,7 +315,7 @@ root. [source,bash] ---- # V — total ProverKind variants (141) -awk '/pub enum ProverKind/{f=1;next} f&&/^\}/{exit} f' src/rust/provers/mod.rs \ +awk '/pub enum ProverKind/{f=1;next} f&&/^\}/{exit} f' crates/echidna-core/src/prover_kind.rs \ | grep -cE '^\s*[A-Z][A-Za-z0-9_]*\s*,' # F — backend implementation files (105) @@ -319,15 +325,15 @@ ls src/rust/provers/*.rs | grep -cv 'mod\.rs$' git grep -l 'fn suggest_tactics' -- 'src/rust/provers/*.rs' | wc -l # C — Tier-1 core, exposed by default at GET /api/provers (12) -awk '/fn all_core/{f=1} f&&/\]/{print;exit} f' src/rust/provers/mod.rs \ +awk '/fn all_core/{f=1} f&&/\]/{print;exit} f' crates/echidna-core/src/prover_kind.rs \ | grep -oE 'ProverKind::[A-Za-z0-9_]+' | wc -l # D — variants carrying a type-checker / discipline role (46) -awk '/pub enum ProverKind/{f=1;next} f&&/^\}/{exit} f' src/rust/provers/mod.rs \ +awk '/pub enum ProverKind/{f=1;next} f&&/^\}/{exit} f' crates/echidna-core/src/prover_kind.rs \ | grep -icE 'typecheck|discipline' ---- -`+ProverKind::all()+` in `+src/rust/provers/mod.rs+` is the machine +`+ProverKind::all()+` in `+crates/echidna-core/src/prover_kind.rs+` is the machine source of truth; this document is its human-readable mirror. If a count changes, update this file *and* `+.machine_readable/provers.a2ml+` in the same PR. @@ -345,5 +351,5 @@ provers`". If a count changes (new wave absorbed, backend retired), update this file in the same PR. The single source of truth for the count is -`+ProverKind::all()+` in `+src/rust/provers/mod.rs+`; this doc is the +`+ProverKind::all()+` in `+crates/echidna-core/src/prover_kind.rs+`; this doc is the human-readable mirror. diff --git a/scripts/check-verification-integrations.sh b/scripts/check-verification-integrations.sh new file mode 100644 index 00000000..a24fa461 --- /dev/null +++ b/scripts/check-verification-integrations.sh @@ -0,0 +1,121 @@ +#!/usr/bin/env bash +# SPDX-License-Identifier: MPL-2.0 +set -euo pipefail + +cd "$(dirname "$0")/.." +enum_source='crates/echidna-core/src/prover_kind.rs' +registry='.machine_readable/provers.a2ml' +ledger='.machine_readable/verification-integrations.a2ml' + +mapfile -t enum_names < <(awk ' + /^pub enum ProverKind \{/ { inside = 1; next } + inside && /^}/ { exit } + inside && /^ [[:alpha:]][[:alnum:]_]*,/ { + name = $1; sub(/,$/, "", name); print name + } +' "$enum_source" | LC_ALL=C sort) +mapfile -t registry_names < <(sed -n 's/^\[prover\.\([[:alnum:]_]*\)\]$/\1/p' "$registry" | LC_ALL=C sort) + +if ((${#enum_names[@]} != 141)); then + printf 'Expected 141 ProverKind declarations, found %s\n' "${#enum_names[@]}" >&2 + exit 1 +fi +if ! diff -u <(printf '%s\n' "${enum_names[@]}") <(printf '%s\n' "${registry_names[@]}"); then + printf 'Registry differs from ProverKind declarations\n' >&2 + exit 1 +fi +if ! grep -Eq '^count[[:space:]]*=[[:space:]]*141$' "$registry" || + ! grep -Eq '^source[[:space:]]*=[[:space:]]*"crates/echidna-core/src/prover_kind.rs::ProverKind"$' "$registry"; then + printf 'Registry count or source metadata is stale\n' >&2 + exit 1 +fi +if ! grep -Fxq 'schema = "verification-integrations/1"' "$ledger" || + ! grep -Fxq 'enum_default = "declared_unverified"' "$ledger"; then + printf 'Ledger schema or default status is stale\n' >&2 + exit 1 +fi +if ! grep -Fxq "enum_source = \"$enum_source\"" "$ledger"; then + printf 'Ledger enum_source is stale\n' >&2 + exit 1 +fi +if ! grep -Fxq "enum_registry = \"$registry\"" "$ledger"; then + printf 'Ledger enum_registry is stale\n' >&2 + exit 1 +fi + +awk ' + /^[[:space:]]*$/ || /^#/ { next } + /^\[metadata\]$/ || /^\[tool\.[[:alnum:]_]+\]$/ { next } + /^[a-z_]+ = "[^"]*"$/ { next } + /^local_paths = \["[^"]+"(, "[^"]+")*\]$/ { next } + { printf "Unsupported or malformed ledger line %d: %s\n", NR, $0 > "/dev/stderr"; exit 1 } +' "$ledger" + +declare -A statuses kinds parents roles evidence +while IFS='|' read -r tool status kind parent role has_paths; do + [[ -n "$tool" ]] || continue + if [[ -v statuses[$tool] ]]; then + printf 'Duplicate tool entry: %s\n' "$tool" >&2; exit 1 + fi + case "$status" in + backend_declared|via_parent|partial_non_backend|not_integrated|not_a_prover) ;; + *) printf 'Invalid status for %s: %s\n' "$tool" "$status" >&2; exit 1 ;; + esac + statuses[$tool]="$status" + kinds[$tool]="$kind" + parents[$tool]="$parent" + roles[$tool]="$role" + evidence[$tool]="$has_paths" +done < <(awk ' + # Write the current tool, status, kind, parent, role and path-presence flag + # to stdout as one pipe-delimited line; emit nothing when tool is empty. + function emit() { if (tool != "") print tool "|" status "|" kind "|" parent "|" role "|" has_paths } + /^\[tool\.[[:alnum:]_]+\]$/ { + emit(); tool = $0; sub(/^\[tool\./, "", tool); sub(/\]$/, "", tool) + status = kind = parent = role = has_paths = ""; next + } + tool != "" && /^status = / { status = $3; gsub(/"/, "", status) } + tool != "" && /^prover_kind = / { kind = $3; gsub(/"/, "", kind) } + tool != "" && /^parent_tool = / { parent = $3; gsub(/"/, "", parent) } + tool != "" && /^role = / { role = $0; sub(/^role = "/, "", role); sub(/"$/, "", role) } + tool != "" && /^local_paths = / { has_paths = "yes" } + END { emit() } +' "$ledger") + +if ((${#statuses[@]} != 12)); then + printf 'Expected 12 assessed tool roles, found %s\n' "${#statuses[@]}" >&2 + exit 1 +fi +for tool in "${!statuses[@]}"; do + if [[ -z "${roles[$tool]}" ]]; then + printf 'Missing role for %s\n' "$tool" >&2; exit 1 + fi + if [[ "${statuses[$tool]}" == backend_declared ]]; then + if [[ -z "${kinds[$tool]}" ]] || ! printf '%s\n' "${enum_names[@]}" | grep -Fxq "${kinds[$tool]}"; then + printf 'Missing declared backend variant for %s\n' "$tool" >&2; exit 1 + fi + if [[ "${evidence[$tool]}" != yes ]]; then + printf 'Missing local backend evidence for %s\n' "$tool" >&2; exit 1 + fi + elif [[ -n "${kinds[$tool]}" ]]; then + printf 'Non-backend %s declares a prover variant\n' "$tool" >&2; exit 1 + fi + if [[ "${statuses[$tool]}" == not_integrated || "${statuses[$tool]}" == not_a_prover ]] && + printf '%s\n' "${enum_names[@]}" | grep -Fxq "$tool"; then + printf '%s is declared in ProverKind but marked %s\n' "$tool" "${statuses[$tool]}" >&2; exit 1 + fi + if [[ "${statuses[$tool]}" == via_parent ]]; then + if [[ -z "${parents[$tool]}" || ! -v statuses[${parents[$tool]}] ]]; then + printf 'Missing parent tool for %s\n' "$tool" >&2; exit 1 + fi + fi +done + +while IFS= read -r path; do + [[ -n "$path" ]] || continue + if ! git cat-file -e "HEAD:$path" 2>/dev/null; then + printf 'Missing local evidence path: %s\n' "$path" >&2; exit 1 + fi +done < <(sed -n 's/^local_paths = \[\(.*\)\]$/\1/p' "$ledger" | tr -d '" ' | tr ',' '\n') + +printf 'OK: %s ProverKind declarations; %s assessed tool roles\n' "${#enum_names[@]}" "${#statuses[@]}" diff --git a/scripts/gen-provers-a2ml.sh b/scripts/gen-provers-a2ml.sh index 01cdb4b3..8b4e5b87 100755 --- a/scripts/gen-provers-a2ml.sh +++ b/scripts/gen-provers-a2ml.sh @@ -32,22 +32,22 @@ cat << 'HEADER' # # provers.a2ml — Authoritative enumeration of ECHIDNA prover backends. # -# Generated from src/rust/provers/mod.rs::ProverKind. One section per +# Generated from crates/echidna-core/src/prover_kind.rs::ProverKind. One section per # variant, keyed by the variant's PascalCase name for stability against # slug-format drift. `slug` is the snake_case identifier used on the # wire (matches serde's rename_all = "snake_case" default). # -# Downstream consumers: -# - .github/workflows/backend-matrix.yml (vcl-ut) reads this file to -# build its matrix strategy, one job per prover. -# - Future sync check fails CI if this file drifts from ProverKind::all(). +# This is a declaration inventory, not a claim that each variant has a +# runnable backend or a successful proof. See verification-integrations.a2ml +# for the assessed roles of selected tools outside and within this enum. # -# SYNC SOURCE-OF-TRUTH: `pub enum ProverKind` in src/rust/provers/mod.rs. +# SYNC SOURCE-OF-TRUTH: `pub enum ProverKind` in +# crates/echidna-core/src/prover_kind.rs. # If that enum changes, regenerate with scripts/gen-provers-a2ml.sh. [metadata] version = "1.0.0" -source = "src/rust/provers/mod.rs::ProverKind" +source = "crates/echidna-core/src/prover_kind.rs::ProverKind" HEADER # Emitted outside the quoted heredoc so it is evaluated at run time rather