{% extends "pages/sandbox_base.html" %}
{% block title %}Policy Verification — {{ sandbox_name }} — Shoreguard{% endblock %}

{% block breadcrumb_tail %}
<li class="breadcrumb-item active">Verify</li>
{% endblock %}

{% block content %}
<div x-data='proverPage({{ gateway_name|tojson }}, {{ sandbox_name|tojson }})' x-init="init()">
    <!-- Header -->
    <div class="d-flex justify-content-between align-items-center mb-3">
        <div>
            <h5 class="mb-1">Policy Formal Verification</h5>
            <p class="text-muted small mb-0">
                Run Z3 SMT solver queries against the active policy to prove security properties.
            </p>
        </div>
    </div>

    <!-- Query builder -->
    <div class="card mb-3">
        <div class="card-header d-flex justify-content-between align-items-center">
            <span class="fw-medium">Verification Queries</span>
            <div class="dropdown">
                <button class="btn btn-sm btn-primary dropdown-toggle" data-bs-toggle="dropdown">
                    <i class="bi bi-plus-lg me-1"></i>Add Query
                </button>
                <ul class="dropdown-menu">
                    <template x-for="preset in presets" :key="preset.query_id">
                        <li>
                            <a class="dropdown-item" href="#" @click.prevent="addQuery(preset)">
                                <div class="fw-medium" x-text="preset.label"></div>
                                <div class="text-muted small" x-text="preset.description"></div>
                            </a>
                        </li>
                    </template>
                </ul>
            </div>
        </div>
        <div class="card-body">
            <!-- Empty state -->
            <div x-show="selectedQueries.length === 0" class="text-center text-muted py-4">
                <i class="bi bi-patch-question fs-1"></i>
                <p class="mt-2">Select a verification query from the dropdown above.</p>
            </div>

            <!-- Selected queries -->
            <template x-for="(sq, idx) in selectedQueries" :key="idx">
                <div class="border rounded p-3 mb-2">
                    <div class="d-flex justify-content-between align-items-start mb-2">
                        <div>
                            <span class="fw-medium" x-text="sq.label"></span>
                            <span class="text-muted small ms-2" x-text="sq.description"></span>
                        </div>
                        <button class="btn btn-sm btn-outline-danger" @click="removeQuery(idx)" title="Remove">
                            <i class="bi bi-x-lg"></i>
                        </button>
                    </div>
                    <!-- Parameter inputs -->
                    <template x-for="(pdef, pname) in sq.paramDefs" :key="pname">
                        <div class="mb-2">
                            <label class="form-label small mb-1" x-text="pname"></label>
                            <input type="text" class="form-control form-control-sm"
                                   :placeholder="pdef.placeholder || ''"
                                   x-model="sq.params[pname]">
                        </div>
                    </template>
                </div>
            </template>

            <!-- Run button -->
            <div x-show="selectedQueries.length > 0" class="mt-3">
                <button class="btn btn-primary" @click="runVerification()" :disabled="running">
                    <span x-show="running">
                        <span class="spinner-border spinner-border-sm me-1"></span>Verifying...
                    </span>
                    <span x-show="!running">
                        <i class="bi bi-play-fill me-1"></i>Run Verification
                    </span>
                </button>
            </div>
        </div>
    </div>

    <!-- Results -->
    <div x-show="results.length > 0" x-cloak>
        <div class="d-flex justify-content-between align-items-center mb-2">
            <h6 class="mb-0">Results</h6>
            <span class="text-muted small">
                Total: <span x-text="totalTimeMs.toFixed(1)"></span> ms
            </span>
        </div>

        <template x-for="(r, i) in results" :key="i">
            <div class="card mb-2" :class="verdictBorder(r.verdict)">
                <div class="card-body py-2">
                    <div class="d-flex justify-content-between align-items-center">
                        <div class="d-flex align-items-center gap-2">
                            <i class="bi fs-5" :class="verdictIcon(r.verdict)"></i>
                            <div>
                                <span class="fw-medium" :class="verdictColor(r.verdict)"
                                      x-text="r.verdict"></span>
                                <span class="text-muted small ms-2" x-text="r.query"></span>
                            </div>
                        </div>
                        <span class="badge bg-light text-dark" x-text="r.z3_time_ms.toFixed(1) + ' ms'"></span>
                    </div>

                    <!-- Counterexample -->
                    <div x-show="r.counterexample" class="mt-2">
                        <div class="bg-light rounded p-2 font-monospace small">
                            <div class="text-danger fw-medium mb-1">Counterexample:</div>
                            <template x-for="[k, v] in Object.entries(r.counterexample || {})" :key="k">
                                <div>
                                    <span class="text-muted" x-text="k + ': '"></span>
                                    <span x-text="v"></span>
                                </div>
                            </template>
                        </div>
                    </div>
                </div>
            </div>
        </template>
    </div>

    <!-- Error -->
    <div x-show="error" class="alert alert-danger" x-text="error" x-cloak></div>
</div>
{% endblock %}

{% block sandbox_js %}
<script src="/static/js/prover.js"></script>
{% endblock %}