Skip to content

Commit 6cb93e7

Browse files
hyperpolymathclaude
hyperpolymath
and
claude
committed
feat(verisim-api): V4 — proof_attempts ↔ VQL-DT certificates (V4a–V4d)
Auto-minting PROVEN + SANCTIFY certificates over mv_prover_success_by_class, policy-driven via a singleton config table. Certificates resolve read-time through views (not materialized) so policy changes apply immediately. Schema additions (verisimdb.*): - proof_attempts_cert_policy (ReplacingMergeTree, seeded τ=0.80, n=20, k=2, n_s=50) - mv_proven_certificates (VIEW: (class,prover) → status via CROSS JOIN on policy) - mv_sanctify_certificates (VIEW: class → status via ≥k PROVEN provers, ≥n combined) - mv_cert_evidence (VIEW: cert_id → backing proof_attempts rows) HTTP API: GET /api/v1/proof_attempts/certificates [?class=X][&prover=Y][&include_pending=BOOL][&include_sanctify=BOOL] [&evidence_limit=0..100] Returns: {policy, proven[], sanctify[]} with optional evidence[] per PROVEN cert. cert_id is deterministic (cityHash64 of "proven|class|prover" resp. "sanctify|class"), so repeat calls are stable and can be referenced in external systems. Exercised end-to-end with real data (35 attempts across 6 classes, 5 provers): default policy (τ=0.80, n=20): all 10 rows status=pending lowered policy (τ=0.80, n=3, k=2, n_s=5): proven: equiv/lean, equiv/agda (both rate=1.0, n=5) sanctified: equiv (2 proven provers, 10 combined attempts) Remaining V4 follow-ups: V4e (hypatia proof_strategy_selection prefers certified pairs), V4f (VQL-DT parser resolves PROOF PROVEN/SANCTIFY), V4g (VQL-SPEC update). Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
1 parent 6b984f4 commit 6cb93e7

6 files changed

Lines changed: 453 additions & 0 deletions

File tree

‎connectors/test-infra/seed/clickhouse-init.sql‎

Lines changed: 68 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -326,3 +326,71 @@ INSERT INTO verisimdb.proof_attempts VALUES
326326
'Guard rule prevents invalid transitions', 'safety', 'z3', 'success', 342, 0.99, NULL,
327327
'gnn-guided', now() - INTERVAL 30 MINUTE, now() - INTERVAL 30 MINUTE + INTERVAL 342 MILLISECOND,
328328
'unsat (proved, no counterexample).', NULL);
329+
330+
-- ---------------------------------------------------------------------------
331+
-- V4: Certificate policy + views (2026-04-05)
332+
-- See docs/design/DESIGN-2026-04-05-V4-proof-attempts-vqldt.adoc
333+
-- ---------------------------------------------------------------------------
334+
335+
CREATE TABLE IF NOT EXISTS verisimdb.proof_attempts_cert_policy
336+
(
337+
policy_id String DEFAULT 'default',
338+
tau_proven Float32,
339+
n_proven UInt64,
340+
k_sanctify UInt32,
341+
n_sanctify UInt64,
342+
updated_at DateTime64(3) DEFAULT now64(3)
343+
)
344+
ENGINE = ReplacingMergeTree(updated_at)
345+
ORDER BY policy_id;
346+
347+
INSERT INTO verisimdb.proof_attempts_cert_policy
348+
(policy_id, tau_proven, n_proven, k_sanctify, n_sanctify)
349+
VALUES ('default', 0.80, 20, 2, 50);
350+
351+
CREATE VIEW IF NOT EXISTS verisimdb.mv_proven_certificates AS
352+
SELECT
353+
m.obligation_class, m.prover_used,
354+
sum(m.success_count) AS success_count,
355+
sum(m.total_attempts) AS total_attempts,
356+
sum(m.total_duration_ms) AS total_duration_ms,
357+
sum(m.success_count) / sum(m.total_attempts) AS success_rate,
358+
sum(m.total_duration_ms) / sum(m.total_attempts) AS avg_duration_ms,
359+
p.tau_proven, p.n_proven,
360+
if(sum(m.success_count) / sum(m.total_attempts) >= p.tau_proven
361+
AND sum(m.total_attempts) >= p.n_proven, 'proven', 'pending') AS status,
362+
cityHash64(concat('proven|', toString(m.obligation_class), '|', toString(m.prover_used))) AS cert_id
363+
FROM verisimdb.mv_prover_success_by_class AS m
364+
CROSS JOIN (
365+
SELECT argMax(tau_proven, updated_at) AS tau_proven,
366+
argMax(n_proven, updated_at) AS n_proven
367+
FROM verisimdb.proof_attempts_cert_policy WHERE policy_id = 'default'
368+
) AS p
369+
GROUP BY m.obligation_class, m.prover_used, p.tau_proven, p.n_proven;
370+
371+
CREATE VIEW IF NOT EXISTS verisimdb.mv_sanctify_certificates AS
372+
SELECT
373+
pc.obligation_class,
374+
count(DISTINCT pc.prover_used) AS proven_provers,
375+
groupArray(pc.prover_used) AS provers,
376+
sum(pc.total_attempts) AS combined_attempts,
377+
p.k_sanctify, p.n_sanctify,
378+
if(count(DISTINCT pc.prover_used) >= p.k_sanctify
379+
AND sum(pc.total_attempts) >= p.n_sanctify, 'sanctified', 'pending') AS status,
380+
cityHash64(concat('sanctify|', toString(pc.obligation_class))) AS cert_id
381+
FROM verisimdb.mv_proven_certificates AS pc
382+
CROSS JOIN (
383+
SELECT argMax(k_sanctify, updated_at) AS k_sanctify,
384+
argMax(n_sanctify, updated_at) AS n_sanctify
385+
FROM verisimdb.proof_attempts_cert_policy WHERE policy_id = 'default'
386+
) AS p
387+
WHERE pc.status = 'proven'
388+
GROUP BY pc.obligation_class, p.k_sanctify, p.n_sanctify;
389+
390+
CREATE VIEW IF NOT EXISTS verisimdb.mv_cert_evidence AS
391+
SELECT
392+
cityHash64(concat('proven|', toString(pa.obligation_class), '|', toString(pa.prover_used))) AS cert_id,
393+
'proven' AS cert_type,
394+
pa.obligation_class, pa.prover_used, pa.attempt_id, pa.obligation_id,
395+
pa.outcome, pa.duration_ms, pa.confidence, pa.started_at, pa.repo, pa.file
396+
FROM verisimdb.proof_attempts AS pa;

