:root {
  --bg: #f4f7f6;
  --paper: #f8f4ec;
  --surface: #ffffff;
  --surface-muted: #edf3f2;
  --surface-hover: #f8fbfa;
  --surface-dark: #132f36;
  --surface-dark-2: #10282e;

  --text: #172126;
  --text-muted: #607078;
  --text-faint: #809097;

  --primary: #174b57;
  --primary-hover: #216371;
  --primary-soft: #e6eff0;

  --accent: #d76642;
  --accent-hover: #bd5334;
  --accent-soft: #f9ece7;

  --success: #28734b;
  --success-soft: #e8f3ec;
  --danger: #ad422c;
  --danger-soft: #f8ebe7;
  --caution: #a76924;
  --warning: #8a4fbf;
  --warning-soft: #f4edfa;

  --border: #d4dfe1;
  --border-strong: #a9bec2;
  --editor-border: #29474e;
  --editor-text: #f7faf9;

  /* One measure for every block of running prose. */
  --prose: 1120px;

  --radius-sm: 8px;
  --radius: 12px;
  --radius-lg: 18px;

  --shadow: 0 1px 2px rgb(20 47 54 / 0.05), 0 8px 24px rgb(20 47 54 / 0.06);

  --shadow-hover: 0 2px 4px rgb(20 47 54 / 0.06), 0 14px 34px rgb(20 47 54 / 0.1);

  --mono: "SFMono-Regular", Consolas, "Liberation Mono", monospace;

  /* Syntax colours for code on a light surface. A dark block redefines the set
     below, so one span class serves both and no snippet carries its own hues. */
  --tok-keyword: #a8452a;
  --tok-builtin: #8a5a12;
  --tok-number: #6b3fa0;
  --tok-operator: #1d6b63;
  --tok-comment: #5f6e74;
  --tok-name: #17323a;
  --tok-ctor: #1f5f8b;
  --global-link: #7a3fa8;
  --tok-punct: #59696f;
}

.mock-editor,
.thm-program,
.loop-code,
.cm-editor {
  --tok-keyword: #f08a65;
  --tok-builtin: #f0c674;
  --tok-number: #c4a7e7;
  --tok-operator: #8bd5ca;
  --tok-comment: #718b91;
  --tok-name: #f7faf9;
  --tok-ctor: #8fc4e8;
  --global-link: #c9a2e8;
  --tok-punct: #a7bbc0;
}

.tok-keyword {
  color: var(--tok-keyword);
  font-weight: 650;
}

.tok-builtin {
  color: var(--tok-builtin);
  font-weight: 600;
}

.tok-number {
  color: var(--tok-number);
}

.tok-operator {
  color: var(--tok-operator);
}

.tok-comment {
  color: var(--tok-comment);
  font-style: italic;
}

.tok-constructor {
  color: var(--tok-ctor);
  font-weight: 600;
}

.tok-function {
  color: var(--tok-ctor);
}

.tok-variableName {
  color: var(--tok-name);
}

.tok-punctuation {
  color: var(--tok-punct);
}

/* A token span carries colour and nothing else. Several snippets draw their
   lines as spans and style them as full-width rows; without this, the spans
   the highlighter nests inside a line would each become a row of their own. */
[data-lang] [class^="tok-"] {
  display: inline;
  min-width: 0;
  padding: 0;
  margin: 0;
  border: 0;
  background: none;
}

* {
  box-sizing: border-box;
}

[hidden] {
  display: none !important;
}

html {
  scroll-behavior: smooth;
}

body {
  margin: 0;
  color: var(--text);
  background: var(--bg);
  font-family: Inter, ui-sans-serif, -apple-system, BlinkMacSystemFont, "Segoe UI", sans-serif;
  line-height: 1.65;
  -webkit-font-smoothing: antialiased;
}

img {
  max-width: 100%;
}

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

button,
select,
input {
  font: inherit;
}

code,
pre {
  font-family: var(--mono);
}

code {
  overflow-wrap: anywhere;
}

/*
 * Code inside prose, wherever it appears: captions, cards, list items, hover notes.
 * Code blocks and controls that embed code set their own look.
 */
:where(p, li, dd, dt, td, th, figcaption, h3, h4, em, strong, span, a, label, button, summary)
  > code {
  padding: 0.1em 0.38em;
  color: #1d5563;
  background: #e8f0f1;
  border: 1px solid #d3e1e3;
  border-radius: 5px;
  font-size: 0.88em;
  overflow-wrap: anywhere;
}

.page-shell {
  width: min(1600px, calc(100% - 48px));
  margin: 0 auto;
}

.visually-hidden {
  position: absolute;
  width: 1px;
  height: 1px;
  overflow: hidden;
  clip-path: inset(50%);
  white-space: nowrap;
}

/* -------------------------------------------------------------------------- */
/* Site navigation                                                            */
/* -------------------------------------------------------------------------- */

.site-nav {
  position: sticky;
  top: 0;
  z-index: 40;
  background: rgb(248 244 236 / 0.86);
  border-bottom: 1px solid rgb(23 75 87 / 0.08);
  backdrop-filter: saturate(1.4) blur(10px);
}

.site-nav-inner {
  display: flex;
  flex-wrap: wrap;
  align-items: center;
  justify-content: space-between;
  gap: 6px 24px;
  min-height: 60px;
}

.site-brand {
  display: inline-flex;
  align-items: center;
  gap: 10px;
  color: var(--primary);
  font-family: "Iowan Old Style", "Palatino Linotype", Georgia, serif;
  font-size: 1.35rem;
  font-weight: 700;
  letter-spacing: -0.01em;
  text-decoration: none;
}

.site-brand img {
  border-radius: 7px;
}

.site-links {
  display: flex;
  flex-wrap: wrap;
  align-items: center;
  gap: 2px 22px;
  margin: 0;
  padding: 0;
  list-style: none;
}

.site-links a {
  position: relative;
  display: inline-flex;
  align-items: center;
  gap: 7px;
  padding: 6px 0;
  color: var(--text-muted);
  font-size: 0.92rem;
  font-weight: 600;
  text-decoration: none;
  transition: color 150ms ease;
}

.site-links a:hover {
  color: var(--primary);
}

/* The current page is marked by a short accent rule under its name, not a filled pill. */
.site-links a[aria-current="page"] {
  color: var(--primary);
}

.site-links a[aria-current="page"]::after {
  content: "";
  position: absolute;
  right: 0;
  bottom: -2px;
  left: 0;
  height: 2px;
  background: var(--accent);
  border-radius: 2px;
}

.site-links a.nav-cta {
  padding: 6px 14px;
  color: #ffffff;
  background: var(--primary);
  border-radius: var(--radius-sm);
}

.site-links a.nav-cta:hover {
  background: var(--primary-hover);
}

.site-links a.nav-cta[aria-current="page"] {
  background: var(--accent-hover);
}

.site-links a.nav-cta[aria-current="page"]::after {
  display: none;
}

.site-links a.nav-icon {
  font-size: 1.15rem;
}

.site-actions {
  display: flex;
  align-items: center;
  gap: 22px;
}

.playground-title {
  margin-top: 10px;
  margin-bottom: 0;
  font-size: clamp(2.2rem, 4.5vw, 3.2rem);
}

/* -------------------------------------------------------------------------- */
/* Hero                                                                       */
/* -------------------------------------------------------------------------- */

.hero {
  overflow: hidden;
  background: var(--paper);
  border-bottom: 1px solid var(--border);
}

.hero-banner {
  display: block;
  width: 100%;
  height: clamp(180px, 25vw, 320px);
  object-fit: cover;
  object-position: center;
  border-bottom: 1px solid rgb(23 75 87 / 0.12);
}

.hero-content {
  padding-top: 50px;
  padding-bottom: 56px;
}

.eyebrow {
  margin: 0;
  color: var(--accent);
  font-family: var(--mono);
  font-size: 0.74rem;
  font-weight: 700;
  letter-spacing: 0.15em;
  line-height: 1.4;
  text-transform: uppercase;
}

.hero-eyebrow {
  color: var(--text-muted);
}

h1,
h2,
h3 {
  margin-top: 0;
  color: var(--primary);
  font-family: "Iowan Old Style", "Palatino Linotype", Georgia, serif;
  font-weight: 650;
  line-height: 1.1;
  letter-spacing: -0.028em;
}

/* Balanced headings never strand one word on the last line; prose avoids orphans too. */
h1,
h2,
h3,
h4 {
  text-wrap: balance;
}

p,
li,
dd,
figcaption {
  text-wrap: pretty;
}

h1 {
  margin-bottom: 20px;
  font-size: clamp(3rem, 7vw, 5rem);
}

h2 {
  margin-bottom: 0;
  font-size: clamp(2rem, 4vw, 2.75rem);
}

