Repository navigation
Document verification integration status separately from prover declarations #463
There are no files selected for viewing
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -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" |
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -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 | ||
|
Comment on lines
+23
to
+25
There was a problem hiding this comment.
When Useful? React with 👍 / 👎. |
||
| 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 | ||
|
Comment on lines
+37
to
+39
There was a problem hiding this comment.
When Useful? React with 👍 / 👎. |
||
| 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 | ||
|
Comment on lines
+60
to
+63
There was a problem hiding this comment.
When a tool's Useful? React with 👍 / 👎. |
||
| 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 | ||
|
There was a problem hiding this comment.
When Creusot's Useful? React with 👍 / 👎. |
||
| 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 | ||
|
Comment on lines
+93
to
+95
There was a problem hiding this comment.
When a Useful? React with 👍 / 👎.
Comment on lines
+94
to
+95
There was a problem hiding this comment.
When Idris2's Useful? React with 👍 / 👎. |
||
| 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 | ||
|
Comment on lines
+100
to
+101
There was a problem hiding this comment.
When a currently non-integrated tool such as Kani later gains a Useful? React with 👍 / 👎. |
||
| 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 | ||
|
Check warning on line 108 in scripts/check-verification-integrations.sh
|
||
| printf 'Missing parent tool for %s\n' "$tool" >&2; exit 1 | ||
|
Comment on lines
+107
to
+109
There was a problem hiding this comment.
When a Useful? React with 👍 / 👎. |
||
| 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[@]}" | ||
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Script executed:
Repository: hyperpolymath/echidna
Length of output: 22295
Script executed:
Repository: hyperpolymath/echidna
Length of output: 29928
Script executed:
Repository: hyperpolymath/echidna
Length of output: 10862
Run the inventory check in CI.
If a
ProverKindvariant is added without updatingprovers.a2ml, the manifest gate will not detect the mismatch. Runscripts/check-verification-integrations.pyin a pull-request workflow to catch it.