fix(resolver): project-wide proof pools take no work budget

Three pools hold a whole project's proofs under fixed caps, and running out of one
refuses the whole publication with no diagnostic:

  shared resolver  4M nodes, 64M work           cbm_shared_resolver_build
  graph buffer     16M nodes, 4G work           cbm_gbuf_new
  infra adapters   65536 nodes, 4M work         cbm_shared_resolver_adapter_init

proof_hash counts every hashed byte as work, so reaching a cap only means a large
enough repository. django reached the shared cap at 78580 proof nodes, and because
every proof hashes the project name, how soon a cap is reached also depends on the
length of the checkout path.

Measured, graph pool / shared pool work:

  redis       (967K occurrences)  524M / 1.2M
  neovim     (1.47M occurrences)  934M / 0.24M
  django      (672K occurrences) 1.36G / 133M    over the shared cap
  kubernetes (6.43M occurrences) 5.03G / 2.28G   over both, and the adapter cap

These pools hold one node per distinct project fact and each operation is linear in
its own text, so the totals follow the input and are not guarding against a runaway.
cbm_resolve_proof_pool_init_project sets no cap, so only the memory core can refuse.
With this kubernetes publishes, 355464 nodes against main's 355619.

Per-file pools keep their limits: they degrade the file's outcomes to LIMITED rather
than stop publication.

Signed-off-by: Martin Vogel <martin.vogel.tech@gmail.com>
This commit is contained in:
Martin Vogel committed 2026-11-01 00:29:44 +01:00
1 parent 2973a3277a
commit 9c946d51a8
4 files changed
+14 -5

No files matched your search

+3
View File
@@ -56,6 +56,9 @@ void cbm_resolve_proof_pool_init(cbm_resolve_proof_pool_t *pool, CBMArena *arena
.work_limit = work_limit ? work_limit : PROOF_DEFAULT_WORK,
.failure = arena ? CBM_RESOLVE_ANALYSIS_COMPLETE : CBM_RESOLVE_ANALYSIS_FAILED};
}
void cbm_resolve_proof_pool_init_project(cbm_resolve_proof_pool_t *pool, CBMArena *arena) {
cbm_resolve_proof_pool_init(pool, arena, SIZE_MAX, SIZE_MAX, UINT64_MAX);
}
const cbm_resolve_proof_view_t *cbm_resolve_proof_view(const cbm_resolve_proof_t *proof) {
return proof ? &proof->value : NULL;
}
+7
View File
@@ -90,6 +90,13 @@ typedef struct cbm_resolve_proof_pool {
* shared registry's arena. */
void cbm_resolve_proof_pool_init(cbm_resolve_proof_pool_t *pool, CBMArena *arena, size_t node_limit,
size_t premise_limit, uint64_t work_limit);
/* A pool whose population is the whole project: one node per distinct fact,
* each operation linear in its own text, so its total is a property of the
* input rather than a runaway. A cap here does not bound anything real; it
* refuses to publish a large enough repository, and because every hashed byte
* counts, how large depends on the length of the checkout path. Only the
* memory core can refuse this pool. */
void cbm_resolve_proof_pool_init_project(cbm_resolve_proof_pool_t *pool, CBMArena *arena);
const cbm_resolve_proof_view_t *cbm_resolve_proof_view(const cbm_resolve_proof_t *proof);
/* Exact pointer membership in this pool's full-key interned entries. A hash
* match alone never establishes ownership. The node must still be alive. */
+1 -2
View File
@@ -1075,8 +1075,7 @@ cbm_gbuf_t *cbm_gbuf_new(const char *project, const char *root_path) {
gb->next_id = SKIP_ONE;
gb->shared_ids = NULL;
cbm_arena_init(&gb->proof_arena);
cbm_resolve_proof_pool_init(&gb->proof_pool, &gb->proof_arena, 16u * 1024u * 1024u,
64u * 1024u * 1024u, UINT64_C(4294967296));
cbm_resolve_proof_pool_init_project(&gb->proof_pool, &gb->proof_arena);
gb->node_by_qn = cbm_ht_create_in(CBM_MEM_CLASS_GBUF_INDEX, CBM_SZ_256);
gb->by_id = NULL;
+3 -3
View File
@@ -1745,8 +1745,7 @@ cbm_shared_resolver_t *cbm_shared_resolver_build(const cbm_pipeline_ctx_t *ctx,
resolver->http_veto = cbm_ht_create(128);
resolver->http_domain_complete = true;
resolver->project = cbm_arena_strdup(&resolver->arena, ctx->project_name);
cbm_resolve_proof_pool_init(&resolver->proofs, &resolver->arena, 4000000, 4000000,
UINT64_C(64000000));
cbm_resolve_proof_pool_init_project(&resolver->proofs, &resolver->arena);
resolver->solver = cbm_resolve_solver_new(&resolver->arena, &resolver->proofs,
(cbm_resolve_solver_limits_t){0});
resolver->go_types =
@@ -3099,7 +3098,8 @@ bool cbm_shared_resolver_adapter_init(cbm_shared_resolver_adapter_t *adapter,
adapter->source_files = cbm_ht_create(0);
if (!adapter->source_files)
return adapter_fail(adapter);
cbm_resolve_proof_pool_init(&adapter->proofs, arena, 0, 0, 0);
/* One adapter serves every infrastructure input in the project. */
cbm_resolve_proof_pool_init_project(&adapter->proofs, arena);
size_t count = 0;
const cbm_resolve_file_t *files = cbm_gbuf_resolver_files(ctx->gbuf, &count);
for (size_t i = 0; i < count; i++) {