h3 {
  font-size: 1.25rem;
}

.hero-lead {
  max-width: var(--prose);
  margin: 0;
  color: var(--text-muted);
  font-size: clamp(1.08rem, 2vw, 1.22rem);
  line-height: 1.75;
}

.actions {
  display: flex;
  flex-wrap: wrap;
  gap: 10px;
  margin-top: 30px;
}

.actions a {
  display: inline-flex;
  align-items: center;
  gap: 8px;
  min-height: 42px;
  padding: 9px 14px;
  color: var(--primary);
  background: rgb(255 255 255 / 0.74);
  border: 1px solid var(--border);
  border-radius: var(--radius-sm);
  font-size: 0.9rem;
  font-weight: 700;
  text-decoration: none;
  transition:
    transform 150ms ease,
    border-color 150ms ease,
    background 150ms ease,
    box-shadow 150ms ease;
}

.actions a:hover {
  transform: translateY(-1px);
  background: var(--surface);
  border-color: var(--border-strong);
  box-shadow: 0 6px 18px rgb(20 47 54 / 0.06);
}

.actions a.primary {
  color: #ffffff;
  background: var(--primary);
  border-color: var(--primary);
}

.actions a.primary:hover {
  background: var(--primary-hover);
  border-color: var(--primary-hover);
}

.actions a.pipeline {
  color: var(--accent-hover);
  background: var(--accent-soft);
  border-color: rgb(215 102 66 / 0.3);
}

.actions a.pipeline:hover {
  border-color: var(--accent);
}

/* -------------------------------------------------------------------------- */
/* Sections                                                                   */
/* -------------------------------------------------------------------------- */

main {
  padding-bottom: 80px;
}

.section {
  padding: 74px 0;
  border-bottom: 1px solid var(--border);
}

.section:last-child {
  border-bottom: 0;
}

.section-heading {
  max-width: var(--prose);
}

.section-heading h2 {
  margin-top: 10px;
}

.section-intro,
.body-copy {
  max-width: var(--prose);
  margin: 18px 0 0;
  color: var(--text-muted);
}

.body-copy {
  margin-top: 30px;
}

.muted {
  color: var(--text-muted);
}

/* -------------------------------------------------------------------------- */
/* Analyzer                                                                   */
/* -------------------------------------------------------------------------- */

.analyzer-section {
  padding-top: 64px;
}

.analyzer {
  display: grid;
  grid-template-columns: minmax(0, 1fr);
  gap: 16px;
  margin-top: 30px;
  padding: 26px;
  background: var(--surface);
  border: 1px solid var(--border);
  border-radius: var(--radius-lg);
  box-shadow: var(--shadow);
}

.editor-shell {
  overflow: hidden;
  background: var(--surface-dark);
  border: 1px solid var(--editor-border);
  border-radius: 10px;
}

.editor-toolbar {
  display: flex;
  align-items: center;
  justify-content: space-between;
  gap: 12px;
  min-height: 38px;
  padding: 0 14px;
  color: #8fa6ab;
  background: var(--surface-dark-2);
  border-bottom: 1px solid var(--editor-border);
  font-size: 0.75rem;
}

.editor-file {
  color: #c2d1d4;
  font-family: var(--mono);
}

.code-editor {
  overflow: hidden;
  background: var(--surface-dark);
}

.code-editor .cm-editor {
  color: var(--editor-text);
  background: var(--surface-dark);
  font: 0.9rem / 1.6 var(--mono);
}

.code-editor .cm-editor.cm-focused {
  outline: 2px solid rgb(72 151 169 / 0.48);
  outline-offset: -2px;
}

.code-editor .cm-scroller {
  overflow: auto;
  font-family: inherit;
}

/* The editor fits its program: a short example gets a short editor, a long one grows up to the cap and scrolls. */
#program-editor .cm-editor,
#program-editor .cm-scroller {
  min-height: 240px;
}

/*
 * Until CodeMirror loads, an editor's mount is empty: skeleton lines hold its place
 * so the page does not jump, and CodeMirror's own DOM replaces them.
 */
#program-editor:empty {
  min-height: 240px;
}

.code-editor:empty {
  --skeleton: rgb(255 255 255 / 0.09);
  position: relative;
}

.code-editor:empty::before {
  content: "";
  position: absolute;
  inset: 18px 24px;
  background-image:
    linear-gradient(var(--skeleton), var(--skeleton)),
    linear-gradient(var(--skeleton), var(--skeleton)),
    linear-gradient(var(--skeleton), var(--skeleton)),
    linear-gradient(var(--skeleton), var(--skeleton)),
    linear-gradient(var(--skeleton), var(--skeleton)),
    linear-gradient(var(--skeleton), var(--skeleton)),
    linear-gradient(var(--skeleton), var(--skeleton)),
    linear-gradient(var(--skeleton), var(--skeleton));
  background-repeat: no-repeat;
  background-size:
    34% 10px,
    58% 10px,
    46% 10px,
    22% 10px,
    64% 10px,
    40% 10px,
    52% 10px,
    18% 10px;
  background-position:
    0 0,
    24px 24px,
    24px 48px,
    48px 72px,
    24px 96px,
    24px 120px,
    0 144px,
    0 168px;
  border-radius: 4px;
  animation: skeleton-pulse 1.4s ease-in-out infinite;
}

@keyframes skeleton-pulse {
  50% {
    opacity: 0.45;
  }
}

#program-editor .cm-scroller {
  max-height: max(560px, 78vh);
}

.code-editor .cm-content {
  padding: 16px 0;
  caret-color: #ffffff;
}

.code-editor .cm-line {
  padding: 0 16px;
}

.code-editor .cm-gutters {
  color: #647f86;
  background: var(--surface-dark-2);
  border-right: 1px solid var(--editor-border);
}

.code-editor .cm-gutterElement {
  padding: 0 10px 0 8px;
}

.code-editor .cm-activeLine {
  background: rgb(255 255 255 / 0.035);
}

.code-editor .cm-activeLineGutter {
  color: #c2d1d4;
  background: rgb(255 255 255 / 0.04);
}

.code-editor .cm-selectionBackground,
.code-editor .cm-content ::selection {
  background: rgb(94 164 178 / 0.32) !important;
}

.code-editor .cm-cursor {
  border-left-color: #ffffff;
}

.code-editor .cm-matchingBracket {
  color: inherit;
  background: rgb(139 213 202 / 0.18);
  outline: 1px solid rgb(139 213 202 / 0.35);
}

.code-editor .cm-panels {
  color: var(--text);
  background: var(--surface);
}

.code-editor .cm-searchMatch {
  background: rgb(240 198 116 / 0.25);
}

.code-editor .cm-searchMatch.cm-searchMatch-selected {
  background: rgb(240 198 116 / 0.45);
}

/* A 3px inset bar rather than a border, so annotated lines keep their indentation. */
.code-editor .cm-verdict-line {
  box-shadow: inset 3px 0 0 var(--verdict-color);
  background: var(--verdict-tint);
}

.code-editor .cm-verdict-proved {
  --verdict-color: #6fcf97;
  --verdict-tint: rgb(111 207 151 / 0.1);
}

.code-editor .cm-verdict-unknown {
  --verdict-color: #f0c674;
  --verdict-tint: rgb(240 198 116 / 0.1);
}

/* Violet, apart from unknown's amber and error's red: a warning is neither. */
.code-editor .cm-verdict-warning {
  --verdict-color: #d7a0ff;
  --verdict-tint: rgb(215 160 255 / 0.1);
}

.code-editor .cm-verdict-refuted,
.code-editor .cm-verdict-error {
  --verdict-color: #ff8a73;
  --verdict-tint: rgb(255 138 115 / 0.13);
}

.code-editor .cm-verdict-dead {
  --verdict-color: #7c9096;
  --verdict-tint: rgb(124 144 150 / 0.08);
}

/* An error in the source: the line is tinted strongly and the offending column underlined. */
.code-editor .cm-verdict-line.cm-verdict-error {
  --verdict-tint: rgb(255 138 115 / 0.2);
}

.code-editor .cm-verdict-error .cm-verdict-badge {
  color: #1c1c1c;
  background: #ff8a73;
}

.code-editor .cm-error-token {
  text-decoration: underline wavy #ff8a73;
  text-decoration-thickness: 2px;
  text-underline-offset: 4px;
  background: rgb(255 138 115 / 0.25);
  border-radius: 2px;
}

.code-editor .cm-verdict-badge {
  margin-left: 1.5em;
  padding: 0 0.5em;
  border-radius: 4px;
  color: var(--verdict-color);
  background: rgb(0 0 0 / 0.22);
  font-size: 0.78em;
  font-weight: 600;
  white-space: pre;
  cursor: help;
}

