runs locally

The playground is a local experience

Each playground session drives a live EasyCrypt process, and the prover runs through your own Claude Code login — so it ships with the repository instead of running on this website. Getting it on your screen takes about a minute once the install steps are done:

Clone the source:

git clone https://github.com/SkyShannonProver/shannon-prover.git
cd shannon-prover

Install EasyCrypt and the Python environment — see the install steps on the home page.
Start the server and open the playground:

eval "$(opam env --switch=easycrypt)"
uv run --with fastapi --with "uvicorn[standard]" \
    uvicorn playground.server:app --host 127.0.0.1 --port 8000
# then open http://127.0.0.1:8000/playground

In the playground you sit where the agent sits: pick a target file and a lemma, press start, read the same panel the agent reads, and submit one intent per turn — EasyCrypt accepts or rejects each tactic live, and you can flip between Goal-only and Workbench mode mid-proof. Until then, the benchmark browser shows recorded agent runs — every turn replayable, right here in the browser.

What it looks like — a game-hopping reduction, replayed

A real session against this repo: replaying, by hand, the agent-found proof of cpa_ddh0 — ElGamal's CPA game reduced to DDH (eval/examples/elgamal.ec).

Playground right after starting a session: transcript on the left, the Workbench panel on the right showing the probability goal linking the CPA game to the DDH game, plus tactic-applicability facts — 1Pick `elgamal.ec` / `cpa_ddh0`, press Start. The right panel is exactly what the agent reads: the `Pr[...]` goal connecting the two games, plus the compiler's factual cards on which opener families even apply here.

After byequiv, proc, inline: the pRHL panel lays both games side by side with numbered, aligned instructions — the ElGamal CPA game on the left, the DDH game on the right — plus a Surgery card summarizing whole-program structure — 2After `byequiv` · `proc` · `inline *` the panel lays the two games side by side, instruction-aligned — CPA left, DDH right, adversary calls and samplings matched up. The *Surgery* card summarizes both programs' structure; this is the map the agent navigates when it decides to `swap`.

The Need more? context topics in action: clicking tactic_forms call returns the call tactic's argument forms in a panel, with a lookahead card above — 3The panel's *context topics* are live — clicking `tactic_forms · call` runs the same read-only intent the agent submits and returns the `call` argument forms (`call LEMMA` vs `call (_: INVARIANT)`). Above it, the *Lookahead* card shows what sits past the current frontier on each side.

The same pRHL proof state rendered in Goal-only mode: the panel collapses to just the bare EasyCrypt goal — 4Flip to **Goal-only** mid-proof: same session, same state — the map disappears and only the raw pRHL goal remains. That is the paper's interface ablation (L1 vs L4), live under your cursor.

Late in the proof: the Pure Logic Residual card lists pending premises and memory-decorated terms, with operator-lemma context topics for the remaining algebra — 5After the program steps are discharged, a different panel family takes over: *Pure Logic Residual* lists the pending premises, and the context topics switch to the operator lemmas (`(^)`, `(\in)`, `dt`) the remaining algebra needs — closed here by `smt(expM)`.

The finished session: the transcript shows the whole reduction proof and the panel reads candidate_closed, 0 goals, complete after qed — 6Commit `qed.` — the panel flips to `candidate_closed · 0 goals · complete`. The transcript is the whole reduction: two `call (_: true)` adversary steps, one `swap` alignment, and a machine-checked close.

Get the source Browse recorded runs ← Home