minicheck-0.4.0-py3-none-any.whl
specforge-0.1.0-py3-none-any.whl
from __future__ import annotations
import json
import gradio as gr
from specforge import DIFFICULTIES, SHAPES, always_safe_baseline, bfs_baseline, generate, score, summarise
INTRO = """
# Can your solver *demonstrate* what it claims?
Paste a submission and it is scored **with the counterexamples replayed**. A claim without a trace
that replays earns nothing — which is the only way to tell a solver that found a bug from one that
guessed the label.
Tasks are **generated**, not fixed, so nothing here can be memorised. Change the seed and the answer
key changes. Everything runs in your browser; nothing is uploaded.
"""
SUBMISSION_HELP = """
A submission maps task id to a prediction:
```json
{
"mutual_exclusion_medium_3": {"violated": true,
"trace": [{"state": {"p0": 0, "p1": 0, "lock": 0}}, ...]},
"handshake_medium_7": {"violated": false}
}
```
`violated` is required. `trace` is what earns the detection: it must start at the initial state,
move only along real transitions, and end in a state that genuinely violates the property.
"""
def _fmt(res: dict) -> str:
gap = res["accuracy_ignoring_replay"] - res["accuracy"]
out = [
f"## Balanced accuracy: **{res['balanced_accuracy']:.3f}**",
"",
"| metric | value |",
"|---|---|",
f"| tasks | {res['n_tasks']} |",
f"| **balanced accuracy** | **{res['balanced_accuracy']:.3f}** |",
f"| accuracy | {res['accuracy']:.3f} |",
f"| trivial always-safe accuracy | {res['trivial_always_safe_accuracy']:.3f} |",
f"| recall on violated | {res['recall_violated']:.3f} |",
f"| recall on safe | {res['recall_safe']:.3f} |",
f"| detections claimed | {res['detections_claimed']} |",
f"| **counterexamples that replayed** | **{res['valid_counterexamples']}** |",
f"| claims that did not replay | {res['unreplayed_claims']} |",
f"| TP / FP / FN / TN | {res['true_positives']} / {res['false_positives']} / "
f"{res['false_negatives']} / {res['true_negatives']} |",
"",
]
if gap > 1e-9:
out.append(
f"> ⚠️ **Accuracy ignoring replay is {res['accuracy_ignoring_replay']:.3f}, "
f"against {res['accuracy']:.3f} credited.** This submission asserts more than it "
f"demonstrates — {res['unreplayed_claims']} claim(s) had no trace that replays."
)
out.append("")
if res["by_shape"]:
out.append("### By shape")
out.append("| shape | tasks | correct |")
out.append("|---|---|---|")
for shape, v in sorted(res["by_shape"].items()):
out.append(f"| `{shape}` | {v['n']} | {v['correct']} |")
out.append("")
bad = [r for r in res["per_task"] if r["predicted_violated"] and not r["credited_detection"]]
if bad:
out.append("### Claims that were not credited, and why")
out.append("| task | reason |")
out.append("|---|---|")
for r in bad[:15]:
out.append(f"| `{r['id']}` | {r['trace'].get('reason', '—')} |")
return "\n".join(out)
def make_tasks(n: int, seed: int, difficulty: str):
return generate(int(n), seed=int(seed), difficulty=difficulty)
def show_tasks(n, seed, difficulty):
tasks = make_tasks(n, seed, difficulty)
if not tasks:
return "No tasks were generated for those settings.", ""
s = summarise(tasks)
lines = [
f"**{s['n_tasks']} tasks** — {s['n_violated']} violated, {s['n_safe']} safe, "
f"{s['total_states']} reachable states in total.",
"",
"| id | shape | states | violated |",
"|---|---|---|---|",
]
for t in tasks[:25]:
lines.append(f"| `{t.id}` | {t.shape} | {t.reachable_states} | {'yes' if t.is_violated else 'no'} |")
if len(tasks) > 25:
lines.append(f"| … | | | *{len(tasks) - 25} more* |")
payload = {"summary": s, "tasks": [t.as_dict() for t in tasks]}
return "\n".join(lines), json.dumps(payload, indent=2)
def run_baseline(which, n, seed, difficulty):
tasks = make_tasks(n, seed, difficulty)
if not tasks:
return "No tasks were generated for those settings."
sub = bfs_baseline(tasks) if which == "bfs (runs the checker)" else always_safe_baseline(tasks)
return _fmt(score(sub, tasks))
def run_fabricated(n, seed, difficulty):
"""The demonstration that makes the metric's point better than any explanation."""
tasks = make_tasks(n, seed, difficulty)
if not tasks:
return "No tasks were generated for those settings."
sub = {t.id: {"violated": t.is_violated, "trace": [{"state": {"NOT": "REAL"}}]} for t in tasks}
res = score(sub, tasks)
return (
"### An oracle that knows every answer and fabricates every trace\n\n"
"Perfect labels. No evidence. Watch what it scores.\n\n" + _fmt(res)
)
def score_submission(text, n, seed, difficulty):
if not (text or "").strip():
return "Paste a submission, or press one of the baseline buttons."
try:
submission = json.loads(text)
except json.JSONDecodeError as e:
return f"### ⚠️ Not valid JSON\n\n```\n{e}\n```"
if not isinstance(submission, dict):
return "### ⚠️ A submission must be a JSON object mapping task id to a prediction."
tasks = make_tasks(n, seed, difficulty)
if not tasks:
return "No tasks were generated for those settings."
known = {t.id for t in tasks}
unknown = [k for k in submission if k not in known]
res = score(submission, tasks)
out = _fmt(res)
if unknown:
out += (
f"\n\n> Note: {len(unknown)} id(s) in your submission are not in this task set "
f"(e.g. `{unknown[0]}`). They were ignored — check the seed, count and difficulty match "
f"the set you solved."
)
return out
with gr.Blocks(title="specforge leaderboard") as demo:
gr.Markdown(INTRO)
with gr.Row():
n = gr.Slider(5, 100, value=20, step=5, label="tasks")
seed = gr.Number(value=42, precision=0, label="seed")
difficulty = gr.Dropdown(sorted(DIFFICULTIES), value="medium", label="difficulty")
with gr.Tab("Score a submission"):
gr.Markdown(SUBMISSION_HELP)
box = gr.Code(label="submission JSON", language="json", lines=14)
btn = gr.Button("Score it — replaying every counterexample", variant="primary")
result = gr.Markdown()
btn.click(score_submission, [box, n, seed, difficulty], result)
with gr.Tab("Baselines"):
gr.Markdown(
"Three reference points. The third is the one worth looking at: **perfect labels, "
"fabricated traces**. It scores what guessing scores, because it demonstrated nothing."
)
which = gr.Radio(
["bfs (runs the checker)", "always-safe (guesses)"],
value="bfs (runs the checker)",
label="baseline",
)
b1 = gr.Button("Run baseline")
b2 = gr.Button("Run the fabricated-trace oracle", variant="stop")
bout = gr.Markdown()
b1.click(run_baseline, [which, n, seed, difficulty], bout)
b2.click(run_fabricated, [n, seed, difficulty], bout)
with gr.Tab("The task set"):
gr.Markdown(
"Generated deterministically from the seed. Every label was computed by an exhaustive "
"model checker; a candidate the checker could not settle produces **no task** rather "
"than a guessed one."
)
t1 = gr.Button("Show the tasks")
tview = gr.Markdown()
tjson = gr.Code(label="tasks.json — download and solve offline", language="json", lines=12)
t1.click(show_tasks, [n, seed, difficulty], [tview, tjson])
gr.Markdown(
f"""
---
**Shapes:** {", ".join(f"`{s}`" for s in SHAPES)}
**Honest scope.** A score here measures how well a solver finds *and demonstrates* safety violations
in synthetic finite state machines at a given size. It says nothing about real-world protocol
implementations, nothing about reading a specification, and nothing comparable across seeds unless
you report which one you used.
Nothing here asserts anything about any named third-party protocol or product.
[generator](https://github.com/nickharris808/specforge) ·
[dataset](https://huggingface.co/datasets/nickh007/specforge) ·
[checker](https://github.com/nickharris808/minicheck)
"""
)
gr.Markdown(
"---\n"
"**A verdict you cannot check is not a verdict** — and *undetermined is not a pass*. "
"This demo is one piece of a larger set.\n\n"
"[Documentation](https://nickharris808.github.io/verification-docs/) · "
"[minicheck](https://github.com/nickharris808/minicheck) · "
"[protocol-bench](https://github.com/nickharris808/protocol-bench) · "
"[specforge](https://github.com/nickharris808/specforge) · "
"[the browser demo](https://huggingface.co/spaces/nickh007/protocol-bench-demo)"
)
demo.launch()