/* Dim the code, not the badge: a line's opacity would fade its DEAD label too. */
.code-editor .cm-dead-line > :not(.cm-verdict-badge) {
  opacity: 0.42;
}

.code-editor .cm-value-hint {
  margin-left: 1.4em;
  color: #8fb3ba;
  font-size: 0.78em;
  font-style: italic;
  white-space: pre;
}

.code-editor .cm-value-hint.merge {
  color: #6f878d;
}

.code-editor .cm-statement-selected {
  background: rgb(94 164 178 / 0.2);
  border-radius: 2px;
}

.code-editor .cm-statement-hovered {
  background: rgb(240 198 116 / 0.18);
  outline: 1px solid rgb(240 198 116 / 0.6);
  border-radius: 2px;
}

.code-editor .cm-tooltip.cm-tooltip-hover {
  color: var(--editor-text);
  background: var(--surface-dark-2);
  border: 1px solid var(--editor-border);
  border-radius: var(--radius-sm);
  box-shadow: var(--shadow-hover);
}

.cm-variable-tooltip {
  padding: 8px 10px;
  font: 0.76rem / 1.45 var(--mono);
}

.cm-variable-tooltip-head {
  display: flex;
  flex-wrap: wrap;
  align-items: baseline;
  gap: 4px 8px;
  margin-bottom: 4px;
}

.cm-variable-tooltip-tag {
  padding: 0 5px;
  color: #8bd5ca;
  border: 1px solid rgb(139 213 202 / 0.4);
  border-radius: 4px;
  font-size: 0.85em;
}

.cm-variable-tooltip-where {
  color: #8fa6ab;
  font-size: 0.9em;
}

.cm-variable-tooltip table {
  border-collapse: collapse;
}

.cm-variable-tooltip td {
  padding: 1px 10px 1px 0;
  white-space: nowrap;
  border: 0;
}

.cm-variable-tooltip td:nth-child(2) {
  color: #8fa6ab;
}

.cm-variable-tooltip-key {
  color: #8bd5ca;
  font-weight: 700;
}

.cm-variable-tooltip-value {
  color: #f0c674;
}

.cm-variable-tooltip-dead {
  color: #7c9096;
  font-style: italic;
}

.editor-toolbar-file {
  display: inline-flex;
  align-items: center;
  gap: 12px;
  min-width: 0;
}

.editor-examples {
  display: inline-flex;
  align-items: center;
  gap: 6px;
  padding: 3px 10px;
  color: #c2d1d4;
  background: rgb(255 255 255 / 0.06);
  border: 1px solid var(--editor-border);
  border-radius: 6px;
  font-size: 0.74rem;
  font-weight: 650;
  cursor: pointer;
}

.editor-examples:hover,
.editor-examples:focus-visible {
  color: #ffffff;
  border-color: #4b7d88;
}

.editor-toolbar-tools {
  display: flex;
  align-items: center;
  gap: 14px;
}

.editor-toggle {
  display: inline-flex;
  align-items: center;
  gap: 6px;
  cursor: pointer;
  user-select: none;
}

.editor-toggle input {
  margin: 0;
  accent-color: #8bd5ca;
}

/* Opened by a click on a graph node, it floats over the page until closed. */
.state-inspector {
  position: fixed;
  z-index: 40;
  right: 16px;
  bottom: 16px;
  width: min(560px, calc(100vw - 32px));
  max-height: min(70vh, 640px);
  overflow: auto;
  padding: 14px 16px;
  background: var(--surface-muted);
  border: 1px solid var(--border-strong);
  border-radius: var(--radius-sm);
  box-shadow: var(--shadow-hover);
}

.state-inspector-close {
  margin-left: auto;
  padding: 0 6px;
  color: var(--text-muted);
  background: none;
  border: 0;
  font-size: 1.3rem;
  line-height: 1;
  cursor: pointer;
}

.state-inspector-close:hover {
  color: var(--text);
}

/* The state run_voblint joins over every context, shown before each context's own. */
.inspector-joined {
  margin: 10px 0 0;
  padding: 8px 10px;
  background: var(--surface);
  border: 1px solid var(--border);
  border-radius: var(--radius-sm);
  font-family: var(--mono);
  font-size: 0.8rem;
  white-space: pre-wrap;
}

.inspector-joined-title {
  display: block;
  margin-bottom: 4px;
  color: var(--text-muted);
  font-family: inherit;
  font-size: 0.75rem;
}

.state-inspector-header {
  display: flex;
  flex-wrap: wrap;
  align-items: baseline;
  gap: 6px 14px;
}

.state-inspector-location {
  display: inline-flex;
  flex-wrap: wrap;
  align-items: baseline;
  gap: 4px 10px;
  min-width: 0;
  font-size: 0.8rem;
}

.state-inspector-location strong {
  font-family: var(--mono);
}

.state-inspector-location code {
  overflow-wrap: anywhere;
  color: var(--text-muted);
  font-family: var(--mono);
}

.state-inspector-body {
  display: grid;
  grid-template-columns: repeat(auto-fill, minmax(min(100%, 380px), 1fr));
  gap: 10px;
  margin-top: 10px;
}

.state-inspector-body:empty {
  display: none;
}

/* A panel's key, inline above what it explains: one wrapping strip of small items. */
.panel-legend {
  display: flex;
  flex-wrap: wrap;
  gap: 4px 18px;
  margin: 8px 0 12px;
  color: var(--text-muted);
  font-size: 0.74rem;
}

/* A key in groups: one row per kind of annotation, each wrapping on its own. */
.panel-legend.grouped {
  flex-direction: column;
  gap: 4px;
}

.legend-row {
  display: flex;
  flex-wrap: wrap;
  gap: 4px 18px;
}

.legend-row > span,
.panel-legend > span {
  display: inline-flex;
  align-items: center;
  gap: 6px;
}

/* The editor's badges and hints, redrawn for the light page: icon and label as in the editor. */
.lg-badge {
  padding: 1px 0.5em;
  border: 1px solid var(--border);
  border-radius: 4px;
  color: var(--verdict-color);
  background: var(--surface);
  font: 600 0.7rem var(--mono);
  white-space: pre;
}

.lg-badge.proved {
  --verdict-color: var(--success);
}

.lg-badge.unknown {
  --verdict-color: var(--caution);
}

.lg-badge.warning {
  --verdict-color: var(--warning);
}

.lg-badge.refuted {
  --verdict-color: var(--danger);
}

.lg-badge.dead {
  --verdict-color: var(--text-faint);
}

.lg-badge.error {
  --verdict-color: var(--danger);
}

.lg-badge.hint {
  color: var(--text-muted);
  font-style: italic;
  font-weight: 400;
}

.lg-badge.hint.merge {
  color: var(--text-faint);
}

.panel-legend .legend-defs {
  position: absolute;
}

.inspector-message,
.panel-lead {
  color: var(--text-muted);
  font-size: 0.8rem;
}

p.inspector-message {
  margin: 8px 0 0;
}

.inspector-context {
  min-width: 0;
  padding: 8px 10px 10px;
  background: var(--surface);
  border: 1px solid var(--border);
  border-radius: 6px;
}

.inspector-context.focused {
  border-color: var(--accent);
  box-shadow: 0 0 0 1px var(--accent);
}

.inspector-context-header {
  display: flex;
  align-items: center;
  justify-content: space-between;
  gap: 10px;
  width: 100%;
  min-width: 0;
  padding: 0;
  color: var(--text);
  background: none;
  border: 0;
  font: 600 0.78rem var(--mono);
  text-align: left;
  cursor: pointer;
}

.inspector-context-header {
  justify-content: flex-start;
}

.inspector-context-header:hover .inspector-context-label {
  text-decoration: underline;
}

.inspector-context-header .inspector-status {
  margin-left: auto;
}

/* A call string of any depth arrives as one unbreakable token. Left alone it
   runs past the card and takes the whole inspector off-screen with it, so it
   wraps inside the card and is capped at a few lines; the full key stays on the
   element's title. */
.inspector-context-key {
  flex: 0 1 auto;
  min-width: 0;
  max-height: 3.4em;
  padding: 0 6px;
  overflow: hidden;
  color: var(--surface);
  background: var(--primary);
  border-radius: 4px;
  font-size: 0.7rem;
  line-height: 1.6;
  overflow-wrap: anywhere;
}

.inspector-table th.global {
  color: var(--primary);
}

.inspector-table th.global::after {
  content: " global";
  color: var(--text-faint);
  font-size: 0.8em;
  font-weight: 400;
}

.inspector-status {
  padding: 1px 7px;
  border-radius: 999px;
  font-size: 0.66rem;
  letter-spacing: 0.06em;
  text-transform: uppercase;
  color: var(--text-muted);
  background: var(--surface-muted);
}

