betterwithage commited on
Commit
8319d38
·
verified ·
1 Parent(s): 22810cf

chore(sync): mirror backend .py + Dockerfile to Space (hf-sync-backend)

Browse files

Automated backend sync from szl-holdings/a11oy main via hf-sync-backend.
Updated (differed from the Space): Dockerfile, serve.py, szl_bounties.py

Keeps the Space-built backend (serve.py + the Dockerfile-COPY'd .py
modules) identical to GitHub main so the Space never rebuilds from a
stale backend and new endpoints don't 404 there.

Files changed (3) hide show
  1. Dockerfile +6 -0
  2. serve.py +14 -0
  3. szl_bounties.py +418 -0
Dockerfile CHANGED
@@ -538,6 +538,12 @@ COPY szl_readiness.py ./szl_readiness.py
538
  # liveness probes, 0 fabricated org values). serve.py imports this try/except-guarded;
539
  # without this per-file COPY the import fails and /api/a11oy/v1/contracting 404s.
540
  COPY szl_contracting.py ./szl_contracting.py
 
 
 
 
 
 
541
 
542
  CMD ["python", "serve.py"]
543
 
 
538
  # liveness probes, 0 fabricated org values). serve.py imports this try/except-guarded;
539
  # without this per-file COPY the import fails and /api/a11oy/v1/contracting 404s.
540
  COPY szl_contracting.py ./szl_contracting.py
541
+ # ADDITIVE (Open-Problem Bounty Board, bounties-tab-patch): stdlib-only bounty module
542
+ # + the canonical bounty YAMLs (single source of truth, copied byte-identical from
543
+ # szl-holdings/lutar-lean). Per-file/dir COPY (this Dockerfile never uses `COPY . .`)
544
+ # -- without these the import fails and /api/a11oy/v1/bounties 404s.
545
+ COPY szl_bounties.py ./szl_bounties.py
546
+ COPY bounties/ ./bounties/
547
 
548
  CMD ["python", "serve.py"]
549
 
serve.py CHANGED
@@ -123,6 +123,20 @@ try:
123
  except Exception as _szl_rd_e: # pragma: no cover
124
  print(f"[a11oy] Operational Readiness NOT registered: {_szl_rd_e!r}", file=__import__("sys").stderr)
125
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
126
  # ── Readiness tab-matrix endpoint (readiness-harness) — a11oy console contract.
127
  # Kept HERE in serve.py (a11oy-only) rather than in the shared szl_readiness.py so
128
  # that module stays byte-identical with killinchu (shared-source drift guard). Serves
 
123
  except Exception as _szl_rd_e: # pragma: no cover
124
  print(f"[a11oy] Operational Readiness NOT registered: {_szl_rd_e!r}", file=__import__("sys").stderr)
125
 
126
+ # ── Open-Problem Bounty Board (bounties-tab-patch) — OPEN proof bounties
127
+ # (Conjecture 1 Λ-aggregator uniqueness, Conjecture 2 Khipu BFT safety) rendered
128
+ # from bounties/*.yaml (single source of truth, copied byte-identical from
129
+ # szl-holdings/lutar-lean, kept in lockstep by bounties-drift.yml). Public recruiting
130
+ # funnel for proofs; renders ONLY status==OPEN, reward is the literal "founder-set",
131
+ # Λ stays "Conjecture 1" (never a theorem). Additive, try/except-guarded, registered
132
+ # EARLY (before the SPA catch-all). Pure stdlib (no PyYAML).
133
+ try:
134
+ import szl_bounties as _szl_bounties
135
+ _szl_bounties.register(app, ns="a11oy")
136
+ print("[a11oy] Open-Problem Bounty Board registered: /api/a11oy/v1/bounties", file=__import__("sys").stderr)
137
+ except Exception as _szl_bn_e: # pragma: no cover
138
+ print(f"[a11oy] Open-Problem Bounty Board NOT registered: {_szl_bn_e!r}", file=__import__("sys").stderr)
139
+
140
  # ── Readiness tab-matrix endpoint (readiness-harness) — a11oy console contract.
141
  # Kept HERE in serve.py (a11oy-only) rather than in the shared szl_readiness.py so
142
  # that module stays byte-identical with killinchu (shared-source drift guard). Serves
