:root {
  --bg: #f7f6f3;
  --bg-panel: #ffffff;
  --bg-inset: #f1efe9;
  --border: #ddd8cd;
  --text: #23201b;
  --text-dim: #6b665c;
  --accent: #b23a2f;
  --accent-ink: #ffffff;
  --accent-dim: #f2d9d3;
  --ok: #1e7a3f;
  --ok-bg: #e5f4e9;
  --ok-border: #b7ddc3;
  --bad: #b23a2f;
  --bad-bg: #fbe9e6;
  --bad-border: #edc0b8;
  --warn: #9a6b12;
  --warn-bg: #fbf1de;
  --warn-border: #eed9ae;
  --skip-bg: #ececec;
  --skip-border: #d7d7d7;
  --skip-text: #6b665c;
  --focus: #3b6fb2;
  --mono: "SFMono-Regular", Consolas, "Liberation Mono", Menlo, monospace;
  --sans: -apple-system, BlinkMacSystemFont, "Segoe UI", Helvetica, Arial, sans-serif;
  --radius: 10px;
}

@media (prefers-color-scheme: dark) {
  :root:not([data-theme="light"]) {
    --bg: #171512;
    --bg-panel: #221f1b;
    --bg-inset: #1b1916;
    --border: #3a352c;
    --text: #ece7de;
    --text-dim: #a89f8f;
    --accent: #e2695b;
    --accent-ink: #1a0e0c;
    --accent-dim: #3a2320;
    --ok: #6fcf8f;
    --ok-bg: #16281c;
    --ok-border: #2c4a35;
    --bad: #e2695b;
    --bad-bg: #2e1c19;
    --bad-border: #55322c;
    --warn: #e0b45a;
    --warn-bg: #2f2717;
    --warn-border: #55452a;
    --skip-bg: #2a2723;
    --skip-border: #423d34;
    --skip-text: #a89f8f;
    --focus: #7aa7e0;
  }
}
:root[data-theme="dark"] {
  --bg: #171512;
  --bg-panel: #221f1b;
  --bg-inset: #1b1916;
  --border: #3a352c;
  --text: #ece7de;
  --text-dim: #a89f8f;
  --accent: #e2695b;
  --accent-ink: #1a0e0c;
  --accent-dim: #3a2320;
  --ok: #6fcf8f;
  --ok-bg: #16281c;
  --ok-border: #2c4a35;
  --bad: #e2695b;
  --bad-bg: #2e1c19;
  --bad-border: #55322c;
  --warn: #e0b45a;
  --warn-bg: #2f2717;
  --warn-border: #55452a;
  --skip-bg: #2a2723;
  --skip-border: #423d34;
  --skip-text: #a89f8f;
  --focus: #7aa7e0;
}

* { box-sizing: border-box; }
/* keep the `hidden` attribute authoritative even over flex/grid display rules */
[hidden] { display: none !important; }

body {
  background: var(--bg);
  color: var(--text);
  font-family: var(--sans);
  line-height: 1.45;
  padding-inline: 20px;
  padding-block: 20px 48px;
}

.wrap { max-width: 1180px; margin: 0 auto; }

a { color: var(--accent); }

/* ---------- header ---------- */
header.top {
  display: flex;
  align-items: center;
  justify-content: space-between;
  gap: 16px;
  flex-wrap: wrap;
  margin-bottom: 18px;
}
.brand { display: flex; align-items: baseline; gap: 10px; flex-wrap: wrap; }
.brand h1 { font-size: 1.5rem; margin: 0; letter-spacing: -0.01em; }
.brand .tag { color: var(--text-dim); font-size: 0.92rem; }

.backend-status {
  display: inline-flex;
  align-items: center;
  gap: 8px;
  font-size: 0.85rem;
  border: 1px solid var(--border);
  background: var(--bg-panel);
  padding: 6px 12px;
  border-radius: 999px;
  white-space: nowrap;
}
.dot { width: 9px; height: 9px; border-radius: 50%; background: var(--skip-text); flex: none; }
.backend-status[data-state="loading"] .dot { background: var(--warn); animation: pulse 1.2s infinite ease-in-out; }
.backend-status[data-state="ready"] .dot { background: var(--ok); }
.backend-status[data-state="unavailable"] .dot { background: var(--bad); }
@keyframes pulse { 0%,100% { opacity: 1; } 50% { opacity: 0.35; } }

