:root {
  --bg-primary: #f5f7fa;
  --bg-sidebar: #1a2332;
  --bg-sidebar-hover: #243044;
  --bg-sidebar-active: #2d4a6f;
  --bg-code: #1e293b;
  --bg-card: #ffffff;
  --bg-note: #eef6ff;
  --bg-tip: #eefff4;
  --bg-warn: #fff8ee;
  --text-primary: #1a2332;
  --text-sidebar: #c8d6e5;
  --text-sidebar-heading: #7f8fa6;
  --text-muted: #636e72;
  --text-code: #e2e8f0;
  --accent-green: #00c853;
  --accent-orange: #ff9100;
  --accent-blue: #448aff;
  --accent-red: #ff5252;
  --border-color: #dfe6e9;
  --border-sidebar: #2a3a50;
  --shadow: 0 1px 3px rgba(0,0,0,0.08), 0 1px 2px rgba(0,0,0,0.06);
  --shadow-lg: 0 4px 12px rgba(0,0,0,0.1);
  --sidebar-width: 280px;
  --content-max: 920px;
}

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

html { scroll-behavior: smooth; font-size: 16px; }

body {
  font-family: -apple-system, BlinkMacSystemFont, "Segoe UI", Roboto, "Helvetica Neue", Arial, "PingFang SC", "Microsoft YaHei", sans-serif;
  background: var(--bg-primary);
  color: var(--text-primary);
  line-height: 1.7;
  display: flex;
  min-height: 100vh;
}

/* Sidebar */
.sidebar {
  width: var(--sidebar-width);
  min-width: var(--sidebar-width);
  background: var(--bg-sidebar);
  color: var(--text-sidebar);
  height: 100vh;
  position: fixed;
  top: 0;
  left: 0;
  overflow-y: auto;
  z-index: 100;
  display: flex;
  flex-direction: column;
}

.sidebar-header {
  padding: 20px 20px 16px;
  border-bottom: 1px solid var(--border-sidebar);
}

.sidebar-header h2 {
  font-size: 1.1rem;
  font-weight: 700;
  color: #fff;
  letter-spacing: 0.02em;
}

.sidebar-header .subtitle {
  font-size: 0.78rem;
  color: var(--text-sidebar-heading);
  margin-top: 4px;
}

.sidebar-nav { padding: 12px 0; flex: 1; }

.nav-part {
  margin-bottom: 2px;
}

