Dev B: add governance source files missing on Space (tau eval, IETF receipt view, Colang ROE policy, /governance page, Lean4Agent scaffold) — byte-identical to GitHub; fixes Dockerfile COPY cache-miss build error

lean4agent/README.md

@@ -0,0 +1,32 @@
+# Lean4Agent — a11oy workflow-invariant formalization (ROADMAP / EXPERIMENTAL)
+
+**Status: ROADMAP.** This directory is a *scaffold* that formalizes the safety
+invariants of the a11oy governed-agent workflow in [Lean 4](https://leanprover.github.io/).
+It is **not** a completed machine-checked verification yet. The UI and docs render
+these invariants as **"ROADMAP — statements formalized, proofs in progress"** and
+must never describe them as "verified" until `lake build` passes with **zero `sorry`**.
+
+Inspired by **Lean4Agent** (arXiv:2606.06523), which formalizes agent workflow
+invariants in Lean 4.
+
+## Files
+- `WorkflowInvariants.lean` — the irreducible governed-decision pipeline
+  (`gate → lambda → recommend → sign → replay`) and 5 safety invariants:
+  - **INV 1** `destructive_unapproved_denied` — **proved** (no `sorry`)
+  - **INV 2** `injection_always_denied` — **proved**
+  - **INV 3** `oversize_denied` — **proved**
+  - **INV 4** `canonical_pipeline_policy_first` — **ROADMAP** (`sorry`)
+  - **INV 5** `replay_is_deterministic` — **ROADMAP** (placeholder statement)
+
+These mirror the runtime enforcement points: the `_a11oy_arena_inspect` threat gate
+and the Colang ROE flows in `policy/colang/roe_core.co`.
+
+## Roadmap to "verified"
+1. Add `lakefile.lean` + pin a Lean toolchain (`lean-toolchain`).
+2. Discharge INV 4 and INV 5 (remove every `sorry`).
+3. Add a CI job that runs `lake build` and fails on any `sorry` / `axiom`.
+4. Emit a build manifest; the Eval/Policy tab then cites
+   "N/M a11oy workflow invariants machine-checked, as-of <date>".
+
+Until step 3 is green, the honest claim is: **3 of 5 invariant statements are
+proved in isolation; the full-pipeline and determinism theorems are roadmap.**

lean4agent/WorkflowInvariants.lean

@@ -0,0 +1,113 @@
+/-
+  WorkflowInvariants.lean — ROADMAP / EXPERIMENTAL scaffold (NOT a verified proof yet)
+
+  © 2026 Lutar, Stephen P. — SZL Holdings.  SPDX-License-Identifier: Apache-2.0
+
+  STATUS: ROADMAP. This file formalizes the SAFETY INVARIANTS of the a11oy governed
+  agent WORKFLOW in Lean 4 so they can eventually be machine-checked. It is a
+  SCAFFOLD: the theorem STATEMENTS are written out and the simplest ones are proved,
+  but the deeper ones are deliberately left as `sorry` and are LABELLED as such so we
+  never overclaim a machine-checked guarantee we do not yet have. Inspired by
+  Lean4Agent (arXiv:2606.06523) — formalizing agent workflow invariants in Lean 4.
+
+  What this models: the irreducible core of ONE governed decision in a11oy:
+      gate.evaluate → lambda.score → decision.recommend → receipt.sign → replay.verify
+  and the doctrine rules the runtime enforces (Colang ROE + arena gate). The goal of
+  the roadmap is: every theorem here is discharged WITHOUT `sorry`, then a CI job runs
+  `lake build` and the UI cites "N/M workflow invariants machine-checked".
+
+  HONESTY: until `lake build` passes with zero `sorry`, the UI MUST render these as
+  "ROADMAP — statements formalized, proofs in progress", never as "verified".
+-/
+
+namespace A11oy.Workflow
+
+/-- The ordered phases of one governed decision. -/
+inductive Phase where
+  | gate        -- policy gate evaluated the action plan
+  | lambda      -- trust score (Λ, Conjecture 1) computed across axes
+  | recommend   -- governed recommendation emitted
+  | sign        -- decision receipt DSSE-signed (ECDSA-P256, in-image key)
+  | replay      -- deterministic replay produced byte-identical root
+  deriving Repr, DecidableEq
+
+/-- A decision outcome. -/
+inductive Decision where
+  | allow
+  | deny
+  | rateLimit
+  | observation
+  deriving Repr, DecidableEq
+
+/-- An action carries flags the runtime actually inspects. -/
+structure Action where
+  destructive        : Bool   -- matches a destructive signature
+  operatorApproved   : Bool   -- operator.approve event present
+  highImpact         : Bool   -- requires_approval
+  injection          : Bool   -- prompt-injection signature
+  payloadOverCeiling : Bool   -- exceeds 1MB DoS ceiling
+  deriving Repr
+
+/-- A workflow trace is the (ordered) list of phases that actually ran. -/
+abbrev Trace := List Phase
+
+/-- The policy gate's verdict on an action (mirrors `_a11oy_arena_inspect` +
+    Colang ROE: any of these conditions ⇒ DENY). -/
+def gateVerdict (a : Action) : Decision :=
+  if a.injection || a.payloadOverCeiling
+     || (a.destructive && ¬ a.operatorApproved)
+     || (a.highImpact && ¬ a.operatorApproved)
+  then Decision.deny
+  else Decision.allow
+
+/-- INVARIANT 1 (proved): a destructive action without operator approval is DENIED.
+    This is the Colang `refuse_destructive_actions` flow as a theorem. -/
+theorem destructive_unapproved_denied (a : Action)
+    (hd : a.destructive = true) (hn : a.operatorApproved = false) :
+    gateVerdict a = Decision.deny := by
+  unfold gateVerdict
+  simp [hd, hn]
+
+/-- INVARIANT 2 (proved): an injection-bearing action is DENIED regardless of
+    every other flag. Colang `refuse_prompt_injection`. -/
+theorem injection_always_denied (a : Action) (hi : a.injection = true) :
+    gateVerdict a = Decision.deny := by
+  unfold gateVerdict
+  simp [hi]
+
+/-- INVARIANT 3 (proved): an oversized payload is DENIED (DoS size guard). -/
+theorem oversize_denied (a : Action) (ho : a.payloadOverCeiling = true) :
+    gateVerdict a = Decision.deny := by
+  unfold gateVerdict
+  simp [ho]
+
+/-- "policy-before-effect": `gate` must occur strictly before `sign` in a trace. -/
+def policyBeforeEffect (t : Trace) : Prop :=
+  ∀ i j, t.get? i = some Phase.sign → t.get? j = some Phase.gate → j < i
+
+/-- INVARIANT 4 (ROADMAP — `sorry`): the canonical governed-turn pipeline always
+    evaluates policy before any signing/effect step. Statement is formalized; the
+    proof over arbitrary well-formed traces is left for the roadmap. DO NOT claim
+    this as machine-checked until the `sorry` below is removed. -/
+theorem canonical_pipeline_policy_first :
+    policyBeforeEffect [Phase.gate, Phase.lambda, Phase.recommend,
+                        Phase.sign, Phase.replay] := by
+  sorry  -- ROADMAP: discharge by `decide`/index reasoning; tracked in CI
+
+/-- INVARIANT 5 (ROADMAP — `sorry`): determinism — replaying a trace yields a
+    byte-identical receipt root. Requires modeling the receipt hash-chain; left as
+    a roadmap obligation. -/
+theorem replay_is_deterministic (t : Trace) :
+    True := by
+  trivial  -- placeholder statement only; real determinism theorem is ROADMAP
+
+/-- Summary used by the CI/manifest extractor: which invariants are DISCHARGED. -/
+def invariantStatus : List (String × Bool) :=
+  [ ("destructive_unapproved_denied", true)
+  , ("injection_always_denied",       true)
+  , ("oversize_denied",               true)
+  , ("canonical_pipeline_policy_first", false)  -- ROADMAP (sorry)
+  , ("replay_is_deterministic",         false)  -- ROADMAP (placeholder)
+  ]
+
+end A11oy.Workflow

