Skip to content

Commit a4b5453

Browse files
hyperpolymathclaude
hyperpolymath
and
claude
committed
feat(abi): N6 — Idris2 ProofAttempts ABI with typed ObligationClass
New module VeriSimDB.ABI.ProofAttempts exposes the 11-value obligation_class allow-list as a sum type, plus round-trip correctness proofs (roundTrip : (c : ObligationClass) -> obligationClassFromString (obligationClassToString c) = Just c). Typed fields in ProofAttemptSubmission record: obligationClass : ObligationClass — 11 variants, compile-time checked outcome : Outcome — 4 variants, compile-time checked Free-form fields validated at runtime (UUIDs, timestamps, paths, etc.). Kept in sync with: - rust-core/verisim-api/src/proof_attempts.rs ALLOWED_OBLIGATION_CLASSES - connectors/test-infra/seed/clickhouse-init.sql proof_attempts.obligation_class - verification/proofs/idris2/OctadCoherence.idr modality tags Effect on downstream clients: any client that goes through the ABI now cannot construct a submission with a misspelled obligation_class (e.g., "linaerity") — the compiler rejects it. The Rust API boundary still validates strings for clients that bypass the ABI. idris2 --check rc=0 with %default total; all round-trip lemmas discharged via Refl. Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
1 parent b660778 commit a4b5453

1 file changed

Lines changed: 141 additions & 0 deletions

File tree

‎src/abi/VeriSimDB/ABI/ProofAttempts.idr‎

