Skip to main content

verify_block_counter_key

Function verify_block_counter_key 

Source
pub fn verify_block_counter_key(vb: &VerifyBlock) -> String
Expand 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.