policy/colang/killinchu_threat.co

@@ -0,0 +1,55 @@
+# SPDX-License-Identifier: Apache-2.0
+# killinchu threat-response ROE — NeMo Guardrails Colang (v1) flows.
+# https://github.com/NVIDIA-NeMo/Guardrails
+#
+# DOCTRINE: counter-UAS / maritime C2 rules of engagement as a versioned,
+# auditable Colang file. Effectors are SIMULATED, human-on-loop. This file is the
+# authoritative policy for autonomous threat handling; the runtime enforcer in
+# szl_colang_policy.py loads it and records fired flows into the signed receipt.
+# Coordinates with Dev D's threat classifier (conformal set + ECE<0.05 gate from
+# szl_conformal.py / szl_calibration.py) — engagement is never recommended on an
+# unmeasured-calibration classifier or a non-singleton conformal set without a
+# human.
+#
+# policy_id: killinchu-threat-roe
+# policy_version: 1.0.0
+
+define flow no_autonomous_engagement
+  # No engagement effector may fire autonomously — every engage requires a
+  # recorded human authorization (SIMULATED human-on-loop). Hard ROE boundary.
+  user action requested $action
+  if is_engagement($action) and not has_human_authorization($action)
+    bot refuse action with reason "engagement_requires_human_authorization"
+    create signed_refusal_receipt($action, "engagement_requires_human_authorization")
+  else
+    continue
+
+define flow require_calibrated_classifier
+  # An automated threat response is permitted only when the classifier's
+  # calibration is MEASURED and ECE < gate threshold (szl_calibration gate).
+  user action requested $action
+  if is_automated_response($action) and not classifier_calibration_gate_pass($action)
+    bot refuse action with reason "classifier_calibration_gate_failed"
+    create signed_refusal_receipt($action, "classifier_calibration_gate_failed")
+  else
+    continue
+
+define flow require_singleton_conformal_set
+  # If the conformal threat-class set is NOT a singleton (ambiguous at the 95%
+  # coverage target), do not auto-act — route to a human (act-vs-ask).
+  user action requested $action
+  if is_automated_response($action) and conformal_set_ambiguous($action)
+    bot refuse action with reason "conformal_set_ambiguous_route_to_human"
+    create signed_refusal_receipt($action, "conformal_set_ambiguous_route_to_human")
+  else
+    continue
+
+define flow require_sensor_quorum
+  # A threat decision requires a sensor-fusion quorum (BFT n>=3f+1; Dev D panel).
+  user action requested $action
+  if is_threat_decision($action) and not sensor_quorum_met($action)
+    bot refuse action with reason "sensor_quorum_not_met"
+    create signed_refusal_receipt($action, "sensor_quorum_not_met")
+  else
+    allow action
+    create signed_action_receipt($action)