/* ---------- layout ---------- */
main { display: flex; flex-direction: column; gap: 18px; }

.editors {
  display: grid;
  grid-template-columns: 1fr 1fr;
  gap: 16px;
}
@media (max-width: 760px) {
  .editors { grid-template-columns: 1fr; }
}

.panel {
  background: var(--bg-panel);
  border: 1px solid var(--border);
  border-radius: var(--radius);
  overflow: hidden;
}

.editor-panel h2 {
  font-size: 0.95rem;
  margin: 0;
  padding: 10px 14px;
  border-bottom: 1px solid var(--border);
  background: var(--bg-inset);
  display: flex;
  align-items: center;
  justify-content: space-between;
}
.editor-panel h2 .fname { font-family: var(--mono); font-weight: 400; color: var(--text-dim); font-size: 0.8rem; }

.code-editor {
  display: flex;
  height: 320px;
  overflow: auto;
  background: var(--bg-panel);
}
.code-editor .gutter {
  flex: none;
  padding: 10px 10px 10px 14px;
  text-align: right;
  color: var(--text-dim);
  font-family: var(--mono);
  font-size: 0.85rem;
  line-height: 1.5;
  user-select: none;
  border-right: 1px solid var(--border);
  background: var(--bg-inset);
  white-space: pre;
}
.code-editor textarea {
  flex: 1;
  border: 0;
  resize: none;
  padding: 10px 14px;
  font-family: var(--mono);
  font-size: 0.85rem;
  line-height: 1.5;
  color: var(--text);
  background: transparent;
  outline: none;
  white-space: pre;
  overflow: auto;
  tab-size: 2;
}
.code-editor textarea:focus-visible { outline: 2px solid var(--focus); outline-offset: -2px; }

/* ---------- config form (inside Advanced options) ---------- */
.config-grid {
  display: grid;
  grid-template-columns: repeat(auto-fit, minmax(220px, 1fr));
  gap: 12px 16px;
}
.field { display: flex; flex-direction: column; gap: 4px; }
.field label { font-size: 0.82rem; font-weight: 600; color: var(--text-dim); }
.field .hint { font-size: 0.76rem; color: var(--text-dim); font-weight: 400; }
.field input[type="text"], .field input[type="number"] {
  border: 1px solid var(--border);
  border-radius: 6px;
  padding: 7px 9px;
  background: var(--bg-panel);
  color: var(--text);
  font: inherit;
  font-family: var(--mono);
  font-size: 0.85rem;
}
.field input:focus-visible { outline: 2px solid var(--focus); outline-offset: 1px; }

.toggle-row {
  display: flex;
  flex-wrap: wrap;
  gap: 10px 20px;
  margin-top: 14px;
  padding-top: 12px;
  border-top: 1px solid var(--border);
}
.toggle {
  display: flex;
  align-items: center;
  gap: 7px;
  font-size: 0.85rem;
}
.toggle input[disabled] + span { color: var(--text-dim); }
.toggle .hint { display: block; font-size: 0.74rem; color: var(--text-dim); }

/* ---------- advanced options (collapsed by default) ---------- */
details.advanced {
  background: var(--bg-panel);
  border: 1px solid var(--border);
  border-radius: var(--radius);
  overflow: hidden;
}
details.advanced > summary {
  cursor: pointer;
  font-size: 0.85rem;
  color: var(--text-dim);
  font-weight: 600;
  padding: 11px 16px;
  list-style: none;
  user-select: none;
}
details.advanced > summary::-webkit-details-marker { display: none; }
details.advanced > summary::before {
  content: "▸";
  display: inline-block;
  margin-right: 8px;
  transition: transform 0.15s ease;
}
details.advanced[open] > summary {
  border-bottom: 1px solid var(--border);
  background: var(--bg-inset);
}
details.advanced[open] > summary::before { transform: rotate(90deg); }
details.advanced summary:focus-visible { outline: 2px solid var(--focus); outline-offset: -2px; }
.advanced-inner { padding: 14px 16px 16px; }

