/* ===========================
   Verifier Results

   Rendered by vp-engine.js, in the Workbench's results pane and under the
   runnable models in the documentation: the results code, declared
   assumptions and scenarios, one panel per query with its attack trace, the
   summary and the analysis messages. What only the Workbench can do with a
   result (jump to a query's line, replay a trace on the diagram) is styled
   in workbench.css.
   =========================== */

.resultHeader {
	display: flex;
	flex-wrap: wrap;
	justify-content: space-between;
	gap: 4px 16px;
	font-family: var(--font-mono);
	font-size: 0.68rem;
	letter-spacing: 0.09em;
	text-transform: uppercase;
	color: var(--ink-3);
	margin-bottom: 16px;
	padding-bottom: 9px;
	border-bottom: 1px solid var(--line);
}

/* Declared weakening assumptions, shown above the results because they change
   what those results claim: an attack found under one is genuine only under
   that assumption, and a passing result is conditional on it. */
.resultAssumptions,
.resultScenarios {
	background: var(--sienna-tint);
	border: 1px solid var(--sienna-line);
	border-radius: var(--radius);
	padding: 14px 16px;
	margin-bottom: 12px;
}

.resultAssumptions .assumptionsTitle,
.resultScenarios .scenariosTitle {
	font-family: var(--font-mono);
	font-size: 0.68rem;
	font-weight: 500;
	letter-spacing: 0.1em;
	text-transform: uppercase;
	color: var(--sienna);
	margin-bottom: 9px;
}

.resultAssumptions .assumptionsList,
.resultScenarios .scenariosList {
	margin: 0;
	padding-left: 18px;
	list-style: square;
}

.resultAssumptions .assumptionsList li,
.resultScenarios .scenariosList li {
	font-size: 0.78em;
	color: var(--text-secondary);
	line-height: 1.7;
}

/* The site-wide `code` rule is a display:block code listing. These are inline
   terms inside a list item, so the block presentation has to be undone. */
.resultAssumptions .assumptionsList code,
.resultScenarios .scenariosList code {
	font-family: var(--font-mono);
	font-size: 0.95em;
	color: var(--sienna);
	background: var(--assumption-code-bg);
	padding: 1px 5px;
	border-radius: 3px;
}

.resultAssumptions .assumptionPhase,
.resultScenarios .scenarioPeer {
	color: var(--sienna);
	font-style: italic;
}

.resultAssumptions .assumptionsNote {
	font-size: 0.74em;
	color: var(--text-muted);
	margin-top: 8px;
	line-height: 1.6;
}

.resultQuery {
	background: var(--surface);
	border: 1px solid var(--line);
	border-radius: var(--radius);
	padding: 13px 16px;
	margin-bottom: 8px;
}

/* A contradiction colours the whole panel, since it changes what the model
   means. A query that holds needs no decoration beyond its badge. */
.resultQuery.resultFail {
	background: var(--breach-tint);
	border-color: var(--breach-line);
}

.resultQuery .queryText {
	font-family: var(--font-mono);
	font-size: 0.8rem;
	color: var(--ink);
	line-height: 1.5;
}

.resultQuery .querySubtype {
	color: var(--ink-3);
	margin-left: 0.4em;
}

.resultQuery .queryStatus {
	font-family: var(--font-mono);
	font-size: 0.62rem;
	font-weight: 500;
	letter-spacing: 0.11em;
	float: right;
	margin-left: 12px;
	padding: 2px 8px;
	border-radius: 3px;
	border: 1px solid transparent;
}

.resultQuery .queryStatus.pass {
	color: var(--olive-deep);
	background: var(--olive-tint);
	border-color: var(--olive-line);
}

.resultQuery .queryStatus.fail {
	color: var(--breach-deep);
	background: var(--surface);
	border-color: var(--breach-line);
}

/* The search a hold was reached under, as the CLI prints it after PASS. */
.resultQuery .queryEnvelope {
	margin-top: 6px;
	font-family: var(--font-mono);
	font-size: 0.68rem;
	letter-spacing: 0.02em;
	color: var(--ink-3);
}

