diff --git a/README.md b/README.md index 9ef3d2917e..902d7bc3cb 100644 --- a/README.md +++ b/README.md @@ -26,7 +26,6 @@ EasyCrypt is part of the [Formosa Crypto project](https://formosa-crypto.org/). - [Visual Studio Code](#visual-studio-code) - [Useful Resources](#useful-resources) - [Examples](#examples) - - [LaTeX Formatting](#latex-formatting) # Installation @@ -186,10 +185,3 @@ Examples of how to use EasyCrypt are in the `examples` directory. You will find basic examples at the root of this directory, as well as a more advanced example in the `MEE-CBC` sub-directory and a tutorial on how to use the complexity system in `cost` sub-directory. - -## LaTeX Formatting - -LaTeX style file is in `assets/latex` directory. The basic usages are -`\begin{eclst} ... \end{eclst}` (display mode) and -`\ecinl{proc main() = { ... }}` (inline mode). - diff --git a/assets/latex/eclistings.sty b/assets/latex/eclistings.sty deleted file mode 100644 index 7b5c15d681..0000000000 --- a/assets/latex/eclistings.sty +++ /dev/null @@ -1,155 +0,0 @@ -\NeedsTeXFormat{LaTeX2e} -\ProvidesPackage{eclistings}[2026/04/07 EasyCrypt listings] - -\RequirePackage{listings} -\RequirePackage{xcolor} -\RequirePackage{xparse} - -% EasyCrypt % Language -\lstdefinelanguage{easycrypt}{% - sensitive=true, % Case sensitive keywords - % Keywords: Global and programming language - morekeywords=[1]% - { - Pr, Self, Top, abbrev, abort, abstract, as, axiom, axiomatized, clone, const, - declare, dump, end, exception, exit, export, from, global, goal, hint, import, - include, inductive, instance, lemma, local, locate, module, notation, of, op, - pred, print, proof, prover, qed, realize, remove, rename, require, search, - section, subtype, theory, timeout, type, why3, with, - async, ehoare, elif, else, equiv, exists, for, forall, fun, glob, hoare, if, - in, is, islossless, let, match, phoare, proc, raise, res, return, then, var, - while - }, - % Keywords: Regular (i.e., non-closing) tactics - morekeywords=[2]% - { - algebra, alias, apply, auto, beta, byehoare, byequiv, byphoare, bypr, byupto, - call, case, cbv, cfold, change, clear, congr, conseq, delta, eager, ecall, - elim, eta, exfalso, exlim, fel, field, fieldeq, fission, fusion, gen, have, - idassign, idtac, inline, interleave, iota, kill, left, logic, modpath, move, - outline, pose, pr_bounded, progress, rcondf, rcondt, replace, rewrite, right, - ring, ringeq, rnd, rndsem, rwnormal, seq, sim, simplify, skip, sp, split, - splitwhile, subst, suff, swap, symmetry, transitivity, trivial, unroll, - weakmem, wlog, wp, zeta - }, - % Keywords: Closing/byclose tactics and dangerous commands - morekeywords=[3]% - { - admit, admitted, - assumption, by, check, coq, done, edit, exact, fix, reflexivity, smt, solve - }, - % Keywords: Tacticals and internal - morekeywords=[4]% - { - do, expect, first, last, try, - debug, fail, pragma, time, undo - }, - comment=[n]{(*}{*)}, % Multi-line, nested comments delimited by (* and *) - string=[d]{"}, % Strings delimited by " and ", non-escapable -} - -% Style (base/default) -\lstdefinestyle{easycrypt-base}{% - % Frame - captionpos=t, % Position caption at top (mirroring what's typical for algorithms) - frame=tb, % Top and bottom rules - framesep=\smallskipamount, % Small skip between frame and listing content - % Float placement - floatplacement=tbhp, - % Character printing and placement - upquote=true, % Print backtick and single quote as is - columns=[c]fixed, % Monospace characters, centered in their box - keepspaces=true, % Don't drop spaces for column alignment - tabsize=2, % Tabstops every 2 spaces - mathescape=false, % Don't allow escaping to LaTeX with $ - showstringspaces=false, % Don't print characters for spaces - % Line numbers - numbers=none, % No line numbers - % Basic style - basicstyle={\normalsize\ttfamily}, - % Style for (non-keyword) identifiers - identifierstyle={}, -} - -% Define default colors based on availability of colorblind colors -\@ifpackageloaded{colorblind}{ - \lstdefinestyle{easycrypt-default}{% - style=easycrypt-base, - % Styles for different keyword classes - keywordstyle=[1]{\color{T-Q-B6}},% - keywordstyle=[2]{\color{T-Q-B1}},% - keywordstyle=[3]{\color{T-Q-B5}},% - keywordstyle=[4]{\color{T-Q-B4}},% - % Styles for comments and strings - commentstyle={\itshape\color{T-Q-B0}},% - stringstyle={\color{T-Q-B3}}, - % Style of line numbers (in case numbers is overwritten to true) - numberstyle={\small\color{T-Q-B0}}, - } -}{% - \lstdefinestyle{easycrypt-default}{% - style=easycrypt-base, - % Styles for different keyword classes - keywordstyle=[1]{\color{violet}},% - keywordstyle=[2]{\color{blue}},% - keywordstyle=[3]{\color{red}},% - keywordstyle=[4]{\color{olive}},% - % Styles for comments and strings - commentstyle={\itshape\color{gray}},% - stringstyle={\color{green}}, - % Style of line numbers (in case numbers is overwritten to true) - numberstyle={\small\color{gray}}, - } -} - -% Style for drafting/debugging (explicit spaces/tabs) -\lstdefinestyle{easycrypt-draft}{% - style=easycrypt-default, - showspaces=true, - showtabs=true, - showstringspaces=true, -} - -% Style without top/bottom frame rules -\lstdefinestyle{easycrypt-plain}{% - style=easycrypt-default, - frame=none, - framesep=0pt, - basicstyle={\small\ttfamily}, - aboveskip=0.3\baselineskip, - belowskip=0.3\baselineskip, - columns=fullflexible -} - -% Environments % Default, non-floating environment % Meant to be used inside -%other (potentially floating) environment % that takes care of the caption and -%surrounding spacing -\lstnewenvironment{eclst}[1][]{% - \lstset{% - language=easycrypt,% - style=easycrypt-default,% - aboveskip=\smallskipamount,% Equal to framesep of style if top rule, else 0pt - belowskip=\smallskipamount,% Equal to framesep of style if bottom rule, else 0pt - abovecaptionskip=0pt,% - belowcaptionskip=0pt,% - #1% - }% -}{} - -% Inline -\NewDocumentCommand{\ecinl}{O{easycrypt-default} m O{}}{% - \lstinline[% - language=easycrypt,% - style=#1,% - breaklines,% - breakindent=0pt,% - columns=fullflexible,% - #3% - ]{#2}% -} - -\NewDocumentCommand{\ecinlfoot}{O{easycrypt-default} m O{}}{% - \ecinl[#1]{#2}[basicstyle={\footnotesize\ttfamily},#3]% -} - -\endinput \ No newline at end of file diff --git a/doc/llm/CLAUDE.md b/doc/llm/CLAUDE.md new file mode 100644 index 0000000000..0d7dd179c7 --- /dev/null +++ b/doc/llm/CLAUDE.md @@ -0,0 +1,432 @@ +# EasyCrypt — LLM Agent Guide + +EasyCrypt is a proof assistant for reasoning about the security of +cryptographic constructions. It provides support for probabilistic +computations, program logics (Hoare logic, probabilistic Hoare logic, +probabilistic relational Hoare logic), and ambient mathematical +reasoning. + +## Using the `llm` interactive mode + +The `llm` subcommand provides an interactive REPL with a +machine-friendly protocol designed for LLM agents. The LLM sends +commands over stdin and receives structured responses on stdout. + +``` +easycrypt llm [OPTIONS] +``` + +Standard loader and prover options (`-I`, `-timeout`, `-p`, etc.) are +available. Use `-help` to print this guide and exit: + +``` +easycrypt llm -help +``` + +### Protocol + +**Startup.** EasyCrypt prints a `READY` message and waits for input: + +``` +READY [uuid:0] + +``` + +**Responses.** Every response has a typed envelope and an `` +sentinel: + +``` +OK [uuid:N] + + +``` + +``` +ERROR [uuid:N] + + +``` + +The `uuid` is a monotonically increasing integer identifying the proof +engine state. It increments with each successful command. + +### Meta-commands + +These are protocol-level commands, not EasyCrypt syntax: + +| Command | Description | +|---------|-------------| +| `LOAD "file.ec" [LINE[:COL]] [-nosmt]` | Reset state, compile file (optionally skip SMT) | +| `UNDO` | Undo the last proof step | +| `REVERT ` | Revert to a specific state (by uuid or checkpoint name) | +| `GOALS` | Print the current goal (first subgoal only, with remaining count) | +| `GOALS ALL` | Print all subgoals | +| `CHECKPOINT ` | Save current uuid under a name for later `REVERT` | +| `SEARCH ` | Search for lemmas matching a pattern | +| `QUIET ON` / `QUIET OFF` | Suppress/enable automatic goal display after tactics | +| `` / `` | Delimit multi-line EasyCrypt input | +| `HELP` | Print this guide | +| `QUIT` | Exit | + +### EasyCrypt commands + +Any line that is not a meta-command is parsed as EasyCrypt input. +This covers tactics, declarations, `search`, `print`, `require`, +etc. The line must be a complete EasyCrypt statement ending with `.` + +``` +smt(). +rewrite H1 H2. +search (%/). +print mulzK. +``` + +For multi-line statements, wrap with `` and ``: + +``` + +lemma test : + 0 <= n => + 0 < n + 1. + +``` + +### Workflow + +**1. Load a file up to the proof point:** + +``` +LOAD "myfile.ec" 42 +``` + +This compiles the file through line 42 (processing any command whose +end is on or before that line). The response includes where it +stopped: + +``` +OK [uuid:15] [loaded:myfile.ec:42] +Current goal +... + +``` + +For large files, use `-nosmt` to skip SMT calls during prefix +compilation (safe when the prefix was already verified): + +``` +LOAD "myfile.ec" 436 -nosmt +``` + +**2. Try tactics, using REVERT to restart:** + +The uuid returned by LOAD is a revertible state. Use `REVERT` to +return to it after failed experiments — this is instant, unlike +re-doing LOAD which recompiles the prefix. + +``` +LOAD "myfile.ec" 42 +→ OK [uuid:15] [loaded:myfile.ec:42] + +smt(). ← fails, state unchanged +rewrite H1. smt(). ← succeeds (uuid:17) +rewrite H2. ← wrong direction +REVERT 17 ← back to after the successful smt() +``` + +To restart the proof from scratch, revert to the LOAD uuid: + +``` +REVERT 15 ← back to the state right after LOAD +``` + +Always note the LOAD uuid so you can return to it. + +**3. Use checkpoints for branching exploration:** + +``` +CHECKPOINT before_split +split. +smt(). ← fails +REVERT before_split +apply H. ← try a different approach +``` + +**4. Use QUIET mode to save tokens during bulk tactic application:** + +``` +QUIET ON +rewrite H1. +rewrite H2. +rewrite H3. +QUIET OFF +GOALS +``` + +**5. Search for lemmas using patterns:** + +EasyCrypt `search` uses pattern syntax, not keywords. Use `_` as +wildcard: + +``` +search (fdom _). ← lemmas involving fdom +search (_ %/ _). ← integer division lemmas +search (card (_ `|` _)). ← card of union +search (mu _ _) (_ <= _). ← mu lemmas with inequalities +``` + +The SEARCH meta-command is a shorthand that adds `search`/`.`: + +``` +SEARCH (fdom _) +SEARCH (_ %/ _) +``` + +### When the agent can't hold a persistent pipe + +Some LLM front-ends (Claude Code, Codex CLI, etc.) expose the shell as +one-shot command execution — the agent *cannot* keep stdin/stdout open +to `easycrypt llm` across turns. Naively, every tactic would then +require re-`LOAD`-ing the file prefix. + +The `scripts/llm/` directory contains a reference fifo-backed daemon +that lets many short-lived shell invocations drive one persistent EC +REPL. Start it once at the beginning of a session, then issue each +tactic as a separate `ec_send.sh` call. See `scripts/llm/README.md` for +the full pattern. + +### Iterate interactively, then codify + +For long proofs — especially program-logic bodies with 5+ chained +`ecall`s, or big algebraic derivations — write tactics one at a time +in the REPL, inspecting `GOALS` after each, and only commit the final +sequence back to the file once it works. Two reasons: + +- **SMT budget.** Committing a long batch and issuing one LOAD + compounds SMT cost across every intermediate side-condition at once. + The same tactics often pass individually with a shorter per-call + timeout. +- **Cheap backtracking.** Use `CHECKPOINT` at every branching point + and `REVERT` liberally — it's O(1), whereas re-LOAD re-compiles the + whole prefix. + +Pattern: + +``` +LOAD "file.ec" 100 ← note uuid:N +CHECKPOINT before_body + +GOALS ← inspect + +REVERT before_body ← if the branch fails +``` + +## EasyCrypt proof strategy + +### General approach + +- Start with a pen-and-paper proof plan before writing tactics. +- Use `smt()` aggressively. Try it first — if it fails, add hints: + `smt(lemma1 lemma2)`. +- Build proofs with `have` assertions. Establish intermediate facts + as named hypotheses, then combine with `smt()`. Avoid long rewrite + chains. +- Case split early: `case (n = 0) => [->|hn0].` Base cases often + close by computation. +- Provide specific instances of lemmas to smt: + `have h := lemma arg1 arg2.` SMT works much better with ground + instances than with universally quantified axioms. + +### Integer division (`%/`) + +- `divzK`: `d %| m => m %/ d * d = m` — recovering from exact + division +- `mulzK`: `d <> 0 => m * d %/ d = m` — canceling a known factor +- `divzMpl`: `0 < p => p * m %/ (p * d) = m %/ d` — simplifying + common factors +- To prove `a %/ d = x`, establish `a = x * d` (with `d %| a`), + then use `mulzK`. +- Don't try to rewrite inside `%/` expressions directly. Instead, + prove the equality as a `have` and use it. + +### What works, what doesn't + +- `ring` solves polynomial equalities over integers but treats + abstract ops (like `fact`) as opaque. It **cannot** simplify + `fact(n-1+1)` to `fact(n)`. +- `smt()` can do linear arithmetic and combine hypotheses, but + struggles with nonlinear integer division. Pre-compute key facts + with `have` and `divzK`/`mulzK`, then let smt combine them. +- `rewrite {k}h` rewrites the k-th occurrence only. Essential when a + term appears on both sides of an equation. +- For induction on naturals: `elim/natind: n` gives base (`n ≤ 0`) + and step (`0 ≤ n → P n → P (n+1)`). + +### SMT usage + +`smt()` and `/#` are equivalent — both call external SMT solvers. + +- Use `smt()` **only** on goals that are pure arithmetic or pure + propositional logic. If the goal contains abstract operators, + FMap terms, or `if-then-else`, reduce it first with `rewrite`, + `case`, or `have` before calling `smt()`. +- If `smt()` takes more than 1 second, the goal is too complex. + Simplify with interactive tactics instead of increasing the + timeout. + +### Common pitfalls + +- `rewrite (factS n) //` generates a side goal `0 <= n`. Use + `first smt()` or provide the precondition explicitly. +- `by` closes **all** remaining subgoals. If it fails, the error + refers to the first unclosed goal, which may not be the intended + one. +- When a tactic generates multiple subgoals, each subgoal must be + closed in order. Use `GOALS ALL` to see them all. +- `rewrite lemma in H` modifies hypothesis `H` in place (it does + not consume it). If you need to preserve the original, copy it + first: `have H' := H; rewrite lemma in H'`. +- **`have H := lemma args` may leave unevaluated lambdas.** Lemma + applications that produce `init`/`map`/`filter` terms often carry + β-redexes into the introduced hypothesis. Later `rewrite H` can then + hang indefinitely while the kernel tries to unify. Force + normalization at introduction with `have /= H := lemma args`. +- **Tactic-repetition (`!tac`) over-applies on nested structures.** + `!mapiE`, `!initiE`, `!allP` descend into inner layers at different + array sizes, generate side-conditions that can't be closed by `/#`, + and either leave stale goals or hang. Use the exact count needed + (usually 1 or 2 for an equality: `rewrite mapiE 1:/# /= mapiE 1:/#`). +- **`1:/#` vs `1:smt(hints)` in rewrite chains.** Inside a + `rewrite lemma 1:...` position only `/#` parses; `1:smt(hints)` is + a parse error. Break the chain: + `rewrite lemma 1:/#; first smt(hints). rewrite next_lemma.` +- **`suff` not `suffices`.** The surface syntax uses `suff H : P.`; + `suffices` triggers a parse error. +- **`rewrite allP` only touches the first `all`.** When unfolding + range predicates on both sides of an implication + (`all P x => all Q x`), use `!allP` — otherwise the subsequent + `=> H j Hj` fails with "nothing to introduce" because the conclusion + is still wrapped in `all`. +- **`congr` vs `congr 1`.** `congr` walks down an array equality all + the way to list/element equality; `congr 1` takes one structural + step. Reach for `congr 1` when `congr` descends too far and exposes + stale `init`/`mkseq` structure. + +### Reconciling syntactically distinct constants + +When a word-type modulus (`W13.modulus`, `W8.modulus`, …) appears on +one side of a goal and its numeric literal (`8192`, `256`, …) on the +other — for instance after one subterm was lowered through a circuit +lemma while the other came from the spec — `smt()` treats them as +distinct atoms and won't bridge. Normalize explicitly: + +```easycrypt +have W13_eq : W13.modulus = 8192 by smt(W13.ge2_modulus). +rewrite W13_eq. +``` + +Same pattern for `modulus_W`, cardinalities of finite types, and other +constants that have both a symbolic and a numeric form. + +### Ring/field commutativity: use the fully-qualified path + +Bare `mulrC`/`addrC` may not resolve against a concrete ring clone's +theory. When working in a cloned ring (`Zq`, `Fq`, polynomial rings +over Zq, …), the fully-qualified name of the `ComRing`/`ZModule` lemma +usually succeeds where the short form fails: + +```easycrypt +by rewrite Zq.ComRing.mulrC. +``` + +Use `SEARCH` to find the right path: + +``` +SEARCH (_ * _) (commutative _) +``` + +## EasyCrypt language overview + +### File structure + +An EasyCrypt file typically begins with `require` and `import` +statements, followed by type, operator, and module declarations, and +then lemma statements with their proofs. + +``` +require import AllCore List. + +type key. +op n : int. +axiom gt0_n : 0 < n. + +lemma foo : 0 < n + 1. +proof. smt(gt0_n). qed. +``` + +### Proofs + +A proof is delimited by `proof.` and `qed.`. Inside, tactics are +applied sequentially to transform the goal until it is discharged. + +``` +lemma bar (x : int) : x + 0 = x. +proof. by ring. qed. +``` + +### Common tactics + +- `trivial` — solve trivial goals +- `smt` / `smt(lemmas...)` — call SMT solvers, optionally with hints +- `auto` — automatic reasoning +- `split` — split conjunctions +- `left` / `right` — choose a disjunct +- `assumption` — close goal from a hypothesis +- `apply H` — apply a hypothesis or lemma +- `rewrite H` — rewrite using an equality +- `have : P` — introduce an intermediate goal +- `elim` — elimination / induction +- `case` — case analysis +- `congr` — congruence +- `ring` / `field` — algebraic reasoning +- `proc` — unfold a procedure (program logics) +- `inline` — inline a procedure call +- `sp` / `wp` — symbolic execution (forward / backward) +- `if` — handle conditionals in programs +- `while I` — handle while loops with invariant `I` +- `rnd` — handle random sampling +- `seq N : P` — split a program at statement `N` with mid-condition `P` +- `conseq` — weaken/strengthen pre/postconditions +- `byequiv` / `byphoare` — switch between program logics +- `skip` — skip trivial program steps +- `sim` — similarity (automatic relational reasoning) +- `ecall` — external call + +### Tactic combinators + +- `by tac.` — apply `tac` and require all goals to be closed +- `tac1; tac2` — sequence +- `try tac` — try, ignore failure +- `do tac` / `do N tac` — repeat +- `[tac1 | tac2 | ...]` — apply different tactics to each subgoal +- `tac => //.` — apply `tac`, then try `trivial` on generated subgoals +- `move=> H` / `move=> /H` — introduction and views + +### Key libraries + +- `AllCore` — re-exports the core libraries (logic, integers, reals, + lists, etc.) +- `Distr` — probability distributions +- `DBool`, `DInterval`, `DList` — specific distributions +- `FSet`, `FMap` — finite sets and maps +- `SmtMap` — maps with SMT support +- `PROM` — programmable/lazy random oracles + +### Guidelines + +* Use SMT solver only in direct mode (smt() or /#) on simple goals + (arithmetic goals, pure logical goals). + +* Refrain from unfolding operator definitions unless necessary. + If you need more properties on an operator, state this property + in a dedicated lemma, but avoid unfolding definitions in higher + level proofs. diff --git a/dune b/dune index 7c8edf7096..b232abeca3 100644 --- a/dune +++ b/dune @@ -1,4 +1,4 @@ -(dirs 3rdparty src etc theories examples assets scripts) +(dirs 3rdparty src etc theories examples assets scripts doc) (install (section (site (easycrypt commands))) @@ -6,7 +6,9 @@ (install (section (site (easycrypt doc))) - (files (assets/styles/styles.css as styles.css))) + (files + (assets/styles/styles.css as styles.css) + (doc/llm/CLAUDE.md as llm-guide.md))) (install (section (bin)) diff --git a/scripts/llm/README.md b/scripts/llm/README.md new file mode 100644 index 0000000000..600add1ed9 --- /dev/null +++ b/scripts/llm/README.md @@ -0,0 +1,107 @@ +# LLM-oriented tooling for `easycrypt llm` + +This directory contains two example clients for the interactive REPL +exposed by `easycrypt llm` (see `doc/llm/CLAUDE.md` for the wire +protocol). They are layered: each can be useful independently, depending +on how your driver (human, script, or LLM agent) is structured. + +| Layer | File | Use when | +|-------|------|----------| +| Python binding | `ec_llm.py` | Writing a Python program that drives one EasyCrypt REPL. | +| Fifo daemon | `daemon.py` + `ec_send.sh` | Driving one persistent REPL from *many* short-lived shell invocations — notably LLM agents that issue one bash tool call per tactic. | + +## Why a fifo daemon? + +`easycrypt llm` is a stateful, long-running process. Python programs can +keep its stdin/stdout pipe open across commands, but many LLM-agent +front-ends (Claude Code, Codex CLI, etc.) only expose the shell via +one-shot command execution. Without a persistent intermediary, every +tactic would require re-LOADing the file prefix — minutes wasted per +step on a large project. + +The daemon opens `easycrypt llm` once, listens on a named pipe for JSON +requests, and writes JSON responses to a second named pipe. The +companion `ec_send.sh` is the shell-side client: it takes a single JSON +request, forwards it through the pipes, and prints the structured +response. Combined, they let an agent drive a persistent REPL with one +bash call per step. + +## Python binding (Layer 1) + +```python +from ec_llm import ECLLM + +with ECLLM(cwd="/path/to/project", extra_args=["-p", "Z3"]) as ec: + ok, resp = ec.load("proofs/myfile.ec", 42, nosmt=True) + print(ec.goals()) + ok, resp = ec.tactic("smt().") + print(resp) +``` + +Everything in the `easycrypt llm` protocol is exposed as a method: +`load`, `checkpoint`, `revert`, `undo`, `goals`, `goals_all`, `tactic`, +`tactic_multiline`, `search`, `quiet`, `close`. Status parsing tracks +the running uuid in `ec.uuid`. + +CLI mode provides a quick "LOAD and report" check: + +``` +python3 ec_llm.py proofs/myfile.ec 42 --cwd /path/to/project --nosmt +``` + +## Fifo daemon (Layer 2) + +Start the daemon once (most easily in the background): + +``` +# Create the fifos if needed and start the daemon +mkfifo /tmp/ec_in /tmp/ec_out 2>/dev/null || true +python3 scripts/llm/daemon.py \ + --cwd /path/to/project \ + --prover Z3 --timeout 5 & +``` + +Drive it with `ec_send.sh`: + +``` +./ec_send.sh '{"op":"load","arg":"proofs/myfile.ec","arg2":"42","nosmt":true}' +./ec_send.sh '{"op":"goals"}' +./ec_send.sh '{"op":"tactic","arg":"smt()."}' +./ec_send.sh '{"op":"checkpoint","arg":"before_split"}' +./ec_send.sh '{"op":"tactic","arg":"split."}' +./ec_send.sh '{"op":"revert","arg":"before_split"}' +``` + +For payloads with shell-hostile content (EC escapes like `/\\`), +write the JSON to a file and use `--file`: + +``` +cat > /tmp/req.json <<'EOF' +{"op":"tactic","arg":"rewrite /wpoly_srng !allP => H j Hj; smt(hint)."} +EOF +./ec_send.sh --file /tmp/req.json +``` + +## Operational tips + +- **Per-session setup.** Create fifos once per session. The daemon keeps + them; don't delete them while it's running. +- **Recovering from a dead daemon.** If the EasyCrypt process crashes + (stack overflow, OOM on SMT), `ec_send.sh` will hang. Kill the daemon + process, recreate the fifos (`rm -f /tmp/ec_in /tmp/ec_out; mkfifo + /tmp/ec_in /tmp/ec_out`), and restart. +- **Fast SMT feedback.** Pass `--timeout 1 --prover Z3` to the daemon + during exploration; fragile SMT calls surface immediately. Raise the + timeout when codifying a final proof. +- **Parallel sessions.** To run multiple daemons side-by-side, give each + a distinct pair of fifo paths and set `EC_IN_FIFO` / `EC_OUT_FIFO` + for the `ec_send.sh` caller. +- **Logging.** Exceptions inside the daemon are written to `/tmp/ec_daemon.log` + (or `--log`). Check there first if a request seems silently dropped. + +## Security note + +The daemon trusts whatever shows up on its input fifo — it forwards the +`arg` payload straight to EasyCrypt as tactic text. Don't expose the +fifos on a shared filesystem, and don't run the daemon as a privileged +user. diff --git a/scripts/llm/daemon.py b/scripts/llm/daemon.py new file mode 100755 index 0000000000..16a681dba0 --- /dev/null +++ b/scripts/llm/daemon.py @@ -0,0 +1,142 @@ +#!/usr/bin/env python3 +""" +Fifo-backed daemon exposing one persistent `easycrypt llm` instance to many +shell callers. Typical use case: an LLM agent (Claude Code, etc.) that +invokes a bash tool *once per tactic* — the agent can't hold stdin/stdout +open across turns, so without a daemon every tactic would re-LOAD the +whole file prefix. + +Protocol (matches the JSON line format produced by `ec_send.sh`): + + request (one line on stdin-fifo): + {"op": "", "arg": "...", "arg2": "...", "nosmt": bool} + + response (one line on stdout-fifo): + {"ok": bool, "uuid": N, "resp": "..."} + +Supported ops: + load arg=path, arg2=line (string or int), optional nosmt: bool + tactic arg="proc." + tactic_multiline arg="" (wraps in /) + undo + revert arg="" + checkpoint arg="" + goals + goals_all + search arg="" + quiet arg="on"|"off" + close + +Usage: + # start daemon (in background) + python3 scripts/llm/daemon.py --cwd /path/to/project \\ + --in-fifo /tmp/ec_in --out-fifo /tmp/ec_out & + + # then drive with scripts/llm/ec_send.sh (see that file for details) + +The fifos are created if they don't exist. Only one connected writer and +one connected reader are expected at a time — the client (`ec_send.sh`) +enforces this by opening them sequentially. +""" + +import argparse +import json +import os +import sys +import traceback + +HERE = os.path.dirname(os.path.abspath(__file__)) +sys.path.insert(0, HERE) +from ec_llm import ECLLM # noqa: E402 + + +def _ensure_fifo(path): + if not os.path.exists(path): + os.mkfifo(path) + elif not os.path.exists(path): # raced out; recreate + os.mkfifo(path) + + +def _handle(req, ec): + op = req.get("op") + arg = req.get("arg", "") + arg2 = req.get("arg2", "") + + if op == "load": + ok, resp = ec.load(arg, int(arg2), nosmt=bool(req.get("nosmt", False))) + elif op == "tactic": + ok, resp = ec.tactic(arg) + elif op == "tactic_multiline": + ok, resp = ec.tactic_multiline(arg) + elif op == "undo": + ok, resp = ec.undo() + elif op == "revert": + ok, resp = ec.revert(arg) + elif op == "checkpoint": + ok, resp = ec.checkpoint(arg) + elif op == "goals": + resp, ok = ec.goals(), True + elif op == "goals_all": + resp, ok = ec.goals_all(), True + elif op == "search": + resp, ok = ec.search(arg), True + elif op == "quiet": + ok, resp = ec.quiet(on=(arg.lower() == "on")) + elif op == "close": + ec.close() + return {"ok": True, "uuid": ec.uuid, "resp": "bye"}, True + else: + return {"ok": False, "uuid": ec.uuid, "resp": f"unknown op: {op}"}, False + + return {"ok": ok, "uuid": ec.uuid, "resp": resp}, False + + +def main(): + p = argparse.ArgumentParser(description=__doc__.splitlines()[1]) + p.add_argument("--cwd", default=None, help="Project root (default: cwd)") + p.add_argument("--in-fifo", default="/tmp/ec_in", help="Request fifo path") + p.add_argument("--out-fifo", default="/tmp/ec_out", help="Response fifo path") + p.add_argument("--log", default="/tmp/ec_daemon.log", help="Log file") + p.add_argument("--prover", default=None, help="SMT prover (e.g. Z3)") + p.add_argument("--timeout", type=int, default=None, help="Per-goal SMT timeout (s)") + args = p.parse_args() + + _ensure_fifo(args.in_fifo) + _ensure_fifo(args.out_fifo) + + extra = [] + if args.prover: + extra += ["-p", args.prover] + if args.timeout is not None: + extra += ["-timeout", str(args.timeout)] + + ec = ECLLM(cwd=args.cwd, extra_args=extra) + with open(args.log, "w") as lf: + lf.write(f"EC started. uuid={ec.uuid}\n") + + while True: + try: + # Opening a fifo for reading blocks until a writer opens it. + with open(args.in_fifo, "r") as fi: + line = fi.readline() + if not line.strip(): + continue + req = json.loads(line) + result, should_exit = _handle(req, ec) + with open(args.out_fifo, "w") as fo: + fo.write(json.dumps(result) + "\n") + if should_exit: + break + except Exception: + with open(args.log, "a") as lf: + lf.write("EXCEPTION: " + traceback.format_exc() + "\n") + try: + with open(args.out_fifo, "w") as fo: + fo.write(json.dumps({"ok": False, "uuid": -1, + "resp": traceback.format_exc()}) + "\n") + except Exception: + pass + + +if __name__ == "__main__": + main() diff --git a/scripts/llm/ec_llm.py b/scripts/llm/ec_llm.py new file mode 100644 index 0000000000..09f34fba3b --- /dev/null +++ b/scripts/llm/ec_llm.py @@ -0,0 +1,205 @@ +""" +Python binding for the `easycrypt llm` interactive REPL. + +Usage: + from ec_llm import ECLLM + + ec = ECLLM(cwd="path/to/project") # start REPL in project dir, wait for READY + ec.load("proofs/foo.ec", 42) # load through line 42 + ec.load("proofs/foo.ec", 100, nosmt=True) # fast prefix load, skip SMT + ec.checkpoint("c0") # name current state + ec.goals() # first subgoal + remaining count + ec.goals_all() # all subgoals + ec.tactic("apply H.") # send one tactic (must end with '.') + ec.revert("c0") # instant jump back to saved state + ec.search("(fdom _)") # pattern-based lemma search + ec.close() + +Protocol (from `doc/llm/CLAUDE.md`): + - Each response ends with a line containing only ``. + - `OK [uuid:N] ... ` — success, uuid incremented. + - `ERROR [uuid:N] ... ` — failure, uuid unchanged. + +Run EasyCrypt from a directory that contains (or is under) a valid +`easycrypt.project`, otherwise `LOAD` will not resolve library paths. +""" + +import os +import re +import subprocess + + +class ECLLM: + """Thin Python wrapper around one `easycrypt llm` process.""" + + def __init__(self, cwd=None, extra_args=None, exe="easycrypt"): + """ + Start an `easycrypt llm` subprocess and block until READY. + + Args: + cwd: Working directory (should contain / be under easycrypt.project). + Defaults to os.getcwd(). + extra_args: Extra CLI flags passed to `easycrypt llm`, e.g. + `["-p", "Z3", "-timeout", "5"]`. + exe: Name or path of the EasyCrypt binary (default: `easycrypt`). + """ + if cwd is None: + cwd = os.getcwd() + args = [exe, "llm"] + if extra_args: + args.extend(extra_args) + self.proc = subprocess.Popen( + args, + stdin=subprocess.PIPE, + stdout=subprocess.PIPE, + stderr=subprocess.STDOUT, + text=True, + bufsize=1, + cwd=cwd, + ) + self.uuid = 0 + banner = self._read_until_end() + if "READY" not in banner: + raise RuntimeError(f"Expected READY, got:\n{banner}") + + # ------------------------------------------------------------------ protocol + + def _read_until_end(self): + """Read lines until a line that is exactly `` (stripped).""" + lines = [] + for raw in self.proc.stdout: + line = raw.rstrip("\n") + if line.strip() == "": + break + lines.append(line) + return "\n".join(lines) + + def _send(self, command): + """Send one command line and return the full response body.""" + self.proc.stdin.write(command + "\n") + self.proc.stdin.flush() + return self._read_until_end() + + def _parse_status(self, response): + """Update self.uuid and return True on OK, False on ERROR. + + LOAD responses may include theory/axiom dumps before the status + line, so we search the entire response. + """ + m_ok = re.search(r'^OK\s+\[uuid:(\d+)\]', response, re.MULTILINE) + m_err = re.search(r'^ERROR\s+\[uuid:(\d+)\]', response, re.MULTILINE) + if m_ok: + self.uuid = int(m_ok.group(1)) + return True + if m_err: + return False + # Fallback: tolerate early-banner responses + return response.lstrip().upper().startswith("OK") + + # ------------------------------------------------------------------ commands + + def load(self, path, line, nosmt=False): + """LOAD `path` through `line`. Returns `(ok, response)`.""" + cmd = f'LOAD "{path}" {line}' + if nosmt: + cmd += " -nosmt" + resp = self._send(cmd) + return self._parse_status(resp), resp + + def checkpoint(self, name): + """Save the current uuid under `name` for later REVERT.""" + resp = self._send(f"CHECKPOINT {name}") + return self._parse_status(resp), resp + + def revert(self, name_or_uuid): + """Jump back to a named checkpoint or a uuid.""" + resp = self._send(f"REVERT {name_or_uuid}") + return self._parse_status(resp), resp + + def undo(self): + """Undo the last successful step.""" + resp = self._send("UNDO") + return self._parse_status(resp), resp + + def goals(self): + """Return the first subgoal + remaining count.""" + return self._send("GOALS") + + def goals_all(self): + """Return all open subgoals.""" + return self._send("GOALS ALL") + + def tactic(self, tac): + """Send one EasyCrypt statement (must end with `.`). Returns `(ok, response)`.""" + resp = self._send(tac) + return self._parse_status(resp), resp + + def tactic_multiline(self, body): + """Send a multi-line EasyCrypt block delimited by ``/``.""" + payload = "\n" + body.rstrip() + "\n" + resp = self._send(payload) + return self._parse_status(resp), resp + + def search(self, pattern): + """Run `SEARCH pattern` — pattern syntax per the EasyCrypt manual.""" + return self._send(f"SEARCH {pattern}") + + def quiet(self, on=True): + """Turn automatic goal display after each tactic on/off.""" + resp = self._send("QUIET ON" if on else "QUIET OFF") + return self._parse_status(resp), resp + + def close(self): + """Terminate the subprocess (sends QUIT, then waits).""" + try: + self.proc.stdin.write("QUIT\n") + self.proc.stdin.flush() + self.proc.stdin.close() + except (BrokenPipeError, ValueError): + pass + try: + self.proc.wait(timeout=5) + except subprocess.TimeoutExpired: + self.proc.kill() + + # Context manager support + def __enter__(self): + return self + + def __exit__(self, exc_type, exc, tb): + self.close() + + +# -------------------------------------------------------------------------- CLI + +def _main(): + import argparse + p = argparse.ArgumentParser( + description="Quick LOAD check: compile a file through a line and report status." + ) + p.add_argument("file", help="EasyCrypt source file (relative to --cwd)") + p.add_argument("line", type=int, help="Line number to load through") + p.add_argument("--cwd", default=None, help="Project root (default: cwd)") + p.add_argument("--nosmt", action="store_true", help="Skip SMT during LOAD") + p.add_argument("--timeout", type=int, default=None, help="Per-goal SMT timeout (s)") + p.add_argument("--prover", default=None, help="SMT prover (e.g. Z3)") + p.add_argument("--quiet", action="store_true", help="Suppress response body") + args = p.parse_args() + + extra = [] + if args.prover: + extra += ["-p", args.prover] + if args.timeout is not None: + extra += ["-timeout", str(args.timeout)] + + with ECLLM(cwd=args.cwd, extra_args=extra) as ec: + ok, resp = ec.load(args.file, args.line, nosmt=args.nosmt) + status = "OK" if ok else "ERROR" + print(f"{status} uuid={ec.uuid}") + if not args.quiet: + print(resp) + raise SystemExit(0 if ok else 1) + + +if __name__ == "__main__": + _main() diff --git a/scripts/llm/ec_send.sh b/scripts/llm/ec_send.sh new file mode 100755 index 0000000000..3daefb2dfd --- /dev/null +++ b/scripts/llm/ec_send.sh @@ -0,0 +1,36 @@ +#!/bin/bash +# Send one JSON request to the EasyCrypt LLM daemon, print the response. +# +# Usage: +# ec_send.sh '{"op":"tactic","arg":"proc."}' # inline JSON +# ec_send.sh --file /path/to/request.json # JSON from file +# +# The --file form is useful for tactic payloads containing shell-meta +# characters (e.g. EC escapes like /\\) that would otherwise need +# elaborate quoting. +# +# Fifo paths default to /tmp/ec_in, /tmp/ec_out and can be overridden via +# env vars EC_IN_FIFO, EC_OUT_FIFO. The daemon must already be running +# and listening on the same fifos. +set -eu + +IN_FIFO="${EC_IN_FIFO:-/tmp/ec_in}" +OUT_FIFO="${EC_OUT_FIFO:-/tmp/ec_out}" + +if [ "${1:-}" = "--file" ]; then + REQ=$(cat "$2") +else + REQ="$1" +fi + +# Write in background so we can read the response; fifos block until both +# ends are connected. +printf '%s\n' "$REQ" > "$IN_FIFO" & +WRITER=$! +RESP=$(cat "$OUT_FIFO") +wait "$WRITER" + +python3 -c "import sys, json +r = json.loads(sys.argv[1]) +print('OK' if r['ok'] else 'ERR', 'uuid=', r['uuid']) +print(r['resp'])" "$RESP" diff --git a/src/ec.ml b/src/ec.ml index 627d25b81b..92ea759483 100644 --- a/src/ec.ml +++ b/src/ec.ml @@ -404,6 +404,469 @@ let main () = (* Register user messages printers *) begin let open EcUserMessages in register () end; + (* -------------------------------------------------------------------- *) + (* LLM interactive mode *) + (* -------------------------------------------------------------------- *) + + let llm_guide_path () = + let (module Sites) = EcRelocate.sites in + match EcRelocate.sourceroot with + | Some root -> + Filename.concat (Filename.concat root "doc/llm") "CLAUDE.md" + | None -> + Filename.concat Sites.doc "llm-guide.md" + in + + let print_llm_guide () = + let path = llm_guide_path () in + try + let ic = open_in path in + begin try while true do + print_char (input_char ic) + done with End_of_file -> () end; + close_in ic + with Sys_error e -> + Printf.eprintf "cannot read LLM guide: %s\n%!" e + in + + let run_llm_repl (llmopts : llm_option) = + if llmopts.llmo_help then begin + print_llm_guide (); + exit 0 + end; + + let prvopts = llmopts.llmo_provers in + (* Initialize PRNG *) + Random.self_init (); + + (* Connect to external Why3 server if requested *) + prvopts.prvo_why3server |> oiter (fun server -> + try + Why3.Prove_client.connect_external server + with Why3.Prove_client.ConnectionError e -> + Format.eprintf + "cannot connect to Why3 server `%s': %s" server e; + exit 1); + + (* Add current directory to load path *) + (match relocdir with + | None -> EcCommands.addidir Filename.current_dir_name + | Some pwd -> EcCommands.addidir pwd); + + (* Proof engine configuration *) + let checkmode = { + EcCommands.cm_checkall = prvopts.prvo_checkall; + EcCommands.cm_timeout = odfl 3 prvopts.prvo_timeout; + EcCommands.cm_cpufactor = odfl 1 prvopts.prvo_cpufactor; + EcCommands.cm_nprovers = odfl 4 prvopts.prvo_maxjobs; + EcCommands.cm_provers = prvopts.prvo_provers; + EcCommands.cm_profile = prvopts.prvo_profile; + EcCommands.cm_iterate = prvopts.prvo_iterate; + } in + + (* Notice buffer: collects messages during command processing *) + let notices = Buffer.create 256 in + + let notifier (_ : EcGState.loglevel) (lazy msg) = + Buffer.add_string notices msg; + Buffer.add_char notices '\n' + in + + let initialized = ref false in + + let do_initialize () = + EcCommands.initialize + ~restart:!initialized ~undo:true + ~boot:ldropts.ldro_boot ~checkmode ~checkproof:true; + initialized := true; + (try + List.iter EcCommands.apply_pragma prvopts.prvo_pragmas + with EcCommands.InvalidPragma x -> + EcScope.hierror "invalid pragma: `%s'\n%!" x); + EcCommands.addnotifier notifier; + oiter (fun ppwidth -> + let gs = EcEnv.gstate (EcScope.env (EcCommands.current ())) in + EcGState.setvalue "PP:width" (`Int ppwidth) gs) + prvopts.prvo_ppwidth + in + + (* Error formatting *) + let format_error ?(src="") e = + let base = match e with + | EcScope.TopError (loc, e) -> + let msg = String.strip (EcPException.tostring e) in + if loc = EcLocation._dummy then msg + else Format.asprintf "%s: %s" (EcLocation.tostring loc) msg + | e -> + String.strip (EcPException.tostring e) + in + if src = "" then base + else Printf.sprintf "%s\nsource: %s" base src + in + + (* Output helpers *) + let goals_to_string ?(all=false) () = + let buf = Buffer.create 256 in + let fmt = Format.formatter_of_buffer buf in + EcCommands.pp_current_goal_or_noproof ~all fmt; + Format.pp_print_flush fmt (); + Buffer.contents buf + in + + let quiet = ref false in + + let checkpoints : (string, int) Hashtbl.t = Hashtbl.create 16 in + + let reply_ok ?(tag="") body = + let n = Buffer.contents notices in + Printf.printf "OK [uuid:%d]%s\n" (EcCommands.uuid ()) tag; + if n <> "" then print_string n; + if body <> "" then begin + print_string body; + let len = String.length body in + if len > 0 && body.[len - 1] <> '\n' then + print_char '\n' + end; + Printf.printf "\n%!"; + Buffer.clear notices + in + + let reply_ok_goals ?(all=false) () = + if !quiet then reply_ok "" + else reply_ok (goals_to_string ~all ()) + in + + let reply_error msg = + let goals = goals_to_string () in + Printf.printf "ERROR [uuid:%d]\n%s\n" (EcCommands.uuid ()) msg; + if goals <> "" then begin + print_string goals; + let len = String.length goals in + if len > 0 && goals.[len - 1] <> '\n' then + print_char '\n' + end; + Printf.printf "\n%!"; + Buffer.clear notices + in + + (* Process a single EasyCrypt command, respecting gl_fail *) + let process_action ~src (p : EP.global) = + let loc = p.EP.gl_action.EcLocation.pl_loc in + let succeeded = ref false in + begin try + ignore (EcCommands.process ~src p.EP.gl_action : float option); + succeeded := true + with + | EcCommands.Restart -> raise EcCommands.Restart + | _ when p.EP.gl_fail -> () + | e -> raise (EcScope.toperror_of_exn ~gloc:loc e) + end; + if !succeeded && p.EP.gl_fail then + raise (EcScope.toperror_of_exn ~gloc:loc + (EcScope.HiScopeError (None, + "this command is expected to fail"))) + in + + (* Process EasyCrypt input from a string (one parsed program) *) + let process_ec_input input = + Buffer.clear notices; + let reader = EcIo.from_string input in + let last_src = ref "" in + begin try + let (src, prog) = EcIo.xparse reader in + let src = String.strip src in + last_src := src; + begin match EcLocation.unloc prog with + | EP.P_Prog (commands, _) -> + List.iter (process_action ~src) commands; + reply_ok_goals () + | EP.P_Undo i -> + EcCommands.undo i; + reply_ok_goals () + | EP.P_Exit -> + EcIo.finalize reader; exit 0 + | EP.P_DocComment doc -> + EcCommands.doc_comment doc; + reply_ok "" + end + with + | EcCommands.Restart -> + do_initialize (); + reply_ok "Session restarted" + | e -> + reply_error (format_error ~src:!last_src e) + end; + EcIo.finalize reader + in + + (* Handle LOAD "file.ec" [LINE[:COL]] *) + let handle_load args = + Buffer.clear notices; + let args = String.strip args in + let last_src = ref "" in + + try + (* Parse quoted or unquoted filename *) + let filename, rest = + if String.length args > 0 && args.[0] = '"' then + let close = + try String.index_from args 1 '"' + with Not_found -> + failwith "LOAD: unterminated filename" + in + let fn = String.sub args 1 (close - 1) in + let rest = String.strip ( + String.sub args (close + 1) + (String.length args - close - 1)) in + (fn, rest) + else + match String.split_on_char ' ' args with + | [] -> failwith "LOAD: missing filename" + | [f] -> (f, "") + | f :: rest -> (f, String.concat " " rest) + in + + (* Parse optional LINE[:COL] and flags (-nosmt) *) + let upto, nosmt = + if rest = "" then (None, false) + else + let words = String.split_on_char ' ' rest in + let words = List.filter (fun s -> s <> "") words in + let nosmt = List.mem "-nosmt" words in + let words = List.filter (fun s -> s <> "-nosmt") words in + let upto = match words with + | [] -> None + | [w] -> + begin match String.split_on_char ':' w with + | [line] -> + Some (int_of_string line, None) + | [line; col] -> + Some (int_of_string line, Some (int_of_string col)) + | _ -> failwith "LOAD: invalid LINE[:COL] format" + end + | _ -> failwith "LOAD: unexpected arguments" + in + (upto, nosmt) + in + + (* Validate file extension *) + begin try + ignore (EcLoader.getkind + (Filename.extension filename) : EcLoader.kind) + with EcLoader.BadExtension ext -> + failwith (Format.sprintf + "unknown file extension: %s" ext) + end; + + (* Reset proof engine and process file *) + do_initialize (); + Hashtbl.clear checkpoints; + EcCommands.addidir (Filename.dirname filename); + + let reader = EcIo.from_file filename in + + let past_upto (loc : EcLocation.t) = + match upto with + | None -> false + | Some (line, col) -> + let (el, ec) = loc.loc_end in + el > line || (el = line && match col with + | None -> false + | Some c -> ec > c) + in + + let last_loc = ref None in + + (* In -nosmt mode, admit all SMT calls during prefix loading *) + if nosmt then EcCommands.pragma_check `WeakCheck; + + begin try while true do + let (src, prog) = EcIo.xparse reader in + let src = String.strip src in + last_src := src; + match EcLocation.unloc prog with + | EP.P_Prog (commands, locterm) -> + List.iter (fun p -> + let loc = p.EP.gl_action.EcLocation.pl_loc in + if past_upto loc then raise Exit; + process_action ~src p; + last_loc := Some loc + ) commands; + if locterm then raise Exit + | EP.P_Undo i -> + EcCommands.undo i + | EP.P_Exit -> + raise Exit + | EP.P_DocComment doc -> + EcCommands.doc_comment doc + done with + | Exit | End_of_file -> () + | e -> + EcIo.finalize reader; + if nosmt then EcCommands.pragma_check `Check; + raise e + end; + + EcIo.finalize reader; + + (* Restore full SMT checking for interactive tactics *) + if nosmt then EcCommands.pragma_check `Check; + + let tag = + match !last_loc with + | None -> "" + | Some loc -> + let (el, _) = loc.EcLocation.loc_end in + Printf.sprintf " [loaded:%s:%d]" filename el + in + reply_ok ~tag (goals_to_string ()) + + with + | EcCommands.Restart -> + do_initialize (); + Hashtbl.clear checkpoints; + reply_ok "Session restarted" + | Failure s -> + reply_error s + | e -> + reply_error (format_error ~src:!last_src e) + in + + (* Initialize proof engine *) + do_initialize (); + + (* Signal ready *) + Printf.printf "READY [uuid:%d]\n\n%!" + (EcCommands.uuid ()); + + (* Main REPL loop *) + let multi_buf = Buffer.create 256 in + let in_multi = ref false in + + begin try while true do + let line = input_line stdin in + let line = String.strip line in + + (* Multi-line input: starts, flushes *) + if line = "" then begin + Buffer.clear multi_buf; + in_multi := true + end + else if line = "" && !in_multi then begin + let input = Buffer.contents multi_buf in + Buffer.clear multi_buf; + in_multi := false; + if input <> "" then process_ec_input input + end + else if !in_multi then begin + if Buffer.length multi_buf > 0 then + Buffer.add_char multi_buf ' '; + Buffer.add_string multi_buf line + end + + else if line = "" then + () + else if line = "QUIT" then + exit 0 + else if line = "HELP" then begin + Buffer.clear notices; + let buf = Buffer.create 4096 in + let path = llm_guide_path () in + begin try + let ic = open_in path in + begin try while true do + Buffer.add_char buf (input_char ic) + done with End_of_file -> () end; + close_in ic; + reply_ok (Buffer.contents buf) + with Sys_error e -> + reply_error (Printf.sprintf "cannot read guide: %s" e) + end + end + else if line = "UNDO" then begin + Buffer.clear notices; + let uuid = EcCommands.uuid () in + if uuid > 0 then begin + EcCommands.undo (uuid - 1); + reply_ok_goals () + end else + reply_error "nothing to undo" + end + else if line = "GOALS ALL" then begin + Buffer.clear notices; + reply_ok (goals_to_string ~all:true ()) + end + else if line = "GOALS" then begin + Buffer.clear notices; + reply_ok (goals_to_string ()) + end + else if String.starts_with line "CHECKPOINT " then begin + Buffer.clear notices; + let name = String.strip ( + String.sub line 11 (String.length line - 11)) in + if name = "" then + reply_error "CHECKPOINT: missing name" + else begin + Hashtbl.replace checkpoints name (EcCommands.uuid ()); + reply_ok (Printf.sprintf + "checkpoint '%s' set at uuid %d" name (EcCommands.uuid ())) + end + end + else if String.starts_with line "REVERT " then begin + Buffer.clear notices; + let n = String.strip ( + String.sub line 7 (String.length line - 7)) in + let target = + try Some (int_of_string n) + with Failure _ -> Hashtbl.find_opt checkpoints n + in + begin match target with + | None -> + reply_error (Printf.sprintf + "REVERT: '%s' is not a valid uuid or checkpoint name" n) + | Some target -> + let uuid = EcCommands.uuid () in + if target < 0 || target > uuid then + reply_error (Printf.sprintf + "REVERT: uuid %d out of range [0, %d]" target uuid) + else begin + EcCommands.undo target; + reply_ok_goals () + end + end + end + else if line = "QUIET ON" then begin + Buffer.clear notices; + quiet := true; + reply_ok "" + end + else if line = "QUIET OFF" then begin + Buffer.clear notices; + quiet := false; + reply_ok "" + end + else if String.starts_with line "SEARCH " then begin + let query = String.strip ( + String.sub line 7 (String.length line - 7)) in + let query = + if String.ends_with query "." + then String.sub query 0 (String.length query - 1) + else query + in + process_ec_input (Printf.sprintf "search %s." query) + end + else if String.starts_with line "LOAD " then + handle_load (String.sub line 5 (String.length line - 5)) + else + (* Treat as EasyCrypt input *) + process_ec_input line + done with + | End_of_file -> () + end; + + exit 0 + in + (* Initialize I/O + interaction module *) let module State = struct type t = { @@ -415,6 +878,7 @@ let main () = (*---*) gccompact : int option; (*---*) docgen : bool; (*---*) outdirp : string option; + (*---*) upto : (int * int option) option; mutable trace : trace1 list option; } @@ -493,6 +957,7 @@ let main () = ; gccompact = None ; docgen = false ; outdirp = None + ; upto = None ; trace = None } end @@ -528,10 +993,16 @@ let main () = ; gccompact = cmpopts.cmpo_compact ; docgen = false ; outdirp = None + ; upto = None ; trace = trace0 } end + | `Llm llmopts -> + run_llm_repl + {llmopts with llmo_provers = + {llmopts.llmo_provers with prvo_iterate = true}} + | `Runtest _ -> (* Eagerly executed *) assert false @@ -572,6 +1043,7 @@ let main () = ; gccompact = None ; docgen = true ; outdirp = docopts.doco_outdirp + ; upto = None ; trace = None } end @@ -585,7 +1057,7 @@ let main () = | Some pwd -> EcCommands.addidir pwd); (* Check if the .eco is up-to-date and exit if so *) - (if not state.docgen then + (if not state.docgen && state.upto = None then oiter (fun input -> if EcCommands.check_eco input then exit 0) state.input); @@ -669,6 +1141,16 @@ let main () = if T.interactive terminal then T.notice ~immediate:true `Warning copyright terminal; + (* Check if a location is past the -upto point *) + let past_upto (loc : EcLocation.t) = + match state.upto with + | None -> false + | Some (line, col) -> + let (sl, sc) = loc.loc_start in + sl > line || (sl = line && match col with + | None -> true + | Some c -> sc >= c) in + try if T.interactive terminal then Sys.catch_break true; @@ -737,6 +1219,14 @@ let main () = List.iter (fun p -> let loc = p.EP.gl_action.EcLocation.pl_loc in + + (* -upto: if this command starts past the target, print goals and exit *) + if past_upto loc then begin + T.finalize terminal; + EcCommands.pp_current_goal_or_noproof ~all:true Format.std_formatter; + exit 0 + end; + let timed = p.EP.gl_debug = Some `Timed in let break = p.EP.gl_debug = Some `Break in let ignore_fail = ref false in diff --git a/src/ecCommands.ml b/src/ecCommands.ml index 438295196e..474eab8888 100644 --- a/src/ecCommands.ml +++ b/src/ecCommands.ml @@ -1024,6 +1024,13 @@ let pp_current_goal ?(all = false) stream = end end +(* -------------------------------------------------------------------- *) +let pp_current_goal_or_noproof ?(all = false) stream = + if Option.is_some (S.xgoal (current ())) then + pp_current_goal ~all stream + else + Format.fprintf stream "No active proof.@\n%!" + (* -------------------------------------------------------------------- *) let pp_maybe_current_goal stream = match (Pragma.get ()).pm_verbose with diff --git a/src/ecCommands.mli b/src/ecCommands.mli index a72d31a437..e411b99d6c 100644 --- a/src/ecCommands.mli +++ b/src/ecCommands.mli @@ -60,6 +60,7 @@ val doc_comment : [`Global | `Item] * string -> unit (* -------------------------------------------------------------------- *) val pp_current_goal : ?all:bool -> Format.formatter -> unit +val pp_current_goal_or_noproof : ?all:bool -> Format.formatter -> unit val pp_maybe_current_goal : Format.formatter -> unit val pp_all_goals : unit -> string list diff --git a/src/ecOptions.ml b/src/ecOptions.ml index f012e8e8d6..76db91bfe8 100644 --- a/src/ecOptions.ml +++ b/src/ecOptions.ml @@ -10,6 +10,7 @@ type command = [ | `Runtest of run_option | `Why3Config | `DocGen of doc_option + | `Llm of llm_option ] and options = { @@ -47,6 +48,11 @@ and doc_option = { doco_outdirp : string option; } +and llm_option = { + llmo_provers : prv_options; + llmo_help : bool; +} + and prv_options = { prvo_maxjobs : int option; prvo_timeout : int option; @@ -351,6 +357,11 @@ let specs = { `Spec ("trace" , `Flag , "Save all goals & messages in .eco"); `Spec ("compact", `Int , "")]); + ("llm", "LLM-friendly interactive mode", [ + `Group "loader"; + `Group "provers"; + `Spec ("help", `Flag, "Print the LLM agent guide and exit")]); + ("cli", "Run EasyCrypt top-level", [ `Group "loader"; `Group "provers"; @@ -533,6 +544,10 @@ let doc_options_of_values values input = { doco_input = input; doco_outdirp = get_string "outdir" values; } +let llm_options_of_values ini values = + { llmo_provers = prv_options_of_values ini values; + llmo_help = get_flag "help" values; } + (* -------------------------------------------------------------------- *) let parse getini argv = let (command, values, anons) = parse specs argv in @@ -604,6 +619,15 @@ let parse getini argv = raise (Arg.Bad "this command takes a single input file as argument") end + | "llm" -> + if not (List.is_empty anons) then + raise (Arg.Bad "this command does not take arguments"); + + let ini = getini None in + let cmd = `Llm (llm_options_of_values ini values) in + + (cmd, ini, true) + | _ -> assert false in { diff --git a/src/ecOptions.mli b/src/ecOptions.mli index 59009718ad..91e93fbe28 100644 --- a/src/ecOptions.mli +++ b/src/ecOptions.mli @@ -6,6 +6,7 @@ type command = [ | `Runtest of run_option | `Why3Config | `DocGen of doc_option + | `Llm of llm_option ] and options = { @@ -43,6 +44,11 @@ and doc_option = { doco_outdirp : string option; } +and llm_option = { + llmo_provers : prv_options; + llmo_help : bool; +} + and prv_options = { prvo_maxjobs : int option; prvo_timeout : int option; diff --git a/src/ecTerminal.ml b/src/ecTerminal.ml index 94f7c048e5..c5f85bc814 100644 --- a/src/ecTerminal.ml +++ b/src/ecTerminal.ml @@ -148,8 +148,9 @@ type progress = [ `Human | `Script | `Silent ] class from_channel ?(gcstats : bool = true) ?(progress : progress option) - ~(name : string) - (stream : in_channel) + ?(lastgoals : bool = false) + ~(name : string) + (stream : in_channel) : terminal = object(self) @@ -260,11 +261,11 @@ class from_channel self#_clean_progress_line (); begin match progress with | `Human -> - Format.eprintf "[%s] [%s] %s\n%!" prefix strloc msg; + Format.eprintf "[%s] [%s] %s\n%!" prefix strloc msg | `Script -> Format.eprintf "E %s %s %s\n%!" prefix strloc (String.escaped msg) | `Silent -> - () + Format.eprintf "[%s] [%s] %s\n%!" prefix strloc msg end; self#_update_progress @@ -290,6 +291,8 @@ class from_channel let msg = String.strip (EcPException.tostring e) in self#_clean_progress_line (); + if lastgoals then + EcCommands.pp_current_goal_or_noproof ~all:true Format.std_formatter; self#_notice ?subloc ~immediate:true `Critical msg; self#_update_progress; self#_clean_progress_line ~erase:false (); @@ -314,5 +317,5 @@ class from_channel Format.pp_set_margin Format.err_formatter i end -let from_channel ?gcstats ?progress ~name stream = - new from_channel ?gcstats ?progress ~name stream +let from_channel ?gcstats ?progress ?lastgoals ~name stream = + new from_channel ?gcstats ?progress ?lastgoals ~name stream diff --git a/src/ecTerminal.mli b/src/ecTerminal.mli index 0a96a56d24..faacff0e7f 100644 --- a/src/ecTerminal.mli +++ b/src/ecTerminal.mli @@ -22,6 +22,7 @@ type progress = [ `Human | `Script | `Silent ] val from_channel : ?gcstats:bool -> ?progress:progress + -> ?lastgoals:bool -> name:string -> in_channel -> terminal diff --git a/src/phl/ecPhlLoopTx.ml b/src/phl/ecPhlLoopTx.ml index 71f33072dc..b8bf396d5e 100644 --- a/src/phl/ecPhlLoopTx.ml +++ b/src/phl/ecPhlLoopTx.ml @@ -254,8 +254,8 @@ let process_unroll_for ~cfold side cpos tc = e | _ -> tc_error !!tc - "last instruction of the while loop must be \ - an \"increment\" of the loop counter" in + "last instruction of the while loop must be" + "an \"increment\" of the loop counter" in (* Apply loop increment *) let incrz = diff --git a/theories/algebra/Perms.ec b/theories/algebra/Perms.ec index 1ebc0e1d70..5423d79128 100644 --- a/theories/algebra/Perms.ec +++ b/theories/algebra/Perms.ec @@ -3,13 +3,19 @@ require import AllCore List IntDiv Binomial Ring StdOrder. (*---*) import IntID IntOrder. (* -------------------------------------------------------------------- *) -op allperms_r (n : unit list) (s : 'a list) : 'a list list = -with n = [] => [[]] -with n = x::n => flatten ( +op allperms_r (n : unit list) (s : 'a list) : 'a list list. + +axiom allperms_r0 (s : 'a list) : + allperms_r [] s = [[]]. + +axiom allperms_rS (x : unit) (n : unit list) (s : 'a list) : + allperms_r (x :: n) s = flatten ( map (fun x => map ((::) x) (allperms_r n (rem x s))) (undup s)). op allperms (s : 'a list) = allperms_r (nseq (size s) tt) s. +hint rewrite ap_r : allperms_r0 allperms_rS. + (* -------------------------------------------------------------------- *) lemma allperms_rP n (s t : 'a list) : size s = size n => (mem (allperms_r n s) t) <=> (perm_eq s t). @@ -45,7 +51,7 @@ qed. (* -------------------------------------------------------------------- *) lemma uniq_allperms_r n (s : 'a list) : uniq (allperms_r n s). proof. -elim: n s => [|? n ih] s; rewrite ?ap_r //=. +elim: n s => [|? n ih] s; rewrite ?ap_r //. apply/uniq_flatten_map/undup_uniq. by move=> x /=; apply/map_inj_in_uniq/ih => a b _ _ []. move=> x y; rewrite !mem_undup => sx sy /= /hasP[t]. @@ -73,7 +79,7 @@ require import StdBigop. lemma size_allperms_uniq_r n (s : 'a list) : size s = size n => uniq s => size (allperms_r n s) = fact (size s). proof. -elim: n s => /= [s|n ih s]. +elim: n s => /= [|? n ih] s; rewrite ?ap_r /=. by move/size_eq0=> -> /=; rewrite fact0. case: s=> [|x s]; first by rewrite addz_neq0 ?size_ge0. (pose s' := undup _)=> /=; move/addrI=> eq_sz [Nsz uqs].