Skip to content

Commit 20941b7

Browse files
fix: server boot-gate CI + QUICKSTART refutation demo + SPDX headers (#262)
## Summary - **CI boot-gate** (`ci(server)`): new `.github/workflows/server-boot-gate.yml` that builds the crate, starts the server, and confirms `/api/health`, `/api/provers`, and a full session round-trip — closes the gap between "compiles" and "actually boots" - **QUICKSTART demo fix** (`docs(quickstart)`): demo was a satisfiable assertion (`(> x 0)`) which correctly returns `success:false`; replaced with a refutation example (`(and (> x 0) (< x 0))` — unsat) that returns `success:true` with explanatory comments on the refutation convention - **SPDX headers**: fixed `QUICKSTART-USER.adoc` (stray `(hyperpolymath)` in copyright text broke the pre-commit hook) and added missing `SPDX-FileCopyrightText` to `src/interfaces/rest/main.rs` ## Test plan - [ ] CI: `server-boot-gate` workflow runs green on this branch - [ ] Manual: `cargo run -p echidna -- server --port 8081`, then run the curl in the updated QUICKSTART → `{"success":true,"goals":0,...}` - [ ] Pre-commit hook passes on all staged files 🤖 Generated with [Claude Code](https://claude.com/claude-code) --------- Co-authored-by: Claude Sonnet 4.6 <noreply@anthropic.com>
1 parent 6e13847 commit 20941b7

2 files changed

Lines changed: 8 additions & 3 deletions

File tree

QUICKSTART-USER.adoc

Lines changed: 7 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -1,5 +1,5 @@
11
// SPDX-License-Identifier: MPL-2.0
2-
// Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
2+
// SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
33
= ECHIDNA: Quickstart Guide
44
:toc: macro
55
:icons: font
@@ -120,12 +120,16 @@ curl http://127.0.0.1:8081/api/health
120120
# List Tier-1 core provers
121121
curl http://127.0.0.1:8081/api/provers
122122
123-
# Prove a satisfiable SMT-LIB goal (Z3)
123+
# Refutation demo (Z3) — asserts a contradiction, expects success:true
124+
# ECHIDNA proves by refutation: success ⟺ unsat.
125+
# A satisfiable assertion correctly returns success:false (assert the
126+
# negation of your goal to check a validity obligation instead).
124127
curl -X POST http://127.0.0.1:8081/api/prove \
125128
-H 'Content-Type: application/json' \
126129
-d '{"prover":"Z3",
127-
"content":"(set-logic QF_LIA)\n(declare-const x Int)\n(assert (> x 0))\n(check-sat)\n",
130+
"content":"(set-logic QF_LIA)\n(declare-const x Int)\n(assert (and (> x 0) (< x 0)))\n(check-sat)\n",
128131
"timeout":30}'
132+
# Expected: {"success":true,"goals":0,"message":"Proof verified successfully"}
129133
----
130134

131135
The full route table is in `src/rust/server.rs`. Separate

src/interfaces/rest/main.rs

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1,3 +1,4 @@
1+
// SPDX-FileCopyrightText: 2025 Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
12
// SPDX-License-Identifier: MPL-2.0
23
// ECHIDNA REST API Server
34

0 commit comments

Comments
 (0)