pub fn verify_block_counter_key(vb: &VerifyBlock) -> StringExpand description
Stable identity key for a verify block’s case-index space, shared by the
Lean emitter’s per-block case counters and the CLI’s VM ground-truth
collection (CodegenContext::sample_expected).
Plain verify <fn> blocks share one index space per fn — the VM verify
runner merges them (checker::merge_verify_blocks) and the Lean emitter
continues the counter across blocks with the same key — while each
verify <fn> law <name> block keeps its own space. Both sides MUST derive
keys from this one function: index drift between them would associate a
case with another case’s ground-truth value.