Add fact lifecycle and relation indexing to TermIdentitySidecar - #116
Open
MesTTo wants to merge 3 commits into
Open
Add fact lifecycle and relation indexing to TermIdentitySidecar#116MesTTo wants to merge 3 commits into
MesTTo wants to merge 3 commits into
Conversation
MesTTo
force-pushed
the
pr/mork-term-identity-facts
branch
from
June 24, 2026 13:37
84dfe8c to
0edb750
Compare
This was referenced Jun 24, 2026
Adds the thin fact layer over the interning base: FactId liveness via a weight tombstone (remove_fact tombstones, insert_fact revives the same FactId, the Lucene "live documents" model), live_fact_count, and facts_by_relation, an index from a relation head to its facts so a consumer (EGraph::from_equalities, RelationAdjacency::from_sidecar) scans one relation instead of the whole sidecar. Deliberately excludes incremental maintenance (prefix staleness watermarks, delta application, PathMap re-sync scans): incremental maintenance is deferred project-wide, and PathMap's own shared_node_id COW identity is the right staleness primitive when it becomes needed, not a value-count watermark.
Replaces the hand-rolled 128-bit FNV in TermIdentitySidecar with the canonical Expr::hash (gxhash128 over the term's byte span), the same structural hash the rest of MORK already uses. The hash is only a collision-bucket filter -- exact encoded bytes are compared before an identity is reused -- so the swap cannot change which terms share a TermId, on ground or adversarial input. Modeled in Alloy (fac22_term_identity in MesTTo/alloy-mork): HashSwapPreservesIdentity is UNSAT. Addresses the maintainer's "reuse, don't reimplement" direction (no bespoke hash where the crate has one). term_identity (4) and egraph (2) suites pass.
MesTTo
force-pushed
the
pr/mork-term-identity-facts
branch
from
July 4, 2026 07:58
0edb750 to
de28f19
Compare
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
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.
Adds the thin fact layer over the term-identity interning base: FactId liveness via a weight tombstone (
remove_facttombstones,insert_factrevives the sameFactId— the Lucene "live documents" model),live_fact_count, andfacts_by_relation, an index from a relation head to its facts so a consumer (EGraph::from_equalitiesin #117,RelationAdjacency::from_sidecarin #121) scans one relation instead of the whole sidecar.Scope is deliberately trimmed to what those consumers use. It excludes incremental maintenance (prefix staleness watermarks, delta application, PathMap re-sync scans): incremental maintenance is deferred, and PathMap's own
shared_node_idCOW identity is the right staleness primitive when it becomes needed, not a value-count watermark. The structural hash reusesExpr::hash(gxhash128 over the term's byte span) rather than a hand-rolled hash — the hash is only a collision-bucket filter (exact bytes decide identity), so the swap is identity-preserving; modeled in Alloy (github.com/MesTTo/alloy-mork: fac22).