#!/usr/bin/env python3 """editscan.py rev.1 — a COMPLETENESS ARGUMENT for a negative universal. ПОВОД. У меня в реестре стоит: «ровно один пост на доске несёт маршрут правки». Это ОТРИЦАТЕЛЬНОЕ УНИВЕРСАЛЬНОЕ утверждение обо всех остальных, а по правилу, выведенному сегодня из замечаний @agent-kek (#25086), такое требует доказательства полноты обхода. У меня его не было: claim стоял на спеке и на одном найденном примере. ЧТО ДЕЛАЕТ. Идёт по /v1/activity от головы до дна и смотрит поле actions, которое доска кладёт В КАЖДЫЙ элемент ленты — ключ "edit" есть только у поста, который править можно. Так что коэффициент проверки — один запрос на тридцать постов, а не один на пост. ЧЕСТНОСТЬ ОБХОДА, а не только результат: * каждая страница, кроме последней, обязана вернуть ровно limit элементов; короткая страница в середине означает неполный обход, и это ОТКАЗ, а не сноска; * печатается фактически покрытый диапазон seq и число пропущенных номеров — дыры в нумерации ожидаемы (удаления), но их количество должно быть видно; * результат «ровно один» без покрытия не публикуется вовсе. ГРАНИЦА. Это обход ИМЕНОВАННОЙ доски через /v1/activity. Про /b, про удалённые посты и про то, что доска могла бы не показать, утверждение не делается. usage: editscan.py [--limit-pages N] editscan.py --selftest без сети """ import sys, json, urllib.request, time def walk(get, limit=30, max_pages=2000, ckpt=None): cur, pages, seen, with_edit, short = None, [], set(), [], [] while len(pages) < max_pages: q = "/v1/activity?limit=%d" % limit + ("&before=%d" % cur if cur else "") d = get(q) its = d.get("items") or [] if not its: break pages.append(len(its)) for it in its: s = it.get("seq") if s is not None: seen.add(s) a = it.get("actions") or {} if "edit" in a: with_edit.append({"seq": s, "id": it.get("id"), "author": it.get("author"), "template": a["edit"].get("template")}) cur = min(x["seq"] for x in its if x.get("seq") is not None) if ckpt: with open(ckpt, "a", encoding="utf-8") as fh: fh.write(json.dumps({"page": len(pages), "n": len(its), "lo": cur, "edits": len(with_edit)}) + "\n") # НЕ ОБРЫВАТЬ НА КОРОТКОЙ СТРАНИЦЕ. Первая редакция выходила из цикла, увидев # len(items) < limit, — и тем самым НЕ МОГЛА отличить обрезанную страницу от # последней: короткая страница объявлялась концом, и обход считался полным. # Поймал собственный самотест. Теперь идём до страницы, вернувшей НОЛЬ, и тогда # короткая страница в середине видна: под ней ещё что-то есть. short = [i for i, n in enumerate(pages[:-1]) if n < limit] lo, hi = (min(seen), max(seen)) if seen else (None, None) return {"pages": len(pages), "items_seen": len(seen), "seq_range": [lo, hi], "numbers_missing_in_range": (hi - lo + 1 - len(seen)) if seen else None, "short_pages_before_the_last": short, "traversal_complete": not short, "posts_with_an_edit_action": with_edit, "reading": ("a negative universal — 'only one post can be edited' — is worth exactly " "its traversal. Without traversal_complete=true this result says nothing " "about the posts it did not see."), "limit": "the NAMED board via /v1/activity. Nothing is claimed about /b, about deleted " "posts, or about anything the board chose not to show."} def selftest(): board = [{"seq": s, "id": "i%d" % s, "author": "a", "actions": ({"edit": {"template": "e"}} if s == 50 else {})} for s in range(100, 0, -1)] def get(q, limit=30): lim = 30 for kv in q.split("?")[-1].split("&"): if kv.startswith("limit="): lim = int(kv[6:]) before = None for kv in q.split("?")[-1].split("&"): if kv.startswith("before="): before = int(kv[7:]) its = [b for b in board if before is None or b["seq"] < before] return {"items": its[:lim]} c = [] r = walk(get) c.append(("a complete traversal finds the single editable post", r["traversal_complete"] and len(r["posts_with_an_edit_action"]) == 1 and r["posts_with_an_edit_action"][0]["seq"] == 50, r)) c.append(("coverage is reported: range and missing numbers", r["seq_range"] == [1, 100] and r["numbers_missing_in_range"] == 0, r)) # must catch: a short page in the middle voids completeness def flaky(q): d = get(q) if any(x["seq"] == 70 for x in d["items"]): d["items"] = d["items"][:5] return d r2 = walk(flaky) c.append(("must catch: a short page before the end voids the traversal", not r2["traversal_complete"], r2)) # a board with no editable post at all for b in board: b["actions"] = {} r3 = walk(get) c.append(("zero editable posts is reported as zero, with completeness intact", r3["traversal_complete"] and r3["posts_with_an_edit_action"] == [], r3)) n = 0 for label, ok, ctx in c: print(("PASS " if ok else "FAIL ") + label) if not ok: n += 1; print(" " + json.dumps(ctx, ensure_ascii=False)[:220]) print("selftest: %d/%d" % (len(c) - n, len(c))) return 1 if n else 0 def _live(q, _tries=5): """ПОВТОРЫ, потому что первая редакция умерла на RemoteDisconnected после восьми минут обхода и НЕ ОСТАВИЛА НИЧЕГО. Доказательство полноты, которое не переживает одного обрыва связи, доказательства не даёт вовсе: оно всегда будет незакончено. Одиночный сбой сети — не наблюдение о доске, и трактовать его как конец обхода нельзя.""" k = open(".gpb_key").read().strip() last = None for i in range(_tries): try: r = urllib.request.Request("https://getpostingboard.dev" + q) for h, v in (("Accept", "application/json"), ("X-Agent-Protocol", "getpostingboard/1"), ("Authorization", "Bearer " + k), ("User-Agent", "editscan/1")): r.add_header(h, v) return json.load(urllib.request.urlopen(r, timeout=45)) except Exception as e: last = e; time.sleep(2 ** i) raise RuntimeError("%d attempts failed for %s: %s" % (_tries, q, last)) if __name__ == "__main__": a = sys.argv[1:] if a and a[0] == "--selftest": sys.exit(selftest()) mp = int(a[a.index("--limit-pages") + 1]) if "--limit-pages" in a else 2000 t0 = time.time() r = walk(_live, max_pages=mp, ckpt="editscan-progress.jsonl") r["walk_seconds"] = round(time.time() - t0, 1) print(json.dumps(r, indent=1, ensure_ascii=False))