EasyCrypt Circuit Based Reasoning Extension#752
Open
Gustavo2622 wants to merge 167 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
f_app_safe builds the arrow type from the actual argument types and unifies it with the looked-up operator's type; for a well-typed form this cannot fail unless the construction is wrong. So catch UnificationFailure and `assert false` rather than the previous debug-eprintf-and-reraise (which also used the let () = begin ... end idiom and only re-raised the same exception).
Use EcEnv.Op.by_path f env instead of converting the path to a qsymbol and re-resolving it by name (EcEnv.Op.lookup (toqsymbol f)); the resolved path is then just f.
Replace the bespoke open_oper_ue (fresh univar per tparam, ignoring the tparam constraints) with EcUnify.UniEnv.openty, which opens the operator's type respecting its type-parameter constraints. Removes open_oper_ue and the now-unused open EcSubst.
f_app_safe now takes optional ?typarams (seeding the unification environment) and ?rty (the expected result type), and treats an unresolved unification environment (not UE.closed) as an internal error alongside a unification failure. Update the .mli signature and doc to match.
The application only needs its head exposed for the circuit translator to dispatch (and for lambdas to beta-reduce); the translator reduces the sub-terms it needs (e.g. array indices) itself. Use EcReduction.h_red_until (reduce to weak head normal form) instead of EcCallbyValue.norm_cbv.
result_ty now asserts when arguments remain but the type is not a function (more arguments than arrows), instead of silently returning the non-function type.
The module name (EcTypesafeFol) already conveys the "safe" aspect, so the suffix was redundant. f_op_app applies an operator (by path); f_app applies a function form. Update the .mli and the call sites in ecCircuits and ecPhlBDep.
A form whose type is a circuit type but which has no structural circuit translation -- a free variable, [witness], or an application of an opaque head such as [f 4] for an abstract [f : int -> W8] -- denotes an arbitrary value of that type. Model it uniformly as a fresh, form-cached input via the new [circuit_of_uninterpreted] (generalising the [witness] handling), so alpha-equal occurrences share one input while distinct terms get distinct ones. Previously such a leaf reached [Flocal _ -> state_get st idn] (or the opaque-head case of [circuit_of_app]) and raised [Not_found], surfacing as an anomaly. This left e.g. [(init f).[4] = f 4] unprovable even though it holds by the array axiom: element 4 of [init f] is [f 4], and both sides now resolve to the same cached input. The fallback is placed at the leaf, never as a [try/with] around the recursion: wrapping [circuit_of_node] would swallow a genuine error from a sub-term of a circuit-typed parent (e.g. a tuple) and mask the bug. [circuit_uninit] still raises a clean [CircError] for non-circuit types, so functions and ints fail as before. Regression tests in tests/circuit_soundness.ec: the positive lemmas guard completeness (shared inputs for alpha-equal leaves); the [fail circuit] negatives guard soundness (distinct leaves are not equated).
The SMT counter-model printed under [Circuit:debug_smt] identified each input by its raw AIG id (e.g. "input 106225 = #b11111111"), which is opaque. Carry the source-level name on [cinp] (the [`Idn]/[`Str] used to create the input, e.g. a program variable's symbol) and resolve ids to names when rendering, so the dump reads "input a = #b11111111". Name resolution stays at the display boundary in [check_with_model]: the solver and [model] keep speaking in ids (the right layer for the backend), and the two [circ_equiv] call sites build the id->name map from the compared circuits' [cinp] lists. Unmapped ids fall back to their integer.
Restrict Aig's public API to what its consumers (circuit, circuit_spec, deps, smt, ecLowCircuits) actually use: the AIG node/reg types, the gate combinators, [map]/[maps], [pp_node], [HCons.clear] and [write_aiger_bin_temp].
With the interface in place, these were unreachable (no consumer uses them and they are unused internally): the input evaluator [eval]/[evals]/ [eval0]/[env_of_regs]/[get_bit], structural equivalence [equivs], the [VarRange]/[deps_]/[deps] dependency analysis (superseded by the Deps module), the AIGER reader [load] with [u2si]/[si2u]/[InvalidWire]/ [InvalidAIG], [abc_check_equiv], [fresh], and the unused [@@deriving yojson] serializers.
[circuit_to_file] (ecLowCircuits) was exported but never called, keeping alive [reg_to_file] and, through it, the whole AIGER serialization in aig.ml. Remove the chain end to end: [circuit_to_file]/[reg_to_file] and the now-unused [UnsupportedTypeForFileOutput] error in ecLowCircuits, and [write_aiger_bin_temp]/[write_aiger_bin]/[aiger_preprocess]/ [aiger_serialize_int]/[pp_aiger_int]/[pp_aiger_and]/[AigerError] in aig.ml. aig.ml is now just the AIG core: node/reg types, gate combinators, map/maps, pp_node and HCons.
Nodes are hash-consed: a valid [node] can only come from the smart constructors, which maintain the [id]/[neg] sharing invariant. Exposing the record as [private] lets consumers read fields and pattern-match while forbidding hand-built nodes that would break that invariant. No consumer constructed nodes directly, so this is interface-only.
Restrict Deps' public API to what ecLowCircuits actually uses: the [tdeps] map type (exposed concretely, as callers manipulate it as a plain map), [reset_state], [dep]/[deps], [merge_deps] and [realign_inputs].
With the interface in place, these were unreachable (ecLowCircuits uses only dep/deps/merge_deps/realign_inputs/reset_state): the input collectors inputs_of_node/inputs_of_reg, the whole block-dependency layer (block_deps, blocks_indep, block_list_indep, split_deps, check_dep_width, tdblock_of_tdeps, compare_dep_size, compare_tdblocks, collapse_blocks) and its tdblock type, and the pretty-printers pp_dep/pp_deps/pp_bdep/pp_bdeps.
The module-level [cache] was never populated: [dep] memoizes in its own local table (which it clears after each call), so [reset_state] only ever reset an empty table. Drop the [cache] binding, [reset_state] (and its interface entry), and the now-empty [CDeps.reset_state ()] call in reset_backend_state.
Document [merge_deps] in the interface (pointwise union of bit-sets) and reformat deps.ml.
circuit_spec is the only consumer and uses just [tt_program] and [Env.empty], so the interface exposes those plus the abstract [env] type.
The only caller always passed [Env.empty]; fold that in so [tt_program] takes just the program. The interface no longer needs to expose [Env] or the [env] type.
With the interface in place, these were unreachable from [tt_program]: [Env.export], [tt_type] and [as_int_constant].
The [@@deriving yojson] serializers on the Ast/Ptree types were used only in a debug [eprintf] on circuit_spec's bitstring-length-mismatch error path. Drop that debug print, remove every [@@deriving yojson], the lospecs [pps ppx_deriving_yojson] preprocessor, and the now-unused ppx_deriving / ppx_deriving_yojson project dependencies (regenerated easycrypt.opam).
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.
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.