switched over to ty

philzook58 · philzook58 · commit 5346eb021d1a · 2026-02-08T13:27:54.000-05:00
diff --git a/.github/workflows/python-package.yml b/.github/workflows/python-package.yml
@@ -68,5 +68,6 @@ jobs:
         run: |
           uv run python -m pytest -m ""
           #KNUCKLE_SOLVER=cvc5 pytest
-      - name: Run pyright
-        uses: jakebailey/pyright-action@v2
+      - name: Run ty
+        run: |
+          uvx ty check
diff --git a/pyproject.toml b/pyproject.toml
@@ -12,7 +12,7 @@ classifiers = [
     "Topic :: Software Development :: Disassemblers",
 
 ]
-requires-python = ">= 3.11"
+requires-python = ">= 3.12"
 dependencies = [
     "z3-solver >= 4.15.4",
     "lark>=1.3.1",
@@ -116,7 +116,6 @@ dev = [
     "jupyter>=1.1.1",
     "line-profiler>=5.0.0",
     "nbclient>=0.10.2",
-    "pyright>=1.1.392.post0",
     "pytest>=8.3.4",
     "ruff>=0.11.13",
 ]
diff --git a/src/kdrag/contrib/pcode/__init__.py b/src/kdrag/contrib/pcode/__init__.py
@@ -111,7 +111,7 @@ def getRegisterName(self) -> str:
 
 # Varnode by default has pointer identity. This makes dictionaries not work correctly.
 
-pypcode.Varnode.__hash__ = lambda self: hash((self.space.name, self.offset, self.size))
+pypcode.Varnode.__hash__ = lambda self: hash((self.space.name, self.offset, self.size))  # type: ignore[assignment]
 
 
 def varnode_eq(self: pypcode.Varnode, other) -> bool:
@@ -123,7 +123,7 @@ def varnode_eq(self: pypcode.Varnode, other) -> bool:
     )
 
 
-pypcode.Varnode.__eq__ = varnode_eq
+pypcode.Varnode.__eq__ = varnode_eq  # type: ignore[assignment]
 
 
 class CachedArray(NamedTuple):