.inspector-status.proved {
  color: var(--success);
  background: var(--success-soft);
}

.inspector-status.refuted {
  color: var(--danger);
  background: var(--danger-soft);
}

.inspector-status.unknown {
  color: var(--caution);
  background: rgb(240 198 116 / 0.22);
}

.inspector-table {
  margin-top: 6px;
  overflow-x: auto;
}

.inspector-analysis {
  margin: 8px 0 2px;
  color: var(--text-muted);
  font-size: 0.72rem;
  font-weight: 750;
  letter-spacing: 0.02em;
}

.inspector-analysis:first-child {
  margin-top: 0;
}

.seed-lines code.seed-analysis {
  background: none;
  color: var(--text-muted);
  font-weight: 700;
}

.inspector-table table {
  width: 100%;
  border-collapse: collapse;
  font-family: var(--mono);
  font-size: 0.74rem;
}

.inspector-table th,
.inspector-table td {
  padding: 3px 8px;
  text-align: left;
  white-space: nowrap;
  border-bottom: 1px solid var(--border);
}

.inspector-table th {
  color: var(--text-muted);
  font-weight: 600;
}

.inspector-findings {
  margin: 6px 0 0;
  padding-left: 18px;
  color: var(--text-muted);
  font-size: 0.74rem;
}

.editor-note {
  margin: -6px 0 0;
  color: var(--text-muted);
  font-size: 0.82rem;
}

.editor-note a {
  font-weight: 600;
}

kbd {
  padding: 1px 5px;
  color: var(--text);
  background: var(--surface-muted);
  border: 1px solid var(--border);
  border-bottom-width: 2px;
  border-radius: 4px;
  font-family: var(--mono);
  font-size: 0.78em;
}

/* Editor two thirds, settings one third; the settings come first in source order so
   the narrow layout stacks them above the editor. */
.analyzer-workspace {
  display: grid;
  grid-template-areas: "editor controls";
  grid-template-columns: minmax(0, 2fr) minmax(0, 1fr);
  gap: 16px;
  align-items: start;
}

.editor-column {
  display: grid;
  grid-area: editor;
  gap: 16px;
  min-width: 0;
}

.analyzer-sidebar {
  display: grid;
  grid-area: controls;
  gap: 16px;
  min-width: 0;
}

.analyzer-controls {
  display: flex;
  flex-direction: column;
  gap: 12px;
  padding: 16px 18px;
  background: var(--surface-muted);
  border: 1px solid rgb(23 75 87 / 0.06);
  border-radius: 10px;
}

.control-group {
  display: grid;
  gap: 6px;
}

.control-group select {
  width: 100%;
}

.analysis-choices {
  grid-template-columns: repeat(auto-fit, minmax(7.5rem, 1fr));
  gap: 4px 12px;
  margin: 0;
  padding: 0;
  border: 0;
}

.analysis-choices legend {
  grid-column: 1 / -1;
  margin-bottom: 2px;
  padding: 0;
  color: var(--text-muted);
  font-size: 0.8rem;
  font-weight: 750;
  line-height: 1.2;
}

.analyzer-controls .analysis-choices label {
  display: inline-flex;
  align-items: center;
  gap: 6px;
  color: var(--text);
  font-weight: 500;
  cursor: pointer;
}

.analysis-choices input {
  margin: 0;
  accent-color: #8bd5ca;
}

.analyzer-controls label {
  color: var(--text-muted);
  font-size: 0.8rem;
  font-weight: 750;
  line-height: 1.2;
}

.analyzer-controls label code {
  padding: 0;
  background: none;
}

.analyzer-controls select,
.analyzer-controls input,
.analyzer-controls > button {
  min-height: 42px;
  padding: 8px 12px;
  border-radius: var(--radius-sm);
}

.analyzer-controls select,
.analyzer-controls input {
  color: var(--text);
  background: var(--surface);
  border: 1px solid var(--border);
}

.analyzer-controls select:focus,
.analyzer-controls input:focus {
  border-color: var(--primary);
  outline: 2px solid rgb(23 75 87 / 0.14);
  outline-offset: 1px;
}

.control-help {
  margin: 0;
  color: var(--text-muted);
  font-size: 0.78rem;
  line-height: 1.45;
}

.analyzer-controls > button {
  display: inline-flex;
  align-items: center;
  justify-content: center;
  gap: 8px;
  padding-inline: 18px;
  color: #ffffff;
  background: var(--primary);
  border: 1px solid var(--primary);
  font-weight: 750;
  cursor: pointer;
  transition:
    background 150ms ease,
    transform 100ms ease;
}

.analyzer-controls > button:hover:not(:disabled) {
  background: var(--primary-hover);
}

.analyzer-controls > button:active:not(:disabled) {
  transform: translateY(1px);
}

.analyzer-controls > button:disabled {
  opacity: 0.6;
  cursor: wait;
}

.run-feedback {
  display: flex;
  flex-wrap: wrap;
  align-items: center;
  gap: 6px 12px;
  min-width: 0;
}

.status {
  margin: 0;
  color: var(--text-muted);
  font-size: 0.78rem;
  line-height: 1.45;
}

.status.ok {
  color: var(--success);
}

.status.error {
  color: var(--danger);
}

.analysis-timing {
  display: inline-flex;
  align-items: center;
  gap: 6px;
  padding: 2px 9px;
  color: var(--primary);
  background: var(--surface);
  border: 1px solid var(--border);
  border-radius: 999px;
  font-size: 0.78rem;
  font-variant-numeric: tabular-nums;
}

/* A failed run, or a finished one with diagnostics, is announced below the settings. */
.analysis-problems {
  display: flex;
  align-items: flex-start;
  gap: 14px;
  padding: 14px 18px;
  color: var(--text);
  background: var(--danger-soft);
  border: 1px solid rgb(173 66 44 / 0.35);
  border-left: 5px solid var(--danger);
  border-radius: 10px;
  animation: problem-in 220ms ease;
}

.analysis-problems.warning {
  background: var(--warning-soft);
  border-color: rgb(138 79 191 / 0.35);
  border-left-color: var(--warning);
}

.analysis-problems > i {
  margin-top: 2px;
  color: var(--danger);
  font-size: 1.35rem;
}

.analysis-problems.warning > i {
  color: var(--warning);
}

@keyframes problem-in {
  from {
    opacity: 0;
    transform: translateY(-4px);
  }
}

.problem-body {
  display: grid;
  gap: 6px;
  min-width: 0;
}

.problem-title {
  margin: 0;
  color: var(--danger);
  font-size: 1.02rem;
  font-weight: 750;
}

.analysis-problems.warning .problem-title {
  color: var(--warning);
}

.problem-message {
  margin: 0;
  font-family: var(--mono);
  font-size: 0.88rem;
  overflow-wrap: anywhere;
}

.problem-note {
  margin: 0;
  color: var(--text-muted);
  font-size: 0.86rem;
}

.problem-excerpt {
  min-width: min(100%, 520px);
  margin: 2px 0;
  padding: 8px 12px;
  overflow-x: auto;
  color: var(--editor-text);
  background: var(--surface-dark);
  border-radius: 6px;
  font-size: 0.84rem;
  line-height: 1.5;
}

.problem-caret {
  color: #ff8a73;
  font-weight: 700;
}

.problem-jump {
  justify-self: start;
  padding: 3px 12px;
  color: var(--primary);
  background: var(--surface);
  border: 1px solid var(--border-strong);
  border-radius: 999px;
  font-size: 0.8rem;
  font-weight: 650;
  cursor: pointer;
}

.problem-jump:hover {
  border-color: var(--primary);
}

.problem-items {
  display: grid;
  gap: 6px;
  margin: 4px 0 0;
  padding: 0;
  list-style: none;
}

.problem-items li {
  display: flex;
  flex-wrap: wrap;
  align-items: center;
  gap: 6px 12px;
  padding-left: 12px;
  border-left: 3px solid var(--warning);
  font-size: 0.88rem;
}

.problem-items li.error {
  border-left-color: var(--danger);
}

#run-analysis.running #run-analysis-icon {
  animation: analyzer-spin 0.8s linear infinite;
}

@keyframes analyzer-spin {
  to {
    transform: rotate(360deg);
  }
}

/* -------------------------------------------------------------------------- */
/* Analysis graph                                                             */
/* -------------------------------------------------------------------------- */

.raw-result {
  min-width: 0;
  padding: 10px 14px;
  background: var(--surface-muted);
  border: 1px solid var(--border);
  border-radius: 10px;
}

/* The call takes a second row and wraps there, so it is never cut off. */
.raw-result summary {
  display: flex;
  flex-wrap: wrap;
  align-items: baseline;
  gap: 4px 12px;
  list-style: none;
  cursor: pointer;
}

.raw-result summary .eyebrow {
  flex: none;
}

