db491ddd35
This PR moves the issue tracking infrastructure from `GrindM` to `SymM`. Issues can occur in different places within a `sym =>` block (e.g., during arithmetic normalization, simplification), not just during `grind` invocations. Moving them to `SymM` makes them available to all modules operating within the symbolic computation framework. - `Sym.reportIssue`: adds an issue to the `SymM` state - `Sym.getIssues`: retrieves accumulated issues - `Sym.withNewIssueContext`: saves/restores the issue list around a computation, used at grind entry points to isolate per-invocation issues while preserving them in the outer context - `GrindM.State.issues` removed; `Grind.reportIssue` delegates to `Sym.reportIssue` 🤖 Generated with [Claude Code](https://claude.com/claude-code) --------- Co-authored-by: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
39 lines
974 B
Text
39 lines
974 B
Text
module
|
|
example {n} (x y : BitVec n) : x * y = y * x := by
|
|
grind
|
|
|
|
example {n} (x y z w : BitVec n) : w = z → x * y - z*w = 0 → z*z = y * x := by
|
|
grind
|
|
|
|
example (x y : BitVec 64) : x * y = y * x := by
|
|
grind
|
|
|
|
example (x y : BitVec 128) : x * y = y * x := by
|
|
grind
|
|
|
|
example (x y : BitVec 128) : x * y = y * x + 2^64 * 2^64 * x := by
|
|
grind
|
|
|
|
example (x y : BitVec 256) : x * y = y * x := by
|
|
grind
|
|
|
|
example (x y : BitVec 1024) : x * y = y * x := by
|
|
grind
|
|
|
|
example (x y : BitVec 1024) : x * y = y * x := by
|
|
grind -lia
|
|
|
|
example (x y : BitVec 100000) : x * y = y * x := by
|
|
grind -lia
|
|
|
|
example (x y z : BitVec 100000) : x * y - z*z = 0 → z*z = y * x := by
|
|
grind -lia
|
|
|
|
/--
|
|
trace: [sym.issues] exponent 1024 exceeds threshold for exponentiation `(exp := 16)`
|
|
[sym.issues] exponent 1024 exceeds threshold for exponentiation `(exp := 16)`
|
|
-/
|
|
#guard_msgs in
|
|
set_option trace.sym.issues true in
|
|
example (x y : BitVec 1024) : x * y = y * x := by
|
|
grind (exp := 16)
|