Skip to content

Commit e4ec090

Browse files
hyperpolymathclaude
andcommitted
feat(panel): N3 — StrategyDrift panel scaffold (config + README)
New clade panel 'strategy-drift' for visualising the learning loop's strategy recommendations and drift events. Scaffolded with config (K9 kennel format matching other panels like verisim-feeds) + README documenting the four data sources and four views: - Timeline: per-class top-prover trajectory over time - Certs Grid: 11-class × 42-prover cert status grid (PROVEN/ pending/sanctified borders) - Drift Events: append-only log of shift events with candidate re-queue counts - Coverage Bars: per-class n_repos × n_provers × n_attempts Data sources: - verisim-api /strategy, /certificates, /coverage endpoints - hypatia Hypatia.Rules.StrategyDrift ETS snapshot Backend endpoints all live and tested (committed in verisimdb e7c5e5a, b660778, a4b5453 and hypatia d6b5144). ReScript/Deno panel module itself is scheduled as follow-up work. Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
1 parent 3c7fa3d commit e4ec090

2 files changed

Lines changed: 145 additions & 0 deletions

File tree

Lines changed: 74 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,74 @@
1+
// SPDX-License-Identifier: PMPL-1.0-or-later
2+
= Strategy Drift Panel (StrategyDrift)
3+
:toc: preamble
4+
5+
Visualises the learning loop's strategy recommendations over time,
6+
the PROVEN/SANCTIFY certificate landscape, and strategy-shift events
7+
that trigger re-proving of previously-failed attempts.
8+
9+
== Data Sources
10+
11+
Four endpoints on `verisim-api` plus one ETS snapshot on `hypatia`:
12+
13+
[cols="1,2,2"]
14+
|===
15+
| Source | Endpoint | Refresh
16+
17+
| Strategy
18+
| `GET /api/v1/proof_attempts/strategy?class=X`
19+
| On user action (class selector)
20+
21+
| Certificates
22+
| `GET /api/v1/proof_attempts/certificates`
23+
| Every 60s
24+
25+
| Coverage
26+
| `GET /api/v1/proof_attempts/coverage`
27+
| Every 60s
28+
29+
| Drift snapshot
30+
| `Hypatia.Rules.StrategyDrift.snapshot/0` (ETS via HTTP bridge)
31+
| Every 60s
32+
|===
33+
34+
== Views
35+
36+
=== Timeline
37+
Per-class top-prover trajectory. Each obligation class gets its own row;
38+
colour-coded segments show which prover held the top rank during that
39+
time window. Drift events appear as vertical separators.
40+
41+
=== Certs Grid
42+
11-obligation-classes × 42-provers cell grid. Each cell shows
43+
`success_rate × total_attempts` as size and colour intensity. Cell
44+
border indicates certificate status:
45+
46+
* thin grey — pending
47+
* green — proven
48+
* gold double-border — proven AND part of a sanctified class
49+
50+
=== Drift Events
51+
Append-only log of `{timestamp, class, old_top, new_top, candidates_requeued}`
52+
records, produced by `Hypatia.Rules.StrategyDrift.check_all_shifts/1`
53+
on each polling tick.
54+
55+
=== Coverage Bars
56+
Per-class horizontal bar triple: `n_repos`, `n_provers`, `n_attempts`.
57+
Surfaces how narrow or broad the evidence base is for each class —
58+
a class with `n_repos=1` has narrow cross-repo transfer confidence.
59+
60+
== Related
61+
62+
* verisimdb source — `.../proof_attempts*` handlers and MV DDL
63+
* hypatia — `Hypatia.Rules.ProofStrategySelection` (N1 novelty gate +
64+
N2 quarantine) and `Hypatia.Rules.StrategyDrift` (N4 drift tracker)
65+
* `docs/design/DESIGN-2026-04-05-V4-proof-attempts-vqldt.adoc` (V4 cert design)
66+
67+
== Implementation Status (2026-04-05)
68+
69+
* Config scaffolded (this file)
70+
* Backend endpoints live on `verisim-api` (strategy, certificates,
71+
coverage — all tested, plus hypatia ETS snapshot via StrategyDrift)
72+
* ReScript/Deno panel module — not yet written (placeholder for
73+
follow-up sprint). Skeleton files follow the pattern established by
74+
`verisim-feeds` and other real panels.
Lines changed: 71 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,71 @@
1+
# K9 Kennel: Strategy Drift Panel Configuration
2+
# SPDX-License-Identifier: PMPL-1.0-or-later
3+
#
4+
# N3: Panel showing top-prover-per-class over time, with drift events
5+
# flagged. Data source: Verisim's /api/v1/proof_attempts/strategy and
6+
# /certificates endpoints, plus hypatia's StrategyDrift ETS snapshots.
7+
{
8+
pedigree = {
9+
name = "strategy-drift-config",
10+
version = "0.1.0",
11+
author = "Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>",
12+
leash = 'Kennel,
13+
},
14+
panel = {
15+
id = "StrategyDrift",
16+
short_name = "SD",
17+
description = "Top-prover-per-class over time + PROVEN/SANCTIFY certificates + drift events",
18+
has_backend = true,
19+
clade_id = "strategy-drift",
20+
isolation_tier = "native",
21+
},
22+
wiring = {
23+
model_slice = "strategyDrift",
24+
msg_namespace = "strategyDriftMsg",
25+
view_route = "PanelStrategyDrift",
26+
module_name = "StrategyDrift",
27+
},
28+
data_sources = {
29+
primary = {
30+
endpoint = "http://localhost:8080/api/v1/proof_attempts/strategy",
31+
method = "GET",
32+
query_params = ["class", "limit"],
33+
},
34+
certificates = {
35+
endpoint = "http://localhost:8080/api/v1/proof_attempts/certificates",
36+
method = "GET",
37+
query_params = ["class", "prover", "evidence_limit"],
38+
},
39+
coverage = {
40+
endpoint = "http://localhost:8080/api/v1/proof_attempts/coverage",
41+
method = "GET",
42+
},
43+
drift_snapshot = {
44+
source = "hypatia.Hypatia.Rules.StrategyDrift.snapshot/0",
45+
refresh_interval_seconds = 60,
46+
},
47+
},
48+
views = {
49+
timeline = {
50+
description = "Per-class top prover trajectory. X: time. Y: class. Colour: prover.",
51+
obligation_classes = [
52+
"safety", "linearity", "termination", "equiv", "correctness",
53+
"confluence", "totality", "invariant", "refinement", "model-check", "other"
54+
],
55+
},
56+
certs_grid = {
57+
description = "11-class × N-prover grid. Cell = success_rate × total_attempts. Border = cert status (proven/pending/sanctified).",
58+
},
59+
drift_events = {
60+
description = "List of (timestamp, class, old_top, new_top, candidates_requeued) shifts.",
61+
},
62+
coverage_bars = {
63+
description = "Per-class: n_repos × n_provers × n_attempts horizontal bars.",
64+
},
65+
},
66+
obligations = {
67+
requires_tests = true,
68+
requires_backend_health = true,
69+
requires_clade_manifest = true,
70+
},
71+
}

0 commit comments

Comments
 (0)