Lines changed: 141 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,141 @@
1+
||| SPDX-License-Identifier: PMPL-1.0-or-later
2+
||| VeriSimDB ABI — Proof Attempts submission types
3+
|||
4+
||| N6: Typed obligation_class. The verisim-api POST /api/v1/proof_attempts
5+
||| endpoint accepts obligation_class as a String (validated at runtime
6+
||| against an 11-value allow-list). This module exposes the same
7+
||| allow-list as an Idris2 data type so clients that go through the ABI
8+
||| can't construct a submission with a typo-ed class.
9+
|||
10+
||| Callers construct ProofAttemptSubmission with an ObligationClass
11+
||| value; the obligationClassToString function renders the canonical
12+
||| API-compatible lowercase string.
13+
14+
module VeriSimDB.ABI.ProofAttempts
15+
16+
%default total
17+
18+
--------------------------------------------------------------------------------
19+
-- Obligation class (the 11 allowed values)
20+
--------------------------------------------------------------------------------
21+
22+
||| The eleven obligation classes accepted by the proof_attempts table.
23+
||| Values mirror the allow-list enforced at the API boundary in
24+
||| verisim-api::proof_attempts::validate_obligation_class and the
25+
||| Enum8 / String column stored in ClickHouse.
26+
|||
27+
||| Kept in sync with:
28+
||| - rust-core/verisim-api/src/proof_attempts.rs (ALLOWED_OBLIGATION_CLASSES)
29+
||| - verification/proofs/idris2/OctadCoherence.idr (modality tags)
30+
||| - connectors/test-infra/seed/clickhouse-init.sql (proof_attempts.obligation_class)
31+
public export
32+
data ObligationClass
33+
= Safety -- invariants, non-interference, memory safety
34+
| Linearity -- linear/affine/ownership claims
35+
| Termination -- halting, totality, structural recursion
36+
| Equiv -- equivalence, behaviour preservation, bisimulation
37+
| Correctness -- functional correctness / specification conformance
38+
| Confluence -- rewriting systems: diamond / Church-Rosser
39+
| Totality -- no partial functions, no undefined behaviour
40+
| Invariant -- predicate holds through state transitions
41+
| Refinement -- spec S1 refines spec S2
42+
| ModelCheck -- LTL/CTL model-checking obligations
43+
| Other -- any obligation class not yet canonicalised
44+
45+
||| Serialise an ObligationClass to its canonical wire-format string.
46+
||| The API accepts these exact values; any other string is rejected
47+
||| with HTTP 400.
48+
public export
49+
obligationClassToString : ObligationClass -> String
50+
obligationClassToString Safety = "safety"
51+
obligationClassToString Linearity = "linearity"
52+
obligationClassToString Termination = "termination"
53+
obligationClassToString Equiv = "equiv"
54+
obligationClassToString Correctness = "correctness"
55+
obligationClassToString Confluence = "confluence"
56+
obligationClassToString Totality = "totality"
57+
obligationClassToString Invariant = "invariant"
58+
obligationClassToString Refinement = "refinement"
59+
obligationClassToString ModelCheck = "model-check"
60+
obligationClassToString Other = "other"
61+
62+
||| Parse a wire-format string back to an ObligationClass. Returns
63+
||| Nothing if the string is not in the allow-list; callers should
64+
||| treat Nothing as "reject with HTTP 400".
65+
public export
66+
obligationClassFromString : String -> Maybe ObligationClass
67+
obligationClassFromString "safety" = Just Safety
68+
obligationClassFromString "linearity" = Just Linearity
69+
obligationClassFromString "termination" = Just Termination
70+
obligationClassFromString "equiv" = Just Equiv
71+
obligationClassFromString "correctness" = Just Correctness
72+
obligationClassFromString "confluence" = Just Confluence
73+
obligationClassFromString "totality" = Just Totality
74+
obligationClassFromString "invariant" = Just Invariant
75+
obligationClassFromString "refinement" = Just Refinement
76+
obligationClassFromString "model-check" = Just ModelCheck
77+
obligationClassFromString "other" = Just Other
78+
obligationClassFromString _ = Nothing
79+
80+
--------------------------------------------------------------------------------
81+
-- Round-trip correctness
82+
--------------------------------------------------------------------------------
83+
84+
||| Round-trip: serialising then parsing is the identity on all classes.
85+
||| Every ObligationClass value ktoString is a valid input to fromString,
86+
||| and yields the original value.
87+
public export
88+
roundTrip : (c : ObligationClass) ->
89+
obligationClassFromString (obligationClassToString c) = Just c
90+
roundTrip Safety = Refl
91+
roundTrip Linearity = Refl
92+
roundTrip Termination = Refl
93+
roundTrip Equiv = Refl
94+
roundTrip Correctness = Refl
95+
roundTrip Confluence = Refl
96+
roundTrip Totality = Refl
97+
roundTrip Invariant = Refl
98+
roundTrip Refinement = Refl
99+
roundTrip ModelCheck = Refl
100+
roundTrip Other = Refl
101+
102+
--------------------------------------------------------------------------------
103+
-- Proof outcome (Enum8 in ClickHouse)
104+
--------------------------------------------------------------------------------
105+
106+
public export
107+
data Outcome = Success | Timeout | Failure | Unknown
108+
109+
public export
110+
outcomeToString : Outcome -> String
111+
outcomeToString Success = "success"
112+
outcomeToString Timeout = "timeout"
113+
outcomeToString Failure = "failure"
114+
outcomeToString Unknown = "unknown"
115+
116+
--------------------------------------------------------------------------------
117+
-- ProofAttemptSubmission
118+
--------------------------------------------------------------------------------
119+
120+
||| The payload for POST /api/v1/proof_attempts, with compile-time
121+
||| guarantees on the obligation class (typed) and outcome (typed).
122+
||| Fields kept as String are free-form (repo paths, UUIDs, claim text)
123+
||| and validated at runtime by verisim-api.
124+
public export
125+
record ProofAttemptSubmission where
126+
constructor MkProofAttemptSubmission
127+
attemptId : String -- UUID v4
128+
obligationId : String -- sha256(repo|file|claim) or similar
129+
repo : String -- "owner/name"
130+
file : String -- path relative to repo root
131+
claim : String -- human-readable claim
132+
obligationClass : ObligationClass -- TYPED — compile-time checked
133+
proverUsed : String -- lowercase prover name (free, 42 variants)
134+
outcome : Outcome -- TYPED — compile-time checked
135+
durationMs : Nat -- wall-clock duration
136+
confidence : Double -- [0.0, 1.0]
137+
strategyTag : String -- "batch-direct", "retry", etc.
138+
startedAt : String -- ISO-8601 DateTime64(3), no trailing Z
139+
completedAt : String -- ISO-8601 DateTime64(3), no trailing Z
140+
proverOutput : String -- truncated stdout+stderr
141+
errorMessage : Maybe String

0 commit comments

Comments
 (0)