/* ==========================================================================
   VERISYS-AI — FORMAL VERIFICATION & INVARIANT SYNTHESIS STYLESHEET
   Design Theme: Academic Scientific Research IDE & Proof Assistant Workbench
   ========================================================================== */

:root {
  --bg-darkest: #050912;
  --bg-header: #080E1C;
  --bg-panel: #0D1629;
  --bg-card: #121F38;
  --bg-card-hover: #182A4D;
  
  --border-subtle: rgba(255, 255, 255, 0.08);
  --border-active: #38BDF8;
  
  --text-main: #F8FAFC;
  --text-muted: #94A3B8;
  --text-dim: #64748B;
  
  --cyan-bright: #38BDF8;
  --cyan-glow: rgba(56, 189, 248, 0.2);
  --emerald-pass: #10B981;
  --emerald-glow: rgba(16, 185, 129, 0.2);
  --rose-fail: #F43F5E;
  --rose-glow: rgba(244, 63, 94, 0.2);
  --amber-warn: #F59E0B;
  --amber-glow: rgba(245, 158, 11, 0.2);
  
  --font-sans: 'Inter', -apple-system, sans-serif;
  --font-mono: 'JetBrains Mono', 'Fira Code', monospace;
  
  --radius-xs: 4px;
  --radius-sm: 6px;
  --radius-md: 10px;
  --radius-lg: 14px;
}

*, *::before, *::after {
  box-sizing: border-box;
  margin: 0;
  padding: 0;
}

body {
  font-family: var(--font-sans);
  background-color: var(--bg-darkest);
  color: var(--text-main);
  font-size: 13px;
  line-height: 1.5;
  -webkit-font-smoothing: antialiased;
  min-height: 100vh;
  display: flex;
  flex-direction: column;
}

.container-fluid {
  width: 100%;
  padding: 0 20px;
}

/* ════════ HEADER & NAVIGATION ════════ */
.app-header {
  background: var(--bg-header);
  border-bottom: 1px solid var(--border-subtle);
  padding: 10px 0;
  position: sticky;
  top: 0;
  z-index: 100;
}

.header-inner {
  display: flex;
  justify-content: space-between;
  align-items: center;
  gap: 20px;
}

.brand-group {
  display: flex;
  align-items: center;
  gap: 12px;
}

