Skip to content

refactor(Circuit): preserve intermediate synthesis targets - #935

Merged
SamuelSchlesinger merged 2 commits into
leanprover:mainfrom
SamuelSchlesinger:samschles/circuit-synthesis
Sep 23, 2026
Merged

SamuelSchlesinger merged 2 commits into
leanprover:mainfrom
SamuelSchlesinger:samschles/circuit-synthesis

Conversation

@SamuelSchlesinger

@SamuelSchlesinger SamuelSchlesinger commented Sep 22, 2026 •

Copy link
Copy Markdown
Collaborator

Keep both target families when composing synthesis bounds, and provide trans for retaining only the final targets. Add of_mem to reuse available functions through existing synthesis combinators, infer fold arguments from their proofs, and simplify shared-output examples and Lupanov synthesis.

This is the first in a sequence of circuit-library refactors, preparing for a simpler circuit representation and a circuit-complexity API.

Keep both target families when composing synthesis bounds, and provide trans for retaining only the final targets. Add helpers for available unary and binary arguments, infer fold data from their proofs, and update shared-output examples and Lupanov synthesis.
Replace the eight membership and pair gate helpers with Synthesis.of_mem and the existing operation combinators. Preserve intermediate targets in composition and inferred fold arguments while simplifying Boolean folds and shared-output examples.

@crei crei left a comment

Copy link
Copy Markdown
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Nice improvement!

@SamuelSchlesinger
SamuelSchlesinger added this pull request to the merge queue Sep 23, 2026
Merged via the queue into leanprover:main with commit 5f50a6c Sep 23, 2026
3 checks passed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

4 participants