:root {
  --bg: #fdfcf9;
  --panel: #ffffff;
  --ink: #1a1a1a;
  --ink-soft: #555;
  --ink-faint: #888;
  --rule: #e7e5e0;
  --accent: #0d4a7a;
  --accent-soft: #e8f1f7;
  --ok: #16a34a;
  --ok-soft: #ecfdf5;
  --warn: #b45309;
  --warn-soft: #fef6e7;
  --bad: #b91c1c;
  --bad-soft: #fef2f2;
  --code-bg: #f6f4ee;
  --sans:  system-ui, -apple-system, "Segoe UI", Roboto, Helvetica, Arial, sans-serif;
  --serif: ui-serif, Georgia, "Times New Roman", Times, serif;
  --mono:  ui-monospace, "SF Mono", Menlo, Monaco, Consolas, monospace;
}
* { box-sizing: border-box; }
html { scroll-behavior: smooth; }
body {
  margin: 0;
  font-family: var(--sans);
  background: var(--bg);
  color: var(--ink);
  line-height: 1.55;
  -webkit-font-smoothing: antialiased;
}
h1, h2, h3 {
  font-family: var(--serif);
  font-weight: 500;
  letter-spacing: -0.005em;
}
code, pre, .mono {
  font-family: var(--mono);
}
a { color: var(--accent); text-decoration: none; }
a:hover { text-decoration: underline; }

.wrap { max-width: 1080px; margin: 0 auto; padding: 0 24px; }

/* ----- top nav ----- */
nav.top {
  position: sticky; top: 0; z-index: 10;
  background: rgba(253,252,249,0.92);
  backdrop-filter: blur(6px);
  border-bottom: 1px solid var(--rule);
}
nav.top .wrap {
  display: flex; align-items: center; justify-content: space-between;
  height: 52px;
}
nav.top .brand { font-weight: 600; letter-spacing: -0.01em; }
nav.top .brand a { color: inherit; }
nav.top .brand a:hover { color: var(--accent); text-decoration: none; }
nav.top .links { display: flex; gap: 18px; font-size: 14px; }
nav.top .links a { color: var(--ink-soft); }
nav.top .links a:hover { color: var(--accent); text-decoration: none; }
nav.top .links a.current { color: var(--accent); font-weight: 500; }

/* ----- hero ----- */
header.hero { padding: 72px 0 40px; }
header.hero h1 {
  font-size: 38px; line-height: 1.15; letter-spacing: -0.02em;
  margin: 0 0 16px;
  max-width: 820px;
}
header.hero .lede {
  font-size: 18px; color: var(--ink-soft); max-width: 720px;
  margin: 0 0 28px;
}
header.hero .stats {
  display: flex; flex-wrap: wrap; gap: 28px 40px;
  border-top: 1px solid var(--rule);
  border-bottom: 1px solid var(--rule);
  padding: 18px 0;
}
header.hero .stat .num {
  font-size: 24px; font-weight: 600; letter-spacing: -0.01em;
}
header.hero .stat .lbl {
  font-size: 12px; color: var(--ink-faint);
  text-transform: uppercase; letter-spacing: 0.06em;
}

section { padding: 56px 0; border-top: 1px solid var(--rule); }
section h2 {
  font-size: 26px; margin: 0 0 8px; letter-spacing: -0.015em;
}
section .section-lede {
  color: var(--ink-soft); margin: 0 0 28px; max-width: 760px;
}
section h3 {
  font-size: 17px; margin: 24px 0 8px;
}

/* ----- invariant layer cards ----- */
.layers { display: grid; grid-template-columns: 1fr; gap: 12px; }
.layer {
  display: grid;
  grid-template-columns: 48px 1fr;
  gap: 16px;
  padding: 18px 20px;
  background: var(--panel);
  border: 1px solid var(--rule);
  border-radius: 10px;
}
.layer .idx {
  width: 36px; height: 36px;
  border-radius: 50%;
  background: var(--accent-soft);
  color: var(--accent);
  display: flex; align-items: center; justify-content: center;
  font-weight: 600;
}
.layer h3 { margin: 0 0 4px; font-size: 16px; }
.layer .tag {
  display: inline-block; font-size: 11px;
  color: var(--ink-faint);
  border: 1px solid var(--rule);
  padding: 2px 8px; border-radius: 999px;
  margin-left: 8px; vertical-align: middle;
}
.layer p { margin: 4px 0 0; color: var(--ink-soft); font-size: 15px; }
.layer p.fragility {
  margin-top: 8px; font-size: 13px; color: var(--ink-faint);
}