@@ -726,7 +726,10 @@ def sym_execute(
                         max_insns1 = max_insns
                         memstate2 = memstate1
                     next_pc = (addr, pcode_pc)
-                    path_cond1 = path_cond + [pc1[0] == vaddr, pc1[1] == vpcode_pc]
+                    path_cond1 = path_cond + [
+                        smt.Eq(pc1[0], vaddr),
+                        smt.Eq(pc1[1], vpcode_pc),
+                    ]
                     if addr in breakpoints:
                         res.append(SimState(memstate2, next_pc, path_cond1))
                     elif max_insns1 <= 0:
diff --git a/src/kdrag/datatype.py b/src/kdrag/datatype.py
@@ -375,9 +375,10 @@ def Struct(
     >>> kd.QForAll([p], p.x > -42)
     ForAll(p, Implies(And(x(p) > 0, y(p) > 0), x(p) > -42))
     """
-    rec = Inductive(name)
-    rec.declare(name, *fields)
-    rec = rec.create()
+    rec0 = Inductive(name)
+    rec0.declare(name, *fields)
+    rec = rec0.create()
+    assert isinstance(rec, smt.DatatypeSortRef)
     rec.mk = rec.constructor(0)
     wf_cond = [
         n for (n, (_, sort)) in enumerate(fields) if sort in kd.notation.wf.methods
@@ -461,7 +462,7 @@ def declare(
         olddeclare(name, *args)
         preds.append(pred)
 
-    dt.declare = declare
+    dt.declare = declare  # type: ignore[assignment]
 
     oldcreate = dt.create
 
@@ -505,7 +506,7 @@ def create():
                 kd.notation.wf.register(dt, lambda x: x.rel())
         return dt
 
-    dt.create = create
+    dt.create = create  # type: ignore[assignment]
     return dt
 
 
diff --git a/src/kdrag/kernel.py b/src/kdrag/kernel.py
@@ -377,7 +377,7 @@ def subst(t: smt.ExprRef, eqs: Sequence[Proof]) -> tuple[smt.ExprRef, Proof]:
     assert all(isinstance(eq, kd.Proof) and smt.is_eq(eq.thm) for eq in eqs)
     subst = [(eq.thm.arg(0), eq.thm.arg(1)) for eq in eqs]
     t1 = smt.substitute(t, *subst)
-    return t1, kd.axiom(t == t1, ["subst", t, eqs])
+    return t1, kd.axiom(smt.Eq(t, t1), ["subst", t, eqs])
 
 
 def instan(ts: Sequence[smt.ExprRef], pf: Proof) -> Proof:
@@ -653,8 +653,8 @@ def declare(name, *args):
             ],
         )
 
-    dt.create = create
-    dt.declare = declare
+    dt.create = create  # type: ignore[assignment]
+    dt.declare = declare  # type: ignore[assignment]
     return dt
 
 
diff --git a/src/kdrag/modal.py b/src/kdrag/modal.py
@@ -209,4 +209,6 @@ def In(x: PExprRef, S: smt.FuncRef, prefix="t") -> PBoolRef:
     """
     doms = smt.domains(S)
     vs = [smt.FreshConst(d, prefix=prefix) for n, d in enumerate(doms)]
-    return smt.Lambda(vs, S[*vs][x(*vs)])
+    S1 = S(*vs)
+    assert isinstance(S1, smt.QuantifierRef) or isinstance(S1, smt.ArrayRef)
+    return smt.Lambda(vs, S1[x(*vs)])
diff --git a/src/kdrag/notation.py b/src/kdrag/notation.py
@@ -19,9 +19,9 @@
 import kdrag as kd
 
 
-smt.SortRef.__rshift__ = lambda self, other: smt.ArraySort(self, other)  # type: ignore
+smt.SortRef.__rshift__ = lambda self, other: smt.ArraySort(self, other)  # type: ignore[assignment]
 
-smt.ArrayRef.__call__ = lambda self, *arg: self[arg]
+smt.ArrayRef.__call__ = lambda self, *arg: self[arg]  # type: ignore[assignment]
 
 
 def compose(f: smt.FuncDeclRef, g: smt.FuncDeclRef) -> smt.FuncDeclRef:
@@ -57,7 +57,7 @@ def quantifier_call(self, *args):
     )
 
 
-smt.QuantifierRef.__call__ = quantifier_call
+smt.QuantifierRef.__call__ = quantifier_call  # type: ignore[assignment]
 
 
 class SortDispatch:
diff --git a/src/kdrag/parsers/microlean.py b/src/kdrag/parsers/microlean.py
@@ -13,7 +13,8 @@
 import kdrag.smt as smt
 from lark import Tree
 import kdrag as kd
-from typing import NamedTuple, Optional
+from typing import Optional
+from dataclasses import dataclass
 
 
 # TODO: let syntax
@@ -90,7 +91,8 @@
 )
 
 
-class Env(NamedTuple):
+@dataclass
+class Env:
     locals: dict
     globals: dict
 
diff --git a/src/kdrag/parsers/tptp.py b/src/kdrag/parsers/tptp.py
@@ -308,7 +308,13 @@ def tff_typed_variable(self, items):
             cast(str | list[Any] | tuple[str, Any, Any], items[1])
         )
         if isinstance(sort, tuple):
-            sort = self._function_sort_from_sig(sort) if self.thf_mode else self.sort
+            sort = (
+                self._function_sort_from_sig(
+                    cast(tuple[list[smt.SortRef], Optional[smt.SortRef]], sort)
+                )
+                if self.thf_mode
+                else self.sort
+            )
         if sort is None:
             sort = self.sort
         v = smt.Const(name, sort)
