EasyCrypt Circuit Based Reasoning Extension#752
Open
Gustavo2622 wants to merge 83 commits into
Open
Conversation
Gustavo2622
force-pushed
the
bdep_ecCircuitsRefactor
branch
3 times, most recently
from
1b12249 to
66efdd7
Compare
Gustavo2622
force-pushed
the
bdep_ecCircuitsRefactor
branch
from
fdefb72 to
7ec289f
Compare
Gustavo2622
force-pushed
the
bdep_ecCircuitsRefactor
branch
2 times, most recently
from
aef3a2b to
01f21ac
Compare
Gustavo2622
force-pushed
the
bdep_ecCircuitsRefactor
branch
from
58c193f to
433cbb4
Compare
Gustavo2622
force-pushed
the
bdep_ecCircuitsRefactor
branch
3 times, most recently
from
d7c187a to
f433cb0
Compare
Gustavo2622
changed the title
Gustavo2622
changed the title
Gustavo2622
force-pushed
the
bdep_ecCircuitsRefactor
branch
from
8288caf to
57a2e2b
Compare
Gustavo2622
force-pushed
the
bdep_ecCircuitsRefactor
branch
from
5b0ce21 to
d299f15
Compare
Gustavo2622
force-pushed
the
bdep_ecCircuitsRefactor
branch
from
a828b25 to
bada5a0
Compare
strub
requested changes
Jan 20, 2026
…ypt into bdep_ecCircuitsRefactor
Add two new flags for the `easycrypt` CLI to support LLM coding agents: - `-upto <pos>`: compile up to a given position and print goals there - `-lastgoals`: print the last unproven goals Also add a dedicated `llm` command mode and an LLM agent guide (doc/llm/CLAUDE.md) documenting EasyCrypt tactics and workflow for use with AI coding assistants.
Replace the batch `easycrypt llm file.ec` command with an interactive REPL (`easycrypt llm`) using a line-oriented protocol over stdin/stdout. The REPL supports: - LOAD "file.ec" [LINE[:COL]] — compile a file, optionally up to a line - UNDO / REVERT <uuid|name> — navigate proof state - GOALS / GOALS ALL — inspect current or all subgoals - CHECKPOINT <name> — named bookmarks for branching exploration - SEARCH <pattern> — lemma search - QUIET ON/OFF — suppress goal display for bulk tactic application - Direct EasyCrypt input (tactics, declarations, search, print, etc.) Responses use a typed envelope (OK/ERROR with uuid) and <END> sentinel for reliable parsing by LLM agent frameworks. Additional improvements: - LOAD reports the last processed line in the response tag - Error messages include the source tactic text - Only the current subgoal is shown by default (with remaining count) - LOAD uses loc_end for upto check (more intuitive line semantics) Update doc/llm/CLAUDE.md with the new protocol reference, interactive workflow guide, and proof strategy tips from practical usage.
New REPL features: - LOAD -nosmt: skip SMT calls during prefix compilation (uses Proofs:weak pragma), restores strict mode for interactive tactics - Error responses now include the current goal state, eliminating the need for a separate GOALS roundtrip after failures - Multi-line input support via <BEGIN>/<DONE> delimiters - HELP meta-command and -help flag: print the LLM agent guide (doc/llm/CLAUDE.md) from within the REPL or at startup The guide is installed as part of the distribution (doc site) so it stays version-matched with the binary. Agent frameworks can use `easycrypt llm -help` to populate their system prompt automatically. Documentation updates: - REVERT-to-LOAD-uuid workflow (instant restart vs recompile) - Pattern-based search syntax with examples - SMT usage guidance (pure arithmetic/logic only) - rewrite-in-H clarification
# Conflicts: # dune # src/ecEnv.ml # src/ecHiTacticals.ml # src/ecOptions.ml # src/ecPV.ml # src/ecPV.mli # src/phl/ecPhlExists.ml # src/phl/ecPhlRewrite.ml # tests/forward-call.ec
# Conflicts: # doc/llm/CLAUDE.md # src/ec.ml # src/ecDecl.ml # src/ecDecl.mli # src/ecHiGoal.ml # src/ecHiInductive.ml # src/ecOptions.ml # src/ecOptions.mli # src/ecParser.mly # src/ecScope.ml # src/ecSection.ml # src/ecSubst.ml # src/ecTheoryReplay.ml # theories/algebra/Perms.ec
Brings the editor/agent-tooling surface back in sync with origin/main: - delete LSP server (src/ecLsp.ml/.mli) and the whole vscode/ extension - revert the interactive llm REPL back to origin/main's batch llm mode (ec.ml, ecOptions.ml/.mli, doc/llm/CLAUDE.md) - drop the LSP-only deps (fmt, logs, lsp, lwt) from dune-project/src/dune Circuit/bdep features (incl. spec-relative loading via set_current_path) are untouched.
…ken) These were sentence-parsing support for the now-removed LSP server and had no remaining users. Reverts src/ecIo.ml and src/ecIo.mli to origin/main.
The 'rewrite /~' rigid-delta feature is in flight as open PR #923 ([refold]: allow rigid unification) and will be rebased onto main on its own. Drop it from this branch: - ecHiGoal.ml/.mli: reverted to origin/main (process_delta rigid logic) - ecParser.mly / ecParsetree.ml: RWDelta back to (rwoptions * pformula), dropping the rigid bool; circuit/bdep content in these files retained.
This LaTeX listings style file was dropped on the branch (incidentally, via a merge); origin/main keeps it. Restore it verbatim.
Adds a 'tyd_clinline' flag to 'tydecl', the type-level analogue of the
existing 'op_clinline'. A type cloned with an inline override ('<-' or
'<=') is tagged clinline and retains its body; when it is later used as
the target of a 'theory ... <=' override, the consumer receives that
body rather than a reference to the type (the two remain convertible —
the difference shows only when printing). The replay 'ByPath' branch now
consults 'reftyd.tyd_clinline' to choose body-vs-reference, mirroring
the operator side.
All three type override paths (BySyntax / ByPath / Direct) set
tyd_clinline = (mode <> `Alias), matching the operator side exactly.
Threads the field through ecDecl, ecHiInductive, ecScope, ecSection,
ecSubst. Adds tests/clone-type-inline.ec (expect-based).
…bdep_ecCircuitsRefactor # Conflicts: # src/ecDecl.ml # src/ecScope.ml # src/ecTheoryReplay.ml
The branch's flake changes are unrelated dev-environment churn: prover version bumps (z3, cvc5, alt-ergo, nixpkgs, ocaml), personal dev shells (emacs/proof-general, difftastic), and build-override patches. None of it concerns the circuit/bdep feature (bitwuzla is pulled via opam in dune-project, not the flake). Restore both files to match main.
- README.md: restore the 'LaTeX Formatting' section (its removal was unrelated to the circuit feature; eclistings.sty is kept). - Remove leftover backup files libs/lospecs/deps.ml.bck and deps.mli.bck. - tests/abstract_bind.ec: 'bdep solve' -> 'circuit' (the tactic was renamed; the test was stale and failed to parse).
Splits the eqobs-in machinery into a parse layer and a tactic layer:
- A new elaborated 'sim_info' record (in EcPhlEqobs) holds resolved
data (Mpv2.t equalities, ts_inv invariant, resolved codegap1
positions), distinct from the parsetree side which is renamed
'sim_info' -> 'psim_info'.
- 'process_eqobs_in{,S,F}' now only elaborate 'psim_info' -> 'sim_info'
and delegate to new tactic functions 't_eqobs_in{,S,F}' that operate
on already-elaborated data. New 'empty_sim_info' helper.
- This exposes a programmatic 't_eqobs_in cm info tc' entry point,
used by ecPhlRwEquiv and ecPhlOutline (which previously had to go
through the parser-facing path).
- ecPhlRwEquiv.t_rewrite_equiv now takes an elaborated 'codepos1'
(callers elaborate via EcTyping.trans_codepos1) instead of 'pcodepos1'.
Behaviour-preserving refactor (uses the existing ts_inv type).
… API) into bdep_ecCircuitsRefactor
# Conflicts: # src/ecTheoryReplay.ml
- ecTerminal.ml: revert err_formatter -> std_formatter (LLM-tooling residue; tooling was removed). - ecPhlLoopTx.ml: revert a botched error-message edit (a single continued string was split into two args, truncating the message). - ecLowPhlGoal.ml, ecEco.ml, ecDoc.ml, ecPhlRCond.mli: drop pure cosmetic churn (parens/whitespace/val reordering) unrelated to the circuit feature.
The ?kinds option (commit 9b6dd79 'Improve locate API') was added to let Loader.locate find .spec files, but spec-file loading was later reworked to resolve paths via Loader.current_path + Filename.concat, so ?kinds had no remaining non-default caller and no `Spec loader kind. Revert EcLoader.locate to origin/main and drop the ?kinds plumbing in EcCommands.
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
3 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Adds circuit based reasoning to EasyCrypt in the form of a module for converting EC constructs into circuits and reasoning over said circuits.
Adds various tactics to use the added functionality in proofs.
Depends on external SMT solver BitWutzla and on external circuit library Lospecs.