1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
|
"""Typed contracts for the literal five-stage GAP kernel pipeline."""
from __future__ import annotations
import json
import re
from typing import Any, Literal
from pydantic import BaseModel, ConfigDict, Field, field_validator, model_validator
from .models import SCHEMA_VERSION
class StrictModel(BaseModel):
model_config = ConfigDict(extra="forbid")
class ProofNode(StrictModel):
node_id: str
claim: str
dependencies: list[str] = Field(default_factory=list)
@model_validator(mode="after")
def validate_content(self) -> "ProofNode":
if not re.fullmatch(r"n[1-9][0-9]*", self.node_id):
raise ValueError("proof node IDs must be n1, n2, ...")
if not self.claim.strip():
raise ValueError("proof-node claim must be non-empty")
if len(self.dependencies) != len(set(self.dependencies)):
raise ValueError(f"{self.node_id} has duplicate dependencies")
return self
class ProofDAG(StrictModel):
nodes: list[ProofNode] = Field(min_length=1)
terminal_node_id: str
def node_ids(self) -> list[str]:
return [node.node_id for node in self.nodes]
@model_validator(mode="after")
def validate_graph(self) -> "ProofDAG":
node_ids = self.node_ids()
expected = [f"n{index}" for index in range(1, len(node_ids) + 1)]
if node_ids != expected:
raise ValueError("proof DAG nodes must be topologically ordered n1 through nN")
known: set[str] = set()
for node in self.nodes:
if node.node_id in node.dependencies:
raise ValueError(f"{node.node_id} cannot depend on itself")
unknown = set(node.dependencies) - known
if unknown:
raise ValueError(
f"{node.node_id} has non-prior dependencies {sorted(unknown)}"
)
known.add(node.node_id)
if self.terminal_node_id not in known:
raise ValueError("terminal node is not present in the DAG")
by_id = {node.node_id: node for node in self.nodes}
ancestors: set[str] = set()
pending = [self.terminal_node_id]
while pending:
node_id = pending.pop()
if node_id in ancestors:
continue
ancestors.add(node_id)
pending.extend(by_id[node_id].dependencies)
if ancestors != known:
raise ValueError("every proof node must contribute to the terminal node")
return self
class MethodNode(StrictModel):
node_id: str
method_label: str
@model_validator(mode="after")
def validate_content(self) -> "MethodNode":
if not self.method_label.strip():
raise ValueError("method label must be non-empty")
return self
class MethodPlan(StrictModel):
nodes: list[MethodNode] = Field(min_length=1)
def validate_against(self, dag: ProofDAG) -> "MethodPlan":
if [node.node_id for node in self.nodes] != dag.node_ids():
raise ValueError("method-plan IDs must exactly match proof-DAG IDs")
return self
class ReplacementChange(StrictModel):
slot_id: str
source_node_id: str
description: str
original_value: str
replacement_value: str
guard_condition: str
guard_justification: str
@model_validator(mode="after")
def validate_change(self) -> "ReplacementChange":
text_fields = [
self.slot_id,
self.source_node_id,
self.description,
self.original_value,
self.replacement_value,
self.guard_condition,
self.guard_justification,
]
if any(not value.strip() for value in text_fields):
raise ValueError("replacement fields must be non-empty")
if self.original_value.strip() == self.replacement_value.strip():
raise ValueError("replacement must differ from the original value")
return self
class ReplacementPlan(StrictModel):
changes: list[ReplacementChange] = Field(min_length=1)
closure_statement: str
@model_validator(mode="after")
def validate_content(self) -> "ReplacementPlan":
slot_ids = [change.slot_id for change in self.changes]
if len(slot_ids) != len(set(slot_ids)):
raise ValueError("replacement slot IDs must be unique")
if not self.closure_statement.strip():
raise ValueError("replacement plan must state its closure guarantee")
return self
def validate_against(self, dag: ProofDAG) -> "ReplacementPlan":
known = set(dag.node_ids())
unknown = {
change.source_node_id
for change in self.changes
if change.source_node_id not in known
}
if unknown:
raise ValueError(f"replacement plan references unknown nodes {sorted(unknown)}")
return self
class DiffusedProofNode(StrictModel):
node_id: str
dependencies: list[str] = Field(default_factory=list)
method_label: str
instantiated_claim: str
justification: str
@model_validator(mode="after")
def validate_content(self) -> "DiffusedProofNode":
if not self.method_label.strip():
raise ValueError("diffused method label must be non-empty")
if not self.instantiated_claim.strip() or not self.justification.strip():
raise ValueError("diffused claim and justification must be non-empty")
return self
class DiffusedProof(StrictModel):
nodes: list[DiffusedProofNode] = Field(min_length=1)
terminal_node_id: str
terminal_answer: str
def validate_against(
self,
dag: ProofDAG,
method_plan: MethodPlan,
) -> "DiffusedProof":
method_plan.validate_against(dag)
if [node.node_id for node in self.nodes] != dag.node_ids():
raise ValueError("diffused proof must contain exactly one row per DAG node")
dag_by_id = {node.node_id: node for node in dag.nodes}
methods = {node.node_id: node.method_label for node in method_plan.nodes}
for node in self.nodes:
if node.dependencies != dag_by_id[node.node_id].dependencies:
raise ValueError(
f"{node.node_id} dependencies changed during DAG diffusion"
)
if node.method_label != methods[node.node_id]:
raise ValueError(
f"{node.node_id} method label changed during DAG diffusion"
)
if self.terminal_node_id != dag.terminal_node_id:
raise ValueError("diffused terminal node must match the source DAG")
if not self.terminal_answer.strip():
raise ValueError("diffused proof must expose a terminal answer")
return self
class RenderedVariant(StrictModel):
question: str
solution: str
node_order: list[str] = Field(min_length=1)
terminal_answer: str
@model_validator(mode="after")
def validate_content(self) -> "RenderedVariant":
if not self.question.strip() or not self.solution.strip():
raise ValueError("rendered question and solution must be non-empty")
if not self.terminal_answer.strip():
raise ValueError("rendered terminal answer must be non-empty")
return self
def validate_against(
self,
dag: ProofDAG,
diffused_proof: DiffusedProof,
) -> "RenderedVariant":
if self.node_order != dag.node_ids():
raise ValueError("rendered solution must cite every proof node in order")
missing_markers = [
node_id
for node_id in self.node_order
if f"[{node_id}]" not in self.solution
]
if missing_markers:
raise ValueError(
f"rendered solution is missing node markers {missing_markers}"
)
if self.terminal_answer.strip() != diffused_proof.terminal_answer.strip():
raise ValueError("rendered terminal answer differs from diffused proof")
return self
class CandidateBundle(StrictModel):
replacement_plan: ReplacementPlan
diffused_proof: DiffusedProof
variant: RenderedVariant
class JudgeVerdict(StrictModel):
verdict: Literal["accept", "reject"]
step_by_step_check: str
replacement_check: str
blocking_issues: str = ""
patch_suggestion: str = ""
@field_validator(
"step_by_step_check",
"replacement_check",
"blocking_issues",
"patch_suggestion",
mode="before",
)
@classmethod
def normalize_text_fields(cls, value: Any) -> str:
if value is None:
return ""
if isinstance(value, str):
return value
return json.dumps(value, ensure_ascii=False, sort_keys=True)
@field_validator("blocking_issues", "patch_suggestion", mode="after")
@classmethod
def normalize_absence_sentinels(cls, value: str) -> str:
normalized = value.strip().lower().rstrip(".")
if normalized in {
"",
"none",
"none detected",
"n/a",
"no issues",
"no blocking issues",
}:
return ""
return value
@model_validator(mode="after")
def validate_verdict(self) -> "JudgeVerdict":
if self.verdict == "accept" and self.blocking_issues.strip():
raise ValueError("accept verdict cannot contain blocking issues")
if self.verdict == "reject" and not self.blocking_issues.strip():
raise ValueError("reject verdict must identify a blocking issue")
return self
def validate_coverage(
self,
dag: ProofDAG,
replacement_plan: ReplacementPlan,
) -> "JudgeVerdict":
missing_nodes = [
node_id
for node_id in dag.node_ids()
if re.search(
rf"(?<![A-Za-z0-9_]){re.escape(node_id)}(?![A-Za-z0-9_])",
self.step_by_step_check,
)
is None
]
missing_slots = [
change.slot_id
for change in replacement_plan.changes
if re.search(
rf"(?<![A-Za-z0-9_]){re.escape(change.slot_id)}(?![A-Za-z0-9_])",
self.replacement_check,
)
is None
]
if missing_nodes or missing_slots:
raise ValueError(
"judge coverage incomplete: "
f"nodes={missing_nodes}, slots={missing_slots}"
)
return self
class VerificationIteration(StrictModel):
iteration: int
bundle_sha256: str
candidate_sha256: str
verdicts: list[JudgeVerdict]
unanimous: bool
pass_streak_after: int
repaired_from_previous: bool = False
class KernelRunResult(StrictModel):
item_id: str
status: Literal["accepted", "rejected"]
proof_dag: ProofDAG
method_plan: MethodPlan
accepted_replacement_plan: ReplacementPlan | None = None
accepted_diffused_proof: DiffusedProof | None = None
accepted_candidate: RenderedVariant | None = None
iterations: list[VerificationIteration]
rejection_reason: str = ""
accepted_candidate_sha256: str | None = None
accepted_bundle_sha256: str | None = None
schema_version: str = f"{SCHEMA_VERSION}-literal-five-stage"
@model_validator(mode="after")
def validate_terminal_state(self) -> "KernelRunResult":
if self.status == "accepted":
required = [
self.accepted_replacement_plan,
self.accepted_diffused_proof,
self.accepted_candidate,
self.accepted_candidate_sha256,
self.accepted_bundle_sha256,
]
if any(value is None for value in required):
raise ValueError("accepted run must include complete stage provenance")
elif not self.rejection_reason:
raise ValueError("rejected run must state a reason")
return self
|