[6-1] Pair dataset schema, builder skeleton, and split logic#98
Open
duckyquang wants to merge 5 commits into
Open
[6-1] Pair dataset schema, builder skeleton, and split logic#98duckyquang wants to merge 5 commits into
duckyquang wants to merge 5 commits into
Conversation
…audit [3-5] audit direct vs post-hoc EML-DAG equivalence
[3-6] goal 3 metrics pipeline: checkpoint/resume, atomic writes, coun…
[3-7] goal 3 analysis: stratification, reuse metrics, compression-vs-…
[3-8] frozen EML-DAG cost interface for goal 4, Goal 3 summary docs
Schema + control flow for the equivalence-pair build, with the e-graph engine and the verifier injected as protocols so nothing imports 4-4/4-5 or 2-6 while those are unmerged. Split/leakage/OOD logic is finished rather than stubbed - it needs nothing from other branches. Production >=50k/5k/5k build still waits on 1-8, 4-4/4-5 and 2-6.
duckyquang
added
partial-start
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Summary
Partial start on [6-1]. The full build needs 1-8, 4-4/4-5 and 2-6, none of which are merged, so what's here is everything that doesn't: the pair record schema, the builder control flow with its failure accounting, the hard-negative matching, and all the split/leakage/OOD bookkeeping.
The e-graph engine and the verifier come in as protocols instead of imports, so nothing on this branch depends on an unmerged module. Swapping the fakes for the real objects when 4-4/4-5 and 2-6 land shouldn't need changes here.
Only touches 6-1's owned paths, and they're all new files, so this shouldn't collide with anything in flight.
Result
14 new tests, full suite 106 passing on a fresh clone:
Notes
left_signaturetoPairRecordandsignaturetoSourceExpressionwhile writing [7-0]. Without a starting state you can't replay step 0, so the trace is unusable. Flagging it because it's a schema field other people will consume.group_idfalls back to the expression id until 4-2 gives us e-class ids. That fallback can't see that two ids are e-class relatives, so a cleanfind_leaksunder it is weaker evidence than it looks — the real build has to run witheclass_idpopulated. Documented in the spec.SaturationEngine/Equivalentshape ingenerate.pyis my read of what 4-2–4-5 will hand back (equivalent id, size, depth, full rule sequence). If that's not what saturation will actually produce, tell me now and I'll change it rather than making you work around it later.Verifier.verify(left, right, rule_sequence) -> Verificationagainst 2-6 — I've got tiers asegraph_proof/symbolic/numericand statuses asverified/refuted/unsupported. Negatives need a positiverefuted, not just "couldn't prove equal", so I want to be sure 2-6 can give me that.