‎rust-core/verisim-api/migrations/03_cert_policy.sql‎

Lines changed: 25 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,25 @@
1+
-- SPDX-License-Identifier: PMPL-1.0-or-later
2+
-- V4a: Certificate policy configuration
3+
-- ---------------------------------------------------------------------------
4+
-- Single-row table holding thresholds that govern PROVEN/SANCTIFY minting.
5+
-- Edit the row to tune certification strictness; the cert views (V4b) read
6+
-- from here on every query so changes propagate immediately.
7+
-- ---------------------------------------------------------------------------
8+
9+
CREATE TABLE IF NOT EXISTS verisimdb.proof_attempts_cert_policy
10+
(
11+
policy_id String DEFAULT 'default', -- singleton row key
12+
tau_proven Float32, -- success_rate threshold for PROVEN, e.g. 0.80
13+
n_proven UInt64, -- min total_attempts for PROVEN, e.g. 20
14+
k_sanctify UInt32, -- min DISTINCT proven provers, e.g. 2
15+
n_sanctify UInt64, -- min combined attempts for SANCTIFY, e.g. 50
16+
updated_at DateTime64(3) DEFAULT now64(3)
17+
)
18+
ENGINE = ReplacingMergeTree(updated_at)
19+
ORDER BY policy_id;
20+
21+
-- Seed default policy row matching the V4 design doc.
22+
INSERT INTO verisimdb.proof_attempts_cert_policy
23+
(policy_id, tau_proven, n_proven, k_sanctify, n_sanctify)
24+
VALUES
25+
('default', 0.80, 20, 2, 50);

‎rust-core/verisim-api/migrations/04_cert_views.sql‎