/* ----- matrix ----- */
.matrix-wrap { overflow-x: auto; margin-top: 8px; }
table.matrix {
  border-collapse: collapse; min-width: 100%;
  font-size: 13px;
}
table.matrix th, table.matrix td {
  padding: 10px 12px;
  border-bottom: 1px solid var(--rule);
  text-align: center;
  white-space: nowrap;
}
table.matrix th.row-h, table.matrix td.row-h {
  text-align: left; font-weight: 500;
}
table.matrix thead th {
  font-weight: 600;
  color: var(--ink-soft);
  border-bottom: 1px solid var(--ink);
}
table.matrix tr.env td.row-h { color: var(--ink-faint); font-style: italic; }
.pill {
  display: inline-flex; align-items: center; justify-content: center;
  min-width: 22px; height: 22px;
  border-radius: 6px;
  font-size: 12px; font-weight: 600;
}
.pill.ok    { background: var(--ok-soft);   color: var(--ok); }
.pill.cond  { background: var(--warn-soft); color: var(--warn); }
.pill.bad   { background: var(--bad-soft);  color: var(--bad); }
.legend { display: flex; gap: 16px; flex-wrap: wrap; margin-top: 16px; font-size: 13px; color: var(--ink-soft); }
.legend .item { display: inline-flex; gap: 8px; align-items: center; }

/* ----- preservation conditions ----- */
.conditions {
  display: grid;
  grid-template-columns: 1fr;
  gap: 14px;
}
.cond-card {
  background: var(--panel);
  border: 1px solid var(--rule);
  border-radius: 10px;
  padding: 20px 24px;
}
.cond-card h3 {
  margin: 0 0 8px;
  font-size: 17px;
}
.cond-card ul {
  margin: 8px 0 0;
  padding-left: 20px;
  color: var(--ink);
  font-size: 14.5px;
  line-height: 1.7;
}
.cond-card ul li { margin: 4px 0; }
.cond-card ul li .mono,
.cond-card ul li code {
  font-size: 13px;
}
.cond-card .note {
  margin-top: 16px;
  font-size: 13px;
  color: var(--ink-faint);
  border-top: 1px dashed var(--rule);
  padding-top: 12px;
  line-height: 1.6;
}

/* ----- scope diagram ----- */
.scope-single {
  display: flex;
  justify-content: center;
  margin-top: 8px;
}
.scope-card {
  background: var(--panel);
  border: 1px solid var(--rule);
  border-radius: 10px;
  padding: 24px 28px;
  max-width: 560px;
  width: 100%;
}
.scope-card svg { width: 100%; height: auto; display: block; }

/* ----- architecture / lifecycle diagram ----- */
.arch-wrap { background: var(--panel); border: 1px solid var(--rule); border-radius: 10px; padding: 24px; }
.arch-wrap svg { width: 100%; height: auto; display: block; }
.diagram-note {
  margin: 18px 4px 0;
  font-size: 13px;
  color: var(--ink-soft);
  line-height: 1.5;
  border-top: 1px dashed var(--rule);
  padding-top: 14px;
}
.diagram-note code {
  font-size: 12.5px;
  background: var(--code-bg);
  padding: 1px 5px;
  border-radius: 3px;
}