szl_bounties.py ADDED
@@ -0,0 +1,418 @@
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
1
+ """
2
+ szl_bounties.py — Open-Problem Bounty Board layer (a11oy console tab)
3
+ ====================================================================
4
+
5
+ Renders the **genuinely OPEN** problem bounties — Conjecture 1 (Λ-aggregator
6
+ unconditional uniqueness) and Conjecture 2 (Khipu Byzantine quorum safety) —
7
+ on a public surface (the a11oy console), turning the board into a recruiting
8
+ funnel for proofs that links straight to the lambda-bounty intake webhook.
9
+
10
+ Single source of truth
11
+ ----------------------
12
+ The page is *generated from* the canonical YAML in ``bounties/*.yaml`` (copied
13
+ byte-identical from ``szl-holdings/lutar-lean`` and kept in lockstep by the
14
+ ``bounties-drift.yml`` CI guard). Nothing here is hand-authored bounty prose,
15
+ so the rendered page cannot drift from the kernel repo. Only bounties whose
16
+ ``status`` is ``OPEN`` are surfaced.
17
+
18
+ Honesty doctrine (v11)
19
+ ----------------------
20
+ Λ unconditional uniqueness is **Conjecture 1 — NOT a theorem** (machine-checked
21
+ FALSE under the bare axioms via the maxAgg/min counterexample). Khipu
22
+ unconditional BFT safety is **Conjecture 2**. The reward is always the literal
23
+ label **"founder-set"** — this board never invents a figure. The ``honesty``
24
+ line from each YAML is surfaced verbatim, and any numeric reward value is
25
+ defensively coerced back to ``founder-set``.
26
+
27
+ This module is **stdlib-only** (no PyYAML in the a11oy image): it ships a small,
28
+ faithful YAML-subset reader for exactly the constructs the bounty files use
29
+ (top-level scalars, ``|``/``>`` block scalars, nested mappings, scalar lists,
30
+ and lists of mappings).
31
+
32
+ Pattern mirrors szl_readiness.py / szl_contracting.py::
33
+
34
+ import szl_bounties
35
+ szl_bounties.register(app, ns="a11oy")
36
+
37
+ Endpoints (per namespace ns)::
38
+
39
+ GET /api/{ns}/v1/bounties
40
+ -> { layer, honest, doctrine, source, board, count, bounties:[...] }
41
+ one entry per OPEN bounty with statement, the gap, acceptance
42
+ criteria, reward label ("founder-set"), submission/claim links,
43
+ and the verbatim honesty line.
44
+ GET /api/{ns}/v1/bounties/{bounty_id}
45
+ -> a single OPEN bounty (404 if unknown / not OPEN).
46
+ """
47
+ from __future__ import annotations
48
+
49
+ import os
50
+ import re
51
+ import threading
52
+ from typing import Any, Dict, List, Optional
53
+
54
+ _HONEST = (
55
+ "These are the genuinely OPEN problems — honest open conjectures under public "
56
+ "axiom audit, NOT theorems. \u039b unconditional uniqueness is Conjecture 1 "
57
+ "(machine-checked FALSE under the bare axioms); unconditional Khipu BFT safety "
58
+ "is Conjecture 2. A bounty clears ONLY when the kernel verifies the proof (REAL): "
59
+ "kernel-checked, zero `sorry`, in-policy axioms. The reward is founder-set; this "
60
+ "board never invents a figure."
61
+ )
62
+ _DOCTRINE = "v11"
63
+ _SOURCE = "szl-holdings/lutar-lean — bounties/*.yaml (single source of truth)"
64
+ _BOARD_URL = "https://github.com/szl-holdings/lutar-lean/tree/main/bounties"
65
+ _DOCS_URL = "https://github.com/szl-holdings/lutar-lean/blob/main/docs/bounties.md"
66
+
67
+ _LOCK = threading.Lock()
68
+ _CACHE: Optional[List[Dict[str, Any]]] = None
69
+
70
+
71
+ # ---------------------------------------------------------------------------
72
+ # Minimal, faithful YAML-subset reader (stdlib only).
73
+ # Handles exactly what the bounty files use; not a general YAML parser.
74
+ # ---------------------------------------------------------------------------
75
+ def _indent_of(line: str) -> int:
76
+ return len(line) - len(line.lstrip(" "))
77
+
78
+
79
+ def _first_sig(lines: List[str], i: int) -> int:
80
+ """Index of the next significant (non-blank, non-comment) line, or len."""
81
+ while i < len(lines):
82
+ s = lines[i].strip()
83
+ if s == "" or s.startswith("#"):
84
+ i += 1
85
+ continue
86
+ return i
87
+ return i
88
+
89
+
90
+ def _dequote(s: str) -> str:
91
+ s = s.strip()
92
+ if len(s) >= 2 and s[0] == s[-1] and s[0] in ("'", '"'):
93
+ inner = s[1:-1]
94
+ if s[0] == '"':
95
+ inner = (inner.replace('\\"', '"').replace("\\n", "\n")
96
+ .replace("\\t", "\t").replace("\\\\", "\\"))
97
+ else:
98
+ inner = inner.replace("''", "'")
99
+ return inner
100
+ return s
101
+
102
+
103
+ def _scalar(s: str) -> Any:
104
+ s = s.strip()
105
+ if s == "":
106
+ return ""
107
+ if s in ("null", "~", "Null", "NULL"):
108
+ return None
109
+ if s in ("true", "True", "TRUE"):
110
+ return True
111
+ if s in ("false", "False", "FALSE"):
112
+ return False
113
+ if re.fullmatch(r"-?\d+", s):
114
+ try:
115
+ return int(s)
116
+ except ValueError:
117
+ pass
118
+ return _dequote(s)
119
+
120
+
121
+ def _read_block_scalar(lines: List[str], i: int, parent_indent: int, style: str) -> Any:
122
+ """Read a `|` (literal) or `>` (folded) block scalar; return (text, next_i)."""
123
+ block: List[str] = []
124
+ base: Optional[int] = None
125
+ while i < len(lines):
126
+ line = lines[i]
127
+ if line.strip() == "":
128
+ block.append("")
129
+ i += 1
130
+ continue
131
+ ind = _indent_of(line)
132
+ if ind <= parent_indent:
133
+ break
134
+ if base is None:
135
+ base = ind
136
+ block.append(line[base:] if len(line) >= base else line.lstrip(" "))
137
+ i += 1
138
+ while block and block[-1] == "":
139
+ block.pop()
140
+ if style == "|":
141
+ text = ("\n".join(block) + "\n") if block else ""
142
+ return text, i
143
+ # folded ">": single newlines -> spaces; blank lines -> paragraph breaks
144
+ paras: List[str] = []
145
+ cur: List[str] = []
146
+ for ln in block:
147
+ if ln == "":
148
+ paras.append(" ".join(cur))
149
+ cur = []
150
+ else:
151
+ cur.append(ln.strip())
152
+ paras.append(" ".join(cur))
153
+ text = "\n".join(p for p in paras).strip("\n")
154
+ return (text + "\n") if text else "", i
155
+
156
+
157
+ _BLOCK_MARKERS = ("|", ">", "|-", ">-", "|+", ">+")
158
+
159
+
160
+ def _parse(lines: List[str], i: int, floor: int):
161
+ i = _first_sig(lines, i)
162
+ if i >= len(lines):
163
+ return None, i
164
+ line = lines[i]
165
+ ind = _indent_of(line)
166
+ if ind < floor:
167
+ return None, i
168
+ s = line.strip()
169
+ if s == "-" or s.startswith("- "):
170
+ return _parse_list(lines, i, ind)
171
+ return _parse_map(lines, i, ind)
172
+
173
+
174
+ def _parse_map(lines: List[str], i: int, indent: int):
175
+ node: Dict[str, Any] = {}
176
+ while i < len(lines):
177
+ i = _first_sig(lines, i)
178
+ if i >= len(lines):
179
+ break
180
+ line = lines[i]
181
+ ind = _indent_of(line)
182
+ if ind != indent:
183
+ break
184
+ s = line.strip()
185
+ m = re.match(r"^([^:]+):(.*)$", s)
186
+ if not m:
187
+ break
188
+ key = _dequote(m.group(1).strip())
189
+ rest = m.group(2).strip()
190
+ i += 1
191
+ if rest in _BLOCK_MARKERS:
192
+ node[key], i = _read_block_scalar(lines, i, indent, rest[0])
193
+ elif rest == "":
194
+ j = _first_sig(lines, i)
195
+ if j < len(lines) and _indent_of(lines[j]) > indent:
196
+ node[key], i = _parse(lines, i, indent + 1)
197
+ else:
198
+ node[key] = None
199
+ else:
200
+ node[key] = _scalar(rest)
201
+ return node, i
202
+
203
+
204
+ def _parse_list(lines: List[str], i: int, indent: int):
205
+ items: List[Any] = []
206
+ while i < len(lines):
207
+ j = _first_sig(lines, i)
208
+ if j >= len(lines):
209
+ i = j
210
+ break
211
+ line = lines[j]
212
+ ind = _indent_of(line)
213
+ s = line.strip()
214
+ if ind != indent or not (s == "-" or s.startswith("- ")):
215
+ i = j
216
+ break
217
+ rest = line[ind + 1:]
218
+ content_indent = ind + 1 + (len(rest) - len(rest.lstrip(" ")))
219
+ first = rest.strip()
220
+ block: List[str] = []
221
+ if first != "":
222
+ block.append(" " * content_indent + first)
223
+ k = j + 1
224
+ while k < len(lines):
225
+ ll = lines[k]
226
+ if ll.strip() == "" or ll.strip().startswith("#"):
227
+ block.append(ll)
228
+ k += 1
229
+ continue
230
+ if _indent_of(ll) < content_indent:
231
+ break
232
+ block.append(ll)
233
+ k += 1
234
+ if not block:
235
+ items.append(None)
236
+ else:
237
+ bs = block[0].strip()
238
+ if re.match(r"^[^:'\"]+:(\s|$)", bs):
239
+ val, _ = _parse_map(block, 0, content_indent)
240
+ items.append(val)
241
+ else:
242
+ items.append(_scalar(bs))
243
+ i = k
244
+ return items, i
245
+
246
+
247
+ def parse_yaml(text: str) -> Dict[str, Any]:
248
+ """Parse the YAML-subset used by the bounty files into a dict."""
249
+ lines = text.replace("\r\n", "\n").replace("\r", "\n").split("\n")
250
+ node, _ = _parse(lines, 0, 0)
251
+ return node if isinstance(node, dict) else {}
252
+
253
+
254
+ # ---------------------------------------------------------------------------
255
+ # Bounty loading + honest shaping
256
+ # ---------------------------------------------------------------------------
257
+ def _bounty_dir() -> str:
258
+ here = os.path.dirname(os.path.abspath(__file__))
259
+ for cand in (os.path.join(here, "bounties"), os.path.join(os.getcwd(), "bounties")):
260
+ if os.path.isdir(cand):
261
+ return cand
262
+ return os.path.join(here, "bounties")
263
+
264
+
265
+ def _reward_label(reward: Any) -> str:
266
+ """Always a non-numeric label. This board never invents a figure."""
267
+ if isinstance(reward, dict):
268
+ amt = reward.get("amount")
269
+ else:
270
+ amt = reward
271
+ label = str(amt).strip() if amt is not None else "founder-set"
272
+ if label == "" or re.search(r"\d", label):
273
+ return "founder-set"
274
+ return label
275
+
276
+
277
+ def _claim_links(b: Dict[str, Any]) -> Dict[str, Any]:
278
+ sub = b.get("submission") or {}
279
+ if not isinstance(sub, dict):
280
+ sub = {}
281
+ out: Dict[str, Any] = {
282
+ "intake_repo": sub.get("intake_repo"),
283
+ "pull_request": sub.get("pull_request"),
284
+ }
285
+ if sub.get("webhook"):
286
+ out["webhook"] = sub.get("webhook")
287
+ if sub.get("template"):
288
+ out["template"] = sub.get("template")
289
+ if sub.get("schema"):
290
+ out["schema"] = sub.get("schema")
291
+ return out
292
+
293
+
294
+ def _shape(b: Dict[str, Any]) -> Dict[str, Any]:
295
+ reward = b.get("reward") or {}
296
+ reward_note = reward.get("note") if isinstance(reward, dict) else None
297
+ reward_extras = reward.get("extras") if isinstance(reward, dict) else None
298
+ crit = []
299
+ for c in (b.get("acceptance_criteria") or []):
300
+ if isinstance(c, dict):
301
+ crit.append({"id": c.get("id"), "check": c.get("check")})
302
+ elif c is not None:
303
+ crit.append({"id": None, "check": str(c)})
304
+ verification = b.get("verification") or {}
305
+ target = b.get("target") or {}
306
+ return {
307
+ "id": b.get("id"),
308
+ "title": b.get("title"),
309
+ "status": b.get("status"),
310
+ "conjecture": b.get("conjecture"),
311
+ "formula": b.get("formula"),
312
+ "doctrine": b.get("doctrine") or _DOCTRINE,
313
+ "summary": (b.get("summary") or "").strip(),
314
+ "problem_statement": (b.get("problem_statement") or "").strip(),
315
+ "the_gap": (b.get("the_gap") or "").strip(),
316
+ "missing_assumption": b.get("missing_assumption"),
317
+ "already_proven_do_not_reclaim": (b.get("already_proven_do_not_reclaim") or "").strip() or None,
318
+ "target": {
319
+ "theorem_name": target.get("theorem_name"),
320
+ "file": target.get("file"),
321
+ "repo": target.get("repo"),
322
+ } if target else None,
323
+ "acceptance_criteria": crit,
324
+ "verification": {
325
+ "arbiter": verification.get("arbiter"),
326
+ "must_become_real": verification.get("must_become_real"),
327
+ "signal": verification.get("signal"),
328
+ } if verification else None,
329
+ "reward": {
330
+ "label": _reward_label(reward),
331
+ "note": (reward_note or "").strip() or None,
332
+ "extras": reward_extras if isinstance(reward_extras, list) else None,
333
+ },
334
+ "submission": _claim_links(b),
335
+ "references": b.get("references") if isinstance(b.get("references"), list) else None,
336
+ "honesty": (b.get("honesty") or "").strip(),
337
+ }
338
+
339
+
340
+ def _load(force: bool = False) -> List[Dict[str, Any]]:
341
+ global _CACHE
342
+ with _LOCK:
343
+ if _CACHE is not None and not force:
344
+ return _CACHE
345
+ out: List[Dict[str, Any]] = []
346
+ d = _bounty_dir()
347
+ try:
348
+ names = sorted(f for f in os.listdir(d)
349
+ if f.endswith((".yaml", ".yml")) and not f.startswith("."))
350
+ except OSError:
351
+ names = []
352
+ for name in names:
353
+ try:
354
+ with open(os.path.join(d, name), "r", encoding="utf-8") as fh:
355
+ parsed = parse_yaml(fh.read())
356
+ except Exception: # noqa: BLE001 (a malformed file must never crash the board)
357
+ continue
358
+ if not isinstance(parsed, dict) or not parsed.get("id"):
359
+ continue
360
+ parsed["_file"] = name
361
+ out.append(parsed)
362
+ _CACHE = out
363
+ return out
364
+
365
+
366
+ def _open_bounties() -> List[Dict[str, Any]]:
367
+ return [_shape(b) for b in _load()
368
+ if str(b.get("status", "")).strip().upper() == "OPEN"]
369
+
370
+
371
+ # ---------------------------------------------------------------------------
372
+ # Registration
373
+ # ---------------------------------------------------------------------------
374
+ def register(app, ns: str = "a11oy") -> None:
375
+ """Attach the OPEN-bounty board endpoints for namespace ns to a FastAPI app."""
376
+ try:
377
+ from fastapi.responses import JSONResponse
378
+ except Exception: # pragma: no cover
379
+ return
380
+
381
+ base = "/api/%s/v1/bounties" % ns
382
+
383
+ def _now_iso() -> str:
384
+ import datetime
385
+ return datetime.datetime.now(datetime.timezone.utc).strftime("%Y-%m-%dT%H:%M:%SZ")
386
+
387
+ @app.get(base)
388
+ async def _bounties_index(): # noqa: ANN202
389
+ bounties = _open_bounties()
390
+ return JSONResponse({
391
+ "layer": "%s open-problem bounty board" % ns,
392
+ "honest": _HONEST,
393
+ "doctrine": _DOCTRINE,
394
+ "source": _SOURCE,
395
+ "board": _BOARD_URL,
396
+ "docs": _DOCS_URL,
397
+ "count": len(bounties),
398
+ "bounties": bounties,
399
+ "checked_at": _now_iso(),
400
+ })
401
+
402
+ @app.get(base + "/{bounty_id}")
403
+ async def _bounty_one(bounty_id: str): # noqa: ANN202
404
+ for b in _open_bounties():
405
+ if b.get("id") == bounty_id:
406
+ return JSONResponse({
407
+ "layer": "%s open-problem bounty" % ns,
408
+ "honest": _HONEST,
409
+ "doctrine": _DOCTRINE,
410
+ "source": _SOURCE,
411
+ "bounty": b,
412
+ "checked_at": _now_iso(),
413
+ })
414
+ return JSONResponse(
415
+ {"error": "unknown or non-OPEN bounty", "bounty_id": bounty_id,
416
+ "open": [b.get("id") for b in _open_bounties()]},
417
+ status_code=404,
418
+ )