Symbol-level ABI-compatibility store lane (abi/): min/max compatible version via versioned-symbol containment - #4262
Merged
Merged
Conversation
s243a
marked this pull request as draft
September 13, 2026 04:55
s243a
added a commit
that referenced
this pull request
Sep 13, 2026
…s, explicit evidence Addresses Astra's REQUEST-CHANGES review of #4262. Direction unchanged (three evidence tiers; a driver above the frozen resolver); model + ingest rebuilt. 1. Identity is the exact (soname, symbol, version-node) triple, stored and matched by string equality; no collapse to bare names, no numeric intro. 2. Every obligation is preserved (non-numeric nodes, unversioned and weak references); NEEDED is checked; evidence completeness is explicit (evidence.jsonl) and a missing/unreadable ELF is a loud exit-3 failure that records INCOMPLETE evidence instead of an empty success. Verdicts are tri-state: compatible(exact|extrapolated) / incompatible / unknown. 3. Requirements are attributed via the ELF version INDEX (.gnu.version -> .gnu.version_r), so two libraries sharing a node name (COMMON_1) no longer collide. 4. The Debian package-version axis reuses debian/deb_parse + the frozen resolver:version_lt/2 on deb/3 (epoch, tilde, revision); ELF nodes are an unordered label axis. `.symbols` minimums are documented as curated lower bounds, not introduction dates (below_floor is reported distinctly). 5. Ranges are computed over the actual release axis (apt-cache madison + dpkg); [min,max] ends are compatible by construction (range(1,5) bug gone). 6. Cross-check compares exact sym@node sets: 3006/3006 (100%); corrected per-name earliest-row figure 2478/2478 (100%). The false "glibc 2.34 merge divergence" explanation is removed from the docs. 7. `.symbols` templates: (optional)/(arch=..) processed (arch needs --arch); (symver)/(regex)/(c++)/quoted patterns/#include rejected loudly. Verification (Ubuntu 22.04.5, libc6 2.35-0ubuntu3.15, /bin/ls): computed floors 2.34 / 3.1~ equal coreutils' declared Pre-Depends; gcc-built fixtures for foo@LIB_1-vs-foo@LIB_2 (loader confirms "undefined symbol: foo, version LIB_1"), COMMON_1 cross-attribution, PUBLIC + unversioned obligations, and a missing ELF. test_abi.pl: 63 passed, 0 failed. REVIEW_NOTES.md maps each review point to code + proving fixture. Frozen resolver files untouched. Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01RoXjhStCqoig6944pVNBGe
s243a
force-pushed
the
claude/abi-symbol-store
branch
from
September 13, 2026 05:29
23bf873 to
0afcce3
Compare
Extend resolution from coarse version constraints to fine-grained ABI
compatibility at the SYMBOL level: for a binary, compute the min AND max
(newest) compatible library version via versioned-symbol-set containment --
the [min,max] range ldd won't give you. A driver above the frozen spec;
resolver.pl / resolver_store.pl untouched.
Model: a library version PROVIDES exported versioned symbols {sym@ver} +
soname; a binary REQUIRES referenced versioned symbols + NEEDED sonames;
compatible = soname match AND requires subset provides. Each symbol is stored
once as a validity interval [intro, inf) within a soname -- the same interval
store as snapshot membership, one level down.
- ingest_symbols.mjs -- 3-tier ingest -> P/2 interval JSONL:
(1) Packages `Depends` = the coarse min, free from the repo index (noted);
(2) `.symbols` control-member -> symprov intervals [soname|sym, intro#inf]
(curated `minimum-version` = intro; zero binary download; the common
Debian/Ubuntu path); `symbols-dir` batches a whole dpkg info dir;
(3) readelf fallback -- `elf`/`requires` for any ELF anywhere.
- abi_resolve.pl -- new module (reuses resolver:version_lt/2): abi_min (the
verneed floor), provides_at (intro =< V interval lookup), abi_compatible
(name-intro containment, the max-side predicate), newest_abi_compatible,
abi_range. + abi_cli.pl driver.
- test_abi.pl + run_abi_verify.sh -- real-data harness.
- README.md + SYMBOL_ABI_HOWTO.md -- model, the 3 ingest tiers, the min/max
epistemics (symbol-absence = hard veto, presence = defeasible maybe),
Debian/Ubuntu/any-ELF coverage, package-manager vs coding-agent consumers.
Verified on this machine (Ubuntu 22.04), 8/8 checks: libc6 .symbols -> 4827
symprov rows (3006 for libc.so.6); /bin/ls -> 112 symreq, NEEDED
[libselinux.so.1, libc.so.6]; abi_min(/bin/ls, libc.so.6) = 2.34;
abi_range = range(2.34, 2.35); simulating getenv removed at 2.30 caps the max
at 2.29, so min 2.34 > max 2.29 -> no_candidate. Batch across all 562 .symbols
= 256,225 interval rows / 2,231 sonames -- the genuine memory-pressure dataset.
Note: readelf-derived intro vs curated .symbols agree on 91.7% of shared
libc symbols; every divergence is the glibc 2.34 pthread/rt-into-libc merge
(curated .symbols dates those to 2.34, when they entered libc.so.6's stable
ABI; raw ELF keeps the historical libpthread tag) -- the curated metadata is
the more ABI-faithful source, which is why the .symbols tier is preferred.
Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01RoXjhStCqoig6944pVNBGe
…s, explicit evidence Addresses Astra's REQUEST-CHANGES review of #4262. Direction unchanged (three evidence tiers; a driver above the frozen resolver); model + ingest rebuilt. 1. Identity is the exact (soname, symbol, version-node) triple, stored and matched by string equality; no collapse to bare names, no numeric intro. 2. Every obligation is preserved (non-numeric nodes, unversioned and weak references); NEEDED is checked; evidence completeness is explicit (evidence.jsonl) and a missing/unreadable ELF is a loud exit-3 failure that records INCOMPLETE evidence instead of an empty success. Verdicts are tri-state: compatible(exact|extrapolated) / incompatible / unknown. 3. Requirements are attributed via the ELF version INDEX (.gnu.version -> .gnu.version_r), so two libraries sharing a node name (COMMON_1) no longer collide. 4. The Debian package-version axis reuses debian/deb_parse + the frozen resolver:version_lt/2 on deb/3 (epoch, tilde, revision); ELF nodes are an unordered label axis. `.symbols` minimums are documented as curated lower bounds, not introduction dates (below_floor is reported distinctly). 5. Ranges are computed over the actual release axis (apt-cache madison + dpkg); [min,max] ends are compatible by construction (range(1,5) bug gone). 6. Cross-check compares exact sym@node sets: 3006/3006 (100%); corrected per-name earliest-row figure 2478/2478 (100%). The false "glibc 2.34 merge divergence" explanation is removed from the docs. 7. `.symbols` templates: (optional)/(arch=..) processed (arch needs --arch); (symver)/(regex)/(c++)/quoted patterns/#include rejected loudly. Verification (Ubuntu 22.04.5, libc6 2.35-0ubuntu3.15, /bin/ls): computed floors 2.34 / 3.1~ equal coreutils' declared Pre-Depends; gcc-built fixtures for foo@LIB_1-vs-foo@LIB_2 (loader confirms "undefined symbol: foo, version LIB_1"), COMMON_1 cross-attribution, PUBLIC + unversioned obligations, and a missing ELF. test_abi.pl: 63 passed, 0 failed. REVIEW_NOTES.md maps each review point to code + proving fixture. Frozen resolver files untouched. Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01RoXjhStCqoig6944pVNBGe
…, atomic ingest)
Sol's REQUEST-CHANGES on the redesigned symbol-level ABI lane, all points:
P1a Provider bounds are tied to their evidence row (since/4 carries the
evidence release; at/2 = its own) and every evidence row is aggregated
per identity (ident_status/5: at-release decides, nearest below/above
combined) instead of `->` committing to the first symprov/4. since(2.0)
+ at(1.0) at release 1.0 is compatible(exact), not below_floor. C7*,
A25, C7e (a bound without its evidence row is not evidence).
P1b Ingest keeps the @ vs @@ distinction from the .gnu.version hidden bit
(cross-checked against the name); rows carry default|nondefault|
unproven. An unversioned reference is satisfied only by Base or a
default export; .symbols-only rows yield unknown; a nondefault-only
export is a hard no_default_export veto. The loader's oldest-node rule
(verdef index 2 binds even when hidden) is encoded and verified with the
loader. D10/D10b/D10c (gcc libhid fixtures), C8*, A7b/A7c.
P1c (optional) rows are exports only when --elf cross-checks them against
the binary; without --elf the file is rejected. D8 inverted: the
optional row absent from the ELF is NOT stored. libc6's .symbols is now
ingested with --elf libc.so.6 (0 dropped, 0 disagreements).
P2a symbols-dir: a file with an unresolvable block is rejected atomically
(exit 3, no rows, no evidence). D11 + fixtures/batch.
P2b Tag whitelist (every other tag rejects the file); --release validated
by the same Debian-version gate everywhere. D9 tmpl_unknown_tag,
bad_release (symbols-file and elf).
P2c crosscheck.mjs fails on empty inputs / zero denominators.
P2d soname_mismatch only under a declared replaces(New, Old) row
(replaces.jsonl, `ingest replaces`); no stem heuristic. C9*, A19b.
P3 The dotted-version comparator over node names is gone; per-name
comparison is node-set equality; fixtures/crosscheck pins the case.
Res. compatible(curated) for .symbols-derived presence; exact only for
readelf at that release.
Also: absence from complete evidence propagates down (missing for Rel =< R1)
but not up (unknown for later releases); an observed present-then-absent
gives unknown(dropped_between). REVIEW_NOTES.md maps each point to the fix
and its fixture; README/HOWTO updated. run_abi_verify.sh: 92 passed, 0
failed, 0 skipped. Frozen resolver.pl / resolver_store.pl / debian/ untouched.
Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01RoXjhStCqoig6944pVNBGe
s243a
force-pushed
the
claude/abi-symbol-store
branch
from
September 13, 2026 06:23
0afcce3 to
0e4253a
Compare
…b-version gate, P3 fixture)
Sol's re-review closed five of eight findings and requested changes on four,
all rooted in one principle: a `.symbols` file is a curated LOWER-BOUND list,
not a complete export set, so its ABSENCE proves nothing.
- P1 curated absence (abi_resolve.pl:289): a plain `.symbols` ingest (no --elf)
is now tagged `curated`, not `complete`; only readelf or an --elf cross-check
is `complete`. prov_usable/4 + ev_says/5 let curated evidence establish
PRESENCE but never ABSENCE (a curated omission -> unknown, never missing).
Fixtures C10/C10b/C10c, A26 (real libselinux1), D7.
- P1 contradictory floor (abi_resolve.pl:311): a curated minimum above its
evidence release is rejected at ingest (debLe, exit 3) and at load
(assert_symprov rel_le(Deb,R0)). Fixtures C11/C11b, contradictory.symbols.
- P2 deb-version gate (ingest_symbols.mjs:114): validDebVersion() replaces the
loose regex and rejects 1:, 1-, 1::2 the way dpkg --validate-version does.
Fixtures bad_release_{1:,1-,1::2}.
- P3 crosscheck fixture: added a numeric-collapse pair (LIBX_2.1/LIBX_2.10) and
a negative elf_numcollapse fixture that only a reintroduced numeric node
comparator would pass.
Curated presence stays compatible(curated) (distinct from exact); below_floor
remains a declared-minimum veto that never overrides a direct presence
observation. Frozen resolver.pl / resolver_store.pl / debian/ untouched.
run_abi_verify.sh: 98 passed, 0 failed, 0 skipped.
Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01RoXjhStCqoig6944pVNBGe
…obustness nits An independent Fable re-verification of the previous commit found that widening the unversioned-path completeness gate to prov_usable/4 let a curated-only NEEDED object fall through to a hard missing veto -- the very curated-absence bug, reintroduced on the unversioned side (invisible to the harness because /bin/ls's unversioned refs are all WEAK). - unversioned_status/7: gate the missing veto on \+ prov_evidence(S,_,_,complete) for the NEEDED object; a curated-only lib now yields unknown(absent_from_incomplete_evidence), never missing. New fixtures C12/C12b (unversioned req vs curated-only omission -> unknown; vs complete omission -> missing). - Robustness (Fable-flagged): debLe die()s clearly if dpkg is absent from PATH; load_abi_store/1 clears the partial store when a row throws; removed the now dead bound_evidence/4. Frozen files untouched. run_abi_verify.sh: 100 passed, 0 failed, 0 skipped. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01RoXjhStCqoig6944pVNBGe
…, dpkg-equivalence) Astra (original reviewer) re-reviewed and found new issues, the key one by ingesting live libstdc++.so.6. All real findings fixed and fixture-proven. P1: - ingest: elfProvides now keeps STB_GNU_UNIQUE exports (was GLOBAL/WEAK only); dropping them (106 in libstdc++.so.6) caused false missing vetoes. Regression ingests libstdc++ and asserts a real UNIQUE export is stored. - abi_resolve unversioned_status: a missing veto now requires absence ESTABLISHED at Rel (complete evidence at a release >= Rel); complete evidence only below Rel -> unknown(absence_unestablished), never a veto (C14/C14b). - abi_resolve: binding_at/6 ties the default-version binding to the evidence applicable at Rel, so a stale/orphaned default row cannot yield a false compatible(exact) for an unversioned ref (C15/C15b/C15c). P2: - ingest archSelects: only exact arch names (+ !neg); dpkg wildcard patterns (any, linux-any, any-*) are rejected, not mis-selected (tmpl_arch_wild). - ingest validDebVersion: epoch capped at 2147483647 (dpkg's limit). - abi_resolve: hypothetical unversioned drop is node- and release-aware, like the versioned path (C13/C13b). P3 (documented, not changed): crosscheck per-name is redundant with exact identity (guarded); debLe uses dpkg (reference impl) while the resolver orders via frozen version_lt and the authoritative floor check is Prolog rel_le. Frozen files untouched. run_abi_verify.sh: 108 passed, 0 failed, 0 skipped. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01RoXjhStCqoig6944pVNBGe
…R1/R2) A Fable re-verification of the Astra-fix commit caught two regressions the binding_at rework introduced; the harness missed them because every unversioned .symbols test queried AT the evidence release. - R1 (false missing veto): binding_at took the binding only from the row AT Rel or BELOW, but ident_status can credit a curated .symbols floor row ABOVE Rel (combine, Min =< Rel). binding_at now also selects that above curated row. Fixtures C16/C16b (unversioned ref BELOW a curated floor -> compatible(curated)). - R2 (cross-axis false unknown): the missing-veto coverage gate compared So's query release with a sibling's own evidence release. The gate now applies to the queried So only; siblings are evaluated at their own release. Fixture C17. Also cleaned a stray NUL byte in the debLe cache-key string (ASCII escape in source; runtime key unchanged). Frozen files untouched. run_abi_verify.sh: 111 passed, 0 failed, 0 skipped. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01RoXjhStCqoig6944pVNBGe
…-review 2) Astra re-reviewed and found more unversioned-path issues, all rooted in binding_at being a separate re-derivation from ident_status and the veto branches not being uniformly release-gated. Rather than patch case-by-case, the binding is unified into the aggregation. P1: - ident_status now returns provided(Basis, Binding); says_status/combine carry the binding from the SAME row that establishes presence, so binding and presence can never diverge. Conflicting cross-tier bindings -> ambiguous -> unknown (default_binding_conflict), never a veto or confident compat. binding_at deleted; unversioned_in/unproven/nondefault + new unversioned_ambiguous read the binding from ident_status. Fixture C19. - no_default_export is now release-gated too: the coverage gate precedes BOTH veto branches, so a nondefault export seen only BELOW the query release -> unknown, not a veto. Fixtures C18/C18b. P2: - archSelects validates every term first (an early match/negation can't skip a later unsupported term) and rejects tuples/GNU forms/comma-lists/any-wildcards (tmpl_arch_tuple, tmpl_arch_list). - arch-bits/arch-endian use explicit ARCH_BITS/ARCH_ENDIAN tables; a non-tabulated --arch rejects the row rather than guessing (arch_bits_unknown). - test isolation: epoch cap proven via the releases command (epoch_releases); hyp-drop node/release matching isolated by C13c/C13d. Frozen files untouched. run_abi_verify.sh: 118 passed, 0 failed, 0 skipped. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01RoXjhStCqoig6944pVNBGe
…Fable M2/M3) A Fable re-verification confirmed the binding unification introduced no regression but surfaced two pre-existing false verdicts, now fixed. - M2 (false compatible): ident_status/5 was mode-dependent -- combine/4 and says_status/3 carry their cut AFTER head unification, so a caller passing a bound Status (e.g. provided(_,default)) could skip the clause the unbound call fires and match a later one, giving compatible(extrapolated) for a symbol observed DROPPED. Fixed: ident_status computes into a fresh variable via ident_status_/5, then unifies -- every caller sees the one mode-independent status. Fixture C20. - M3 (false no_default_export): combine clause 3 extrapolated the below-row binding and ignored a disagreeing above row. Fixed: merge_binding/3 marks two conflicting DEFINITE bindings ambiguous (-> unknown); unproven is no-info, never a conflict. Fixture C21. Frozen files untouched. run_abi_verify.sh: 120 passed, 0 failed, 0 skipped. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01RoXjhStCqoig6944pVNBGe
Astra re-review found the M3 change regressed combine/4 clause 3: extrapolating a present-below row past a NON-covering above row used merge_binding, which promoted an `unproven` below binding to a future definite above binding -> a false compatible where it should stay unknown(default_binding_unproven). - combine clause 3 now uses extrapolate_binding/3: keep the below binding; flag ambiguous only when both are definite and differ; never import the above binding. Clause 2 (covering-curated, where the above floor applies at Rel) keeps merge_binding. Fixtures C22 (curated-unproven below + complete default-since above -> unknown, not compatible), C22b (ELF default above). C19/C21 still pass (definite conflicts -> ambiguous). - Cleaned a stray NUL byte in REVIEW_NOTES.md. Frozen files untouched. run_abi_verify.sh: 122 passed, 0 failed, 0 skipped. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01RoXjhStCqoig6944pVNBGe
s243a
marked this pull request as ready for review
September 14, 2026 05:42
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.
Symbol-level ABI-compatibility store lane (
examples/pkg_resolver/abi/)Extends the package resolver from coarse version constraints (
libfoo (>= 2.0)) to fine-grained ABI compatibility at the symbol level, computing the real[min, max]compatible library-version range for a binary via versioned-symbol containment. It sits above the frozen resolver — it only importsresolver:version_lt/2anddebian/deb_parse:parse_deb_version/2;resolver.pl,resolver_store.pl, anddebian/are untouched.Model
(soname, symbol, version-node)triple — nodes are opaque ELF labels matched by string equality, never parsed numerically or collapsed to bare names.version_lt/2overdeb/3)..gnu.versionindex, not by version name, so two libraries sharing a node name (e.g.COMMON_1) never collide.complete(readelf, or a.symbolsfile cross-checked with--elf: absence is a fact) vs.curated(a plain.symbolslower-bound list: presence is evidence, absence proves nothing). A hard veto (missing/below_floor/no_default_export/soname_mismatch) requires complete, index-attributed evidence; otherwise the verdict isunknown.@@/index-2 vs. hidden@) is carried through the evidence aggregation so an unversioned reference binds only to aBaseor default export; conflicting cross-tier bindings resolve tounknown, never a false verdict.compatible(exact | curated | extrapolated)/incompatible([...])/unknown([...])/not_needed(So).Contents
Prolog resolver (
abi_resolve.pl), ingest (ingest_symbols.mjs:.symbols+readelf, atomic loud failures), tier cross-check (crosscheck.mjs), CLI, the fixture harness (run_abi_verify.sh), andtest_abi.pl(real-data / version-axis / model / gcc-built-ELF fixtures).SYMBOL_ABI_HOWTO.mdandREADME.mddocument the model with worked examples on real Ubuntu data;REVIEW_NOTES.mdmaps every review finding → fix → proving fixture.Verification
run_abi_verify.sh: 122 passed, 0 failed, 0 skipped on real Ubuntu 22.04 data plus gcc-built ELF fixtures (loader used as ground truth). Frozen resolver/store/debian diff againstmainis empty.Review
Reviewed across ten rounds by three independent models — original-Astra (
gpt-6-astra), Sol (gpt-5.6-sol), and Fable — each finding real defects that are fixed and fixture-proven (seeREVIEW_NOTES.md); final Astra verdict APPROVE.🤖 Generated with Claude Code
https://claude.ai/code/session_01RoXjhStCqoig6944pVNBGe