code/docs/DEPENDENCY_POLICY.md

Dependency policy

align runs on torch, triton, numpy, safetensors. That is the whole list. It is enforced by tests/test_dependency_firewall.py (AST scan of every module, lazy imports included), not by convention.

What was removed, and what replaced it

Removed	Was used for	Replacement in align
transformers	tokenizer, MistralConfig, HF-layout load for the golden regression	align/tokenizer/ (pure-Python BPE from tokenizer.json, parity-certified), align/model/hf_config.py (own config.json read/write), golden regression loads through align.model
omegaconf	dataclass+YAML config with struct mode	align/config.py: dataclass + stdlib tomllib, struct mode (unknown keys raise), dotted CLI overrides. Configs are .toml
datasets	HF streaming	align/data/hub.py: HTTP streaming of JSONL/parquet row groups from the HF hub via urllib; parquet ingest is a one-time step behind the ingest extra
pyarrow	parquet	only align/data/ingest_parquet.py (whitelisted, lazy, one-time ingest into the repo's own shard format)
math_verify + sympy	answer equivalence	align/verify/: boxed extraction, normalisation, exact rational/decimal/interval/set equivalence, small expression evaluator. Ceiling-tested
wandb	metrics	align/utils/tracking.py: JSONL history.jsonl (mtime is the liveness signal), optional stdout
bitsandbytes	8-bit AdamW (optimizer.name = "adamw8bit", named by every shipped full-FT config)	align/train/adamw8bit.py: pure-torch block-wise 8-bit AdamW (Dettmers et al. 2022, arXiv:2110.02861), codebook and quantize/dequantize in align/train/quant8.py. Dynamic 256-entry maps, block 2048, uint8 codes + fp32 absmax per block, fp32 state below 4096 elements, no master copy (stochastic rounding into bf16 params), DTensor/FSDP2 local-shard stepping, global pre-clip grad norm, bit-exact resume. 2 + 8/block = 2.004 B/param on the device, zero host RSS. make_optimizer builds it for adamw8bit; OffloadAdamW (align/train/offload_adamw.py) stays the RunConfig default but cannot launch 7.25B/4 ranks (4x over its pinned-staging cap, ~105GB host RSS)
peft	LoRA adapters for the PPO value head	align/ppo/lora.py (own LoRA on nn.Linear)
deepspeed	ZeRO in the old PRM-PPO	banned. FSDP2 via torch (align/train/fsdp.py). (Also: ZeRO-3 + Adafactor silently did not train, 2026-08.)
trl	--	banned; never was a dependency of this lineage
vllm / ray	high-throughput rollout	optional, isolated in extras/vllm_rollout/ with its own venv; talks to the trainer only via align/rollout/protocol.py. The core rollout is align/rollout/native.py (torch KV-cache sampler)
matplotlib	plots	dropped from the alignment package (plots live in the interp repo)

Rules

1. New runtime dependency => a dated entry in this file and a change to ALLOWED in the firewall test, in the same commit.
2. Optional extras live in exactly one file each, imported lazily, whitelisted by path.
3. Parity tests against the legacy stack (transformers tokenizer, math_verify) run under the legacy venv as an oracle (pytest -m oracle); the oracle is never imported at runtime.

External binary: Lean 4 toolchain (2026-10-12)

Track L's strict proof verifier (align/verify/lean/, docs/LEAN_VERIFIER.md) needs a real Lean kernel. This is not a Python dependency: nothing under align/ or scripts/ imports it, the firewall's ALLOWED set is unchanged, and the Python side of the verifier is stdlib-only. It is an external toolchain reached only through subprocess, the same category as git, nvidia-smi or du.

What	elan 4.2.4 -> Lean v4.9.0-rc1 (leanprover/lean4), Mathlib d1d1e4b72c6e (2024-06-12), leanprover-community/repl tag v4.9.0-rc1 (7df77c0a1c91)
Why this pin	It is the environment Goedel-Prover-V2 (primary prover base), DeepSeek-Prover-V1.5 and Goedel-Prover-V1 verify against: V2's mathlib4 submodule is xinhjBrant/mathlib4@2f65ba7f, one commit on top of upstream d1d1e4b7 that only adds DeepSeek's REPL fork to lakefile.lean. We pin the upstream parent because Mathlib's prebuilt .olean cache is keyed on a hash that includes lakefile.lean; the edit would orphan the cache and force a multi-hour Mathlib build
Where	/apps/development/rlhf/lean/ (ELAN_HOME, MATHLIB_CACHE_DIR, XDG_CACHE_HOME, TMPDIR all redirected there; nothing is written to $HOME, / or /tmp). ~5.8 GB
Installed by	scripts/lean_setup.sh (idempotent, every network/build step under timeout, preflighted against the host rules); records PINS.json
How it is reached	align.verify.lean.toolchain finds the install; repl_pool spawns the REPL as a child with a minimal environment (PATH, LEAN_PATH, LD_LIBRARY_PATH, LEAN_SYSROOT; no tokens, no $HOME), its own session, prlimit --as/--fsize/--core, and a memory watchdog
Absent toolchain	find_toolchain() raises ToolchainNotFound naming the setup command. Tests that need it are @pytest.mark.slow and skip; everything else uses a fake REPL binary
Network	install time only (github.com, releases.lean-lang.org, Mathlib cache host); the verifier itself makes no network access
Licences	Lean 4, Mathlib, REPL, elan: Apache-2.0
Rule it follows	Rule 1 above is about runtime Python dependencies. An external binary needs (a) a dated entry here, (b) a pinned version and an install script, (c) subprocess-only access, (d) a skip-when-absent test path, (e) a resource cap (the report counts a Lean pool as a heavy job: one REPL = 0.25 GiB private + a shared 3.4 GiB .olean mapping, measured)

Vendored assets (2026-10-12)

assets/tokenizer/mistral-7b-v0.3/ holds the four Mistral-7B-v0.3 tokenizer files (~2.6MB, Apache-2.0; md5s in its PROVENANCE.md). They are byte-identical to the HF snapshot's, and exist because (a) the HF-cache snapshot the code names is not present on every box and (b) the only other copies were inside rotating legacy SFT checkpoint directories. tests/conftest.py::resolve_v03_tokenizer_dir and scripts/build_data.py::default_tokenizer_dir prefer the real snapshot when it exists and fall back to this copy. It is tokenizer-only: no config.json, no weights, so anything that needs the base model's weights still requires the snapshot.

Status (2026-10-12, second integration pass)

Firewall and import health

• Dependency firewall (tests/test_dependency_firewall.py): 2 passed, 0 violators, no whitelist additions. bitsandbytes stays banned; adamw8bit is in-repo.
• Import smoke (15 modules incl. train.adamw8bit, train.quant8, train.offload_adamw, utils.guard; no GPU, no transformers): OK.
• Py_compile scan (every scripts/*.py): OK.

Test coverage

• Full CPU suite (pytest -m "not gpu and not oracle and not slow", align venv): 1089 passed, 13 skipped, 60 deselected (61 s). Up from 997 passed at HEAD a4d4d5e.
  • Skips (unchanged): 5 (argilla_arm_a, HF cache missing), 3 (eval_set_build, MATH-500 missing), 1 (parquet ingest, no pyarrow), 3 (shard-tree data), 1 (manifest).
  • Deselected: GPU tests (51), slow tests (~9).
• Oracle parity (legacy venv, last measured in the first pass, not re-run): tokenizer 100% identical, verifier agreement 0.9975 on 400 pairs, tiny forward identical logits, checkpoint round-trip exact.

Optimizer resolution

Every shipped full-FT config (sft, pretrain, grpo_stageb, dpo via scripts/dpo.py) names optimizer.name = "adamw8bit". After bitsandbytes was removed that name raised NotImplementedError, and the only other optimizer (offload_adamw) cannot launch 7.25B on 4 ranks (4x over its pinned-staging cap, ~105GB host RSS). Resolved by align/train/adamw8bit.py (BlockwiseAdamW8bit): make_optimizer(load_config("configs/sft.toml"), params) now returns it and it steps (pinned by tests/test_adamw8bit.py::test_every_shipped_adamw8bit_config_constructs_the_real_optimizer_and_steps).

Projection for 7.25B / 4 ranks (guard.projected_full_ft_rss_gb, config-derived):

Quantity	adamw8bit	offload_adamw
host optimizer state + master	0 GB	81 GB
on-GPU optimizer state, per rank	3.38 GB	0
steady-state host RSS (total_gb)	22.0 GB	104.7 GB
checkpoint-save transient, rank-0 gather	40.6 GB (3x state, estimate)	not modelled
checkpoint-save transient, train.per_rank_optimizer_state	13.5 GB (1x)	not modelled
peak_gb preflight gates on	62.6 GB (35.5 GB per-rank files)	104.7 GB

preflight_rss now requires peak_gb + 45GB of MemAvailable (the 45GB floor of /apps/CLAUDE.md). With the ~85GB the shipped configs were sized against, the default rank-0 gather is REFUSED (62.6 + 45 = 107.6) and per-rank files pass (35.5 + 45 = 80.5). train.per_rank_optimizer_state = true is now set in configs/sft.toml and configs/pretrain.toml (validated on 2 CPU/gloo ranks, bit-exact resume, tests/test_trainer_dist.py). The DPO and GRPO stage configs cannot carry it yet (the flag is not plumbed into the RunConfig their scripts build); see .tmp/handoff/per_rank.md.

Resolved in this pass (was open in the first report)

Area	Item	Resolution
Launch	No optimizer constructible for any shipped full-FT config	adamw8bit implemented, wired, tested (41 + 4 tests, 16 hand mutants killed)
Trainer	Logged lr was the post-step value	logs the last APPLIED lr; saved as last_applied_lr in resume.pt
Trainer	Resume lost checkpoints_written (stale-substrate rollout, keep-N blind to resumed checkpoint)	resume_from registers the resumed micro-step (idempotent); scripts/ppo.py::_resume is now a thin wrapper
Trainer	extra_state hook	TrainModule.extra_state()/load_extra_state() base stubs; Trainer saves/restores resume.pt["extra_state"]
Trainer	Rank-0 optimizer gather	opt-in train.per_rank_optimizer_state (field now exists, so struct-mode TOML can set it)
Checkpoint	Partial tokenizer copy	all-or-nothing, loud fallback to the vendored copy
GRPO	grad-norm tripwire measured post-clip	pre-clip norm captured from clip_grad_norm_'s return
GRPO	CollapseTripwire state lost on resume	state_dict/load_state_dict; rides extra_state
DPO	RefCacheKey could not tell checkpoints apart	key carries a streamed sha256 of the weights; old caches refused (re-precompute)
DPO	path-bias forward_impl mismatch; global_batch not validated	dpo.py reads forward_impl from the cache header; launch topology checked against global_batch
PPO	gamma != 1.0, lm_head without label_token_ids	refused at stage-config validation
PPO	optimizer/scheduler stepped on an all-skipped window	skipped (rank-consistent via one tiny all-reduce)
Config	OptimizerConfig.max_grad_norm	new optional field, forwarded to adamw8bit (None = no clipping, as before)
Guard	No device/save-transient projection for 8-bit	device_optimizer_state_gb_per_rank, checkpoint_save_transient_gb, peak_gb; preflight gates on peak

Still open

Area	Issue	Why not closed
GRPO	scripts/grpo.py never calls resume_from_latest()	a correct resume needs the prompt cursor and dead-group-retry draws checkpointed (GrpoBatchSource._cursor/_order are not in any state); wiring only the Trainer resume would re-draw the earliest prompt blocks
GRPO	bf16 log_softmax under FSDP2 (rho misses it)	needs a GPU memory check at the 2-row micro shape
GRPO	restored latched tripwire does not re-populate GrpoBatchSource.alarms	collapse_tripwire.fired in stage_result.json still reports it
adamw8bit	no triton kernel; GPU step time at 1.8B local elements unmeasured; save peak is an estimate	no GPU jobs allowed
per-rank ckpt	barriers/resume now exercised on 2 CPU gloo ranks; NCCL/GPU 4-rank and DPO/GRPO plumbing still open	no GPU jobs allowed; DPO/GRPO need package edits (handoff)
PPO	configs/ppo_stage.toml [TBD] fields, PRM checkpoint absent, KL in both reward and loss	experiment-owner decisions
PPO	path-bias report is not bound to a checkpoint hash	pre-existing
Data	base model snapshot absent; data not migrated; corpus agreement figures stale	environment

Pre-flight checklist for next run

1. Firewall: .venv/bin/python -m pytest tests/test_dependency_firewall.py -q must pass.
2. CPU suite: .venv/bin/python -m pytest tests -q -m "not gpu and not oracle and not slow" -p no:cacheprovider (1365 passed, 13 skipped expected; test_roundtrip_ceiling.py x2 fail unless the PRM800K snapshot is cached).
3. Host: free -g; uptime; awk '$3=="nvme2n1"{print $12}' /proc/diskstats. Require >=45GB free, load < 2x cores, disk queue < 64 (/apps/CLAUDE.md); for adamw8bit the preflight additionally requires the projected save peak.
4. Re-run scripts/precompute_ref_logprobs.py for both DPO arms before scripts/dpo.py (old ref caches are refused by design).
5. train.per_rank_optimizer_state = true is set in sft/pretrain TOMLs; for DPO/GRPO 7B jobs it is not settable until plumbed (handoff) -- ensure MemAvailable >= ~108GB for those.
6. A pre-fix checkpoint resumes with the corrected LR schedule applied from the next step.
7. PPO: resolve the [TBD] fields in configs/ppo_stage.toml first.