Skip to content

Commit 0ef64b2

Browse files
hyperpolymathclaude
andcommitted
docs: update CHANGELOG + STATE for proof_attempts loop + Zig client
Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
1 parent 44dcded commit 0ef64b2

2 files changed

Lines changed: 18 additions & 3 deletions

File tree

.machine_readable/6a2/STATE.a2ml

Lines changed: 6 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -7,7 +7,7 @@
77
(version "1.1.0")
88
(schema-version "1.0")
99
(created "2026-01-03")
10-
(updated "2026-04-04")
10+
(updated "2026-04-05")
1111
(project "verisimdb")
1212
(repo "github.com/hyperpolymath/verisimdb")
1313
(crg-grade "C"))
@@ -40,7 +40,9 @@
4040
("Full-text search" "working")
4141
("Graph relationships" "working")
4242
("Temporal versioning" "working")
43-
("Atomic transactions" "working")))
43+
("Atomic transactions" "working")
44+
("proof_attempts learning loop" "working")
45+
("Zig client SDK with C ABI" "working")))
4446

4547
(route-to-mvp
4648
(milestones
@@ -80,4 +82,5 @@
8082
("Plan grade B work (mutation testing)" "TODO")))
8183

8284
(session-history
83-
("2026-04-04: CRG C blitz - added 55 tests across E2E, contract, aspect, reflexive, property categories"))))
85+
("2026-04-04: CRG C blitz - added 55 tests across E2E, contract, aspect, reflexive, property categories")
86+
("2026-04-05: added proof_attempts learning loop (table + MV + /strategy endpoint) and Zig client SDK; closes loop with echidna/hypatia"))))

CHANGELOG.adoc

Lines changed: 12 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -11,6 +11,18 @@ All notable changes to VeriSimDB are documented here. This project uses https://
1111

1212
=== Added
1313

14+
==== Proof-Attempts Learning Loop (2026-04-05)
15+
- **proof_attempts ClickHouse table**: Records every prover invocation across the estate (attempt_id, obligation_id, repo, file, claim, obligation_class, prover_used, outcome, duration_ms, confidence, strategy_tag, timestamps). 20-prover enum covering the echidna portfolio.
16+
- **mv_prover_success_by_class materialized view**: SummingMergeTree aggregation of success_count / total_attempts / total_duration_ms per (obligation_class, prover_used) — the source of truth for strategy recommendations.
17+
- **POST /api/v1/proof_attempts**: echidna's `verisimdb_bridge` posts here on every attempt.
18+
- **GET /api/v1/proof_attempts/strategy?class=<class>&limit=<n>**: Returns provers ranked by success_rate DESC, avg_duration_ms ASC. Consumed by hypatia's `ProofStrategySelection` rule.
19+
- Closes the learning loop: echidna runs prover → this table → hypatia reads MV → strategy recommendation fed back to echidnabot as prover hint in the GraphQL mutation.
20+
21+
==== Zig Client SDK
22+
- **connectors/clients/zig/**: Native Zig client with thin C ABI wrapper. Produces `libverisimdb_zig.{a,so}`. Aligns with hyperpolymath ABI/FFI standard (Idris2 ABI + Zig FFI).
23+
- Exposes: `verisimdb_health`, `verisimdb_create_octad`, `verisimdb_get_octad`, `verisimdb_update_octad`, `verisimdb_delete_octad`, `verisimdb_vql_execute`, `verisimdb_free`.
24+
- 9 integration tests against live verisim-api.
25+
1426
==== Security Hardening (Phase 1)
1527
- **RwLock poisoning protection**: 35+ locations across 7 Rust files converted from `.expect("poisoned")` panics to graceful `map_err` error propagation. Server no longer crashes on lock contention.
1628
- **API error sanitization**: Internal Rust error strings no longer leak to clients. All `ApiError::Internal` responses now log the real error via tracing and return a generic "Internal server error" to the client.

0 commit comments

Comments
 (0)