Skip to content

Commit 946541f

Browse files
Add minimal browser UI and update prover documentation (#100)
## Summary This PR introduces a self-contained browser UI for proof submission and updates documentation to reflect the actual prover surface exposed by the REST API. The changes clarify that while ECHIDNA implements 100+ prover backends, the default API surface is deliberately limited to a 12-prover core set. ## Key Changes - **New file: `src/ui/public/prove.html`** — A minimal, self-contained REST client UI for proof submission - No build step required; opens directly in any modern browser via `file://` - Connects to a running ECHIDNA server (e.g., `cargo run -- server --cors`) - Supports prover selection, timeout configuration, neural assist toggle - Displays proof results with elapsed time, goal count, and outcome status - Includes example SMT-LIB snippets (Z3 SAT/UNSAT) for quick testing - Dark theme with GitHub-inspired color palette - **New file: `docs/SUPPORTED_PROVERS.md`** — Authoritative documentation of prover support - Clarifies the 12-prover core set exposed via `GET /api/provers` - Documents required external binaries and installation hints for each core prover - Explains the distinction between core (12), advertised (67), and total (141) prover variants - Provides quickstart instructions for proving the first goal with Z3 - Describes how to expose additional backends through the REST API - **Updated: `README.adoc`** - Revised prover badge from "128" to "12 core / 67 advertised" - Updated test count from "917+" to "1059" - Replaced "Leadership Position" section with "Prover Surface" and "Distinguishing Features" - Simplified prover tier table to focus on the 12-core set - Added "Prove your first goal" quickstart section with curl examples - Updated architecture documentation to reflect 102 backend implementation files - Clarified test suite counts and VeriSim integration - **Minor: `src/rust/corpus/octad.rs`** — Refactored hex formatting - Extracted `to_hex()` helper function to avoid repeated `format!("{:x}", ...)` patterns - Applied consistently across `octad_key()`, `cross_prover_key()`, `content_hash_of()`, and `hash_provenance()` - Improves code maintainability and readability ## Implementation Details The browser UI (`prove.html`) is fully self-contained with: - Inline CSS (dark theme with semantic color variables) - Vanilla JavaScript (no dependencies) - Health check polling on API base change - Prover roster auto-loading from `/api/provers` - Real-time result display with outcome classification (ok/bad/warn) - Example snippets that auto-populate content and prover selection The documentation updates align the public-facing narrative with the actual REST API surface, reducing confusion for new users while preserving the full 100+ prover capability for Rust API consumers. https://claude.ai/code/session_01RLu1DN3tSHfaVc8aqTd7VZ --------- Co-authored-by: Claude <noreply@anthropic.com>
1 parent 36c7b18 commit 946541f

31 files changed

Lines changed: 838 additions & 187 deletions

.machine_readable/6a2/ANCHOR.a2ml

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1,3 +1,4 @@
1+
# SPDX-License-Identifier: MPL-2.0
12
# ⚓ ANCHOR: rsr-template-repo
23
# Canonical authority and project recalibration trigger for rsr-template-repo.
34
# Template from: https://github.com/hyperpolymath/standards

.machine_readable/contractiles/bust/bust.k9.ncl

Lines changed: 4 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -51,6 +51,10 @@ let base = import "../_base.ncl" in
5151
allow_filesystem_write = true, # drills may write transient state (tmp dirs, test DBs)
5252
allow_subprocess = true,
5353
injection_scope = 'system_under_test_only,
54+
# Hunt-tier files must declare whether a cryptographic signature
55+
# is required. Bust trident runs in CI on every PR; signatures
56+
# are enforced at the trident-runner layer, not in-band.
57+
signature_required = true,
5458
},
5559
},
5660

0 commit comments

Comments
 (0)