From cd3b1bc92198f74b430b8fbd99c1ede1deb22988 Mon Sep 17 00:00:00 2001 From: mrwulf Date: Thu, 30 Jul 2026 18:24:31 +0200 Subject: [PATCH] cockpit: the estate page now MEASURES instead of asserting MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit The /estate page was hand-written prose inside estateview.py: 32 hard-coded fact arrays and zero places reading live data, last edited 2026-07-22. It cannot go stale by accident — it can only go stale, because nothing connected it to the repositories it describes. For eight days it told the operator: · SLH-DSA "campaign in progress", "check.sh exits non-green by design" — while it had 11 proven certificates, a green button, an 18-attack self-test and an outside reviewer's attest-with-conditions; · ed25519 "16 reviewed certificates" — while they had 31 bound certificates and 3022 inventoried constants; · nothing at all about five audit phases and five self-tests per repo, none of which existed on the day the page was last touched. Those four claims are corrected. More importantly the page now carries a MEASURED panel rendered from formal-verification-control's tools/estate-progress.py, which derives every figure from the repositories at generation time. The panel states three things a reader would otherwise have to assume: · WHEN it was measured, and by what; · WHETHER the repositories have moved since — the snapshot records the HEADs it was taken against, and the panel compares them live, naming any repo that has moved rather than quietly showing old numbers as current; · WHICH PART OF THE PAGE IS MEASURED AT ALL. Everything above the panel is labelled, in the page itself, as hand-written prose that can be out of date. That label is the honest part: the map is still prose, and a reader should know which half is which. If the snapshot is absent the panel says NOT MEASURED in words and prints the command to produce one. It never renders nothing, and never falls back to prose — a blank space and a confident-looking stale figure are the same failure, and the second is worse. Two numbers, never one, per PROGRESS-METRIC.md: a single figure is what let the old metric report 100% for work nobody had attacked. All three paths tested: current, moved-since, and absent. 145/145 tests pass, including the sync test guarding drift between this page and ESTATE.md. Co-Authored-By: Claude Opus 4.8 --- src/pacta/estateview.py | 144 ++++++++++++++++++++++++++++++++++++++-- src/pacta/walletui.py | 7 +- 2 files changed, 143 insertions(+), 8 deletions(-) diff --git a/src/pacta/estateview.py b/src/pacta/estateview.py index 1967d79..dbeb664 100644 --- a/src/pacta/estateview.py +++ b/src/pacta/estateview.py @@ -173,7 +173,7 @@ ESTATE_HTML = r'''LTL estate map — repos, services, loops

pasta-pallas-verified

field layer proven · curve layer pending
not attested

fips205-slhdsa-verified

SLH-DSA-SHA2-128s verify path · skeleton — 0 certificates
-
campaign in progressnot attested
+
11 certs · reviewer attest-with-conditionsnot attested

ltl-accumulator-verified

61 certs · proofs about the log's own accumulator model
attested · entry 13frozen 172a1d0loop 2
@@ -249,7 +249,7 @@ const RUNTIME = { dalek:"static repo — proofs replay on demand", anza:"static repo — proofs replay on demand", risc0:"static repo — proofs replay on demand", bet:"static repo — proofs replay on demand", pasta:"static repo — open work, run manually", corpus:"frozen repo — replay on demand", - fips:"static repo — no process; campaign sessions are episodic operator-machine runs under lean-guard; check.sh exits non-green by design", + fips:"static repo — no process; campaign sessions are episodic operator-machine runs under lean-guard; check.sh GREEN with an 18-attack self-test", provider:"SPLIT: the write side (check/append/publish) runs ON DEMAND on the operator machine, only during a ceremony; the read-only web face runs ALWAYS ON in the droplet container", signer:"on demand — invoked only while signing during a ceremony; key offline otherwise", conslib:"library — runs inside whichever consumer invokes it", @@ -276,10 +276,10 @@ const DOSSIER = { srcBet:{lane:"Upstream inputs",mut:"frozen",facts:["Pinned clone of the Betrusted dalek fork.","xous-core and litex-boards sit alongside as platform context.","Input to extraction; never modified."]}, srcPasta:{lane:"Upstream inputs",mut:"frozen",facts:["Pinned clone of the Pasta curves crate.","Feeds pasta-pallas-verified; never modified."]}, srcFips205:{lane:"Upstream inputs",mut:"frozen",facts:["Verbatim snapshot of integritychain/fips205 — pure-Rust FIPS 205 / SLH-DSA (zero unsafe, no_std, const-generic).","Pinned at upstream 30bac08 (2025-09-01); snapshot head 5dca0db — the single deviation from verbatim is stripping upstream CI workflows, documented in that commit.","Aeneas-compat patches land HERE as transparent, individually-justified commits; nothing is proposed upstream (no affiliation)."]}, - dalek:{lane:"Verified subjects",mut:"frozen",facts:["16 reviewed certificates: field, group law, scalars, signature apex (T1–T4).","Attested in all three log generations; current leaf 8.","LOOP 1 anchor: the dogfood signer binary is built from this source — the log's heads are signed by code whose proofs are inside the log.","Attestation pins a commit; the branch only moves for docs."]}, - anza:{lane:"Verified subjects",mut:"frozen",facts:["16 reviewed certificates; current leaf 9.","Same proof pyramid as dalek, rebuilt for the fork's code structure."]}, - risc0:{lane:"Verified subjects",mut:"frozen",facts:["16 reviewed certificates; current leaf 10.","Differs from Betrusted's corpus by 27 changed proof lines (the paper's portability datum)."]}, - bet:{lane:"Verified subjects",mut:"frozen",facts:["16 reviewed certificates; current leaf 11."]}, + dalek:{lane:"Verified subjects",mut:"frozen",facts:["31 bound certificates (field, group law, scalars, signature apex T1–T4) and 3022 inventoried constants; 16 of the certificates are the curated attested subset in the log.","Attested in all three log generations; current leaf 8.","LOOP 1 anchor: the dogfood signer binary is built from this source — the log's heads are signed by code whose proofs are inside the log.","Attestation pins a commit; the branch only moves for docs."]}, + anza:{lane:"Verified subjects",mut:"frozen",facts:["31 bound certificates, 3022 inventoried constants; attested subset is 16; current leaf 9.","Same proof pyramid as dalek, rebuilt for the fork's code structure."]}, + risc0:{lane:"Verified subjects",mut:"frozen",facts:["31 bound certificates, 3022 inventoried constants; attested subset is 16; current leaf 10.","Differs from Betrusted's corpus by 27 changed proof lines (the paper's portability datum)."]}, + bet:{lane:"Verified subjects",mut:"frozen",facts:["31 bound certificates, 3022 inventoried constants; attested subset is 16; current leaf 11."]}, pasta:{lane:"Verified subjects",mut:"free",facts:["Field layer proven from own extraction; curve layer (group law + scalar mul) remains open work.","NOT attested — the log carries only the four Ed25519 forks + the corpus."]}, fips:{lane:"Verified subjects",mut:"free",facts:["CAMPAIGN IN PROGRESS — ZERO certificates: verification/check.sh exits non-green and says so; that script is the only source of the word «proven» for this repo.","Scope: the FIPS 205 verify path only (slh_verify → fors / hypertree → xmss → wots → chain), parameter set SLH-DSA-SHA2-128s; keygen and signing are trusted base, exactly as ed25519 signing was.","The six SHA-2 hash oracles are opaque external models (TRUSTED-BASE.md), kept outside every future certificate's dependency cone.","Gate-0 (2026-07-22): Charon clean; Aeneas translated the whole cone with exactly one obstruction class (the Hashers fn-pointer struct) — campaign phase 1 is the compat patch in fips205-source.","NOT attested — the log carries nothing from this campaign yet."]}, corpus:{lane:"Verified subjects",mut:"frozen",facts:["61 certificates over one boundary axiom (LTLAcc.sha256); 222-constant environment inventory; 15-gap honest ledger.","Mechanizes the archived report's §6: extractors, consistency binding, per-step pin safety.","LOOP 2 anchor: attested INTO the log as entry 13 — the log carries kernel-checked proofs about its own accumulator model.","Frozen at 172a1d0 (the attested commit); doc-only commits may move the branch.","Docs carry numbering notes: paper references are v0.2 numbering."]}, @@ -418,3 +418,135 @@ window.addEventListener("resize",()=>requestAnimationFrame(draw)); requestAnimationFrame(draw);setTimeout(draw,150); ''' + + +# ───────────────────────────────────────────────────────────────────────────── +# MEASURED PROGRESS PANEL +# +# Everything above this line is hand-written prose. That is why, between +# 2026-07-22 and 2026-07-30, this page told the operator that the SLH-DSA +# campaign was "in progress" with a button "non-green by design" while it had +# eleven proven certificates and a green button, and that the ed25519 forks had +# "16 reviewed certificates" while they had 31 bound and 3022 inventoried. A +# page that asserts cannot notice it has gone out of date; only a page that +# measures can. +# +# So this panel renders ONLY what formal-verification-control's +# tools/estate-progress.py derived from the repositories, and it states three +# things a reader would otherwise have to assume: when it was measured, whether +# the repositories have moved since, and which parts of this page are measured +# at all. If there is no snapshot it renders that fact loudly rather than +# quietly rendering nothing. +# ───────────────────────────────────────────────────────────────────────────── + +import json as _json +import os as _os +import subprocess as _sp + +PROGRESS_JSON = _os.environ.get( + "PACTA_PROGRESS_JSON", + "/home/oho/GitClone/FormalVerification/formal-verification-control/ESTATE-PROGRESS.json") +ESTATE_ROOT = _os.environ.get( + "ESTATE_ROOT", "/home/oho/GitClone/Claude/FormalVerification") + + +def _live_head(repo: str): + try: + r = _sp.run(["git", "-C", _os.path.join(ESTATE_ROOT, repo), + "rev-parse", "--short", "HEAD"], + capture_output=True, text=True, timeout=5) + return r.stdout.strip() or None + except Exception: + return None + + +def _panel(cls: str, title: str, body: str) -> str: + return (f'

