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

crates/qedgen/src/check.rs

@@ -1375,6 +1375,7 @@ fn build_counterexample(
     prop_fields: &[&str],
     op: &ParsedHandler,
     modified_fields: &[&str],
+    constants: &[(String, String)],
 ) -> Option<Counterexample> {
     let relation = parse_property_relation(expr, prop_fields);
 
@@ -1416,7 +1417,13 @@ fn build_counterexample(
     let mut post_rhs = rhs_val;
     let mut effects = Vec::new();
     for (field, kind, value) in &effect_triples {
-        let v: i64 = value.parse().unwrap_or(1);
+        let v: i64 = value.parse().unwrap_or_else(|_| {
+            constants
+                .iter()
+                .find(|(n, _)| n == value)
+                .and_then(|(_, val)| val.parse().ok())
+                .unwrap_or(1)
+        });
         let desc = match *kind {
             "add" => format!("{} += {}", field, value),
             "sub" => format!("{} -= {}", field, value),
@@ -2253,7 +2260,46 @@ pub fn check_completeness(spec: &ParsedSpec) -> Vec<CompletenessWarning> {
 
             for op in &spec.handlers {
                 if prop.preserved_by.contains(&op.name) {
-                    continue; // this op IS covered
+                    // Handler is claimed to preserve the property — verify via
+                    // effect analysis. Warn when the effect demonstrably violates
+                    // the bound (covers preserved_by all expansion and explicit lists).
+                    let covered_modified: Vec<&str> = op
+                        .effects
+                        .iter()
+                        .filter(|(f, _, _)| prop_fields.contains(&f.as_str()))
+                        .map(|(f, _, _)| f.as_str())
+                        .collect();
+                    if !covered_modified.is_empty() {
+                        if let Some(ce) = build_counterexample(
+                            expr,
+                            &prop.name,
+                            &prop_fields,
+                            op,
+                            &covered_modified,
+                            &spec.constants,
+                        ) {
+                            if !ce.invariant_holds {
+                                warnings.push(CompletenessWarning {
+                                    rule: "preserved_by_all_potential_violation".to_string(),
+                                    severity: Severity::Warning,
+                                    priority: 1,
+                                    message: format!(
+                                        "handler '{}' is in `preserved_by` for property '{}' but effect analysis suggests a violation",
+                                        op.name, prop.name
+                                    ),
+                                    subject: Some(op.name.clone()),
+                                    fix: format!(
+                                        "Add a guard to '{}' ensuring the invariant holds after the effect, or remove it from `preserved_by`",
+                                        op.name
+                                    ),
+                                    example: None,
+                                    counterexample: Some(ce),
+                                    fix_options: vec![],
+                                });
+                            }
+                        }
+                    }
+                    continue;
                 }
                 // Check if this excluded op modifies any field in the property expression
                 let modified_prop_fields: Vec<&str> = op
@@ -2293,6 +2339,7 @@ pub fn check_completeness(spec: &ParsedSpec) -> Vec<CompletenessWarning> {
                         &prop_fields,
                         op,
                         &modified_prop_fields,
+                        &spec.constants,
                     );
 
                     let fix_options = build_fix_suggestions(
@@ -4230,4 +4277,56 @@ interface Token {
             "handler fragment missing in merged source"
         );
     }
+
+    #[test]
+    fn build_counterexample_resolves_named_const_in_effect() {
+        let handler = ParsedHandler {
+            name: "reset".to_string(),
+            effects: vec![("counter".to_string(), "set".to_string(), "ZERO".to_string())],
+            ..make_handler("reset")
+        };
+        let constants = vec![("ZERO".to_string(), "0".to_string())];
+        let ce = build_counterexample(
+            "s.counter \u{2264} 5",
+            "bounded",
+            &["counter"],
+            &handler,
+            &["counter"],
+            &constants,
+        )
+        .expect("should produce a counterexample");
+        let post = ce
+            .post_state
+            .iter()
+            .find(|(f, _)| f == "counter")
+            .unwrap()
+            .1;
+        assert_eq!(post, 0, "ZERO should resolve to 0, not fall back to 1");
+    }
+
+    #[test]
+    fn preserved_by_all_potential_violation_fires_for_named_const_effect() {
+        let spec = crate::chumsky_adapter::parse_str(
+            r#"spec Test
+program_id "11111111111111111111111111111111"
+const STEP = 5
+type State | Active of { counter : U64 }
+type Error | E
+property counter_small :
+  state.counter <= 3
+  preserved_by all
+handler tick : State.Active -> State.Active {
+  permissionless
+  effect { counter := STEP }
+}"#,
+        )
+        .unwrap();
+        let warnings = check_completeness(&spec);
+        assert!(
+            warnings
+                .iter()
+                .any(|w| w.rule == "preserved_by_all_potential_violation"),
+            "must warn when preserved_by all handler demonstrably violates the property"
+        );
+    }
 }

crates/qedgen/src/lean_gen.rs

@@ -121,6 +121,14 @@ fn render_single_account(spec: &ParsedSpec) -> String {
 
     emit_uninterpreted_helpers(&mut out, &spec.uninterpreted_helpers);
 
+    // Constants
+    for (name, val) in &spec.constants {
+        out.push_str(&format!("abbrev {} : Nat := {}\n", safe_name(name), val));
+    }
+    if !spec.constants.is_empty() {
+        out.push('\n');
+    }
+
     // Status inductive (if lifecycle states exist)
     let has_lifecycle = !spec.lifecycle_states.is_empty();
     if has_lifecycle {
@@ -217,6 +225,14 @@ fn render_multi_account(spec: &ParsedSpec) -> String {
 
     emit_uninterpreted_helpers(&mut out, &spec.uninterpreted_helpers);
 
+    // Constants
+    for (name, val) in &spec.constants {
+        out.push_str(&format!("abbrev {} : Nat := {}\n", safe_name(name), val));
+    }
+    if !spec.constants.is_empty() {
+        out.push('\n');
+    }
+
     // Per-account sections
     for acct in &spec.account_types {
         let acct_name = &acct.name;
@@ -1122,10 +1138,15 @@ impl WitnessState {
 
     /// Apply a handler's effects, updating field values.
     /// `param_values` maps parameter names to chosen concrete values.
-    fn apply(&mut self, handler: &crate::check::ParsedHandler, param_values: &[(String, String)]) {
+    fn apply(
+        &mut self,
+        handler: &crate::check::ParsedHandler,
+        param_values: &[(String, String)],
+        constants: &[(String, String)],
+    ) {
         // Apply effects
         for (field, op_kind, value) in &handler.effects {
-            let resolved = self.resolve_value(value, param_values);
+            let resolved = self.resolve_value(value, param_values, constants);
             match op_kind.as_str() {
                 "set" => {
                     if let Some(f) = self.fields.iter_mut().find(|(n, _)| n == field) {
@@ -1158,7 +1179,12 @@ impl WitnessState {
     /// Resolve an effect value to a concrete string.
     /// Checks param_values first, then tries parsing as integer.
     /// Falls back to "1" for unknown references.
-    fn resolve_value(&self, value: &str, param_values: &[(String, String)]) -> String {
+    fn resolve_value(
+        &self,
+        value: &str,
+        param_values: &[(String, String)],
+        constants: &[(String, String)],
+    ) -> String {
         // Check if it's a parameter
         if let Some((_, v)) = param_values.iter().find(|(n, _)| n == value) {
             return v.clone();
@@ -1172,6 +1198,10 @@ impl WitnessState {
         if let Some(f) = self.fields.iter().find(|(n, _)| n == value) {
             return f.1.clone();
         }
+        // Check if it's a declared spec constant
+        if let Some((_, v)) = constants.iter().find(|(n, _)| n == value) {
+            return v.clone();
+        }
         // Fallback
         "1".to_string()
     }
@@ -1253,7 +1283,7 @@ fn cover_trace_proof(
             status: state.status.clone(),
         };
 
-        state.apply(handler, &param_values);
+        state.apply(handler, &param_values, &spec.constants);
 
         steps.push((op_name.clone(), param_values, state_before));
     }
@@ -1278,7 +1308,7 @@ fn cover_trace_proof(
             let mut s = WitnessState::new(fields, lifecycle);
             for step in steps.iter().take(i + 1) {
                 let handler = spec.handlers.iter().find(|o| o.name == step.0)?;
-                s.apply(handler, &step.1);
+                s.apply(handler, &step.1, &spec.constants);
             }
             proof.push_str(&format!("  let s{} : State := {}\n", i + 1, s.to_lean()));
         }
@@ -4645,4 +4675,66 @@ handler noop : State -> State {
             "def must not strip the quantifier leaving v unbound"
         );
     }
+
+    #[test]
+    fn witness_state_apply_resolves_spec_const_in_effect() {
+        let mut ws = WitnessState {
+            fields: vec![("counter".to_string(), "0".to_string())],
+            status: None,
+        };
+        let handler = crate::check::ParsedHandler {
+            name: "reset".to_string(),
+            effects: vec![("counter".to_string(), "set".to_string(), "ZERO".to_string())],
+            doc: None,
+            who: None,
+            on_account: None,
+            pre_status: None,
+            post_status: None,
+            takes_params: vec![],
+            guard_str: None,
+            guard_str_rust: None,
+            aborts_if: vec![],
+            requires: vec![],
+            ensures: vec![],
+            modifies: None,
+            let_bindings: vec![],
+            aborts_total: false,
+            permissionless: true,
+            accounts: vec![],
+            transfers: vec![],
+            emits: vec![],
+            invariants: vec![],
+            properties: vec![],
+            calls: vec![],
+        };
+        let constants = vec![("ZERO".to_string(), "0".to_string())];
+        ws.apply(&handler, &[], &constants);
+        let val = &ws.fields.iter().find(|(n, _)| n == "counter").unwrap().1;
+        assert_eq!(
+            val.as_str(),
+            "0",
+            "ZERO const should resolve to 0, not fall back to 1"
+        );
+    }
+
+    #[test]
+    fn lean_gen_single_account_emits_const_abbrevs() {
+        let spec = chumsky_adapter::parse_str(
+            r#"spec ConstTest
+program_id "11111111111111111111111111111111"
+const ZERO = 0
+type State | Active of { counter : U64 }
+type Error | E
+handler init : State.Active -> State.Active {
+  permissionless
+  effect { counter := ZERO }
+}"#,
+        )
+        .unwrap();
+        let lean = render(&spec);
+        assert!(
+            lean.contains("abbrev ZERO : Nat := 0"),
+            "single-account render must emit abbrev for spec constants; got:\n{lean}"
+        );
+    }
 }

crates/qedgen/src/proptest_gen.rs

@@ -127,11 +127,18 @@ fn strategy_for_field(
     if let Some(bound) = field_bound {
         let rust_type = map_type(dsl_type, spec)?;
         return Ok(match mode {
-            StrategyMode::Boundary => format!(
-                "prop_oneof![0{rt}..=3{rt}, ({b} - 3)..={b}{rt}]",
-                rt = rust_type,
-                b = bound
-            ),
+            StrategyMode::Boundary => {
+                let n: u128 = bound.parse().unwrap_or(u128::MAX);
+                if n < 3 {
+                    format!("0{rt}..={b}{rt}", rt = rust_type, b = bound)
+                } else {
+                    format!(
+                        "prop_oneof![0{rt}..=3{rt}, ({b} - 3)..={b}{rt}]",
+                        rt = rust_type,
+                        b = bound
+                    )
+                }
+            }
             StrategyMode::Full => format!("0{rt}..={b}{rt}", rt = rust_type, b = bound),
         });
     }
@@ -1294,4 +1301,12 @@ handler noop { }
             "payload-variant sum should not get unit-strategy: {out}"
         );
     }
+
+    #[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");
+    }
 }

examples/regressions/const-resolution/repro-check-const-counterexample.qedspec

@@ -0,0 +1,32 @@
+// Regression: qedgen check counterexample shows wrong value for named constants
+//
+// Expected: `qedgen check` counterexample for property `counter_small`
+//   (counter <= 3) after effect `counter := STEP` (STEP = 5) shows
+//   post-state counter = 5.
+//
+// Actual (pre-fix): build_counterexample fell back to 1 when the effect
+//   value was a named constant (not a parseable integer), so the diagnostic
+//   showed post-state counter = 1 — a misleading value that doesn't match
+//   any actual execution.
+//
+// Fix site: crates/qedgen/src/check.rs — build_counterexample now resolves
+// named constant values from spec.constants before falling back to 1.
+
+spec ReproCheckConstCounterexample
+program_id "11111111111111111111111111111111"
+
+const STEP = 5
+
+type State
+  | Active of { counter : U64 }
+
+type Error | E
+
+property counter_small :
+  state.counter <= 3
+  preserved_by all
+
+handler tick : State.Active -> State.Active {
+  permissionless
+  effect { counter := STEP }
+}

examples/regressions/const-resolution/repro-lean-const-witness.qedspec

@@ -0,0 +1,30 @@
+// Regression: cover-proof witness uses constant name instead of resolved value
+//
+// Expected: `qedgen codegen --lean` emits a cover witness with
+//   counter := 0   (the resolved value of ZERO)
+//
+// Actual (pre-fix): WitnessState::resolve_value did not look up named
+//   constants, so it emitted `counter := ZERO` (the unresolved identifier).
+//   lake build failed:
+//   error: unknown identifier 'ZERO'
+//
+// Fix site: crates/qedgen/src/lean_gen.rs — WitnessState::resolve_value
+// now looks up the name in spec.constants before falling back to "1".
+
+spec ReproLeanConstWitness
+program_id "11111111111111111111111111111111"
+
+const ZERO = 0
+
+type State
+  | Uninitialized
+  | Active of { counter : U64 }
+
+type Error | E
+
+handler init : State.Uninitialized -> State.Active {
+  permissionless
+  effect { counter := ZERO }
+}
+
+cover init_reachable [init]