.raw-result summary::-webkit-details-marker {
  display: none;
}

/* One line: a long answer outline is cut with an ellipsis; the panel holds the whole term. */
.raw-call {
  display: grid;
  grid-template-columns: max-content minmax(0, 1fr);
  gap: 2px 0.6em;
  order: 1;
  flex: 1 1 100%;
  min-width: 0;
  padding: 0;
  border: 0;
  color: var(--text-muted);
  background: none;
  font-size: 0.72rem;
  overflow-wrap: anywhere;
}

.raw-call-head {
  justify-self: end;
}

.raw-call-body {
  min-width: 0;
}

.raw-call-fn {
  color: var(--primary);
  font-weight: 700;
}

.raw-call-arg {
  color: var(--text);
}

.raw-call-program {
  color: var(--primary);
  font-style: italic;
}

.raw-call-arrow {
  color: var(--text-faint);
}

.raw-call-ctor {
  color: var(--accent-hover);
  font-weight: 700;
}

.raw-call-observed {
  color: var(--text-faint);
  font-style: italic;
}

.raw-call-fields {
  color: var(--text-muted);
}

/* Every collapsible panel says it can be opened, and closed again. */
.expand-hint {
  display: inline-flex;
  flex: none;
  align-items: center;
  gap: 6px;
  margin-left: auto;
  color: var(--text-muted);
  font-size: 0.76rem;
}

.expand-hint i {
  font-size: 0.7rem;
  transition: transform 150ms ease;
}

summary:hover .expand-hint {
  color: var(--primary);
}

details[open] > summary .expand-hint i {
  transform: rotate(180deg);
}

details:not([open]) > summary .expand-hint-open,
details[open] > summary .expand-hint-closed {
  display: none;
}

.raw-result-empty {
  margin: 12px 0 4px;
  color: var(--text-muted);
  font-size: 0.82rem;
}

.raw-result-note {
  margin: 10px 0 0;
  color: var(--text-muted);
  font-size: 0.82rem;
}

.raw-result-panes {
  display: grid;
  grid-template-columns: repeat(3, minmax(0, 1fr));
  gap: 14px;
  margin-top: 12px;
}

/* Too narrow for three panes of JSON and trace: the trace takes its own row. */
@media (max-width: 1280px) {
  .raw-result-panes {
    grid-template-columns: repeat(2, minmax(0, 1fr));
  }

  .raw-result-trace {
    grid-column: 1 / -1;
  }
}

.raw-result-pane {
  display: grid;
  grid-template-rows: auto 1fr;
  gap: 6px;
  min-width: 0;
}

.raw-result-pane-header {
  display: flex;
  flex-wrap: wrap;
  align-items: center;
  justify-content: space-between;
  gap: 10px;
}

.raw-result-stats {
  margin-right: auto;
  color: var(--text-faint);
  font: 0.72rem var(--mono);
}

.raw-result-tools {
  display: flex;
  gap: 10px;
}

.raw-result-tools button {
  padding: 0;
  color: var(--primary);
  background: none;
  border: 0;
  font: 600 0.74rem var(--mono);
  cursor: pointer;
}

.raw-result-tools button:hover:not(:disabled) {
  text-decoration: underline;
}

.raw-result-tools button:disabled {
  color: var(--text-faint);
  cursor: not-allowed;
}

.raw-result-pane-header h2 {
  margin: 0;
  color: var(--text-muted);
  font: 700 0.74rem var(--mono);
  letter-spacing: 0.12em;
  text-transform: uppercase;
}

.raw-result-body {
  height: min(640px, 70vh);
  border: 1px solid var(--editor-border);
  border-radius: 10px;
}

.raw-result-body .cm-editor {
  height: 100%;
  font-size: 0.78rem;
}

.inspector-seed {
  display: flex;
  flex-wrap: wrap;
  align-items: baseline;
  gap: 4px 8px;
  margin-top: 6px;
  font-size: 0.74rem;
}

.inspector-seed-label {
  padding: 0 6px;
  color: var(--primary);
  border: 1px solid var(--border-strong);
  border-radius: 4px;
  font: 600 0.68rem var(--mono);
  cursor: help;
}

.seed-lines {
  display: inline-flex;
  flex-wrap: wrap;
  gap: 4px;
  font-family: var(--mono);
}

.seed-lines code {
  padding: 0 5px;
  background: var(--surface-muted);
  border-radius: 4px;
}

/* Unreachable reads like the graph's dead nodes: grey, dashed, italic. */
.inspector-seed.dead .seed-lines,
.solver-global.dead .seed-lines {
  color: var(--text-faint);
  font-style: italic;
}

.solver-globals {
  min-width: 0;
  padding: 14px 16px;
  background: var(--surface-muted);
  border: 1px solid var(--border);
  border-radius: var(--radius-sm);
}

.solver-globals summary {
  display: flex;
  flex-wrap: wrap;
  align-items: baseline;
  gap: 4px 12px;
  cursor: pointer;
}

.solver-globals-count {
  color: var(--text-muted);
  font-size: 0.8rem;
}

.solver-globals-note {
  margin: 8px 0 0;
  color: var(--text-muted);
  font-size: 0.8rem;
}

.solver-globals-list {
  display: grid;
  gap: 6px;
  margin: 10px 0 0;
  padding: 0;
  list-style: none;
}

.solver-global {
  display: flex;
  flex-wrap: wrap;
  align-items: baseline;
  gap: 4px 10px;
  padding: 6px 10px;
  background: var(--surface);
  border: 1px solid var(--border);
  border-radius: 6px;
  font-size: 0.76rem;
}

.solver-global.dead {
  border-style: dashed;
}

.solver-global-key {
  padding: 0;
  color: var(--text);
  background: none;
  border: 0;
  font: 600 0.76rem var(--mono);
  text-align: left;
}

button.solver-global-key {
  color: var(--primary);
  cursor: pointer;
}

button.solver-global-key:hover {
  text-decoration: underline;
}

/* Scrolls inside the panel: a long trace must not stretch the page. */
.solver-trace-all {
  padding: 0;
  color: var(--primary);
  background: none;
  border: 0;
  font: inherit;
  font-weight: 600;
  cursor: pointer;
}

.solver-trace-all:hover {
  text-decoration: underline;
}

.solver-trace-tools {
  display: flex;
  flex-wrap: wrap;
  align-items: center;
  gap: 6px 18px;
  margin: 10px 0 0;
  font-size: 0.8rem;
}

.solver-trace-tools button:disabled {
  color: var(--text-muted);
  cursor: progress;
}

.solve-replay-body {
  margin-top: 12px;
}

.replay-player {
  display: flex;
  flex-wrap: wrap;
  align-items: center;
  gap: 6px 8px;
}

.replay-player button {
  min-width: 36px;
  height: 34px;
  padding: 0 10px;
  color: var(--primary);
  background: var(--surface);
  border: 1px solid var(--border);
  border-radius: var(--radius-sm);
  cursor: pointer;
}

.replay-player button:hover:not(:disabled) {
  background: var(--surface-hover);
  border-color: var(--border-strong);
}

.replay-player button:disabled {
  color: var(--text-faint);
  cursor: default;
}

.replay-player input[type="range"] {
  flex: 1 1 200px;
  min-width: 140px;
  accent-color: var(--primary);
}

.replay-speed {
  display: inline-flex;
  align-items: center;
  gap: 6px;
  color: var(--text-muted);
  font-size: 0.8rem;
}

/* A fixed width, so a growing step number never rewraps the player row. */
.replay-step {
  min-width: 26ch;
  color: var(--text-muted);
  font: 600 0.8rem var(--mono);
  font-variant-numeric: tabular-nums;
}

/* The swatches repeat the node styles replay.js gives Cytoscape. */
.replay-swatch {
  display: inline-block;
  width: 18px;
  height: 12px;
  border: 1px solid var(--border-strong);
  border-radius: 3px;
  background: var(--surface);
}

.replay-swatch.r-unseen {
  background: var(--surface-muted);
  border: 1px dashed var(--text-faint);
}

.replay-swatch.r-solving {
  background: var(--accent-soft);
  border: 2px solid var(--accent);
}

.replay-swatch.r-current {
  background: var(--accent-soft);
  border: 4px solid var(--accent);
}

.replay-swatch.r-stable {
  background: var(--primary-soft);
  border: 2px solid var(--primary);
}

.replay-swatch.r-destabilized {
  border: 2px dotted var(--border-strong);
}

.replay-swatch.r-wpoint {
  border: 4px double var(--border-strong);
}

.replay-swatch.r-seed {
  width: 14px;
  height: 14px;
  background: var(--warning);
  border: 2px solid var(--warning);
  border-radius: 50%;
}