.nav-part-title {
  padding: 10px 20px;
  font-size: 0.72rem;
  font-weight: 600;
  text-transform: uppercase;
  letter-spacing: 0.08em;
  color: var(--text-sidebar-heading);
  cursor: pointer;
  display: flex;
  justify-content: space-between;
  align-items: center;
  user-select: none;
  transition: color 0.15s;
}
.nav-part-title:hover { color: #fff; }

.nav-part-title .toggle-icon {
  font-size: 0.6rem;
  transition: transform 0.2s;
}
.nav-part.collapsed .toggle-icon { transform: rotate(-90deg); }

.nav-chapters {
  list-style: none;
  overflow: hidden;
  transition: max-height 0.3s ease;
}
.nav-part.collapsed .nav-chapters { max-height: 0 !important; }

.nav-chapters li a {
  display: block;
  padding: 7px 20px 7px 32px;
  color: var(--text-sidebar);
  text-decoration: none;
  font-size: 0.85rem;
  transition: all 0.15s;
  border-left: 3px solid transparent;
}
.nav-chapters li a:hover {
  background: var(--bg-sidebar-hover);
  color: #fff;
}
.nav-chapters li a.active {
  background: var(--bg-sidebar-active);
  color: #fff;
  border-left-color: var(--accent-blue);
}

.nav-appendix .nav-part-title { color: #8fa8c8; }

.sidebar-footer {
  padding: 12px 20px;
  border-top: 1px solid var(--border-sidebar);
  font-size: 0.72rem;
  color: var(--text-sidebar-heading);
}

/* Main content area */
.main-content {
  margin-left: var(--sidebar-width);
  flex: 1;
  min-width: 0;
}

.breadcrumb {
  background: var(--bg-card);
  border-bottom: 1px solid var(--border-color);
  padding: 12px 32px;
  font-size: 0.85rem;
  color: var(--text-muted);
  position: sticky;
  top: 0;
  z-index: 50;
  box-shadow: var(--shadow);
}
.breadcrumb a { color: var(--accent-blue); text-decoration: none; }
.breadcrumb a:hover { text-decoration: underline; }
.breadcrumb .sep { margin: 0 8px; color: #b2bec3; }

article {
  max-width: var(--content-max);
  margin: 0 auto;
  padding: 32px 40px 60px;
}

article h1 {
  font-size: 2rem;
  font-weight: 800;
  color: var(--text-primary);
  margin-bottom: 8px;
  line-height: 1.3;
  border-bottom: 3px solid var(--accent-blue);
  padding-bottom: 12px;
}
article h1 .chapter-num {
  color: var(--accent-blue);
  font-size: 1.2rem;
  display: block;
  font-weight: 600;
  margin-bottom: 4px;
}

article h2 {
  font-size: 1.45rem;
  font-weight: 700;
  color: var(--text-primary);
  margin: 36px 0 16px;
  padding-bottom: 8px;
  border-bottom: 1px solid var(--border-color);
}
article h3 {
  font-size: 1.15rem;
  font-weight: 600;
  color: #2d3e50;
  margin: 28px 0 12px;
}
article h4 {
  font-size: 1rem;
  font-weight: 600;
  color: #34495e;
  margin: 20px 0 8px;
}

article p { margin-bottom: 14px; }
article ul, article ol { margin: 0 0 14px 24px; }
article li { margin-bottom: 6px; }

article a { color: var(--accent-blue); text-decoration: none; }
article a:hover { text-decoration: underline; }

dfn {
  font-style: normal;
  font-weight: 600;
  border-bottom: 1px dotted var(--accent-blue);
  cursor: help;
}

/* Code blocks */
.code-wrapper {
  position: relative;
  margin: 16px 0;
  border-radius: 8px;
  overflow: hidden;
  box-shadow: var(--shadow);
}

.code-src {
  position: absolute;
  top: 0;
  right: 0;
  background: rgba(255,255,255,0.1);
  color: #94a3b8;
  font-size: 0.7rem;
  padding: 4px 12px;
  font-family: "JetBrains Mono", "Fira Code", monospace;
  border-bottom-left-radius: 6px;
  z-index: 2;
}

.code-copy {
  position: absolute;
  top: 4px;
  right: 8px;
  background: rgba(255,255,255,0.12);
  border: none;
  color: #94a3b8;
  font-size: 0.72rem;
  padding: 3px 10px;
  border-radius: 4px;
  cursor: pointer;
  z-index: 3;
  display: none;
}
.code-wrapper:hover .code-copy { display: block; }
.code-copy:hover { background: rgba(255,255,255,0.25); color: #fff; }

pre {
  background: var(--bg-code);
  padding: 16px 20px;
  overflow-x: auto;
  border-radius: 8px;
}

pre code {
  font-family: "JetBrains Mono", "Fira Code", "Consolas", monospace;
  font-size: 0.85rem;
  line-height: 1.6;
  color: var(--text-code);
}

code.inline {
  background: #e8edf2;
  color: #c0392b;
  padding: 2px 6px;
  border-radius: 4px;
  font-family: "JetBrains Mono", "Fira Code", "Consolas", monospace;
  font-size: 0.88em;
}

/* Figures / images */
figure {
  margin: 20px 0;
  text-align: center;
}
figure img {
  max-width: 100%;
  height: auto;
  border-radius: 6px;
  box-shadow: var(--shadow-lg);
  cursor: zoom-in;
  border: 1px solid var(--border-color);
}
figcaption {
  font-size: 0.82rem;
  color: var(--text-muted);
  margin-top: 8px;
  font-style: italic;
}

/* Tables */
table {
  width: 100%;
  border-collapse: collapse;
  margin: 16px 0;
  font-size: 0.9rem;
  box-shadow: var(--shadow);
  border-radius: 8px;
  overflow: hidden;
}
th {
  background: var(--bg-sidebar);
  color: #fff;
  padding: 10px 14px;
  text-align: left;
  font-weight: 600;
  font-size: 0.85rem;
}
td {
  padding: 10px 14px;
  border-bottom: 1px solid var(--border-color);
  background: #fff;
}
tr:nth-child(even) td { background: #f8fafc; }

/* Callout boxes */
.note, .tip, .warn {
  padding: 14px 18px;
  border-radius: 8px;
  margin: 16px 0;
  font-size: 0.92rem;
  border-left: 4px solid;
}
.note { background: var(--bg-note); border-color: var(--accent-blue); }
.tip { background: var(--bg-tip); border-color: var(--accent-green); }
.warn { background: var(--bg-warn); border-color: var(--accent-orange); }
.note::before { content: "📌 注意："; font-weight: 700; }
.tip::before { content: "💡 提示："; font-weight: 700; }
.warn::before { content: "⚠️ 警告："; font-weight: 700; }

/* Source card */
.source-card {
  background: #f0f4f8;
  border: 1px solid var(--border-color);
  border-radius: 8px;
  padding: 16px 20px;
  margin-top: 48px;
  font-size: 0.85rem;
}
.source-card h4 {
  font-size: 0.8rem;
  text-transform: uppercase;
  letter-spacing: 0.06em;
  color: var(--text-muted);
  margin-bottom: 8px;
}
.source-card ul { margin-left: 16px; }
.source-card li { margin-bottom: 3px; color: var(--text-muted); }
.source-card code { font-size: 0.82rem; }

/* Lightbox */
.lightbox-overlay {
  display: none;
  position: fixed;
  top: 0; left: 0;
  width: 100%; height: 100%;
  background: rgba(0,0,0,0.88);
  z-index: 200;
  justify-content: center;
  align-items: center;
  cursor: zoom-out;
}
.lightbox-overlay.active { display: flex; }
.lightbox-overlay img {
  max-width: 95%;
  max-height: 95%;
  object-fit: contain;
  border-radius: 4px;
  box-shadow: 0 8px 40px rgba(0,0,0,0.5);
}

/* Homepage */
.home-hero {
  text-align: center;
  padding: 60px 40px 40px;
  background: linear-gradient(135deg, #1a2332 0%, #2d4a6f 100%);
  color: #fff;
  margin: -32px -40px 40px;
}
.home-hero h1 {
  font-size: 2.4rem;
  border: none;
  color: #fff;
  margin-bottom: 12px;
}
.home-hero p {
  font-size: 1.1rem;
  color: #a8c4e0;
  max-width: 640px;
  margin: 0 auto;
}

.roadmap {
  display: grid;
  grid-template-columns: repeat(auto-fit, minmax(280px, 1fr));
  gap: 20px;
  margin: 32px 0;
}
.roadmap-card {
  background: var(--bg-card);
  border-radius: 12px;
  padding: 24px;
  box-shadow: var(--shadow);
  border-top: 4px solid var(--accent-blue);
  transition: transform 0.2s, box-shadow 0.2s;
}
.roadmap-card:hover {
  transform: translateY(-3px);
  box-shadow: var(--shadow-lg);
}
.roadmap-card h3 {
  font-size: 1.05rem;
  margin: 0 0 8px;
  color: var(--text-primary);
}
.roadmap-card .part-num {
  font-size: 0.72rem;
  text-transform: uppercase;
  letter-spacing: 0.08em;
  color: var(--accent-blue);
  font-weight: 700;
}
.roadmap-card p {
  font-size: 0.88rem;
  color: var(--text-muted);
  margin-bottom: 12px;
}
.roadmap-card a {
  font-size: 0.85rem;
  font-weight: 600;
}

.chapter-list {
  list-style: none;
  margin: 0;
  padding: 0;
}
.chapter-list li {
  padding: 5px 0;
  font-size: 0.82rem;
}
.chapter-list li a {
  color: var(--text-muted);
}
.chapter-list li a:hover { color: var(--accent-blue); }

/* Responsive */
.menu-toggle {
  display: none;
  position: fixed;
  top: 12px;
  left: 12px;
  z-index: 150;
  background: var(--bg-sidebar);
  color: #fff;
  border: none;
  padding: 8px 12px;
  border-radius: 6px;
  font-size: 1.2rem;
  cursor: pointer;
}

@media (max-width: 768px) {
  .sidebar {
    transform: translateX(-100%);
    transition: transform 0.3s;
  }
  .sidebar.open { transform: translateX(0); }
  .main-content { margin-left: 0; }
  .menu-toggle { display: block; }
  article { padding: 24px 16px 40px; }
  .home-hero { padding: 40px 20px 30px; margin: -24px -16px 30px; }
  .home-hero h1 { font-size: 1.8rem; }
}

/* ===== Part7: Examples Deep-Dive Styles ===== */

/* Table of Contents */
.toc {
  background: var(--bg-card);
  border: 1px solid var(--border-color);
  border-radius: 12px;
  padding: 24px 28px;
  margin: 24px 0 32px;
  box-shadow: var(--shadow);
}
.toc h2 {
  margin: 0 0 16px;
  font-size: 1.2rem;
  color: var(--accent-green);
  border: none;
  padding: 0;
}
.toc-grid {
  display: grid;
  grid-template-columns: repeat(auto-fill, minmax(320px, 1fr));
  gap: 6px 24px;
  list-style: none;
  padding: 0;
  margin: 0;
}
.toc-grid li a {
  color: var(--text-primary);
  text-decoration: none;
  font-size: 0.92rem;
  padding: 4px 0;
  display: block;
  transition: color 0.2s;
}
.toc-grid li a:hover {
  color: var(--accent-blue);
}
.toc-grid li a .toc-num {
  color: var(--accent-orange);
  font-weight: 600;
  margin-right: 6px;
  font-family: 'JetBrains Mono', monospace;
  font-size: 0.85rem;
}

/* Example Section */
.example-section {
  border-top: 2px solid var(--border-color);
  padding-top: 32px;
  margin-top: 40px;
}
.example-section:first-of-type {
  border-top: none;
  margin-top: 0;
  padding-top: 0;
}
.example-section h2 {
  color: var(--accent-green);
  border-bottom-color: var(--accent-green);
}

/* Verification Flow Steps */
.flow-steps {
  margin: 20px 0;
}
.flow-step {
  background: var(--bg-card);
  border-left: 4px solid var(--accent-blue);
  border-radius: 0 8px 8px 0;
  padding: 16px 20px;
  margin: 12px 0;
  box-shadow: var(--shadow);
  color: var(--text-primary);
}
.flow-step.step-setup { border-left-color: #42a5f5; }
.flow-step.step-constraint { border-left-color: #ab47bc; }
.flow-step.step-engine { border-left-color: #ffa726; }
.flow-step.step-prove { border-left-color: var(--accent-green); }
.flow-step.step-result { border-left-color: #ef5350; }
.flow-step-title {
  font-weight: 600;
  font-size: 0.95rem;
  color: var(--text-primary);
  margin-bottom: 8px;
}
.flow-step-title .step-num {
  display: inline-flex;
  align-items: center;
  justify-content: center;
  min-width: 24px;
  height: 24px;
  background: var(--accent-blue);
  color: #fff;
  border-radius: 50%;
  font-size: 0.8rem;
  margin-right: 8px;
  padding: 0 4px;
  font-family: 'JetBrains Mono', monospace;
}
.flow-step.step-setup .step-num { background: #42a5f5; }
.flow-step.step-constraint .step-num { background: #ab47bc; }
.flow-step.step-engine .step-num { background: #ffa726; }
.flow-step.step-prove .step-num { background: var(--accent-green); }
.flow-step.step-result .step-num { background: #ef5350; }
.flow-step p { margin: 6px 0; font-size: 0.93rem; color: var(--text-primary); }
.flow-step ul { margin: 6px 0; padding-left: 20px; }
.flow-step li { font-size: 0.93rem; color: var(--text-primary); }

/* Verdict badges */
.verdict {
  display: inline-block;
  padding: 2px 10px;
  border-radius: 4px;
  font-size: 0.82rem;
  font-weight: 600;
  font-family: 'JetBrains Mono', monospace;
}
.verdict-green { background: rgba(0,200,83,0.12); color: #2e7d32; border: 1px solid rgba(0,200,83,0.3); }
.verdict-red { background: rgba(239,83,80,0.12); color: #c62828; border: 1px solid rgba(239,83,80,0.3); }
.verdict-yellow { background: rgba(255,145,0,0.12); color: #e65100; border: 1px solid rgba(255,145,0,0.3); }

/* Run command box */
.run-cmd {
  background: var(--bg-code);
  border: 1px solid #2a3a4a;
  border-radius: 8px;
  padding: 12px 16px;
  margin: 12px 0;
  font-family: 'JetBrains Mono', monospace;
  font-size: 0.88rem;
  color: #80cbc4;
  overflow-x: auto;
}
.run-cmd::before {
  content: "▶ 运行命令";
  display: block;
  font-family: -apple-system, BlinkMacSystemFont, sans-serif;
  color: var(--accent-orange);
  font-weight: 600;
  font-size: 0.8rem;
  margin-bottom: 6px;
}

/* Design structure info box */
.design-info {
  background: rgba(66,165,245,0.06);
  border: 1px solid rgba(66,165,245,0.25);
  border-radius: 8px;
  padding: 14px 18px;
  margin: 14px 0;
  color: var(--text-primary);
}
.design-info h4 {
  margin: 0 0 8px;
  color: #1565c0;
  font-size: 0.9rem;
}
.design-info ul { margin: 4px 0; padding-left: 18px; }
.design-info li { font-size: 0.9rem; margin: 3px 0; color: var(--text-primary); }

@media (max-width: 768px) {
  .toc-grid { grid-template-columns: 1fr; }
  .flow-step { padding: 12px 14px; }
}

/* ===== Floating Feedback Button ===== */
.feedback-btn {
  position: fixed;
  bottom: 24px;
  right: 24px;
  z-index: 200;
  background: var(--accent-green);
  color: #fff;
  border: none;
  border-radius: 50px;
  padding: 10px 20px;
  font-size: 0.88rem;
  font-weight: 600;
  font-family: -apple-system, BlinkMacSystemFont, sans-serif;
  cursor: pointer;
  box-shadow: 0 2px 12px rgba(0,200,83,0.3);
  display: flex;
  align-items: center;
  gap: 6px;
  transition: all 0.2s ease;
  text-decoration: none;
}
.feedback-btn:hover {
  background: #00b848;
  box-shadow: 0 4px 20px rgba(0,200,83,0.4);
  transform: translateY(-1px);
  color: #fff;
  text-decoration: none;
}
.feedback-btn svg {
  width: 16px;
  height: 16px;
}

/* Feedback modal */
.feedback-overlay {
  display: none;
  position: fixed;
  top: 0; left: 0; right: 0; bottom: 0;
  background: rgba(0,0,0,0.5);
  z-index: 300;
  justify-content: center;
  align-items: center;
}
.feedback-overlay.active {
  display: flex;
}
.feedback-modal {
  background: var(--bg-card);
  border-radius: 12px;
  padding: 28px 32px;
  max-width: 480px;
  width: 90%;
  box-shadow: 0 8px 40px rgba(0,0,0,0.2);
}
.feedback-modal h3 {
  margin: 0 0 8px;
  font-size: 1.15rem;
  color: var(--text-primary);
}
.feedback-modal p {
  margin: 0 0 16px;
  font-size: 0.9rem;
  color: var(--text-muted);
  line-height: 1.6;
}
.feedback-options {
  display: grid;
  grid-template-columns: 1fr 1fr;
  gap: 10px;
  margin-bottom: 16px;
}
.feedback-opt {
  display: flex;
  align-items: center;
  gap: 8px;
  padding: 12px 14px;
  border: 2px solid var(--border-color);
  border-radius: 8px;
  cursor: pointer;
  font-size: 0.88rem;
  color: var(--text-primary);
  transition: all 0.15s;
  background: #fff;
}
.feedback-opt:hover {
  border-color: var(--accent-blue);
  background: rgba(68,138,255,0.04);
}
.feedback-opt input { margin: 0; }
.feedback-text {
  width: 100%;
  min-height: 80px;
  border: 1px solid var(--border-color);
  border-radius: 8px;
  padding: 10px 12px;
  font-size: 0.88rem;
  font-family: inherit;
  resize: vertical;
  margin-bottom: 12px;
  box-sizing: border-box;
}
.feedback-text:focus {
  outline: none;
  border-color: var(--accent-blue);
}
.feedback-actions {
  display: flex;
  justify-content: flex-end;
  gap: 8px;
}
.feedback-submit {
  background: var(--accent-green);
  color: #fff;
  border: none;
  border-radius: 6px;
  padding: 8px 20px;
  font-size: 0.88rem;
  font-weight: 600;
  cursor: pointer;
}
.feedback-submit:hover { background: #00b848; }
.feedback-cancel {
  background: transparent;
  color: var(--text-muted);
  border: 1px solid var(--border-color);
  border-radius: 6px;
  padding: 8px 16px;
  font-size: 0.88rem;
  cursor: pointer;
}
.feedback-cancel:hover { background: #f0f4f8; }