{title}

{body}
') + + +def progress_panel() -> str: + """The measured half of this page. Never falls back to prose.""" + style = """ +""" + + if not _os.path.exists(PROGRESS_JSON): + return style + _panel("bad", "Progress: NOT MEASURED", f""" +

No snapshot at {PROGRESS_JSON}, so this page is showing + you nothing rather than something stale. That is deliberate: + the previous version of this page displayed hand-typed claims that were + eight days out of date, and looked exactly as confident as this one.

+

To populate it: + formal-verification-control/tools/estate-progress.py --json

""") + + try: + d = _json.load(open(PROGRESS_JSON)) + except Exception as e: + return style + _panel("bad", "Progress: SNAPSHOT UNREADABLE", f"

{e}

") + + moved = [] + for repo, recorded in (d.get("repo_heads") or {}).items(): + live = _live_head(repo) + if live and recorded and live != recorded: + moved.append((repo, recorded, live)) + + rows = [] + for c in d["campaigns"]: + ax = c["axes"] + for axis, label in (("proof", "act one · proof"), ("attestation", "act two · attestation")): + if axis not in ax: + continue + a = ax[axis] + unm = (f' ' + f'+{a["unmeasurable"]} unmeasurable' if a["unmeasurable"] else "") + rows.append( + f'{c["title"]}{label}' + f'{a["earned"]} / {a["identified"]}' + f'
' + f'{a["pct"]}%{unm}' + f'{c["reproduction_note"]}') + + t = d["totals"] + head = (f'

act one — proof {t["proof"]["pct"]}% · ' + f'act two — attestation {t["attestation"]["pct"]}% ' + f'(two numbers, never one: a single figure is what let the ' + f'old metric report 100% for work nobody had attacked)

') + + table = ('' + '' + + "".join(rows) + "
campaignaxisband-pointsverifiedreproduction
") + + contra = "" + if d.get("contradictions"): + items = "".join(f"
  • {c['id']}: {c['detail']}
    • " + for c in d["contradictions"]) + contra = (f'

    The ledger contradicts the repositories. ' + f'These numbers are not trustworthy until this list is empty:

    ') + + note = (f'

    Measured {d["generated_at"]} by {d["generator"]}, ' + f'from the repositories as they were at that moment. Nothing here is cached or ' + f'carried forward. Everything on this page ABOVE this panel is ' + f'hand-written prose and can be out of date; only this panel is derived.

    ') + + if moved: + rowsm = "".join(f"
  • {r}: measured at {a}, " + f"now {b}
    • " for r, a, b in moved) + return style + _panel( + "warn", "Progress: MEASURED, BUT THE REPOSITORIES HAVE MOVED SINCE", + f'

    {len(moved)} repository(ies) changed after this snapshot, so the figures ' + f'below describe an earlier state:

    {head}{table}{contra}{note}' + f'

    Re-run tools/estate-progress.py --json to refresh.

    ') + + return style + _panel("", "Progress — measured, not asserted", + head + table + contra + note) diff --git a/src/pacta/walletui.py b/src/pacta/walletui.py index 8a60c3a..f126d8d 100644 --- a/src/pacta/walletui.py +++ b/src/pacta/walletui.py @@ -1070,8 +1070,11 @@ def make_handler(wallet_dir: Path): elif route == "/manual": page("lab manual", "/manual", render_manual()) elif route == "/estate": - from .estateview import ESTATE_HTML - self._send(ESTATE_HTML + _ESTATE_BACK_CHIP) + from .estateview import ESTATE_HTML, progress_panel + # The map is hand-written prose; the panel is derived from the + # repositories. Serving them together, in that order, is what + # stops a reader mistaking the first for the second. + self._send(ESTATE_HTML + progress_panel() + _ESTATE_BACK_CHIP) elif route.startswith("/station/"): station_id = route.removeprefix("/station/") station = STATION_BY_ID.get(station_id)