/* A diamond, as the replay draws a flow-insensitive global's unknown. */
.replay-swatch.r-global {
  width: 11px;
  height: 11px;
  margin-inline: 2px;
  background: var(--global-link);
  border: 2px solid var(--global-link);
  transform: rotate(45deg);
}

.replay-swatch.r-infl {
  height: 0;
  border: 0;
  border-top: 2px dotted var(--text-faint);
  border-radius: 0;
}

.replay-swatch.r-edge {
  height: 0;
  border: 0;
  border-top: 4px solid var(--accent);
  border-radius: 0;
}

/* The graph and the trace beside it share the row's height. */
.replay-layout {
  display: grid;
  grid-template-columns: minmax(0, 3fr) minmax(0, 2fr);
  height: clamp(380px, 64vh, 760px);
  gap: 12px;
}

.replay-layout > .replay-graph,
.replay-layout > .replay-trace-view {
  height: 100%;
  min-height: 0;
}

@media (max-width: 960px) {
  .replay-below {
    grid-template-columns: minmax(0, 1fr);
  }

  .replay-layout {
    grid-template-columns: minmax(0, 1fr);
    grid-template-rows: clamp(380px, 64vh, 760px) 360px;
    height: auto;
  }
}

/*
 * Under the graph and the trace: one card per view. Every view that changes from
 * step to step has a fixed height and scrolls, so stepping never moves the player,
 * the graph or the trace.
 */
.replay-below {
  display: grid;
  grid-template-columns: repeat(3, minmax(0, 1fr));
  gap: 14px 20px;
  margin-top: 14px;
}

.replay-card {
  display: flex;
  flex-direction: column;
  min-width: 0;
  gap: 6px;
}

.replay-card[hidden] {
  display: none;
}

.replay-card h3 {
  margin: 0;
}

.replay-scroll {
  height: 17em;
  overflow: auto;
  overscroll-behavior: contain;
}

.replay-stack.replay-scroll {
  height: 14.6em;
  margin: 0;
  padding-left: 2.6em;
}

.replay-global.is-active {
  border-color: var(--accent);
  box-shadow: inset 3px 0 0 var(--accent);
}

/* ------------------------------------------------------------- trace view */

/*
 * A trace view is a .code-editor too: gutters, line padding and font follow the
 * dark editors beside it, and only the trace's own colors are set here.
 */
.trace-view {
  border: 1px solid var(--editor-border);
  border-radius: 10px;
}

.trace-view .cm-editor {
  height: 100%;
  font: 0.78rem / 1.6 var(--mono);
}

.trace-view .tr-current {
  background: rgb(215 102 66 / 0.18);
  box-shadow: inset 3px 0 0 var(--accent);
}

/* A call opens a banner; the trace itself is unchanged. */
.trace-view .tr-banner {
  margin: 6px 0 2px;
  padding: 1px 8px;
  color: #8fc4e8;
  background: rgb(143 196 232 / 0.1);
  border-left: 3px solid #8fc4e8;
  font-weight: 700;
}

.tr-query,
.tr-update,
.tr-widen,
.tr-side,
.tr-route,
.tr-check,
.tr-proved,
.tr-failed {
  font-weight: 700;
}

.tr-query {
  color: #8fc4e8;
}

.tr-update,
.tr-proved {
  color: #6fcf97;
}

/* The value-carrying events: a soft chip that does not move the text. */
.tr-answer,
.tr-sol,
.tr-stored {
  font-weight: 700;
  border-radius: 2px;
}

.tr-answer {
  color: #8bd5ca;
  background: rgb(139 213 202 / 0.14);
  box-shadow: 0 0 0 2px rgb(139 213 202 / 0.14);
}

.tr-stored {
  color: #6fcf97;
  background: rgb(111 207 151 / 0.14);
  box-shadow: 0 0 0 2px rgb(111 207 151 / 0.14);
}

.tr-sol {
  color: #f0c674;
  background: rgb(240 198 116 / 0.14);
  box-shadow: 0 0 0 2px rgb(240 198 116 / 0.14);
}

.tr-widen,
.tr-route,
.tr-check,
.tr-failed {
  color: #f08a65;
}

.tr-iterate {
  color: #95adb4;
}

.tr-stable {
  color: #6c8188;
}

.tr-key,
.tr-step {
  color: #7c9096;
}

.tr-side {
  color: #c9a2e8;
}

.tr-unknown {
  color: #a7bbc0;
}

.tr-on {
  color: #6fcf97;
}

.tr-off {
  color: #6c8188;
}

.tr-value {
  color: #c4a7e7;
}

/* An old/new pair marks the components that differ, like a diff. */
.tr-removed,
.tr-added {
  border-radius: 2px;
}

.tr-removed {
  background: rgb(255 138 115 / 0.2);
}

.tr-added {
  background: rgb(111 207 151 / 0.2);
}

.analysis-graph-header {
  margin: 10px 0 12px;
}

/* Control-flow or analysis graph: two halves of one pill, the shown one filled. */
.graph-view-toggle {
  display: inline-flex;
  margin-bottom: 10px;
  overflow: hidden;
  border: 1px solid var(--border-strong);
  border-radius: 999px;
}

.graph-view-toggle button {
  padding: 5px 14px;
  color: var(--primary);
  background: var(--surface);
  border: 0;
  font: inherit;
  font-size: 0.86rem;
  font-weight: 650;
  cursor: pointer;
}

.graph-view-toggle button + button {
  border-left: 1px solid var(--border-strong);
}

.graph-view-toggle button[aria-checked="true"] {
  color: var(--surface);
  background: var(--primary);
}

.graph-view-toggle button:focus-visible {
  outline: 2px solid var(--accent);
  outline-offset: -2px;
}

.analysis-graph-tools {
  display: flex;
  align-items: center;
  justify-content: space-between;
  gap: 14px;
}

.analysis-graph-tools > span {
  color: var(--text-muted);
  font-size: 0.72rem;
}

.graph-toolbar {
  display: inline-flex;
  align-items: center;
  gap: 6px;
}

.graph-toolbar button {
  width: auto;
  min-width: 42px;
  min-height: 34px;
  height: 34px;
  padding: 0 10px;
  color: var(--primary);
  background: var(--surface);
  border: 1px solid var(--border);
  border-radius: var(--radius-sm);
  font-size: 0.82rem;
  font-weight: 750;
  cursor: pointer;
  transition:
    transform 100ms ease,
    border-color 150ms ease,
    background 150ms ease;
}

.graph-toolbar button:hover {
  transform: translateY(-1px);
  background: var(--surface-hover);
  border-color: var(--border-strong);
}

.graph-toolbar button:active {
  transform: translateY(0);
}

.graph-tooltip {
  position: fixed;
  z-index: 50;
  max-width: min(520px, calc(100vw - 32px));
  padding: 10px 12px;
  color: var(--editor-text);
  background: var(--surface-dark);
  border: 1px solid var(--editor-border);
  border-radius: var(--radius-sm);
  box-shadow: var(--shadow-hover);
  pointer-events: none;
}

.graph-tooltip strong {
  display: block;
  margin-bottom: 6px;
  font-family: var(--mono);
  font-size: 0.8rem;
}

.graph-tooltip pre {
  margin: 0;
  font-family: var(--mono);
  font-size: 0.76rem;
  line-height: 1.45;
  white-space: pre-wrap;
  overflow-wrap: anywhere;
}

/*
 * A fixed view the graph moves inside. touch-action: none hands pinch and drag to
 * the viewer instead of the browser, which would otherwise zoom or scroll the page.
 */
.analysis-graph {
  position: relative;
  height: clamp(420px, 78vh, 900px);
  overflow: hidden;
  background:
    radial-gradient(circle, rgb(23 75 87 / 0.12) 1px, transparent 1.2px) 0 0 / 22px 22px,
    var(--surface-muted);
  border: 1px solid var(--border);
  border-radius: 10px;
  cursor: grab;
  touch-action: none;
  user-select: none;
}

.analysis-graph:focus-visible {
  outline: 3px solid rgb(23 75 87 / 0.25);
  outline-offset: 2px;
}

/*
 * On a touch screen the view is most of the viewport's height, so let vertical
 * swipes scroll the page; a horizontal drag still pans and two fingers still pinch.
 */
@media (pointer: coarse) {
  .analysis-graph {
    height: clamp(320px, 60vh, 560px);
    touch-action: pan-y;
  }
}

.analysis-graph:active {
  cursor: grabbing;
}

.analysis-graph.is-over-context {
  cursor: move;
}

.analysis-graph.is-over-node {
  cursor: pointer;
}

.analysis-graph .analysis-graph-message {
  padding: 20px;
}

.graph-hint {
  color: var(--text-muted);
  font-size: 0.74rem;
}

.graph-hint kbd {
  font-size: 0.7rem;
}

