/* The Property Prover — illustrative demo widget. Mirrors our RE-FORM / formal-verification report
   design language (signal lanes + phase bands + verdict markers). Uses site tokens. */
.prover{max-width:var(--max-w-narrow);margin:0 auto}
.prover-tabs{display:flex;flex-wrap:wrap;gap:8px;margin:0 0 22px}
.prover-tab{font:600 13px/1.2 'Inter',sans-serif;color:var(--muted);background:var(--card);border:1px solid var(--card-bd);border-radius:999px;padding:9px 16px;cursor:pointer;transition:all .2s var(--t)}
.prover-tab[aria-selected="true"]{color:var(--bg);background:var(--brand-2);border-color:var(--brand-2)}
.prover-tab:hover{color:var(--text-strong)}
.prover-card{border:1px solid var(--card-bd);border-radius:16px;background:var(--card);overflow:hidden}
/* toolbar with breadcrumb + verdict pill */
.prover-bar{display:flex;align-items:center;gap:12px;padding:12px 22px;border-bottom:1px solid var(--card-bd);background:rgba(0,0,0,.18)}
.bar-crumb{font-family:ui-monospace,'SF Mono',Menlo,Consolas,monospace;font-size:11.5px;color:var(--dim);letter-spacing:.02em}
.verdict-pill{margin-left:auto;font:700 11.5px/1 'Inter',sans-serif;letter-spacing:.07em;padding:7px 15px;border-radius:999px;border:1px solid var(--card-bd);color:var(--muted);background:var(--bg-2);text-transform:uppercase}
.verdict-pill.pending{color:var(--dim)}
.verdict-pill.running{color:#4dffff;border-color:rgba(77,255,255,.4);background:rgba(77,255,255,.08)}
.verdict-pill.pass{color:#2ee08a;border-color:rgba(46,224,138,.5);background:rgba(46,224,138,.12)}
.verdict-pill.fail{color:#ff6a6a;border-color:rgba(255,90,90,.5);background:rgba(255,90,90,.12)}
/* requirement */
.prover-req{padding:20px 22px;border-bottom:1px solid var(--card-bd)}
.prover-req .req-nl{font-size:16.5px;color:var(--text-strong);margin:0 0 10px;line-height:1.5}
.prover-req .req-type{display:inline-block;font:600 10.5px/1 'Inter',sans-serif;letter-spacing:.08em;text-transform:uppercase;color:var(--brand-2);border:1px solid var(--card-bd);border-radius:6px;padding:5px 9px;margin-right:10px}
.prover-req .req-formal{font-family:ui-monospace,'SF Mono',Menlo,Consolas,monospace;font-size:13px;color:var(--muted);margin-top:12px}
/* pipeline */
.prover-pipe{display:flex;align-items:center;gap:10px;flex-wrap:wrap;padding:16px 22px;border-bottom:1px solid var(--card-bd);font:600 11px/1.2 'Inter',sans-serif;color:var(--dim);text-transform:uppercase;letter-spacing:.07em}
.prover-pipe .pstep{padding:6px 11px;border:1px solid var(--card-bd);border-radius:7px;white-space:nowrap}
.prover-pipe .pstep.on{color:var(--brand-2);border-color:var(--brand-2)}
.prover-pipe .parrow{color:var(--dim)}
/* legend (phase swatches) */
.prover-legend{display:flex;flex-wrap:wrap;gap:16px;padding:13px 22px;border-bottom:1px solid var(--card-bd);font:600 11px/1 'Inter',sans-serif;color:var(--muted)}
.prover-legend .lg-item{display:inline-flex;align-items:center;gap:7px}
.prover-legend .lg-sw{width:22px;height:11px;border-radius:2px;display:inline-block}
.lg-sw.lg-trig{background:rgba(46,204,113,.45)}
.lg-sw.lg-delay{background:rgba(241,196,15,.45)}
.lg-sw.lg-act{background:rgba(231,76,60,.4)}
.lg-sw.lg-dl{width:0;height:14px;border-left:2px dashed var(--dim);border-radius:0}
.lg-sw.lg-vio{width:0;height:14px;border-left:2px dotted #ff5a5a;border-radius:0}
/* trace lanes */
.prover-trace{padding:20px 22px}
.trace-lanes{position:relative}
.trace-row{display:grid;grid-template-columns:150px 1fr;gap:14px;align-items:center;margin-bottom:8px;position:relative;z-index:1}
.trace-name{font-family:ui-monospace,'SF Mono',Menlo,Consolas,monospace;font-size:12px;color:var(--muted);text-align:right;white-space:nowrap;overflow:hidden;text-overflow:ellipsis}
.trace-cells{display:grid;grid-auto-flow:column;grid-auto-columns:1fr;gap:3px;height:30px}
.cell{border-radius:3px;background:var(--bg-2);position:relative;transition:background .15s}
.cell.hi{background:rgba(89,143,255,.5)}
.cell.sig-evidence.hi{background:var(--brand-glow)}
.cell.playhead{outline:2px solid var(--brand-2);outline-offset:1px;z-index:2}
.cell.failcol{background:rgba(255,90,90,.85)!important}
/* verdict row */
.trace-row.verdict .trace-cells .cell.ok{background:rgba(62,178,86,.7)}
.trace-row.verdict .trace-cells .cell.wait{background:rgba(77,255,255,.45)}
.trace-row.verdict .trace-cells .cell.fail{background:rgba(255,90,90,.85)}
/* phase-band + vline overlay (translucent, above lanes, aligned to the plot column) */
.trace-overlay{position:absolute;inset:0;display:grid;grid-template-columns:150px 1fr;column-gap:14px;pointer-events:none;z-index:3}
.ov-spacer{}
.ov-plot{position:relative}
.band{position:absolute;top:0;bottom:0}
.band.b-trig{background:rgba(46,204,113,.16)}
.band.b-delay{background:rgba(241,196,15,.15)}
.band.b-act{background:rgba(231,76,60,.16)}
.vline{position:absolute;top:0;bottom:0;width:0}
.vline.v-dl{border-left:2px dashed var(--dim)}
.vline.v-vio{border-left:2px dotted #ff5a5a;box-shadow:0 0 6px rgba(255,90,90,.4)}
/* observer state */
.prover-state{display:flex;align-items:center;gap:14px;padding:16px 22px;border-top:1px solid var(--card-bd);flex-wrap:wrap}
.state-badge{font:700 13px/1 'Inter',sans-serif;letter-spacing:.04em;padding:9px 16px;border-radius:8px;text-transform:uppercase;white-space:nowrap}
.state-badge.ok{color:#3eb256;background:rgba(62,178,86,.12);border:1px solid rgba(62,178,86,.4)}
.state-badge.wait{color:#4dffff;background:rgba(77,255,255,.1);border:1px solid rgba(77,255,255,.35)}
.state-badge.fail{color:#ff6a6a;background:rgba(255,90,90,.12);border:1px solid rgba(255,90,90,.45)}
.state-expl{font-size:13.5px;color:var(--muted);line-height:1.5;flex:1;min-width:240px}
/* controls */
.prover-ctrl{display:flex;align-items:center;gap:12px;flex-wrap:wrap;padding:16px 22px;border-top:1px solid var(--card-bd)}
.prover-ctrl button{font:600 13px/1 'Inter',sans-serif;border-radius:8px;padding:11px 18px;cursor:pointer;border:1px solid var(--card-bd);background:var(--card);color:var(--text-strong);transition:all .2s var(--t)}
.prover-ctrl .btn-verify{background:var(--brand-2);border-color:var(--brand-2);color:var(--bg)}
.prover-ctrl .btn-verify:hover{filter:brightness(1.08)}
.prover-ctrl button:disabled{opacity:.45;cursor:default}
.prover-toggle{display:inline-flex;align-items:center;gap:8px;margin-left:auto;font:600 12px/1 'Inter',sans-serif;color:var(--muted)}
.prover-toggle .seg{display:inline-flex;border:1px solid var(--card-bd);border-radius:8px;overflow:hidden}
.prover-toggle .seg button{border:none;border-radius:0;padding:8px 13px;background:transparent;color:var(--muted)}
.prover-toggle .seg button.on{background:var(--card-bd);color:var(--text-strong)}
.prover-note{font-size:12px;color:var(--dim);padding:14px 22px;border-top:1px solid var(--card-bd);background:rgba(0,0,0,.15);line-height:1.5}
@media(max-width:560px){
  .trace-row{grid-template-columns:1fr;gap:4px}
  .trace-name{text-align:left}
  .trace-overlay{display:none} /* phase bands rely on the 2-column grid; hide on stacked layout */
}
@media (prefers-reduced-motion:reduce){.cell{transition:none}}