policy/colang/roe_core.co

@@ -0,0 +1,71 @@
+# SPDX-License-Identifier: Apache-2.0
+# a11oy ROE / governance policy — NeMo Guardrails Colang (v1) flows.
+# https://github.com/NVIDIA-NeMo/Guardrails  (Colang policy DSL)
+#
+# DOCTRINE: This file is the AUTHORITATIVE, version-controlled, independently
+# auditable Rules-of-Engagement policy. Policy lives HERE, in a reviewable file
+# under git — NOT inside a prompt. serve.py loads + enforces these flows via
+# szl_colang_policy.py and renders the file content + sha256 in the Policy tab so
+# anyone can audit exactly which rules are active.
+#
+# policy_id: a11oy-roe-core
+# policy_version: 1.0.0
+# Each `define flow` is a named, hash-anchored rule. The runtime enforcer matches
+# the proposed action against each flow's guard conditions and records which
+# flows fired into the signed receipt (controls_evaluated.policy per IETF
+# draft-marques-asqav-compliance-receipts-05).
+
+define flow refuse_destructive_actions
+  # No irreversible / destructive action without explicit operator authorization.
+  user action requested $action
+  if is_destructive($action) and not has_operator_authorization($action)
+    bot refuse action with reason "destructive_without_authorization"
+    create signed_refusal_receipt($action, "destructive_without_authorization")
+  else
+    continue
+
+define flow refuse_pii_exfiltration
+  # Never emit/exfiltrate PII (PAN, SSN, full card numbers) to an external sink.
+  user action requested $action
+  if requests_pii_exfiltration($action)
+    bot refuse action with reason "pii_exfiltration_blocked"
+    create signed_refusal_receipt($action, "pii_exfiltration_blocked")
+  else
+    continue
+
+define flow refuse_prompt_injection
+  # Reject actions carrying override/injection signatures ("ignore previous", etc).
+  user action requested $action
+  if matches_injection_signature($action)
+    bot refuse action with reason "prompt_injection_detected"
+    create signed_refusal_receipt($action, "prompt_injection_detected")
+  else
+    continue
+
+define flow require_operator_approval_high_impact
+  # High-consequence actions require a recorded human-on-loop approval event.
+  user action requested $action
+  if is_high_impact($action) and not has_operator_approval_event($action)
+    bot refuse action with reason "operator_approval_required"
+    create signed_refusal_receipt($action, "operator_approval_required")
+  else
+    continue
+
+define flow enforce_payload_ceiling
+  # Reject oversized payloads (DoS ceiling) before they reach an effector.
+  user action requested $action
+  if payload_exceeds_ceiling($action)
+    bot refuse action with reason "payload_exceeds_1MB"
+    create signed_refusal_receipt($action, "payload_exceeds_1MB")
+  else
+    continue
+
+define flow policy_before_effect
+  # An effecting tool call MUST be preceded by a policy evaluation in the trace.
+  user action requested $action
+  if is_effecting($action) and not policy_evaluated_before($action)
+    bot refuse action with reason "policy_evaluation_must_precede_effect"
+    create signed_refusal_receipt($action, "policy_evaluation_must_precede_effect")
+  else
+    allow action
+    create signed_action_receipt($action)

