EasyCrypt Circuit Based Reasoning Extension#752
Open
Gustavo2622 wants to merge 98 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
# 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.
Move the alpha-invariant-keyed formula hashtable (used as circuit_of_form's memoization cache) out of ecCircuits.ml into its own EcAlphaInvHashtbl module (functor over the hypotheses context), with a .mli exposing only Htbl and clear. No behavior change; circuit tests still pass. (The hash's unhandled program-logic cases / commented-out branches are left as-is here; completing them is a follow-up.)
Rewrite the alpha-invariant formula hash: - Hash bound occurrences by the de-Bruijn *level* of their binder (a stable integer) instead of substituting a canonical ident. This drops the per-binder EcSubst.subst_form (which rebuilt the whole body at every binder) and the module-global bruijn_idents table entirely. - Bound the traversal like OCaml's Hashtbl.hash (= hash_param 10 100): fold at most 10 meaningful leaves, visit at most 100 nodes, so hashing is O(1) on arbitrarily large formulas. Bounding only coarsens the hash, which stays consistent with the is_alpha_eq key equality. - Complete the previously-asserting cases: Fmatch and Flet/LRecord are hashed fully and alpha-correctly; the memory-binding forms (FhoareS, FequivS, Fpr, ...) -- which circuit translation rejects and never caches -- get a coarse, memory-invariant per-kind hash. No behavior change observable in the test-suite (the circuit cache only keys first-order/bitvector forms); 49/50 tests/ pass, the one failure (ext_test.ec) is a pre-existing parse error unrelated to this change.
The hash is hypotheses-independent; only the key equality (is_alpha_eq) needs the context. So replace the Make(hyps) functor with a plain module whose 'a t carries the hyps and create/add/find_opt/clear take/use it. Entries are bucketed by the bounded alpha-invariant hash; within a bucket is_alpha_eq selects the key. ecCircuits uses EcAlphaInvHashtbl.create hyps / add / find_opt / clear directly. No behavior change (49/50 tests/, ext_test.ec pre-existing parse error).
Replace the boolean op_is_* predicates + re-querying dispatchers with single-lookup classifiers that return the bound-op data: - classify_baseop : env -> path -> baseop option (BBvOp | BSpec) - classify_paramop : env -> path -> paramop option (PBvOp | PArray | PBs) circuit_of_op / circuit_of_op_with_args now take the classified data, so they no longer re-query the circuit-bindings registry and no longer need the 'should be guarded by op_is_*' assert-false fallbacks. The Fop/Fapp call sites in circuit_of_form classify once. Removes the now-dead op_is_base/op_is_parametric_base, the per-family op_is_bvop/op_is_parametric_bvop/op_is_bsop/op_is_arrayop/op_has_spec/ is_of_int predicates, and the unused circuit_of_baseop/ circuit_of_parametric_baseop. Net -46 lines; no behavior change (49/50 tests/, ext_test.ec pre-existing parse error).
The 'debug : bool = false' constant (and its alias in ecCircuits) was never read anywhere -- circuit debug output goes through the engine's 'notify env `Debug' log-level mechanism, not this flag. Drop both.
Replace the four duplicated ad-hoc 'time' helpers (two ref-style in ecCircuits, two return-style in ecPhlBDep) and the scattered manual Unix.gettimeofday deltas with a single EcCircuits.stopwatch helper: 'stopwatch env' returns a 'lap msg' closure reporting the time since the previous lap. Timing is now globally toggleable via a new boolean flag 'Circuit:timing' (EcGState, wired through process_option like pp_showtvi/old_mem_restr), off by default and enabled with 'pragma +Circuit:timing.'. When off, stopwatch is a no-op; when on it emits at `Warning so it shows at the default compile verbosity. Removes the dead 'do_time' parameter (and its .mli entries) on circuit_check_posts/circuits_of_equality/circuit_simplify_equality (no caller ever disabled it) and the commented-out timing in process_instr.
Of the 33 values exported by ecCircuits.mli, only 14 are used outside the module (by ecPhlBDep / ecPhlRwPrgm). The other 19 were either pass-through re-exports of EcLowCircuits names or internal helpers needlessly exposed. Drop them from the interface (they remain available internally); also remove the now-unused 'open EcIdent'/'open EcSymbols'. No behaviour change (release + ci builds clean, circuit tests pass).
Introduce a .ocamlformat tuned to approximate the project's hand-written style: margin 80, leading-| cases, match arms not indented under match (match-indent=0 / match-indent-nested=never), no space-around-lists, exp-grouping=preserve to keep begin..end blocks, and break-fun-decl=fit-or-vertical so an over-long parameter list breaks into a vertically-aligned vbox (one parameter per line). It is globally disabled (disable=true) so the rest of the unformatted tree is left alone; .ocamlformat-enable opts in only src/ecCircuits.ml for now. Flip disable=false (and drop the enable file) for a repo-wide migration. Reformat src/ecCircuits.ml accordingly: max line length 164 -> 104 (residual lines are unbreakable strings/comments); begin..end preserved. No behaviour change (release + ci builds clean, circuit tests pass).
Warning 32 (unused value) is disabled project-wide, which had masked a set of never-used module-level bindings in this new file. Building it once with the warning enabled flagged 19 dead values; remove them: ty_of_path, width_of_type, input_of_type, temp_symbol, expand_iter_form, circuit_of_path, vars_of_memtype, compute, circ_equiv, circ_sat, circuit_to_string, circuit_ueq, circuit_has_uninitialized, circuit_to_file, circuit_slice, circuit_flatten, state_get, state_get_opt, state_get_all (mostly thin re-export shims of EcLowCircuits names that nothing consumed, plus a few genuinely-unused helpers). A second warning-32 pass confirms no further dead values remain. No behaviour change (release + ci builds clean, circuit tests pass).
The two variants reported the same failure (an operator that is neither a circuit-bound base op nor an unfoldable definition); they differed only in whether EcFol.op_kind recognized the operator. Since the operator path is always available, drop `OpK of op_kind and report `Op of path in both cases. Removes the now-dead pp_op_kind printer. No behaviour change beyond a slightly less specific message for recognized-kind operators (release + ci clean, circuit tests pass).
tests.config sections are directory-oriented (okdirs scans whole dirs); there was no way to restrict a scenario to specific files. Add a 'file_include' key (whitespace-separated fnmatch globs, mirroring 'file_exclude'): empty means include everything (backward-compatible), otherwise a gathered file is kept only if it matches at least one glob. Also drop a stray debug 'print' in is_file_excluded.
This function (added by this branch, marked 'FIXME PR: Remove?') was never called and not exported in the .mli. Removing it restores ecPhlOutline.ml to origin/main exactly. No behaviour change.
- oget: revert the 'FIXME PR: Remove before merge' backtrace dump (Printexc.get_callstack ... print_raw_backtrace) before assert false; restore the plain 'assert false' as on origin/main. - List.collapse: remove (unused; distinct from the local 'collapse' in ecLowCircuits, which is a different function and stays). - Restore a stray-deleted blank line. ecUtils.ml/.mli now add only List.chunkify (used by ecLowCircuits' lane merging). Release + ci builds clean, circuit tests pass.
The inner driver was a single ~210-line 'doit' with two very large match
arms. Rename it to 'circuit_of_node' and extract the two heavy arms as
sibling functions in the recursive group:
- circuit_of_op_form : the Fop (nullary operator) arm
- circuit_of_app : the Fapp (application) arm
- circuit_of_logic_app: the inner logical-connective dispatch
(Eq/Not/Imp/And/Or/Iff/compose) of an application
circuit_of_node's match is now a one-line-per-node dispatch table. Purely
a behaviour-preserving restructuring (no signature/.mli change, same
shared per-call caches); release + ci clean, circuit tests pass.
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.