.run-row {
  display: flex;
  align-items: center;
  gap: 12px;
  flex-wrap: wrap;
}
button.run {
  background: var(--accent);
  color: var(--accent-ink);
  border: 0;
  border-radius: 8px;
  padding: 10px 22px;
  font-size: 0.95rem;
  font-weight: 600;
  cursor: pointer;
}
button.run:hover:not(:disabled) { filter: brightness(1.08); }
button.run:disabled { opacity: 0.55; cursor: not-allowed; }
button.secondary {
  background: var(--bg-inset);
  color: var(--text);
  border: 1px solid var(--border);
  border-radius: 8px;
  padding: 9px 16px;
  font-size: 0.88rem;
  cursor: pointer;
}
button.secondary:hover { border-color: var(--accent); }

.spinner {
  width: 16px; height: 16px;
  border-radius: 50%;
  border: 2px solid var(--border);
  border-top-color: var(--accent);
  animation: spin 0.8s linear infinite;
  flex: none;
}
@keyframes spin { to { transform: rotate(360deg); } }
.run-note { font-size: 0.82rem; color: var(--text-dim); }
/* library download / check progress (shown while a check runs) */
.progress { flex: 1 1 260px; min-width: 200px; display: flex; flex-direction: column; gap: 4px; }
.progress-track { height: 6px; border-radius: 3px; background: var(--border); overflow: hidden; }
.progress-fill { height: 100%; width: 0; background: var(--accent); transition: width 0.15s linear; }
.progress-fill.indeterminate { width: 30%; animation: slide 1.2s infinite ease-in-out; }
@keyframes slide { 0% { margin-left: 0; } 50% { margin-left: 70%; } 100% { margin-left: 0; } }
.progress-text { font-size: 0.78rem; color: var(--text-dim); }

/* ---------- backend-unavailable banner ---------- */
.notice {
  border-radius: var(--radius);
  border: 1px solid var(--warn-border);
  background: var(--warn-bg);
  color: var(--text);
  padding: 14px 16px;
  display: flex;
  align-items: center;
  gap: 14px;
  flex-wrap: wrap;
}
.notice strong { color: var(--warn); }
.notice .notice-body { display: flex; flex-direction: column; gap: 3px; min-width: 220px; flex: 1; }
.notice .notice-fix { font-size: 0.82rem; color: var(--text-dim); }
.notice .notice-fix code { background: var(--bg-inset); padding: 1px 5px; border-radius: 4px; font-family: var(--mono); }
.notice .actions { display: flex; gap: 8px; flex-wrap: wrap; margin-left: auto; }

/* ---------- engine-honesty note (dismissible) ---------- */
.libs {
  display: flex; flex-wrap: wrap; align-items: baseline; gap: 6px 10px;
  font-size: 0.84rem; color: var(--text-dim);
}
.libs-label { color: var(--text); font-weight: 600; }
.libs-chips { display: inline-flex; flex-wrap: wrap; gap: 6px; }
.lib-chip {
  border: 1px solid var(--border); background: var(--bg-inset); color: var(--text);
  border-radius: 999px; padding: 2px 10px; font-size: 0.8rem; cursor: pointer; font-family: inherit;
}
.lib-chip:hover { border-color: var(--accent); }
.lib-chip small { color: var(--text-dim); margin-left: 4px; }
.libs-hint { flex-basis: 100%; font-size: 0.78rem; }

/* ---------- verdict panel ---------- */
.verdict-panel { padding: 0; }
.verdict-empty {
  padding: 28px 16px;
  text-align: center;
  color: var(--text-dim);
  font-size: 0.9rem;
}

.banner {
  padding: 16px 18px;
  display: flex;
  align-items: center;
  gap: 12px;
  flex-wrap: wrap;
  border-bottom: 1px solid var(--border);
}
.banner .icon { font-size: 1.3rem; line-height: 1; }
.banner .title { font-size: 1.15rem; font-weight: 700; }
.banner .sub { color: var(--text-dim); font-size: 0.85rem; }
.banner[data-kind="ok"] { background: var(--ok-bg); }
.banner[data-kind="ok"] .title { color: var(--ok); }
.banner[data-kind="rejected"] { background: var(--bad-bg); }
.banner[data-kind="rejected"] .title { color: var(--bad); }
.banner[data-kind="infra"] { background: var(--warn-bg); }
.banner[data-kind="infra"] .title { color: var(--warn); }
.banner .meta { margin-left: auto; display: flex; gap: 14px; font-size: 0.78rem; color: var(--text-dim); flex-wrap: wrap; }