.resultQuery .querySummary {
	font-family: var(--font-mono);
	font-size: 0.7rem;
	color: var(--ink-2);
	margin-top: 9px;
	white-space: pre-wrap;
	line-height: 1.65;
}

/* An attack trace, laid out as the CLI prints it in colour: the frame and the
   step numbers are dim, the steps themselves are plain, the outcome is the one
   line that carries the verdict, and the result of a query option sits apart
   from the trace it qualifies. Long terms wrap under their own step. */
.resultQuery .queryTrace {
	font-family: var(--font-mono);
	font-size: 0.7rem;
	color: var(--ink-2);
	margin-top: 9px;
	line-height: 1.65;
}

.queryTrace .qtHead,
.queryTrace .qtStep,
.queryTrace .qtOutcome,
.queryTrace .qtOption {
	display: grid;
	grid-template-columns: 1.7em minmax(0, 1fr);
}

.queryTrace .qtStep {
	grid-template-columns: 1.7em 2.6em minmax(0, 1fr);
}

.queryTrace .qtHead {
	color: var(--ink-4);
	font-style: italic;
}

.queryTrace .qtFrame,
.queryTrace .qtNo {
	color: var(--ink-4);
}

.queryTrace .qtText {
	overflow-wrap: anywhere;
}

.queryTrace .qtOutcome {
	margin-top: 6px;
	padding-top: 6px;
	border-top: 1px dashed var(--breach-line);
	color: var(--breach-deep);
	font-weight: 500;
}

.queryTrace .qtOutcome .qtFrame {
	color: var(--breach);
}

.queryTrace .qtOption {
	margin-top: 4px;
	color: var(--sienna);
	font-style: italic;
}

.queryTrace .qtOption .qtFrame {
	font-style: normal;
}

.resultSummary {
	font-family: var(--font-mono);
	font-size: 0.74rem;
	font-weight: 500;
	letter-spacing: 0.04em;
	margin-top: 16px;
	padding-top: 8px;
	border-top: 1px solid var(--border);
}

.resultSummary.allPass {
	color: var(--olive-deep);
}



.resultSummary.hasFail {
	color: var(--red);
}

.resultMessages {
	margin-top: 16px;
	padding-top: 8px;
	border-top: 1px solid var(--border);
}

.resultMessages summary {
	font-family: var(--font-mono);
	font-size: 0.72em;
	color: var(--text-muted);
	cursor: pointer;
	user-select: none;
}

.resultMessages pre {
	font-family: var(--font-mono);
	font-size: 0.7em;
	line-height: 1.5;
	color: var(--text-secondary);
	margin: 8px 0 0 0;
	white-space: pre-wrap;
	word-break: break-all;
}

.resultError {
	font-family: var(--font-mono);
	font-size: 0.78rem;
	line-height: 1.6;
	color: var(--breach-deep);
	background: var(--breach-tint);
	border: 1px solid var(--breach-line);
	border-radius: var(--radius);
	padding: 13px 16px;
	white-space: pre-wrap;
}

.resultLoading {
	font-family: var(--font-mono);
	font-size: 0.82em;
	color: var(--text-muted);
}

.resultLoading p {
	margin: 0 0 8px;
}

.resultLoading .progressStatus {
	font-size: 0.72rem;
	font-variant-numeric: tabular-nums;
	color: var(--ink-3);
	overflow-wrap: anywhere;
}

.progressVerdicts {
	list-style: none;
	margin: 8px 0 0;
	padding: 0;
	font-size: 0.74rem;
	line-height: 1.8;
	color: var(--ink-2);
}

.progressVerdicts span {
	display: inline-block;
	width: 3.2em;
	font-weight: 500;
	letter-spacing: 0.08em;
}

.progressVerdicts .fail span {
	color: var(--breach);
}

.resultPlaceholder {
	font-family: var(--font-mono);
	font-size: 0.76rem;
	line-height: 1.7;
	color: var(--ink-3);
}

.resultFacts {
	color: var(--ink-3);
	text-transform: none;
	letter-spacing: 0.04em;
}

.resultNote,
.resultDelta {
	font-size: 0.8rem;
	line-height: 1.55;
	color: var(--ink-2);
	margin: -6px 0 14px;
}

