fix: proptest underflow + wrong Lean witnesses + counterexample values for named constants

[tanmay4l]

Fix three correctness bugs triggered by named spec constants.

• proptest_gen: boundary strategy emitted (b-3)..=b when b<3,
  causing u64 underflow panic at test runtime
• lean_gen: WitnessState::resolve_value skipped spec constants,
  producing wrong post-state witnesses → lake build failures on cover proofs
• check: build_counterexample showed wrong arithmetic in lint output
  when effect values referenced named constants

[abishekk92]

Thanks — all three fixes look correct and the gates pass clean (fmt / clippy -D warnings / 241 tests). Before merging, can we pin each fix with a unit test? The existing proptest_gen::tests / lean_gen::tests / check::tests modules are the right homes — each fix is one or two lines to exercise:

proptest_gen.rs — directly call the function, no spec needed:

#[test]
fn strategy_for_field_boundary_small_bound_avoids_underflow() {
    let spec = ParsedSpec::default();
    let s = strategy_for_field("U64", &spec, StrategyMode::Boundary, Some("2")).unwrap();
    assert_eq!(s, "0u64..=2u64");
    assert!(!s.contains("- 3"), "must not emit `(b - 3)` for b < 3");
}

lean_gen.rs — a minimal WitnessState with constants = [("ZERO", "0")], apply a handler whose effect is counter := ZERO, assert the resulting state field renders as 0 not ZERO.

check.rs — a build_counterexample call where the effect triple is ("counter", "set", "ZERO") and constants = [("ZERO".into(), "0".into())], assert the post-state arithmetic uses 0, not the fallback 1.

Without these, a future refactor of the resolution order could quietly re-break any of the three paths. Happy to merge once they're in.

[abishekk92]

Three real bugs, three tight fixes — nice catch on the proptest underflow in particular (that one only surfaces for small bounds, easy to miss). Unit tests cover each fix well.

One ask before merge: could you add .qedspec regression fixtures under examples/regressions/ for the three symptoms? The examples/regressions/issue-8/ bundle is the template — each repro-NN-*.qedspec has an inline header comment linking finding → expected vs actual → fix site. I'd suggest a new directory (e.g. examples/regressions/const-resolution/) with:

• repro-proptest-small-bound.qedspec — a spec with @bound(2) (or similar sub-3 bound) that would panic at test runtime pre-fix
• repro-lean-const-witness.qedspec — spec with const ZERO = 0 + effect field := ZERO where the cover proof's post-state witness matters
• repro-check-const-counterexample.qedspec — spec where the P1 counterexample lint output references a named const in an effect

The Rust unit tests prove the functions behave correctly; the spec fixtures prove the end-to-end qedgen check / codegen / verify pipeline stays correct as surrounding code evolves.

Happy to merge once those land.

[tanmay4l]

Three real bugs, three tight fixes — nice catch on the proptest underflow in particular (that one only surfaces for small bounds, easy to miss). Unit tests cover each fix well.

One ask before merge: could you add .qedspec regression fixtures under examples/regressions/ for the three symptoms? The examples/regressions/issue-8/ bundle is the template — each repro-NN-*.qedspec has an inline header comment linking finding → expected vs actual → fix site. I'd suggest a new directory (e.g. examples/regressions/const-resolution/) with:

• repro-proptest-small-bound.qedspec — a spec with @bound(2) (or similar sub-3 bound) that would panic at test runtime pre-fix
• repro-lean-const-witness.qedspec — spec with const ZERO = 0 + effect field := ZERO where the cover proof's post-state witness matters
• repro-check-const-counterexample.qedspec — spec where the P1 counterexample lint output references a named const in an effect

The Rust unit tests prove the functions behave correctly; the spec fixtures prove the end-to-end qedgen check / codegen / verify pipeline stays correct as surrounding code evolves.

Happy to merge once those land.

added the three unit tests (proptest_gen, lean_gen, check.rs) and the three .qedspec fixtures under examples/regressions/const-resolution/. Should be good to go.

[abishekk92]

Spent some time running the fixtures end-to-end and found two of three don't actually exercise the fix on their advertised symptom. Sharing the findings so we can decide between widening the patch or narrowing the fixtures.

repro-proptest-small-bound.qedspec ✓ works as documented — generated proptest emits 0u8..=2u8 (no underflow form). Boundary-strategy fix is good.

repro-lean-const-witness.qedspec ✗ fails lake build end-to-end:

error: Spec.lean:22:29: Unknown identifier `ZERO`

Generated initTransition body still emits counter := ZERO:

def initTransition (s : State) (signer : Pubkey) : Option State :=
  if s.status = .Uninitialized then
    some { s with counter := ZERO, status := .Active }
  else none

The fix to WitnessState::resolve_value is correct for cover-proof witnesses, but the spec's effect { counter := ZERO } lowers through a separate code path — transition-function effect rendering — which doesn't resolve named constants. The unit test passes because it tests WitnessState::resolve_value in isolation; the fixture exposes the un-fixed sibling site.

repro-check-const-counterexample.qedspec ✗ produces no warning:

$ qedgen check --spec repro-check-const-counterexample.qedspec --json
[]

build_counterexample is reachable in unit tests but unreachable in the live pipeline for this spec — the upstream violation-detection logic in check_completeness (which decides whether to call build_counterexample) doesn't resolve STEP either, so the lint never fires for this case.

Two ways forward:

1. Widen the patch. Add the same const-resolution to (a) Lean transition-function effect-RHS rendering in lean_gen.rs, and (b) the property-violation detection in check.rs::check_completeness that decides whether to call build_counterexample. Then the fixtures exercise the right symptoms.
2. Narrow the fixtures. Replace the two failing fixtures with ones that actually trigger the fixed code paths — e.g. a spec where the cover-witness substitution path runs through WitnessState::resolve_value, and a spec that already triggers the upstream lint with a const-effect the lint detects pre-resolution.

(1) is the higher-value option since the underlying bugs are real on the cited symptoms. Happy to iterate on either approach.

Also: please rebase onto main when you re-push — branch predates 70f4ca9 so it currently shows the issue template as a deletion.

[abishekk92]

I've left a comment requesting changes