Summary
VP-024's proof_file_hash is null because its Kani proofs span TWO files (src/decoder.rs + src/analyzer/arp.rs kani_proofs modules), unlike other VPs whose single-file SHA-256 method doesn't fit.
Work Required
Define a deterministic multi-file digest (SHA-256 of LF-normalized concatenation of the #[cfg(kani)] proof modules, per the repo's input-hash normalization discipline in bin/compute-input-hash), populate proof_file_hash + confirm verified_at_commit, and re-lock VP-024.
This requires a VP withdrawal and re-lock since VP-024 is verification_lock: true.
Severity
Low (governance/traceability only; not a runtime defect). VP-024 is the only F6-locked VP lacking a proof-integrity hash, breaking the cross-VP convention established by VP-020/022/011/019/012/005.
Source
Research-validated per DF-VALIDATION-001. Validation report: .factory/research/arp-followups-validation.md item 1a. From the ARP analyzer F6/F7 cycle (STORY-111..115).
Summary
VP-024's
proof_file_hashis null because its Kani proofs span TWO files (src/decoder.rs+src/analyzer/arp.rskani_proofsmodules), unlike other VPs whose single-file SHA-256 method doesn't fit.Work Required
Define a deterministic multi-file digest (SHA-256 of LF-normalized concatenation of the
#[cfg(kani)]proof modules, per the repo's input-hash normalization discipline inbin/compute-input-hash), populateproof_file_hash+ confirmverified_at_commit, and re-lock VP-024.This requires a VP withdrawal and re-lock since VP-024 is
verification_lock: true.Severity
Low (governance/traceability only; not a runtime defect). VP-024 is the only F6-locked VP lacking a proof-integrity hash, breaking the cross-VP convention established by VP-020/022/011/019/012/005.
Source
Research-validated per DF-VALIDATION-001. Validation report:
.factory/research/arp-followups-validation.mditem 1a. From the ARP analyzer F6/F7 cycle (STORY-111..115).