.resultDelta {
	font-family: var(--font-mono);
	font-size: 0.72rem;
	color: var(--ink-3);
}

.deltaFixed {
	color: var(--olive-deep);
	font-weight: 500;
}

.deltaBroken {
	color: var(--breach);
	font-weight: 500;
}

.resultQuery .queryDelta {
	float: right;
	margin-left: 8px;
	padding: 2px 0;
	font-family: var(--font-mono);
	font-size: 0.62rem;
	letter-spacing: 0.08em;
	color: var(--ink-3);
}

.resultQuery .queryDelta.fixed {
	color: var(--olive-deep);
}

.resultQuery .queryDelta.broken {
	color: var(--breach-deep);
}

/* ===========================
   Diagnostics

   Verifpal reports errors the way a compiler does. The panel lays that back
   out instead of printing it as one block: the headline, a location you can
   click to put the caret on the token, the offending line under its own
   number, the caret span, and the notes.
   =========================== */

.diagnostic {
	border: 1px solid var(--breach-line);
	border-radius: var(--radius);
	background: var(--breach-tint);
	padding: 14px 16px;
	font-size: 0.78rem;
	line-height: 1.6;
}

.diagnostic.diagWarn {
	border-color: var(--sienna-line);
	background: var(--sienna-tint);
}

.diagHead {
	font-family: var(--font-sans);
	color: var(--ink);
	margin-bottom: 10px;
}

.diagPrefix,
.diagKind {
	font-family: var(--font-mono);
	font-size: 0.72rem;
	letter-spacing: 0.08em;
	text-transform: uppercase;
	color: var(--breach-deep);
}

.diagWarn .diagPrefix,
.diagWarn .diagKind {
	color: var(--sienna);
}

.diagMessage {
	display: block;
	margin-top: 4px;
	font-size: 0.88rem;
	color: var(--ink);
}

.diagMessage code,
.diagNote code {
	font-family: var(--font-mono);
	font-size: 0.85em;
	background: var(--diagnostic-code-bg);
	border: 1px solid var(--breach-line);
	border-radius: 3px;
	padding: 0 4px;
}

.diagWarn .diagMessage code,
.diagWarn .diagNote code {
	border-color: var(--sienna-line);
}

.diagLoc {
	display: inline-block;
	font-family: var(--font-mono);
	font-size: 0.72rem;
	color: var(--azure-deep);
	background: none;
	border: none;
	border-bottom: 1px dashed var(--azure-line);
	padding: 0 0 1px 0;
	margin-bottom: 10px;
	cursor: pointer;
}

.diagLoc:hover {
	color: var(--azure);
	border-bottom-style: solid;
}

.diagSnippet {
	background: var(--surface);
	border: 1px solid var(--breach-line);
	border-radius: var(--radius);
	padding: 10px 0;
	margin-bottom: 10px;
	overflow-x: auto;
}

.diagWarn .diagSnippet {
	border-color: var(--sienna-line);
}

.diagRow {
	display: flex;
	font-family: var(--font-mono);
	font-size: 0.78rem;
	line-height: 1.5;
	white-space: pre;
}

.diagGutter {
	flex-shrink: 0;
	width: 46px;
	padding-right: 12px;
	text-align: right;
	color: var(--ink-4);
	user-select: none;
}

.diagCode {
	color: var(--ink);
	padding-right: 16px;
}

.diagCaret {
	color: var(--breach);
	font-weight: 700;
}

.diagWarn .diagCaret {
	color: var(--sienna);
}

.diagLabel {
	color: var(--breach-deep);
}

.diagWarn .diagLabel {
	color: var(--sienna);
}

.diagNote {
	font-family: var(--font-sans);
	font-size: 0.78rem;
	line-height: 1.6;
	color: var(--ink-2);
	padding-left: 14px;
	position: relative;
}

.diagNote+.diagNote {
	margin-top: 5px;
}

.diagNote::before {
	content: "=";
	position: absolute;
	left: 0;
	font-family: var(--font-mono);
	color: var(--ink-4);
}

.diagNoteKind {
	font-family: var(--font-mono);
	font-size: 0.72rem;
	letter-spacing: 0.06em;
	text-transform: uppercase;
	color: var(--ink-3);
}