[docxology]

Three small, independent correctness bugs in the pyk persistence layer. Each has a regression test that fails on develop and passes with the fix.

Fixes

1. Proof.up_to_date hashed the builtin id (pyk/src/pyk/proof/proof.py): the on-disk freshness check compared self.digest against hash_str(id) (a constant path string) instead of hash_str(self.id), so the check never looked at the proof's own file. Proofs were always considered out of date, and subproof re-reads could never short-circuit.
2. APR proof refutations were dropped on read (pyk/src/pyk/proof/reachability.py): from_dict guarded on the singular key node_refutation, while serialization writes node_refutations, silently dropping refutation data on every round trip (affecting e.g. resumed proofs and refutation handling).
3. read_cfg_data crashed on records without vacuous/stuck (pyk/src/pyk/kcfg/kcfg.py): the reader unconditionally del-ed both keys, raising KeyError for older or hand-edited kcfg.json files. The keys are now popped with defaults.

Tests

• test_write_proof_up_to_date (src/tests/unit/test_proof.py)
• test_apr_proof_from_dict_node_refutations (src/tests/unit/test_proof.py)
• test_read_cfg_data_missing_vacuous_stuck (src/tests/unit/test_kcfg.py)

All three fail before the fix and pass after. Full test_proof.py + test_kcfg.py: 54 passed.

Test plan

uv run -- pytest src/tests/unit/test_proof.py src/tests/unit/test_kcfg.py

[docxology]

Tagging @tothtamas28 for review, per CONTRIBUTING.md. Local checks on this branch: make -C pyk check (flake8/mypy/autoflake/isort/pydocstyle/black) passes, and uv run -- pytest src/tests/unit/test_proof.py src/tests/unit/test_kcfg.py passes all 54 tests — the three new regression tests fail without the source fixes. This is an external-fork PR, so CI will not run here.