.analysis-graph-message {
  margin: 0;
  color: var(--text-muted);
  font-size: 0.82rem;
}

.analysis-graph-message.error {
  color: var(--danger);
}

/* -------------------------------------------------------------------------- */
/* Soundness                                                                  */
/* -------------------------------------------------------------------------- */

.pipeline-proof {
  margin: 30px 0 0;
  padding: 20px 22px;
  overflow-x: auto;
  color: #dce9e9;
  background: var(--surface-dark);
  border: 1px solid var(--editor-border);
  border-radius: 10px;
  font-size: 0.79rem;
  line-height: 1.8;
  box-shadow: var(--shadow);
}

.pipeline-proof code {
  white-space: pre;
}

.theorem-grid,
.framework-grid {
  margin: 24px 0 0;
  background: var(--surface);
  border: 1px solid var(--border);
  border-radius: var(--radius);
  box-shadow: var(--shadow);
}

.theorem-grid > div,
.framework-grid > div {
  display: grid;
  grid-template-columns: minmax(230px, 0.9fr) minmax(0, 1.4fr);
  gap: 24px;
  padding: 17px 19px;
}

.theorem-grid > div + div,
.framework-grid > div + div {
  border-top: 1px solid var(--border);
}

.theorem-grid dt,
.framework-grid dt {
  color: var(--primary);
  font-weight: 700;
}

.theorem-grid dd,
.framework-grid dd {
  margin: 0;
  color: var(--text-muted);
  font-size: 0.9rem;
}

.theorem-grid dt code,
.framework-grid dt code {
  background: transparent;
  font-size: 0.82rem;
}

.soundness-claim {
  max-width: var(--prose);
  margin: 30px 0 0;
  padding: 3px 0 3px 20px;
  color: var(--text);
  border-left: 3px solid var(--accent);
  font-family: "Iowan Old Style", "Palatino Linotype", Georgia, serif;
  font-size: 1.28rem;
  line-height: 1.55;
}

/* -------------------------------------------------------------------------- */
/* Gallery                                                                    */
/* -------------------------------------------------------------------------- */

.gallery {
  display: grid;
  grid-template-columns: repeat(auto-fill, minmax(min(100%, 400px), 1fr));
  gap: 20px;
  margin-top: 30px;
}

.gallery figure {
  margin: 0;
  overflow: hidden;
  background: var(--surface);
  border: 1px solid var(--border);
  border-radius: var(--radius);
  box-shadow: var(--shadow);
  transition:
    transform 150ms ease,
    border-color 150ms ease,
    box-shadow 150ms ease;
}

.gallery figure:hover {
  transform: translateY(-3px);
  border-color: var(--border-strong);
  box-shadow: var(--shadow-hover);
}

.gallery a {
  display: block;
  aspect-ratio: 16 / 10;
  overflow: hidden;
  background: linear-gradient(135deg, #edf3f2, #e4eceb);
  border-bottom: 1px solid var(--border);
}

.gallery img {
  display: block;
  width: 100%;
  height: 100%;
  object-fit: contain;
  transition: transform 200ms ease;
}

.gallery figure:hover img {
  transform: scale(1.012);
}

.gallery figcaption {
  padding: 15px 17px 17px;
  color: var(--text-muted);
  font-size: 0.87rem;
  line-height: 1.55;
}

.gallery figcaption strong {
  display: block;
  margin-bottom: 3px;
  color: var(--text);
  font-size: 0.9rem;
}

/* -------------------------------------------------------------------------- */
/* Table                                                                      */
/* -------------------------------------------------------------------------- */

.table-shell {
  margin-top: 28px;
  overflow-x: auto;
  background: var(--surface);
  border: 1px solid var(--border);
  border-radius: var(--radius);
  box-shadow: var(--shadow);
}

table {
  width: 100%;
  border-collapse: collapse;
  text-align: left;
  font-size: 0.88rem;
}

th,
td {
  padding: 14px 16px;
  vertical-align: top;
}

th {
  color: var(--primary);
  background: var(--surface-muted);
  border-bottom: 1px solid var(--border);
  font-size: 0.78rem;
  font-weight: 800;
  letter-spacing: 0.02em;
}

tbody tr + tr td {
  border-top: 1px solid var(--border);
}

tbody tr:hover {
  background: var(--surface-hover);
}

td code,
th code {
  color: var(--primary);
  background: transparent;
  font-size: 0.78rem;
}

/* -------------------------------------------------------------------------- */
/* Resources                                                                  */
/* -------------------------------------------------------------------------- */

.link-list {
  display: grid;
  grid-template-columns: repeat(auto-fill, minmax(min(100%, 420px), 1fr));
  gap: 16px;
  margin: 28px 0 0;
  padding: 0;
  list-style: none;
}

.link-list li {
  min-width: 0;
}

.resource-card {
  display: grid;
  grid-template-columns: 46px minmax(0, 1fr) auto;
  align-items: start;
  gap: 15px;
  height: 100%;
  padding: 20px;
  color: inherit;
  background: var(--surface);
  border: 1px solid var(--border);
  border-radius: var(--radius);
  box-shadow: var(--shadow);
  text-decoration: none;
  transition:
    transform 150ms ease,
    border-color 150ms ease,
    box-shadow 150ms ease,
    background 150ms ease;
}

.resource-card:hover {
  transform: translateY(-2px);
  background: var(--surface-hover);
  border-color: var(--border-strong);
  box-shadow: var(--shadow-hover);
}

.resource-card:focus-visible,
.actions a:focus-visible,
button:focus-visible,
a:focus-visible {
  outline: 3px solid rgb(23 75 87 / 0.22);
  outline-offset: 3px;
}

.resource-icon {
  display: grid;
  width: 46px;
  height: 46px;
  place-items: center;
  color: var(--primary);
  background: var(--primary-soft);
  border-radius: 10px;
}

.resource-icon-accent {
  color: var(--accent);
  background: var(--accent-soft);
}

.resource-icon i {
  font-size: 1.25rem;
}

.resource-card-featured {
  border-color: rgb(215 102 66 / 0.3);
}

.resource-card-featured:hover {
  border-color: rgb(215 102 66 / 0.62);
}

.resource-content {
  display: block;
  min-width: 0;
}

.resource-title {
  display: block;
  margin-top: 1px;
  color: var(--primary);
  font-size: 0.98rem;
  font-weight: 750;
  line-height: 1.35;
}

.resource-description {
  display: block;
  margin-top: 7px;
  color: var(--text-muted);
  font-size: 0.86rem;
  line-height: 1.55;
}

.resource-description code {
  background: var(--surface-muted);
}

.resource-arrow {
  margin-top: 2px;
  color: var(--border-strong);
  font-size: 1.15rem;
  line-height: 1;
  transition:
    color 150ms ease,
    transform 150ms ease;
}

.resource-card:hover .resource-arrow {
  transform: translateX(2px);
  color: var(--primary);
}

/* -------------------------------------------------------------------------- */
/* Footer                                                                     */
/* -------------------------------------------------------------------------- */

.site-footer {
  color: var(--text-muted);
  background: var(--paper);
  border-top: 1px solid var(--border);
}

.footer-content {
  display: flex;
  align-items: center;
  justify-content: space-between;
  gap: 18px;
  padding-top: 26px;
  padding-bottom: 30px;
  font-size: 0.84rem;
}

.footer-content a {
  display: inline-flex;
  align-items: center;
  gap: 7px;
  text-decoration: none;
}

.footer-content a:hover {
  text-decoration: underline;
  text-underline-offset: 3px;
}

/* -------------------------------------------------------------------------- */
/* Project logos                                                              */
/* -------------------------------------------------------------------------- */

.logo-strip {
  display: flex;
  flex-wrap: wrap;
  align-items: center;
  gap: 10px 22px;
  margin: 28px 0 0;
  padding: 0;
  list-style: none;
}

.logo-strip-label {
  color: var(--text-muted);
  font: 700 0.72rem var(--mono);
  letter-spacing: 0.14em;
  text-transform: uppercase;
}

.logo-strip a {
  display: inline-flex;
  align-items: center;
  gap: 8px;
  color: var(--text);
  font-size: 0.9rem;
  font-weight: 650;
  text-decoration: none;
  opacity: 0.85;
  transition: opacity 150ms ease;
}

.logo-strip a:hover {
  opacity: 1;
}

.logo-strip img {
  width: auto;
  height: 32px;
}

.inline-logo {
  width: auto;
  height: 1.15em;
  vertical-align: -0.2em;
}

.logo-badge {
  fill: var(--surface);
  stroke: var(--border);
  stroke-width: 1.5;
}

.logo-credits {
  padding-bottom: 22px;
  color: var(--text-faint);
  font-size: 0.74rem;
}

.logo-credits a {
  color: inherit;
}

/* -------------------------------------------------------------------------- */
/* Responsive                                                                 */
/* -------------------------------------------------------------------------- */

@media (max-width: 820px) {
  .page-shell {
    width: min(100% - 36px, 1600px);
  }

  .hero-content {
    padding-top: 40px;
    padding-bottom: 44px;
  }

  .section {
    padding: 58px 0;
  }

  .analyzer {
    padding: 20px;
  }

  .analyzer-workspace {
    grid-template-areas:
      "controls"
      "editor";
    grid-template-columns: minmax(0, 1fr);
  }

  .raw-result-panes {
    grid-template-columns: minmax(0, 1fr);
  }

  .theorem-grid > div,
  .framework-grid > div {
    grid-template-columns: 1fr;
    gap: 6px;
  }

  .footer-content {
    align-items: flex-start;
    flex-direction: column;
  }
}

/* A sticky bar that wraps to three rows costs a phone a sixth of its screen for the
   whole page, so below this width the call to action shares the brand's row and the
   links keep one of their own. */
@media (max-width: 560px) {
  /* The toolbar's groups do not fit one phone row, and the file name is the one
     label nothing else depends on. */
  .editor-toolbar {
    flex-wrap: wrap;
    padding-block: 6px;
  }

  .editor-file {
    display: none;
  }

  .site-nav-inner {
    position: relative;
    min-height: 0;
    padding: 8px 0;
    gap: 4px;
  }

  .site-links {
    flex: 1 1 100%;
    gap: 2px 10px;
  }

  .site-links a {
    font-size: 0.82rem;
  }

  /* The text links take the second row; the actions share the brand's. */
  .site-actions {
    position: absolute;
    top: 8px;
    right: 0;
  }
}

@media (max-width: 640px) {
  .page-shell {
    width: min(100% - 28px, 1600px);
  }

  .hero-banner {
    height: 170px;
  }

  .hero-content {
    padding-top: 32px;
    padding-bottom: 38px;
  }

  h1 {
    font-size: 3rem;
  }

  .actions a {
    width: 100%;
    justify-content: center;
  }

  .section {
    padding: 48px 0;
  }

  .analyzer {
    gap: 18px;
    padding: 14px;
    border-radius: 12px;
  }

  .analyzer-controls {
    padding: 14px;
  }

  .control-group {
    flex: 1 1 100%;
  }

  #program-editor .cm-editor,
  #program-editor .cm-scroller {
    min-height: 420px;
  }

  .analysis-graph-tools {
    align-items: flex-start;
    flex-direction: column;
    gap: 8px;
  }

  .analysis-graph-tools > span {
    text-align: left;
  }

  .graph-toolbar {
    flex-wrap: wrap;
  }

  .gallery a {
    aspect-ratio: 4 / 3;
  }

  .resource-card {
    grid-template-columns: 40px minmax(0, 1fr) auto;
    gap: 12px;
    padding: 16px;
  }

  .resource-icon {
    width: 40px;
    height: 40px;
  }

  .pipeline-proof {
    padding: 16px;
    font-size: 0.7rem;
  }
}