Lines changed: 63 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,63 @@
1+
-- SPDX-License-Identifier: PMPL-1.0-or-later
2+
-- V4b: Certificate views
3+
-- ---------------------------------------------------------------------------
4+
-- Two read-time views that compute PROVEN and SANCTIFY certificate status
5+
-- by joining aggregate prover outcomes against the policy thresholds.
6+
--
7+
-- These are regular VIEWs (not materialized) because:
8+
-- 1. The source MV (mv_prover_success_by_class) is already aggregated.
9+
-- 2. Policy changes must be reflected immediately, not on next refresh.
10+
-- 3. The cardinality is small: |obligation_class| × |prover| ≤ 200 rows.
11+
-- ---------------------------------------------------------------------------
12+
13+
-- PROVEN: a (class, prover) pair whose aggregate success_rate meets τ AND
14+
-- whose total_attempts meets N, per the current policy row.
15+
CREATE VIEW IF NOT EXISTS verisimdb.mv_proven_certificates AS
16+
SELECT
17+
m.obligation_class AS obligation_class,
18+
m.prover_used AS prover_used,
19+
sum(m.success_count) AS success_count,
20+
sum(m.total_attempts) AS total_attempts,
21+
sum(m.total_duration_ms) AS total_duration_ms,
22+
sum(m.success_count) / sum(m.total_attempts) AS success_rate,
23+
sum(m.total_duration_ms) / sum(m.total_attempts) AS avg_duration_ms,
24+
p.tau_proven AS tau_proven,
25+
p.n_proven AS n_proven,
26+
if(sum(m.success_count) / sum(m.total_attempts) >= p.tau_proven
27+
AND sum(m.total_attempts) >= p.n_proven,
28+
'proven', 'pending') AS status,
29+
cityHash64(concat('proven|', toString(m.obligation_class),
30+
'|', toString(m.prover_used))) AS cert_id
31+
FROM verisimdb.mv_prover_success_by_class AS m
32+
CROSS JOIN (
33+
SELECT argMax(tau_proven, updated_at) AS tau_proven,
34+
argMax(n_proven, updated_at) AS n_proven
35+
FROM verisimdb.proof_attempts_cert_policy
36+
WHERE policy_id = 'default'
37+
) AS p
38+
GROUP BY m.obligation_class, m.prover_used, p.tau_proven, p.n_proven;
39+
40+
41+
-- SANCTIFY: a class for which at least k_sanctify distinct provers each
42+
-- hold PROVEN status AND their combined attempts meet N_sanctify.
43+
CREATE VIEW IF NOT EXISTS verisimdb.mv_sanctify_certificates AS
44+
SELECT
45+
pc.obligation_class AS obligation_class,
46+
count(DISTINCT pc.prover_used) AS proven_provers,
47+
groupArray(pc.prover_used) AS provers,
48+
sum(pc.total_attempts) AS combined_attempts,
49+
p.k_sanctify AS k_sanctify,
50+
p.n_sanctify AS n_sanctify,
51+
if(count(DISTINCT pc.prover_used) >= p.k_sanctify
52+
AND sum(pc.total_attempts) >= p.n_sanctify,
53+
'sanctified', 'pending') AS status,
54+
cityHash64(concat('sanctify|', toString(pc.obligation_class))) AS cert_id
55+
FROM verisimdb.mv_proven_certificates AS pc
56+
CROSS JOIN (
57+
SELECT argMax(k_sanctify, updated_at) AS k_sanctify,
58+
argMax(n_sanctify, updated_at) AS n_sanctify
59+
FROM verisimdb.proof_attempts_cert_policy
60+
WHERE policy_id = 'default'
61+
) AS p
62+
WHERE pc.status = 'proven'
63+
GROUP BY pc.obligation_class, p.k_sanctify, p.n_sanctify;

‎rust-core/verisim-api/migrations/05_cert_evidence.sql‎

Lines changed: 27 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,27 @@
1+
-- SPDX-License-Identifier: PMPL-1.0-or-later
2+
-- V4c: Certificate evidence
3+
-- ---------------------------------------------------------------------------
4+
-- Maps cert_ids back to their backing proof_attempts rows. Evidence is
5+
-- computed on-read from proof_attempts (no persistence) to avoid snapshotting
6+
-- drift — a cert's evidence set is always the current attempts, so if later
7+
-- attempts falsify the claim the cert's supporting evidence follows.
8+
--
9+
-- The API layer (V4d) paginates this view with LIMIT.
10+
-- ---------------------------------------------------------------------------
11+
12+
CREATE VIEW IF NOT EXISTS verisimdb.mv_cert_evidence AS
13+
SELECT
14+
cityHash64(concat('proven|', toString(pa.obligation_class),
15+
'|', toString(pa.prover_used))) AS cert_id,
16+
'proven' AS cert_type,
17+
pa.obligation_class AS obligation_class,
18+
pa.prover_used AS prover_used,
19+
pa.attempt_id AS attempt_id,
20+
pa.obligation_id AS obligation_id,
21+
pa.outcome AS outcome,
22+
pa.duration_ms AS duration_ms,
23+
pa.confidence AS confidence,
24+
pa.started_at AS started_at,
25+
pa.repo AS repo,
26+
pa.file AS file
27+
FROM verisimdb.proof_attempts AS pa;

‎rust-core/verisim-api/src/lib.rs‎

Lines changed: 4 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -828,6 +828,10 @@ pub fn build_router(state: AppState) -> Router {
828828
"/api/v1/proof_attempts/strategy",
829829
get(proof_attempts::strategy_handler),
830830
)
831+
.route(
832+
"/api/v1/proof_attempts/certificates",
833+
get(proof_attempts::certificates_handler),
834+
)
831835
// Authentication middleware layer
832836
.layer(axum_middleware::from_fn_with_state(
833837
auth_state,

0 commit comments

Comments
 (0)