.detail-box {
  margin: 0 18px 16px;
  padding: 10px 12px;
  background: var(--bg-inset);
  border: 1px solid var(--border);
  border-radius: 8px;
  font-family: var(--mono);
  font-size: 0.82rem;
  white-space: pre-wrap;
  word-break: break-word;
}

.section { padding: 0 18px 18px; }
.section h3 {
  font-size: 0.85rem;
  text-transform: uppercase;
  letter-spacing: 0.04em;
  color: var(--text-dim);
  margin: 0 0 10px;
}

.targets { display: flex; flex-direction: column; gap: 8px; }
.target-card {
  border: 1px solid var(--border);
  border-radius: 8px;
  padding: 10px 12px;
  background: var(--bg-inset);
}
.target-card .row1 { display: flex; align-items: center; gap: 10px; flex-wrap: wrap; }
.target-card .tname { font-family: var(--mono); font-weight: 600; }
.status-chip {
  font-size: 0.72rem;
  font-weight: 700;
  text-transform: uppercase;
  letter-spacing: 0.03em;
  border-radius: 999px;
  padding: 2px 10px;
  border: 1px solid transparent;
}
.status-chip[data-status="proved"] { background: var(--ok-bg); color: var(--ok); border-color: var(--ok-border); }
.status-chip[data-status="not_proved"], .status-chip[data-status="mismatch"], .status-chip[data-status="missing"] {
  background: var(--bad-bg); color: var(--bad); border-color: var(--bad-border);
}
.status-chip[data-status="unchecked"] { background: var(--skip-bg); color: var(--skip-text); border-color: var(--skip-border); }

.axiom-list { display: flex; flex-wrap: wrap; gap: 6px; margin-top: 8px; }
.axiom-pill {
  font-family: var(--mono);
  font-size: 0.74rem;
  background: var(--bg-panel);
  border: 1px solid var(--border);
  border-radius: 6px;
  padding: 2px 7px;
}
.target-card .tdetail {
  margin-top: 8px;
  font-family: var(--mono);
  font-size: 0.78rem;
  color: var(--text-dim);
  white-space: pre-wrap;
}
.no-axioms { color: var(--text-dim); font-size: 0.78rem; margin-top: 6px; }

.checks { display: flex; flex-wrap: wrap; gap: 8px; }
.check-chip {
  display: inline-flex;
  align-items: center;
  gap: 6px;
  border-radius: 999px;
  padding: 4px 12px;
  font-size: 0.8rem;
  border: 1px solid var(--border);
  background: var(--bg-inset);
  cursor: default;
}
.check-chip .mark { font-weight: 700; }
.check-chip[data-status="ok"] { background: var(--ok-bg); border-color: var(--ok-border); color: var(--ok); }
.check-chip[data-status="skipped"] { background: var(--skip-bg); border-color: var(--skip-border); color: var(--skip-text); }
.check-chip[data-status="fail"] { background: var(--bad-bg); border-color: var(--bad-border); color: var(--bad); }
.check-chip[data-status="fail"] { cursor: help; }

.timing-table { border-collapse: collapse; width: 100%; font-size: 0.82rem; }
.timing-table td { padding: 3px 8px 3px 0; }
.timing-table td.tval { text-align: right; font-family: var(--mono); color: var(--text-dim); }
.timing-table tr.total td { border-top: 1px solid var(--border); font-weight: 600; padding-top: 6px; }

.footer-note {
  margin-top: 22px;
  color: var(--text-dim);
  font-size: 0.8rem;
  border-top: 1px solid var(--border);
  padding-top: 14px;
}
.footer-note code { background: var(--bg-inset); padding: 1px 5px; border-radius: 4px; font-family: var(--mono); }

.sr-only {
  position: absolute; width: 1px; height: 1px; padding: 0; margin: -1px;
  overflow: hidden; clip: rect(0,0,0,0); white-space: nowrap; border: 0;
}

@media (max-width: 480px) {
  .brand h1 { font-size: 1.25rem; }
  .code-editor { height: 260px; }
}