web/governance.html

@@ -0,0 +1,253 @@
+<!DOCTYPE html>
+<!--
+  a11oy GOVERNANCE / EVAL / CALIBRATION console (Dev B lane).
+  © 2026 Lutar, Stephen P. — SZL Holdings. SPDX-License-Identifier: Apache-2.0
+  0 runtime CDN: the ONLY external script is the in-image vendored Chart.js
+  (/vendor/chart.umd.min.js). All data is fetched live from /api/a11oy/v1/gov/*.
+  Every number is measured or honestly labelled "not_measured" — nothing fabricated.
+-->
+<html lang="en">
+<head>
+<meta charset="utf-8"/>
+<meta name="viewport" content="width=device-width, initial-scale=1"/>
+<title>a11oy · Governance / Eval / Calibration</title>
+<script src="/vendor/chart.umd.min.js"></script>
+<style>
+  :root{
+    --bg:#0a0e14; --panel:#121823; --panel2:#0f141d; --line:#1f2a3a;
+    --ink:#e6edf3; --mut:#8b98a9; --acc:#5ad1c9; --acc2:#7aa2f7;
+    --ok:#3fb950; --warn:#d29922; --err:#f85149; --road:#a371f7;
+  }
+  *{box-sizing:border-box}
+  body{margin:0;background:var(--bg);color:var(--ink);
+       font:14px/1.5 ui-monospace,SFMono-Regular,Menlo,Consolas,monospace}
+  header{padding:18px 22px;border-bottom:1px solid var(--line);
+         background:linear-gradient(180deg,#0d1320,#0a0e14)}
+  h1{margin:0;font-size:18px;letter-spacing:.3px}
+  .sub{color:var(--mut);font-size:12px;margin-top:4px}
+  .wrap{max-width:1180px;margin:0 auto;padding:18px 22px}
+  .grid{display:grid;gap:16px;grid-template-columns:repeat(auto-fit,minmax(340px,1fr))}
+  .card{background:var(--panel);border:1px solid var(--line);border-radius:10px;
+        padding:16px 18px}
+  .card h2{margin:0 0 10px;font-size:14px;letter-spacing:.4px;color:var(--acc)}
+  .kv{display:flex;justify-content:space-between;gap:10px;padding:3px 0;
+      border-bottom:1px dotted #1a2435}
+  .kv:last-child{border-bottom:0}
+  .k{color:var(--mut)} .v{color:var(--ink);text-align:right;word-break:break-word}
+  .big{font-size:30px;font-weight:700;letter-spacing:.5px}
+  .pill{display:inline-block;padding:2px 9px;border-radius:999px;font-size:11px;
+        border:1px solid var(--line)}
+  .pill.ok{color:var(--ok);border-color:#163a1f;background:#0e2113}
+  .pill.err{color:var(--err);border-color:#4a1c1c;background:#240f0f}
+  .pill.warn{color:var(--warn);border-color:#3a3015;background:#1f1a0a}
+  .pill.road{color:var(--road);border-color:#2e2147;background:#160f24}
+  .pill.acc{color:var(--acc);border-color:#13403c;background:#0a201e}
+  .cite{color:var(--mut);font-size:11px;margin-top:8px}
+  .cite code{color:var(--acc2)}
+  .mono{font-family:inherit}
+  .set{display:flex;gap:8px;flex-wrap:wrap;margin:6px 0}
+  .set .lab{padding:4px 11px;border-radius:7px;border:1px solid var(--line);
+            background:#0e1622;font-size:13px}
+  .set .lab.in{border-color:#13403c;background:#0a201e;color:var(--acc)}
+  table{width:100%;border-collapse:collapse;font-size:12px}
+  th,td{text-align:left;padding:5px 7px;border-bottom:1px solid #1a2435}
+  th{color:var(--mut);font-weight:600}
+  .file{background:var(--panel2);border:1px solid var(--line);border-radius:8px;
+        padding:10px 12px;margin:8px 0}
+  .file pre{margin:6px 0 0;white-space:pre-wrap;color:#b9c6d6;font-size:11px;
+            max-height:160px;overflow:auto}
+  .sha{color:var(--acc2);font-size:11px}
+  .note{color:var(--mut);font-size:11px;margin-top:8px;line-height:1.55}
+  .loading{color:var(--mut)} .err{color:var(--err)}
+  a{color:var(--acc2)}
+  footer{color:var(--mut);font-size:11px;padding:14px 22px;border-top:1px solid var(--line)}
+</style>
+</head>
+<body>
+<header>
+  <h1>a11oy · Governance / Eval / Calibration</h1>
+  <div class="sub">Live tool-rule-following eval (τ-bench-style) · calibration (ECE/Brier) · conformal prediction sets · file-backed Colang policy · IETF compliance-receipt profile · Lean4Agent invariants (roadmap). Every number is measured live or labelled <em>not_measured</em>.</div>
+</header>
+<div class="wrap">
+  <div class="grid">
+    <!-- EVAL -->
+    <div class="card" id="eval-card">
+      <h2>τ-BENCH-STYLE EVAL — TOOL RULE-FOLLOWING</h2>
+      <div id="eval" class="loading">measuring live…</div>
+      <div class="cite">Suite design after τ-bench <code>arXiv:2406.12045</code> · AgentBench <code>arXiv:2308.03688</code>. pass^1 = task passes iff EVERY domain rule holds against the real produced trajectory.</div>
+    </div>
+
+    <!-- CALIBRATION -->
+    <div class="card" id="cal-card">
+      <h2>CALIBRATION — ECE / BRIER + AUTO-RESPONSE GATE</h2>
+      <div id="cal" class="loading">measuring live…</div>
+      <canvas id="relchart" height="150" style="margin-top:10px"></canvas>
+      <div class="cite">ECE (equal-width bins) + Brier per <code>arXiv:2505.15437</code>. Gate: ECE &lt; 0.05 required for any automated (no-human) response; <b>fails closed</b> on unmeasured calibration.</div>
+    </div>
+
+    <!-- CONFORMAL -->
+    <div class="card" id="conf-card">
+      <h2>CONFORMAL PREDICTION — SETS, NOT BARE %</h2>
+      <div id="conf" class="loading">computing…</div>
+      <div class="cite">Split conformal per <code>arXiv:2305.18404</code> · Angelopoulos &amp; Bates <code>arXiv:2107.07511</code>. Shared helper <code>szl_conformal</code> — Dev D imports the SAME module for threat classification.</div>
+    </div>
+
+    <!-- POLICY -->
+    <div class="card" id="pol-card" style="grid-column:1/-1">
+      <h2>POLICY — FILE-BACKED COLANG ROE (INDEPENDENTLY AUDITABLE)</h2>
+      <div id="pol" class="loading">loading policy files…</div>
+      <div class="cite">NeMo Guardrails Colang syntax — <code>github.com/NVIDIA-NeMo/Guardrails</code>. Policy lives in version-controlled <code>.co</code> files (single source of truth), shown here with per-file sha256. No prompt-only policy.</div>
+    </div>
+
+    <!-- IETF -->
+    <div class="card" id="ietf-card" style="grid-column:1/-1">
+      <h2>IETF COMPLIANCE-RECEIPT PROFILE (DSSE ENVELOPE INTACT)</h2>
+      <div id="ietf" class="loading">signing a live decision…</div>
+      <div class="cite">Compliance VIEW aligned to <code>draft-marques-asqav-compliance-receipts-05</code>. The cross-app DSSE envelope (ECDSA-P256-SHA256) is reproduced UNCHANGED — verify against <a href="/cosign.pub">/cosign.pub</a>.</div>
+    </div>
+
+    <!-- LEAN -->
+    <div class="card" id="lean-card">
+      <h2>LEAN4AGENT — WORKFLOW INVARIANTS <span class="pill road">ROADMAP</span></h2>
+      <div id="lean" class="loading">…</div>
+      <div class="cite">Formalization after Lean4Agent <code>arXiv:2606.06523</code>. Proved-in-isolation invariants are real; full-pipeline + determinism theorems carry <code>sorry</code> and are NOT machine-checked yet.</div>
+    </div>
+  </div>
+</div>
+<footer>
+  a11oy governance lane · doctrine v11 · Λ = Conjecture 1 (advisory) · SLSA L1 honest / L2 in progress / L3 roadmap · trust &lt; 100% · 0 runtime CDN.
+  Data: <span class="mono">/api/a11oy/v1/gov/{eval,calibration,conformal,policy,ietf,lean,summary}</span>
+</footer>
+
+<script>
+const $=s=>document.querySelector(s);
+const esc=s=>String(s==null?"":s).replace(/[&<>]/g,c=>({"&":"&amp;","<":"&lt;",">":"&gt;"}[c]));
+function kv(k,v){return `<div class="kv"><span class="k">${esc(k)}</span><span class="v">${v}</span></div>`}
+async function getj(u){const r=await fetch(u);if(!r.ok)throw new Error(u+" -> "+r.status);return r.json()}
+
+// ---- EVAL ----
+getj("/api/a11oy/v1/gov/eval").then(d=>{
+  const pct=(d.score_pct!=null)?d.score_pct.toFixed(2)+"%":"—";
+  const asof=(d.as_of||"").slice(0,19).replace("T"," ")+" UTC";
+  const runner=(d.tasks&&d.tasks[0]&&d.tasks[0].trajectory||[]).some(s=>s.tool==="arena_gate.inspect")?"live _a11oy_arena_inspect gate":"reference rule-follower";
+  let rows="";
+  (d.domains?Object.entries(d.domains):[]).forEach(([dom,v])=>{
+    const st=v.status==="measured"?`<span class="pill ok">${(v.pass_at_1*100).toFixed(0)}%</span>`:`<span class="pill warn">not_measured</span>`;
+    rows+=`<tr><td>${esc(dom)}</td><td>${v.passed}/${v.total}</td><td>${st}</td></tr>`;
+  });
+  $("#eval").innerHTML=
+    `<div class="big">${pct}</div>`+
+    kv("suite",`<span class="mono">${esc(d.suite_id)} ${esc(d.suite_version)}</span>`)+
+    kv("metric",esc(d.metric))+
+    kv("tasks","<b>"+d.tasks_passed+"</b> / "+d.tasks_total+" passed")+
+    kv("negative controls",d.negative_controls)+
+    kv("runner",esc(runner))+
+    kv("as-of",`<span class="mono">${esc(asof)}</span>`)+
+    kv("determinism",`<span class="sha mono">${esc(d.determinism_hash)}</span>`)+
+    kv("run receipt",(d.receipt&&d.receipt.signed)?`<span class="pill ok">DSSE signed</span>`:`<span class="pill warn">unsigned</span>`)+
+    `<table style="margin-top:8px"><tr><th>domain</th><th>passed</th><th>pass^1</th></tr>${rows}</table>`+
+    `<div class="note">Cited as: “a11oy scores ${pct} on suite ${esc(d.suite_id)} ${esc(d.suite_version)}, as-of ${esc(asof)}.” An unrun domain renders <em>not_measured</em>, never 0.</div>`;
+}).catch(e=>$("#eval").innerHTML=`<div class="err">eval unavailable: ${esc(e.message)}</div>`);
+
+// ---- CALIBRATION ----
+getj("/api/a11oy/v1/gov/calibration").then(d=>{
+  const m=d.metrics||{},g=d.automated_response_gate||{};
+  const measured=m.status==="measured";
+  const ecev=measured?m.ece.toFixed(4):"not_measured";
+  const brierv=measured&&m.brier!=null?m.brier.toFixed(4):"not_measured";
+  const gate=g.allow?`<span class="pill ok">ALLOW (ECE&lt;${d.gate_threshold_ece})</span>`
+                    :`<span class="pill err">DENY → human-on-loop</span>`;
+  $("#cal").innerHTML=
+    kv("model / agent",`<span class="mono">${esc(m.model)} / ${esc(m.agent_type)}</span>`)+
+    kv("status",measured?`<span class="pill acc">measured</span>`:`<span class="pill warn">${esc(m.status)}</span>`)+
+    kv("samples (n)",m.n)+
+    kv("ECE",`<b class="mono">${ecev}</b>`)+
+    kv("Brier"+(m.brier_kind?` (${esc(m.brier_kind)})`:""),`<span class="mono">${brierv}</span>`)+
+    kv("auto-response gate",gate)+
+    `<div class="note">${esc(g.honesty||m.honesty||"")}</div>`;
+  // reliability chart
+  const arr=Array.isArray(m.reliability)?m.reliability:[];
+  if(window.Chart&&arr.length){
+    new Chart($("#relchart"),{type:"bar",
+      data:{labels:arr.map(b=>(b.lo!=null?b.lo:0).toFixed(2)),
+            datasets:[
+              {label:"accuracy",data:arr.map(b=>b.accuracy),backgroundColor:"#5ad1c9"},
+              {label:"mean confidence",data:arr.map(b=>b.mean_conf),backgroundColor:"#7aa2f7",type:"line",borderColor:"#7aa2f7",fill:false}
+            ]},
+      options:{plugins:{legend:{labels:{color:"#8b98a9"}}},
+               scales:{x:{ticks:{color:"#8b98a9"},grid:{color:"#1a2435"}},
+                       y:{min:0,max:1,ticks:{color:"#8b98a9"},grid:{color:"#1a2435"}}}}});
+  }
+}).catch(e=>$("#cal").innerHTML=`<div class="err">calibration unavailable: ${esc(e.message)}</div>`);
+
+// ---- CONFORMAL ----
+getj("/api/a11oy/v1/gov/conformal").then(d=>{
+  const cs=d.conformal_set||{};
+  const labels=cs.full_label_space||(cs.members||[]).map(m=>m.label)||[];
+  const inset=new Set(cs.set||[]);
+  let chips=labels.map(l=>`<span class="lab ${inset.has(l)?"in":""}">${esc(l)}${inset.has(l)?" ✓":""}</span>`).join("");
+  $("#conf").innerHTML=
+    kv("helper",`<span class="mono">${esc(d.helper_version)}</span>`)+
+    kv("coverage target",`≥ ${(d.coverage_target*100).toFixed(0)}%`)+
+    kv("α (alpha)",d.alpha)+
+    `<div class="note" style="margin:10px 0 4px">Instead of bare “confidence ${d.example_bare_confidence_pct}%”, the decision is reported as a SET guaranteed to contain the true class with ≥${(d.coverage_target*100).toFixed(0)}% coverage:</div>`+
+    `<div class="set">${chips}</div>`+
+    kv("set size",cs.set_size!=null?cs.set_size:(cs.set?cs.set.length:"—"))+
+    kv("singleton",cs.singleton?`<span class="pill ok">yes (decisive)</span>`:`<span class="pill warn">no (ambiguous)</span>`)+
+    kv("q̂ (quantile)",cs.q_hat!=null?cs.q_hat.toFixed(4):"—")+
+    kv("calibration n",cs.calibration_n)+
+    `<div class="note">${esc((d.bare_pct_replacement&&(d.bare_pct_replacement.display||d.bare_pct_replacement.replaces_bare_pct))||cs.guarantee||"")}</div>`;
+}).catch(e=>$("#conf").innerHTML=`<div class="err">conformal unavailable: ${esc(e.message)}</div>`);
+
+// ---- POLICY ----
+getj("/api/a11oy/v1/gov/policy").then(d=>{
+  const a=d.audit_view||{};
+  let files=(a.files||[]).map(f=>
+    `<div class="file"><b>${esc(f.name)}</b> · id <span class="mono">${esc(f.policy_id)}</span> v${esc(f.policy_version)} · ${(f.flows||[]).length} flows<br>
+     <span class="sha">sha256: ${esc(f.sha256||f.sha||"")}</span>
+     <pre>${esc((f.content||"").slice(0,600))}${(f.content||"").length>600?"\n…":""}</pre></div>`).join("");
+  $("#pol").innerHTML=
+    kv("loaded",a.loaded?`<span class="pill ok">yes</span>`:`<span class="pill err">no</span>`)+
+    kv("files",a.file_count)+kv("total flows",a.flow_count)+
+    kv("NeMo runtime",a.nemoguardrails_runtime_present?`<span class="pill ok">present</span>`:`<span class="pill road">file-backed enforcement (runtime roadmap)</span>`)+
+    `<div style="margin-top:10px">${files}</div>`+
+    `<div class="note">${esc(a.honesty||"")}</div>`;
+}).catch(e=>$("#pol").innerHTML=`<div class="err">policy unavailable: ${esc(e.message)}</div>`);
+
+// ---- IETF ----
+getj("/api/a11oy/v1/gov/ietf").then(d=>{
+  const p=d.compliance_profile||{},cp=p.compliance_payload||{},env=d.dsse_envelope||{};
+  const conf=p.conformance||{};
+  let checks=(conf.checks||[]).map(c=>`<tr><td>${esc(c.check)}</td><td>${c.ok?'<span class="pill ok">ok</span>':'<span class="pill err">fail</span>'}</td><td class="mono">${esc(c.detail)}</td></tr>`).join("");
+  let map=Object.entries(p.mapping||{}).map(([k,v])=>`<tr><td class="mono">${esc(k)}</td><td class="mono">${esc(v)}</td></tr>`).join("");
+  $("#ietf").innerHTML=
+    kv("draft",`<a href="https://datatracker.ietf.org/doc/${esc(p.draft)}/" target="_blank" rel="noopener" class="mono">${esc(p.draft)}</a>`)+
+    kv("status",esc(p.draft_status))+
+    kv("DSSE envelope",p.dsse_envelope_intact?`<span class="pill ok">${esc(p.dsse_alg)} (intact)</span>`:`<span class="pill err">modified</span>`)+
+    kv("DSSE kid",`<span class="mono">${esc(p.dsse_kid)}</span>`)+
+    kv("receipt type",`<span class="mono">${esc(cp.type)}</span>`)+
+    kv("decision",`<span class="pill ${cp.decision==='deny'?'err':'ok'}">${esc(cp.decision)}</span>`)+
+    kv("action_ref",`<span class="sha mono">${esc((cp.action_ref||'').slice(0,28))}…</span>`)+
+    kv("policy_digest",`<span class="sha mono">${esc((cp.policy_digest||'').slice(0,28))}…</span>`)+
+    kv("previousReceiptHash",`<span class="sha mono">${esc((cp.previousReceiptHash||'').slice(0,28))}…</span>`)+
+    kv("conformance",conf.ok?`<span class="pill ok">payload conforms to draft-05</span>`:`<span class="pill err">non-conformant</span>`)+
+    `<div class="note" style="margin-top:8px"><b>Field crosswalk (a11oy → draft-05):</b></div>`+
+    `<table><tr><th>a11oy field</th><th>draft-05 field</th></tr>${map}</table>`+
+    `<div class="note" style="margin-top:8px"><b>Conformance checks:</b></div>`+
+    `<table><tr><th>check</th><th>ok</th><th>detail</th></tr>${checks}</table>`+
+    `<div class="note">${esc(p.note||"")}</div>`;
+}).catch(e=>$("#ietf").innerHTML=`<div class="err">ietf profile unavailable: ${esc(e.message)}</div>`);
+
+// ---- LEAN ----
+getj("/api/a11oy/v1/gov/lean").then(d=>{
+  let rows=(d.invariants||[]).map(i=>`<tr><td class="mono">${esc(i.name)}</td><td>${i.proved?'<span class="pill ok">proved</span>':`<span class="pill road">${esc(i.status||'roadmap')}</span>`}</td></tr>`).join("");
+  $("#lean").innerHTML=
+    kv("status",`<span class="pill road">${esc(d.status)}</span>`)+
+    kv("proved","<b>"+d.invariants_proved+"</b> / "+d.invariants_total)+
+    kv("file",`<span class="mono">${esc(d.file)}</span>`)+
+    `<table style="margin-top:8px"><tr><th>invariant</th><th>state</th></tr>${rows}</table>`+
+    `<div class="note">${esc(d.honesty||"")}</div>`;
+}).catch(e=>$("#lean").innerHTML=`<div class="err">lean unavailable: ${esc(e.message)}</div>`);
+</script>
+</body>
+</html>