EasyCrypt Circuit Based Reasoning Extension#752
Open
Gustavo2622 wants to merge 188 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
ecLowCircuits uses only the Bitwuzla backend [BWZ], so the interface exposes just that module (the abstract solving context and its create/equiv/sat/valid/model operations), hiding the SMTInstance/ SMTInterface signatures, the MakeSMTInterface functor and BWZInstance.
Rename the module (file circuit_spec.ml/.mli -> specifications.ml/.mli) and update its two references (the C backend's include in ecLowCircuits and EcEnv.get_specification_by_name).
The only consumer (specifications) uses just [parse], so the interface exposes that alone. [print_source_for_range] was unused; remove it (and the now-redundant [open Ptree]).
Expose the AST data model (types kept concrete, as consumers construct and pattern-match them) plus the used helpers [atype_as_aword], [get_size] and [pp_atype]. [Ident] narrows to [create]; [pp_aword] stays internal (used by [pp_atype]). The interface revealed the unused module [IdentMap] and, with it, the unused [Ident.name]/[Ident.id]; remove them.
Expose the parse-tree types concretely (the parser builds them, the typer matches them), plus [ParseError] and the used [Lc] helpers (of_positions, of_lexbuf, merge, unloc, mk, map). The interface revealed dead [Lc] helpers: remove [mergeall], [range], [pp_range] and [string_of_range].
Remove the unused int64_of_bools, pp_reg, of_int_repr_size and trunc, along with their now-orphaned private helpers (pp_reg_ + int32_of_bools, and of_bigint_repr_size). Export the unsigned/signed less-than/-equal comparisons ult/ule/slt/sle (siblings of the already-exported ugt/uge/sgt/sge).
word.ml/word.mli (fixed-width modular arithmetic via first-class modules) was referenced nowhere; delete it.
These were dropped as "dead" based on EasyCrypt-internal usage, but easycrypt.lospecs is a published library and they are used by downstream consumers (e.g. formosa-crypto/arch-specs' checkspecs). Re-expose them.
This reverts commit 2028a41.
circuit_state_of_memenv opened every program local up front and failed the whole translation if any had a non-circuit type, so a memory with an int local (e.g. a loop counter) aborted with "Missing type binding for type int". Skip such locals instead -- they are not circuit inputs -- mirroring circuit_state_of_hyps. Assigning to a non-circuit variable in the body is still rejected, as before.
This reverts commit fa75712.
`bind bitstring`'s type used `loc(simpl_type_exp)`, an applicative type expression, which was ambiguous against the following size form (two shift/reduce conflicts: the parser could not tell whether the next token extended the type via `type_args qident` or began the size). The handler already required the type to be a monomorphic named type, so accept a qualified name (`qoident`) instead -- matching `bind array`/`bind op` -- and resolve it by [EcEnv.Ty.lookup_opt]. Grammar is now conflict-free.
fillet_tauts/batch_checks/collapse_lanes carried a ?logger:(string -> unit) parameter, but no caller ever passed one (fillet_tauts even threaded its own None into collapse_lanes), so every Option.may (...) logger inside was a permanent no-op. Remove the parameters and their dead log lines. The state-level logger (set_logger/log, injected as EcEnv.notify by callers) is untouched.
The translation state carried a `logger : string -> unit` closure that callers built from `EcEnv.notify env `Debug` and injected via set_logger. Replace it with the gstate itself: - EcGState gains `notify_fmt` (the printf/buffer front-end previously inlined in EcEnv.notify); EcEnv.notify now just delegates to it. - ecLowCircuits' state stores `gstate : EcGState.gstate`; `log` calls `EcGState.notify `Debug` directly. `empty_state` becomes `create_state` taking a (mandatory) gstate; `set_logger` is removed. - Callers build the state with `create_state (EcEnv.gstate env)`; the `?st` defaults derive the gstate from the ambient env/hyps.
Its only external caller (arg_of_form in ecCircuits) already has `env` in scope, so it logs via EcEnv.notify directly. `log` is now internal to EcLowCircuits, used only by open_circ_lambda where no env is available.
CBool and CBitstring 1 were bit-for-bit identical, but kept as distinct ctype constructors, so every 1-bit consumer had to handle both -- and some didn't (e.g. circuit_ite's condition asserted false on a CBitstring 1). Remove the CBool constructor entirely; booleans are now CBitstring 1, with a soft constructor `cbool = CBitstring 1` for building them. Match `CBitstring 1` where a bool is needed. This collapses the redundant CBool/CBitstring-1 cross-cases (circuit_eq, circuit_ite, input compatibility, input unification/aggregation, get-element, fillet) into the existing CBitstring cases, and lets circuit_ite accept a 1-bit condition instead of crashing. circuit_input_compatible's now-unused ?strict parameter is dropped.
`strict` was hard-coded to `true`, making the `not strict` match arm dead code. The input match reduces to: all three operands must be input-free, else assert false. Inline it.
MakeCircuitInterfaceFromCBackend was a functor over CBackend instantiated exactly once (with LospecsBack), never exported, and immediately included at the end -- so its parameterization bought nothing. Inline the body at top level and bind `module Backend = LospecsBack` (still sealed `: CBackend`, so reg/node stay abstract -- the encapsulation is preserved). Also drop `module type CircuitInterface`, which merely duplicated the .mli. CBackend is kept (it seals LospecsBack).
lospecs already fixes its public surface via its own .mli, and ecLowCircuits is itself the abstraction layer, so sealing the backend glue behind a CBackend signature was a redundant extra layer. Remove `module type CBackend` and unseal the implementation (LospecsBack -> plain `module Backend`); its register-level helpers stay in ecLowCircuits for now. Unsealing surfaced that exception NonConstantCircuit was never raised (only a dead catch in `compute`); drop both.
Remove the Backend module: its register-level helpers move into C (alongside the lospecs includes) and its Deps submodule moves into CDeps (alongside `include Lospecs.Deps`). Module order is adjusted so C can use CSMT (equiv/sat/valid) and CDeps can use C. References `Backend.X` / `Backend.Deps.X` become `C.X` / `CDeps.X`. No behavior change.
The C module re-exported many lospecs ops under same/renamed aliases (band/bor/add/sub/input_node/circuit_from_spec, ...) that added no value over the underlying names. Drop them and inline the underlying lospecs calls at the use sites (C.input, C.add_dropc, C.circuit_of_specification, ...). Keep node_eq, a meaningful 1-bit equality alias for xnor.
reg was exposed as 'type reg = node array', letting any consumer poke or mutate the underlying array. Move its ownership into circuit.ml (where the bit-vector arithmetic legitimately needs the concrete representation) and export it abstractly: the type stays at the Circuit top level, the register operations (length/get/extract/append/concat/maps/...) live in a new Circuit.Reg submodule. aig.ml no longer defines reg or maps (maps moves to Circuit.Reg). The few consumers that handled registers structurally -- deps, smt, specifications and ecLowCircuits' C compat layer -- now go through Circuit.Reg instead of raw Array operations. The bit-vector arithmetic core is untouched.
…s' C Follow-up to the Circuit.Reg refactor: move the remaining register helpers out of ecLowCircuits' C compatibility layer into lospecs, where they belong, and drop the ones that merely re-aliased existing functions. - Aig.equal: structural node equality (was C.nodes_eq, an id comparison under a misleading name). - Circuit.node_eq / Circuit.reg_eq: bit-vector equalities (next to eq/bvueq/bvseq), moved out of C. - Circuit.Reg gains truncate, node_of_reg (asserts size 1), insert, input_of_size. - C's slice/get inline to Reg.extract/Reg.get; the custom GetOutOfRange / BadSlice exceptions are removed (call sites catch the underlying Invalid_argument); reg_ite was identical to Circuit.ite; the thin aliases (node_array_of_reg & co, applys, concat, flatten, size_of_reg, pp_node recast) are inlined at their use sites. C now holds only the zint/SMT-context wrappers and the include glue. make unit: 71/71.
The file has seen heavy churn during the Circuit.Reg refactor; bring it under the gradual ocamlformat adoption (add it to .ocamlformat-enable, mirroring ecCircuits.ml) and reformat. ocamlformat aborted on its comment-preservation check (a known bug that drops trailing comments in some positions) for the repeated '(* Should be caught by EC typechecking + binding correctness *)' notes on fall-through 'assert false' arms. Relocated those comments verbatim to a standalone line above their arm, a position ocamlformat handles; no semantic change. release + ci clean; make unit 72/72.
…nslation
- circuit is now a record { cval : cval; inputs : cinput list } instead of
the circ * cinput list tuple (the cfun alias is gone). All construction
and destructuring across ecLowCircuits/ecCircuits is updated.
- the closed-circuit-value type 'circ' is renamed 'cval' (register + ctype,
no open inputs); circ_of_zint/pp_circ -> cval_of_zint/pp_cval.
- cinp -> cinput; flatcirc dropped (the field is the lospecs reg directly);
pp_flatcirc -> pp_reg.
- BVOps and ArrayOps are exported as submodules (no longer include'd).
- circuit_of_bvop's ~25 near-identical arms factored through local
binop/cmp/unop helpers.
make unit: 72/72; release + ci clean; ocamlformat clean.
The bounded alpha-invariant hash collapsed large, structurally-similar formulas into a few buckets, so each lookup ran O(form) is_alpha_eq over long collision chains -- quadratic on big circuit-translation goals (a Keccak round spent ~352s in the form cache here). Make the hash full and memoize it on the hash-cons tag (f_tag), gated on an empty binder environment so it stays context-independent (sound). Add a physical-equality fast path in find_opt before is_alpha_eq. Lookups are now O(1) amortized; Keccak-round circuit generation drops from ~354s to ~12s.
Array [init]/lambda elements were translated by eagerly applying and fully reducing the body for every index (O(body) per element). Instead carry a pending integer substitution and force it lazily: - [arg_of_form]'s init case head-reduces the function once to expose its lambda, then each element only extends the substitution with [binder -> i] rather than substituting/reducing the whole body; - the integer substitution is forced at the leaves ([int_of_form]) and on demand: [circuit_of_node] reduces a stuck form (e.g. an index-dependent [let]) when structural conversion fails; - the [if] case resolves its condition (normalizing under the substitution) and translates only the taken branch, matching eager reduction -- translating the dead branch is unsound to attempt (it may hold an access valid only under the other condition); - the form cache is keyed by (form, substitution restricted to the form's free locals) so the same body under different indices is cached separately. Cuts the per-element reduction cost on large array specs (e.g. a Keccak round).
[destr_conj] (used to split the pre/post into atomic conjuncts) ran a full call-by-value normalization of the whole formula just to inspect its top connective. On a large equality postcondition (e.g. a Keccak-state equality) this normalized the entire spec -- then circuit_of_form re-expanded the same terms -- for ~1s of redundant work, invisible because solve_post had no stopwatch. Head-normalize only (EcReduction.h_red_opt, until head-normal): enough to expose the top /\ / all / = ; the conjuncts' interiors are left to circuit_of_form, which reduces on demand. Also add a solve_post timing lap so this phase is visible under Circuit:timing. destr_conj on the Keccak round goal: ~0.93s -> ~0s. unit suite 72/72.
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.