:root{--pg-bg: #f6f8fa;--pg-surface: #ffffff;--pg-surface-muted: #fafafc;--pg-canvas: #f2f7fd;--pg-border: #d6dce0;--pg-border-soft: #eaeef2;--pg-text: #24292f;--pg-text-muted: #6b7280;--pg-text-faint: #9ca3af;--pg-brand: #3fbb14;--pg-brand-strong: #2f9410;--pg-brand-soft: #ecfae8;--pg-accent: #1e73da;--pg-accent-hover: #185fb5;--pg-accent-soft: #e8f1fc;--pg-accent-soft-border: #c6ddf7;--pg-accent-ring: rgba(30, 115, 218, .18);--pg-status-verified: #3fbb14;--pg-status-transitively-verified: #217a0b;--pg-status-trusted: #9333ea;--pg-status-failed: #bb1416;--pg-status-unverified: #9ca3af;--pg-status-unknown: #217ef0;--pg-edge-precondition: #e65100;--pg-edge-postcondition: #c2185b;--pg-edge-mapping: #7c3aed;--pg-edge-spec: #0891b2;--pg-selection: #ff6b6b;--pg-font-sans: "Inter", ui-sans-serif, system-ui, -apple-system, "Segoe UI", Roboto, sans-serif;--pg-font-mono: ui-monospace, SFMono-Regular, Menlo, Monaco, Consolas, "Liberation Mono", "Courier New", monospace;--pg-radius-sm: 4px;--pg-radius-md: 6px;--pg-radius-lg: 8px}*{margin:0;padding:0;box-sizing:border-box}body{font-family:var(--pg-font-sans);background:var(--pg-bg);color:var(--pg-text);overflow:hidden;accent-color:var(--pg-brand-strong)}.app-container{display:flex;flex-direction:column;height:100vh}.header{background:var(--pg-surface);color:var(--pg-text);border-bottom:1px solid var(--pg-border);padding:1rem 2rem;display:flex;justify-content:space-between;align-items:center}.header h1{display:flex;align-items:center;gap:.5rem;font-size:1.25rem;font-weight:600;color:var(--pg-brand-strong)}.header .logo{flex-shrink:0}.view-switcher{display:flex;gap:0;border-radius:var(--pg-radius-md);overflow:hidden;border:1px solid var(--pg-border)}.view-btn{background:transparent;color:var(--pg-text-muted);border:none;padding:.4rem 1rem;font-size:.85rem;font-weight:500;font-family:inherit;cursor:pointer;transition:all .2s}.view-btn.active{background:var(--pg-brand);color:#fff}.view-btn:hover:not(.active){background:var(--pg-brand-soft);color:var(--pg-text)}.file-input-container{position:relative}.file-input-label{background:var(--pg-accent);color:#fff;padding:.5rem 1.5rem;border-radius:var(--pg-radius-md);cursor:pointer;font-weight:500;transition:background .2s;display:inline-block}.file-input-label:hover{background:var(--pg-accent-hover)}#file-input{display:none}.main-content{display:flex;flex:1;overflow:hidden}.sidebar{width:320px;background:var(--pg-surface);overflow-y:auto;z-index:10}.sidebar-left{border-right:1px solid var(--pg-border)}.sidebar-right{border-left:1px solid var(--pg-border)}.panel{padding:1.5rem;border-bottom:1px solid var(--pg-border-soft)}.panel h2{font-size:1rem;margin-bottom:1rem;color:var(--pg-text);font-weight:600}.panel h3{font-size:.9rem;margin-bottom:.5rem;color:var(--pg-text-muted);font-weight:600}.filter-group{margin-bottom:1.5rem}.checkbox-label{display:flex;align-items:center;margin-bottom:.5rem;cursor:pointer;font-size:.9rem}.checkbox-label input{margin-right:.5rem;cursor:pointer}.checkbox-label .legend-dot{width:10px;height:10px;border:none;box-shadow:none;margin-right:.35rem}.libsignal-badge,.other-badge,.inner-badge,.precondition-badge,.postcondition-badge,.mapping-badge,.spec-link-badge,.lang-badge-rust,.lang-badge-lean,.exec-badge,.proof-badge,.spec-badge{padding:.15rem .6rem;border-radius:var(--pg-radius-md);font-size:.8rem;font-weight:500;background:color-mix(in srgb,currentColor 6%,white);border:1px solid color-mix(in srgb,currentColor 35%,white)}.libsignal-badge{color:var(--pg-accent)}.other-badge{color:#217a0b}.inner-badge{color:#3949ab}.precondition-badge{color:var(--pg-edge-precondition)}.postcondition-badge{color:var(--pg-edge-postcondition)}.mapping-badge{color:var(--pg-edge-mapping)}.spec-link-badge{color:var(--pg-edge-spec)}.lang-badge-rust{color:#92400e}.lang-badge-lean{color:#1e40af}.exec-badge{color:var(--pg-accent)}.proof-badge{color:#7b1fa2}.spec-badge{color:#f57c00}.preset-row{margin-bottom:.5rem}.preset-select{width:100%;padding:.4rem .5rem;border:1px solid var(--pg-border);border-radius:var(--pg-radius-sm);font-size:.85rem;font-family:inherit;background:var(--pg-surface-muted);cursor:pointer}.preset-select:hover{border-color:var(--pg-text-faint)}.preset-select:focus{outline:none;border-color:var(--pg-accent)}.input-label{display:block;margin-bottom:.75rem}.input-label span{display:block;font-size:.85rem;color:var(--pg-text-muted);margin-bottom:.25rem}.search-input{width:100%;padding:.5rem;border:1px solid var(--pg-border);border-radius:var(--pg-radius-sm);font-size:.9rem;font-family:inherit;transition:border-color .2s}.search-input:focus{outline:none;border-color:var(--pg-accent);box-shadow:0 0 0 2px var(--pg-accent-ring)}select.search-input{appearance:auto;cursor:pointer;background:var(--pg-surface)}.slider-label{display:block;margin-bottom:.75rem}.slider-label span{display:block;margin-bottom:.25rem;font-size:.9rem}.slider-label small{display:block;color:var(--pg-text-muted);font-size:.75rem;margin-top:.25rem}.slider{width:100%;height:6px;border-radius:3px;background:var(--pg-border);outline:none;-webkit-appearance:none}.slider::-webkit-slider-thumb{-webkit-appearance:none;appearance:none;width:18px;height:18px;border-radius:50%;background:var(--pg-accent);cursor:pointer}.slider::-moz-range-thumb{width:18px;height:18px;border-radius:50%;background:var(--pg-accent);cursor:pointer}.button-group{display:flex;flex-direction:column;gap:.5rem}.btn{padding:.6rem 1rem;border:1px solid transparent;border-radius:var(--pg-radius-md);font-size:.9rem;font-weight:500;font-family:inherit;cursor:pointer;transition:all .2s}.btn-secondary{background:var(--pg-surface-muted);color:var(--pg-text);border-color:var(--pg-border)}.btn-secondary:hover{background:var(--pg-border-soft)}.btn-primary{background:var(--pg-accent);color:#fff}.btn-primary:hover{background:var(--pg-accent-hover)}.stats-container{font-size:.9rem}.stat-item{display:flex;justify-content:space-between;align-items:center;padding:.5rem 0;border-bottom:1px solid var(--pg-border-soft)}.stat-item:last-child{border-bottom:none}.stat-label{font-weight:500;color:var(--pg-text-muted)}.stat-value{font-weight:600;color:var(--pg-text)}.stat-detail{font-size:.8rem;color:var(--pg-text-faint);margin-left:.25rem}.legend-container{display:flex;flex-direction:column;gap:.5rem}.legend-item{display:flex;align-items:center;gap:.5rem;font-size:.9rem}.legend-dot{width:14px;height:14px;border-radius:50%;border:2px solid white;box-shadow:0 1px 3px #0003;flex-shrink:0}.status-verified{background:var(--pg-status-verified)}.status-transitively-verified{background:var(--pg-status-transitively-verified)}.status-trusted{background:var(--pg-status-trusted)}.status-failed{background:var(--pg-status-failed)}.status-unverified{background:var(--pg-status-unverified)}.status-unknown{background:var(--pg-status-unknown)}.file-list-details{margin-top:.5rem}.file-list-details summary{cursor:pointer;padding:.5rem;background:var(--pg-surface-muted);border-radius:var(--pg-radius-sm);font-size:.85rem;color:var(--pg-text-muted)}.file-list-details summary:hover{background:var(--pg-border-soft)}.file-list-details[open] summary{border-radius:var(--pg-radius-sm) var(--pg-radius-sm) 0 0}.file-list{max-height:200px;overflow-y:auto;border:1px solid var(--pg-border);border-top:none;border-radius:0 0 var(--pg-radius-sm) var(--pg-radius-sm);background:var(--pg-surface)}.file-list-item{padding:.35rem .5rem;font-size:.8rem;cursor:pointer;display:flex;align-items:center;gap:.5rem;border-bottom:1px solid var(--pg-border-soft)}.file-list-item:last-child{border-bottom:none}.file-list-item:hover{background:var(--pg-accent-soft)}.file-list-item.selected{background:var(--pg-accent-soft);font-weight:500}.file-list-item .file-icon{color:var(--pg-text-muted);font-size:.75rem}.file-list-item .file-name{flex:1;overflow:hidden;text-overflow:ellipsis;white-space:nowrap}.file-list-item .file-count{font-size:.7rem;color:var(--pg-text-faint);background:var(--pg-border-soft);padding:.1rem .4rem;border-radius:10px;flex-shrink:0}.file-list-item .file-disambig{font-size:.7rem;color:var(--pg-text-muted);margin-left:.25rem;margin-right:auto;overflow:hidden;text-overflow:ellipsis;white-space:nowrap;max-width:120px}.file-list-item.has-duplicates .file-name{flex:0 0 auto;max-width:100px}.file-list-item.has-duplicates:hover{background:#fff3e0}.file-list-item.has-duplicates.selected{background:#ffe0b2}.input-with-dropdown{position:relative}.disambiguation-dropdown{position:absolute;top:100%;left:0;right:0;background:var(--pg-surface);border:1px solid var(--pg-border);border-radius:var(--pg-radius-md);box-shadow:0 4px 12px #00000026;z-index:1000;max-height:250px;overflow-y:auto;margin-top:4px}.disambiguation-dropdown .dropdown-header{padding:8px 12px;background:var(--pg-surface-muted);border-bottom:1px solid var(--pg-border);font-size:.8rem;color:var(--pg-text-muted);font-weight:500}.disambiguation-dropdown .dropdown-item{padding:8px 12px;cursor:pointer;display:flex;align-items:center;gap:8px;font-size:.85rem;border-bottom:1px solid var(--pg-border-soft)}.disambiguation-dropdown .dropdown-item:last-child{border-bottom:none}.disambiguation-dropdown .dropdown-item:hover,.disambiguation-dropdown .dropdown-item.selected{background:var(--pg-accent-soft)}.disambiguation-dropdown .dropdown-item .file-path{color:var(--pg-text-muted);font-size:.75rem;margin-left:auto;overflow:hidden;text-overflow:ellipsis;white-space:nowrap;max-width:200px}.disambiguation-dropdown .dropdown-item .checkbox{width:16px;height:16px;flex-shrink:0}.disambiguation-dropdown .dropdown-actions{padding:8px 12px;border-top:1px solid var(--pg-border);display:flex;gap:8px;background:var(--pg-surface-muted)}.disambiguation-dropdown .dropdown-actions button{flex:1;padding:6px 12px;border:none;border-radius:var(--pg-radius-sm);cursor:pointer;font-size:.8rem;font-family:inherit}.disambiguation-dropdown .dropdown-actions .btn-apply{background:var(--pg-accent);color:#fff}.disambiguation-dropdown .dropdown-actions .btn-apply:hover{background:var(--pg-accent-hover)}.disambiguation-dropdown .dropdown-actions .btn-cancel{background:var(--pg-border-soft);color:var(--pg-text)}.disambiguation-dropdown .dropdown-actions .btn-cancel:hover{background:var(--pg-border)}.disambiguation-dropdown .dropdown-actions .btn-all{background:var(--pg-status-verified);color:#fff}.disambiguation-dropdown .dropdown-actions .btn-all:hover{background:var(--pg-status-transitively-verified)}.graph-section{flex:1;display:flex;flex-direction:column;position:relative;background:var(--pg-canvas)}.query-label{background:var(--pg-bg);border-bottom:1px solid var(--pg-border);padding:.35rem 1rem;font-size:.8rem;color:var(--pg-text-muted);font-family:var(--pg-font-mono);white-space:nowrap;overflow:hidden;text-overflow:ellipsis}.query-label .query-type{color:var(--pg-edge-mapping);font-weight:600}.query-label .query-param{color:var(--pg-accent)}.query-label .query-dim{color:var(--pg-text-faint)}.graph-container{flex:1;position:relative;overflow:hidden}.graph-instructions{background:var(--pg-surface-muted);padding:1rem 1.5rem;border-top:1px solid var(--pg-border-soft);font-size:.85rem}.graph-instructions ul{list-style:none;display:flex;gap:1.5rem;flex-wrap:wrap}.graph-instructions li{color:var(--pg-text-muted)}.node-info{font-size:.9rem}.node-detail{margin-bottom:1rem}.node-detail h3{font-size:1.1rem;margin-bottom:.5rem;color:var(--pg-text)}.node-detail strong{color:var(--pg-text-muted);display:block;margin-bottom:.25rem}.code-block{display:block;background:var(--pg-surface-muted);border:1px solid var(--pg-border-soft);padding:.5rem;border-radius:var(--pg-radius-sm);font-family:var(--pg-font-mono);font-size:.8rem;overflow-x:auto;margin-top:.25rem;white-space:pre-wrap;word-break:break-all}.github-link{display:inline-flex;align-items:center;gap:.25rem;padding:.5rem .75rem;background:#24292f;color:#fff;text-decoration:none;border-radius:var(--pg-radius-md);font-size:.85rem;font-weight:500;transition:background .2s ease}.github-link:hover{background:#3a3f44}.node-list{list-style:none;max-height:200px;overflow-y:auto;background:var(--pg-surface-muted);padding:.5rem;border-radius:var(--pg-radius-sm);margin-top:.25rem}.node-list li{padding:.25rem 0;border-bottom:1px solid var(--pg-border-soft)}.node-list li:last-child{border-bottom:none}.node-badge{display:inline-block;padding:.15rem .6rem;border-radius:var(--pg-radius-md);font-size:.75rem;font-weight:600;margin-bottom:.5rem;background:color-mix(in srgb,currentColor 6%,white);border:1px solid color-mix(in srgb,currentColor 35%,white)}.badge-libsignal{color:var(--pg-accent)}.badge-other{color:#217a0b}.badge-verified{color:var(--pg-status-transitively-verified)}.badge-trusted{color:var(--pg-status-trusted)}.badge-failed{color:var(--pg-status-failed)}.badge-unverified{color:var(--pg-text-muted)}.badge-unknown{color:var(--pg-accent)}.similar-lemmas-list{list-style:none;padding:0;margin:.5rem 0 0}.similar-lemma-item{padding:.5rem;margin-bottom:.5rem;background:var(--pg-surface-muted);border-radius:var(--pg-radius-md);border-left:3px solid var(--pg-accent)}.similar-lemma-name{font-weight:600;color:var(--pg-text);font-size:.9rem;display:block}.similar-lemma-score{display:inline-block;background:var(--pg-accent);color:#fff;font-size:.7rem;padding:.1rem .4rem;border-radius:10px;margin-top:.25rem;font-weight:600}.similar-lemma-meta{font-size:.75rem;color:var(--pg-text-muted);margin-top:.25rem;font-family:var(--pg-font-mono)}.hidden-nodes-list{list-style:none;max-height:150px;overflow-y:auto;background:#fff3e0;padding:.5rem;border-radius:var(--pg-radius-sm);margin:.5rem 0;border:1px solid #ffcc80}.hidden-node-item{padding:.3rem .5rem;margin-bottom:.25rem;background:var(--pg-surface);border-radius:3px;font-size:.85rem;color:var(--pg-edge-precondition);border-left:3px solid #ff9800;transition:all .2s}.hidden-node-item:hover{background:#ffe0b2}.hidden-node-item:last-child{margin-bottom:0}.placeholder{color:var(--pg-text-faint);font-style:italic;text-align:center;padding:2rem 1rem}.footer{background:var(--pg-surface-muted);border-top:1px solid var(--pg-border);padding:.75rem 2rem;text-align:center;font-size:.85rem;color:var(--pg-text-muted)}.footer a{color:var(--pg-brand-strong);text-decoration:none}.footer a:hover{text-decoration:underline}.link{fill:none}.node{transition:all .2s}.node:hover{filter:brightness(1.2)}.label{pointer-events:none;-webkit-user-select:none;user-select:none}.sidebar::-webkit-scrollbar,.node-list::-webkit-scrollbar{width:6px}.sidebar::-webkit-scrollbar-track,.node-list::-webkit-scrollbar-track{background:var(--pg-border-soft)}.sidebar::-webkit-scrollbar-thumb,.node-list::-webkit-scrollbar-thumb{background:var(--pg-text-faint);border-radius:3px}.sidebar::-webkit-scrollbar-thumb:hover,.node-list::-webkit-scrollbar-thumb:hover{background:var(--pg-text-muted)}.bp-legend{position:absolute;top:10px;right:10px;background:#fffffff2;border:1px solid var(--pg-border);border-radius:var(--pg-radius-lg);padding:0;font-size:.78rem;box-shadow:0 2px 8px #0000001f;z-index:10;max-width:220px;-webkit-user-select:none;user-select:none}.bp-legend-header{display:flex;justify-content:space-between;align-items:center;padding:6px 10px;cursor:pointer;border-bottom:1px solid var(--pg-border-soft);border-radius:var(--pg-radius-lg) var(--pg-radius-lg) 0 0;background:var(--pg-surface-muted)}.bp-legend-header:hover{background:var(--pg-border-soft)}.bp-legend-body{padding:6px 10px 8px}.bp-legend-section{margin-top:6px;margin-bottom:2px;color:var(--pg-text-muted);font-size:.72rem;text-transform:uppercase;letter-spacing:.03em}.bp-legend-section:first-child{margin-top:0}.bp-legend-item{display:flex;align-items:center;gap:6px;padding:1px 0;color:var(--pg-text)}.bp-legend-item svg{flex-shrink:0}.bp-swatch{display:inline-block;width:14px;height:14px;border-radius:3px;flex-shrink:0}.bp-legend-arrow{font-size:.65rem;color:var(--pg-text-muted)}.bp-file-group{pointer-events:none}.bp-file-label{font-size:9px;font-family:var(--pg-font-sans);fill:#00000073;font-weight:600;pointer-events:none}.cm-legend,.hm-legend{position:absolute;top:10px;right:10px;background:#fffffff2;border:1px solid var(--pg-border);border-radius:var(--pg-radius-lg);font-size:.78rem;box-shadow:0 2px 8px #00000014;z-index:10;max-width:220px;-webkit-user-select:none;user-select:none}.cm-legend-header,.hm-legend-header{display:flex;justify-content:space-between;align-items:center;padding:6px 10px;cursor:pointer;border-bottom:1px solid var(--pg-border-soft);border-radius:var(--pg-radius-lg) var(--pg-radius-lg) 0 0;background:var(--pg-surface-muted)}.cm-legend-header:hover,.hm-legend-header:hover{background:var(--pg-border-soft)}.cm-legend-body,.hm-legend-body{padding:6px 10px 8px}.cm-legend-section,.hm-legend-section{margin-top:6px;margin-bottom:2px;color:var(--pg-text-muted);font-size:.72rem;text-transform:uppercase;letter-spacing:.03em}.cm-legend-item,.hm-legend-item{display:flex;align-items:center;gap:6px;padding:1px 0;color:var(--pg-text)}.cm-legend-item svg,.hm-legend-item svg{flex-shrink:0}.cm-legend-arrow,.hm-legend-arrow{font-size:.65rem;color:var(--pg-text-muted)}.cm-crate-group:hover .cm-crate-box{filter:brightness(.96)}.cm-edge{transition:stroke-opacity .15s}.cm-info{font-size:.85rem;line-height:1.5}.cm-info h3{font-size:1rem;margin-bottom:.3rem;color:var(--pg-text)}.cm-info h4{font-size:.82rem;margin-top:.6rem;margin-bottom:.15rem;color:var(--pg-text-muted)}.cm-info ul{list-style:none;padding-left:0;margin:0}.cm-info ul li{padding:1px 0;font-size:.8rem;color:var(--pg-text)}.cm-info ul li:before{content:"•";color:var(--pg-text-faint);margin-right:.4em}.cm-hint{margin-top:.6rem;font-size:.75rem;color:var(--pg-text-faint)}.right-sidebar-tabs{display:flex;border-bottom:2px solid var(--pg-border-soft);margin-bottom:.5rem}.sidebar-tab{flex:1;padding:.5rem .75rem;background:none;border:none;border-bottom:2px solid transparent;margin-bottom:-2px;cursor:pointer;font-size:.85rem;font-weight:500;font-family:inherit;color:var(--pg-text-muted);transition:color .15s,border-color .15s}.sidebar-tab:hover{color:var(--pg-text)}.sidebar-tab.active{color:var(--pg-brand-strong);border-bottom-color:var(--pg-brand)}.guide-onboarding{padding:.5rem;font-size:.85rem;line-height:1.5}.guide-onboarding-title{font-weight:600;font-size:.9rem;margin:0 0 .5rem;color:var(--pg-text)}.guide-suggested-queries{display:flex;flex-direction:column;gap:.35rem;margin-top:.75rem}.guide-chip{display:inline-block;padding:.35rem .65rem;background:var(--pg-accent-soft);border:1px solid var(--pg-accent-soft-border);border-radius:var(--pg-radius-lg);font-size:.8rem;font-family:inherit;cursor:pointer;transition:background .15s,border-color .15s;text-align:left;color:var(--pg-accent)}.guide-chip:hover{background:var(--pg-accent-soft-border);border-color:var(--pg-accent)}.guide-chip .chip-label{font-weight:500}.guide-chip .chip-desc{display:block;font-size:.72rem;color:var(--pg-text-muted);margin-top:.1rem}.toast-container{position:fixed;top:60px;left:50%;transform:translate(-50%);z-index:999;display:flex;flex-direction:column;gap:.4rem;pointer-events:none}.toast{background:#1f2937;color:#fff;padding:.5rem 1rem;border-radius:var(--pg-radius-lg);font-size:.8rem;box-shadow:0 4px 12px #00000026;animation:toast-in .25s ease-out,toast-out .3s ease-in 2.5s forwards;pointer-events:auto}@keyframes toast-in{0%{opacity:0;transform:translateY(-10px)}to{opacity:1;transform:translateY(0)}}@keyframes toast-out{0%{opacity:1}to{opacity:0}}