WIP lean egglog semantics - #57
Conversation
|
Important Review skippedDraft detected. Please check the settings in the CodeRabbit UI or the ⚙️ Run configurationConfiguration used: Organization UI Review profile: ASSERTIVE Plan: Pro Plus Run ID: You can disable this status message by setting the Use the checkbox below for a quick retry:
📝 WalkthroughWalkthroughThe pull request adds a Lean 4 Egglog formalization with executable semantics, congruence closure, merge modeling, proofs, examples, and differential-testing tooling. It also adds project configuration, documentation, and validation commands. ChangesEgglog semantics formalization
Validation and project tooling
Estimated code review effort: 5 (Critical) | ~120 minutes Possibly related PRs
Suggested reviewers: 🚥 Pre-merge checks | ✅ 4 | ❌ 1❌ Failed checks (1 inconclusive)
✅ Passed checks (4 passed)
✨ Finishing Touches📝 Generate docstrings
Thanks for using CodeRabbit! It's free for OSS, and your support helps us grow. If you like it, consider giving us a shout-out. Comment |
![coderabbitai[bot]](https://avatars.githubusercontent.com/in/347564?s=60&v=4){kind=small}
There was a problem hiding this comment.
Actionable comments posted: 22
🤖 Prompt for all review comments with AI agents
Verify each finding against current code. Fix only still-valid issues, skip the
rest with a brief reason, keep changes minimal, and validate.
Inline comments:
In `@Makefile`:
- Around line 22-23: Use LEAN_BIN_DIR consistently for differential testing:
retain the existing Makefile configuration at Makefile lines 22-23, pass
LEAN_BIN_DIR="$(LEAN_BIN_DIR)" when invoking the differential-test script at
Makefile lines 121-122, and update scripts/difftest.sh line 32 to prepend the
configured directory with a fallback to $HOME/.elan/bin. Validate the changes
using the root Makefile validation targets.
In `@scripts/difftest.sh`:
- Around line 42-47: Update the random-case handling loop in scripts/difftest.sh
to inspect timeout’s exit status instead of treating every nonzero result as
skipped: retain the cleanup and skipped counter only for status 124, and abort
or otherwise record a failure for all other statuses, including generator
errors.
In `@semantics/CHECKER.md`:
- Line 12: Set the fenced Markdown block in CHECKER.md to use the text language
identifier, changing the opening fence to ```text while preserving the
architecture diagram content.
In `@semantics/EgglogSemantics/Impl/Closure.lean`:
- Around line 36-39: Update stepAdds to find the transitivity witness by
scanning rel for pairs beginning with p.1, rather than iterating every m in
terms. Preserve the existing witness condition requiring both (p.1, m) and (m,
p.2) to belong to rel, along with the other disjuncts.
In `@semantics/EgglogSemantics/Impl/Interp.lean`:
- Around line 103-121: Hoist the existing database closure computation out of
matchQuery and avoid recomputing it inside patternHolds for every substitution.
Update patternHolds to accept the precomputed d.closureF, seed
candidate-specific closures only with pairs involving newly added terms from
d.addTerm, and reuse the precomputed closure unchanged when the evaluated term
is already in d.terms; preserve the existing expression and equality checks
while passing this closure through matchQuery.
- Around line 186-187: Unify the duplicated pointwise-congruence predicate
around Interp.lean:186-187, Merge.lean:109-110, and Closure.lean:29-32. Keep or
export Interp.congrArgs as the shared definition, remove FMDatabase.congrKeys
and reuse the shared predicate, and update congrPair to reuse it for length and
pointwise relation checks while retaining only its local f == g head check;
standardize all sites on the shared decide (q ∈ rel) comparison style.
In `@semantics/EgglogSemantics/Impl/Merge.lean`:
- Around line 195-211: Guard the `FMDatabase.fireRule` path before calling
`matchQuery d.toF`: validate that every `FnName` occurring in `r.query` resolves
under `d.sig` to `MergeSpec.union`. If any queried function is not a merge
function, fail or return no matches instead of projecting through
`FMDatabase.toF`; preserve the existing firing behavior for valid merge-only
queries.
- Around line 219-233: Add BEq support for Row by deriving BEq alongside its
existing DecidableEq instance or defining a local BEq Row instance, so the List
Row comparison in FMDatabase.settled compiles without changing settled’s
behavior.
- Around line 165-186: Update mergeOne to require r₁ and r₂ be distinct in
addition to matching function and congruent keys. In mergeRound, snapshot the
pre-state row list once and use that same list for both outer and inner folds,
rather than iterating acc'.rows, so each ordered pair of distinct pre-existing
rows is processed once.
In `@semantics/EgglogSemantics/Proofs/Eval.lean`:
- Around line 198-237: Extract the repeated Option.Rel elimination into a helper
lemma such as Option.Rel.exists_of_eq_some, taking an Option.Rel hypothesis and
an equality showing the first option is some value, then returning a witness for
the second option and the relation. Refactor evalActions_envAgree and
evalLocalActions_agree to use this helper with one obtain, while preserving
their existing none-case handling and subsequent relation-specific proof steps.
In `@semantics/EgglogSemantics/Proofs/Interp.lean`:
- Around line 441-455: In semantics/EgglogSemantics/Proofs/Interp.lean lines
441-455, replace mem_terms_foldl and mem_eqs_foldl with one
projection-generalized fold-membership lemma over element type β and proj :
FDatabase → List β, then derive both existing statements by instantiation. In
lines 559-600, introduce one auxiliary lemma using the generalized fold lemma
and apply it to the terms and eqs projections, removing the duplicated branches
while preserving execRunRules_toDatabase behavior.
In `@semantics/EgglogSemantics/Proofs/Merge.lean`:
- Around line 123-129: Rename the theorem from
MergeStep.saturated_of_allConstructors to MergeSaturated.of_allConstructors,
preserving its existing proof and statement so the namespace matches the
MergeSaturated conclusion and supports the intended dot-notation usage.
- Around line 238-241: Define the missing MCongList.symm and MCongList.trans
lemmas in the relevant semantics scope, using the existing MCong.symm and
MCong.trans constructors to transform elementwise congruence. Ensure they
provide symmetry and transitivity for MCongList db and are available to prove
MDatabase.Out.union_cong.
- Around line 204-211: Add a hypothesis to MergeStep.self_id ensuring db.rows
already contains the constructor rows generated by buildAll for both key terms
as and output terms a, then use it to prove the addRow result’s rows equal
db.rows. Keep the existing hfix and conclusion unchanged, and preserve the
current terms-closure argument for hw.rowsInTerms and hw.subtermClosed.
- Around line 134-141: Declare an `MCongList.forall₂` bridge lemma for
`MCongList db as bs`, matching the existing `CongList.forall₂` statement and
converting it to `List.Forall₂ (MCong db) as bs`. Place it with the `MCongList`
definitions or related merge congruence lemmas so `MCong.le` can use it during
mutual induction.
In `@semantics/EgglogSemantics/Spec/Match.lean`:
- Around line 79-112: Remove the empty ValidEnv, ValidSubst, and ValidQuerySubst
namespace blocks and their variable declarations in
semantics/EgglogSemantics/Spec/Match.lean (lines 79-112). Also remove the empty
CongList namespace block and duplicate variable {db : Database} declaration
inside namespace Cong in semantics/EgglogSemantics/Spec/Congruence.lean (lines
47-54); these sites require direct cleanup.
In `@semantics/EgglogSemantics/Spec/Merge.lean`:
- Around line 402-404: Generalize Expr.MEval.lookup at
semantics/EgglogSemantics/Spec/Merge.lean:402-404 to accept a selected column
from a multi-column db.Out row rather than requiring [v]; likewise generalize
RowActionStep.set at semantics/EgglogSemantics/Spec/Merge.lean:434-437 to write
an arbitrary multi-column out row through db.addRow instead of [v], preserving
the existing evaluation and row-action behavior for single-column cases.
- Around line 324-331: The literal/literal branch of Term.blt is non-exhaustive
for Lit constructors other than integers. In
semantics/EgglogSemantics/Spec/Merge.lean lines 324-331, add a catch-all
literal/literal case that provides a deterministic ordering for non-integer
literals and makes Term.blt total. In
semantics/EgglogSemantics/Proofs/Merge.lean lines 226-231, make no direct change
to Term.blt_linear; keep its existing trichotomy clause once the definition is
exhaustive.
- Around line 446-452: Update MergeStep.collide to require that every action in
the merge body satisfies RowAction.MergeLegal, preserving the documented
restriction to let, set, and union actions while running RowActionsStep. Add the
premise alongside the existing collide preconditions and use it when proving the
merge step.
In `@semantics/EgglogSemantics/Tests/Egg.lean`:
- Around line 96-101: Update Program.fnNames to deduplicate the names after
mapping Prod.fst from Program.fnArities, matching MProgram.fnNames and ensuring
each constructor name appears once in expectedSizes output.
In `@semantics/lakefile.toml`:
- Around line 6-11: Disable implicit variable creation for the semantics package
by adding autoImplicit = false in the [leanOptions] configuration alongside
relaxedAutoImplicit. Preserve the existing relaxedAutoImplicit setting and all
other Lean options.
In `@semantics/README.md`:
- Around line 9-13: Resolve the broken documentation references in
semantics/README.md by adding the linked PLAN.md and MERGE.md documents or
updating the links to existing files. Revise the lean-check guidance so
contributors have a passing command or target for the proved surface, while
keeping the 22 unproved theorems tracked separately through a distinct item or
script.
🪄 Autofix
Fix all unresolved CodeRabbit comments on this PR:
- Push a commit to this branch (recommended)
- Create a new PR with the fixes
ℹ️ Review info
⚙️ Run configuration
Configuration used: Organization UI
Review profile: ASSERTIVE
Plan: Pro Plus
Run ID: 9956ce8e-0084-4f49-9ee0-89db99ecd92a
📒 Files selected for processing (38)
.gitignore.mcp.jsonMakefilescripts/difftest.shsemantics/.gitignoresemantics/CHECKER.mdsemantics/DiffTest.leansemantics/EgglogSemantics.leansemantics/EgglogSemantics/Impl/Closure.leansemantics/EgglogSemantics/Impl/Interp.leansemantics/EgglogSemantics/Impl/Merge.leansemantics/EgglogSemantics/Proofs/Closure.leansemantics/EgglogSemantics/Proofs/Congruence.leansemantics/EgglogSemantics/Proofs/Database.leansemantics/EgglogSemantics/Proofs/Eval.leansemantics/EgglogSemantics/Proofs/Interp.leansemantics/EgglogSemantics/Proofs/Match.leansemantics/EgglogSemantics/Proofs/Merge.leansemantics/EgglogSemantics/Proofs/Scope.leansemantics/EgglogSemantics/Proofs/Step.leansemantics/EgglogSemantics/Proofs/Syntax.leansemantics/EgglogSemantics/Proofs/Term.leansemantics/EgglogSemantics/Spec/Congruence.leansemantics/EgglogSemantics/Spec/Database.leansemantics/EgglogSemantics/Spec/Eval.leansemantics/EgglogSemantics/Spec/Match.leansemantics/EgglogSemantics/Spec/Merge.leansemantics/EgglogSemantics/Spec/Scope.leansemantics/EgglogSemantics/Spec/Step.leansemantics/EgglogSemantics/Spec/Syntax.leansemantics/EgglogSemantics/Spec/Term.leansemantics/EgglogSemantics/Tests/Egg.leansemantics/EgglogSemantics/Tests/EggMerge.leansemantics/EgglogSemantics/Tests/Examples.leansemantics/README.mdsemantics/lake-manifest.jsonsemantics/lakefile.tomlsemantics/lean-toolchain
| # elan installs here by default and is not on PATH in a non-login shell. | ||
| LEAN_BIN_DIR ?= $(HOME)/.elan/bin |
There was a problem hiding this comment.
🎯 Functional Correctness | 🟡 Minor | ⚡ Quick win
Use LEAN_BIN_DIR consistently for differential testing.
The Make target does not forward LEAN_BIN_DIR, and the script hardcodes the default elan directory. This breaks custom Lean toolchain locations.
Makefile#L22-L23: retainLEAN_BIN_DIRas the configuration source.Makefile#L121-L122: invoke the script withLEAN_BIN_DIR="$(LEAN_BIN_DIR)".scripts/difftest.sh#L32-L32: useexport PATH="${LEAN_BIN_DIR:-$HOME/.elan/bin}:$PATH".
As per coding guidelines, use the root Makefile validation targets.
📍 Affects 2 files
Makefile#L22-L23(this comment)Makefile#L121-L122scripts/difftest.sh#L32-L32
🤖 Prompt for AI Agents
Verify each finding against current code. Fix only still-valid issues, skip the
rest with a brief reason, keep changes minimal, and validate.
In `@Makefile` around lines 22 - 23, Use LEAN_BIN_DIR consistently for
differential testing: retain the existing Makefile configuration at Makefile
lines 22-23, pass LEAN_BIN_DIR="$(LEAN_BIN_DIR)" when invoking the
differential-test script at Makefile lines 121-122, and update
scripts/difftest.sh line 32 to prepend the configured directory with a fallback
to $HOME/.elan/bin. Validate the changes using the root Makefile validation
targets.
Source: Coding guidelines
| skipped=0 | ||
| for ((i = 0; i < random_cases; i++)); do | ||
| if ! timeout "$per_case_timeout" "$gen" "$out" seed "$i" >/dev/null 2>&1; then | ||
| rm -f -- "$out/rand-$i".* | ||
| skipped=$((skipped + 1)) | ||
| fi |
There was a problem hiding this comment.
🎯 Functional Correctness | 🟠 Major | ⚡ Quick win
Fail on generator errors that are not timeouts.
The if ! timeout ... branch treats every nonzero exit as a skipped case. A Lean generator failure can therefore remove a failing random case and let the command exit successfully. Only exit status 124 should count as a timeout. Abort or record a failure for every other status.
Proposed fix
for ((i = 0; i < random_cases; i++)); do
- if ! timeout "$per_case_timeout" "$gen" "$out" seed "$i" >/dev/null 2>&1; then
- rm -f -- "$out/rand-$i".*
- skipped=$((skipped + 1))
+ if timeout "$per_case_timeout" "$gen" "$out" seed "$i" >/dev/null 2>&1; then
+ continue
+ fi
+ status=$?
+ if [[ $status -eq 124 ]]; then
+ rm -f -- "$out/rand-$i".*
+ skipped=$((skipped + 1))
+ else
+ echo "difftest: generator failed for seed $i (exit $status)" >&2
+ exit "$status"
fi
done🤖 Prompt for AI Agents
Verify each finding against current code. Fix only still-valid issues, skip the
rest with a brief reason, keep changes minimal, and validate.
In `@scripts/difftest.sh` around lines 42 - 47, Update the random-case handling
loop in scripts/difftest.sh to inspect timeout’s exit status instead of treating
every nonzero result as skipped: retain the cleanup and skipped counter only for
status 124, and abort or otherwise record a failure for all other statuses,
including generator errors.
| There is a **conversion** stage between the database and the checker, and it is bigger than | ||
| the checker. | ||
|
|
||
| ``` |
There was a problem hiding this comment.
📐 Maintainability & Code Quality | 🟡 Minor | ⚡ Quick win
Set a language for the fenced block.
Markdownlint reports MD040 for this fence. Use text because the block is an architecture diagram.
-```
+```text🧰 Tools
🪛 markdownlint-cli2 (0.23.2)
[warning] 12-12: Fenced code blocks should have a language specified
(MD040, fenced-code-language)
🤖 Prompt for AI Agents
Verify each finding against current code. Fix only still-valid issues, skip the
rest with a brief reason, keep changes minimal, and validate.
In `@semantics/CHECKER.md` at line 12, Set the fenced Markdown block in CHECKER.md
to use the text language identifier, changing the opening fence to ```text while
preserving the architecture diagram content.
Source: Linters/SAST tools
| def stepAdds (terms : Finset Term) (rel : Finset (Term × Term)) (p : Term × Term) : Bool := | ||
| decide (p.1 = p.2) || decide ((p.2, p.1) ∈ rel) | ||
| || decide (∃ m ∈ terms, (p.1, m) ∈ rel ∧ (m, p.2) ∈ rel) | ||
| || congrPair rel p.1 p.2 |
There was a problem hiding this comment.
🚀 Performance & Scalability | 🔵 Trivial | 💤 Low value
Scan rel instead of terms for the transitivity witness.
Line 38 searches every m ∈ terms. The invariant rel ⊆ candidates terms means any m with (p.1, m) ∈ rel is already in terms. Iterating the pairs of rel that start at p.1 is therefore equivalent and avoids a scan of the full term set for every candidate pair. This reduces one factor of |terms| from each congStep round.
🤖 Prompt for AI Agents
Verify each finding against current code. Fix only still-valid issues, skip the
rest with a brief reason, keep changes minimal, and validate.
In `@semantics/EgglogSemantics/Impl/Closure.lean` around lines 36 - 39, Update
stepAdds to find the transitivity witness by scanning rel for pairs beginning
with p.1, rather than iterating every m in terms. Preserve the existing witness
condition requiring both (p.1, m) and (m, p.2) to belong to rel, along with the
other disjuncts.
| /-- The actions egglog admits inside a `:merge` body: `let`, `set` and `union` only. | ||
| Anything else is rejected at lowering. -/ | ||
| def RowAction.MergeLegal : RowAction → Prop | ||
| | .expr _ => False | ||
| | .letBind _ _ => True | ||
| | .union _ _ => True | ||
| | .set _ _ _ => True |
There was a problem hiding this comment.
🎯 Functional Correctness | 🟠 Major | ⚡ Quick win
RowAction.MergeLegal is defined but never used.
MergeStep.collide on Lines 529-536 runs body through MDatabase.RowActionsStep with no MergeLegal premise. The doc comment on Lines 446-447 states that egglog rejects anything else at lowering. As written, the spec admits a :merge body containing .expr.
State the intent. Either add ∀ a ∈ body, a.MergeLegal as a premise of MergeStep.collide, or add a doc note that MergeLegal is stated only and not consumed, as the doc for MDatabase.NoMergeOk on Lines 566-567 does.
♻️ Proposed premise
| collide {db d : MDatabase} {f : FnName} {as bs a b vs : List Term}
{body : List RowAction} {res : List Expr} :
⟨f, as, a⟩ ∈ db.rows → ⟨f, bs, b⟩ ∈ db.rows → MCongList db as bs →
db.sig.mergeOf f = MergeSpec.merge body res →
+ (∀ act ∈ body, act.MergeLegal) →
MDatabase.RowActionsStep { db with env := mergeEnv a b } body d →🤖 Prompt for AI Agents
Verify each finding against current code. Fix only still-valid issues, skip the
rest with a brief reason, keep changes minimal, and validate.
In `@semantics/EgglogSemantics/Spec/Merge.lean` around lines 446 - 452, Update
MergeStep.collide to require that every action in the merge body satisfies
RowAction.MergeLegal, preserving the documented restriction to let, set, and
union actions while running RowActionsStep. Add the premise alongside the
existing collide preconditions and use it when proving the merge step.
| [leanOptions] | ||
| pp.unicode.fun = true # pretty-prints `fun a ↦ b` | ||
| relaxedAutoImplicit = false | ||
| weak.linter.mathlibStandardSet = true | ||
| weak.linter.style.header = false # Mathlib's copyright header is not ours to claim | ||
| maxSynthPendingDepth = 3 |
There was a problem hiding this comment.
📐 Maintainability & Code Quality | 🔵 Trivial | ⚡ Quick win
🧩 Analysis chain
🌐 Web query:
Lean 4 autoImplicit relaxedAutoImplicit default value lakefile leanOptions
💡 Result:
In Lean 4, both autoImplicit and relaxedAutoImplicit are configuration options that control how the system automatically introduces implicit parameters for unbound identifiers in declaration headers [1][2]. Both options have a default value of true [1][2]. 1. autoImplicit: When true (default), Lean automatically treats unbound local variables in declaration headers as implicit arguments [1][2]. 2. relaxedAutoImplicit: This option modifies the behavior of autoImplicit [1]. - When relaxedAutoImplicit is true (default), any atomic (non-empty) identifier is eligible to be automatically bound as an implicit parameter [1][3]. - When relaxedAutoImplicit is false (strict mode), only identifiers consisting of a single character followed by optional numeric digits, underscores, or specific suffixes are eligible [1][3][4]. You can set these options project-wide in your lakefile.lean using the leanOptions configuration field [5][6][7]. For example: package "your_project_name" where leanOptions:= #[ ⟨autoImplicit, false⟩, ⟨relaxedAutoImplicit, false⟩ ] This configuration is passed to both the Lean compiler and the Lean language server [6][7]. If you are using a lakefile.toml configuration instead, you can define them under the [leanOptions] table [8]. Note that if autoImplicit is set to false, the relaxedAutoImplicit setting has no practical effect [9].
Citations:
- 1: https://lean-lang.org/doc/reference/latest/Definitions/Headers-and-Signatures/
- 2: https://github.com/leanprover/lean4/blob/a832f398b80a5ebb820d27b9e55ec949759043ff/src/Lean/Elab/AutoBound.lean
- 3: https://github.com/leanprover/lean4/blob/3dc1a088b6d2d8eafe25a7cd7ec7b58d731bd7cc/src/Lean/Elab/AutoBound.lean
- 4: https://github.com/leanprover/lean4/blob/62eed1db4d67327ec8120be05f1a1b0847d74561/src/Lean/Elab/AutoBound.lean
- 5: https://proofassistants.stackexchange.com/questions/2189/project-wide-set-option-autoimplicit-false-in-lean-4
- 6: https://lean-lang.org/doc/reference/latest/Build-Tools-and-Distribution/Lake/
- 7: https://github.com/leanprover/lean4/blob/dc1498b5/src/lake/Lake/Config/LeanConfig.lean
- 8: https://proofassistants.stackexchange.com/questions/4952/lakefile-toml-with-more-than-one-defaulttargets
- 9: mariainesdff/mathlib4@e8110d4
🏁 Script executed:
#!/bin/bash
set -euo pipefail
echo "== repository roots and lakefile files =="
git ls-files | rg '(^|/)lakefile(\.toml|\.lean)$|(^|/)lakefile\.toml$|(^|/)lakefile\.lean$|semantic.*\.lean$' | sed -n '1,200p'
echo
echo "== semantics/lakefile.toml =="
if [ -f semantics/lakefile.toml ]; then
cat -n semantics/lakefile.toml
else
echo "semantics/lakefile.toml not found"
fi
echo
echo "== occurrences of autoImplicit / relaxedAutoImplicit in repository =="
rg -n "autoImplicit|relaxedAutoImplicit|mathlibStandardSet|leanOptions" . || true
echo
echo "== candidate Mathlib repo references =="
rg -n "Lean 4|mathlib|autoImplicit" README.md Cargo.toml semantics 2>/dev/null || trueRepository: saulshanabrook/egglog-encoding
Length of output: 2827
🏁 Script executed:
#!/bin/bash
set -euo pipefail
echo "== lockfile relevant entries =="
if [ -f semantics/lake-manifest.json ]; then
python3 - <<'PY'
import json
with open('semantics/lake-manifest.json') as f:
data=json.load(f)
for p in data:
if p.get('name') == 'mathlib':
print(json.dumps(p, indent=2))
PY
fi
echo
echo "== inspect EgglogSemantics headers for single-char bound identifiers =="
rg -n "^\s*(def|theorem|lemma|inductive|structure|class)\s+[A-Za-z_\u03B1-\u03C9]\b|^\s*(case|cases|match)\s*[A-Za-z_\u03B1-\u03C9]\b" semantics -g '*.lean' || true
echo
echo "== inspect diff around changed lakefile =="
git diff -- semantics/lakefile.toml || trueRepository: saulshanabrook/egglog-encoding
Length of output: 325
🏁 Script executed:
#!/bin/bash
set -euo pipefail
echo "== lockfile mathlib entry =="
if [ -f semantics/lake-manifest.json ]; then
python3 - <<'PY'
import json
with open('semantics/lake-manifest.json') as f:
data=json.load(f)
for item in data:
if isinstance(item, dict) and item.get('name') == 'mathlib':
print(json.dumps(item, indent=2))
break
else:
print("no mathlib project entry found")
PY
fi
echo
echo "== inspect files for simple autoImplicit-style header identifiers =="
python3 - <<'PY'
import re
from pathlib import Path
pat = re.compile(r'^\s*(def|theorem|lemma|inductive|structure|class)\s+([A-Za-z_\u03B1-\u03C9][A-Za-z0-9_]*)(?:\s+\\([^)]*)|)', re.M)
for path in Path('semantics').glob('*.lean'):
text = path.read_text(errors='ignore')
for name in re.findall(r'^\s*(def|theorem|lemma|inductive|structure|class)\s+([A-Za-z_\u03B1-\u03C9]\b)', text, flags=re.M):
print(f"{path}:{name[1]}")
PY
echo
echo "== inspect diff around changed lakefile =="
git diff -- semantics/lakefile.toml || trueRepository: saulshanabrook/egglog-encoding
Length of output: 342
Turn off autoImplicit for the semantics package.
relaxedAutoImplicit = false only narrows which identifiers are auto-bound; it still allows single-character names. Set autoImplicit = false alongside the relaxed flag so misspelled constructors or lemma names fail instead of becoming fresh implicit variables.
♻️ Proposed change
[leanOptions]
pp.unicode.fun = true # pretty-prints `fun a ↦ b`
+autoImplicit = false
relaxedAutoImplicit = false
weak.linter.mathlibStandardSet = true📝 Committable suggestion
‼️ IMPORTANT
Carefully review the code before committing. Ensure that it accurately replaces the highlighted code, contains no missing lines, and has no issues with indentation. Thoroughly test & benchmark the code to ensure it meets the requirements.
| [leanOptions] | |
| pp.unicode.fun = true # pretty-prints `fun a ↦ b` | |
| relaxedAutoImplicit = false | |
| weak.linter.mathlibStandardSet = true | |
| weak.linter.style.header = false # Mathlib's copyright header is not ours to claim | |
| maxSynthPendingDepth = 3 | |
| [leanOptions] | |
| pp.unicode.fun = true # pretty-prints `fun a ↦ b` | |
| autoImplicit = false | |
| relaxedAutoImplicit = false | |
| weak.linter.mathlibStandardSet = true | |
| weak.linter.style.header = false # Mathlib's copyright header is not ours to claim | |
| maxSynthPendingDepth = 3 |
🤖 Prompt for AI Agents
Verify each finding against current code. Fix only still-valid issues, skip the
rest with a brief reason, keep changes minimal, and validate.
In `@semantics/lakefile.toml` around lines 6 - 11, Disable implicit variable
creation for the semantics package by adding autoImplicit = false in the
[leanOptions] configuration alongside relaxedAutoImplicit. Preserve the existing
relaxedAutoImplicit setting and all other Lean options.
There was a problem hiding this comment.
Actionable comments posted: 8
Caution
Some comments are outside the diff and can’t be posted inline due to platform limitations.
⚠️ Outside diff range comments (2)
semantics/EgglogSemantics/Impl/Merge.lean (1)
66-68: 🎯 Functional Correctness | 🟠 Major | ⚡ Quick win
execExprfails when the first recorded output is multi-column, even if a single-column output exists.The pattern
| [v] :: _ => some vrequires the first element ofd.outs f tsto be single-column.Expr.MEval.lookupinsemantics/EgglogSemantics/Spec/Merge.leanLines 237-239 requires only that some congruent row records[v]. The two disagree.The case is reachable.
mergeOneon Line 101 writesvscomputed fromres, andres : List Exprhas one entry per value column, so a multi-columnMergeSpec.mergewrites a row whoseouthas length greater than one.outsreturns rows ind.rowsorder, andaddRowprepends, so a later multi-column merge row precedes an earlier single-column row.execExprthen returnsnone, the enclosing action gets stuck, and the differential test reports a mismatch that the spec does not have.Search the list for the first single-column output instead.
🐛 Proposed fix
match d.sig.mergeOf f with | .union => some (.app f ts) - | _ => match d.outs f ts with - | [v] :: _ => some v - | _ => none + | _ => (d.outs f ts).findSome? fun o => + match o with + | [v] => some v + | _ => none🤖 Prompt for AI Agents
Verify each finding against current code. Fix only still-valid issues, skip the rest with a brief reason, keep changes minimal, and validate. In `@semantics/EgglogSemantics/Impl/Merge.lean` around lines 66 - 68, Update the execExpr output lookup branch in Merge.lean to search d.outs f ts for the first row whose output is exactly single-column, rather than inspecting only the first recorded row. Return that value when found and none when no single-column output exists, preserving the existing behavior for empty or non-matching results.semantics/EgglogSemantics/Spec/Merge.lean (1)
300-309: 🗄️ Data Integrity & Integration | 🟡 Minor | ⚡ Quick win
mergeEnvsilently truncates when the two colliding rows have different column counts.
mergeEnvIdxstops at the shorter list.mergeEnv os nstherefore binds only the common prefix whenos.length ≠ ns.length. The doc on Lines 296-299 states that every column is bound.MergeStep.collidedoes not requirea.length = b.length, and no premise ties either length toFnDecl.outArity.The effect is a silent under-approximation: for a ragged pair the body's reference to a missing
oldᵢhas noMEvalderivation, so the step does not fire and the state is treated as saturated. Add the arity premise tocollide, or state the row-arity invariant inDatabase.WFand cite it here.🛡️ Proposed premise
| collide {db d : Database} {f : FnName} {as bs a b vs : List Term} {body : List Action} {res : List Expr} : ⟨f, as, a⟩ ∈ db.rows → ⟨f, bs, b⟩ ∈ db.rows → MCongList db as bs → + a.length = b.length → db.sig.mergeOf f = MergeSpec.merge body res →Run the following script to check whether any well-formedness predicate already constrains row output arity:
#!/bin/bash # Description: Look for an invariant tying Row.out length to FnDecl.outArity. set -euo pipefail rg -n -C4 'outArity' semantics rg -n -C6 'structure WF|def WF|rowsInTerms|CtorRows' semantics/EgglogSemantics/SpecAlso applies to: 364-371
🤖 Prompt for AI Agents
Verify each finding against current code. Fix only still-valid issues, skip the rest with a brief reason, keep changes minimal, and validate. In `@semantics/EgglogSemantics/Spec/Merge.lean` around lines 300 - 309, Ensure MergeStep.collide only accepts colliding rows with equal column counts, or establish and reference an existing Database.WF invariant tying each row’s output length to FnDecl.outArity. Update the collide premises and affected proofs so mergeEnv binds every column for both rows, preserving the documented all-column behavior.
♻️ Duplicate comments (1)
semantics/EgglogSemantics/Impl/Interp.lean (1)
201-203: 📐 Maintainability & Code Quality | 🔵 Trivial | ⚡ Quick winThe pointwise-congruence predicate is still duplicated.
Egglog.congrArgshere andEgglog.FDatabase.congrKeysinsemantics/EgglogSemantics/Impl/Merge.leanLines 39-40 now have identical bodies. Both files are in this cohort, so the two copies can drift while both feed row-count results. Keep one definition and call it from both sites.🤖 Prompt for AI Agents
Verify each finding against current code. Fix only still-valid issues, skip the rest with a brief reason, keep changes minimal, and validate. In `@semantics/EgglogSemantics/Impl/Interp.lean` around lines 201 - 203, The pointwise-congruence logic is duplicated between congrArgs and FDatabase.congrKeys. Retain a single shared definition, preferably congrArgs, and update FDatabase.congrKeys to call it while preserving the existing length and pairwise-membership behavior.
🤖 Prompt for all review comments with AI agents
Verify each finding against current code. Fix only still-valid issues, skip the
rest with a brief reason, keep changes minimal, and validate.
Inline comments:
In `@semantics/EgglogSemantics/Impl/Interp.lean`:
- Around line 65-72: Update addTerms to append all terms from ts to the database
in one accumulation step, then deduplicate the resulting terms and rows once
rather than folding addTerm per element. Preserve the resulting database
membership semantics used by addRow and toDatabase, including behavior for empty
lists.
In `@semantics/EgglogSemantics/Impl/Merge.lean`:
- Around line 110-115: Update FDatabase.mergeRound to snapshot d.rows before
folding, then use that fixed pre-state row list for both the outer and inner
folds. Keep mergeOne behavior unchanged, including self-pairs, while ensuring
each ordered pair is processed once and newly written rows are not revisited
within the round.
- Around line 79-91: In semantics/EgglogSemantics/Impl/Merge.lean:79-91, rename
the merge-aware action functions to execMAction and execMActions, then add
execMCmd, execMProgram, and execM so execution threads mergeRound through the
.run case. In semantics/EgglogSemantics/Proofs/Merge.lean:325-327, restate
execM_reachable using execM rather than exec so it relates the merge interpreter
to ProgramStep.
- Around line 79-91: Rename the merge-specific FDatabase functions execAction
and execActions to distinct names such as execMAction and execMActions,
including their recursive and explicit call sites. Preserve their existing
execExpr-based merge behavior and update all references in this file so they
cannot resolve to the constructor-only evaluators from Interp.lean.
- Around line 120-122: Update FDatabase.settled to compare the denotations or
member sets of mergeRound.terms, rows, and eqs with the corresponding fields in
d rather than comparing the order-sensitive lists directly; preserve the
existing settled result when the collections contain the same elements
regardless of ordering.
In `@semantics/EgglogSemantics/Proofs/Merge.lean`:
- Around line 218-225: Add a db.CtorRows hypothesis to MergeStep.self_id and use
it to establish that inserting the key and value terms adds no new rows; update
the proof to rewrite the addRow result using this constructor-row closure
alongside hfix. Follow the existing CtorRows usage in mem_rows_iff and preserve
the theorem’s conclusion.
- Around line 129-132: Replace the global hprim assumption in Expr.MEval_of_eval
with a condition restricted to function names occurring in e, and use that
condition throughout the proof. Add Expr.fnNames in Spec/Syntax.lean beside
Expr.vars using the same mutual recursion, then apply it to identify the names
referenced by the expression while preserving the theorem’s intended eval/MEval
equivalence guard.
In `@semantics/PLAN.md`:
- Around line 99-102: Update the M9 architecture references across
semantics/PLAN.md lines 99-102, semantics/PLAN.md lines 293-301, and
semantics/MERGE.md lines 803-806: describe the action-block merge form and its
result expressions in the first section, rename mcong_toM_iff to mcong_iff_cong
in the second, and state that the separate-MDatabase design was rejected or
remove that stale description in the third, consistently reflecting the unified
Database design without MDatabase.
---
Outside diff comments:
In `@semantics/EgglogSemantics/Impl/Merge.lean`:
- Around line 66-68: Update the execExpr output lookup branch in Merge.lean to
search d.outs f ts for the first row whose output is exactly single-column,
rather than inspecting only the first recorded row. Return that value when found
and none when no single-column output exists, preserving the existing behavior
for empty or non-matching results.
In `@semantics/EgglogSemantics/Spec/Merge.lean`:
- Around line 300-309: Ensure MergeStep.collide only accepts colliding rows with
equal column counts, or establish and reference an existing Database.WF
invariant tying each row’s output length to FnDecl.outArity. Update the collide
premises and affected proofs so mergeEnv binds every column for both rows,
preserving the documented all-column behavior.
---
Duplicate comments:
In `@semantics/EgglogSemantics/Impl/Interp.lean`:
- Around line 201-203: The pointwise-congruence logic is duplicated between
congrArgs and FDatabase.congrKeys. Retain a single shared definition, preferably
congrArgs, and update FDatabase.congrKeys to call it while preserving the
existing length and pairwise-membership behavior.
🪄 Autofix
Fix all unresolved CodeRabbit comments on this PR:
- Push a commit to this branch (recommended)
- Create a new PR with the fixes
ℹ️ Review info
⚙️ Run configuration
Configuration used: Organization UI
Review profile: ASSERTIVE
Plan: Pro Plus
Run ID: 332cf01f-a62b-456f-9b14-dcb456ccf124
📒 Files selected for processing (23)
semantics/DiffTest.leansemantics/EgglogSemantics.leansemantics/EgglogSemantics/Impl/Interp.leansemantics/EgglogSemantics/Impl/Merge.leansemantics/EgglogSemantics/Proofs/Database.leansemantics/EgglogSemantics/Proofs/Eval.leansemantics/EgglogSemantics/Proofs/Interp.leansemantics/EgglogSemantics/Proofs/Merge.leansemantics/EgglogSemantics/Proofs/Scope.leansemantics/EgglogSemantics/Proofs/Step.leansemantics/EgglogSemantics/Proofs/Syntax.leansemantics/EgglogSemantics/Proofs/Term.leansemantics/EgglogSemantics/Spec/Database.leansemantics/EgglogSemantics/Spec/Eval.leansemantics/EgglogSemantics/Spec/Merge.leansemantics/EgglogSemantics/Spec/Scope.leansemantics/EgglogSemantics/Spec/Syntax.leansemantics/EgglogSemantics/Spec/Term.leansemantics/EgglogSemantics/Tests/Egg.leansemantics/EgglogSemantics/Tests/Examples.leansemantics/MERGE.mdsemantics/PLAN.mdsemantics/README.md
💤 Files with no reviewable changes (1)
- semantics/EgglogSemantics.lean
| /-- `addTerm` over a list. -/ | ||
| def addTerms (ts : List Term) (d : FDatabase) : FDatabase := | ||
| ts.foldl (fun e t => e.addTerm t) d | ||
|
|
||
| /-- `(set (f as…) vs)`, computed. -/ | ||
| def addRow (f : FnName) (as vs : List Term) (d : FDatabase) : FDatabase := | ||
| let d := (d.addTerms as).addTerms vs | ||
| { d with rows := (⟨f, as, vs⟩ :: d.rows).dedup } |
There was a problem hiding this comment.
🚀 Performance & Scalability | 🔵 Trivial | ⚡ Quick win
addTerms runs one full dedup of terms and rows per element.
addTerm dedups the whole accumulated terms list and the whole accumulated rows list on every call. addTerms folds addTerm over ts, so inserting a k-element tuple performs k quadratic passes over the entire database instead of one. addRow calls addTerms twice, so a single set action pays this for every key column and every value column.
Accumulate first, then dedup once. This keeps the denotation identical, because toDatabase reads membership only.
♻️ Proposed refactor
/-- `addTerm` over a list. -/
def addTerms (ts : List Term) (d : FDatabase) : FDatabase :=
- ts.foldl (fun e t => e.addTerm t) d
+ { d with terms := (ts.flatMap Term.subtermList ++ d.terms).dedup,
+ rows := (ts.flatMap Term.ctorRowList ++ d.rows).dedup }
/-- `(set (f as…) vs)`, computed. -/
def addRow (f : FnName) (as vs : List Term) (d : FDatabase) : FDatabase :=
- let d := (d.addTerms as).addTerms vs
+ let d := d.addTerms (as ++ vs)
{ d with rows := (⟨f, as, vs⟩ :: d.rows).dedup }📝 Committable suggestion
‼️ IMPORTANT
Carefully review the code before committing. Ensure that it accurately replaces the highlighted code, contains no missing lines, and has no issues with indentation. Thoroughly test & benchmark the code to ensure it meets the requirements.
| /-- `addTerm` over a list. -/ | |
| def addTerms (ts : List Term) (d : FDatabase) : FDatabase := | |
| ts.foldl (fun e t => e.addTerm t) d | |
| /-- `(set (f as…) vs)`, computed. -/ | |
| def addRow (f : FnName) (as vs : List Term) (d : FDatabase) : FDatabase := | |
| let d := (d.addTerms as).addTerms vs | |
| { d with rows := (⟨f, as, vs⟩ :: d.rows).dedup } | |
| /-- `addTerm` over a list. -/ | |
| def addTerms (ts : List Term) (d : FDatabase) : FDatabase := | |
| { d with terms := (ts.flatMap Term.subtermList ++ d.terms).dedup, | |
| rows := (ts.flatMap Term.ctorRowList ++ d.rows).dedup } | |
| /-- `(set (f as…) vs)`, computed. -/ | |
| def addRow (f : FnName) (as vs : List Term) (d : FDatabase) : FDatabase := | |
| let d := d.addTerms (as ++ vs) | |
| { d with rows := (⟨f, as, vs⟩ :: d.rows).dedup } |
🤖 Prompt for AI Agents
Verify each finding against current code. Fix only still-valid issues, skip the
rest with a brief reason, keep changes minimal, and validate.
In `@semantics/EgglogSemantics/Impl/Interp.lean` around lines 65 - 72, Update
addTerms to append all terms from ts to the database in one accumulation step,
then deduplicate the resulting terms and rows once rather than folding addTerm
per element. Preserve the resulting database membership semantics used by addRow
and toDatabase, including behavior for empty lists.
| def FDatabase.execAction (d : FDatabase) : Action → Option FDatabase | ||
| | .expr e => (d.execExpr d.env e).map fun t => d.addTerm t | ||
| | .letBind v e => (d.execExpr d.env e).map fun t => | ||
| { d.addTerm t with env := (v, t) :: d.env } | ||
| | .union e₁ e₂ => (d.execExpr d.env e₁).bind fun t₁ => | ||
| (d.execExpr d.env e₂).map fun t₂ => d.addEq t₁ t₂ | ||
| | .set f args out => (d.execExprList d.env args).bind fun ts => | ||
| (d.execExpr d.env out).map fun v => d.addRow f ts [v] | ||
|
|
||
| /-- `MDatabase.ActionsStep`, computed. -/ | ||
| def FDatabase.execActions (d : FDatabase) : List Action → Option FDatabase | ||
| | [] => some d | ||
| | a :: as => (d.execAction a).bind fun d' => d'.execActions as |
There was a problem hiding this comment.
🗄️ Data Integrity & Integration | 🟠 Major | 🏗️ Heavy lift
The merge interpreter is incomplete and reuses the constructor-only interpreter's names. semantics/EgglogSemantics/Impl/Merge.lean builds on FDatabase and stops at the action level, reusing the short names execAction and execActions that semantics/EgglogSemantics/Impl/Interp.lean already defines on the same type. Because no merge-aware exec exists, the M9 refinement theorem can only name the constructor-only one.
semantics/EgglogSemantics/Impl/Merge.lean#L79-L91: rename the merge-aware action functions toexecMActionandexecMActions, then addexecMCmd,execMProgramandexecMthat threadmergeRoundthrough the.runcase.semantics/EgglogSemantics/Proofs/Merge.lean#L325-L327: restateexecM_reachableover the newexecMinstead ofexec, so the theorem relates the merge interpreter toProgramStep.
📍 Affects 2 files
semantics/EgglogSemantics/Impl/Merge.lean#L79-L91(this comment)semantics/EgglogSemantics/Proofs/Merge.lean#L325-L327
🤖 Prompt for AI Agents
Verify each finding against current code. Fix only still-valid issues, skip the
rest with a brief reason, keep changes minimal, and validate.
In `@semantics/EgglogSemantics/Impl/Merge.lean` around lines 79 - 91, In
semantics/EgglogSemantics/Impl/Merge.lean:79-91, rename the merge-aware action
functions to execMAction and execMActions, then add execMCmd, execMProgram, and
execM so execution threads mergeRound through the .run case. In
semantics/EgglogSemantics/Proofs/Merge.lean:325-327, restate execM_reachable
using execM rather than exec so it relates the merge interpreter to ProgramStep.
📐 Maintainability & Code Quality | 🟠 Major | ⚡ Quick win
FDatabase.execAction and execActions shadow the constructor-only functions of the same short name.
semantics/EgglogSemantics/Impl/Interp.lean Lines 139 and 149 define Egglog.execAction and Egglog.execActions on the same FDatabase type, using Expr.eval. This file defines Egglog.FDatabase.execAction and Egglog.FDatabase.execActions, using execExpr. This file imports Impl/Interp.lean, so both pairs are in scope and both typecheck at every call site.
Line 91 relies on dot notation to select the merge version. Line 99 writes FDatabase.execActions explicitly. A bare execActions d as anywhere in this file would silently select the constructor-only evaluator and skip every :merge lookup.
Give the merge versions distinct names, for example execMAction and execMActions.
🤖 Prompt for AI Agents
Verify each finding against current code. Fix only still-valid issues, skip the
rest with a brief reason, keep changes minimal, and validate.
In `@semantics/EgglogSemantics/Impl/Merge.lean` around lines 79 - 91, Rename the
merge-specific FDatabase functions execAction and execActions to distinct names
such as execMAction and execMActions, including their recursive and explicit
call sites. Preserve their existing execExpr-based merge behavior and update all
references in this file so they cannot resolve to the constructor-only
evaluators from Interp.lean.
| def FDatabase.mergeRound (d : FDatabase) : FDatabase := | ||
| d.rows.foldl (fun acc r₁ => | ||
| acc.rows.foldl (fun acc' r₂ => | ||
| match acc'.mergeOne r₁ r₂ with | ||
| | some acc'' => acc'' | ||
| | none => acc') acc) d |
There was a problem hiding this comment.
🎯 Functional Correctness | 🟡 Minor | ⚡ Quick win
The inner fold iterates acc.rows, so mergeRound is not one pass over the pre-state.
The outer fold iterates d.rows, the pre-state. The inner fold iterates acc.rows, which grows as mergeOne writes rows. A row written during an earlier outer iteration is therefore visited as r₂ in a later inner fold. The docstring on Line 105 states "every ordered pair of rows, fired once".
The self-pair concern from the earlier review no longer applies: semantics/EgglogSemantics/Spec/Merge.lean Lines 322-331 deliberately removed the a ≠ b guard, so mergeOne matching that is correct.
Snapshot the row list once and use it for both folds.
🐛 Proposed fix
def FDatabase.mergeRound (d : FDatabase) : FDatabase :=
- d.rows.foldl (fun acc r₁ =>
- acc.rows.foldl (fun acc' r₂ =>
+ let rows := d.rows
+ rows.foldl (fun acc r₁ =>
+ rows.foldl (fun acc' r₂ =>
match acc'.mergeOne r₁ r₂ with
| some acc'' => acc''
| none => acc') acc) d🤖 Prompt for AI Agents
Verify each finding against current code. Fix only still-valid issues, skip the
rest with a brief reason, keep changes minimal, and validate.
In `@semantics/EgglogSemantics/Impl/Merge.lean` around lines 110 - 115, Update
FDatabase.mergeRound to snapshot d.rows before folding, then use that fixed
pre-state row list for both the outer and inner folds. Keep mergeOne behavior
unchanged, including self-pairs, while ensuring each ordered pair is processed
once and newly written rows are not revisited within the round.
| def FDatabase.settled (d : FDatabase) : Bool := | ||
| let e := d.mergeRound | ||
| e.terms == d.terms && e.rows == d.rows && e.eqs == d.eqs |
There was a problem hiding this comment.
🎯 Functional Correctness | 🟠 Major | ⚡ Quick win
settled compares lists, so a merge that only reorders rows never reports saturation.
terms, rows and eqs are Lists whose denotation under FDatabase.toDatabase is set membership. settled compares them with ==, which is order-sensitive.
mergeOne writes through addRow, which prepends ⟨f, args, vs⟩ and then calls List.dedup. dedup keeps the first occurrence, so re-deriving a row that is already present moves it to the head. The member set is unchanged and the list is not. settled returns false.
This breaks exactly the case the spec depends on. semantics/EgglogSemantics/Spec/Merge.lean Lines 322-331 and MergeSaturated on Line 395 rely on an idempotent merge re-deriving a present row so that db' = db. MergeStep.self_id in semantics/EgglogSemantics/Proofs/Merge.lean Lines 218-225 states the same fixpoint. The interpreter's decision procedure disagrees, so mergeSaturate has no accessibility witness for the union-find merge that motivates the design.
Compare denotations, not list structure.
🐛 Proposed fix
def FDatabase.settled (d : FDatabase) : Bool :=
let e := d.mergeRound
- e.terms == d.terms && e.rows == d.rows && e.eqs == d.eqs
+ e.terms.toFinset == d.terms.toFinset && e.rows.toFinset == d.rows.toFinset &&
+ e.eqs.toFinset == d.eqs.toFinset🤖 Prompt for AI Agents
Verify each finding against current code. Fix only still-valid issues, skip the
rest with a brief reason, keep changes minimal, and validate.
In `@semantics/EgglogSemantics/Impl/Merge.lean` around lines 120 - 122, Update
FDatabase.settled to compare the denotations or member sets of mergeRound.terms,
rows, and eqs with the corresponding fields in d rather than comparing the
order-sensitive lists directly; preserve the existing settled result when the
collections contain the same elements regardless of ordering.
| theorem Expr.MEval_of_eval {db : Database} (hsig : db.sig.AllConstructors) {σ : Env} | ||
| {e : Expr} {t : Term} (hprim : ∀ f, Prim.ofName f = none) (h : e.eval σ = some t) : | ||
| Expr.MEval db σ e t := by | ||
| sorry |
There was a problem hiding this comment.
🎯 Functional Correctness | 🟠 Major | ⚡ Quick win
Expr.MEval_of_eval is vacuous: hprim is unsatisfiable.
hprim : ∀ f, Prim.ofName f = none claims no name resolves to a primitive. Prim.ofName in semantics/EgglogSemantics/Spec/Merge.lean Lines 192-195 maps "ordering-min" to some .orderingMin. So hprim is false, and the theorem holds for the empty set of instances.
The doc on Lines 125-128 states this theorem is the guard against Expr.eval and Expr.MEval drifting apart. As stated it guards nothing, and the sorry can be closed by deriving a contradiction from hprim.
Restrict the condition to the function names that occur in e.
🐛 Proposed statement
theorem Expr.MEval_of_eval {db : Database} (hsig : db.sig.AllConstructors) {σ : Env}
- {e : Expr} {t : Term} (hprim : ∀ f, Prim.ofName f = none) (h : e.eval σ = some t) :
+ {e : Expr} {t : Term} (hprim : ∀ f ∈ e.fnNames, Prim.ofName f = none)
+ (h : e.eval σ = some t) :
Expr.MEval db σ e t := byExpr.fnNames does not exist yet. Add it to semantics/EgglogSemantics/Spec/Syntax.lean beside Expr.vars, by the same mutual recursion.
🤖 Prompt for AI Agents
Verify each finding against current code. Fix only still-valid issues, skip the
rest with a brief reason, keep changes minimal, and validate.
In `@semantics/EgglogSemantics/Proofs/Merge.lean` around lines 129 - 132, Replace
the global hprim assumption in Expr.MEval_of_eval with a condition restricted to
function names occurring in e, and use that condition throughout the proof. Add
Expr.fnNames in Spec/Syntax.lean beside Expr.vars using the same mutual
recursion, then apply it to identify the names referenced by the expression
while preserving the theorem’s intended eval/MEval equivalence guard.
| A `Cmd.decl` case and a `Signature` (`FnName → Option FnDecl`, `FnDecl` carrying | ||
| arity and a `MergeSpec` of `.union | .merge Expr | .noMerge`) go in **from day | ||
| one**, with Phase 1 theorems carrying an `AllConstructors sig` hypothesis. This is | ||
| what keeps the `:merge` extension from churning the AST. |
There was a problem hiding this comment.
📐 Maintainability & Code Quality | 🟡 Minor | ⚡ Quick win
Update the M9 architecture references after database unification.
These sections describe incompatible current architectures. The current design uses one Database, removes MDatabase, and names the compatibility theorem mcong_iff_cong.
semantics/PLAN.md#L99-L102: Describe the action-block merge form and its result expressions.semantics/PLAN.md#L293-L301: Replacemcong_toM_iffwithmcong_iff_cong.semantics/MERGE.md#L803-L806: State that the separate-MDatabasedesign was rejected, or remove this stale description.
📍 Affects 2 files
semantics/PLAN.md#L99-L102(this comment)semantics/PLAN.md#L293-L301semantics/MERGE.md#L803-L806
🤖 Prompt for AI Agents
Verify each finding against current code. Fix only still-valid issues, skip the
rest with a brief reason, keep changes minimal, and validate.
In `@semantics/PLAN.md` around lines 99 - 102, Update the M9 architecture
references across semantics/PLAN.md lines 99-102, semantics/PLAN.md lines
293-301, and semantics/MERGE.md lines 803-806: describe the action-block merge
form and its result expressions in the first section, rename mcong_toM_iff to
mcong_iff_cong in the second, and state that the separate-MDatabase design was
rejected or remove that stale description in the third, consistently reflecting
the unified Database design without MDatabase.
There was a problem hiding this comment.
Actionable comments posted: 11
Caution
Some comments are outside the diff and can’t be posted inline due to platform limitations.
⚠️ Outside diff range comments (4)
semantics/EgglogSemantics/Spec/Database.lean (1)
109-110: 📐 Maintainability & Code Quality | 🔵 Trivial | 💤 Low valueBind the intermediate database in
addRow.Line 110 writes
(db.addTerms as).addTerms vstwice. The two occurrences elaborate to two copies of the same term, which enlarges every goal that unfoldsaddRow. Aletstates the intent once and keeps the definition equal byrfl.♻️ Proposed refactor
def addRow (f : FnName) (as vs : List Term) (db : Database) : Database := - { (db.addTerms as).addTerms vs with rows := insert ⟨f, as, vs⟩ ((db.addTerms as).addTerms vs).rows } + let d := (db.addTerms as).addTerms vs + { d with rows := insert ⟨f, as, vs⟩ d.rows }🤖 Prompt for AI Agents
Verify each finding against current code. Fix only still-valid issues, skip the rest with a brief reason, keep changes minimal, and validate. In `@semantics/EgglogSemantics/Spec/Database.lean` around lines 109 - 110, Update addRow to bind the repeated (db.addTerms as).addTerms vs expression to a local intermediate database with let, then use that binding for both the record update and its rows field while preserving definitional equality by rfl.semantics/EgglogSemantics/Impl/Merge.lean (3)
51-55: 🚀 Performance & Scalability | 🟠 Major | 🏗️ Heavy lift
outsrecomputes the congruence closure on every lookup, which defeats the once-per-pass claim inmergeRound.Line 53 calls
d.closureFon eachoutscall.closureFisclosureTotal d.termsF d.eqsF, a fixpoint overterms ×ˢ terms.outsis called fromexecExpr's lookup branch, so one call happens per.mergeapplication in every expression evaluated.Two paths pay this repeatedly:
mergeOneWithhoistsclfor the key comparison, but Line 148 runsexecActionsfor the body and Line 149 evaluatesres. Every.mergeapplication inbodyorrestriggers a fresh closure. The docstring at Lines 187-193 states that a pass computes the closure once.patternHoldsMcomputes its own closure and additionally callsexecExprper candidate substitution, so each candidate can trigger several closures.Thread a closure parameter through
outs,execExpr, andexecExprList, and pass the hoistedclfrommergeRoundandpatternHoldsM.♻️ Proposed signature change
/-- `Database.Out`, computed: every output recorded at a key congruent to `as`. -/ -def outs (d : FDatabase) (f : FnName) (as : List Term) : List (List Term) := - let cl := d.closureF - d.rows.filterMap fun r => +def outsWith (cl : Finset (Term × Term)) (d : FDatabase) (f : FnName) (as : List Term) : + List (List Term) := + d.rows.filterMap fun r => if r.fn = f && congrKeys cl as r.args then some r.out else none + +/-- `outsWith` at `d`'s own closure. -/ +def outs (d : FDatabase) (f : FnName) (as : List Term) : List (List Term) := + outsWith d.closureF d f as🤖 Prompt for AI Agents
Verify each finding against current code. Fix only still-valid issues, skip the rest with a brief reason, keep changes minimal, and validate. In `@semantics/EgglogSemantics/Impl/Merge.lean` around lines 51 - 55, Thread a precomputed congruence closure through outs, execExpr, and execExprList instead of recomputing d.closureF inside outs. Update mergeRound and mergeOneWith to pass their hoisted closure through action/body/result evaluation, and have patternHoldsM pass its own closure through candidate expression evaluation so each pass reuses one closure.
75-77: 🎯 Functional Correctness | 🟡 Minor | ⚡ Quick winThe lookup branch rejects a key class whose first recorded output is multi-column, even when a one-column output is also recorded.
Line 76 matches
[v] :: _, so it inspects only the head ofd.outs f ts.Expr.MEval.lookupinsemantics/EgglogSemantics/Spec/Merge.leanLine 283 requiresdb.Out f ts [v], that is some recorded output with exactly one column. The docstring at Lines 60-61 states that the interpreter "takes the first recorded output", which describes a choice among candidates, not a rejection of all of them.
FnDecl.outArityis never checked by any rule, so one function name can carry rows of different widths. In that state this returnsnone,execMreturnsnone, and the difftest reportsSTUCKfor a program the spec evaluates.Scan for the first single-column output instead of testing only the head.
🐛 Proposed fix
match d.sig.mergeOf f with | .union => some (.app f ts) - | _ => match d.outs f ts with - | [v] :: _ => some v - | _ => none + | _ => (d.outs f ts).findSome? fun vs => + match vs with + | [v] => some v + | _ => none🤖 Prompt for AI Agents
Verify each finding against current code. Fix only still-valid issues, skip the rest with a brief reason, keep changes minimal, and validate. In `@semantics/EgglogSemantics/Impl/Merge.lean` around lines 75 - 77, Update the lookup branch in the surrounding merge evaluation function to scan d.outs f ts for the first recorded output matching exactly one column, rather than pattern-matching only the head. Return some v for that first [v] entry and none when no single-column output exists, preserving the documented first-candidate behavior.
37-41: 🎯 Functional Correctness | 🟠 Major | 🏗️ Heavy lift
execCmdMaccepts aseton a.unionfunction, which invalidates theclosureFassumption stated at Lines 37-41.The header states that
closureFneeds nofddisjunct because a.unionfunction's rows "are exactly the constructor rowsImpl/Closure.leanalready sees throughterms", qualified by "as long as every declared function is.mergeor.noMerge".That qualification covers declared functions only.
Signature.mergeOfinsemantics/EgglogSemantics/Spec/Syntax.leanLines 132-135 sends an undeclared name to.union, andexecCmdMat Line 323 runs any.action, including.set f args outfor an undeclaredf.FDatabase.addRowthen writes a row of a.unionfunction whoseoutis not.app f args.MCong.fdinsemantics/EgglogSemantics/Spec/Merge.leanLines 74-77 derives equalities from such a pair of rows, andclosureFdoes not, sopatternHoldsMandkeyRowCountunder-report.
semantics/EgglogSemantics/Spec/Scope.leanLines 148-152 already defineAction.SetLegalfor exactly this condition, but nothing in this file consults it. Reject the command, or state the hypothesis whereexecMis invoked.Run the following script to check what hypothesis
closureF_okcarries and whether any caller enforcesSetLegal:#!/bin/bash # Description: Check closureF_ok's hypotheses and any SetLegal enforcement in the interpreters and tooling. set -euo pipefail rg -n -C10 'closureF_ok' semantics/EgglogSemantics/Proofs/Merge.lean rg -n -C4 'SetLegal' --glob '*.lean'Also applies to: 322-326
🤖 Prompt for AI Agents
Verify each finding against current code. Fix only still-valid issues, skip the rest with a brief reason, keep changes minimal, and validate. In `@semantics/EgglogSemantics/Impl/Merge.lean` around lines 37 - 41, Update execCmdM and its callers to enforce Action.SetLegal before accepting .set actions, rejecting commands that set undeclared .union functions; alternatively, add and propagate this legality hypothesis through execM and the closureF-related proofs. Ensure closureF_ok, patternHoldsM, and keyRowCount are only used under the same SetLegal assumption so MCong.fd rows cannot be omitted.
🤖 Prompt for all review comments with AI agents
Verify each finding against current code. Fix only still-valid issues, skip the
rest with a brief reason, keep changes minimal, and validate.
Inline comments:
In `@semantics/EgglogSemantics/Impl/Merge.lean`:
- Around line 24-29: Update the module documentation and mergeSaturate docstring
to consistently describe execCmdM as saturating via FDatabase.mergeSaturateF.
Clarify that mergeRound performs one pass and is iterated by the saturating
execution path, while preserving the existing distinction for execCmd.
- Around line 150-151: Update the header refinement claim for execM so it no
longer states that ProgramStep reaches the interpreter’s resulting database.
Describe the actual containment/confinement relation established by the merge
semantics, and explicitly reference the corresponding theorem in
Proofs/Merge.lean, such as mergeRound_confined or the verified execM theorem
found there. Leave mergeOneWith and its row-removal behavior unchanged.
- Around line 350-352: Update the discussion around `mergeRound_rowCount` to
track or restate the theorem under the hypotheses required by its recorded
counterexample, and ensure the differential-test row-count path no longer relies
on the theorem as currently stated. Preserve the counterexample reference while
clearly identifying the corrected theorem scope.
In `@semantics/EgglogSemantics/Proofs/Merge.lean`:
- Line 10: Correct the theorem-status statement in the referenced documentation
to reflect all unproved proofs in Merge.lean, including the listed merge,
execution, row-count, lattice, and refinement-chain results; either provide the
accurate total count or describe these groups without claiming only five remain.
- Around line 929-951: Remove the four unusable theorem declarations
`MergeStep.diamond_of_join`, `RunStep.unique_of_confluent`, `execM_reachable`,
and `mergeRound_closure` instead of leaving them as open `sorry` goals; retain
their explanatory text only as comments beside the valid replacements
`RunStep.unique_of_diamond`, `execM_contained`, and
`FDatabase.mergeRound_contained`.
- Around line 455-457: Remove the redundant theorem Database.contained_addRow
from the merge proofs. Update any references to use Database.Contained.addRow
directly, preserving the existing argument order at callers such as
MergeStep.contained and Database.ActionStep.contained.
- Around line 497-533: The general-purpose lemmas are declared in the wrong
modules. Move Database.addTerm_eq_self, Database.addTerms_eq_self, and
Database.addTerms_terms_rows from semantics/EgglogSemantics/Proofs/Merge.lean
lines 497-533 to semantics/EgglogSemantics/Proofs/Database.lean beside the
existing Database.addTerms lemmas; move Database.Contained.addTerm_mono from
semantics/EgglogSemantics/Proofs/Merge.lean lines 977-982 into the Contained
namespace in semantics/EgglogSemantics/Proofs/Database.lean; and move
evalAction_sig from semantics/EgglogSemantics/Proofs/Step.lean lines 263-272 to
semantics/EgglogSemantics/Proofs/Eval.lean beside evalAction_rules, removing the
note that the destination file is not editable.
In `@semantics/EgglogSemantics/Proofs/Step.lean`:
- Around line 263-272: Move the evalAction_sig theorem from Step.lean to
Eval.lean, placing it next to the existing evalAction_rules lemma. Remove the
stale explanatory docstring and preserve the theorem statement and proof
unchanged.
- Around line 191-203: Move the shared merge lemma into the common Spec/Merge
module, declaring it once using the existing Signature.mergeOf and
Signature.AllConstructors symbols. Remove both
Signature.AllConstructors.mergeOf_eq in Step.lean and Signature.mergeOf_eq_union
in Merge.lean, and update any references to use the centralized lemma without
changing the import graph.
In `@semantics/EgglogSemantics/Spec/Encode.lean`:
- Around line 413-425: Extend Program.EncodeDomain with a WellScoped requirement
for the program, using the existing scope predicate and preserving the
associated SetLegal requirement from Scope.lean. Anchor the change in the
EncodeDomain structure so encoding theorems require well-scoped programs and
cannot admit Pattern.expr values whose encodeQueryExpr result is silently
discarded by encodePattern.
In `@semantics/MERGE.md`:
- Around line 802-804: Update the differential-test result in the
`semantics/MERGE.md` passage to report 118 cases for the current default matrix,
or explicitly identify 114 as belonging to an earlier configuration; keep the
pass/fail/skip and saturation details accurate.
---
Outside diff comments:
In `@semantics/EgglogSemantics/Impl/Merge.lean`:
- Around line 51-55: Thread a precomputed congruence closure through outs,
execExpr, and execExprList instead of recomputing d.closureF inside outs. Update
mergeRound and mergeOneWith to pass their hoisted closure through
action/body/result evaluation, and have patternHoldsM pass its own closure
through candidate expression evaluation so each pass reuses one closure.
- Around line 75-77: Update the lookup branch in the surrounding merge
evaluation function to scan d.outs f ts for the first recorded output matching
exactly one column, rather than pattern-matching only the head. Return some v
for that first [v] entry and none when no single-column output exists,
preserving the documented first-candidate behavior.
- Around line 37-41: Update execCmdM and its callers to enforce Action.SetLegal
before accepting .set actions, rejecting commands that set undeclared .union
functions; alternatively, add and propagate this legality hypothesis through
execM and the closureF-related proofs. Ensure closureF_ok, patternHoldsM, and
keyRowCount are only used under the same SetLegal assumption so MCong.fd rows
cannot be omitted.
In `@semantics/EgglogSemantics/Spec/Database.lean`:
- Around line 109-110: Update addRow to bind the repeated (db.addTerms
as).addTerms vs expression to a local intermediate database with let, then use
that binding for both the record update and its rows field while preserving
definitional equality by rfl.
🪄 Autofix
Fix all unresolved CodeRabbit comments on this PR:
- Push a commit to this branch (recommended)
- Create a new PR with the fixes
ℹ️ Review info
⚙️ Run configuration
Configuration used: Organization UI
Review profile: ASSERTIVE
Plan: Pro Plus
Run ID: a3fabdd2-17f3-4ebb-881e-1a24ea0cf0f3
📒 Files selected for processing (25)
scripts/difftest.shsemantics/CHECKER.mdsemantics/DiffTest.leansemantics/EgglogSemantics.leansemantics/EgglogSemantics/Impl/Interp.leansemantics/EgglogSemantics/Impl/Merge.leansemantics/EgglogSemantics/Proofs/Database.leansemantics/EgglogSemantics/Proofs/Encode.leansemantics/EgglogSemantics/Proofs/Eval.leansemantics/EgglogSemantics/Proofs/Interp.leansemantics/EgglogSemantics/Proofs/Match.leansemantics/EgglogSemantics/Proofs/Merge.leansemantics/EgglogSemantics/Proofs/Scope.leansemantics/EgglogSemantics/Proofs/Step.leansemantics/EgglogSemantics/Spec/Database.leansemantics/EgglogSemantics/Spec/Encode.leansemantics/EgglogSemantics/Spec/Eval.leansemantics/EgglogSemantics/Spec/Match.leansemantics/EgglogSemantics/Spec/Merge.leansemantics/EgglogSemantics/Spec/Scope.leansemantics/EgglogSemantics/Spec/Syntax.leansemantics/EgglogSemantics/Tests/Egg.leansemantics/MERGE.mdsemantics/PLAN.mdsemantics/README.md
| **The merge phase is one pass, not a fixpoint.** `mergeRound` fires each collision among | ||
| the pre-pass rows once and is structurally terminating, which is sound because `RunStep` | ||
| is `MergeClosure` with no `MergeSaturated` requirement — a prefix of the closure is a | ||
| reachable state. Saturation is *now* reachable, since `min` and `max` became `Prim`s and | ||
| merging is an idempotent join again; `mergeSaturateF` says what switching to it would | ||
| buy and cost. |
There was a problem hiding this comment.
📐 Maintainability & Code Quality | 🟡 Minor | ⚡ Quick win
The module documentation contradicts itself about whether the merge phase is one pass or a fixpoint.
Three statements disagree:
- Lines 24-25: "The merge phase is one pass, not a fixpoint."
- Lines 215-216: "Not used by
execCmd, which runs one pass — seemergeRound." - Lines 320-321: "The phase runs to a fixpoint, as
merge_alldoes."
execCmdM at Lines 323 and 325 calls FDatabase.mergeSaturateF mergeFuel, so the fixpoint statement is the current behavior and the other two are stale. Update Lines 24-29 and the mergeSaturate docstring to say that execCmdM saturates with mergeSaturateF, and that mergeRound is the single pass it iterates.
Also applies to: 213-216
🤖 Prompt for AI Agents
Verify each finding against current code. Fix only still-valid issues, skip the
rest with a brief reason, keep changes minimal, and validate.
In `@semantics/EgglogSemantics/Impl/Merge.lean` around lines 24 - 29, Update the
module documentation and mergeSaturate docstring to consistently describe
execCmdM as saturating via FDatabase.mergeSaturateF. Clarify that mergeRound
performs one pass and is iterated by the saturating execution path, while
preserving the existing distinction for execCmd.
| let e' := { e with rows := e.rows.filter fun r => r ≠ r₁ && r ≠ r₂ } | ||
| { e'.addRow r₁.fn r₁.args vs with env := d.env, rules := d.rules } |
There was a problem hiding this comment.
🗄️ Data Integrity & Integration | 🟠 Major | 🏗️ Heavy lift
mergeOneWith removes rows, so execM's result is not a state ProgramStep reaches, and the header claim at Lines 19-22 is stale.
Line 150 filters r₁ and r₂ out of e.rows. MergeStep in semantics/EgglogSemantics/Spec/Merge.lean Line 414 produces { d.addRow f as vs with env := db.env, rules := db.rules } and removes nothing. MergeClosure is Relation.ReflTransGen MergeStep, so every spec-reachable state still holds both colliding rows.
The header of this file states the refinement as ProgramStep d.toDatabase p (exec p).toDatabase, "the interpreter's result is one the spec reaches". A state with rows deleted is not such a state. Database.Contained in semantics/EgglogSemantics/Spec/Database.lean Lines 142-145 requires rows ⊆, which fails in both directions here.
The docstring at Lines 104-112 argues the contract weakens to containment, and mergeRound_confined bounds what is removed. Neither establishes reachability. Correct the header to state the actual relation between execM and the spec, and state which theorem in Proofs/Merge.lean carries it.
Run the following script to check what Proofs/Merge.lean currently claims:
#!/bin/bash
# Description: Inspect the stated refinement and confinement theorems for the merge interpreter.
set -euo pipefail
ast-grep outline semantics/EgglogSemantics/Proofs/Merge.lean --items all --view expanded || true
rg -n -C8 'execM_reachable|exec_toDatabase|mergeRound_confined|ProgramStep' \
semantics/EgglogSemantics/Proofs/Merge.lean🤖 Prompt for AI Agents
Verify each finding against current code. Fix only still-valid issues, skip the
rest with a brief reason, keep changes minimal, and validate.
In `@semantics/EgglogSemantics/Impl/Merge.lean` around lines 150 - 151, Update the
header refinement claim for execM so it no longer states that ProgramStep
reaches the interpreter’s resulting database. Describe the actual
containment/confinement relation established by the merge semantics, and
explicitly reference the corresponding theorem in Proofs/Merge.lean, such as
mergeRound_confined or the verified execM theorem found there. Leave
mergeOneWith and its row-removal behavior unchanged.
| therefore invariant under the merge phase, which `Proofs/Merge.lean`'s | ||
| `mergeRound_rowCount` states — and does not hold as stated; the counterexample is | ||
| recorded there. It is also why keeping every superseded output — the |
There was a problem hiding this comment.
📐 Maintainability & Code Quality | 🔵 Trivial
mergeRound_rowCount is recorded as not holding as stated.
Lines 350-352 state that Proofs/Merge.lean's mergeRound_rowCount "does not hold as stated; the counterexample is recorded there." The row count is what the differential test compares, so the gap sits on the checked path.
Do you want me to open an issue to track restating mergeRound_rowCount under the hypotheses the counterexample needs?
🤖 Prompt for AI Agents
Verify each finding against current code. Fix only still-valid issues, skip the
rest with a brief reason, keep changes minimal, and validate.
In `@semantics/EgglogSemantics/Impl/Merge.lean` around lines 350 - 352, Update the
discussion around `mergeRound_rowCount` to track or restate the theorem under
the hypotheses required by its recorded counterexample, and ensure the
differential-test row-count path no longer relies on the theorem as currently
stated. Preserve the counterexample reference while clearly identifying the
corrected theorem scope.
| /-! | ||
| # What M9 has to prove | ||
|
|
||
| `MERGE.md` says which theorem buys what. Five are still unproved; the rest are proved. |
There was a problem hiding this comment.
📐 Maintainability & Code Quality | 🟡 Minor | ⚡ Quick win
Correct the unproved count.
The line states "Five are still unproved; the rest are proved." This file contains far more than five sorry proofs: MergeStep.diamond_of_join, RunStep.unique_of_confluent, execM_reachable, mergeRound_closure, FDatabase.mergeRound_rowCount, execM_current_of_lattice, and the whole refinement chain from FDatabase.Inv.empty through FDatabase.execProgramM_contained (Lines 1103-1194).
execM_contained at Lines 1199-1201 has no sorry of its own, but it depends on FDatabase.execProgramM_contained and FDatabase.Inv.empty, so it is also unproved.
State the actual count, or describe the groups instead of a number.
🤖 Prompt for AI Agents
Verify each finding against current code. Fix only still-valid issues, skip the
rest with a brief reason, keep changes minimal, and validate.
In `@semantics/EgglogSemantics/Proofs/Merge.lean` at line 10, Correct the
theorem-status statement in the referenced documentation to reflect all unproved
proofs in Merge.lean, including the listed merge, execution, row-count, lattice,
and refinement-chain results; either provide the accurate total count or
describe these groups without claiming only five remain.
| theorem Database.contained_addRow {db : Database} {f : FnName} {as vs : List Term} : | ||
| db.Contained (db.addRow f as vs) := | ||
| Database.Contained.addRow f as vs db |
There was a problem hiding this comment.
📐 Maintainability & Code Quality | 🔵 Trivial | 💤 Low value
Database.contained_addRow adds nothing over Database.Contained.addRow.
The body is Database.Contained.addRow f as vs db with the arguments reordered. MergeStep.contained at Line 488 and Database.ActionStep.contained at Line 466 both call Database.Contained.addRow directly, so this alias has no caller in this file. Delete it and use the lemma from Proofs/Database.lean.
As per coding guidelines: "Prefer current local APIs over reviving old downstream-only helper methods."
🤖 Prompt for AI Agents
Verify each finding against current code. Fix only still-valid issues, skip the
rest with a brief reason, keep changes minimal, and validate.
In `@semantics/EgglogSemantics/Proofs/Merge.lean` around lines 455 - 457, Remove
the redundant theorem Database.contained_addRow from the merge proofs. Update
any references to use Database.Contained.addRow directly, preserving the
existing argument order at callers such as MergeStep.contained and
Database.ActionStep.contained.
Source: Coding guidelines
| theorem MergeStep.diamond_of_join {db d₁ d₂ : Database} | ||
| {le : List Term → List Term → Prop} | ||
| (hjoin : ∀ f as v w, db.Current le f as v → db.Out f as w → le w v) | ||
| (h₁ : MergeStep db d₁) (h₂ : MergeStep db d₂) : | ||
| ∃ d, MergeClosure d₁ d ∧ MergeClosure d₂ d := by | ||
| sorry | ||
|
|
||
| /-- **`hconf` is too weak to use.** Local confluence plus "both are normal forms" gives | ||
| uniqueness only via Newman's lemma, which needs the relation to be *terminating* — and | ||
| `MergeStep` deliberately is not (`MERGE.md`, constraint (6)). Without termination the | ||
| implication genuinely fails in general rewriting: `a ⇄ b`, `a → c`, `b → d` with `c`, | ||
| `d` normal is locally confluent and has two normal forms. That shape cannot arise here, | ||
| because `MergeStep.contained` forbids cycles — so the *conclusion* is very likely true | ||
| — but it is true for a reason `hconf` does not supply, and the only route to it is the | ||
| strong diamond, which is `MergeStep.diamond_of_join` restated. Hence | ||
| `RunStep.unique_of_diamond` below, which is this theorem with a hypothesis a proof can | ||
| actually consume. -/ | ||
| theorem RunStep.unique_of_confluent {db d₁ d₂ : Database} | ||
| (hconf : ∀ e e₁ e₂, MergeStep e e₁ → MergeStep e e₂ → | ||
| ∃ e', MergeClosure e₁ e' ∧ MergeClosure e₂ e') | ||
| (hs₁ : MergeSaturated d₁) (hs₂ : MergeSaturated d₂) | ||
| (h₁ : RunStep db d₁) (h₂ : RunStep db d₂) : d₁ = d₂ := by | ||
| sorry |
There was a problem hiding this comment.
📐 Maintainability & Code Quality | 🔵 Trivial | ⚡ Quick win
Do not keep statements you have shown to be false or vacuous as open sorry goals.
Four declarations are documented as unusable, and each already has a replacement in this file:
MergeStep.diamond_of_join(Lines 929-934): the docstring stateshjoinis vacuous.RunStep.unique_of_confluent(Lines 946-951): the docstring stateshconfis too weak to consume;RunStep.unique_of_diamondat Lines 961-967 is the version that is proved.execM_reachable(Lines 1051-1053): the docstring states the theorem is false as stated;execM_containedat Lines 1199-1201 replaces it.mergeRound_closure(Lines 1254-1256): the docstring states it is false once the implementation deletes;FDatabase.mergeRound_containedat Lines 1168-1170 replaces it.
A sorry marks a goal someone is expected to close. These four goals cannot be closed. Delete each statement, or keep the text as a comment beside its replacement. Otherwise a reader cannot tell the open work from the abandoned work, and downstream code can depend on a false statement.
🤖 Prompt for AI Agents
Verify each finding against current code. Fix only still-valid issues, skip the
rest with a brief reason, keep changes minimal, and validate.
In `@semantics/EgglogSemantics/Proofs/Merge.lean` around lines 929 - 951, Remove
the four unusable theorem declarations `MergeStep.diamond_of_join`,
`RunStep.unique_of_confluent`, `execM_reachable`, and `mergeRound_closure`
instead of leaving them as open `sorry` goals; retain their explanatory text
only as comments beside the valid replacements `RunStep.unique_of_diamond`,
`execM_contained`, and `FDatabase.mergeRound_contained`.
| /-- On an all-constructors signature every function's merge is `.union`. | ||
|
|
||
| The same statement as `Proofs/Merge.lean`'s `Signature.mergeOf_eq_union`, under another | ||
| name rather than imported: that file sits above this one in the import graph and will | ||
| want `Proofs/Interp.lean` once `execM_reachable` is proved, so importing it here would | ||
| risk a cycle. The two should become one lemma when these results move next to | ||
| `mcong_iff_cong`. -/ | ||
| theorem Signature.AllConstructors.mergeOf_eq {sig : Signature} (h : sig.AllConstructors) | ||
| (f : FnName) : sig.mergeOf f = MergeSpec.union := by | ||
| unfold Signature.mergeOf | ||
| cases hf : sig f with | ||
| | none => rfl | ||
| | some d => exact h f d hf |
There was a problem hiding this comment.
📐 Maintainability & Code Quality | 🔵 Trivial | ⚡ Quick win
Move the shared lemma below both files instead of duplicating it.
Signature.AllConstructors.mergeOf_eq here and Signature.mergeOf_eq_union in semantics/EgglogSemantics/Proofs/Merge.lean (Lines 43-48) have the same statement and the same proof. The import-cycle reason in the docstring is correct: Proofs/Merge.lean imports Proofs/Interp.lean, which reaches this file through Proofs/Scope.lean, so this file cannot import Proofs/Merge.lean.
The duplication is avoidable without changing the import graph. Signature.mergeOf and Signature.AllConstructors come from EgglogSemantics/Spec/Merge.lean, which both files already import. Declare the lemma once there and delete both copies. Two copies can drift apart if the mergeOf default changes.
🤖 Prompt for AI Agents
Verify each finding against current code. Fix only still-valid issues, skip the
rest with a brief reason, keep changes minimal, and validate.
In `@semantics/EgglogSemantics/Proofs/Step.lean` around lines 191 - 203, Move the
shared merge lemma into the common Spec/Merge module, declaring it once using
the existing Signature.mergeOf and Signature.AllConstructors symbols. Remove
both Signature.AllConstructors.mergeOf_eq in Step.lean and
Signature.mergeOf_eq_union in Merge.lean, and update any references to use the
centralized lemma without changing the import graph.
| /-- No action touches the signature. Belongs in `Proofs/Eval.lean` beside | ||
| `evalAction_rules`; it is here because that file is not this one's to edit. -/ | ||
| theorem evalAction_sig {db db' : Database} {a : Action} | ||
| (h : evalAction db a = some db') : db'.sig = db.sig := by | ||
| rcases evalAction_eq_some h with ⟨_, _, -, -, rfl⟩ | ⟨_, _, _, -, -, rfl⟩ | | ||
| ⟨_, _, _, _, -, -, -, rfl⟩ | ⟨_, _, _, _, _, -, -, -, rfl⟩ | ||
| · rfl | ||
| · rfl | ||
| · rfl | ||
| · simp |
There was a problem hiding this comment.
📐 Maintainability & Code Quality | 🔵 Trivial | 💤 Low value
The stated reason for placing evalAction_sig here is stale.
The docstring says the lemma belongs in Proofs/Eval.lean and that "that file is not this one's to edit". This pull request does edit semantics/EgglogSemantics/Proofs/Eval.lean. evalAction_rules, the lemma this one mirrors, is declared there at Lines 131-138.
Move evalAction_sig next to evalAction_rules and delete the comment.
🤖 Prompt for AI Agents
Verify each finding against current code. Fix only still-valid issues, skip the
rest with a brief reason, keep changes minimal, and validate.
In `@semantics/EgglogSemantics/Proofs/Step.lean` around lines 263 - 272, Move the
evalAction_sig theorem from Step.lean to Eval.lean, placing it next to the
existing evalAction_rules lemma. Remove the stale explanatory docstring and
preserve the theorem statement and proof unchanged.
| /-- Constructors only, and no name that would collide with a generated one. -/ | ||
| structure Program.EncodeDomain (P : Program) : Prop where | ||
| /-- Every declared function is a constructor. -/ | ||
| ctorsOnly : ∀ c ∈ P, ∀ f d, c = Cmd.decl f d → d.merge = MergeSpec.union | ||
| /-- No `set` action anywhere. -/ | ||
| noSet : ∀ c ∈ P, c.NoSet | ||
| /-- No source function shadows a primitive, so every application builds. -/ | ||
| noPrim : ∀ fk ∈ P.ctors, Prim.ofName fk.1 = none | ||
| /-- No source function is in the generated namespace. -/ | ||
| noAt : ∀ fk ∈ P.ctors, ¬ "@".isPrefixOf fk.1 | ||
| /-- Nor any source variable: the generated `@v0`, `@v1`, … are numbered from one | ||
| supply for the whole program, so they collide with nothing but a source `@` name. -/ | ||
| noAtVar : ∀ v ∈ P.vars, ¬ "@".isPrefixOf v |
There was a problem hiding this comment.
🎯 Functional Correctness | 🟠 Major | ⚡ Quick win
Program.EncodeDomain does not require WellScoped, and encodeQueryExpr silently drops a non-application fact.
encodeQueryExpr returns (.var v, [], n) for .var v and (.lit l, [], n) for .lit l. encodePattern on .expr e keeps only the pattern list, so a source fact Pattern.expr (.var v) encodes to no pattern at all. The encoded rule then has a strictly weaker query than the source rule, which breaks the soundness half of simulation.
Spec/Scope.lean's Pattern.Scoped rules that shape out through Expr.IsApp, and Scope.lean Line 136 records the pair to carry as WellScoped p ∧ p.SetLegal sig. Record the same requirement here so the M11 theorems cannot be stated without it.
🛡️ Proposed field
structure Program.EncodeDomain (P : Program) : Prop where
/-- Every declared function is a constructor. -/
ctorsOnly : ∀ c ∈ P, ∀ f d, c = Cmd.decl f d → d.merge = MergeSpec.union
+ /-- Every query fact is an application, so `encodeQueryExpr` emits a view read for
+ it. Without this a `Pattern.expr (.var v)` fact encodes to no pattern at all. -/
+ scoped : WellScoped P
/-- No `set` action anywhere. -/
noSet : ∀ c ∈ P, c.NoSet📝 Committable suggestion
‼️ IMPORTANT
Carefully review the code before committing. Ensure that it accurately replaces the highlighted code, contains no missing lines, and has no issues with indentation. Thoroughly test & benchmark the code to ensure it meets the requirements.
| /-- Constructors only, and no name that would collide with a generated one. -/ | |
| structure Program.EncodeDomain (P : Program) : Prop where | |
| /-- Every declared function is a constructor. -/ | |
| ctorsOnly : ∀ c ∈ P, ∀ f d, c = Cmd.decl f d → d.merge = MergeSpec.union | |
| /-- No `set` action anywhere. -/ | |
| noSet : ∀ c ∈ P, c.NoSet | |
| /-- No source function shadows a primitive, so every application builds. -/ | |
| noPrim : ∀ fk ∈ P.ctors, Prim.ofName fk.1 = none | |
| /-- No source function is in the generated namespace. -/ | |
| noAt : ∀ fk ∈ P.ctors, ¬ "@".isPrefixOf fk.1 | |
| /-- Nor any source variable: the generated `@v0`, `@v1`, … are numbered from one | |
| supply for the whole program, so they collide with nothing but a source `@` name. -/ | |
| noAtVar : ∀ v ∈ P.vars, ¬ "@".isPrefixOf v | |
| /-- Constructors only, and no name that would collide with a generated one. -/ | |
| structure Program.EncodeDomain (P : Program) : Prop where | |
| /-- Every declared function is a constructor. -/ | |
| ctorsOnly : ∀ c ∈ P, ∀ f d, c = Cmd.decl f d → d.merge = MergeSpec.union | |
| /-- Every query fact is an application, so `encodeQueryExpr` emits a view read for | |
| it. Without this a `Pattern.expr (.var v)` fact encodes to no pattern at all. -/ | |
| scoped : WellScoped P | |
| /-- No `set` action anywhere. -/ | |
| noSet : ∀ c ∈ P, c.NoSet | |
| /-- No source function shadows a primitive, so every application builds. -/ | |
| noPrim : ∀ fk ∈ P.ctors, Prim.ofName fk.1 = none | |
| /-- No source function is in the generated namespace. -/ | |
| noAt : ∀ fk ∈ P.ctors, ¬ "@".isPrefixOf fk.1 | |
| /-- Nor any source variable: the generated `@v0`, `@v1`, … are numbered from one | |
| supply for the whole program, so they collide with nothing but a source `@` name. -/ | |
| noAtVar : ∀ v ∈ P.vars, ¬ "@".isPrefixOf v |
🤖 Prompt for AI Agents
Verify each finding against current code. Fix only still-valid issues, skip the
rest with a brief reason, keep changes minimal, and validate.
In `@semantics/EgglogSemantics/Spec/Encode.lean` around lines 413 - 425, Extend
Program.EncodeDomain with a WellScoped requirement for the program, using the
existing scope predicate and preserving the associated SetLegal requirement from
Scope.lean. Anchor the change in the EncodeDomain structure so encoding theorems
require well-scoped programs and cannot admit Pattern.expr values whose
encodeQueryExpr result is silently discarded by encodePattern.
| `Lit.int` fixed all three: the suite went from 102 passed / 12 skipped to **114 passed, 0 | ||
| failed, 0 skipped**, and saturation became reachable again (`execCmdM` still runs one pass, | ||
| for the reason in `mergeSaturateF`'s docstring). This is the sharpest thing the coverage |
There was a problem hiding this comment.
📐 Maintainability & Code Quality | 🟡 Minor | ⚡ Quick win
Correct the stated differential-test total.
The default matrix contains 10 curated cases, 18 curated merge cases, 60 random cases, and 30 random merge cases. A clean default run covers 118 cases, not 114. Update this result, or state that it describes an earlier configuration.
🤖 Prompt for AI Agents
Verify each finding against current code. Fix only still-valid issues, skip the
rest with a brief reason, keep changes minimal, and validate.
In `@semantics/MERGE.md` around lines 802 - 804, Update the differential-test
result in the `semantics/MERGE.md` passage to report 118 cases for the current
default matrix, or explicitly identify 114 as belonging to an earlier
configuration; keep the pass/fail/skip and saturation details accurate.
Stage 1 and stage 2 of the chain in Proofs/Merge.lean, plus the repair the
statements needed.
FDatabase.Inv.addTerm, .addEq and .addRow were false as stated: addTerm takes
an arbitrary Term, so inserting an application of a declared :merge function
puts a non-constructor into terms and breaks the ctorTerms field. Each now
carries the constructor-term condition on what it inserts. addRow's hf was
also defending the wrong field -- RowsComplete is only an inclusion, which
adding a row cannot break -- and now earns its keep against ctorRows.
Inv gains the two fields the chain actually reads: rowsWF, without which a
lookup's result is unconstrained and execAction cannot re-establish
ctorTerms, and ctorRows, which is closureF_ok's hrow. Spec/Database.lean
already predicted the first ("belongs there once something reads it").
Discharged: Inv.empty, Inv.addTerm, Inv.addEq, Inv.addRow, Inv.execAction,
execExpr_MEval, execExprList_MEvalList. Merge.lean goes from 23 sorries to
16; lake build is clean at 716 jobs and mcong_iff_cong still depends on
propext alone.
Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
…emmas
Proofs/Counterexamples.lean collects machine-checked witnesses, so they are
checked by lake build rather than described in prose. Every witness keeps its
:merge function nullary, which makes congrKeys reduce without forcing
closureF, whose well-founded recursion the kernel cannot unfold; the whole
interpreter down to mergeSaturateF 64 then reduces by rfl.
execM_contained is false, not merely unproved. execCmdM runs a merge phase
after every top-level .action while CmdStep.action has none, so the
implementation reaches states holding a merge result no ProgramStep state
holds. claim2_execM refutes it on
(function f () i64 :merge 7) (set (f) 1) (set (f) 2)
where execM prog = some d2 by rfl and every spec successor has rows exactly
{f()->1, f()->2}. Since execM_contained was derived rather than sorried, it
read as settled. execCmdM_contained and execProgramM_contained fall with it.
Inv.mergeRound is false for a separate reason: a merge body carries no
SetLegal obligation, so a set on a constructor inside one writes a .union row
that is not a constructor row. Replaced by Inv.mergeRound_of_legalMerges.
CtorTerms is preserved, as its docstring claims; the break is ctorRows.
Also proves Inv.execActions, mergeOneWith_inv, Inv.setEnv/setEnvRules/
filterRows. Merge.lean goes from 23 sorries to 15, lake build is clean at 717
jobs, and mcong_iff_cong still depends on propext alone.
Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
lean-check greps the sources for `sorry` because lake build only warns. The grep also matched a module docstring that discusses `sorry` in prose, so the target could never pass even at zero real obligations. Dropping backtick- quoted hits fixes it without giving up the source grep. The known-false table blamed `execM_reachable` on "every MergeStep grows the state". That is `mergeRound_closure`'s reason. Despite the name, `execM_reachable` is about `exec`, which has no merge phase; it is false because Expr.eval builds an application for every name, and its own docstring says so with two counterexamples. Split into two rows. Queue item 7 claimed the import-order strays were "all flagged in place". Two are not flagged, and two that are flagged were missing from the list. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Fifteen of the chain's seventeen lemmas are now proved. Merge.lean goes from 15 sorries to 8; lake build is clean at 717 jobs and mcong_iff_cong still depends on propext alone. Nine of the seventeen were false as stated. Three of those were wrong in ways their already-proved M10 analogues in Proofs/Interp.lean had solved: - matchQueryM_MValidQuerySubst wanted the conclusion up to Env.Agree, as validQuerySubst_of_mem_matchQuery already concludes. Query.freeVars deduplicates while Env.UnionAll is literal concatenation, so the un-Agree'd form is unsatisfiable for any query with a repeated variable. - patternHoldsM_MValidSubst lacked patternHolds_iff's ValidEnv. - execActions_ActionsStep lacked SetLegal, so its cons step could not re-establish Inv. mergeRound_contained, mergeSaturateF_contained and execRunRulesM_contained carry legality side conditions, all instances of one condition: an action block that writes a row must be SetLegal. The spec gap is that Cmd.SetLegal (.decl _ _) is True, so nothing constrains a merge body. HANDOFF queue item 6 estimated the ActionsStep transport lemma at 150-250 lines and called it the whole cost of the merge phase. ActionsStep.mono is 35: an ActionStep's effect is fixed by its MEval witnesses and Expr.MEval.mono carries those into a larger database. Containment needs only a lower bound. diamond_of_join still wants the exact componentwise join and stays open. execCmdM_contained and execProgramM_contained remain refuted and are blocked on the specification fix in queue item 0, verified against the release binary: egglog resolves a :merge collision at the second top-level set, with no (run). Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
CmdStep.action gains a MergeClosure phase. Real egglog resolves a :merge collision at a top-level set with no (run): a bare action is compiled into a one-rule run (lib.rs:1490, eval_actions) and every rule-set run ends in merge_all. Checked against the release binary -- (function f () i64 :merge (max old new)) (set (f) 1) (set (f) 2) => (print-size f) = 1, (f) -> 2 and swapping the merge gives old->1, new->2, min->1, max->2, so the merge function really runs rather than last-write-wins. The specification was the side that was wrong; execM was faithful all along. That makes execCmdM_contained, execProgramM_contained and execM_contained provable, so the chain is 17 of 17. They carry two side conditions: Signature.MergesLegal, because a declared merge body writes rows and nothing else constrains it (Cmd.SetLegal (.decl _ _) is True), and FDatabase.ProgramLegal, whose FDatabase.Unused clause is egglog's own declare- before-use -- Falsity.claim1 shows a declaration can otherwise destroy Inv. Neither is vacuous: empty.ProgramLegal holds of the three-command merge program that used to refute execM_contained. Falsity.claim2_* are deleted. They recorded this spec bug and the bug is fixed. claim1, claim3, mergeRound_inv_false and the matching refutations stand. Merge.lean goes from 8 sorries to 6; lake build is clean at 717 jobs and mcong_iff_cong still depends on propext alone. Impl/ is untouched. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Proofs/Rebuilt.lean, machine-checked. Rebuilt is the hypothesis encode_complete, encode_simulation and encode_simulation_run carry, so its satisfiability is what decides whether those say anything. Its shape is sound -- rebuilt₁ exhibits a state satisfying both conjuncts, and MergeSaturated is reachable now that CmdStep.action merges. But conjunct 1 fails whenever the union does any work. encode P emits no Cmd.run when P has none, only CmdStep.run reaches RunRules, and a merge only re-adds a row at an existing key, so a view row keyed on a non-leader is never re-keyed. rebuilt_rekeys is the general form; not_rebuilt₀ and rebuilt₁ are one program differing only in which literal is built, since Term.blt's orientation decides whether the union is inert. The recorded fix does not work. Cmd.run is one round and RunRules fires every rule against the pre-state, so union chains need a round per link and congruence needs one per level -- the count grows with term depth, and with source rules there may be no k. An achievability lemma is what closes it; HANDOFF item 4 states it. Also machine-checked, and narrower than encode_complete's docstring claims: MergeStep never applies to an EncodeDomain source, so trailing (run)s are a no-op there and for the rule-free fragment can be appended to the target alone. lake build clean at 718 jobs. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Replaces the file rather than patching it: the previous version described a chain that was "stated and ready to prove" and a Rebuilt fix that does not work, and enough had changed that the edits were reading as a diff. New sections for the two things a reader most needs: why the merge phase now runs between commands, with the egglog evidence; and the Rebuilt problem, which is the one place M11 is broken independently of the encoder being unfinished, with three routes out and a recommendation. Every identifier named in the file is checked to resolve. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
|
out of date |
1 participant
Summary by CodeRabbit
New Features
Documentation
Chores