.brand-badge {
  width: 34px;
  height: 34px;
  background: linear-gradient(135deg, #0284C7 0%, #0F172A 100%);
  border: 1px solid var(--cyan-bright);
  border-radius: var(--radius-sm);
  display: flex;
  align-items: center;
  justify-content: center;
  font-family: var(--font-mono);
  font-size: 18px;
  font-weight: 700;
  color: #FFFFFF;
  box-shadow: 0 0 15px var(--cyan-glow);
}

.brand-title {
  font-size: 15px;
  font-weight: 800;
  letter-spacing: -0.2px;
  color: var(--text-main);
}

.brand-title em {
  font-style: normal;
  color: var(--cyan-bright);
}

.version-tag {
  font-size: 10px;
  font-family: var(--font-mono);
  color: var(--text-dim);
  font-weight: 500;
}

.brand-sub {
  font-size: 10.5px;
  color: var(--text-muted);
}

/* Navigation Tabs */
.nav-tabs {
  display: flex;
  background: #050B16;
  border: 1px solid var(--border-subtle);
  padding: 3px;
  border-radius: var(--radius-sm);
  gap: 4px;
}

.nav-tab {
  background: transparent;
  border: none;
  color: var(--text-muted);
  font-family: var(--font-sans);
  font-size: 12px;
  font-weight: 600;
  padding: 7px 14px;
  border-radius: var(--radius-xs);
  cursor: pointer;
  display: flex;
  align-items: center;
  gap: 6px;
  transition: all 0.2s ease;
}

.nav-tab:hover {
  color: var(--text-main);
  background: rgba(255, 255, 255, 0.04);
}

.nav-tab.is-active {
  background: var(--bg-card);
  color: var(--cyan-bright);
  border: 1px solid rgba(56, 189, 248, 0.3);
  box-shadow: 0 2px 8px rgba(0, 0, 0, 0.3);
}

.tab-icon {
  font-family: var(--font-mono);
  font-weight: 700;
}

.header-actions {
  display: flex;
  align-items: center;
  gap: 14px;
}

.bound-control {
  display: flex;
  align-items: center;
  gap: 6px;
  font-size: 11.5px;
  color: var(--text-muted);
  font-family: var(--font-mono);
}

.bound-control select {
  background: #050B16;
  border: 1px solid var(--border-subtle);
  color: var(--cyan-bright);
  font-family: var(--font-mono);
  font-size: 11px;
  padding: 5px 8px;
  border-radius: var(--radius-xs);
  outline: none;
}

/* ════════ BUTTONS ════════ */
.btn {
  font-family: var(--font-sans);
  font-size: 12px;
  font-weight: 700;
  padding: 8px 14px;
  border-radius: var(--radius-xs);
  cursor: pointer;
  border: none;
  display: inline-flex;
  align-items: center;
  justify-content: center;
  gap: 6px;
  transition: all 0.2s ease;
}

.btn-primary {
  background: #0284C7;
  color: #FFFFFF;
}

.btn-primary:hover {
  background: #38BDF8;
  box-shadow: 0 0 15px var(--cyan-glow);
}

.btn-secondary {
  background: var(--bg-card);
  border: 1px solid var(--border-subtle);
  color: var(--text-main);
}

.btn-secondary:hover {
  background: var(--bg-card-hover);
  border-color: var(--cyan-bright);
}

.btn-block { width: 100%; }
.btn-sm { font-size: 11px; padding: 5px 10px; }
.btn-lg { font-size: 14px; padding: 12px 20px; }

/* ════════ MAIN LAYOUT & TABS ════════ */
.main-content {
  flex: 1;
  padding: 16px 0 30px;
}

.tab-panel {
  display: none;
}

.tab-panel.is-active {
  display: block;
}

/* ──────────────── VERIFIER TAB ──────────────── */
.verifier-layout {
  display: grid;
  grid-template-columns: 1fr 1.15fr;
  gap: 16px;
  height: calc(100vh - 120px);
  min-height: 600px;
  padding: 0 20px;
}

.editor-pane {
  background: var(--bg-panel);
  border: 1px solid var(--border-subtle);
  border-radius: var(--radius-md);
  display: flex;
  flex-direction: column;
  overflow: hidden;
}

.pane-toolbar {
  background: var(--bg-header);
  border-bottom: 1px solid var(--border-subtle);
  padding: 8px 14px;
  display: flex;
  justify-content: space-between;
  align-items: center;
  gap: 10px;
}

.preset-selector {
  display: flex;
  align-items: center;
  gap: 8px;
  font-size: 11.5px;
  color: var(--text-muted);
}

.preset-selector select {
  background: #050B16;
  border: 1px solid var(--border-subtle);
  color: var(--text-main);
  font-family: var(--font-sans);
  font-size: 12px;
  font-weight: 600;
  padding: 5px 10px;
  border-radius: var(--radius-xs);
  outline: none;
  max-width: 320px;
}

.preset-selector select:focus {
  border-color: var(--cyan-bright);
}

.editor-meta-tags {
  display: flex;
  gap: 6px;
}

.tag-pill {
  font-family: var(--font-mono);
  font-size: 9.5px;
  color: var(--text-dim);
  background: rgba(255, 255, 255, 0.04);
  padding: 2px 6px;
  border-radius: 3px;
}

.cm-wrapper {
  flex: 1;
  overflow: hidden;
  position: relative;
}

.CodeMirror {
  height: 100% !important;
  font-family: var(--font-mono) !important;
  font-size: 13px !important;
  line-height: 1.6 !important;
  background: #070D1A !important;
}

.editor-footer-help {
  background: var(--bg-header);
  border-top: 1px solid var(--border-subtle);
  padding: 6px 14px;
  font-size: 11px;
  color: var(--text-dim);
  font-family: var(--font-mono);
}

.editor-footer-help code {
  color: var(--cyan-bright);
  background: rgba(56, 189, 248, 0.08);
  padding: 1px 4px;
  border-radius: 3px;
}

/* ──────────────── RESULTS PANE ──────────────── */
.results-pane {
  background: var(--bg-panel);
  border: 1px solid var(--border-subtle);
  border-radius: var(--radius-md);
  display: flex;
  flex-direction: column;
  overflow-y: auto;
  padding: 16px;
  gap: 14px;
}

/* Status Banner */
.status-banner {
  border-radius: var(--radius-sm);
  padding: 14px 18px;
  display: flex;
  align-items: center;
  gap: 14px;
  border: 1px solid transparent;
  transition: all 0.25s ease;
}

.banner-pending {
  background: rgba(100, 116, 139, 0.1);
  border-color: rgba(100, 116, 139, 0.3);
}

.banner-pass {
  background: rgba(16, 185, 129, 0.1);
  border-color: var(--emerald-pass);
  box-shadow: 0 0 20px var(--emerald-glow);
}

.banner-fail {
  background: rgba(244, 63, 94, 0.12);
  border-color: var(--rose-fail);
  box-shadow: 0 0 20px var(--rose-glow);
}

.sb-icon {
  font-size: 22px;
}

.sb-title {
  font-size: 14px;
  font-weight: 800;
  letter-spacing: -0.2px;
}

.banner-pass .sb-title { color: var(--emerald-pass); }
.banner-fail .sb-title { color: var(--rose-fail); }
.banner-pending .sb-title { color: var(--text-muted); }

.sb-desc {
  font-size: 11.5px;
  color: var(--text-muted);
}

.sb-meta {
  margin-left: auto;
  font-family: var(--font-mono);
  font-size: 10px;
  color: var(--text-dim);
  text-transform: uppercase;
}

/* Loop Invariant Inspector Strip */
.loop-strip {
  background: var(--bg-card);
  border: 1px solid var(--border-subtle);
  border-radius: var(--radius-sm);
  padding: 14px;
}

.loop-strip-header {
  display: flex;
  justify-content: space-between;
  align-items: center;
  margin-bottom: 10px;
}

.lsh-title {
  font-size: 12px;
  font-weight: 700;
  color: var(--text-main);
}

.lsh-badge {
  font-family: var(--font-mono);
  font-size: 9.5px;
  background: rgba(56, 189, 248, 0.1);
  color: var(--cyan-bright);
  padding: 2px 6px;
  border-radius: 3px;
}

.loop-cards-grid {
  display: grid;
  grid-template-columns: repeat(3, 1fr);
  gap: 10px;
}

.loop-card {
  background: #080F1E;
  border: 1px solid var(--border-subtle);
  border-radius: var(--radius-xs);
  padding: 10px;
  display: flex;
  flex-direction: column;
  transition: all 0.2s ease;
}

.loop-card.is-pass {
  border-color: var(--emerald-pass);
  background: rgba(16, 185, 129, 0.05);
}

.loop-card.is-fail {
  border-color: var(--rose-fail);
  background: rgba(244, 63, 94, 0.08);
}

.lc-head {
  display: flex;
  justify-content: space-between;
  align-items: center;
  margin-bottom: 6px;
}

.lc-name {
  font-size: 11px;
  font-weight: 700;
  color: var(--text-main);
}

.lc-status {
  font-family: var(--font-mono);
  font-size: 9px;
  font-weight: 700;
  padding: 1.5px 5px;
  border-radius: 3px;
}

.badge-wait { background: #1E293B; color: var(--text-dim); }
.badge-pass { background: var(--emerald-pass); color: #050912; }
.badge-fail { background: var(--rose-fail); color: #FFFFFF; }

.lc-formula {
  font-size: 11px;
  color: var(--cyan-bright);
  margin-bottom: 4px;
}

.lc-desc {
  font-size: 10px;
  color: var(--text-dim);
  line-height: 1.35;
}

/* Verification Conditions Section */
.vc-section {
  flex: 1;
}

.vc-header {
  display: flex;
  justify-content: space-between;
  align-items: center;
  margin-bottom: 10px;
}

.vc-header h3 {
  font-size: 13px;
  font-weight: 700;
}

.vc-count {
  font-family: var(--font-mono);
  font-size: 10px;
  color: var(--text-dim);
}

.vc-list {
  display: flex;
  flex-direction: column;
  gap: 10px;
}

.vc-card {
  background: var(--bg-card);
  border: 1px solid var(--border-subtle);
  border-radius: var(--radius-sm);
  padding: 12px 14px;
  transition: all 0.2s ease;
}

.vc-card.vc-pass {
  border-left: 3.5px solid var(--emerald-pass);
}

.vc-card.vc-fail {
  border-left: 3.5px solid var(--rose-fail);
}

.vc-top {
  display: flex;
  justify-content: space-between;
  align-items: center;
  margin-bottom: 8px;
}

.vc-label {
  font-size: 12px;
  font-weight: 700;
  color: var(--text-main);
}

.vc-status-badge {
  font-family: var(--font-mono);
  font-size: 9.5px;
  font-weight: 700;
  padding: 2px 7px;
  border-radius: 3px;
}

.vc-math-box {
  background: #070E1C;
  border: 1px solid var(--border-subtle);
  border-radius: var(--radius-xs);
  padding: 10px 12px;
  overflow-x: auto;
  margin-bottom: 8px;
  color: var(--cyan-bright);
}

.vc-result-meta {
  font-size: 11px;
  color: var(--text-muted);
}

.cex-box {
  margin-top: 8px;
  background: rgba(244, 63, 94, 0.1);
  border: 1px dashed var(--rose-fail);
  border-radius: var(--radius-xs);
  padding: 8px 10px;
  font-family: var(--font-mono);
  font-size: 11px;
  color: #FECDD3;
}

.cex-box strong {
  color: #FFE4E6;
}

.empty-state {
  text-align: center;
  padding: 40px 20px;
  color: var(--text-dim);
  font-size: 12px;
  border: 1px dashed var(--border-subtle);
  border-radius: var(--radius-sm);
}

/* Theory note */
.theory-note {
  background: #060D1A;
  border: 1px solid rgba(56, 189, 248, 0.2);
  border-radius: var(--radius-sm);
  padding: 12px 14px;
}

.tn-title {
  font-size: 11px;
  font-weight: 700;
  color: var(--cyan-bright);
  margin-bottom: 4px;
  text-transform: uppercase;
  letter-spacing: 0.5px;
}

.theory-note p {
  font-size: 11px;
  color: var(--text-muted);
  line-height: 1.5;
}

/* ──────────────── AUTOMATA TAB ──────────────── */
.automata-layout {
  display: grid;
  grid-template-columns: 380px 1fr;
  gap: 16px;
  height: calc(100vh - 120px);
  min-height: 600px;
  padding: 0 20px;
}

.automata-sidebar {
  background: var(--bg-panel);
  border: 1px solid var(--border-subtle);
  border-radius: var(--radius-md);
  padding: 18px;
  display: flex;
  flex-direction: column;
  gap: 14px;
  overflow-y: auto;
}

.as-header h3 {
  font-size: 14px;
  font-weight: 700;
  margin-bottom: 8px;
}

.as-presets {
  display: flex;
  flex-direction: column;
  gap: 4px;
  font-size: 11px;
  color: var(--text-muted);
}

.as-presets select {
  background: #050B16;
  border: 1px solid var(--border-subtle);
  color: var(--text-main);
  font-family: var(--font-sans);
  font-size: 12px;
  padding: 6px 10px;
  border-radius: var(--radius-xs);
  outline: none;
}

.as-section h4 {
  font-size: 11.5px;
  font-weight: 700;
  color: var(--text-muted);
  text-transform: uppercase;
  letter-spacing: 0.5px;
  margin-bottom: 8px;
}

.prop-check-row {
  display: flex;
  flex-direction: column;
  gap: 8px;
}

.automata-result-box {
  background: var(--bg-card);
  border: 1px solid var(--border-subtle);
  border-radius: var(--radius-sm);
  padding: 12px;
}

.arb-title {
  font-size: 12.5px;
  font-weight: 700;
  margin-bottom: 4px;
}

.arb-msg {
  font-size: 11px;
  color: var(--text-muted);
  line-height: 1.45;
}

.arb-trace-controls {
  margin-top: 10px;
  display: flex;
  gap: 6px;
}

.trace-log-box {
  background: #050B16;
  border: 1px solid var(--border-subtle);
  border-radius: var(--radius-xs);
  padding: 10px;
  flex: 1;
  display: flex;
  flex-direction: column;
}

.tlb-header {
  font-size: 10.5px;
  font-weight: 700;
  color: var(--text-dim);
  text-transform: uppercase;
  letter-spacing: 0.5px;
  margin-bottom: 6px;
}

.tlb-content {
  font-family: var(--font-mono);
  font-size: 11px;
  color: var(--cyan-bright);
  overflow-y: auto;
  line-height: 1.5;
}

.model-legend {
  display: flex;
  flex-wrap: wrap;
  gap: 10px;
  padding-top: 8px;
  border-top: 1px solid var(--border-subtle);
  font-size: 10.5px;
  color: var(--text-dim);
}

.legend-item {
  display: flex;
  align-items: center;
  gap: 4px;
}

.dot {
  width: 8px;
  height: 8px;
  border-radius: 50%;
}
.dot-start { background: #38BDF8; }
.dot-good { background: #10B981; }
.dot-bad { background: #F43F5E; }
.dot-active { background: #F59E0B; }

.automata-canvas-pane {
  background: var(--bg-panel);
  border: 1px solid var(--border-subtle);
  border-radius: var(--radius-md);
  display: flex;
  flex-direction: column;
  overflow: hidden;
}

.canvas-toolbar {
  background: var(--bg-header);
  border-bottom: 1px solid var(--border-subtle);
  padding: 10px 16px;
  display: flex;
  justify-content: space-between;
  align-items: center;
}

.canvas-title {
  font-size: 12.5px;
  font-weight: 700;
  color: var(--text-main);
}

.zoom-hint {
  font-size: 10px;
  font-family: var(--font-mono);
  color: var(--text-dim);
}

#vis_network_canvas {
  flex: 1;
  background: #060B16;
}

/* ──────────────── CERTIFICATES TAB ──────────────── */
.certificate-layout {
  padding: 0 20px;
}

.cert-header-card {
  background: var(--bg-panel);
  border: 1px solid var(--border-subtle);
  border-radius: var(--radius-md);
  padding: 24px;
  display: flex;
  justify-content: space-between;
  align-items: center;
  gap: 20px;
  margin-bottom: 16px;
}

.chc-left h2 {
  font-size: 18px;
  font-weight: 800;
  color: var(--text-main);
  margin-bottom: 4px;
}

.chc-left p {
  font-size: 12.5px;
  color: var(--text-muted);
}

.cert-grid {
  display: grid;
  grid-template-columns: 1fr 1fr;
  gap: 16px;
}

.cert-card {
  background: var(--bg-panel);
  border: 1px solid var(--border-subtle);
  border-radius: var(--radius-md);
  padding: 20px;
  display: flex;
  flex-direction: column;
}

.cc-head {
  display: flex;
  justify-content: space-between;
  align-items: center;
  margin-bottom: 14px;
  padding-bottom: 10px;
  border-bottom: 1px solid var(--border-subtle);
}

.cc-head h3 {
  font-size: 14px;
  font-weight: 700;
}

.hash-badge {
  font-family: var(--font-mono);
  font-size: 9px;
  font-weight: 700;
  background: rgba(16, 185, 129, 0.1);
  color: var(--emerald-pass);
  padding: 2px 6px;
  border-radius: 3px;
}

.session-history-list {
  display: flex;
  flex-direction: column;
  gap: 8px;
  max-height: 380px;
  overflow-y: auto;
}

.history-item {
  background: #080F1E;
  border: 1px solid var(--border-subtle);
  border-radius: var(--radius-xs);
  padding: 10px 12px;
  display: flex;
  justify-content: space-between;
  align-items: center;
}

.hi-title {
  font-size: 12px;
  font-weight: 700;
  color: var(--text-main);
}

.hi-meta {
  font-size: 10px;
  color: var(--text-dim);
  font-family: var(--font-mono);
}

.proof-tree-preview {
  background: #050B16;
  border: 1px solid var(--border-subtle);
  border-radius: var(--radius-xs);
  padding: 14px;
  font-family: var(--font-mono);
  font-size: 11.5px;
  color: var(--cyan-bright);
  white-space: pre-wrap;
  min-height: 220px;
  margin-bottom: 14px;
  line-height: 1.6;
}

.hash-box {
  background: #070E1A;
  border: 1px solid var(--border-subtle);
  border-radius: var(--radius-xs);
  padding: 10px 12px;
}

.hb-label {
  display: block;
  font-size: 10px;
  color: var(--text-dim);
  text-transform: uppercase;
  margin-bottom: 4px;
}

.hb-hash {
  font-family: var(--font-mono);
  font-size: 11px;
  color: var(--emerald-pass);
  word-break: break-all;
}

/* ════════ FOOTER & TOAST ════════ */
.app-footer {
  background: var(--bg-header);
  border-top: 1px solid var(--border-subtle);
  padding: 10px 0;
  margin-top: auto;
}

.footer-inner {
  display: flex;
  justify-content: space-between;
  align-items: center;
  font-size: 11px;
  color: var(--text-dim);
}

.footer-left a {
  color: var(--cyan-bright);
  text-decoration: none;
}

.sep { margin: 0 8px; opacity: 0.3; }

.toast {
  position: fixed;
  bottom: 24px;
  right: 24px;
  background: var(--cyan-bright);
  color: #050912;
  font-weight: 700;
  font-size: 12px;
  padding: 10px 18px;
  border-radius: var(--radius-sm);
  box-shadow: 0 8px 25px rgba(0, 0, 0, 0.6);
  transform: translateY(100px);
  opacity: 0;
  transition: all 0.3s cubic-bezier(0.16, 1, 0.3, 1);
  z-index: 1000;
}

.toast.show {
  transform: translateY(0);
  opacity: 1;
}

.is-hidden { display: none !important; }