pyk: persistence/correctness bugs (PR attached) #4951

Trigger (as reviewed): The guard tests for the singular key 'node_refutation' but the body reads the plural dct['node_refutations']. A proof.json containing the singular key (or the plural key without the singular) causes an uncaught KeyError, or the guard fails and genuine refutation data is silently dropped. Refutation data is what suppresses verified nodes from the failing/pending accounting (own_status, line 366).

Impact (as reviewed): Denial of service on proof loading, or silent loss of refutation metadata that changes the reported proof status. Both derive from a one-line typo consuming untrusted proof.json; the silent-drop branch is the more dangerous for verification correctness.

Trigger (as reviewed): hash_str(id) is called with the Python builtin id (the function object), not self.id. hash_str stringifies its argument, so every proof computes the same path f'{hash_str()}.json'. The freshness/digest check therefore never inspects the actual proof file (whose name is derived from hash_str(self.id) in write_proof, line 97). fetch_subproof (line 157) and fetch_subproof_data (line 168) use up_to_date to decide whether to re-read a proof from disk.

Impact (as reviewed): The 'is my cached proof stale?' gate is broken: it returns False whenever the mis-derived path does not exist (proofs re-read unnecessarily), or compares the current digest against an unrelated file if one matches that name. This weakens the integrity guarantee that a cached proof object corresponds to the on-disk artifact and can cause stale proof state to be treated as current.

Trigger (as reviewed): read_cfg_data synthesizes vacuous/stuck in the write path (kcfg/kcfg.py:80-81) but deletes them unconditionally on read. Any kcfg.json produced by an older pyk, hand-edited, truncated, or otherwise lacking those keys makes del dct['vacuous'] raise KeyError before the data is used. This runs before KCFG.from_dict (line 1300), so one missing optional key aborts loading of an otherwise-usable KCFG.

Impact (as reviewed): Denial of proof/KCFG loading for legacy or partially-written artifact directories. Low severity, but a robustness gap on data read from a directory the user may not control, and it masks the traversal issue in 001 by failing first on well-formed-but-older inputs.

Trigger (as reviewed): After the loop breaks because the current token is neither the separator nor the closing delimiter, line 152 calls self._consume() unconditionally: it discards whatever token happens to be current, whatever its type. For input such as App{f}(a b) the list parse produces [a], silently consumes b, and returns; the enclosing grammar may then accept the malformed term. There is no check that the consumed token is in fact rdelim. This is the shared list helper for sorts, patterns, and attribute lists.

Impact (as reviewed): Malformed KORE is accepted with parts silently dropped, so a term can be parsed as a different (weaker) term than written. For a tool whose correctness depends on faithfully representing KORE input, silently discarding tokens is a validation/soundness gap that crafted input can rely on to slip past a downstream check.