@media (prefers-reduced-motion: reduce) {
  html {
    scroll-behavior: auto;
  }

  *,
  *::before,
  *::after {
    transition-duration: 0.01ms !important;
    animation-duration: 0.01ms !important;
    animation-iteration-count: 1 !important;
  }
}

/* -------------------------------------------------------------------------- */
/* Regression examples                                                        */
/* -------------------------------------------------------------------------- */

.examples-dialog {
  width: min(1100px, calc(100vw - 32px));
  max-height: min(86vh, 920px);
  padding: 0;
  color: var(--text);
  background: var(--surface);
  border: 1px solid var(--border);
  border-radius: var(--radius-lg);
  box-shadow: var(--shadow-hover);
}

.examples-dialog::backdrop {
  background: rgb(16 40 46 / 0.45);
}

.examples-panel {
  display: flex;
  flex-direction: column;
  max-height: inherit;
}

.examples-header {
  display: flex;
  align-items: flex-end;
  gap: 16px;
  padding: 20px 22px 12px;
}

.examples-header .eyebrow {
  margin-bottom: 4px;
  font-size: 0.68rem;
}

.examples-header h2 {
  margin: 0;
  font-size: 1.3rem;
}

.examples-header input {
  flex: 1;
  min-width: 0;
  min-height: 40px;
  padding: 8px 12px;
  color: var(--text);
  background: var(--surface);
  border: 1px solid var(--border);
  border-radius: var(--radius-sm);
}

.examples-header input:focus {
  border-color: var(--primary);
  outline: 2px solid rgb(23 75 87 / 0.14);
}

.examples-close {
  width: 40px;
  height: 40px;
  color: var(--text-muted);
  background: var(--surface-muted);
  border: 1px solid var(--border);
  border-radius: var(--radius-sm);
  cursor: pointer;
}

.examples-close:hover {
  color: var(--primary);
}

.examples-note {
  margin: 0;
  padding: 0 22px 12px;
  color: var(--text-muted);
  font-size: 0.8rem;
  border-bottom: 1px solid var(--border);
}

.examples-body {
  overflow-y: auto;
  padding: 0 22px 22px;
}

.examples-group h3 {
  position: sticky;
  top: 0;
  z-index: 1;
  display: flex;
  align-items: center;
  gap: 8px;
  margin: 0;
  padding: 14px 0 8px;
  font-size: 0.92rem;
  background: var(--surface);
}

.examples-grid {
  display: grid;
  grid-template-columns: repeat(auto-fill, minmax(min(100%, 250px), 1fr));
  gap: 10px;
}

.example-card {
  display: flex;
  flex-direction: column;
  gap: 6px;
  min-width: 0;
  padding: 10px 12px;
  color: var(--text);
  text-align: left;
  background: var(--surface-muted);
  border: 1px solid var(--border);
  border-radius: var(--radius-sm);
  font: inherit;
  cursor: pointer;
}

.example-card:hover,
.example-card:focus-visible {
  background: var(--surface);
  border-color: var(--primary);
}

.example-card[hidden],
.examples-group[hidden] {
  display: none;
}

.example-card.picked {
  background: var(--surface);
  border-color: var(--border-strong);
  box-shadow: inset 3px 0 0 var(--accent);
}

.example-card.picked strong {
  font-family: inherit;
  font-size: 0.92rem;
}

/* Pinned to the card's bottom, so paths line up across a row of cards. */
.example-path {
  margin-top: auto;
  overflow: hidden;
  color: var(--text-faint);
  font-size: 0.68rem;
  text-overflow: ellipsis;
  white-space: nowrap;
}

.example-card strong {
  font-family: var(--mono);
  font-size: 0.82rem;
}

.example-chips {
  display: flex;
  flex-wrap: wrap;
  gap: 4px;
}

.example-chip {
  padding: 0 7px;
  color: var(--text-muted);
  background: var(--surface);
  border: 1px solid var(--border);
  border-radius: 999px;
  font: 600 0.68rem var(--mono);
}

.example-chip.precision {
  color: var(--success);
  background: var(--success-soft);
}

.example-chip.soundness {
  color: var(--primary);
  background: var(--primary-soft);
}

.example-chip.known-imprecision {
  color: var(--caution);
  background: #f7efe2;
}

.example-summary {
  display: -webkit-box;
  overflow: hidden;
  color: var(--text-muted);
  font-size: 0.76rem;
  line-height: 1.4;
  -webkit-box-orient: vertical;
  -webkit-line-clamp: 3;
}

.examples-message {
  margin: 18px 0 0;
  color: var(--text-muted);
  font-size: 0.86rem;
}

@media (max-width: 640px) {
  .examples-header {
    flex-wrap: wrap;
  }

  .examples-header input {
    order: 3;
    flex-basis: 100%;
  }
}

.replay-stack,
.replay-routes {
  margin: 0 0 12px;
  padding-left: 1.4em;
  font-family: var(--mono);
  font-size: 0.8rem;
}

.replay-stack-entry.is-active {
  font-weight: 600;
}

.replay-global-detail {
  display: block;
  font-size: 0.75rem;
  color: var(--text-faint);
}

.replay-counters {
  width: 100%;
  table-layout: auto;
  margin-bottom: 12px;
  border-collapse: collapse;
  font-size: 0.75rem;
}

.replay-counters th,
.replay-counters td {
  padding: 2px 4px;
  text-align: right;
}

.replay-counters td:first-child {
  width: 100%;
  max-width: 0;
  overflow: hidden;
  text-overflow: ellipsis;
  white-space: nowrap;
}

.replay-route {
  font-weight: 600;
}

.replay-routes li + li {
  margin-top: 6px;
}

.replay-counters th:first-child,
.replay-counters td:first-child {
  text-align: left;
  font-family: var(--mono);
}