@@ -408,15 +414,17 @@ def _declare_symbol(
         if isinstance(type_repr, tuple) and type_repr[0] == "fun":
             sig = self._type_repr_to_sort(type_repr)
             assert isinstance(sig, tuple)
-            doms, rng = sig
+            doms, rng = cast(tuple[list[smt.SortRef], Optional[smt.SortRef]], sig)
             doms = list(doms)
             rng = rng if rng is not None else self.sort
             self.func_sigs[name] = (doms, rng)
             if not self.thf_mode:
                 fn = smt.Function(name, *doms, rng)
                 self.funcs[(name, len(doms))] = fn
                 return fn
-            sort = self._function_sort_from_sig((doms, rng))
+            sort = self._function_sort_from_sig(
+                cast(tuple[list[smt.SortRef], Optional[smt.SortRef]], (doms, rng))
+            )
             const = smt.Const(name, sort)
             self.consts[name] = const
             return const
@@ -451,17 +459,14 @@ def _type_repr_to_sort(
             rng_sort = self._type_repr_to_sort(rng)
             if isinstance(rng_sort, tuple):
                 rng_doms, rng_rng = rng_sort
-                dom_sorts.extend(rng_doms)
+                dom_sorts.extend(cast(list[smt.SortRef], rng_doms))  # type: ignore
                 rng_sort = rng_rng
             return (
                 cast(list[smt.SortRef], dom_sorts),
                 cast(Optional[smt.SortRef], rng_sort),
             )
         if isinstance(type_repr, list):
-            return [
-                cast(smt.SortRef, self._type_repr_to_sort(cast(Any, t)))
-                for t in type_repr
-            ]
+            return [cast(smt.SortRef, self._type_repr_to_sort(t)) for t in type_repr]
         if isinstance(type_repr, str):
             if type_repr == "$o":
                 return smt.BoolSort()
diff --git a/src/kdrag/reflect.py b/src/kdrag/reflect.py
@@ -73,9 +73,9 @@ def type_of_sort(s: smt.SortRef) -> type:
     >>> type_of_sort(smt.IntSort())
     <class 'int'>
     >>> type_of_sort(smt.ArraySort(smt.StringSort(), smt.IntSort()))
-    dict[str, int]
+    <class 'dict'>
     >>> type_of_sort(smt.SeqSort(smt.IntSort()))
-    list[int]
+    <class 'list'>
     """
     if s == smt.IntSort():
         return int
@@ -86,9 +86,9 @@ def type_of_sort(s: smt.SortRef) -> type:
     elif s == smt.StringSort():
         return str
     elif isinstance(s, smt.ArraySortRef):
-        return dict[type_of_sort(s.domain()), type_of_sort(s.range())]
+        return dict  # type_of_sort(s.domain()), type_of_sort(s.range())]
     elif isinstance(s, smt.SeqSortRef):
-        return list[type_of_sort(s.basis())]
+        return list  # [type_of_sort(s.basis())]
     else:
         raise NotImplementedError(f"Sort {s} is not supported")
 
diff --git a/src/kdrag/smt.pyi b/src/kdrag/smt.pyi
@@ -3451,7 +3451,7 @@ class ArraySortRef(SortRef):
 class ArrayRef(ExprRef):
     """Array expressions."""
     def __call__(
-        self, *args
+        self, *args: ExprRef
     ) -> ExprRef: ...  # ArrayRef is monkeypatched to support _call__
     def sort(self):  # -> ArraySortRef:
         """Return the array sort of the array expression `self`.
diff --git a/src/kdrag/solvers/__init__.py b/src/kdrag/solvers/__init__.py
@@ -132,6 +132,7 @@ def __init__(self):
     def add(self, thm: smt.BoolRef | list[smt.BoolRef]):
         if isinstance(thm, list):
             for t in thm:
+                assert isinstance(t, smt.BoolRef)
                 self.add(t)
         else:
             assert isinstance(thm, smt.BoolRef)
diff --git a/src/kdrag/solvers/egglog.py b/src/kdrag/solvers/egglog.py
@@ -2,6 +2,7 @@
 import kdrag as kd
 import kdrag.smt as smt
 import kdrag.solvers as solvers
+from typing import cast
 
 # https://www.philipzucker.com/egglog_z3_simp/
 
@@ -71,6 +72,7 @@ def add(self, thm: kd.Proof | smt.BoolRef | list[smt.BoolRef | kd.Proof]):
             rules = [thm.thm]
         else:
             rules = [thm]
+        rules = cast(list[smt.BoolRef], rules)
         for sort in solvers.collect_sorts(rules):
             if sort not in self.sorts:
                 self.run_cmd(f"(sort {sort.name()})")
diff --git a/src/kdrag/tactics.py b/src/kdrag/tactics.py
@@ -9,7 +9,7 @@
 import kdrag.solvers as solvers
 from enum import IntEnum
 import operator as op
-from typing import NamedTuple, Optional, Sequence, Callable
+from typing import NamedTuple, Optional, Sequence, Callable, Any, cast
 import pprint
 import time
 from dataclasses import dataclass
@@ -277,21 +277,21 @@ def prove(
         thm = smt.Implies(smt.And(assumes), thm)
 
     if by is None:
-        by = []
+        by_list: list[kd.kernel.Proof] = []
     elif isinstance(by, kd.Proof):
-        by = [by]
-    elif not isinstance(by, list):
-        by = list(by)
+        by_list = [by]
+    else:
+        by_list = list(by)
 
     if contracts is None:
         pass
     elif contracts is True:
-        by = by + kd.contracts.lemmas(thm)
+        by_list += kd.contracts.lemmas(thm)
     elif isinstance(contracts, list):
-        by = list(by)
+        by_list = list(by_list)
         for decl in contracts:
             if decl in kd.contracts.contracts:
-                by.append(kd.contracts.contracts[decl].proof)
+                by_list.append(kd.contracts.contracts[decl].proof)
             else:
                 raise KeyError(f"No contract found for {decl}")
 
@@ -304,16 +304,16 @@ def prove(
             thm1 = kd.rewrite.unfold(thm1, trace=trace)
         # It is arguable if we're better off dumping trace into by or hiding trace
         if not thm.eq(thm1):
-            by.extend(trace)
+            by_list.extend(cast(list[kd.kernel.Proof], trace))
     elif isinstance(unfold, list):
         trace = []
         thm1 = kd.rewrite.unfold(thm, decls=unfold, trace=trace)
         if not thm.eq(thm1):
-            by.extend(trace)
+            by_list.extend(cast(list[kd.kernel.Proof], trace))
 
     try:
         pf = kd.kernel.prove(
-            thm, by, timeout=timeout, dump=dump, solver=solver, admit=admit
+            thm, by=by_list, timeout=timeout, dump=dump, solver=solver, admit=admit
         )
         if fixes:
             pf = kd.kernel.generalize(fixes, pf)
@@ -329,7 +329,7 @@ def prove(
                 _, thm = kd.utils.open_binder_unhygienic(thm)  # type: ignore
             # We anticipate this failing with a better countermodel since we can now see the quantified variables
             pf = kd.kernel.prove(
-                thm, by=by, timeout=timeout, dump=dump, solver=solver, admit=admit
+                thm, by=by_list, timeout=timeout, dump=dump, solver=solver, admit=admit
             )
             # TODO: Maybe we should herbrandize and just let the quantifier free version work for us.
             raise Exception(
@@ -1394,7 +1394,7 @@ def rw(
         ctx, goal = goalctx.ctx, goalctx.goal
         if at is not None:
             (at, hyp) = goalctx.ctx_find(at)
-        if isinstance(rule, int) or isinstance(rule, smt.ExprRef):
+        if isinstance(rule, int) or isinstance(rule, smt.BoolRef):
             _, rulethm = goalctx.ctx_find(rule)
         elif kd.kernel.is_proof(rule):
             rulethm = rule.thm
@@ -2066,7 +2066,7 @@ def Theorem(
     def res(f: Callable[[ProofState], None]) -> kd.kernel.Proof:
         start = time.perf_counter()
         if timing:
-            print("Starting theorem", f.__name__)
+            print("Starting theorem", cast(Any, f).__name__)
             l = ProofStateProxy(
                 Goal(
                     sig=[],
@@ -2080,7 +2080,7 @@ def res(f: Callable[[ProofState], None]) -> kd.kernel.Proof:
         pf = l.qed()
         if timing:
             end = time.perf_counter()
-            print(f"Theorem {f.__name__} took {end - start:.4f} seconds")
+            print(f"Theorem {cast(Any, f).__name__} took {end - start:.4f} seconds")
         # To override metadata of the returned proof
         # Proof is frozen, so this is a bit fishy
         # @functools.update_wrapper had assumptions about return type being a function
diff --git a/src/kdrag/tele.py b/src/kdrag/tele.py
diff --git a/src/kdrag/theories/logic/axioms.py b/src/kdrag/theories/logic/axioms.py
diff --git a/src/kdrag/theories/logic/sep.py b/src/kdrag/theories/logic/sep.py
diff --git a/tests/test_hypothesis.py b/tests/test_hypothesis.py
