Speed up proof encoding using egglog's `:merge` and unboxing pairs#933

Draft

oflatt wants to merge 23 commits into

mainfrom

fd-proof-encoding

Commits on Jun 24, 2026

Proofs: add term-free MergeFnFree justification (reconstruct conclusion)

oflatt
and
claude
committed
Proofs: evolve MergeFnFree into index-carrying MergeFnIdx

oflatt
and
claude
committed
Proofs: FD pair-view for primitive-bodied custom functions (Phase A)

oflatt
and
claude
committed
Proofs: fold single-parent UF invariant into the UF index :merge

oflatt
and
claude
committed
Proofs: remove dead begin/uf-set primitives (block-merge superseded them)

oflatt
and
claude
committed
egglog-bridge: add multi-value mint-in-merge (MergeFn::Construct)

oflatt
and
claude
committed
Proofs: split MergeRow (view-row) from MergeIdx (bare body node)

oflatt
and
claude
committed
Phase B: function-bodied custom FD encoder + fix desugar-rerun term-proof linkage

oflatt
and
claude
committed
Phase C: reflexivize FD merge premises for eq-sort inputs (primitive-bodied)

oflatt
and
claude
committed
Phase C: document constructor-bodied eq-sort-input stays legacy; CHANGELOG

oflatt
and
claude
committed
Phase C: constructor-bodied eq-sort-input customs on FD via identity-column merge short-circuit

oflatt
and
claude
committed
Scope identity-column merge short-circuit to FD views via :identity-values annotation

oflatt
and
claude
committed
Remove legacy handle_merge_fn; trivial eq-sort-output merges on FD

oflatt
and
claude
committed
Merge remote-tracking branch 'origin/main' into fd-proof-encoding
oflatt
committed
Proofs: reject function-reading merges at the file-level gate (close unreachable! gap)

oflatt
and
claude
committed
Typecheck: reject reading a function inside a :merge body in ALL modes

oflatt
and
claude
committed
test: a DB-reading primitive in :merge is rejected (merges are pure writes)

oflatt
and
claude
committed
Revert CHANGELOG entries (PR should not modify the changelog)

oflatt
and
claude
committed
Tone down FD-proof documentation per review

oflatt
and
claude
committed

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Uh oh!

Speed up proof encoding using egglog's `:merge` and unboxing pairs#933

Speed up proof encoding using egglog's `:merge` and unboxing pairs#933
oflatt wants to merge 23 commits into
mainfrom
fd-proof-encoding

Commits on Jun 23, 2026

WIP: FD proof encoding — block-merge, TableInsert, multi-value bridge foundation

Multi-value bridge: generalize the merge eval to a value tuple

Multi-value front-end: transparent box/unbox for Pair-output functions

Proof encoding: pair-valued FD views with per-row congruence proofs

Commits on Jun 24, 2026

Proofs: add term-free MergeFnFree justification (reconstruct conclusion)

Proofs: evolve MergeFnFree into index-carrying MergeFnIdx

Proofs: FD pair-view for primitive-bodied custom functions (Phase A)

Proofs: fold single-parent UF invariant into the UF index :merge

Proofs: remove dead begin/uf-set primitives (block-merge superseded them)

egglog-bridge: add multi-value mint-in-merge (MergeFn::Construct)

Proofs: split MergeRow (view-row) from MergeIdx (bare body node)

Phase B: function-bodied custom FD encoder + fix desugar-rerun term-proof linkage

Phase C: reflexivize FD merge premises for eq-sort inputs (primitive-bodied)

Phase C: document constructor-bodied eq-sort-input stays legacy; CHANGELOG

Phase C: constructor-bodied eq-sort-input customs on FD via identity-column merge short-circuit

Scope identity-column merge short-circuit to FD views via :identity-values annotation

Remove legacy handle_merge_fn; trivial eq-sort-output merges on FD

Merge remote-tracking branch 'origin/main' into fd-proof-encoding

Proofs: reject function-reading merges at the file-level gate (close unreachable! gap)

Typecheck: reject reading a function inside a :merge body in ALL modes

test: a DB-reading primitive in :merge is rejected (merges are pure writes)

Revert CHANGELOG entries (PR should not modify the changelog)

Tone down FD-proof documentation per review