/* ----- theorem cards ----- */
.thms { display: grid; grid-template-columns: 1fr; gap: 14px; }
.thm {
  background: var(--panel);
  border: 1px solid var(--rule);
  border-radius: 10px;
  padding: 20px 22px;
}
.thm h3 { margin: 0 0 4px; font-size: 17px; }
.thm .nm { color: var(--ink-faint); font-size: 13px; }
.thm p.plain { margin: 8px 0 14px; color: var(--ink); font-size: 15px; }
.thm ul.plain-list {
  margin: 6px 0 14px;
  padding-left: 22px;
  color: var(--ink);
  font-size: 15px;
  line-height: 1.6;
}
.thm ul.plain-list li { margin: 6px 0; }
.thm details {
  border-top: 1px dashed var(--rule);
  padding-top: 12px;
  margin-top: 12px;
}
.thm details summary {
  cursor: pointer; font-size: 13px; color: var(--accent);
  list-style: none;
  user-select: none;
}
.thm details summary::-webkit-details-marker { display: none; }
.thm details summary::before { content: "▸ "; }
.thm details[open] summary::before { content: "▾ "; }
.thm details summary:hover { text-decoration: underline; }
.thm pre {
  margin: 12px 0 0;
  padding: 14px 16px;
  background: var(--code-bg);
  border-radius: 6px;
  font-size: 13px;
  overflow-x: auto;
  line-height: 1.5;
}
.thm .footer {
  margin-top: 14px;
  font-size: 13px;
  display: flex; gap: 14px; flex-wrap: wrap;
  color: var(--ink-faint);
}
.thm .footer a { font-size: 13px; }

/* tiny syntax tint */
.kw   { color: #7a3e9d; }
.name { color: #0d4a7a; }
.ty   { color: #2563eb; }
.com  { color: #7a7066; font-style: italic; }
.lit  { color: #b45309; }

/* ----- two-column comparison (also used by Certora page) ----- */
.compare-grid {
  display: grid;
  grid-template-columns: 1fr 1fr;
  gap: 14px;
}
.compare-grid .card {
  background: var(--panel);
  border: 1px solid var(--rule);
  border-radius: 10px;
  padding: 20px 22px;
}
.compare-grid h3 { margin-top: 0; }
.compare-grid p { color: var(--ink-soft); font-size: 14.5px; margin: 8px 0; }
.compare-grid ul { margin: 8px 0 0; padding-left: 18px; color: var(--ink-soft); font-size: 14px; }
.compare-grid ul li { margin: 4px 0; }
.compare-grid .cond {
  font-family: var(--mono);
  font-size: 12.5px;
  color: #555;
  background: var(--code-bg);
  padding: 6px 10px;
  border-radius: 5px;
  margin-top: 10px;
  display: inline-block;
}

/* legacy alias */
.certora-grid { display: grid; grid-template-columns: 1fr 1fr; gap: 14px; }
.certora-grid .card { background: var(--panel); border: 1px solid var(--rule); border-radius: 10px; padding: 18px 20px; }
.certora-grid h3 { margin-top: 0; }
.certora-grid ul { margin: 8px 0 0; padding-left: 18px; color: var(--ink-soft); font-size: 14px; }
.certora-grid ul li { margin: 4px 0; }

/* ----- bridge chain (used in safety page) ----- */
.bridge-wrap {
  background: var(--panel);
  border: 1px solid var(--rule);
  border-radius: 10px;
  padding: 24px 28px;
}
.bridge-wrap svg { width: 100%; height: auto; display: block; }

/* ----- explore (spoke pages) ----- */
.explore {
  display: grid;
  grid-template-columns: repeat(auto-fit, minmax(220px, 1fr));
  gap: 14px;
}
.explore a.tile {
  display: block;
  background: var(--panel);
  border: 1px solid var(--rule);
  border-radius: 10px;
  padding: 18px 20px;
  color: var(--ink);
  transition: border-color 120ms ease, transform 120ms ease;
}
.explore a.tile:hover {
  border-color: var(--accent);
  text-decoration: none;
  transform: translateY(-1px);
}
.explore .tile h3 { margin: 0 0 4px; font-size: 15px; color: var(--accent); }
.explore .tile p { margin: 0; font-size: 13px; color: var(--ink-soft); }
.explore .tile.disabled {
  opacity: 0.55; pointer-events: none;
  border-style: dashed;
}
.explore .tile.disabled .h3 { color: var(--ink-faint); }

footer.site {
  border-top: 1px solid var(--rule);
  padding: 40px 0 60px;
  font-size: 13px; color: var(--ink-faint);
}
footer.site .wrap { display: flex; justify-content: space-between; flex-wrap: wrap; gap: 12px; }

/* responsive */
@media (max-width: 720px) {
  header.hero h1 { font-size: 30px; }
  .compare-grid { grid-template-columns: 1fr; }
  .certora-grid { grid-template-columns: 1fr; }
  nav.top .links { display: none; }
}