Spaces:
Running
Running
| <html lang="en"> | |
| <head> | |
| <meta charset="utf-8" /> | |
| <meta name="viewport" content="width=device-width, initial-scale=1" /> | |
| <title>a11oy — Verifiable Inference</title> | |
| <style> | |
| /* ===================================================================== | |
| a11oy Tier-1 Demo — elite showcase aesthetic | |
| Dark palette · Cabinet Grotesk / JetBrains Mono · honest-label chips | |
| ===================================================================== */ | |
| @import url('https://fonts.googleapis.com/css2?family=JetBrains+Mono:ital,wght@0,400;0,600;1,400&display=swap'); | |
| :root { | |
| --bg: #0a0c0f; | |
| --bg-panel: #111318; | |
| --bg-card: #16191f; | |
| --border: #2a2d35; | |
| --border-hi: #3d4250; | |
| --text: #e8eaf0; | |
| --text-dim: #8891a8; | |
| --text-mute: #4a5068; | |
| --accent: #6c8ef5; | |
| --accent-hi: #8aaaf8; | |
| --green: #4ade80; | |
| --amber: #f59e0b; | |
| --red: #f87171; | |
| --mono: 'JetBrains Mono', 'Fira Code', 'Cascadia Code', monospace; | |
| --sans: 'Cabinet Grotesk', 'Inter', 'Segoe UI', system-ui, sans-serif; | |
| --radius: 8px; | |
| --radius-lg: 14px; | |
| --shadow: 0 2px 12px rgba(0,0,0,0.5); | |
| } | |
| *, *::before, *::after { box-sizing: border-box; margin: 0; padding: 0; } | |
| body { | |
| background: var(--bg); | |
| color: var(--text); | |
| font-family: var(--sans); | |
| font-size: 15px; | |
| line-height: 1.6; | |
| min-height: 100vh; | |
| } | |
| /* ---- header ---- */ | |
| .site-header { | |
| border-bottom: 1px solid var(--border); | |
| padding: 18px 32px; | |
| display: flex; | |
| align-items: center; | |
| gap: 16px; | |
| background: var(--bg-panel); | |
| } | |
| .logo-mark { | |
| width: 32px; height: 32px; | |
| flex-shrink: 0; | |
| } | |
| .site-title { font-size: 16px; font-weight: 700; letter-spacing: -0.02em; } | |
| .site-tagline { font-size: 12px; color: var(--text-dim); margin-left: auto; } | |
| .nav-back { | |
| font-size: 12px; color: var(--text-dim); | |
| text-decoration: none; margin-left: auto; | |
| border: 1px solid var(--border); border-radius: 6px; | |
| padding: 5px 12px; | |
| transition: border-color .15s, color .15s; | |
| } | |
| .nav-back:hover { border-color: var(--accent); color: var(--accent-hi); } | |
| /* ---- layout ---- */ | |
| .page { max-width: 900px; margin: 0 auto; padding: 48px 24px 80px; } | |
| .page-hero { margin-bottom: 56px; } | |
| .page-hero h1 { | |
| font-size: 28px; font-weight: 800; letter-spacing: -0.03em; | |
| line-height: 1.2; margin-bottom: 10px; | |
| } | |
| .page-hero p { color: var(--text-dim); max-width: 600px; } | |
| /* ---- sections ---- */ | |
| .section { | |
| margin-bottom: 56px; | |
| border: 1px solid var(--border); | |
| border-radius: var(--radius-lg); | |
| overflow: hidden; | |
| } | |
| .section-head { | |
| background: var(--bg-panel); | |
| padding: 20px 24px; | |
| border-bottom: 1px solid var(--border); | |
| } | |
| .section-head h2 { | |
| font-size: 16px; font-weight: 700; letter-spacing: -0.01em; | |
| margin-bottom: 4px; display: flex; align-items: center; gap: 10px; | |
| } | |
| .section-label { | |
| font-size: 10px; font-weight: 700; letter-spacing: 0.08em; | |
| text-transform: uppercase; color: var(--text-dim); | |
| border: 1px solid var(--border-hi); border-radius: 4px; | |
| padding: 2px 6px; | |
| } | |
| .section-head p { font-size: 13px; color: var(--text-dim); max-width: 620px; } | |
| .section-body { padding: 24px; background: var(--bg-card); } | |
| .moat-line { | |
| font-size: 12px; color: var(--text-dim); | |
| font-style: italic; margin-top: 8px; | |
| } | |
| /* ---- chip / badges ---- */ | |
| .chip { | |
| display: inline-block; border-radius: 4px; | |
| padding: 2px 8px; font-size: 11px; font-weight: 700; | |
| letter-spacing: 0.05em; text-transform: uppercase; | |
| border: 1px solid transparent; | |
| } | |
| .chip-allow { background: #052e12; border-color: #166534; color: var(--green); } | |
| .chip-review { background: #2d1e00; border-color: #92400e; color: var(--amber); } | |
| .chip-deny { background: #2d0f0f; border-color: #991b1b; color: var(--red); } | |
| .chip-info { background: #0d1533; border-color: #1e3a8a; color: var(--accent-hi); } | |
| .chip-dim { background: #1a1d24; border-color: var(--border); color: var(--text-dim); } | |
| .chip-ok { background: #052e12; border-color: #166534; color: var(--green); } | |
| .chip-warn { background: #2d1e00; border-color: #92400e; color: var(--amber); } | |
| .chip-err { background: #2d0f0f; border-color: #991b1b; color: var(--red); } | |
| /* ---- buttons ---- */ | |
| .btn-row { display: flex; gap: 10px; flex-wrap: wrap; margin-bottom: 20px; } | |
| .btn { | |
| padding: 9px 18px; border-radius: var(--radius); | |
| font-family: var(--sans); font-size: 13px; font-weight: 600; | |
| cursor: pointer; border: 1px solid transparent; | |
| transition: opacity .15s, transform .05s; | |
| outline: none; | |
| } | |
| .btn:active { transform: scale(0.97); } | |
| .btn-primary { | |
| background: #1e3a8a; border-color: #2563eb; | |
| color: #dbeafe; | |
| } | |
| .btn-primary:hover { background: #1d4ed8; } | |
| .btn-allow { background: #052e12; border-color: #166534; color: var(--green); } | |
| .btn-allow:hover { background: #14532d; } | |
| .btn-review { background: #2d1e00; border-color: #92400e; color: var(--amber); } | |
| .btn-review:hover { background: #451a03; } | |
| .btn-deny { background: #2d0f0f; border-color: #991b1b; color: var(--red); } | |
| .btn-deny:hover { background: #450a0a; } | |
| .btn:disabled { opacity: 0.5; cursor: not-allowed; } | |
| /* ---- output panels ---- */ | |
| .output { | |
| background: var(--bg-panel); border: 1px solid var(--border); | |
| border-radius: var(--radius); padding: 16px 20px; | |
| font-family: var(--mono); font-size: 12px; line-height: 1.7; | |
| white-space: pre-wrap; word-break: break-all; | |
| color: var(--text-dim); min-height: 56px; | |
| transition: border-color .2s; | |
| } | |
| .output.verified { border-color: #166534; } | |
| .output.failed { border-color: #991b1b; } | |
| .output.loading { border-color: var(--accent); animation: pulse 1s ease-in-out infinite; } | |
| @keyframes pulse { 0%,100%{opacity:.8} 50%{opacity:.4} } | |
| /* ---- verdict banner ---- */ | |
| .verdict-banner { | |
| border-radius: var(--radius); padding: 14px 20px; | |
| margin-bottom: 16px; font-size: 14px; font-weight: 700; | |
| display: flex; align-items: center; gap: 12px; | |
| border: 1px solid transparent; | |
| } | |
| .verdict-ok { background: #052e12; border-color: #166534; color: var(--green); } | |
| .verdict-fail{ background: #2d0f0f; border-color: #991b1b; color: var(--red); } | |
| .verdict-dim { background: var(--bg-panel); border-color: var(--border); color: var(--text-dim); } | |
| /* ---- formula cards ---- */ | |
| .formula-grid { display: grid; gap: 14px; } | |
| .formula-card { | |
| background: var(--bg-panel); border: 1px solid var(--border); | |
| border-radius: var(--radius); padding: 16px 20px; | |
| } | |
| .formula-card-head { | |
| display: flex; align-items: center; gap: 10px; margin-bottom: 8px; | |
| } | |
| .formula-id { | |
| font-family: var(--mono); font-size: 11px; font-weight: 600; | |
| color: var(--accent); background: #0d1533; border: 1px solid #1e3a8a; | |
| border-radius: 4px; padding: 2px 7px; | |
| } | |
| .formula-name { font-size: 14px; font-weight: 700; } | |
| .formula-lean { | |
| font-family: var(--mono); font-size: 12px; color: #a5f3fc; | |
| background: #051e24; border: 1px solid #0e4a57; | |
| border-radius: 6px; padding: 10px 14px; margin: 8px 0; | |
| white-space: pre-wrap; word-break: break-all; line-height: 1.6; | |
| } | |
| .formula-desc { font-size: 12px; color: var(--text-dim); } | |
| .formula-status { | |
| font-size: 10px; color: var(--green); font-family: var(--mono); | |
| margin-top: 6px; | |
| } | |
| /* ---- corpus diagram ---- */ | |
| .corpus-diagram { | |
| display: flex; gap: 14px; flex-wrap: wrap; margin: 20px 0; | |
| } | |
| .corpus-tier { | |
| flex: 1; min-width: 180px; | |
| border: 1px solid var(--border); border-radius: var(--radius); | |
| padding: 16px; background: var(--bg-panel); | |
| } | |
| .corpus-count { | |
| font-size: 32px; font-weight: 800; font-family: var(--mono); | |
| line-height: 1; | |
| } | |
| .corpus-count.proven { color: var(--green); } | |
| .corpus-count.gates { color: var(--amber); } | |
| .corpus-count.total { color: var(--accent-hi); } | |
| .corpus-tier-label { font-size: 11px; font-weight: 700; text-transform: uppercase; | |
| letter-spacing: 0.07em; margin: 4px 0 8px; } | |
| .corpus-tier-desc { font-size: 12px; color: var(--text-dim); } | |
| .corpus-never-claim { | |
| background: #2d1e00; border: 1px solid #92400e; | |
| border-radius: var(--radius); padding: 12px 16px; | |
| font-size: 13px; color: var(--amber); margin-top: 14px; | |
| } | |
| /* ---- hash display ---- */ | |
| .hash-row { | |
| display: flex; gap: 8px; align-items: center; | |
| flex-wrap: wrap; margin: 6px 0; | |
| } | |
| .hash-label { font-size: 11px; color: var(--text-dim); min-width: 90px; } | |
| .hash-val { | |
| font-family: var(--mono); font-size: 11px; color: var(--text); | |
| background: var(--bg); border-radius: 4px; padding: 2px 6px; | |
| border: 1px solid var(--border); word-break: break-all; | |
| } | |
| .hash-match { border-color: #166534; color: var(--green); } | |
| .hash-mismatch { border-color: #991b1b; color: var(--red); } | |
| /* ---- gate row ---- */ | |
| .gate-row { | |
| display: flex; align-items: center; gap: 12px; | |
| padding: 8px 12px; border-radius: 6px; | |
| background: var(--bg); border: 1px solid var(--border); | |
| margin-bottom: 6px; | |
| } | |
| .gate-name { font-family: var(--mono); font-size: 12px; flex: 1; } | |
| .gate-fired { font-size: 11px; font-weight: 700; } | |
| /* ---- loading spinner ---- */ | |
| .spinner { | |
| display: inline-block; width: 14px; height: 14px; | |
| border: 2px solid var(--border); border-top-color: var(--accent); | |
| border-radius: 50%; animation: spin .7s linear infinite; | |
| vertical-align: middle; margin-right: 6px; | |
| } | |
| @keyframes spin { to { transform: rotate(360deg); } } | |
| /* ---- status line ---- */ | |
| .status-line { font-size: 12px; color: var(--text-dim); margin-top: 8px; } | |
| /* ---- divider ---- */ | |
| .divider { border: none; border-top: 1px solid var(--border); margin: 20px 0; } | |
| /* ---- conjecture chip ---- */ | |
| .conj { | |
| display: inline-block; | |
| font-size: 10px; font-weight: 700; letter-spacing: 0.06em; | |
| text-transform: uppercase; border-radius: 4px; | |
| padding: 2px 7px; border: 1px solid #92400e; | |
| background: #2d1e00; color: var(--amber); | |
| } | |
| /* ---- footer ---- */ | |
| .footer { | |
| border-top: 1px solid var(--border); padding: 24px; | |
| color: var(--text-mute); font-size: 12px; text-align: center; | |
| } | |
| a { color: var(--accent); text-decoration: none; } | |
| a:hover { color: var(--accent-hi); text-decoration: underline; } | |
| </style> | |
| </head> | |
| <body> | |
| <!-- ===== HEADER ===== --> | |
| <header class="site-header"> | |
| <svg class="logo-mark" viewBox="0 0 32 32" fill="none" aria-label="a11oy"> | |
| <rect width="32" height="32" rx="7" fill="#1e3a8a"/> | |
| <path d="M8 24 L16 8 L24 24" stroke="#6c8ef5" stroke-width="2.5" stroke-linecap="round" stroke-linejoin="round" fill="none"/> | |
| <circle cx="16" cy="16" r="2.5" fill="#8aaaf8"/> | |
| </svg> | |
| <span class="site-title">a11oy</span> | |
| <span class="site-tagline">Governed Inference · Verifiable by Design</span> | |
| <a href="/" class="nav-back">← Console</a> | |
| </header> | |
| <!-- ===== MAIN ===== --> | |
| <main class="page"> | |
| <div class="page-hero"> | |
| <h1>Verifiable Inference</h1> | |
| <p>Real, verifiable governance receipts — including our own public ledger. Every receipt is signed and independently verifiable. The honesty is the product.</p> | |
| </div> | |
| <!-- =================================================================== | |
| SECTION A — Buyer-Verifiable Receipt (BVIR) | |
| =================================================================== --> | |
| <section class="section" id="section-bvir"> | |
| <div class="section-head"> | |
| <h2> | |
| <span class="section-label">A</span> | |
| Buyer-Verifiable Inference Receipt | |
| </h2> | |
| <p> | |
| Makes a real POST /api/a11oy/v1/govern/infer call, then verifies the DSSE ECDSA-P256 | |
| signature <strong>in-browser</strong> using WebCrypto — no server round-trip for verification. | |
| SHA-256 of the decoded payload is recomputed and matched to <code>receipt.payload_digest</code>. | |
| </p> | |
| <p class="moat-line"> | |
| "No other inference provider gives you a receipt you can re-verify yourself, offline, with just a hash function and our public key." | |
| </p> | |
| </div> | |
| <div class="section-body"> | |
| <div class="btn-row"> | |
| <button class="btn btn-primary" id="bvir-run" onclick="runBVIR()"> | |
| Run Inference & Verify Receipt | |
| </button> | |
| </div> | |
| <div id="bvir-status" class="status-line"></div> | |
| <div id="bvir-verdict" style="display:none"></div> | |
| <div id="bvir-output" class="output" style="display:none"></div> | |
| </div> | |
| </section> | |
| <!-- =================================================================== | |
| SECTION B — Λ-Gated Honest Refusal | |
| =================================================================== --> | |
| <section class="section" id="section-govern"> | |
| <div class="section-head"> | |
| <h2> | |
| <span class="section-label">B</span> | |
| Λ-Gated Honest Refusal | |
| </h2> | |
| <p> | |
| Three preset governance cases. Each returns a REAL signed receipt via | |
| <code>szl_dsse.sign_khipu_receipt</code>. Λ is always labeled | |
| <span class="conj">Conjecture 1 — advisory, NOT a theorem</span>. | |
| </p> | |
| <p class="moat-line">"Even our refusals are signed and explained — no black-box boolean."</p> | |
| </div> | |
| <div class="section-body"> | |
| <div class="btn-row"> | |
| <button class="btn btn-allow" onclick="runGovern('allow')">Allow</button> | |
| <button class="btn btn-review" onclick="runGovern('review')">Review</button> | |
| <button class="btn btn-deny" onclick="runGovern('deny')">Deny</button> | |
| </div> | |
| <div id="govern-status" class="status-line"></div> | |
| <div id="govern-panel" style="display:none"> | |
| <div id="govern-verdict-banner"></div> | |
| <div id="govern-lambda-row" style="margin-bottom:14px"></div> | |
| <div id="govern-gates"></div> | |
| <div id="govern-receipt-block" style="display:none;margin-top:16px"> | |
| <div style="font-size:12px;font-weight:700;color:var(--text-dim);margin-bottom:8px;text-transform:uppercase;letter-spacing:.06em">Signed Denial Receipt</div> | |
| <div id="govern-receipt-output" class="output"></div> | |
| </div> | |
| </div> | |
| </div> | |
| </section> | |
| <!-- =================================================================== | |
| SECTION C — Verifiable Thesis | |
| =================================================================== --> | |
| <section class="section" id="section-thesis"> | |
| <div class="section-head"> | |
| <h2> | |
| <span class="section-label">C</span> | |
| Verifiable Thesis | |
| </h2> | |
| <p> | |
| The 8 PROVEN formulas with verbatim Lean 4 statements, the 3-tier honest corpus | |
| (8 / ~35 / ~185), and the honest conjecture labels for Λ and Khipu BFT. | |
| </p> | |
| <p class="moat-line">"The honesty is the product. Click any formula — verify it yourself."</p> | |
| </div> | |
| <div class="section-body"> | |
| <div class="btn-row"> | |
| <button class="btn btn-primary" id="thesis-load" onclick="loadThesis()"> | |
| Load Formulas & Corpus | |
| </button> | |
| </div> | |
| <div id="thesis-status" class="status-line"></div> | |
| <div id="thesis-panel" style="display:none"> | |
| <!-- corpus diagram --> | |
| <div id="thesis-corpus"></div> | |
| <hr class="divider" /> | |
| <!-- 8 formulas --> | |
| <div style="font-size:13px;font-weight:700;margin-bottom:14px;color:var(--text-dim);text-transform:uppercase;letter-spacing:.07em"> | |
| 8 Kernel-Proven Formulas | |
| </div> | |
| <div id="thesis-formulas" class="formula-grid"></div> | |
| <hr class="divider" /> | |
| <!-- conjecture labels --> | |
| <div id="thesis-conjectures"></div> | |
| </div> | |
| </div> | |
| </section> | |
| <!-- =================================================================== | |
| SECTION D — Public Ledger (real receipts from szl-lake) | |
| =================================================================== --> | |
| <section class="section" id="section-ledger"> | |
| <div class="section-head"> | |
| <h2> | |
| <span class="section-label">D</span> | |
| Public Ledger — Real Receipts | |
| </h2> | |
| <p> | |
| Real signed Khipu receipts from our public dataset | |
| <a href="https://huggingface.co/datasets/SZLHOLDINGS/szl-lake" target="_blank" rel="noopener">SZLHOLDINGS/szl-lake</a> | |
| (snapshot 2026-07-02). This page recomputes the <strong>hash-chain linkage in your browser</strong>; | |
| the DSSE / sigstore signatures verify <strong>offline</strong> with the | |
| <a href="https://pypi.org/project/szl-receipt/" target="_blank" rel="noopener">szl-receipt</a> | |
| library and cross-check against the canonical rows on Hugging Face — infrastructure we do not control. | |
| </p> | |
| <p class="moat-line">"The receipts you would read in diligence — including the ones where we mark our own central claim, Λ, still OPEN."</p> | |
| </div> | |
| <div class="section-body"> | |
| <div class="btn-row"> | |
| <button class="btn btn-primary" id="ledger-load" onclick="renderLedger()"> | |
| Load Public Ledger & Check Chain | |
| </button> | |
| </div> | |
| <div id="ledger-status" class="status-line"></div> | |
| <div id="ledger-panel" style="display:none"> | |
| <div id="ledger-chain"></div> | |
| <hr class="divider" /> | |
| <div id="ledger-cards"></div> | |
| </div> | |
| </div> | |
| </section> | |
| </main> | |
| <footer class="footer"> | |
| <p>SZL Holdings · a11oy · Doctrine v11 · 8 kernel-verified formulas @ c7c0ba17 · | |
| Λ = Conjecture 1 (advisory) · Khipu BFT = Conjecture 2 · | |
| <a href="/govern/health" target="_blank">Governance Health</a> · | |
| <a href="/api/a11oy/v1/demo/thesis" target="_blank">Thesis API</a> | |
| </p> | |
| </footer> | |
| <!-- =================================================================== | |
| JAVASCRIPT — all in-browser, no CDN | |
| =================================================================== --> | |
| <script> | |
| ; | |
| /* ---- utility ---- */ | |
| function el(id) { return document.getElementById(id); } | |
| function show(id) { const e = el(id); if (e) e.style.display = ''; } | |
| function hide(id) { const e = el(id); if (e) e.style.display = 'none'; } | |
| function setText(id, txt) { const e = el(id); if (e) e.textContent = txt; } | |
| function setHTML(id, html) { const e = el(id); if (e) e.innerHTML = html; } | |
| function setStatus(id, msg, loading) { | |
| const e = el(id); | |
| if (!e) return; | |
| if (loading) { | |
| e.innerHTML = '<span class="spinner"></span>' + escHTML(msg); | |
| } else { | |
| e.textContent = msg; | |
| } | |
| } | |
| function escHTML(s) { | |
| return String(s) | |
| .replace(/&/g,'&') | |
| .replace(/</g,'<') | |
| .replace(/>/g,'>') | |
| .replace(/"/g,'"'); | |
| } | |
| /* ---- base64 helpers ---- */ | |
| function b64Decode(s) { | |
| // standard base64 → Uint8Array (not URL-safe; WebCrypto importKey returns SPKI base64) | |
| const bin = atob(s); | |
| const b = new Uint8Array(bin.length); | |
| for (let i = 0; i < bin.length; i++) b[i] = bin.charCodeAt(i); | |
| return b; | |
| } | |
| function b64Encode(buf) { | |
| let s = ''; | |
| const b = new Uint8Array(buf); | |
| for (let i = 0; i < b.length; i++) s += String.fromCharCode(b[i]); | |
| return btoa(s); | |
| } | |
| /* ---- DER ASN.1 → raw r‖s converter (for WebCrypto ECDSA P-256) ---- | |
| cosign / cryptography-lib ECDSA signs in DER (ASN.1 SEQUENCE { INTEGER r, INTEGER s }). | |
| WebCrypto ECDSA P-256 SHA-256 expects IEEE P-1363 raw r‖s (64 bytes: 32+32). | |
| We decode the DER SEQUENCE here entirely in JS — no library needed. | |
| */ | |
| function derToRaw(derBytes) { | |
| let i = 0; | |
| if (derBytes[i++] !== 0x30) throw new Error('not DER SEQUENCE'); | |
| // Length (short form or long form) | |
| let seqLen = derBytes[i++]; | |
| if (seqLen & 0x80) { | |
| const nb = seqLen & 0x7f; | |
| seqLen = 0; | |
| for (let b = 0; b < nb; b++) seqLen = (seqLen << 8) | derBytes[i++]; | |
| } | |
| function readInt() { | |
| if (derBytes[i++] !== 0x02) throw new Error('expected INTEGER tag'); | |
| let len = derBytes[i++]; | |
| if (len & 0x80) { | |
| const nb = len & 0x7f; len = 0; | |
| for (let b = 0; b < nb; b++) len = (len << 8) | derBytes[i++]; | |
| } | |
| const val = derBytes.slice(i, i + len); i += len; | |
| return val; | |
| } | |
| const rArr = readInt(); | |
| const sArr = readInt(); | |
| // Pad / strip prefix zero byte (ASN.1 adds 0x00 prefix when high-bit is set) | |
| function pad32(arr) { | |
| // strip prefix 0x00 byte | |
| let j = 0; | |
| while (j < arr.length - 1 && arr[j] === 0) j++; | |
| const stripped = arr.slice(j); | |
| const out = new Uint8Array(32); | |
| const off = 32 - stripped.length; | |
| if (off < 0) throw new Error('integer too long: ' + stripped.length); | |
| out.set(stripped, off); | |
| return out; | |
| } | |
| const raw = new Uint8Array(64); | |
| raw.set(pad32(rArr), 0); | |
| raw.set(pad32(sArr), 32); | |
| return raw; | |
| } | |
| /* ---- DSSE PAE ---- | |
| PAE(type, body) = "DSSEv1" SP LEN(type) SP type SP LEN(body) SP body | |
| Exactly mirrors szl_dsse.pae() | |
| */ | |
| function buildPAE(payloadType, bodyBytes) { | |
| const enc = new TextEncoder(); | |
| const t = enc.encode(payloadType); | |
| const prefix = enc.encode(`DSSEv1 ${t.length} `); | |
| const mid = enc.encode(` ${bodyBytes.length} `); | |
| const total = prefix.length + t.length + mid.length + bodyBytes.length; | |
| const buf = new Uint8Array(total); | |
| let off = 0; | |
| buf.set(prefix, off); off += prefix.length; | |
| buf.set(t, off); off += t.length; | |
| buf.set(mid, off); off += mid.length; | |
| buf.set(bodyBytes, off); | |
| return buf; | |
| } | |
| /* ---- SHA-256 via WebCrypto ---- */ | |
| async function sha256(data) { | |
| const hash = await crypto.subtle.digest('SHA-256', data); | |
| return Array.from(new Uint8Array(hash)).map(b => b.toString(16).padStart(2,'0')).join(''); | |
| } | |
| /* ---- Import P-256 SPKI public key from PEM ---- */ | |
| async function importPubKeyFromPEM(pem) { | |
| const b64 = pem | |
| .replace('-----BEGIN PUBLIC KEY-----','') | |
| .replace('-----END PUBLIC KEY-----','') | |
| .replace(/\s+/g,''); | |
| const raw = b64Decode(b64); | |
| return crypto.subtle.importKey( | |
| 'spki', raw.buffer, | |
| { name: 'ECDSA', namedCurve: 'P-256' }, | |
| false, ['verify'] | |
| ); | |
| } | |
| /* ==================================================================== | |
| SECTION A — BVIR | |
| ==================================================================== */ | |
| async function runBVIR() { | |
| const btn = el('bvir-run'); | |
| btn.disabled = true; | |
| hide('bvir-verdict'); | |
| hide('bvir-output'); | |
| setStatus('bvir-status', 'Calling /api/a11oy/v1/govern/infer …', true); | |
| let data; | |
| try { | |
| const resp = await fetch('/api/a11oy/v1/govern/infer', { | |
| method: 'POST', | |
| headers: { 'Content-Type': 'application/json' }, | |
| body: JSON.stringify({ prompt: 'hello', vertical: 'general', declared: 'PUBLIC' }) | |
| }); | |
| data = await resp.json(); | |
| } catch(e) { | |
| setStatus('bvir-status', 'Error calling govern/infer: ' + e.message); | |
| btn.disabled = false; | |
| return; | |
| } | |
| setStatus('bvir-status', 'Verifying signature in-browser via WebCrypto …', true); | |
| const dsse = data.dsse || {}; | |
| const receipt= data.receipt|| {}; | |
| // A demo-signed receipt is signed by the clearly-labelled demo-signing-key, NOT | |
| // the production founder-gated cosign key. We must verify it against the DEMO | |
| // public key (/demo-cosign.pub), and the badge must say so explicitly. | |
| const dsseKeyid = ((dsse.signatures || [])[0] || {}).keyid || dsse.key_id || ''; | |
| const isDemoKey = dsseKeyid === 'demo-signing-key'; | |
| const pubKeyURL = isDemoKey ? '/demo-cosign.pub' : '/cosign.pub'; | |
| // Step 1: Fetch the matching public key (production cosign.pub, or demo-cosign.pub) | |
| let pubKey; | |
| let pubKeyPEM = ''; | |
| try { | |
| const pkResp = await fetch(pubKeyURL); | |
| pubKeyPEM = await pkResp.text(); | |
| pubKey = await importPubKeyFromPEM(pubKeyPEM); | |
| } catch(e) { | |
| setStatus('bvir-status', 'Could not fetch/import ' + pubKeyURL + ': ' + e.message); | |
| btn.disabled = false; | |
| return; | |
| } | |
| // Step 2: Decode payload bytes | |
| const payloadType = dsse.payloadType || 'application/vnd.szl.khipu+json'; | |
| let payloadBytes; | |
| try { | |
| payloadBytes = b64Decode(dsse.payload || ''); | |
| } catch(e) { | |
| setStatus('bvir-status', 'Could not decode dsse.payload: ' + e.message); | |
| btn.disabled = false; | |
| return; | |
| } | |
| // Step 3: Recompute SHA-256 of decoded payload | |
| const payloadDigestComputed = await sha256(payloadBytes.buffer); | |
| // Step 4: PAE and verify signature | |
| const paeBytes = buildPAE(payloadType, payloadBytes); | |
| const paeSHA = await sha256(paeBytes.buffer); | |
| const sigs = dsse.signatures || []; | |
| let verified = false; | |
| let verifyError = ''; | |
| let sigKeyid = ''; | |
| if (!dsse.signed) { | |
| verifyError = 'UNSIGNED envelope — private key not available in this runtime. Receipt chain is still valid.'; | |
| } else if (sigs.length === 0) { | |
| verifyError = 'No signatures in envelope.'; | |
| } else { | |
| const sigEntry = sigs[0]; | |
| sigKeyid = sigEntry.keyid || ''; | |
| try { | |
| // Try IEEE P-1363 raw first; if that fails, try DER | |
| const sigBytes = b64Decode(sigEntry.sig || ''); | |
| let rawSig = sigBytes; | |
| // Detect DER: starts with 0x30 | |
| if (sigBytes[0] === 0x30) { | |
| try { | |
| rawSig = derToRaw(sigBytes); | |
| } catch(e2) { | |
| verifyError = 'DER→raw conversion failed: ' + e2.message; | |
| } | |
| } | |
| if (!verifyError) { | |
| verified = await crypto.subtle.verify( | |
| { name: 'ECDSA', hash: 'SHA-256' }, | |
| pubKey, | |
| rawSig.buffer, | |
| paeBytes.buffer | |
| ); | |
| if (!verified) { | |
| // Try without DER conversion (in case it was already raw) | |
| if (sigBytes[0] === 0x30) { | |
| verified = await crypto.subtle.verify( | |
| { name: 'ECDSA', hash: 'SHA-256' }, | |
| pubKey, | |
| sigBytes.buffer, | |
| paeBytes.buffer | |
| ); | |
| } | |
| } | |
| if (!verified) verifyError = 'ECDSA verification returned false.'; | |
| } | |
| } catch(e) { | |
| verifyError = 'Signature verify error: ' + e.message; | |
| } | |
| } | |
| // Step 5: Hash-chain check | |
| // IMPORTANT: keep the receipt's DECLARED payload digest separate from the | |
| // chain/receipt id. receipt.digest is the chain id; receipt.payload_digest is | |
| // the digest the receipt DECLARES for its payload. The MATCH/MISMATCH chip must | |
| // compare the recomputed payload sha256 against the DECLARED payload digest only, | |
| // never against the chain id (that comparison is meaningless and would show a | |
| // spurious red MISMATCH next to a genuinely VERIFIED signature). | |
| const declaredPayloadDigest = String(receipt.payload_digest || '').toLowerCase(); | |
| const hasDeclaredDigest = declaredPayloadDigest.length > 0; | |
| const payloadDigestMatches = hasDeclaredDigest && | |
| (payloadDigestComputed.toLowerCase() === declaredPayloadDigest); | |
| const chainPrev = receipt.prev || '(genesis)'; | |
| const chainDigest = receipt.digest || ''; | |
| // Build result UI | |
| let verdictHTML = ''; | |
| if (verified && isDemoKey) { | |
| verdictHTML = `<div class="verdict-banner verdict-ok"> | |
| ✓ VERIFIED (demo-signing-key — not the production cosign key) | |
| <span class="chip chip-ok">keyid: ${escHTML(sigKeyid)}</span> | |
| <div style="font-size:12px;font-weight:400;margin-top:6px;color:var(--text-dim)"> | |
| Real ECDSA-P256 signature, verified in your browser against /demo-cosign.pub. | |
| This is a clearly-labelled DEMO key — the production cosign key stays | |
| founder-gated and is never placed in this runtime. | |
| </div> | |
| </div>`; | |
| } else if (verified) { | |
| verdictHTML = `<div class="verdict-banner verdict-ok"> | |
| ✓ VERIFIED — WebCrypto ECDSA-P256 signature valid | |
| <span class="chip chip-ok">keyid: ${escHTML(sigKeyid)}</span> | |
| </div>`; | |
| } else if (!dsse.signed) { | |
| verdictHTML = `<div class="verdict-banner verdict-dim"> | |
| ⚠ UNSIGNED — private key not in runtime; receipt chain still valid | |
| </div>`; | |
| } else { | |
| verdictHTML = `<div class="verdict-banner verdict-fail"> | |
| ✗ VERIFICATION FAILED — ${escHTML(verifyError)} | |
| </div>`; | |
| } | |
| // Two clearly separate, non-contradictory results: | |
| // (1) signature verify -> shown in the verdict banner above | |
| // (2) payload-digest match -> computed sha256 vs the receipt's DECLARED payload_digest | |
| // When the receipt declares no payload_digest we show an honest neutral state, | |
| // NEVER a red MISMATCH. | |
| let digestChipClass, digestChipText, digestValClass; | |
| if (!hasDeclaredDigest) { | |
| digestChipClass = 'chip-dim'; | |
| digestChipText = 'NO DECLARED DIGEST'; | |
| digestValClass = ''; | |
| } else if (payloadDigestMatches) { | |
| digestChipClass = 'chip-ok'; | |
| digestChipText = 'MATCH'; | |
| digestValClass = 'hash-match'; | |
| } else { | |
| digestChipClass = 'chip-err'; | |
| digestChipText = 'MISMATCH'; | |
| digestValClass = 'hash-mismatch'; | |
| } | |
| verdictHTML += ` | |
| <div style="margin-bottom:12px"> | |
| <div class="hash-row"> | |
| <span class="hash-label">Signature verify:</span> | |
| <span class="chip ${verified ? 'chip-ok' : (dsse.signed === false ? 'chip-dim' : 'chip-err')}">${verified ? 'VERIFIED' : (dsse.signed === false ? 'UNSIGNED' : 'FAILED')}</span> | |
| </div> | |
| <div class="hash-row"> | |
| <span class="hash-label">Payload digest:</span> | |
| <span class="hash-val ${digestValClass}">${payloadDigestComputed.substring(0,32)}…</span> | |
| <span class="chip ${digestChipClass}">${digestChipText}</span> | |
| </div> | |
| ${hasDeclaredDigest ? `<div class="hash-row"> | |
| <span class="hash-label">Declared digest:</span> | |
| <span class="hash-val">${escHTML(declaredPayloadDigest.substring(0,32))}…</span> | |
| </div>` : `<div class="hash-row"> | |
| <span class="hash-label">Declared digest:</span> | |
| <span class="hash-val" style="color:var(--text-dim)">(none declared — nothing to compare against)</span> | |
| </div>`} | |
| <div class="hash-row"> | |
| <span class="hash-label">PAE SHA-256:</span> | |
| <span class="hash-val">${paeSHA.substring(0,32)}…</span> | |
| </div> | |
| <div class="hash-row"> | |
| <span class="hash-label">Chain prev:</span> | |
| <span class="hash-val">${escHTML(String(chainPrev).substring(0,32))}…</span> | |
| </div> | |
| <div class="hash-row"> | |
| <span class="hash-label">Chain digest:</span> | |
| <span class="hash-val">${escHTML(String(chainDigest).substring(0,32))}…</span> | |
| </div> | |
| </div> | |
| <div style="font-size:12px;color:var(--text-dim);margin-bottom:8px"> | |
| <span class="conj">Λ Conjecture 1 — advisory</span> | |
| Λ = ${escHTML(String((data.governance||{}).lambda ?? 'N/A'))} | |
| · | |
| Energy: <span class="chip chip-dim">${escHTML((data.energy||{}).label || 'UNAVAILABLE')}</span> | |
| </div> | |
| `; | |
| setHTML('bvir-verdict', verdictHTML); | |
| show('bvir-verdict'); | |
| const outputData = { | |
| decision: data.decision, | |
| 'governance.lambda': (data.governance||{}).lambda, | |
| 'governance.lambda_kind': (data.governance||{}).lambda_kind, | |
| 'receipt.seq': receipt.seq, | |
| 'receipt.prev': String(chainPrev).substring(0,32) + '…', | |
| 'receipt.digest': String(chainDigest).substring(0,32) + '…', | |
| 'dsse.signed': dsse.signed, | |
| 'dsse.keyid': dsseKeyid || null, | |
| 'dsse.key_kind': isDemoKey ? 'demo (demo-signing-key — NOT production cosign)' : (dsse.signed ? 'production cosign' : null), | |
| 'dsse.payloadType': dsse.payloadType, | |
| 'verify.public_key_url': pubKeyURL, | |
| 'verify.computed_payload_sha256': payloadDigestComputed.substring(0,32) + '…', | |
| 'verify.declared_payload_digest': hasDeclaredDigest ? declaredPayloadDigest.substring(0,32) + '…' : null, | |
| 'verify.payload_digest_match': hasDeclaredDigest ? (payloadDigestMatches ? 'MATCH' : 'MISMATCH') : 'no declared digest to compare', | |
| 'verify.pae_sha256': paeSHA.substring(0,32) + '…', | |
| 'verify.result': verified ? (isDemoKey ? 'VERIFIED ✓ (demo-signing-key — not production cosign)' : 'VERIFIED ✓') : (dsse.signed === false ? 'UNSIGNED (no private key in runtime)' : 'FAILED: ' + verifyError), | |
| 'energy.label': (data.energy||{}).label, | |
| }; | |
| el('bvir-output').textContent = JSON.stringify(outputData, null, 2); | |
| show('bvir-output'); | |
| el('bvir-output').className = 'output ' + (verified ? 'verified' : (dsse.signed === false ? '' : 'failed')); | |
| setStatus('bvir-status', verified | |
| ? (isDemoKey | |
| ? '✓ WebCrypto verified — real ECDSA-P256 over DSSE PAE with demo-signing-key (NOT the production cosign key).' | |
| : '✓ WebCrypto verified — real ECDSA-P256 signature over DSSE PAE.') | |
| : (dsse.signed === false | |
| ? 'Unsigned receipt (private key absent from runtime). Chain valid.' | |
| : 'Verification result: ' + verifyError)); | |
| btn.disabled = false; | |
| } | |
| /* ==================================================================== | |
| SECTION B — Governed Refusal | |
| ==================================================================== */ | |
| async function runGovern(caseKey) { | |
| hide('govern-panel'); | |
| setStatus('govern-status', `Calling /api/a11oy/v1/demo/govern case="${caseKey}" …`, true); | |
| let data; | |
| try { | |
| const resp = await fetch('/api/a11oy/v1/demo/govern', { | |
| method: 'POST', | |
| headers: { 'Content-Type': 'application/json' }, | |
| body: JSON.stringify({ case: caseKey }) | |
| }); | |
| data = await resp.json(); | |
| } catch(e) { | |
| setStatus('govern-status', 'Error: ' + e.message); | |
| return; | |
| } | |
| const gov = data.governance || {}; | |
| const receipt = data.receipt || {}; | |
| const dsse = data.dsse || {}; | |
| const chain = data.chain || {}; | |
| const decision = data.decision || caseKey; | |
| // Verdict banner | |
| const decClasses = { allow:'verdict-ok', review:'verdict-dim', deny:'verdict-fail' }; | |
| const decLabels = { allow:'✓ ALLOW — governance passed', review:'⚠ REVIEW — below advisory floor', deny:'✗ DENY — gate fired' }; | |
| const bannerCls = decClasses[decision] || 'verdict-dim'; | |
| const bannerLbl = decLabels[decision] || decision.toUpperCase(); | |
| el('govern-verdict-banner').innerHTML = `<div class="verdict-banner ${bannerCls}">${bannerLbl}</div>`; | |
| // Λ row | |
| const lambdaPass = gov.lambda_pass; | |
| el('govern-lambda-row').innerHTML = ` | |
| <div style="display:flex;align-items:center;gap:10px;flex-wrap:wrap"> | |
| <span style="font-size:14px;font-weight:700">Λ = ${escHTML(String(gov.lambda ?? 'N/A'))}</span> | |
| <span class="chip ${lambdaPass ? 'chip-ok' : 'chip-err'}"> | |
| ${lambdaPass ? 'PASS' : 'FAIL'} (floor ${escHTML(String(gov.lambda_floor ?? 0.9))}) | |
| </span> | |
| <span class="conj">Conjecture 1 — advisory, NOT a theorem</span> | |
| </div> | |
| <div style="font-size:12px;color:var(--text-dim);margin-top:4px"> | |
| ${escHTML(gov.lambda_kind || 'Conjecture 1 (advisory; NOT a theorem)')} | |
| </div> | |
| `; | |
| // Gates | |
| const gates = gov.gates || []; | |
| let gatesHTML = `<div style="font-size:11px;font-weight:700;text-transform:uppercase;letter-spacing:.07em;color:var(--text-dim);margin-bottom:8px">Gates</div>`; | |
| gates.forEach(g => { | |
| const fired = g.fired; | |
| gatesHTML += ` | |
| <div class="gate-row"> | |
| <span class="gate-name">${escHTML(g.name || '—')}</span> | |
| <span class="gate-fired ${fired ? 'chip chip-err' : 'chip chip-ok'}">${fired ? 'FIRED' : 'PASS'}</span> | |
| <span class="chip chip-dim">${escHTML(g.decision || '—')}</span> | |
| </div>`; | |
| }); | |
| el('govern-gates').innerHTML = gatesHTML; | |
| // Signed receipt on deny | |
| if (decision === 'deny' || decision === 'review') { | |
| const signed = dsse.signed; | |
| const receiptOut = { | |
| decision: receipt.decision, | |
| seq: receipt.seq, | |
| lambda: receipt.lambda, | |
| lambda_kind: receipt.lambda_kind, | |
| gates: receipt.gates, | |
| prev: String(chain.prev || '').substring(0,32) + '…', | |
| digest: String(chain.digest || '').substring(0,32) + '…', | |
| 'dsse.signed': signed, | |
| 'dsse.keyid': ((dsse.signatures||[])[0]||{}).keyid, | |
| honesty: data.honesty, | |
| }; | |
| el('govern-receipt-output').className = 'output ' + (signed ? 'verified' : ''); | |
| el('govern-receipt-output').textContent = JSON.stringify(receiptOut, null, 2); | |
| show('govern-receipt-block'); | |
| } else { | |
| hide('govern-receipt-block'); | |
| } | |
| show('govern-panel'); | |
| setStatus('govern-status', `Decision: ${decision.toUpperCase()} · Λ = ${gov.lambda} · ${dsse.signed ? 'Receipt signed ✓' : 'Receipt unsigned (key absent)'}`); | |
| } | |
| /* ==================================================================== | |
| SECTION C — Verifiable Thesis | |
| ==================================================================== */ | |
| async function loadThesis() { | |
| const btn = el('thesis-load'); | |
| btn.disabled = true; | |
| hide('thesis-panel'); | |
| setStatus('thesis-status', 'Loading /api/a11oy/v1/demo/thesis …', true); | |
| let data; | |
| try { | |
| const resp = await fetch('/api/a11oy/v1/demo/thesis'); | |
| data = await resp.json(); | |
| } catch(e) { | |
| setStatus('thesis-status', 'Error: ' + e.message); | |
| btn.disabled = false; | |
| return; | |
| } | |
| const corpus = data.corpus || {}; | |
| const formulas = data.formulas || []; | |
| const doctrine = data.doctrine_static || {}; | |
| // ---- Corpus diagram ---- | |
| const tiers = corpus.tiers || []; | |
| const corpusColors = ['proven','gates','total']; | |
| let corpusHTML = `<div style="font-size:13px;font-weight:700;margin-bottom:14px;color:var(--text-dim);text-transform:uppercase;letter-spacing:.07em">3-Tier Honest Corpus</div>`; | |
| corpusHTML += `<div class="corpus-diagram">`; | |
| tiers.forEach((t, idx) => { | |
| corpusHTML += ` | |
| <div class="corpus-tier"> | |
| <div class="corpus-count ${corpusColors[idx] || ''}">${escHTML(String(t.count))}</div> | |
| <div class="corpus-tier-label">${escHTML(t.label || '')}</div> | |
| <div class="corpus-tier-desc">${escHTML(t.description || '')}</div> | |
| </div>`; | |
| }); | |
| corpusHTML += `</div>`; | |
| corpusHTML += `<div class="corpus-never-claim"> | |
| ⚠ ${escHTML(corpus.honest_note || 'We never claim 183 proven.')} | |
| </div>`; | |
| el('thesis-corpus').innerHTML = corpusHTML; | |
| // ---- 8 formulas ---- | |
| let formulasHTML = ''; | |
| formulas.forEach(f => { | |
| formulasHTML += ` | |
| <div class="formula-card"> | |
| <div class="formula-card-head"> | |
| <span class="formula-id">${escHTML(f.id)}</span> | |
| <span class="formula-name">${escHTML(f.name)}</span> | |
| </div> | |
| <div class="formula-lean">${escHTML(f.lean)}</div> | |
| <div class="formula-desc">${escHTML(f.description)}</div> | |
| <div class="formula-status">✓ ${escHTML(f.status)}</div> | |
| </div>`; | |
| }); | |
| el('thesis-formulas').innerHTML = formulasHTML; | |
| // ---- Conjecture labels ---- | |
| el('thesis-conjectures').innerHTML = ` | |
| <div style="font-size:13px;font-weight:700;margin-bottom:12px;color:var(--text-dim);text-transform:uppercase;letter-spacing:.07em"> | |
| Advisory / Conjecture Labels | |
| </div> | |
| <div style="display:flex;gap:14px;flex-wrap:wrap"> | |
| <div style="flex:1;min-width:220px;background:var(--bg-panel);border:1px solid #92400e;border-radius:var(--radius);padding:14px"> | |
| <div style="font-size:11px;font-weight:700;color:var(--amber);text-transform:uppercase;letter-spacing:.07em;margin-bottom:6px">Conjecture 1 — Λ (Lambda)</div> | |
| <div style="font-size:13px;color:var(--text-dim)">${escHTML(doctrine.lambda_kind || 'Conjecture 1 (advisory; NOT a theorem)')}</div> | |
| <div style="font-size:12px;color:var(--text-mute);margin-top:6px">Open bounty: szl-holdings/lambda-bounty</div> | |
| </div> | |
| <div style="flex:1;min-width:220px;background:var(--bg-panel);border:1px solid #991b1b;border-radius:var(--radius);padding:14px"> | |
| <div style="font-size:11px;font-weight:700;color:var(--red);text-transform:uppercase;letter-spacing:.07em;margin-bottom:6px">Conjecture 2 — Khipu BFT</div> | |
| <div style="font-size:13px;color:var(--text-dim)">${escHTML(doctrine.bft_kind || 'Conjecture 2 (NOT proven; NOT a theorem)')}</div> | |
| <div style="font-size:12px;color:var(--text-mute);margin-top:6px">Labeled honestly everywhere — no false safety claim</div> | |
| </div> | |
| </div> | |
| <div style="margin-top:14px;font-size:12px;color:var(--text-dim)"> | |
| ${escHTML(doctrine.moat_line || '')} | |
| </div> | |
| `; | |
| show('thesis-panel'); | |
| setStatus('thesis-status', `Loaded ${formulas.length} proven formulas · 3-tier corpus · live doctrine`); | |
| btn.disabled = false; | |
| } | |
| /* ==================================================================== | |
| SECTION D — Public Ledger (real receipts from szl-lake, snapshot) | |
| In-browser: hash-chain linkage check. Offline: signatures via szl-receipt. | |
| ==================================================================== */ | |
| const LEDGER_SNAPSHOT = {"source": "https://huggingface.co/datasets/SZLHOLDINGS/szl-lake", "captured_utc": "2026-07-02", "lutar_lean": [{"branch": "theorem-u-kernel", "chain_index": 1, "doctrine": "v11", "honesty": {"conjecture_1": "OPEN: unconditional Lambda uniqueness is Conjecture 1 and is machine-checked FALSE as stated. Theorem U does NOT close it.", "doctrine": "v11", "locked_five_unchanged": true, "locked_set": ["F1", "F11", "F12", "F18", "F19"], "theorem_u": "REAL-conditional: Lutar.Uniqueness Theorem U is kernel-verified (axiom footprint within the Lean/Mathlib trust base, no sorry) but CONDITIONAL on its stated checkable hypotheses; it is NOT part of the locked-proven baseline."}, "kernel_commit": "e736decd244ae06e8bb48531c6c7dc0f1029b25a", "kernel_commit_short": "e736decd244a", "kind": "theorem-u-anchor", "lambda_status": "Conjecture_1 (OPEN; unconditional uniqueness machine-checked FALSE)", "numbers": {"axioms_unique": 22, "declarations": 1323, "sorries_noncomment": 254}, "organ": "lutar-lean", "prev_hash": null, "receipt_id": "d70f444db57df9a4a2d52e69408ce61b511e4b50152f7fbf97456b1af66fe9a0", "schema": "szl.khipu.receipt/v1", "signing": {"format": "sigstore-keyless-bundle", "bytes": 18428, "b64_head": "eyJtZWRpYVR5cGUiOiJhcHBsaWNhdGlvbi92bmQuZGV2\u2026"}, "source_run": {"conclusion": "success", "id": "27186151340", "url": "https://github.com/szl-holdings/lutar-lean/actions/runs/27186151340", "workflow": "Lake build (gate + numbers)"}, "subject": {"name": "theorem_u_snapshot.json", "sha256": "82d08a4e892579e815d880d51f61cb8035a3325e077c29e412f310f76b50985e", "snapshot": {"branch": "theorem-u-kernel", "built_at_utc": "2026-06-09T05:37:45Z", "honesty": {"conjecture_1": "OPEN: unconditional Lambda uniqueness is Conjecture 1 and is machine-checked FALSE as stated. Theorem U does NOT close it.", "doctrine": "v11", "locked_five_unchanged": true, "locked_set": ["F1", "F11", "F12", "F18", "F19"], "theorem_u": "REAL-conditional: Lutar.Uniqueness Theorem U is kernel-verified (axiom footprint within the Lean/Mathlib trust base, no sorry) but CONDITIONAL on its stated checkable hypotheses; it is NOT part of the locked-proven baseline."}, "kernel_commit": "e736decd244ae06e8bb48531c6c7dc0f1029b25a", "kernel_commit_short": "e736decd244a", "lean_numbers": {"lean_numbers_sha256": "50098073e92aefdf275ec53e60faafc0f1bd5d4a1a88023e819490aaaa69d4d6", "numbers": {"axiom_names": ["A6'_block_consistent", "KS_theorem_1_1", "MomentSubGaussian", "audit_reidemeister_invariance", "canonicalReceipt", "chromotopology_code_bijection", "compression_collision_resistant", "domain_separation", "gleason_length_mod_8", "klDivergence_nonneg", "lambda_schur_concave_n_axis", "lambda_stationary_unique", "leaf_collision_resistant", "liu_hui_pi_converges", "node_collision_resistant", "pinsker", "r1_invariance", "r2_invariance", "setAlpha_cauchy", "setDelta_stage2", "sha256", "sha256_collision_resistant"], "axioms_raw": 23, "axioms_unique": 22, "declarations": 1323, "sorries_baseline": 251, "sorries_noncomment": 254, "sorries_putnam": 56, "sorries_raw": 307}, "reference_vectors_sha256": "857967629daf5e5c45a167306ea0e0091569a29766b01ac91bef15a539b816dc", "replay_hash": "9860c3332a2d0b0553b775dcd27111b0ce4fae4bc5cebe2827dc6148be4cbebe", "schema": "szl.lean_numbers/v1"}, "repo": "szl-holdings/lutar-lean", "schema": "szl.theorem_u.snapshot/v1", "theorem_u": {"decl_source_sha256": {"Lutar/Uniqueness/AxiomCheck.lean": "f45781ef2becf15eccd0c31702603a55cfab1eb7960483593a045202b66f4887", "Lutar/Uniqueness/Identifiability.lean": "fa340e6a999eac7ea1cd035d90647548baaa290b7376d7fcbdcbd165e475dedf", "Lutar/Uniqueness/LambdaEquiv.lean": "03f63e36f3a9b19e8e9d4f48313a450bae7c85fcb53049d52e0f6d4adf4b1c23", "Lutar/Uniqueness/TheoremU.lean": "c958520ba31d6fc1f48a9b49871d67812f178e168b31bf2be9e3d5fb2061386c"}, "full_axiom_footprint": {"Lutar.Uniqueness.AxiomCheck.conjecture1_still_open": [], "Lutar.Uniqueness.AxiomCheck.locked_count_five": [], "Lutar.Uniqueness.AxiomCheck.theoremU_axiom_sets_kernel_only": [], "Lutar.Uniqueness.AxiomCheck.theoremU_excluded_from_locked": [], "Lutar.Uniqueness.CorollaryU1_LambdaUnique_Separable": ["Classical.choice", "Quot.sound", "propext"], "Lutar.Uniqueness.CorollaryU2_LambdaUnique_Factors": ["Classical.choice", "Quot.sound", "propext"], "Lutar.Uniqueness.TheoremU_LambdaUnique": ["Classical.choice", "Quot.sound", "propext"], "Lutar.Uniqueness.TheoremU_LambdaUnique_eq": ["Classical.choice", "Quot.sound", "propext"], "Lutar.Uniqueness.identifiability_forces_lambda": ["Classical.choice", "Quot.sound", "propext"], "Lutar.Uniqueness.lambda_equiv_to_eq_of_anchored": ["Classical.choice", "Quot.sound", "propext"]}, "headline_axiom_footprint": {"CorollaryU1_LambdaUnique_Separable": ["Classical.choice", "Quot.sound", "propext"], "CorollaryU2_LambdaUnique_Factors": ["Classical.choice", "Quot.sound", "propext"], "TheoremU_LambdaUnique": ["Classical.choice", "Quot.sound", "propext"], "TheoremU_LambdaUnique_eq": ["Classical.choice", "Quot.sound", "propext"], "identifiability_forces_lambda": ["Classical.choice", "Quot.sound", "propext"], "lambda_equiv_to_eq_of_anchored": ["Classical.choice", "Quot.sound", "propext"]}, "headline_decls": ["CorollaryU1_LambdaUnique_Separable", "CorollaryU2_LambdaUnique_Factors", "TheoremU_LambdaUnique", "TheoremU_LambdaUnique_eq", "identifiability_forces_lambda", "lambda_equiv_to_eq_of_anchored"], "kernel_only": true, "kernel_trust_base": ["Classical.choice", "Quot.sound", "funext", "propext"], "module": "Lutar.Uniqueness", "status": "REAL-conditional"}}}, "theorem_u_status": "REAL-conditional", "timestamp": "2026-06-09T05:39:22Z"}, {"branch": "main", "chain_index": 2, "doctrine": "v11", "honesty": {"conjecture": "This is a GENERATED, OPEN conjecture \u2014 NOT a theorem and NOT machine-verified. It remains OPEN until a solution is independently verified.", "difficulty": "Difficulty 'open-resistant' / grade 'OPEN' come from a REAL bounded solver run. OPEN means searched-to-budget, not proven true; VERIFIED-FINITE certifies only the finite enumerated domain; REFUTED carries a concrete witness. No score is fabricated.", "doctrine": "v11", "kernel_only": false, "novelty": "Novelty verdict 'novel-candidate' is an advisory screen, not a proof of originality; external prior-art sources are labelled live/cached/unreachable and an unreachable source never confirms novelty.", "signing": "Disclosure is cosign keyless-OIDC signed and anchored into the szl-lake DSSE Khipu ledger; the signature attests the timestamp + content, NOT the truth of the conjecture.", "status": "OPEN"}, "kernel_commit": "d851aefe86b9f12f9d4423200bd9e5257d05c41e", "kernel_commit_short": "d851aefe86b9", "kind": "conjecture-disclosure-anchor", "milestone_kind": "conjecture-disclosure", "milestone_status": "OPEN", "milestone_title": "SZL mixing-map convergence conjecture", "numbers": {"axioms_unique": null, "declarations": null, "sorries_noncomment": null}, "organ": "lutar-lean", "prev_hash": "d70f444db57df9a4a2d52e69408ce61b511e4b50152f7fbf97456b1af66fe9a0", "receipt_id": "08744b67b647039f87abbf0b29587638ae777308ca7fc2434ed3ae4033687b50", "schema": "szl.khipu.receipt/v1", "signing": {"format": "sigstore-keyless-bundle", "bytes": 17488, "b64_head": "eyJtZWRpYVR5cGUiOiJhcHBsaWNhdGlvbi92bmQuZGV2\u2026"}, "source_run": {"conclusion": "success", "id": "27318564784", "url": "https://github.com/szl-holdings/lutar-lean/actions/runs/27318564784", "workflow": "Conjecture Factory (generate -> timestamp -> grade -> anchor)"}, "subject": {"name": "conjecture_snapshot.json", "sha256": "7faded7df9ac5bea4ca7ddaa1e5c38c247c237fd49b8a1a39d35a260c2189fb0", "snapshot": {"branch": "main", "built_at_utc": "2026-06-11T01:54:20Z", "candidate": {"created_utc": "2026-06-11T01:54:19Z", "doctrine": "v11", "domain": "number-theory / arithmetic dynamics", "id": "cf-5ddbbe7571a9", "intended_solution_outline": "Bound the orbit by a Lyapunov / drift argument on the 2-adic valuation: show the\ncontracting branch (n = 3 mod 4) dominates the accelerating branch (n = 1 mod 4)\nin expectation, then rule out non-trivial cycles via a residue-class descent.\nStatus: OPEN \u2014 no proof is claimed; the predicate only performs bounded testing.", "predicate": {"description": "Sound bounded-orbit checker: returns False only on a detected non-1 cycle (a certain counterexample); inconclusive bounded runs assert no counterexample.", "entry": "holds", "kind": "python-callable", "module": "conjectures/samples/szl-mixing-map/predicate.py"}, "references": ["conjectures/corpus/collatz.md (related but distinct: classical 3n+1 map)", "Lagarias, J. (2010). The 3x+1 problem: an annotated bibliography."], "schema": "szl.conjecture.candidate/v1", "statement": "Define M : Z+ -> Z+ by\n M(n) = n / 2 if n is even,\n M(n) = (3n + 1) / 2 if n is odd and n = 1 (mod 4),\n M(n) = (n + 1) / 2 if n is odd and n = 3 (mod 4).\nConjecture: for every integer n >= 1 there exists k >= 0 with M^k(n) = 1.", "statement_canonical": "Define M : Z+ -> Z+ by M(n) = n / 2 if n is even, M(n) = (3n + 1) / 2 if n is odd and n = 1 (mod 4), M(n) = (n + 1) / 2 if n is odd and n = 3 (mod 4). Conjecture: for every integer n >= 1 there exists k >= 0 with M^k(n) = 1.", "statement_hash": "sha256:5ddbbe7571a93f9ed3d49c37dbb3559eb339a51380e427882bd3783b7cb2743a", "taxonomy": "OPEN", "title": "SZL mixing-map convergence conjecture"}, "grade": {"budget": 100000, "candidate_id": "cf-5ddbbe7571a9", "difficulty": "open-resistant", "graded_utc": "2026-06-11T01:54:20Z", "honesty": "Grade from a REAL ensemble run. REFUTED carries a concrete witness. VERIFIED-FINITE certifies only the finite enumerated domain, not the conjecture in general. OPEN means searched-to-budget with no counterexample \u2014 NOT a proof of truth. The candidate stays OPEN (doctrine v11).", "result": "OPEN", "schema": "szl.conjecture.grade/v1", "seed": 1729, "solver_ensemble": [{"budget": 100000, "checked": 100000, "elapsed_sec": 0.411268, "note": "infinite/streaming domain", "resolved": false, "result": "OPEN", "solver": "exhaustive", "witness": null}, {"budget": 100000, "checked": 100000, "elapsed_sec": 0.654207, "note": "random sampling found no counterexample (not a proof)", "resolved": false, "result": "OPEN", "solver": "sampler", "witness": null}], "success_rate": 0.0, "witness": null}, "honesty": {"conjecture": "This is a GENERATED, OPEN conjecture \u2014 NOT a theorem and NOT machine-verified. It remains OPEN until a solution is independently verified.", "difficulty": "Difficulty 'open-resistant' / grade 'OPEN' come from a REAL bounded solver run. OPEN means searched-to-budget, not proven true; VERIFIED-FINITE certifies only the finite enumerated domain; REFUTED carries a concrete witness. No score is fabricated.", "doctrine": "v11", "kernel_only": false, "novelty": "Novelty verdict 'novel-candidate' is an advisory screen, not a proof of originality; external prior-art sources are labelled live/cached/unreachable and an unreachable source never confirms novelty.", "signing": "Disclosure is cosign keyless-OIDC signed and anchored into the szl-lake DSSE Khipu ledger; the signature attests the timestamp + content, NOT the truth of the conjecture.", "status": "OPEN"}, "kernel_commit": "d851aefe86b9f12f9d4423200bd9e5257d05c41e", "kernel_commit_short": "d851aefe86b9", "kind": "conjecture-disclosure", "milestone": {"difficulty": "open-resistant", "grade_result": "OPEN", "headline_decls": [], "id": "cf-5ddbbe7571a9", "kernel_only": false, "novelty_verdict": "novel-candidate", "release_stage": "statement", "statement_hash": "sha256:5ddbbe7571a93f9ed3d49c37dbb3559eb339a51380e427882bd3783b7cb2743a", "status": "OPEN", "title": "SZL mixing-map convergence conjecture"}, "novelty": {"candidate_id": "cf-5ddbbe7571a9", "external": [{"hits": 0, "note": "offline run (--online not set)", "source": "arxiv", "status": "unreachable", "top": []}, {"hits": 0, "note": "offline run (--online not set)", "source": "crossref", "status": "unreachable", "top": []}], "honesty": "Novelty is a screen, not a proof of originality. External sources are labelled live/cached/unreachable; an unreachable source contributes no hits and is never silently treated as confirming novelty. The candidate stays OPEN regardless of this verdict (doctrine v11).", "local_corpus": {"corpus_dir": "conjectures/corpus", "documents_scanned": 2, "max_similarity": 0.0688, "method": "char-5-gram shingle Jaccard", "near_duplicate": false, "nearest": {"doc": "collatz.md", "similarity": 0.0688}, "threshold": 0.8, "top": [{"doc": "collatz.md", "similarity": 0.0688}, {"doc": "goldbach.md", "similarity": 0.0451}]}, "schema": "szl.conjecture.novelty/v1", "screened_utc": "2026-06-11T01:54:19Z", "statement_hash": "sha256:5ddbbe7571a93f9ed3d49c37dbb3559eb339a51380e427882bd3783b7cb2743a", "verdict": "novel-candidate", "verdict_reason": "no near-duplicate found (local-only; external prior-art not fully screened \u2014 unreachable: ['arxiv', 'crossref'])"}, "predicate_type": "https://szl-holdings/conjecture-disclosure/v1", "repo": "szl-holdings/lutar-lean", "schema": "szl.conjecture.disclosure/v1"}}, "timestamp": "2026-06-11T01:54:27Z"}, {"branch": "main", "chain_index": 3, "doctrine": "v11", "honesty": {"conjecture_1": "OPEN: unconditional Lambda uniqueness is Conjecture 1 and is machine-checked FALSE as stated; conjecture1_still_open re-asserts it stays open.", "doctrine": "v11", "locked_baseline": "REAL-invariant: kernel-verified meta-theorems in Lutar/Uniqueness/AxiomCheck.lean (locked_count_eight, theoremU_excluded_from_locked, theoremU_axiom_sets_kernel_only, conjecture1_still_open) \u2014 each proven by `decide`, axiom footprint within the Lean/Mathlib trust base, no sorry. They ASSERT that the locked-proven baseline is EXACTLY the eight {F1,F4,F7,F11,F12,F18,F19,F22}; they do NOT themselves re-prove those formulas (the formula proofs live in Lutar/Puriq/Formulas/ProvedFormulas.lean).", "locked_set": ["F1", "F4", "F7", "F11", "F12", "F18", "F19", "F22"], "theorem_u": "Theorem U stays REAL-conditional and EXCLUDED from this locked baseline (theoremU_excluded_from_locked); anchoring this milestone does not change Theorem U's status."}, "kernel_commit": "25e0b2af781f5fb10324945ea10c861bcc28cc83", "kernel_commit_short": "25e0b2af781f", "kind": "locked-baseline-anchor", "milestone_kind": "locked-baseline", "milestone_status": "REAL-invariant", "milestone_title": "Locked-proven baseline (Doctrine v11) \u2014 kernel meta-invariants", "numbers": {"axioms_unique": 22, "declarations": 1323, "sorries_noncomment": 254}, "organ": "lutar-lean", "prev_hash": "08744b67b647039f87abbf0b29587638ae777308ca7fc2434ed3ae4033687b50", "receipt_id": "dcdad01763241e4d7af6b45e59949e6596c12ccf43ed6b784471c1f05b4715c0", "schema": "szl.khipu.receipt/v1", "signing": {"format": "sigstore-keyless-bundle", "bytes": 19036, "b64_head": "eyJtZWRpYVR5cGUiOiJhcHBsaWNhdGlvbi92bmQuZGV2\u2026"}, "source_run": {"conclusion": "success", "id": "27319352318", "url": "https://github.com/szl-holdings/lutar-lean/actions/runs/27319352318", "workflow": "Lake build (gate + numbers)"}, "subject": {"name": "locked_baseline_snapshot.json", "sha256": "19ea5946195f7437cfb881eb5489898d0d45f5f074dfa210c22eb6c8bbfc3bc9", "snapshot": {"branch": "main", "built_at_utc": "2026-06-11T02:18:27Z", "honesty": {"conjecture_1": "OPEN: unconditional Lambda uniqueness is Conjecture 1 and is machine-checked FALSE as stated; conjecture1_still_open re-asserts it stays open.", "doctrine": "v11", "locked_baseline": "REAL-invariant: kernel-verified meta-theorems in Lutar/Uniqueness/AxiomCheck.lean (locked_count_eight, theoremU_excluded_from_locked, theoremU_axiom_sets_kernel_only, conjecture1_still_open) \u2014 each proven by `decide`, axiom footprint within the Lean/Mathlib trust base, no sorry. They ASSERT that the locked-proven baseline is EXACTLY the eight {F1,F4,F7,F11,F12,F18,F19,F22}; they do NOT themselves re-prove those formulas (the formula proofs live in Lutar/Puriq/Formulas/ProvedFormulas.lean).", "locked_set": ["F1", "F4", "F7", "F11", "F12", "F18", "F19", "F22"], "theorem_u": "Theorem U stays REAL-conditional and EXCLUDED from this locked baseline (theoremU_excluded_from_locked); anchoring this milestone does not change Theorem U's status."}, "kernel_commit": "25e0b2af781f5fb10324945ea10c861bcc28cc83", "kernel_commit_short": "25e0b2af781f", "kind": "locked-baseline", "lean_numbers": {"lean_numbers_sha256": "38f9a69cb289110e44ffa9bc4a8575d811220c4654a7985b85694d6f1bb3f7f9", "numbers": {"axiom_names": ["A6'_block_consistent", "KS_theorem_1_1", "MomentSubGaussian", "audit_reidemeister_invariance", "canonicalReceipt", "chromotopology_code_bijection", "compression_collision_resistant", "domain_separation", "gleason_length_mod_8", "klDivergence_nonneg", "lambda_schur_concave_n_axis", "lambda_stationary_unique", "leaf_collision_resistant", "liu_hui_pi_converges", "node_collision_resistant", "pinsker", "r1_invariance", "r2_invariance", "setAlpha_cauchy", "setDelta_stage2", "sha256", "sha256_collision_resistant"], "axioms_raw": 23, "axioms_unique": 22, "declarations": 1323, "sorries_baseline": 251, "sorries_noncomment": 254, "sorries_putnam": 56, "sorries_raw": 307}, "reference_vectors_sha256": "857967629daf5e5c45a167306ea0e0091569a29766b01ac91bef15a539b816dc", "replay_hash": "1f0c9d9938b96b3d56fe01e37b955e1b91ff1aec0610fe30c30e515cc8ab469c", "schema": "szl.lean_numbers/v1"}, "milestone": {"decl_source_sha256": {"Lutar/Uniqueness/AxiomCheck.lean": "5e7998d33a1928c12f2e07595ec929544ac04e37f17ad7693ab2838136ab540f", "Lutar/Uniqueness/Identifiability.lean": "fa340e6a999eac7ea1cd035d90647548baaa290b7376d7fcbdcbd165e475dedf", "Lutar/Uniqueness/LambdaEquiv.lean": "03f63e36f3a9b19e8e9d4f48313a450bae7c85fcb53049d52e0f6d4adf4b1c23", "Lutar/Uniqueness/TheoremU.lean": "c958520ba31d6fc1f48a9b49871d67812f178e168b31bf2be9e3d5fb2061386c"}, "full_axiom_footprint": {"Lutar.Uniqueness.AxiomCheck.conjecture1_still_open": [], "Lutar.Uniqueness.AxiomCheck.locked_count_eight": [], "Lutar.Uniqueness.AxiomCheck.theoremU_axiom_sets_kernel_only": [], "Lutar.Uniqueness.AxiomCheck.theoremU_excluded_from_locked": [], "Lutar.Uniqueness.CorollaryU1_LambdaUnique_Separable": ["Classical.choice", "Quot.sound", "propext"], "Lutar.Uniqueness.CorollaryU2_LambdaUnique_Factors": ["Classical.choice", "Quot.sound", "propext"], "Lutar.Uniqueness.TheoremU_LambdaUnique": ["Classical.choice", "Quot.sound", "propext"], "Lutar.Uniqueness.TheoremU_LambdaUnique_eq": ["Classical.choice", "Quot.sound", "propext"], "Lutar.Uniqueness.identifiability_forces_lambda": ["Classical.choice", "Quot.sound", "propext"], "Lutar.Uniqueness.lambda_equiv_to_eq_of_anchored": ["Classical.choice", "Quot.sound", "propext"]}, "headline_axiom_footprint": {"conjecture1_still_open": [], "locked_count_eight": [], "theoremU_axiom_sets_kernel_only": [], "theoremU_excluded_from_locked": []}, "headline_decls": ["conjecture1_still_open", "locked_count_eight", "theoremU_axiom_sets_kernel_only", "theoremU_excluded_from_locked"], "id": "locked-baseline", "kernel_only": true, "kernel_trust_base": ["Classical.choice", "Quot.sound", "funext", "propext"], "module": "Lutar.Uniqueness.AxiomCheck", "status": "REAL-invariant", "title": "Locked-proven baseline (Doctrine v11) \u2014 kernel meta-invariants"}, "repo": "szl-holdings/lutar-lean", "schema": "szl.proof.snapshot/v1"}}, "timestamp": "2026-06-11T02:20:21Z"}], "amaru": [{"receipt_id": "4c9c3f2b8d6452d9bc0e9a9144fc9e1743b3ca76544a988d4d9e4b39df87ba73", "timestamp": "2026-06-02T02:13:07.827680+00:00", "organ": "amaru", "kind": "tick", "index": 0, "lambda": 0.9, "lambda_pass": true, "predicted_hash": "", "actual_hash": "4c9c3f2b8d6452d9bc0e9a9144fc9e1743b3ca76544a988d4d9e4b39df87ba73", "delta": 0.0, "lutar_anchor": "c7c0ba17", "doctrine": "v11", "decl": 749, "axioms": 14, "sorries": 163, "neuro_citations": "[]", "dsse_payload_type": "application/vnd.szl.khipu+json", "dsse_pae_sha256": "6a8ba013ddcd1938e0fc2174ef79287ca49266277b0195595f324dacb9eb02c9", "dsse_sig": "MEQCIBIZjd6T0E4Bhl0OGkhcMZmAuqmnN0ZxmWrL+7U/h31JAiAmF2U1DBEQieaDrFkHcjBcOW91PY1glK0X+/2EKprpVQ==", "dsse_keyid": "szlholdings-cosign", "dsse_signed": true, "verify_key_url": "https://github.com/szl-holdings/.github/blob/main/cosign.pub"}, {"receipt_id": "bc4d6a1629c01584eb6789d19a432fbc9448ce92ada8d47e14552fe94dee9fa1", "timestamp": "2026-06-02T02:13:08.490579+00:00", "organ": "amaru", "kind": "tick", "index": 1, "lambda": 0.9, "lambda_pass": true, "predicted_hash": "4c9c3f2b8d6452d9bc0e9a9144fc9e1743b3ca76544a988d4d9e4b39df87ba73", "actual_hash": "bc4d6a1629c01584eb6789d19a432fbc9448ce92ada8d47e14552fe94dee9fa1", "delta": 0.0, "lutar_anchor": "c7c0ba17", "doctrine": "v11", "decl": 749, "axioms": 14, "sorries": 163, "neuro_citations": "[]", "dsse_payload_type": "application/vnd.szl.khipu+json", "dsse_pae_sha256": "3cb923bc57002b34cd52124601bfbeeff68c6232e598dd06eccb4ff2847f1371", "dsse_sig": "MEUCIQDBB4xUJMFm4YKcZ0mcz6n3q6XomOKEepJWmaplX9Xo0gIgUIg3Xm316oVN05pvIoNxhJBDyL6Vhp1xfEq9nx9V5Wg=", "dsse_keyid": "szlholdings-cosign", "dsse_signed": true, "verify_key_url": "https://github.com/szl-holdings/.github/blob/main/cosign.pub"}, {"receipt_id": "2f872c5144585602dd1016ce732912134ad30423e442fda009cdc0d168c6732d", "timestamp": "2026-06-02T02:13:09.173270+00:00", "organ": "amaru", "kind": "tick", "index": 2, "lambda": 0.9, "lambda_pass": true, "predicted_hash": "bc4d6a1629c01584eb6789d19a432fbc9448ce92ada8d47e14552fe94dee9fa1", "actual_hash": "2f872c5144585602dd1016ce732912134ad30423e442fda009cdc0d168c6732d", "delta": 0.0, "lutar_anchor": "c7c0ba17", "doctrine": "v11", "decl": 749, "axioms": 14, "sorries": 163, "neuro_citations": "[]", "dsse_payload_type": "application/vnd.szl.khipu+json", "dsse_pae_sha256": "f72e37f1ea8d785d862ec7469d3908fc7b455360964d6cdea61e430d89b3e66d", "dsse_sig": "MEYCIQDvfS5l1nyk5zHz9wsNwe/wj6ZPNAMbbJ4KzMG2ZXEQkwIhAJ4mkTOAnOdNWFb2SuweFbQnjP0QPORGAA/IU8sHB+X5", "dsse_keyid": "szlholdings-cosign", "dsse_signed": true, "verify_key_url": "https://github.com/szl-holdings/.github/blob/main/cosign.pub"}]}; | |
| function renderLedger() { | |
| const btn = el('ledger-load'); | |
| btn.disabled = true; | |
| setStatus('ledger-status', 'Checking hash-chain linkage in-browser …', true); | |
| const lut = LEDGER_SNAPSHOT.lutar_lean || []; | |
| const ama = LEDGER_SNAPSHOT.amaru || []; | |
| const hfBase = 'https://huggingface.co/datasets/SZLHOLDINGS/szl-lake/blob/main/khipu/'; | |
| let links = 0, broken = 0; | |
| const rows = lut.map((r, i) => { | |
| const prev = r.prev_hash; | |
| const ok = (i === 0) ? (prev === null || prev === '' || prev === undefined) | |
| : (prev === lut[i-1].receipt_id); | |
| if (ok) links++; else broken++; | |
| return { r, i, prev, ok }; | |
| }); | |
| const intact = broken === 0; | |
| let chainHTML = '<div class="verdict-banner ' + (intact ? 'verdict-ok' : 'verdict-fail') + '">' | |
| + (intact ? '✓ CHAIN INTACT' : '✗ CHAIN BROKEN') + ' — ' + links + '/' + lut.length | |
| + ' hash-links verified in your browser <span class="chip chip-dim">organ: lutar-lean</span></div>' | |
| + '<div style="font-size:12px;color:var(--text-dim);margin-bottom:8px">Each receipt\'s <code>prev_hash</code> ' | |
| + 'is compared to the previous receipt\'s <code>receipt_id</code>. This proves append-only ordering. ' | |
| + 'Content-hash and signature verification run offline via szl-receipt.</div>'; | |
| rows.forEach(({ r, i, prev, ok }) => { | |
| chainHTML += '<div class="hash-row"><span class="hash-label">#' + escHTML(String(r.chain_index)) + ' ' | |
| + escHTML(r.kind || '') + '</span><span class="hash-val">id ' + escHTML(String(r.receipt_id).substring(0,16)) | |
| + '…</span><span class="hash-val ' + (ok ? 'hash-match' : 'hash-mismatch') + '">prev ' | |
| + escHTML(prev == null ? '(genesis)' : String(prev).substring(0,16) + '…') + '</span>' | |
| + '<span class="chip ' + (ok ? 'chip-ok' : 'chip-err') + '">' + (ok ? 'LINK OK' : 'BROKEN') + '</span></div>'; | |
| }); | |
| el('ledger-chain').innerHTML = chainHTML; | |
| let cardsHTML = '<div style="font-size:13px;font-weight:700;margin-bottom:14px;color:var(--text-dim);text-transform:uppercase;letter-spacing:.07em">Receipts (verbatim honesty labels)</div>'; | |
| lut.forEach(r => { | |
| const h = r.honesty || {}; | |
| let honestyHTML = ''; | |
| Object.keys(h).forEach(k => { | |
| const v = h[k]; | |
| if (typeof v === 'string') { | |
| honestyHTML += '<div style="margin:4px 0"><span class="chip chip-warn">' + escHTML(k) + '</span> ' | |
| + '<span style="font-size:12px;color:var(--text-dim)">' + escHTML(v) + '</span></div>'; | |
| } | |
| }); | |
| const sg = r.signing || {}; | |
| cardsHTML += '<div class="formula-card"><div class="formula-card-head">' | |
| + '<span class="formula-id">lutar-lean</span><span class="formula-name">' + escHTML(r.kind || 'receipt') + '</span>' | |
| + '<span class="chip chip-dim">schema ' + escHTML(r.schema || '') + '</span></div>' | |
| + '<div class="hash-row"><span class="hash-label">receipt_id</span><span class="hash-val">' | |
| + escHTML(String(r.receipt_id).substring(0,40)) + '…</span></div>' | |
| + (r.numbers ? '<div style="font-size:12px;color:var(--text-dim);margin:6px 0">declarations ' | |
| + escHTML(String(r.numbers.declarations)) + ' · axioms ' + escHTML(String(r.numbers.axioms_unique)) | |
| + ' · sorries ' + escHTML(String(r.numbers.sorries_noncomment)) + ' · kernel ' | |
| + escHTML(String(r.kernel_commit_short || '')) + '</div>' : '') | |
| + '<div style="margin:8px 0">' + honestyHTML + '</div>' | |
| + '<div style="font-size:12px;color:var(--text-mute)">signing: ' + escHTML(sg.format || '—') | |
| + (sg.bytes ? ' (' + escHTML(String(sg.bytes)) + ' bytes)' : '') + '</div>' | |
| + '<div style="margin-top:8px;font-size:12px"><a href="' + hfBase + 'lutar_lean_receipts.ndjson" target="_blank" rel="noopener">Canonical rows on Hugging Face ↗</a>' | |
| + ' · <a href="https://pypi.org/project/szl-receipt/" target="_blank" rel="noopener">Verify offline (szl-receipt)</a></div></div>'; | |
| }); | |
| ama.forEach(r => { | |
| cardsHTML += '<div class="formula-card"><div class="formula-card-head">' | |
| + '<span class="formula-id">amaru</span><span class="formula-name">' + escHTML(r.kind || 'tick') + '</span>' | |
| + '<span class="chip ' + (r.lambda_pass ? 'chip-ok' : 'chip-err') + '">Λ ' + escHTML(String(r.lambda)) + ' ' | |
| + (r.lambda_pass ? 'PASS' : 'FAIL') + '</span><span class="conj">Conjecture 1 — advisory</span></div>' | |
| + '<div class="hash-row"><span class="hash-label">receipt_id</span><span class="hash-val">' | |
| + escHTML(String(r.receipt_id).substring(0,40)) + '…</span></div>' | |
| + '<div style="font-size:12px;color:var(--text-dim);margin:6px 0">doctrine ' + escHTML(String(r.doctrine)) | |
| + ' · decl ' + escHTML(String(r.decl)) + ' · axioms ' + escHTML(String(r.axioms)) + ' · sorries ' | |
| + escHTML(String(r.sorries)) + ' · anchor ' + escHTML(String(r.lutar_anchor || '')) + '</div>' | |
| + '<div style="font-size:12px;color:var(--text-mute)">DSSE ' + (r.dsse_signed ? 'signed ✓' : 'unsigned') | |
| + ' · keyid ' + escHTML(String(r.dsse_keyid || '—')) + '</div>' | |
| + '<div style="margin-top:8px;font-size:12px"><a href="' + hfBase + 'amaru_receipts.ndjson" target="_blank" rel="noopener">Canonical rows on Hugging Face ↗</a>' | |
| + ' · <a href="' + escHTML(String(r.verify_key_url || '#')) + '" target="_blank" rel="noopener">Public key ↗</a></div></div>'; | |
| }); | |
| el('ledger-cards').innerHTML = cardsHTML; | |
| show('ledger-panel'); | |
| setStatus('ledger-status', 'Chain: ' + (intact ? 'INTACT' : 'BROKEN') + ' (' + links + '/' + lut.length | |
| + ' links) · ' + (lut.length + ama.length) + ' real receipts shown · signatures verify offline against Hugging Face.'); | |
| btn.disabled = false; | |
| } | |
| </script> | |
| </body> | |
| </html> | |