feat(cli): add memory budget option for extract/update (#3011)

[adityachaudhary99]

Closes #3011

Adds a first-class memory budget for extraction/update:

• --memory-limit-mb CLI flag (or GRAPHIFY_MEMORY_LIMIT_MB env), flag wins
• Low-overhead sampler polls aggregate process-tree RSS (CLI plus worker children; /proc with psapi/rusage fallback)
• On breach: worker children terminated, hard exit with code EXIT_MEMORY_LIMIT=3, message reporting limit/observed/phase - never publishing partial graph.json

Default path (no flag/env) is a zero-cost no-op. cgroup-v2 auto-detection deliberately left out of this minimal scope.

[graphify-labs]

Graphify reviewed this change.

Worth a look — the grounded gate found no coupling regressions or blocking issues, but 5 advisory finding(s) below merit a look before merge.

Formal verification. 3 change(s) tested, no difference found (not proven).

---

Graphify review — findings

Adds an opt-in process-tree memory budget for graphify extract, enabled via --memory-limit-mb N or GRAPHIFY_MEMORY_LIMIT_MB, that samples aggregate RSS twice a second and, on breach, terminates child workers and exits with stable code 3 before graph.json or the manifest are written so a killed run is never published as success. start_memory_budget_monitor arms the sampler ahead of the first heavy stage (flag wins over env; absent both it's a no-op), and set_extraction_phase tags scan/AST/semantic/graph-build so a breach report names the phase that overran. resolve_memory_limit_mb treats malformed or non-positive values as off rather than fatal, RSS is read tree-wide from /proc on Linux and falls back to this process's own RSS elsewhere, and graphify update arms the monitor too since its rebuild runs inline.

Worth a look

• Test arms a live hard-exit monitor with a likely-too-low memory limit — tests/test_extract_memory_limit.py:58 · Escalate · high
  • agreed by 2 of 2 members but NOT verified (no proof, no reproducing execution) — consensus is not a verdict; needs human review
• os._exit from sampler thread bypasses cleanup and can corrupt partial output files — graphify/memory_budget.py · Escalate · medium
  • agreed by 2 of 2 members but NOT verified (no proof, no reproducing execution) — consensus is not a verdict; needs human review
• Worker children termination not synchronized with child spawning — graphify/memory_budget.py · Escalate · medium
  • agreed by 2 of 2 members but NOT verified (no proof, no reproducing execution) — consensus is not a verdict; needs human review
• Explicit non-positive memory limit arms an impossible budget — graphify/memory_budget.py:44 · Escalate · medium
  • agreed by 2 of 2 members but NOT verified (no proof, no reproducing execution) — consensus is not a verdict; needs human review
• Stopped memory monitor can still abort after an in-flight sample — graphify/memory_budget.py:174 · Escalate · medium
  • agreed by 2 of 2 members but NOT verified (no proof, no reproducing execution) — consensus is not a verdict; needs human review

Analysis details — impact, health, verification

Impact & health

Graphify review

Impact — 287 functions depend on the 99 functions this change touches.

Health — this change adds coupling hotspots:

• new: dispatch_command() — 2 callers, 121 callees
• new: _stale_graph_sources() — 7 callers, 6 callees
• new: _run_hook_guard() — 4 callers, 7 callees
• new: test_poisoned_manifest_is_healed() — 0 callers, 6 callees

Verification — 287 functions in the blast radius were not formally verified this run (proofs are advisory here).

Gate & verification

graphify gate

PASS — objectively clean (no health regressions, tests not run — proofs not run this pass (advisory)). Grounded, not self-assessed.

Advisory (not blocking):

• verification_scope: 287 function(s) in the blast radius were not formally verified this run

Formal verification

Could not verify: Could not verify load\_cached.

The verifier did not have enough to check load\_cached, so it is saying so rather than guessing. No false assurance is the whole point.

Guarantee: No guarantee either way, this is an honest abstention, not a pass.

Note: Reason: parameter `path` is annotated `Path` — outside the synthesizable primitive/collection set

Could not verify: Could not verify save\_semantic\_cache.

The verifier did not have enough to check save\_semantic\_cache, so it is saying so rather than guessing. No false assurance is the whole point.

Guarantee: No guarantee either way, this is an honest abstention, not a pass.

Note: Reason: parameter `root` is annotated `Path` — outside the synthesizable primitive/collection set

Could not verify: Could not verify dispatch\_command.

The verifier did not have enough to check dispatch\_command, so it is saying so rather than guessing. No false assurance is the whole point.

Guarantee: No guarantee either way, this is an honest abstention, not a pass.

Note: Reason: not verifiable: all 23 sampled inputs raised on both versions — the function never executed, so 'no divergence' would be vacuous (mostly SystemExit — names the real obstacle, not a sampling gap)

Could not verify: Could not verify \_stamped\_manifest\_files.

The verifier did not have enough to check \_stamped\_manifest\_files, so it is saying so rather than guessing. No false assurance is the whole point.

Guarantee: No guarantee either way, this is an honest abstention, not a pass.

Note: Reason: parameter `root` is annotated `Path` — outside the synthesizable primitive/collection set

No difference found (not proven): No behavior difference found in to\_obsidian (not a proof).

The verifier ran both versions of to\_obsidian on many inputs and saw identical behavior every time. Strong evidence the change is safe, but evidence, not a proof.

Guarantee: Empirical: differential testing (both versions run on many generated inputs). A divergence on an untested input remains possible, so this is 'no counterexample found', not 'proven equivalent'.

Note: An input the sampler did not try could still differ.

Could not verify: Could not verify extract.

The verifier did not have enough to check extract, so it is saying so rather than guessing. No false assurance is the whole point.

Guarantee: No guarantee either way, this is an honest abstention, not a pass.

Note: Reason: parameter `cache_root` is annotated `Path | None` — outside the synthesizable primitive/collection set

Could not verify: Could not verify \_rewire\_unique\_stub\_nodes.

The verifier did not have enough to check \_rewire\_unique\_stub\_nodes, so it is saying so rather than guessing. No false assurance is the whole point.

Guarantee: No guarantee either way, this is an honest abstention, not a pass.

Note: Reason: not verifiable: the input domain has 81 values but only 9 distinct were tested — a small finite domain must be EXHAUSTED, not sampled (an untested input could invert the result)

Could not verify: Could not verify extract\_bash.

The verifier did not have enough to check extract\_bash, so it is saying so rather than guessing. No false assurance is the whole point.

Guarantee: No guarantee either way, this is an honest abstention, not a pass.

Note: Reason: parameter `path` is annotated `Path` — outside the synthesizable primitive/collection set

Could not verify: Could not verify extract\_commonlisp.

The verifier did not have enough to check extract\_commonlisp, so it is saying so rather than guessing. No false assurance is the whole point.

Guarantee: No guarantee either way, this is an honest abstention, not a pass.

Note: Reason: parameter `path` is annotated `Path` — outside the synthesizable primitive/collection set

Could not verify: Could not verify \_extract\_generic.

The verifier did not have enough to check \_extract\_generic, so it is saying so rather than guessing. No false assurance is the whole point.

Guarantee: No guarantee either way, this is an honest abstention, not a pass.

Note: Reason: parameter `path` is annotated `Path` — outside the synthesizable primitive/collection set

Could not verify: Could not verify extract\_julia.

The verifier did not have enough to check extract\_julia, so it is saying so rather than guessing. No false assurance is the whole point.

Guarantee: No guarantee either way, this is an honest abstention, not a pass.

Note: Reason: parameter `path` is annotated `Path` — outside the synthesizable primitive/collection set

Could not verify: Could not verify extract\_powershell.

The verifier did not have enough to check extract\_powershell, so it is saying so rather than guessing. No false assurance is the whole point.

Guarantee: No guarantee either way, this is an honest abstention, not a pass.

Note: Reason: parameter `path` is annotated `Path` — outside the synthesizable primitive/collection set

Could not verify: Could not verify \_load\_tsconfig\_aliases.

The verifier did not have enough to check \_load\_tsconfig\_aliases, so it is saying so rather than guessing. No false assurance is the whole point.

Guarantee: No guarantee either way, this is an honest abstention, not a pass.

Note: Reason: parameter `start_dir` is annotated `Path` — outside the synthesizable primitive/collection set

Could not verify: Could not verify \_load\_tsconfig\_base\_url.

The verifier did not have enough to check \_load\_tsconfig\_base\_url, so it is saying so rather than guessing. No false assurance is the whole point.

Guarantee: No guarantee either way, this is an honest abstention, not a pass.

Note: Reason: parameter `start_dir` is annotated `Path` — outside the synthesizable primitive/collection set

Could not verify: Could not verify \_merge\_decl\_def\_classes.

The verifier did not have enough to check \_merge\_decl\_def\_classes, so it is saying so rather than guessing. No false assurance is the whole point.

Guarantee: No guarantee either way, this is an honest abstention, not a pass.

Note: Reason: not verifiable: the input domain has 81 values but only 9 distinct were tested — a small finite domain must be EXHAUSTED, not sampled (an untested input could invert the result)

Could not verify: Could not verify extract\_sql.

The verifier did not have enough to check extract\_sql, so it is saying so rather than guessing. No false assurance is the whole point.

Guarantee: No guarantee either way, this is an honest abstention, not a pass.

Note: Reason: parameter `path` is annotated `Path` — outside the synthesizable primitive/collection set

Could not verify: Could not verify extract\_zig.

The verifier did not have enough to check extract\_zig, so it is saying so rather than guessing. No false assurance is the whole point.

Guarantee: No guarantee either way, this is an honest abstention, not a pass.

Note: Reason: parameter `path` is annotated `Path` — outside the synthesizable primitive/collection set

Could not verify: Could not verify bisect\_slice.

The verifier did not have enough to check bisect\_slice, so it is saying so rather than guessing. No false assurance is the whole point.

Guarantee: No guarantee either way, this is an honest abstention, not a pass.

Note: Reason: parameter `fs` is annotated `FileSlice` — outside the synthesizable primitive/collection set

No difference found (not proven): No behavior difference found in expand\_oversized\_files (not a proof).

The verifier ran both versions of expand\_oversized\_files on many inputs and saw identical behavior every time. Strong evidence the change is safe, but evidence, not a proof.

Guarantee: Empirical: differential testing (both versions run on many generated inputs). A divergence on an untested input remains possible, so this is 'no counterexample found', not 'proven equivalent'.

Note: An input the sampler did not try could still differ.

Could not verify: Could not verify is\_splittable\_text.

The verifier did not have enough to check is\_splittable\_text, so it is saying so rather than guessing. No false assurance is the whole point.

Guarantee: No guarantee either way, this is an honest abstention, not a pass.

Note: Reason: parameter `path` is annotated `Path` — outside the synthesizable primitive/collection set

Could not verify: Could not verify read\_slice\_text.

The verifier did not have enough to check read\_slice\_text, so it is saying so rather than guessing. No false assurance is the whole point.

Guarantee: No guarantee either way, this is an honest abstention, not a pass.

Note: Reason: parameter `fs` is annotated `FileSlice` — outside the synthesizable primitive/collection set

Could not verify: Could not verify \_estimate\_file\_tokens.

The verifier did not have enough to check \_estimate\_file\_tokens, so it is saying so rather than guessing. No false assurance is the whole point.

Guarantee: No guarantee either way, this is an honest abstention, not a pass.

Note: Reason: parameter `unit` is annotated `'Path | FileSlice'` — outside the synthesizable primitive/collection set

No difference found (not proven): No behavior difference found in \_run\_cli (not a proof).

The verifier ran both versions of \_run\_cli on many inputs and saw identical behavior every time. Strong evidence the change is safe, but evidence, not a proof.

Guarantee: Empirical: differential testing (both versions run on many generated inputs). A divergence on an untested input remains possible, so this is 'no counterexample found', not 'proven equivalent'.

Note: An input the sampler did not try could still differ.

Could not verify: Could not verify \_build\_server.

The verifier did not have enough to check \_build\_server, so it is saying so rather than guessing. No false assurance is the whole point.

Guarantee: No guarantee either way, this is an honest abstention, not a pass.

Note: Reason: not verifiable: all 23 sampled inputs raised on both versions — the function never executed, so 'no divergence' would be vacuous

· 4 more finding(s) on lines outside this diff (see the check run).