Proofs refactors#725

Draft

ezrosent wants to merge 37 commits intomainfrom

ezr-oflatt-refactor-proofs-4

Commits on Dec 10, 2025

move literal_to_value to bridge crate and make reverse direction

oflatt
authored and
ezrosent
committed
move termdag

oflatt
authored and
ezrosent
committed
almost ready to do swap

oflatt
authored and
ezrosent
committed
some progress

oflatt
authored and
ezrosent
committed
try to write test

oflatt
authored and
ezrosent
committed
test fails with failed to find term

oflatt
authored and
ezrosent
committed
Got tests passing
ezrosent
committed
Store rule names in rule data
ezrosent
committed
Initial plumbing -- mid debugging
ezrosent
committed
support rewrites better
ezrosent
committed
Start to relax restrictions on AssertEq in proofs
ezrosent
committed
Initial work toward getting lets+proofs working
ezrosent
committed
basic-let passing
ezrosent
committed
fail with more informative error for unbound variable
ezrosent
committed
comitting local state
ezrosent
committed
nits

oflatt
authored and
ezrosent
committed
more filtering on tests

oflatt
authored and
ezrosent
committed
Proof API work, new tests (#743)

oflatt
authored and
ezrosent
committed
Rip out old proof syntax code.
ezrosent
committed
correct SourceSyntax translation.
ezrosent
committed
fix for "unbound variable" error
ezrosent
committed
Fix i64.egg and other simple tests
ezrosent
committed
typos
ezrosent
committed
WIP
ezrosent
committed
Fix nasty saturation bug when proofs are enabled.
ezrosent
committed
add reason consistency table
ezrosent
committed
[with debug logging] flake is gone
ezrosent
committed
Cleanups
ezrosent
committed
explain the edge case
ezrosent
committed
typo
ezrosent
committed
Fix some clippy lints after rebase to main
ezrosent
committed

Commits on Dec 11, 2025

Commits on Dec 13, 2025