diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index fe5c259..efd60b7 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -2,6 +2,22 @@ name: CI on: [push, pull_request] jobs: + # Fast lint pass: ruff format, ruff check, mypy. + lint: + runs-on: ubuntu-latest + steps: + - uses: actions/checkout@v4 + - name: Install uv + uses: astral-sh/setup-uv@v5 + - run: uv python install 3.12 + - run: uv sync --dev + - name: ruff format + run: uv run ruff format --check . + - name: ruff check + run: uv run ruff check . + - name: mypy + run: uv run mypy lean_py/ + # Run the full test suite on Linux + macOS. test: strategy: diff --git a/LeanPy/Z3.lean b/LeanPy/Z3.lean index f127c64..8b48d06 100644 --- a/LeanPy/Z3.lean +++ b/LeanPy/Z3.lean @@ -247,7 +247,20 @@ partial def compileSort (varMap : Std.HashMap String Lean.Expr) : Z3Sort → Met | .uninterp name => match varMap.get? name with | some e => return e - | none => throwError s!"compileSort: unknown uninterpreted sort '{name}'" + | none => do + let tName := Name.mkSimple name + let env ← getEnv + if env.contains tName then return mkConst tName + else do + -- Auto-declare as an opaque type (axiom of sort Type) + let decl := Declaration.axiomDecl { + name := tName + levelParams := [] + type := mkSort (.succ .zero) + isUnsafe := false + } + addDecl decl + return mkConst tName | .arrow dom cod => do let domExpr ← compileSort varMap dom let codExpr ← compileSort varMap cod @@ -1000,7 +1013,8 @@ def z3Compile (expr : Z3Expr) : IO Lean.Expr := do let ctx ← LeanPy.Kernel.freshCoreContext let cs : Core.State := { env } let act : MetaM Lean.Expr := compileExpr {} expr - let (r, _) ← (act.run' {} {}).toIO ctx cs + let (r, cs') ← (act.run' {} {}).toIO ctx cs + LeanPy.Kernel.envRef.set (some cs'.env) return r @[python "z3_goal_create_expr"] diff --git a/examples/04_sympy_tactic/python/lean_to_sympy.py b/examples/04_sympy_tactic/python/lean_to_sympy.py index 245590f..0241c77 100644 --- a/examples/04_sympy_tactic/python/lean_to_sympy.py +++ b/examples/04_sympy_tactic/python/lean_to_sympy.py @@ -16,7 +16,7 @@ from typing import TYPE_CHECKING import sympy -from sympy import Integer, Symbol, Eq, simplify +from sympy import Eq, Integer, Symbol, simplify from lean_py.marshal import LeanInductiveValue @@ -28,6 +28,7 @@ # Name helpers # --------------------------------------------------------------------------- + def name_to_str(name: LeanInductiveValue) -> str: """Walk a ``Lean.Name`` ADT (anonymous / str / num) to a dot-separated string.""" parts: list[str] = [] @@ -53,13 +54,14 @@ def name_to_str(name: LeanInductiveValue) -> str: # Expr helpers # --------------------------------------------------------------------------- + def uncurry_app(expr: LeanInductiveValue) -> tuple[LeanInductiveValue, list[LeanInductiveValue]]: """Flatten nested ``Expr.app(f, x)`` into ``(head, [arg0, arg1, ...])``.""" args: list[LeanInductiveValue] = [] cur = expr while cur.ctor == "app": - args.append(cur._1) # arg - cur = cur._0 # fn + args.append(cur._1) # arg + cur = cur._0 # fn args.reverse() return cur, args @@ -72,19 +74,24 @@ def uncurry_app(expr: LeanInductiveValue) -> tuple[LeanInductiveValue, list[Lean # For elaborated Lean expressions, the first few args are type/instance params; # we only look at the *last N* arguments. + def _binop(op): """Return a builder for a binary operation (last 2 args).""" + def build(args): a = expr_to_sympy(args[-2]) b = expr_to_sympy(args[-1]) return op(a, b) + return 2, build def _unop(op): """Return a builder for a unary operation (last 1 arg).""" + def build(args): return op(expr_to_sympy(args[-1])) + return 1, build @@ -93,11 +100,11 @@ def build(args): "HSub.hSub": _binop(lambda a, b: a - b), "HMul.hMul": _binop(lambda a, b: a * b), "HDiv.hDiv": _binop(lambda a, b: a / b), - "HPow.hPow": _binop(lambda a, b: a ** b), - "Eq": (2, lambda args: Eq(expr_to_sympy(args[-2]), expr_to_sympy(args[-1]))), - "Neg.neg": _unop(lambda x: -x), + "HPow.hPow": _binop(lambda a, b: a**b), + "Eq": (2, lambda args: Eq(expr_to_sympy(args[-2]), expr_to_sympy(args[-1]))), + "Neg.neg": _unop(lambda x: -x), "HNeg.hNeg": _unop(lambda x: -x), - "Nat.succ": (1, lambda args: expr_to_sympy(args[-1]) + 1), + "Nat.succ": (1, lambda args: expr_to_sympy(args[-1]) + 1), "Int.ofNat": (1, lambda args: expr_to_sympy(args[-1])), "Int.negSucc": (1, lambda args: -(expr_to_sympy(args[-1]) + 1)), } @@ -175,6 +182,7 @@ def expr_to_sympy(expr: LeanInductiveValue) -> sympy.Basic: # Proposition checkers # --------------------------------------------------------------------------- + def sympy_prop_check(prop: sympy.Basic) -> bool: """Check if a SymPy proposition is identically true.""" s = simplify(prop) @@ -206,9 +214,7 @@ def decode_and_check_prop(lean_obj) -> bool: Called from the Lean tactic via ``Py.ofLeanObj`` + ``@[python]``. """ if _marshaller is None: - raise RuntimeError( - "lean_to_sympy.setup(lib) must be called before decode_and_check_prop" - ) + raise RuntimeError("lean_to_sympy.setup(lib) must be called before decode_and_check_prop") expr_tree = _marshaller.decode_lean_obj("Lean.Expr", lean_obj) prop = expr_to_sympy(expr_tree) return sympy_prop_check(prop) diff --git a/examples/05_knuckledragger/python/lean_to_z3.py b/examples/05_knuckledragger/python/lean_to_z3.py index 4801e2a..ca4ca6c 100644 --- a/examples/05_knuckledragger/python/lean_to_z3.py +++ b/examples/05_knuckledragger/python/lean_to_z3.py @@ -28,6 +28,7 @@ # Name helpers # --------------------------------------------------------------------------- + def name_to_str(name: LeanInductiveValue) -> str: """Walk a ``Lean.Name`` ADT (anonymous / str / num) to a dot-separated string.""" parts: list[str] = [] @@ -53,13 +54,14 @@ def name_to_str(name: LeanInductiveValue) -> str: # Expr helpers # --------------------------------------------------------------------------- + def uncurry_app(expr: LeanInductiveValue) -> tuple[LeanInductiveValue, list[LeanInductiveValue]]: """Flatten nested ``Expr.app(f, x)`` into ``(head, [arg0, arg1, ...])``.""" args: list[LeanInductiveValue] = [] cur = expr while cur.ctor == "app": - args.append(cur._1) # arg - cur = cur._0 # fn + args.append(cur._1) # arg + cur = cur._0 # fn args.reverse() return cur, args @@ -81,15 +83,18 @@ def _var(name: str) -> z3.ArithRef: # Main converter # --------------------------------------------------------------------------- + def _binop(op): def build(args): return op(expr_to_z3(args[-2]), expr_to_z3(args[-1])) + return 2, build def _unop(op): def build(args): return op(expr_to_z3(args[-1])) + return 1, build @@ -98,11 +103,11 @@ def build(args): "HSub.hSub": _binop(lambda a, b: a - b), "HMul.hMul": _binop(lambda a, b: a * b), "HDiv.hDiv": _binop(lambda a, b: a / b), - "HPow.hPow": _binop(lambda a, b: a ** b), - "Eq": (2, lambda args: expr_to_z3(args[-2]) == expr_to_z3(args[-1])), - "Neg.neg": _unop(lambda x: -x), + "HPow.hPow": _binop(lambda a, b: a**b), + "Eq": (2, lambda args: expr_to_z3(args[-2]) == expr_to_z3(args[-1])), + "Neg.neg": _unop(lambda x: -x), "HNeg.hNeg": _unop(lambda x: -x), - "Nat.succ": (1, lambda args: expr_to_z3(args[-1]) + 1), + "Nat.succ": (1, lambda args: expr_to_z3(args[-1]) + 1), "Int.ofNat": (1, lambda args: expr_to_z3(args[-1])), "Int.negSucc": (1, lambda args: -(expr_to_z3(args[-1]) + 1)), } @@ -179,6 +184,7 @@ def expr_to_z3(expr: LeanInductiveValue): # Proposition checkers # --------------------------------------------------------------------------- + def check_prop(prop) -> bool: """Check a proposition via Knuckledragger (backed by Z3).""" try: @@ -208,9 +214,7 @@ def decode_and_check_prop(lean_obj) -> bool: Called from the Lean tactic via ``Py.ofLeanObj`` + ``@[python]``. """ if _marshaller is None: - raise RuntimeError( - "lean_to_z3.setup(lib) must be called before decode_and_check_prop" - ) + raise RuntimeError("lean_to_z3.setup(lib) must be called before decode_and_check_prop") expr_tree = _marshaller.decode_lean_obj("Lean.Expr", lean_obj) prop = expr_to_z3(expr_tree) return check_prop(prop) diff --git a/examples/05_knuckledragger/python/main.py b/examples/05_knuckledragger/python/main.py index a797992..21ce9b4 100644 --- a/examples/05_knuckledragger/python/main.py +++ b/examples/05_knuckledragger/python/main.py @@ -59,7 +59,6 @@ def mk_eq(lhs, rhs): rhs, ) - import z3 print("== expr_to_z3 ==") diff --git a/examples/06_effectful_verifier/python/main.py b/examples/06_effectful_verifier/python/main.py index 93d3e8e..b406c65 100644 --- a/examples/06_effectful_verifier/python/main.py +++ b/examples/06_effectful_verifier/python/main.py @@ -15,11 +15,11 @@ from pathlib import Path from typing import Annotated +from refine import Ge, Gt, assert_refined, verify_function + from lean_py import LeanLibrary from lean_py.kernel import Kernel -from refine import Gt, Ge, assert_refined, verify_function - lake_dir = Path(__file__).resolve().parent.parent / "lean" lib = LeanLibrary.from_lake(lake_dir, "EffectfulVerifier", build=True) @@ -27,6 +27,7 @@ kernel.init_search("") kernel.load(["Init"]) + def verify(fn): all_ok = True for msg, ok in verify_function(fn, lib, kernel): @@ -42,22 +43,29 @@ def verify(fn): # Programs under verification # --------------------------------------------------------------------------- + def positive_increment(x: Annotated[int, Gt(0)]): y = x + 3 - assert_refined(y, Gt(3)) # x > 0 → x + 3 > 3 ✓ + assert_refined(y, Gt(3)) # x > 0 → x + 3 > 3 ✓ z = x + 10 - assert_refined(z, Gt(10)) # x > 0 → x + 10 > 10 ✓ + assert_refined(z, Gt(10)) # x > 0 → x + 10 > 10 ✓ + + assert verify(positive_increment) + def bounded_sum(x: Annotated[int, Gt(0)], y: Annotated[int, Gt(0)]): s = x + y - assert_refined(s, Gt(1)) # x > 0 ∧ y > 0 → x + y > 1 ✓ - assert_refined(s, Ge(2)) # x > 0 ∧ y > 0 → x + y >= 2 ✓ + assert_refined(s, Gt(1)) # x > 0 ∧ y > 0 → x + y > 1 ✓ + assert_refined(s, Ge(2)) # x > 0 ∧ y > 0 → x + y >= 2 ✓ + + assert verify(bounded_sum) def failing(x: Annotated[int, Gt(0)]): y = x + 1 - assert_refined(y, Gt(10)) # x > 0 → x + 1 > 10 ✗ -assert not verify(failing) + assert_refined(y, Gt(10)) # x > 0 → x + 1 > 10 ✗ + +assert not verify(failing) diff --git a/examples/06_effectful_verifier/python/refine.py b/examples/06_effectful_verifier/python/refine.py index 87dbcc9..9cf8dbb 100644 --- a/examples/06_effectful_verifier/python/refine.py +++ b/examples/06_effectful_verifier/python/refine.py @@ -14,32 +14,36 @@ import inspect from dataclasses import dataclass -from typing import Annotated, get_type_hints +from typing import get_type_hints from effectful.ops.semantics import evaluate, handler from effectful.ops.syntax import defdata, defop from effectful.ops.types import Operation - from expr_builder import ExprBuilder -from lean_py.kernel import GoalState +from lean_py.kernel import GoalState # --------------------------------------------------------------------------- # Refinement annotations # --------------------------------------------------------------------------- + class Gt: """Refinement: value > n.""" + def __init__(self, n: int): self.n = n + def __repr__(self): return f"Gt({self.n})" class Ge: """Refinement: value >= n.""" + def __init__(self, n: int): self.n = n + def __repr__(self): return f"Ge({self.n})" @@ -48,6 +52,7 @@ def __repr__(self): # assert_refined — effectful operation (intercepted by handler) # --------------------------------------------------------------------------- + @defop def assert_refined(value: int, refinement) -> None: """Declare that *value* satisfies *refinement*. @@ -62,6 +67,7 @@ def assert_refined(value: int, refinement) -> None: # Verification result # --------------------------------------------------------------------------- + @dataclass class VerificationResult: description: str @@ -75,6 +81,7 @@ def __iter__(self): # Term → human-readable Lean syntax string (for display) # --------------------------------------------------------------------------- + def _build_lean_str(vc_term, var_names, var_ops, precond_terms) -> str: """Convert an effectful Term to a Lean proposition string.""" int_ops = defdata.dispatch(int) @@ -92,10 +99,10 @@ def _wrap(x): str_handler[int_ops.__add__] = lambda a, b: f"({_wrap(a)} + {_wrap(b)})" str_handler[int_ops.__sub__] = lambda a, b: f"({_wrap(a)} - {_wrap(b)})" str_handler[int_ops.__mul__] = lambda a, b: f"({_wrap(a)} * {_wrap(b)})" - str_handler[int_ops.__gt__] = lambda a, b: f"({_wrap(a)} > {_wrap(b)})" - str_handler[int_ops.__ge__] = lambda a, b: f"({_wrap(a)} >= {_wrap(b)})" - str_handler[int_ops.__lt__] = lambda a, b: f"({_wrap(a)} < {_wrap(b)})" - str_handler[int_ops.__le__] = lambda a, b: f"({_wrap(a)} <= {_wrap(b)})" + str_handler[int_ops.__gt__] = lambda a, b: f"({_wrap(a)} > {_wrap(b)})" + str_handler[int_ops.__ge__] = lambda a, b: f"({_wrap(a)} >= {_wrap(b)})" + str_handler[int_ops.__lt__] = lambda a, b: f"({_wrap(a)} < {_wrap(b)})" + str_handler[int_ops.__le__] = lambda a, b: f"({_wrap(a)} <= {_wrap(b)})" with handler(str_handler): body_str = evaluate(vc_term) @@ -112,6 +119,7 @@ def _wrap(x): # Term → Lean.Expr (for formal verification) # --------------------------------------------------------------------------- + def _make_expr_handler(eb: ExprBuilder, var_names, var_ops, depth): """Build an effectful handler that maps Term ops → Lean.Expr builders. @@ -131,10 +139,10 @@ def coerce(x): h[int_ops.__add__] = lambda a, b: eb.mk_int_add(coerce(a), coerce(b)) h[int_ops.__sub__] = lambda a, b: eb.mk_int_sub(coerce(a), coerce(b)) h[int_ops.__mul__] = lambda a, b: eb.mk_int_mul(coerce(a), coerce(b)) - h[int_ops.__gt__] = lambda a, b: eb.mk_int_gt(coerce(a), coerce(b)) - h[int_ops.__ge__] = lambda a, b: eb.mk_int_ge(coerce(a), coerce(b)) - h[int_ops.__lt__] = lambda a, b: eb.mk_int_lt(coerce(a), coerce(b)) - h[int_ops.__le__] = lambda a, b: eb.mk_int_le(coerce(a), coerce(b)) + h[int_ops.__gt__] = lambda a, b: eb.mk_int_gt(coerce(a), coerce(b)) + h[int_ops.__ge__] = lambda a, b: eb.mk_int_ge(coerce(a), coerce(b)) + h[int_ops.__lt__] = lambda a, b: eb.mk_int_lt(coerce(a), coerce(b)) + h[int_ops.__le__] = lambda a, b: eb.mk_int_le(coerce(a), coerce(b)) return h @@ -171,6 +179,7 @@ def _build_vc_expr(eb: ExprBuilder, vc_term, var_names, var_ops, precond_terms): # Core: verify_function # --------------------------------------------------------------------------- + def verify_function(fn, lib, kernel) -> list[VerificationResult]: """Verify all ``assert_refined`` calls in *fn* hold given its refinements. @@ -229,6 +238,7 @@ def _handle_assert(value, refinement): # Lean verification via goalFromExpr # --------------------------------------------------------------------------- + def _verify_expr(lib, kernel, lean_expr) -> bool: """Create a goal from a ``Lean.Expr`` and close it. diff --git a/examples/07_z3py_drop_in/prove_with_lean.py b/examples/07_z3py_drop_in/prove_with_lean.py index 9d73dcb..f70c83f 100644 --- a/examples/07_z3py_drop_in/prove_with_lean.py +++ b/examples/07_z3py_drop_in/prove_with_lean.py @@ -20,12 +20,14 @@ # -- kernel setup ----------------------------------------------------------- + def setup_kernel(managed: bool = False): from lean_py.z3 import set_kernel if managed: from lean_py.project import ManagedProject from lean_py.utils import add_lean_lib_to_dyld_path + add_lean_lib_to_dyld_path() mp = ManagedProject.get() k = mp.kernel() @@ -36,6 +38,7 @@ def setup_kernel(managed: bool = False): from lean_py import LeanLibrary from lean_py.kernel import Kernel from lean_py.utils import add_lean_lib_to_dyld_path + add_lean_lib_to_dyld_path() # Point at tests/lean as a convenient pre-built fixture @@ -130,11 +133,12 @@ def quantifiers_and_uninterpreted(): socrates = Const("socrates", Entity) x = Const("x", Entity) - prove(Implies( - And(ForAll([x], Implies(Man(x), Mortal(x))), - Man(socrates)), - Mortal(socrates), - )) + prove( + Implies( + And(ForAll([x], Implies(Man(x), Mortal(x))), Man(socrates)), + Mortal(socrates), + ) + ) # Function congruence: f(x) = f(y) if x = y S = DeclareSort("S") diff --git a/lean_py/_parse.py b/lean_py/_parse.py index fcc3a41..770143b 100644 --- a/lean_py/_parse.py +++ b/lean_py/_parse.py @@ -9,9 +9,8 @@ from pathlib import Path import pycparser -from pycparser.c_parser import ParseError import pycparser.c_ast as c_ast - +from pycparser.c_parser import ParseError # ============================================================================ # Data model @@ -90,13 +89,7 @@ def find_lean_header() -> Path: toolchain = toolchain_file.read_text().strip() toolchain_dir = toolchain.replace("/", "--").replace(":", "---") header = ( - Path.home() - / ".elan" - / "toolchains" - / toolchain_dir - / "include" - / "lean" - / "lean.h" + Path.home() / ".elan" / "toolchains" / toolchain_dir / "include" / "lean" / "lean.h" ) if header.exists(): return header @@ -235,9 +228,7 @@ def _extract_struct(node: c_ast.Struct) -> StructDef | None: bitfield = None if decl.bitsize and isinstance(decl.bitsize, c_ast.Constant): bitfield = int(decl.bitsize.value) - fields.append( - StructField(name=fname, c_type=ftype, is_pointer=is_ptr, bitfield=bitfield) - ) + fields.append(StructField(name=fname, c_type=ftype, is_pointer=is_ptr, bitfield=bitfield)) return StructDef(name=node.name or "", fields=fields) @@ -272,9 +263,7 @@ def _extract_export_names(header_path: Path) -> set[str]: def _extract_inline_names(header_path: Path) -> set[str]: text = header_path.read_text() - pattern = re.compile( - r"static\s+inline\s+(?:LEAN_ALWAYS_INLINE\s+)?[\w\s*]+\s+(\w+)\s*\(" - ) + pattern = re.compile(r"static\s+inline\s+(?:LEAN_ALWAYS_INLINE\s+)?[\w\s*]+\s+(\w+)\s*\(") return {m.group(1) for m in pattern.finditer(text)} @@ -283,9 +272,7 @@ def _extract_inline_names(header_path: Path) -> set[str]: # ============================================================================ -def _classify( - ast: c_ast.FileAST, defines: dict[str, int], header_path: Path -) -> HeaderModel: +def _classify(ast: c_ast.FileAST, defines: dict[str, int], header_path: Path) -> HeaderModel: model = HeaderModel() model.constants = defines @@ -294,18 +281,14 @@ def _classify( for node in ast.ext: if isinstance(node, c_ast.Typedef): - if isinstance(node.type, c_ast.TypeDecl) and isinstance( - node.type.type, c_ast.Struct - ): + if isinstance(node.type, c_ast.TypeDecl) and isinstance(node.type.type, c_ast.Struct): struct = _extract_struct(node.type.type) if struct: struct.name = node.name model.structs.append(struct) continue typedef_type = _decl_type_to_str(node.type) - model.typedefs.append( - TypedefDef(name=node.name, underlying_type=typedef_type) - ) + model.typedefs.append(TypedefDef(name=node.name, underlying_type=typedef_type)) elif isinstance(node, c_ast.Decl): if isinstance(node.type, c_ast.FuncDecl): diff --git a/lean_py/_runtime.py b/lean_py/_runtime.py index 51b0179..27b792a 100644 --- a/lean_py/_runtime.py +++ b/lean_py/_runtime.py @@ -209,9 +209,7 @@ def __init__(self): self._preloaded_libs: list[ctypes.CDLL] = [] for lib in all_lean_runtime_libs(): try: - self._preloaded_libs.append( - ctypes.CDLL(str(lib), mode=ctypes.RTLD_GLOBAL) - ) + self._preloaded_libs.append(ctypes.CDLL(str(lib), mode=ctypes.RTLD_GLOBAL)) except OSError: pass # The "main" libleanshared is the source of all the symbols we @@ -245,9 +243,7 @@ def __init__(self): # init code can run with the flag still true (which is required # by Lean's `initialize` blocks), then flip it after. try: - self.lean_io_mark_end_initialization = ( - self.lib.lean_io_mark_end_initialization - ) + self.lean_io_mark_end_initialization = self.lib.lean_io_mark_end_initialization self.lean_io_mark_end_initialization.argtypes = [] self.lean_io_mark_end_initialization.restype = None except AttributeError: @@ -291,9 +287,7 @@ def _bind_exported(self, lib): try: cfunc = getattr(lib, func.name) if func.params: - cfunc.argtypes = [ - _resolve_type(p.c_type, structs) for p in func.params - ] + cfunc.argtypes = [_resolve_type(p.c_type, structs) for p in func.params] restype = _resolve_type(func.return_type, structs) if restype is not None: cfunc.restype = restype @@ -478,9 +472,7 @@ def lean_ctor_get(self, o, i): # pointer that aliases into the Lean ctor's m_objs memory. If the # ctor is later freed (lean_dec), an aliased pointer would become # stale when the Lean allocator reuses the memory. - elem_addr = ( - ctypes.addressof(ctor.contents) + offset + i * ctypes.sizeof(LeanObjectPtr) - ) + elem_addr = ctypes.addressof(ctor.contents) + offset + i * ctypes.sizeof(LeanObjectPtr) raw_val = c_void_p.from_address(elem_addr).value or 0 return ctypes.cast(c_void_p(raw_val), LeanObjectPtr) @@ -572,9 +564,7 @@ def lean_alloc_ctor(self, tag, num_objs, scalar_sz): def lean_alloc_array(self, size, capacity): fn = self._find_leanpy_helper("leanpy_alloc_array") if fn is None: - raise RuntimeError( - "leanpy_alloc_array not found — leanpy_native not linked" - ) + raise RuntimeError("leanpy_alloc_array not found — leanpy_native not linked") fn.argtypes = [c_size_t, c_size_t] fn.restype = LeanObjectPtr return fn(size, capacity) @@ -644,9 +634,7 @@ def lean_uint64_to_nat(self, n): big.argtypes = [c_uint64] big.restype = LeanObjectPtr return big(c_uint64(n).value) - raise RuntimeError( - f"Cannot convert uint64 {n} to Nat: lean_big_uint64_to_nat not found" - ) + raise RuntimeError(f"Cannot convert uint64 {n} to Nat: lean_big_uint64_to_nat not found") def lean_uint64_of_nat(self, p): # Inline: small scalar fast-path; large path via lean_uint64_of_big_nat. diff --git a/lean_py/base_types.py b/lean_py/base_types.py index f5e9d5f..0485789 100644 --- a/lean_py/base_types.py +++ b/lean_py/base_types.py @@ -9,7 +9,7 @@ from ctypes import _Pointer -from lean_py._runtime import get_structs, get_constants +from lean_py._runtime import get_constants, get_structs # Dynamically created struct types _structs = get_structs() diff --git a/lean_py/kernel.py b/lean_py/kernel.py index e3f42e4..39f8763 100644 --- a/lean_py/kernel.py +++ b/lean_py/kernel.py @@ -28,8 +28,9 @@ from __future__ import annotations +from collections.abc import Iterable from dataclasses import dataclass -from typing import Any, Iterable +from typing import Any @dataclass(frozen=True) @@ -45,14 +46,14 @@ class TacticResult: status: str messages: list[str] - state: "GoalState | None" + state: GoalState | None @property def ok(self) -> bool: return self.status == "success" @classmethod - def parse(cls, encoded: str, kernel: "Kernel", raw_state: Any) -> "TacticResult": + def parse(cls, encoded: str, kernel: Kernel, raw_state: Any) -> TacticResult: """Parse the multi-line encoding produced by Lean's ``encodeTacticResult``.""" if not encoded: @@ -72,7 +73,7 @@ class GoalState: __slots__ = ("_kernel", "_handle") - def __init__(self, kernel: "Kernel", handle: Any) -> None: + def __init__(self, kernel: Kernel, handle: Any) -> None: self._kernel = kernel self._handle = handle @@ -96,33 +97,23 @@ def pretty(self) -> str: return self._kernel._lib.leanpy_kernel_goal_pretty(self._handle) def try_tactic(self, tactic: str) -> TacticResult: - encoded, next_state = self._kernel._lib.leanpy_kernel_goal_try_tactic( - self._handle, tactic - ) + encoded, next_state = self._kernel._lib.leanpy_kernel_goal_try_tactic(self._handle, tactic) return TacticResult.parse(encoded, self._kernel, next_state) def try_assign(self, expr: str) -> TacticResult: - encoded, next_state = self._kernel._lib.leanpy_kernel_goal_try_assign( - self._handle, expr - ) + encoded, next_state = self._kernel._lib.leanpy_kernel_goal_try_assign(self._handle, expr) return TacticResult.parse(encoded, self._kernel, next_state) def conv_enter(self) -> TacticResult: - encoded, next_state = self._kernel._lib.leanpy_kernel_goal_conv_enter( - self._handle - ) + encoded, next_state = self._kernel._lib.leanpy_kernel_goal_conv_enter(self._handle) return TacticResult.parse(encoded, self._kernel, next_state) def calc_enter(self) -> TacticResult: - encoded, next_state = self._kernel._lib.leanpy_kernel_goal_calc_enter( - self._handle - ) + encoded, next_state = self._kernel._lib.leanpy_kernel_goal_calc_enter(self._handle) return TacticResult.parse(encoded, self._kernel, next_state) def fragment_exit(self) -> TacticResult: - encoded, next_state = self._kernel._lib.leanpy_kernel_goal_fragment_exit( - self._handle - ) + encoded, next_state = self._kernel._lib.leanpy_kernel_goal_fragment_exit(self._handle) return TacticResult.parse(encoded, self._kernel, next_state) # ---- prograde tactics -------------------------------------------------- @@ -169,9 +160,7 @@ def goal_names(self) -> list[str]: return list(self._kernel._lib.leanpy_kernel_goal_state_goal_names(self._handle)) def parent_names(self) -> list[str]: - return list( - self._kernel._lib.leanpy_kernel_goal_state_parent_names(self._handle) - ) + return list(self._kernel._lib.leanpy_kernel_goal_state_parent_names(self._handle)) def root_name(self) -> str: return self._kernel._lib.leanpy_kernel_goal_state_root_name(self._handle) @@ -197,7 +186,7 @@ def pickle(self, path: str) -> None: # ---- resume / continue / replay / subsume ------------------------------ - def resume(self, goal_names: list[str]) -> "GoalState": + def resume(self, goal_names: list[str]) -> GoalState: next_state, err = self._kernel._lib.leanpy_kernel_goal_resume( self._handle, goal_names, @@ -206,7 +195,7 @@ def resume(self, goal_names: list[str]) -> "GoalState": raise RuntimeError(f"resume failed: {err}") return GoalState(self._kernel, next_state) - def continue_with(self, branch: "GoalState") -> "GoalState": + def continue_with(self, branch: GoalState) -> GoalState: next_state, err = self._kernel._lib.leanpy_kernel_goal_continue( self._handle, branch._handle, @@ -215,7 +204,7 @@ def continue_with(self, branch: "GoalState") -> "GoalState": raise RuntimeError(f"continue failed: {err}") return GoalState(self._kernel, next_state) - def replay(self, src: "GoalState", src_prime: "GoalState") -> "GoalState": + def replay(self, src: GoalState, src_prime: GoalState) -> GoalState: """Merge differential ``src → src_prime`` onto ``self`` (the dst).""" next_state, err = self._kernel._lib.leanpy_kernel_goal_replay( self._handle, @@ -228,7 +217,7 @@ def replay(self, src: "GoalState", src_prime: "GoalState") -> "GoalState": def subsume( self, goal_name: str, candidate_names: list[str] - ) -> tuple[str, "GoalState | None", str]: + ) -> tuple[str, GoalState | None, str]: """Try to discharge ``goal_name`` using one of ``candidate_names``. Returns (``"none"|"subsumed"|"cycle"|"error"``, optional new state, optional name of the candidate that subsumed).""" @@ -237,9 +226,7 @@ def subsume( goal_name, candidate_names, ) - next_gs = ( - GoalState(self._kernel, next_state) if next_state is not None else None - ) + next_gs = GoalState(self._kernel, next_state) if next_state is not None else None return label, next_gs, sub_name def __repr__(self) -> str: diff --git a/lean_py/lean_ffi.py b/lean_py/lean_ffi.py index 1fd53b1..772b88e 100644 --- a/lean_py/lean_ffi.py +++ b/lean_py/lean_ffi.py @@ -5,7 +5,7 @@ by parsing lean.h — no generated files needed. """ -from lean_py._runtime import get_lean_ffi, get_ffi_class +from lean_py._runtime import get_ffi_class, get_lean_ffi LeanFFI = get_ffi_class() diff --git a/lean_py/lean_types.py b/lean_py/lean_types.py index 063325b..32a5717 100644 --- a/lean_py/lean_types.py +++ b/lean_py/lean_types.py @@ -7,8 +7,9 @@ # Higher-level Python Type Wrappers # ============================================================================ -from ctypes import POINTER, addressof import ctypes +from ctypes import POINTER, addressof + from lean_py.base_types import LeanArrayObject, LeanStringObject from lean_py.lean_ffi import LeanFFI, get_lean_ffi @@ -68,9 +69,7 @@ def get(self, index): """Get element at index.""" array_obj = ctypes.cast(self.ptr, POINTER(LeanArrayObject)).contents if index < 0 or index >= array_obj.m_size: - raise IndexError( - f"Index {index} out of bounds for array of size {array_obj.m_size}" - ) + raise IndexError(f"Index {index} out of bounds for array of size {array_obj.m_size}") elem_ptr = array_obj.m_data[index] self.ffi.inc_ref(elem_ptr) diff --git a/lean_py/library.py b/lean_py/library.py index aea7fce..de29755 100644 --- a/lean_py/library.py +++ b/lean_py/library.py @@ -24,9 +24,10 @@ import os import subprocess import sys +from collections.abc import Callable from ctypes import POINTER, c_uint8, c_void_p from pathlib import Path -from typing import Any, Callable +from typing import Any from lean_py._runtime import get_structs from lean_py.base_types import LeanObject @@ -59,11 +60,7 @@ def _list_init_symbols(dylib: Path) -> list[str]: # macOS prefixes exported symbols with `_`; strip that. if sym.startswith("_"): sym = sym[1:] - if ( - sym.startswith("initialize_") - and "Lean_" not in sym - and "LeanPy_" not in sym - ): + if sym.startswith("initialize_") and "Lean_" not in sym and "LeanPy_" not in sym: candidates.append(sym) return candidates @@ -175,16 +172,13 @@ def __init__(self, ti: TypeInfo, marshaller: Marshaller): def __call__(self, *args, **kwargs) -> LeanInductiveValue: if kwargs: raise TypeError( - f"{self._ti.name}: keyword fields not supported yet " - f"(use positional args)" + f"{self._ti.name}: keyword fields not supported yet (use positional args)" ) if len(args) != len(self._ctor.fields): raise TypeError( f"{self._ti.name} expects {len(self._ctor.fields)} args, got {len(args)}" ) - return LeanInductiveValue( - self._ti.name, self._ctor.name, self._ctor.tag, tuple(args) - ) + return LeanInductiveValue(self._ti.name, self._ctor.name, self._ctor.tag, tuple(args)) # ============================================================================ @@ -192,9 +186,7 @@ def __call__(self, *args, **kwargs) -> LeanInductiveValue: # ============================================================================ -def _build_callable( - lib: ctypes.CDLL, finfo: FuncInfo, marshaller: Marshaller -) -> Callable: +def _build_callable(lib: ctypes.CDLL, finfo: FuncInfo, marshaller: Marshaller) -> Callable: """Build a Python wrapper around an `@[export]`'d Lean function. Conventions for the C ABI of Lean-exported functions: @@ -241,17 +233,13 @@ def _ctype_for_call(ct): # If the return is a pointer, we need to cast it back to LeanObjectPtr # before handing it to the unmarshaller. LObjPtr = get_structs()["_LeanObjectPtr"] - return_is_pointer = isinstance(rwrap.ctype, type) and issubclass( - rwrap.ctype, ctypes._Pointer - ) + return_is_pointer = isinstance(rwrap.ctype, type) and issubclass(rwrap.ctype, ctypes._Pointer) _ffi = get_lean_ffi() def _wrapper(*args): if len(args) != len(pwraps): - raise TypeError( - f"{finfo.exportName}: expected {len(pwraps)} args, got {len(args)}" - ) + raise TypeError(f"{finfo.exportName}: expected {len(pwraps)} args, got {len(args)}") cargs = [] for w, a in zip(pwraps, args): v = w.to_lean(a) @@ -296,7 +284,7 @@ def from_lake( library_name: str | None = None, *, build: bool = False, - ) -> "LeanLibrary": + ) -> LeanLibrary: """Load a Lean library from a Lake project directory. Looks for `/.lake/build/lib/lib.` @@ -348,9 +336,7 @@ def _diagnostic() -> str: if not build_root.is_dir(): return f"{build_root} does not exist (lake build did not run or failed)" entries = sorted( - str(p.relative_to(build_root)) - for p in build_root.rglob("*") - if p.is_file() + str(p.relative_to(build_root)) for p in build_root.rglob("*") if p.is_file() ) return f"contents of {build_root}: {entries[:50]}" @@ -360,9 +346,7 @@ def _diagnostic() -> str: # Some Lake versions don't honour `defaultFacets = ["shared"]` # in lakefile.toml; ask for the shared facet explicitly. try: - run_command( - ["lake", "build", f"{library_name}:shared"], cwd=lake_path - ) + run_command(["lake", "build", f"{library_name}:shared"], cwd=lake_path) except Exception: pass found = _find(library_name) @@ -383,8 +367,7 @@ def _diagnostic() -> str: ] if not shared: raise FileNotFoundError( - f"no shared library found under {build_root}; run `lake build`. " - f"{_diagnostic()}" + f"no shared library found under {build_root}; run `lake build`. {_diagnostic()}" ) if len(shared) > 1: names = ", ".join(p.stem.removeprefix("lib") for p in shared) @@ -568,10 +551,7 @@ def __getitem__(self, key: str) -> Any: raise KeyError(key) def __repr__(self) -> str: - return ( - f"" - ) + return f"" # Re-export under both names for compatibility. diff --git a/lean_py/marshal.py b/lean_py/marshal.py index 67ecc10..41001d8 100644 --- a/lean_py/marshal.py +++ b/lean_py/marshal.py @@ -23,6 +23,7 @@ import ctypes import struct as _struct +from collections.abc import Callable from ctypes import ( c_double, c_int8, @@ -36,13 +37,12 @@ c_uint64, c_void_p, ) -from typing import Any, Callable +from typing import Any from lean_py._runtime import _ptr_as_int, get_lean_ffi, get_structs from lean_py.exceptions import LeanError, LeanPyCallbackError, parse_io_error_message from lean_py.registry import CtorInfo, LibraryRegistry, TypeInfo, TypeRepr - # ============================================================================ # Owned wrapper around a lean_object* # ============================================================================ @@ -67,7 +67,7 @@ def __init__(self, ptr: Any, *, owned: bool = True) -> None: self._owned = owned @classmethod - def borrow(cls, ptr: Any) -> "LeanObj": + def borrow(cls, ptr: Any) -> LeanObj: ffi = get_lean_ffi() if ptr: ffi.lean_inc(ptr) @@ -191,8 +191,7 @@ def __call__(cls, *args): n_fields = len(cls.__match_args__) if hasattr(cls, "__match_args__") else 0 if len(args) != n_fields: raise TypeError( - f"{cls._type_name}.{cls._ctor_name} expects {n_fields} args, " - f"got {len(args)}" + f"{cls._type_name}.{cls._ctor_name} expects {n_fields} args, got {len(args)}" ) # Convert zero-arg _CtorMeta sentinels to LeanInductiveValue so that # all tree nodes are uniformly LeanInductiveValue for pattern matching. @@ -206,16 +205,10 @@ def __call__(cls, *args): def __instancecheck__(cls, instance): if isinstance(instance, LeanInductiveValue): - return ( - instance.ctor == cls._ctor_name - and instance._type_name == cls._type_name - ) + return instance.ctor == cls._ctor_name and instance._type_name == cls._type_name if type(instance) is _CtorMeta: # Allow isinstance(Color.red, Color.red) — both are _CtorMeta classes - return ( - instance._ctor_name == cls._ctor_name - and instance._type_name == cls._type_name - ) + return instance._ctor_name == cls._ctor_name and instance._type_name == cls._type_name return False def __repr__(cls): @@ -229,10 +222,7 @@ def __eq__(cls, other): and other.fields == () ) if isinstance(other, _CtorMeta): - return ( - cls._type_name == other._type_name - and cls._ctor_name == other._ctor_name - ) + return cls._type_name == other._type_name and cls._ctor_name == other._ctor_name return NotImplemented def __hash__(cls): @@ -272,17 +262,13 @@ def __getattr__(self, name: str) -> Any: idx = int(name[1:]) if idx < len(self.fields): return self.fields[idx] - raise AttributeError( - f"field index {idx} out of range (have {len(self.fields)} fields)" - ) + raise AttributeError(f"field index {idx} out of range (have {len(self.fields)} fields)") raise AttributeError(name) def __repr__(self) -> str: if not self.fields: return f"{self._type_name}.{self.ctor}" - return ( - f"{self._type_name}.{self.ctor}({', '.join(repr(f) for f in self.fields)})" - ) + return f"{self._type_name}.{self.ctor}({', '.join(repr(f) for f in self.fields)})" def __eq__(self, other: object) -> bool: if isinstance(other, LeanInductiveValue): @@ -417,9 +403,7 @@ def _mk(ffi, ObjPtr, ch, _fn=fn, _n=nargs, _st=scalar_tail): # type: ignore[mis for i, c in enumerate(ch[:_n]): if _st and i == _n - 1: # Trailing BinderInfo / Bool — unbox to uint8. - c_args.append( - ffi.lean_unbox(c) if ffi.lean_is_scalar(c) else _ptr_as_int(c) - ) + c_args.append(ffi.lean_unbox(c) if ffi.lean_is_scalar(c) else _ptr_as_int(c)) else: c_args.append(_ptr_as_int(c)) _fn.restype = c_void_p @@ -470,7 +454,7 @@ def _py_to_lean_string(self, s: str) -> Any: raise TypeError(f"expected str, got {type(s).__name__}") return self.ffi.mk_string(s) - def _lean_array_to_py(self, ptr: Any, elem_w: "TypeWrapper") -> list: + def _lean_array_to_py(self, ptr: Any, elem_w: TypeWrapper) -> list: n = self.ffi.lean_array_size(ptr) out = [] for i in range(n): @@ -481,7 +465,7 @@ def _lean_array_to_py(self, ptr: Any, elem_w: "TypeWrapper") -> list: out.append(elem_w.from_lean(e_ptr)) return out - def _py_to_lean_array(self, xs, elem_w: "TypeWrapper") -> Any: + def _py_to_lean_array(self, xs, elem_w: TypeWrapper) -> Any: """Build a Lean Array from a Python iterable. Returns owned ptr.""" items = list(xs) arr = self.ffi.lean_alloc_array(len(items), len(items)) @@ -634,9 +618,7 @@ def _encode_inductive(self, ti: TypeInfo, value: Any) -> Any: # -- public -------------------------------------------------------------- - def decode_lean_obj( - self, type_name: str, lean_obj: "LeanObj" - ) -> LeanInductiveValue: + def decode_lean_obj(self, type_name: str, lean_obj: LeanObj) -> LeanInductiveValue: """Decode a ``LeanObj`` (raw ``lean_object*``) as a registered inductive. This is the entry point for Path B (tactic): Lean wraps an ``Expr`` @@ -756,12 +738,8 @@ def to_lean(f): to_lean, c_double, ctor_scalar_size=8, - from_ctor_scalar=lambda raw: _struct.unpack( - "d", _struct.pack("Q", raw) - )[0], - to_ctor_scalar=lambda f: _struct.unpack( - "Q", _struct.pack("d", float(f)) - )[0], + from_ctor_scalar=lambda raw: _struct.unpack("d", _struct.pack("Q", raw))[0], + to_ctor_scalar=lambda f: _struct.unpack("Q", _struct.pack("d", float(f)))[0], ) if k == "uint": @@ -1161,7 +1139,7 @@ def _string_field(self, ptr: Any, idx: int) -> str: except Exception: return "" - def _build_io_exception(self, ptr: Any) -> "Exception": + def _build_io_exception(self, ptr: Any) -> Exception: """Decode an `IO.Error` ctor pointer into a typed exception. For `userError` — the most common, used by every `LeanPy.Python.*` diff --git a/lean_py/project.py b/lean_py/project.py index aa15680..f48c62e 100644 --- a/lean_py/project.py +++ b/lean_py/project.py @@ -17,7 +17,8 @@ import json import os import shutil -from importlib.metadata import distribution, version as pkg_version +from importlib.metadata import distribution +from importlib.metadata import version as pkg_version from pathlib import Path from lean_py.kernel import Kernel diff --git a/lean_py/registry.py b/lean_py/registry.py index 64a9f61..2a2b764 100644 --- a/lean_py/registry.py +++ b/lean_py/registry.py @@ -35,14 +35,14 @@ class TypeRepr: kind: str # Optional fields, depending on kind bits: int | None = None - elem: "TypeRepr | None" = None - a: "TypeRepr | None" = None - b: "TypeRepr | None" = None - e: "TypeRepr | None" = None + elem: TypeRepr | None = None + a: TypeRepr | None = None + b: TypeRepr | None = None + e: TypeRepr | None = None name: str | None = None @classmethod - def from_json(cls, data: dict[str, Any]) -> "TypeRepr": + def from_json(cls, data: dict[str, Any]) -> TypeRepr: kind = data["kind"] kw: dict[str, Any] = {"kind": kind} if "bits" in data: @@ -111,7 +111,7 @@ class CtorInfo: fields: tuple[TypeRepr, ...] @classmethod - def from_json(cls, data: dict[str, Any]) -> "CtorInfo": + def from_json(cls, data: dict[str, Any]) -> CtorInfo: return cls( name=data["name"], tag=int(data["tag"]), @@ -136,7 +136,7 @@ class TypeInfo: ctors: tuple[CtorInfo, ...] @classmethod - def from_json(cls, data: dict[str, Any]) -> "TypeInfo": + def from_json(cls, data: dict[str, Any]) -> TypeInfo: return cls( name=data["name"], isStructure=bool(data.get("isStructure", False)), @@ -162,7 +162,7 @@ class FuncInfo: returnType: TypeRepr @classmethod - def from_json(cls, data: dict[str, Any]) -> "FuncInfo": + def from_json(cls, data: dict[str, Any]) -> FuncInfo: return cls( declName=data["declName"], exportName=data["exportName"], @@ -186,7 +186,7 @@ class LibraryRegistry: types: tuple[TypeInfo, ...] = field(default_factory=tuple) @classmethod - def from_json_strings(cls, funcs_json: str, types_json: str) -> "LibraryRegistry": + def from_json_strings(cls, funcs_json: str, types_json: str) -> LibraryRegistry: farr = json.loads(funcs_json) if funcs_json else [] tarr = json.loads(types_json) if types_json else [] # Dedupe types by name. `derive_python` for recursive inductives diff --git a/lean_py/z3/_ast.py b/lean_py/z3/_ast.py index dc73846..8b26ff6 100644 --- a/lean_py/z3/_ast.py +++ b/lean_py/z3/_ast.py @@ -7,7 +7,6 @@ from __future__ import annotations from dataclasses import dataclass -from typing import Union # --------------------------------------------------------------------------- # Sorts @@ -88,22 +87,22 @@ class SeqASTSort: elem: ASTSort -ASTSort = Union[ - PropSort, - IntASTSort, - NatASTSort, - RealASTSort, - BitvecASTSort, - TypeASTSort, - UninterpASTSort, - ArrowASTSort, - StringASTSort, - FpASTSort, - FinDomainASTSort, - InductiveASTSort, - CharASTSort, - SeqASTSort, -] +ASTSort = ( + PropSort + | IntASTSort + | NatASTSort + | RealASTSort + | BitvecASTSort + | TypeASTSort + | UninterpASTSort + | ArrowASTSort + | StringASTSort + | FpASTSort + | FinDomainASTSort + | InductiveASTSort + | CharASTSort + | SeqASTSort +) # --------------------------------------------------------------------------- # Operations @@ -548,69 +547,69 @@ class SeqNthNode: idx: ASTNode -ASTNode = Union[ - Var, - IntLit, - NatLit, - BoolLit, - BvLit, - BinOpNode, - UnOpNode, - IteNode, - ForAllNode, - ExistsNode, - AppNode, - DistinctNode, - SelectNode, - StoreNode, - ConstArrayNode, - ExtractNode, - ZeroExtNode, - SignExtNode, - Int2BvNode, - ToRealNode, - ToIntNode, - LambdaNode, - StringLit, - StrLenNode, - StrContainsNode, - StrPrefixOfNode, - StrSuffixOfNode, - StrReplaceNode, - StrConcatNode, - StrSubstrNode, - StrIndexOfNode, - StrToIntNode, - IntToStrNode, - ReStarNode, - RePlusNode, - ReOptionNode, - ReUnionNode, - ReIntersectNode, - ReConcatNode, - ReRangeNode, - ReComplementNode, - ReLoopNode, - InReNode, - FpLitNode, - FpOpNode, - FinDomainLit, - InductiveCtorNode, - InductiveAccessorNode, - InductiveRecognizerNode, - CharLit, - CharToNatNode, - CharFromBvNode, - CharIsDigitNode, - SeqEmptyNode, - SeqUnitNode, - SeqLenNode, - SeqConcatNode, - SeqContainsNode, - SeqPrefixOfNode, - SeqSuffixOfNode, - SeqNthNode, -] +ASTNode = ( + Var + | IntLit + | NatLit + | BoolLit + | BvLit + | BinOpNode + | UnOpNode + | IteNode + | ForAllNode + | ExistsNode + | AppNode + | DistinctNode + | SelectNode + | StoreNode + | ConstArrayNode + | ExtractNode + | ZeroExtNode + | SignExtNode + | Int2BvNode + | ToRealNode + | ToIntNode + | LambdaNode + | StringLit + | StrLenNode + | StrContainsNode + | StrPrefixOfNode + | StrSuffixOfNode + | StrReplaceNode + | StrConcatNode + | StrSubstrNode + | StrIndexOfNode + | StrToIntNode + | IntToStrNode + | ReStarNode + | RePlusNode + | ReOptionNode + | ReUnionNode + | ReIntersectNode + | ReConcatNode + | ReRangeNode + | ReComplementNode + | ReLoopNode + | InReNode + | FpLitNode + | FpOpNode + | FinDomainLit + | InductiveCtorNode + | InductiveAccessorNode + | InductiveRecognizerNode + | CharLit + | CharToNatNode + | CharFromBvNode + | CharIsDigitNode + | SeqEmptyNode + | SeqUnitNode + | SeqLenNode + | SeqConcatNode + | SeqContainsNode + | SeqPrefixOfNode + | SeqSuffixOfNode + | SeqNthNode +) __all__ = [ # Sorts diff --git a/lean_py/z3/_inductive_reg.py b/lean_py/z3/_inductive_reg.py index bb3c765..56eaff0 100644 --- a/lean_py/z3/_inductive_reg.py +++ b/lean_py/z3/_inductive_reg.py @@ -8,7 +8,27 @@ from typing import Any -from lean_py.z3._ast import InductiveASTSort +from lean_py.z3._ast import ( + ArrowASTSort, + InductiveASTSort, + SeqASTSort, + UninterpASTSort, +) + +# Uninterpreted sort names that have been declared as Lean axioms. +# These should not be treated as free type variables in expressions. +_declared_uninterp_sorts: set[str] = set() + + +def _collect_uninterp_sorts(ast_sort: Any) -> set[str]: + """Recursively collect uninterpreted sort names from an AST sort.""" + if isinstance(ast_sort, UninterpASTSort): + return {ast_sort.name} + if isinstance(ast_sort, ArrowASTSort): + return _collect_uninterp_sorts(ast_sort.dom) | _collect_uninterp_sorts(ast_sort.cod) + if isinstance(ast_sort, SeqASTSort): + return _collect_uninterp_sorts(ast_sort.elem) + return set() def _register_inductive(name: str, ctors: list[tuple[str, Any]]) -> None: @@ -18,11 +38,14 @@ def _register_inductive(name: str, ctors: list[tuple[str, Any]]) -> None: k = _get_kernel() lib = k._lib + # Collect uninterpreted sorts used in constructor fields + uninterp_names: set[str] = set() lean_ctors = [] for ctor_name, fields in ctors: lean_fields = [] for f_name, f_sort in fields: if hasattr(f_sort, "_ast_sort"): + uninterp_names |= _collect_uninterp_sorts(f_sort._ast_sort) sort = _marshal_sort(lib, f_sort._ast_sort) else: # Self-referential: f_sort is a _DatatypeBuilder @@ -32,3 +55,6 @@ def _register_inductive(name: str, ctors: list[tuple[str, Any]]) -> None: desc = lib.Z3InductiveDesc(name, lean_ctors) lib.z3_add_inductive(desc) + + # Track uninterpreted sorts that are now axioms in the Lean environment + _declared_uninterp_sorts.update(uninterp_names) diff --git a/lean_py/z3/core.py b/lean_py/z3/core.py index 4786138..0f8072b 100644 --- a/lean_py/z3/core.py +++ b/lean_py/z3/core.py @@ -14,26 +14,40 @@ import math import struct +from collections.abc import Sequence from decimal import Decimal, getcontext from fractions import Fraction -from typing import Any, Sequence +from typing import Any -from lean_py.z3._inductive_reg import _register_inductive from lean_py.z3._ast import ( - ASTNode, - ASTSort, AppNode, ArrowASTSort, - BitvecASTSort, + ASTNode, + ASTSort, BinOp, BinOpNode, + BitvecASTSort, BoolLit, BvLit, + CharASTSort, + CharFromBvNode, + CharIsDigitNode, + CharLit, + CharToNatNode, ConstArrayNode, DistinctNode, ExistsNode, ExtractNode, + FinDomainASTSort, + FinDomainLit, ForAllNode, + FpASTSort, + FpLitNode, + FpOpNode, + InductiveAccessorNode, + InductiveASTSort, + InductiveCtorNode, + InductiveRecognizerNode, InReNode, Int2BvNode, IntASTSort, @@ -45,8 +59,8 @@ NatLit, PropSort, RealASTSort, - ReConcatNode, ReComplementNode, + ReConcatNode, ReIntersectNode, ReLoopNode, ReOptionNode, @@ -55,51 +69,40 @@ ReStarNode, ReUnionNode, SelectNode, + SeqASTSort, + SeqConcatNode, + SeqContainsNode, + SeqEmptyNode, + SeqLenNode, + SeqNthNode, + SeqPrefixOfNode, + SeqSuffixOfNode, + SeqUnitNode, SignExtNode, StoreNode, StrConcatNode, StrContainsNode, StrIndexOfNode, + StringASTSort, + StringLit, StrLenNode, StrPrefixOfNode, StrReplaceNode, StrSubstrNode, StrSuffixOfNode, StrToIntNode, - StringASTSort, - StringLit, ToIntNode, ToRealNode, - UnOp, TypeASTSort, - UnOpNode, UninterpASTSort, - Var as _AstVar, + UnOp, + UnOpNode, ZeroExtNode, - FpASTSort, - FpLitNode, - FpOpNode, - FinDomainASTSort, - FinDomainLit, - InductiveASTSort, - InductiveCtorNode, - InductiveAccessorNode, - InductiveRecognizerNode, - CharASTSort, - CharLit, - CharToNatNode, - CharFromBvNode, - CharIsDigitNode, - SeqASTSort, - SeqEmptyNode, - SeqUnitNode, - SeqLenNode, - SeqConcatNode, - SeqContainsNode, - SeqPrefixOfNode, - SeqSuffixOfNode, - SeqNthNode, ) +from lean_py.z3._ast import ( + Var as _AstVar, +) +from lean_py.z3._inductive_reg import _declared_uninterp_sorts, _register_inductive def _is_literal(node: ASTNode) -> bool: @@ -329,9 +332,7 @@ def __hash__(self) -> int: return hash(self._ast) def __bool__(self) -> bool: - raise TypeError( - "Symbolic expressions cannot be cast to concrete Boolean values" - ) + raise TypeError("Symbolic expressions cannot be cast to concrete Boolean values") def num_args(self) -> int: """Number of arguments (children) of this expression.""" @@ -802,9 +803,7 @@ def __init__( ) -> None: # Build nested ForAllNode/ExistsNode from inside out bound_names = frozenset( - (v._ast.name, v._sort._ast_sort) - for v in bound - if isinstance(v._ast, _AstVar) + (v._ast.name, v._sort._ast_sort) for v in bound if isinstance(v._ast, _AstVar) ) free = body._vars - bound_names @@ -919,20 +918,16 @@ def __init__( def __call__(self, *args: ExprRef) -> ExprRef: if len(args) != len(self._domain): - raise TypeError( - f"{self._name} expects {len(self._domain)} args, got {len(args)}" - ) - merged: frozenset[tuple[str, ASTSort]] = frozenset().union( - *(a._vars for a in args) - ) + raise TypeError(f"{self._name} expects {len(self._domain)} args, got {len(args)}") + merged: frozenset[tuple[str, ASTSort]] = frozenset().union(*(a._vars for a in args)) # The function itself is a free variable merged = merged | frozenset([(self._name, self._ast_sort)]) # Uninterpreted sorts used by the function are also free + # (unless already declared as axioms in the Lean environment) for s in (*self._domain, self._range): - if isinstance(s, UninterpretedSortRef) and isinstance( - s._ast_sort, UninterpASTSort - ): - merged = merged | frozenset([(s._ast_sort.name, TypeASTSort())]) + if isinstance(s, UninterpretedSortRef) and isinstance(s._ast_sort, UninterpASTSort): + if s._ast_sort.name not in _declared_uninterp_sorts: + merged = merged | frozenset([(s._ast_sort.name, TypeASTSort())]) func_ast = _AstVar(self._name) args_ast = tuple(a._ast for a in args) ast = AppNode(func_ast, args_ast) if args else func_ast @@ -977,9 +972,7 @@ def __init__( def __call__(self, *args: ExprRef) -> DatatypeRef: if len(args) != len(self._domain): - raise TypeError( - f"{self._ctor_name} expects {len(self._domain)} args, got {len(args)}" - ) + raise TypeError(f"{self._ctor_name} expects {len(self._domain)} args, got {len(args)}") coerced = [] for a, d in zip(args, self._domain): if isinstance(a, (int, float)): @@ -988,9 +981,7 @@ def __call__(self, *args: ExprRef) -> DatatypeRef: merged: frozenset[tuple[str, ASTSort]] = ( frozenset().union(*(a._vars for a in coerced)) if coerced else frozenset() ) - ast = InductiveCtorNode( - self._type_name, self._ctor_name, tuple(a._ast for a in coerced) - ) + ast = InductiveCtorNode(self._type_name, self._ctor_name, tuple(a._ast for a in coerced)) return DatatypeRef(ast, self._result_sort, merged) @@ -1106,11 +1097,13 @@ def Array(name: str, domain: SortRef, range_sort: SortRef) -> ArrayRef: def Const(name: str, sort: SortRef) -> ExprRef: v: frozenset[tuple[str, ASTSort]] = frozenset([(name, sort._ast_sort)]) - # If the sort is uninterpreted, also track it as a free type variable. - if isinstance(sort, UninterpretedSortRef) and isinstance( - sort._ast_sort, UninterpASTSort - ): - v = v | frozenset([(sort._ast_sort.name, TypeASTSort())]) + # If the sort is uninterpreted and not yet declared as a Lean axiom, + # track it as a free type variable so ForAll wraps it. Sorts that + # have been declared (e.g. used in a Datatype field) are already + # axioms in the Lean environment and must not be re-bound. + if isinstance(sort, UninterpretedSortRef) and isinstance(sort._ast_sort, UninterpASTSort): + if sort._ast_sort.name not in _declared_uninterp_sorts: + v = v | frozenset([(sort._ast_sort.name, TypeASTSort())]) if isinstance(sort, BoolSortRef): return BoolRef(_AstVar(name), v) if isinstance(sort, ArithSortRef): @@ -1153,10 +1146,10 @@ def RealVal(n: int | float | str) -> ArithRef: return RatNumRef(num, den) if isinstance(n, str): if "/" in n: - num, den = n.split("/", 1) - return RatNumRef(int(num.strip()), int(den.strip())) - n = float(n) if "." in n or "e" in n.lower() else int(n) - return RealVal(n) + num_s, den_s = n.split("/", 1) + return RatNumRef(int(num_s.strip()), int(den_s.strip())) + coerced: int | float = float(n) if "." in n or "e" in n.lower() else int(n) + return RealVal(coerced) return ArithRef(ToRealNode(IntLit(n)), RealSort()) @@ -1197,9 +1190,7 @@ def Store(a: ArrayRef, idx: ExprRef, val: ExprRef) -> ArrayRef: sort = a._sort if not isinstance(sort, ArraySortRef): raise TypeError(f"Store requires ArrayRef, got {type(a)}") - merged: frozenset[tuple[str, ASTSort]] = frozenset().union( - a._vars, idx._vars, val._vars - ) + merged: frozenset[tuple[str, ASTSort]] = frozenset().union(a._vars, idx._vars, val._vars) return ArrayRef( StoreNode(a._ast, idx._ast, val._ast), sort, @@ -1227,13 +1218,9 @@ class _DatatypeBuilder: def __init__(self, name: str) -> None: self._name = name - self._ctors: list[ - tuple[str, tuple[tuple[str, SortRef | _DatatypeBuilder], ...]] - ] = [] + self._ctors: list[tuple[str, tuple[tuple[str, SortRef | _DatatypeBuilder], ...]]] = [] - def declare( - self, ctor_name: str, *fields: tuple[str, SortRef | _DatatypeBuilder] - ) -> None: + def declare(self, ctor_name: str, *fields: tuple[str, SortRef | _DatatypeBuilder]) -> None: self._ctors.append((ctor_name, tuple(fields))) def create(self) -> DatatypeSortRef: @@ -1244,9 +1231,7 @@ def create(self) -> DatatypeSortRef: for ctor_name, fields in self._ctors: if fields: domain = tuple( - DatatypeSortRef( - InductiveASTSort(f[1]._name), f[1]._name, f[1]._ctors - ) + DatatypeSortRef(InductiveASTSort(f[1]._name), f[1]._name, f[1]._ctors) if isinstance(f[1], _DatatypeBuilder) else f[1] for f in fields @@ -1256,16 +1241,12 @@ def create(self) -> DatatypeSortRef: sort._constructors.append(ctor) else: # Nullary: z3py stores a DatatypeRef directly - val = DatatypeRef( - InductiveCtorNode(self._name, ctor_name, ()), sort, frozenset() - ) + val = DatatypeRef(InductiveCtorNode(self._name, ctor_name, ()), sort, frozenset()) setattr(sort, ctor_name, val) sort._constructors.append(val) # Recognizer: sort.is_ - rec = _InductiveRecognizerDecl( - self._name, f"is_{ctor_name}", (sort,), BoolSort() - ) + rec = _InductiveRecognizerDecl(self._name, f"is_{ctor_name}", (sort,), BoolSort()) setattr(sort, f"is_{ctor_name}", rec) sort._recognizers.append(rec) @@ -1274,9 +1255,7 @@ def create(self) -> DatatypeSortRef: for field_name, field_sort in fields: if isinstance(field_sort, _DatatypeBuilder): field_sort = sort # self-reference - acc = _InductiveAccessorDecl( - self._name, field_name, (sort,), field_sort - ) + acc = _InductiveAccessorDecl(self._name, field_name, (sort,), field_sort) setattr(sort, field_name, acc) ctor_accessors.append(acc) sort._accessors.append(ctor_accessors) @@ -1368,9 +1347,7 @@ def Xor(a: BoolRef, b: BoolRef) -> BoolRef: def If(c: BoolRef, t: ExprRef, e: ExprRef) -> ExprRef: - merged: frozenset[tuple[str, ASTSort]] = frozenset().union( - c._vars, t._vars, e._vars - ) + merged: frozenset[tuple[str, ASTSort]] = frozenset().union(c._vars, t._vars, e._vars) ast = IteNode(c._ast, t._ast, e._ast) sort = t._sort # Return the appropriate subclass so arithmetic/comparison ops work @@ -1584,9 +1561,7 @@ def Concat(*args: BitVecRef) -> BitVecRef: for b in args[1:]: a_sort = result._sort b_sort = b._sort - if not isinstance(a_sort, BitVecSortRef) or not isinstance( - b_sort, BitVecSortRef - ): + if not isinstance(a_sort, BitVecSortRef) or not isinstance(b_sort, BitVecSortRef): raise TypeError("Concat requires BitVecRef arguments") width = a_sort._width + b_sort._width result = BitVecRef( @@ -1803,9 +1778,7 @@ def _substitute_ast(ast: ASTNode, mapping: dict[str, ASTNode]) -> ASTNode: if isinstance(ast, DistinctNode): return DistinctNode(tuple(_substitute_ast(a, mapping) for a in ast.args)) if isinstance(ast, SelectNode): - return SelectNode( - _substitute_ast(ast.arr, mapping), _substitute_ast(ast.idx, mapping) - ) + return SelectNode(_substitute_ast(ast.arr, mapping), _substitute_ast(ast.idx, mapping)) if isinstance(ast, StoreNode): return StoreNode( _substitute_ast(ast.arr, mapping), @@ -1831,9 +1804,7 @@ def _substitute_ast(ast: ASTNode, mapping: dict[str, ASTNode]) -> ASTNode: inner.pop(ast.name, None) return LambdaNode(ast.name, ast.sort, _substitute_ast(ast.body, inner)) if isinstance(ast, StrConcatNode): - return StrConcatNode( - _substitute_ast(ast.lhs, mapping), _substitute_ast(ast.rhs, mapping) - ) + return StrConcatNode(_substitute_ast(ast.lhs, mapping), _substitute_ast(ast.rhs, mapping)) if isinstance(ast, StrLenNode): return StrLenNode(_substitute_ast(ast.arg, mapping)) if isinstance(ast, StrContainsNode): @@ -1871,9 +1842,7 @@ def _substitute_ast(ast: ASTNode, mapping: dict[str, ASTNode]) -> ASTNode: if isinstance(ast, IntToStrNode): return IntToStrNode(_substitute_ast(ast.arg, mapping)) if isinstance(ast, InReNode): - return InReNode( - _substitute_ast(ast.s, mapping), _substitute_ast(ast.re, mapping) - ) + return InReNode(_substitute_ast(ast.s, mapping), _substitute_ast(ast.re, mapping)) if isinstance(ast, ReStarNode): return ReStarNode(_substitute_ast(ast.arg, mapping)) if isinstance(ast, RePlusNode): @@ -1881,17 +1850,11 @@ def _substitute_ast(ast: ASTNode, mapping: dict[str, ASTNode]) -> ASTNode: if isinstance(ast, ReOptionNode): return ReOptionNode(_substitute_ast(ast.arg, mapping)) if isinstance(ast, ReUnionNode): - return ReUnionNode( - _substitute_ast(ast.a, mapping), _substitute_ast(ast.b, mapping) - ) + return ReUnionNode(_substitute_ast(ast.a, mapping), _substitute_ast(ast.b, mapping)) if isinstance(ast, ReIntersectNode): - return ReIntersectNode( - _substitute_ast(ast.a, mapping), _substitute_ast(ast.b, mapping) - ) + return ReIntersectNode(_substitute_ast(ast.a, mapping), _substitute_ast(ast.b, mapping)) if isinstance(ast, ReConcatNode): - return ReConcatNode( - _substitute_ast(ast.a, mapping), _substitute_ast(ast.b, mapping) - ) + return ReConcatNode(_substitute_ast(ast.a, mapping), _substitute_ast(ast.b, mapping)) if isinstance(ast, ReComplementNode): return ReComplementNode(_substitute_ast(ast.arg, mapping)) if isinstance(ast, ReLoopNode): @@ -2351,23 +2314,17 @@ def SuffixOf(suf: StringRef | SeqRef, s: StringRef | SeqRef) -> BoolRef: def Replace(s: StringRef, old: StringRef, new: StringRef) -> StringRef: """Replace first occurrence of old with new in s.""" - merged: frozenset[tuple[str, ASTSort]] = frozenset().union( - s._vars, old._vars, new._vars - ) + merged: frozenset[tuple[str, ASTSort]] = frozenset().union(s._vars, old._vars, new._vars) return StringRef(StrReplaceNode(s._ast, old._ast, new._ast), merged) -def SubString( - s: StringRef, offset: ArithRef | int, length: ArithRef | int -) -> StringRef: +def SubString(s: StringRef, offset: ArithRef | int, length: ArithRef | int) -> StringRef: """Extract substring.""" if isinstance(offset, int): offset = IntVal(offset) if isinstance(length, int): length = IntVal(length) - merged: frozenset[tuple[str, ASTSort]] = frozenset().union( - s._vars, offset._vars, length._vars - ) + merged: frozenset[tuple[str, ASTSort]] = frozenset().union(s._vars, offset._vars, length._vars) return StringRef(StrSubstrNode(s._ast, offset._ast, length._ast), merged) @@ -2375,9 +2332,7 @@ def IndexOf(s: StringRef, substr: StringRef, offset: ArithRef | int = 0) -> Arit """Find index of substr in s starting at offset.""" if isinstance(offset, int): offset = IntVal(offset) - merged: frozenset[tuple[str, ASTSort]] = frozenset().union( - s._vars, substr._vars, offset._vars - ) + merged: frozenset[tuple[str, ASTSort]] = frozenset().union(s._vars, substr._vars, offset._vars) return ArithRef(StrIndexOfNode(s._ast, substr._ast, offset._ast), IntSort(), merged) @@ -2462,9 +2417,7 @@ def Intersect(*args: ReRef) -> ReRef: raise TypeError("Intersect requires at least 2 arguments") result = args[0] for a in args[1:]: - result = ReRef( - ReIntersectNode(result._ast, a._ast), _merge(result._vars, a._vars) - ) + result = ReRef(ReIntersectNode(result._ast, a._ast), _merge(result._vars, a._vars)) return result @@ -2847,9 +2800,7 @@ def _ast_decl_name(node: ASTNode) -> str: return type(node).__name__ -def _make_typed_expr( - ast: ASTNode, sort: SortRef, vars: frozenset[tuple[str, ASTSort]] -) -> ExprRef: +def _make_typed_expr(ast: ASTNode, sort: SortRef, vars: frozenset[tuple[str, ASTSort]]) -> ExprRef: """Create appropriately-typed ExprRef subclass for a sort.""" if isinstance(sort, BoolSortRef): return BoolRef(ast, vars) @@ -2963,7 +2914,9 @@ def _ast_repr(node: ASTNode) -> str: if isinstance(node, UnOpNode): return f"({node.op} {_ast_repr(node.arg)})" if isinstance(node, IteNode): - return f"(if {_ast_repr(node.cond)} then {_ast_repr(node.then_)} else {_ast_repr(node.else_)})" + return ( + f"(if {_ast_repr(node.cond)} then {_ast_repr(node.then_)} else {_ast_repr(node.else_)})" + ) if isinstance(node, ForAllNode): return f"(\u2200 {node.name}, {_ast_repr(node.body)})" if isinstance(node, ExistsNode): @@ -2977,9 +2930,7 @@ def _ast_repr(node: ASTNode) -> str: if isinstance(node, SelectNode): return f"(select {_ast_repr(node.arr)} {_ast_repr(node.idx)})" if isinstance(node, StoreNode): - return ( - f"(store {_ast_repr(node.arr)} {_ast_repr(node.idx)} {_ast_repr(node.val)})" - ) + return f"(store {_ast_repr(node.arr)} {_ast_repr(node.idx)} {_ast_repr(node.val)})" if isinstance(node, ConstArrayNode): return f"(const-array {_ast_repr(node.val)})" if isinstance(node, ExtractNode): @@ -3013,7 +2964,9 @@ def _ast_repr(node: ASTNode) -> str: if isinstance(node, StrSubstrNode): return f"(str.substr {_ast_repr(node.s)} {_ast_repr(node.offset)} {_ast_repr(node.length)})" if isinstance(node, StrIndexOfNode): - return f"(str.indexof {_ast_repr(node.s)} {_ast_repr(node.substr)} {_ast_repr(node.offset)})" + return ( + f"(str.indexof {_ast_repr(node.s)} {_ast_repr(node.substr)} {_ast_repr(node.offset)})" + ) if isinstance(node, StrToIntNode): return f"(str.to_int {_ast_repr(node.arg)})" if isinstance(node, IntToStrNode): @@ -3435,9 +3388,7 @@ def fpSqrt(rm: FPRMRef, a: FPRef, ctx: Context | None = None) -> FPRef: return _fp_op("fpSqrt", rm, a) -def fpFMA( - rm: FPRMRef, a: FPRef, b: FPRef, c: FPRef, ctx: Context | None = None -) -> FPRef: +def fpFMA(rm: FPRMRef, a: FPRef, b: FPRef, c: FPRef, ctx: Context | None = None) -> FPRef: return _fp_op("fpFMA", rm, a, b, c) @@ -3508,25 +3459,19 @@ def fpToReal(a: FPRef, ctx: Context | None = None) -> ArithRef: return ArithRef(AppNode(_AstVar("fpToReal"), (a._ast,)), RealSort(), a._vars) -def fpToSBV( - rm: FPRMRef, a: FPRef, sort: BitVecSortRef, ctx: Context | None = None -) -> BitVecRef: +def fpToSBV(rm: FPRMRef, a: FPRef, sort: BitVecSortRef, ctx: Context | None = None) -> BitVecRef: return BitVecRef( AppNode(_AstVar("fpToSBV"), (rm._ast, a._ast)), sort, _merge(rm._vars, a._vars) ) -def fpToUBV( - rm: FPRMRef, a: FPRef, sort: BitVecSortRef, ctx: Context | None = None -) -> BitVecRef: +def fpToUBV(rm: FPRMRef, a: FPRef, sort: BitVecSortRef, ctx: Context | None = None) -> BitVecRef: return BitVecRef( AppNode(_AstVar("fpToUBV"), (rm._ast, a._ast)), sort, _merge(rm._vars, a._vars) ) -def fpToFP( - rm: Any, a: Any, sort: FPSortRef | None = None, ctx: Context | None = None -) -> FPRef: +def fpToFP(rm: Any, a: Any, sort: FPSortRef | None = None, ctx: Context | None = None) -> FPRef: if sort is None: sort = Float64() merged: frozenset[tuple[str, ASTSort]] = frozenset() @@ -3542,17 +3487,11 @@ def fpBVToFP(a: BitVecRef, sort: FPSortRef, ctx: Context | None = None) -> FPRef return FPRef(AppNode(_AstVar("fpBVToFP"), (a._ast,)), sort, a._vars) -def fpFPToFP( - rm: FPRMRef, a: FPRef, sort: FPSortRef, ctx: Context | None = None -) -> FPRef: - return FPRef( - AppNode(_AstVar("fpFPToFP"), (rm._ast, a._ast)), sort, _merge(rm._vars, a._vars) - ) +def fpFPToFP(rm: FPRMRef, a: FPRef, sort: FPSortRef, ctx: Context | None = None) -> FPRef: + return FPRef(AppNode(_AstVar("fpFPToFP"), (rm._ast, a._ast)), sort, _merge(rm._vars, a._vars)) -def fpRealToFP( - rm: FPRMRef, a: ArithRef, sort: FPSortRef, ctx: Context | None = None -) -> FPRef: +def fpRealToFP(rm: FPRMRef, a: ArithRef, sort: FPSortRef, ctx: Context | None = None) -> FPRef: return FPRef( AppNode(_AstVar("fpRealToFP"), (rm._ast, a._ast)), sort, @@ -3560,9 +3499,7 @@ def fpRealToFP( ) -def fpSignedToFP( - rm: FPRMRef, a: ExprRef, sort: FPSortRef, ctx: Context | None = None -) -> FPRef: +def fpSignedToFP(rm: FPRMRef, a: ExprRef, sort: FPSortRef, ctx: Context | None = None) -> FPRef: return FPRef( AppNode(_AstVar("fpSignedToFP"), (rm._ast, a._ast)), sort, @@ -3570,9 +3507,7 @@ def fpSignedToFP( ) -def fpUnsignedToFP( - rm: FPRMRef, a: ExprRef, sort: FPSortRef, ctx: Context | None = None -) -> FPRef: +def fpUnsignedToFP(rm: FPRMRef, a: ExprRef, sort: FPSortRef, ctx: Context | None = None) -> FPRef: return FPRef( AppNode(_AstVar("fpUnsignedToFP"), (rm._ast, a._ast)), sort, @@ -3614,24 +3549,18 @@ def fpZero(sort: FPSortRef, negative: bool) -> FPNumRef: return fpPlusZero(sort) -def fpFP( - sgn: BitVecRef, exp: BitVecRef, sig: BitVecRef, ctx: Context | None = None -) -> FPRef: +def fpFP(sgn: BitVecRef, exp: BitVecRef, sig: BitVecRef, ctx: Context | None = None) -> FPRef: """Construct FP from sign/exponent/significand BitVecs.""" exp_sort = exp._sort sig_sort = sig._sort ebits = exp_sort._width if isinstance(exp_sort, BitVecSortRef) else 11 sbits = (sig_sort._width if isinstance(sig_sort, BitVecSortRef) else 52) + 1 sort = FPSort(ebits, sbits) - merged: frozenset[tuple[str, ASTSort]] = frozenset().union( - sgn._vars, exp._vars, sig._vars - ) + merged: frozenset[tuple[str, ASTSort]] = frozenset().union(sgn._vars, exp._vars, sig._vars) return FPRef(AppNode(_AstVar("fpFP"), (sgn._ast, exp._ast, sig._ast)), sort, merged) -def fpToFPUnsigned( - rm: FPRMRef, a: ExprRef, sort: FPSortRef, ctx: Context | None = None -) -> FPRef: +def fpToFPUnsigned(rm: FPRMRef, a: ExprRef, sort: FPSortRef, ctx: Context | None = None) -> FPRef: """Alias for fpUnsignedToFP.""" return fpUnsignedToFP(rm, a, sort, ctx) @@ -3810,9 +3739,7 @@ def FiniteSetMap(f: FuncDeclRef, s: ArrayRef) -> ArrayRef: exists_body = Exists([x], body) lam = Lambda(i, exists_body) result_sort = SetSort(f._range) - return ArrayRef( - lam._ast, result_sort, _merge(s._vars, frozenset([(f._name, f._ast_sort)])) - ) + return ArrayRef(lam._ast, result_sort, _merge(s._vars, frozenset([(f._name, f._ast_sort)]))) def FiniteSetFilter(f: FuncDeclRef, s: ArrayRef) -> ArrayRef: @@ -3824,14 +3751,10 @@ def FiniteSetFilter(f: FuncDeclRef, s: ArrayRef) -> ArrayRef: i = Const("__fsf_i", dom) mem = BoolRef(SelectNode(s._ast, i._ast), _merge(s._vars, i._vars)) pred = f(i) - pred_bool = ( - BoolRef(pred._ast, pred._vars) if not isinstance(pred, BoolRef) else pred - ) + pred_bool = BoolRef(pred._ast, pred._vars) if not isinstance(pred, BoolRef) else pred body = And(mem, pred_bool) lam = Lambda(i, body) - return ArrayRef( - lam._ast, sort, _merge(s._vars, frozenset([(f._name, f._ast_sort)])) - ) + return ArrayRef(lam._ast, sort, _merge(s._vars, frozenset([(f._name, f._ast_sort)]))) def FiniteSetRange(f: Any, lo: Any, hi: Any) -> ArrayRef: @@ -3844,9 +3767,7 @@ def is_finite_set(a: object) -> bool: if not isinstance(a, ExprRef): return False sort = a._sort - return isinstance(sort, ArraySortRef) and isinstance( - sort.range()._ast_sort, PropSort - ) + return isinstance(sort, ArraySortRef) and isinstance(sort.range()._ast_sort, PropSort) def is_finite_set_sort(s: object) -> bool: @@ -3915,9 +3836,7 @@ def CharFromBv(bv: BitVecRef, ctx: Context | None = None) -> CharRef: def CharToBv(ch: ExprRef, ctx: Context | None = None) -> BitVecRef: - return BitVecRef( - CharToNatNode(ch._ast), BitVecSort(21), ch._vars - ) + return BitVecRef(CharToNatNode(ch._ast), BitVecSort(21), ch._vars) def CharToInt(ch: ExprRef, ctx: Context | None = None) -> ArithRef: @@ -3984,7 +3903,7 @@ def __getitem__(self, idx: ArithRef | int) -> ExprRef: _merge(self._vars, idx._vars), ) - def at(self, idx: ArithRef | int) -> SeqRef: + def at(self, idx: ArithRef | int) -> ExprRef: """Return a unit sequence at the given index.""" elem = self[idx] return Unit(elem) @@ -4089,9 +4008,7 @@ def size(self) -> int: return self._size -def FiniteDomainSort( - name: str, sz: int, ctx: Context | None = None -) -> _FiniteDomainSortRef: +def FiniteDomainSort(name: str, sz: int, ctx: Context | None = None) -> _FiniteDomainSortRef: return _FiniteDomainSortRef(name, sz) @@ -4211,11 +4128,7 @@ def is_K(a: object) -> bool: def is_map(a: object) -> bool: - return ( - isinstance(a, ExprRef) - and isinstance(a._ast, LambdaNode) - and isinstance(a, ArrayRef) - ) + return isinstance(a, ExprRef) and isinstance(a._ast, LambdaNode) and isinstance(a, ArrayRef) def is_select(a: object) -> bool: @@ -4268,10 +4181,7 @@ def is_fp_sort(s: object) -> bool: def is_fprm_sort(s: object) -> bool: """True if s is a rounding mode sort.""" if isinstance(s, SortRef): - return ( - isinstance(s._ast_sort, UninterpASTSort) - and s._ast_sort.name == "RoundingMode" - ) + return isinstance(s._ast_sort, UninterpASTSort) and s._ast_sort.name == "RoundingMode" return False @@ -4529,9 +4439,7 @@ def substitute_funs(expr: ExprRef, *args: tuple[FuncDeclRef, ExprRef]) -> ExprRe def deserialize(s: str) -> ExprRef: """Deserialize an expression from string.""" - raise NotImplementedError( - "deserialize is not supported: Lean uses its own expression format" - ) + raise NotImplementedError("deserialize is not supported: Lean uses its own expression format") def to_symbol(s: Any, ctx: Context | None = None) -> str: @@ -4581,23 +4489,17 @@ def __repr__(self) -> str: def __add__(self, other: Any) -> Numeral: return Numeral( - self._expr + other._expr - if isinstance(other, Numeral) - else self._expr + other + self._expr + other._expr if isinstance(other, Numeral) else self._expr + other ) def __sub__(self, other: Any) -> Numeral: return Numeral( - self._expr - other._expr - if isinstance(other, Numeral) - else self._expr - other + self._expr - other._expr if isinstance(other, Numeral) else self._expr - other ) def __mul__(self, other: Any) -> Numeral: return Numeral( - self._expr * other._expr - if isinstance(other, Numeral) - else self._expr * other + self._expr * other._expr if isinstance(other, Numeral) else self._expr * other ) def __lt__(self, other: Any) -> bool: diff --git a/lean_py/z3/smt2.py b/lean_py/z3/smt2.py index e8221be..63ef41c 100644 --- a/lean_py/z3/smt2.py +++ b/lean_py/z3/smt2.py @@ -5,53 +5,51 @@ from __future__ import annotations - from lean_py.z3.core import ( - ExprRef, - SortRef, - FuncDeclRef, - IntSort, - BoolSort, - RealSort, - BitVecSort, + UGE, + UGT, + ULE, + ULT, + And, ArraySort, - DeclareSort, - IntVal, - BoolVal, + BitVecSort, BitVecVal, - StringVal, + BoolSort, + BoolVal, + BV2Int, + Concat, Const, - Function, - And, - Or, - Not, - Implies, - Xor, - If, + DeclareSort, Distinct, - ForAll, Exists, - Select, - Store, - Concat, + ExprRef, Extract, - ZeroExt, - SignExt, + ForAll, + FuncDeclRef, + Function, + If, + Implies, + Int2BV, + IntSort, + IntVal, LShR, + Not, + Or, + RealSort, + RepeatBitVec, RotateLeft, RotateRight, - RepeatBitVec, - ToReal, + Select, + SignExt, + SortRef, + Store, + StringVal, ToInt, - Int2BV, - BV2Int, - ULT, - ULE, - UGT, - UGE, + ToReal, + Xor, + ZeroExt, ) - # --------------------------------------------------------------------------- # S-expression tokenizer / parser # --------------------------------------------------------------------------- @@ -187,9 +185,7 @@ def resolve_sort(self, sexpr: SExpr) -> SortRef: return self.sorts[head] raise ValueError(f"Unknown sort: {sexpr}") - def resolve_expr( - self, sexpr: SExpr, let_env: dict[str, ExprRef] | None = None - ) -> ExprRef: + def resolve_expr(self, sexpr: SExpr, let_env: dict[str, ExprRef] | None = None) -> ExprRef: """Convert an S-expression to an ExprRef.""" if let_env is None: let_env = {} @@ -278,11 +274,7 @@ def resolve_expr( # (_ op ...) at top level of application if head == "_": # This is an indexed identifier used standalone, e.g. (_ bv0 32) - if ( - len(sexpr) >= 3 - and isinstance(sexpr[1], str) - and sexpr[1].startswith("bv") - ): + if len(sexpr) >= 3 and isinstance(sexpr[1], str) and sexpr[1].startswith("bv"): # (_ bvN width) val = int(sexpr[1][2:]) width = int(sexpr[2]) @@ -585,6 +577,6 @@ def parse_smt2_file( This function is similar to :func:`parse_smt2_string`. """ - with open(filename, "r") as f: + with open(filename) as f: content = f.read() return parse_smt2_string(content, sorts=sorts, decls=decls) diff --git a/lean_py/z3/solver.py b/lean_py/z3/solver.py index f6b23d0..c1b180c 100644 --- a/lean_py/z3/solver.py +++ b/lean_py/z3/solver.py @@ -23,22 +23,33 @@ from lean_py.kernel import Kernel from lean_py.project import ManagedProject from lean_py.z3._ast import ( - ASTNode, - ASTSort, AppNode, ArrowASTSort, - BitvecASTSort, + ASTNode, + ASTSort, BinOpNode, + BitvecASTSort, BoolLit, BvLit, + CharASTSort, + CharFromBvNode, + CharIsDigitNode, + CharLit, + CharToNatNode, ConstArrayNode, DistinctNode, ExistsNode, ExtractNode, + FinDomainASTSort, + FinDomainLit, ForAllNode, FpASTSort, FpLitNode, FpOpNode, + InductiveAccessorNode, + InductiveASTSort, + InductiveCtorNode, + InductiveRecognizerNode, InReNode, Int2BvNode, IntASTSort, @@ -50,8 +61,8 @@ NatLit, PropSort, RealASTSort, - ReConcatNode, ReComplementNode, + ReConcatNode, ReIntersectNode, ReLoopNode, ReOptionNode, @@ -60,46 +71,35 @@ ReStarNode, ReUnionNode, SelectNode, + SeqASTSort, + SeqConcatNode, + SeqContainsNode, + SeqEmptyNode, + SeqLenNode, + SeqNthNode, + SeqPrefixOfNode, + SeqSuffixOfNode, + SeqUnitNode, SignExtNode, StoreNode, StrConcatNode, StrContainsNode, StrIndexOfNode, + StringASTSort, + StringLit, StrLenNode, StrPrefixOfNode, StrReplaceNode, StrSubstrNode, StrSuffixOfNode, StrToIntNode, - StringASTSort, - StringLit, ToIntNode, ToRealNode, - UnOpNode, TypeASTSort, UninterpASTSort, + UnOpNode, Var, ZeroExtNode, - FinDomainASTSort, - FinDomainLit, - InductiveASTSort, - InductiveCtorNode, - InductiveAccessorNode, - InductiveRecognizerNode, - CharASTSort, - CharLit, - CharToNatNode, - CharFromBvNode, - CharIsDigitNode, - SeqASTSort, - SeqEmptyNode, - SeqUnitNode, - SeqLenNode, - SeqConcatNode, - SeqContainsNode, - SeqPrefixOfNode, - SeqSuffixOfNode, - SeqNthNode, ) from lean_py.z3.core import ( And, @@ -136,9 +136,7 @@ def __hash__(self) -> int: return hash(self._name) def __bool__(self) -> bool: - raise TypeError( - "CheckSatResult cannot be used as bool; compare to sat/unsat/unknown" - ) + raise TypeError("CheckSatResult cannot be used as bool; compare to sat/unsat/unknown") sat = CheckSatResult("sat") @@ -662,9 +660,7 @@ def __iter__(self): @staticmethod def from_file(filename: str) -> Solver: """Load solver from file (not supported).""" - raise NotImplementedError( - "from_file not supported: Lean uses its own syntax, not SMT-LIB2" - ) + raise NotImplementedError("from_file not supported: Lean uses its own syntax, not SMT-LIB2") @staticmethod def from_string(s: str) -> Solver: @@ -781,9 +777,7 @@ def solve_using(s: Solver, *args: BoolRef) -> CheckSatResult: return s.check() -def parse_smt2_string( - s: str, sorts: dict | None = None, decls: dict | None = None -) -> list: +def parse_smt2_string(s: str, sorts: dict | None = None, decls: dict | None = None) -> list: """Parse a string in SMT-LIB2 format using the given sorts and decls. Returns a list of assertions (z3py ``ExprRef`` objects). @@ -791,9 +785,7 @@ def parse_smt2_string( return _parse_smt2_string_impl(s, sorts=sorts, decls=decls) -def parse_smt2_file( - filename: str, sorts: dict | None = None, decls: dict | None = None -) -> list: +def parse_smt2_file(filename: str, sorts: dict | None = None, decls: dict | None = None) -> list: """Parse an SMT-LIB2 file using the given sorts and decls. Returns a list of assertions (z3py ``ExprRef`` objects). @@ -905,9 +897,7 @@ def _abstract(self, expr: BoolRef) -> BoolRef: """Wrap *expr* in ForAll over declared vars that appear in it.""" var_names = {name for name, _ in expr._vars} used = [ - v - for v in self._declared_vars - if isinstance(v._ast, Var) and v._ast.name in var_names + v for v in self._declared_vars if isinstance(v._ast, Var) and v._ast.name in var_names ] if used: return ForAll(used, expr) @@ -951,9 +941,7 @@ def query(self, *query: Any) -> CheckSatResult: # Build: (premise₁ ∧ … ∧ premiseₙ) → query goal: BoolRef if self._premises: - conj = ( - And(*self._premises) if len(self._premises) > 1 else self._premises[0] - ) + conj = And(*self._premises) if len(self._premises) > 1 else self._premises[0] goal = Implies(conj, q) else: goal = q @@ -1097,16 +1085,12 @@ def is_as_array(a: Any) -> bool: def get_as_array_func(a: Any) -> Any: """Get FuncDeclRef from as-array expression.""" - raise NotImplementedError( - "get_as_array_func not supported: Lean cannot produce counter-models" - ) + raise NotImplementedError("get_as_array_func not supported: Lean cannot produce counter-models") def get_map_func(a: Any) -> Any: """Get FuncDeclRef from mapped array expression.""" - raise NotImplementedError( - "get_map_func not supported: Lean cannot produce counter-models" - ) + raise NotImplementedError("get_map_func not supported: Lean cannot produce counter-models") # --------------------------------------------------------------------------- @@ -1123,19 +1107,13 @@ def __init__(self, opt: Any, is_max: bool, idx: int) -> None: self._idx = idx def lower(self) -> Any: - raise NotImplementedError( - "OptimizeObjective.lower not supported: Lean is a proof checker" - ) + raise NotImplementedError("OptimizeObjective.lower not supported: Lean is a proof checker") def upper(self) -> Any: - raise NotImplementedError( - "OptimizeObjective.upper not supported: Lean is a proof checker" - ) + raise NotImplementedError("OptimizeObjective.upper not supported: Lean is a proof checker") def value(self) -> Any: - raise NotImplementedError( - "OptimizeObjective.value not supported: Lean is a proof checker" - ) + raise NotImplementedError("OptimizeObjective.value not supported: Lean is a proof checker") def __repr__(self) -> str: kind = "maximize" if self._is_max else "minimize" diff --git a/lean_py/z3/tactic.py b/lean_py/z3/tactic.py index 28b6ae3..001c220 100644 --- a/lean_py/z3/tactic.py +++ b/lean_py/z3/tactic.py @@ -8,7 +8,6 @@ from lean_py.z3.core import And, BoolRef, BoolVal, Or from lean_py.z3.solver import Solver, _get_kernel, _marshal_expr, _wrap_free_vars - # --------------------------------------------------------------------------- # Goal # --------------------------------------------------------------------------- diff --git a/pyproject.toml b/pyproject.toml index 331e433..588f361 100644 --- a/pyproject.toml +++ b/pyproject.toml @@ -31,7 +31,7 @@ Issues = "https://github.com/BasisResearch/lean.py/issues" Documentation = "https://BasisResearch.github.io/lean.py" [dependency-groups] -dev = ["pytest>=8.0"] +dev = ["pytest>=8.0", "ruff>=0.8", "mypy>=1.13"] [build-system] requires = ["hatchling"] @@ -39,3 +39,17 @@ build-backend = "hatchling.build" [tool.pytest.ini_options] testpaths = ["tests"] + +[tool.ruff] +target-version = "py312" +line-length = 100 +extend-exclude = ["examples"] + +[tool.ruff.lint] +select = ["E", "F", "I", "W", "UP"] + +[tool.mypy] +python_version = "3.12" +warn_unused_configs = true +disallow_untyped_defs = false +ignore_missing_imports = true diff --git a/tests/conftest.py b/tests/conftest.py index f275c5a..27d10c0 100644 --- a/tests/conftest.py +++ b/tests/conftest.py @@ -23,7 +23,9 @@ def example_lib() -> LeanLibrary: add_lean_lib_to_dyld_path() return LeanLibrary.from_lake( - Path(__file__).parent / "lean", "TestLib", build=True, + Path(__file__).parent / "lean", + "TestLib", + build=True, ) @@ -34,6 +36,7 @@ def pytest_collection_modifyitems(config, items): finalisation interacts poorly with later tests. Reordering keeps the rest of the suite green. """ + def is_kernel_full(item): return "test_kernel_full" in item.nodeid diff --git a/tests/test_callable.py b/tests/test_callable.py index 76e105f..c7d9888 100644 --- a/tests/test_callable.py +++ b/tests/test_callable.py @@ -9,8 +9,6 @@ import pytest -from lean_py.exceptions import LeanError, LeanPyCallbackError - def test_callable_basic_sum(example_lib): """A Lean closure that sums its arguments behaves as a Python callable.""" diff --git a/tests/test_exceptions.py b/tests/test_exceptions.py index 828c53d..17e5518 100644 --- a/tests/test_exceptions.py +++ b/tests/test_exceptions.py @@ -143,8 +143,9 @@ def test_python_callback_error_python_message_attr(example_lib): example_lib.propagatePythonError("undefined_x") e = ei.value assert "undefined_x" in e.python_message - assert not e.python_message.startswith("NameError:"), \ + assert not e.python_message.startswith("NameError:"), ( "python_message should be the unprefixed payload" + ) def test_lean_error_no_python_attrs(example_lib): diff --git a/tests/test_ffi.py b/tests/test_ffi.py index 6c41ff3..38cffa0 100644 --- a/tests/test_ffi.py +++ b/tests/test_ffi.py @@ -1,19 +1,21 @@ import ctypes -from lean_py.base_types import LeanStringObject + from lean_py.lean_ffi import LeanFFI, get_lean_ffi from lean_py.lean_types import LeanString + def test_ffi_can_be_created(): ffi = get_lean_ffi() assert isinstance(ffi, LeanFFI) + def test_ffi_has_initialised(): ffi = get_lean_ffi() isinstance(ffi.lean_initialize, ctypes._CFuncPtr) + def test_lean_string_wrap(): ffi = get_lean_ffi() kiran_str = ffi.mk_string("kiran") obj = LeanString(kiran_str) assert str(obj) == "kiran" - diff --git a/tests/test_introspection.py b/tests/test_introspection.py index f0eec61..587c118 100644 --- a/tests/test_introspection.py +++ b/tests/test_introspection.py @@ -11,8 +11,6 @@ from __future__ import annotations -import pytest - def test_name_returned_from_lean(example_lib): """`makeName` returns a Lean.Name that Python decodes to a structured @@ -63,8 +61,8 @@ def test_expr_built_in_python(example_lib): nat_lit_name = Name.str(Name.anonymous, "Nat") succ_name = Name.str(nat_lit_name, "succ") zero_name = Name.str(nat_lit_name, "zero") - f = Expr.const(succ_name, []) # Expr.const "Nat.succ" [] - x = Expr.const(zero_name, []) # Expr.const "Nat.zero" [] + f = Expr.const(succ_name, []) # Expr.const "Nat.succ" [] + x = Expr.const(zero_name, []) # Expr.const "Nat.zero" [] e = Expr.app(f, x) s = example_lib.py_expr_describe(e) assert s == "app (const Nat.succ) (const Nat.zero)" @@ -82,9 +80,18 @@ def test_expr_lit_described(example_lib): def test_kernel_types_registered(example_lib): """Smoke test: every kernel ADT we promised to expose is present on the library.""" - for name in ("Name", "Level", "Expr", "Syntax", "Literal", - "BinderInfo", "MVarId", "FVarId", "LevelMVarId", - "SourceInfo"): + for name in ( + "Name", + "Level", + "Expr", + "Syntax", + "Literal", + "BinderInfo", + "MVarId", + "FVarId", + "LevelMVarId", + "SourceInfo", + ): assert hasattr(example_lib, name), f"missing {name}" # Constructors assert example_lib.Name.anonymous.ctor == "anonymous" diff --git a/tests/test_kernel.py b/tests/test_kernel.py index 4c2f68c..0986a68 100644 --- a/tests/test_kernel.py +++ b/tests/test_kernel.py @@ -54,7 +54,7 @@ def test_infer_type(kernel): t = kernel.leanpy_kernel_infer_type("true") assert "Bool" in t - t = kernel.leanpy_kernel_infer_type("\"hello\"") + t = kernel.leanpy_kernel_infer_type('"hello"') assert "String" in t diff --git a/tests/test_kernel_full.py b/tests/test_kernel_full.py index f704304..23e4b2d 100644 --- a/tests/test_kernel_full.py +++ b/tests/test_kernel_full.py @@ -9,9 +9,9 @@ import pytest - # --- shared fixture --------------------------------------------------------- + @pytest.fixture(scope="module") def kernel(example_lib): """Initialize the kernel and load the `Init` env.""" @@ -22,6 +22,7 @@ def kernel(example_lib): # --- environment introspection ---------------------------------------------- + def test_env_loaded(kernel): assert kernel.leanpy_kernel_is_loaded(None) is True @@ -74,6 +75,7 @@ def test_env_is_internal(kernel): # --- elaboration ----------------------------------------------------------- + def test_infer_type_basic(kernel): assert "Nat" in kernel.leanpy_kernel_infer_type("Nat.succ Nat.zero") assert "Bool" in kernel.leanpy_kernel_infer_type("true") @@ -114,6 +116,7 @@ def test_decide_false(kernel): # --- goal state ------------------------------------------------------------ + def test_goal_create(kernel): """We can create a goal state and read off its solved/unsolved flag.""" state = kernel.leanpy_kernel_goal_create("∀ n : Nat, n + 0 = n") @@ -125,6 +128,7 @@ def test_goal_create(kernel): def test_goal_create_invalid(kernel): """Invalid types raise `LeanError`.""" from lean_py import LeanError + with pytest.raises(LeanError): kernel.leanpy_kernel_goal_create("@@@@") diff --git a/tests/test_marshal.py b/tests/test_marshal.py index 8a63218..720197d 100644 --- a/tests/test_marshal.py +++ b/tests/test_marshal.py @@ -1,7 +1,5 @@ """End-to-end tests for the Lean→Python marshalling pipeline.""" -import pytest - from lean_py import LeanInductiveValue diff --git a/tests/test_memory.py b/tests/test_memory.py index 09f59c3..103f621 100644 --- a/tests/test_memory.py +++ b/tests/test_memory.py @@ -87,6 +87,7 @@ def test_leanobj_handle_dropping(example_lib): """Pure Python LeanObj wrappers should release their refs on GC.""" from lean_py import LeanObj from lean_py.lean_ffi import get_lean_ffi + ffi = get_lean_ffi() # Allocate / drop in a loop and ensure no exceptions. @@ -219,9 +220,10 @@ def test_error_propagation_no_type_name_leak(example_lib): total_growth = sum(s.size_diff for s in stats if s.size_diff > 0) # With the bug, each call leaks a ~60-byte "NameError" string → - # ~120 KB growth for 2000 calls. Without it, growth is negligible. - # Use a generous threshold to avoid flakiness. - assert total_growth < 50_000, ( + # ~120 KB growth for 2000 calls. Without it, growth should stay + # under ~60 KB (Python interpreter noise). Use 80 KB threshold + # to avoid CI flakiness while still catching the ~125 KB leak. + assert total_growth < 80_000, ( f"Memory grew by {total_growth} bytes after {N} error propagations " - f"(threshold 50 KB) — likely a leak in raise_py_error" + f"(threshold 80 KB) — likely a leak in raise_py_error" ) diff --git a/tests/test_pattern_match.py b/tests/test_pattern_match.py index 43db18b..288f412 100644 --- a/tests/test_pattern_match.py +++ b/tests/test_pattern_match.py @@ -5,7 +5,6 @@ from lean_py import LeanInductiveValue from lean_py.marshal import _CtorMeta - # ============================================================================ # isinstance checks # ============================================================================ @@ -93,18 +92,26 @@ class _NameNs: pass NameNs = _NameNs() - NameNs.str = _CtorMeta("str", (), { - '_ctor_name': 'str', - '_type_name': 'Name', - '_tag': 1, - '__match_args__': ('_0', '_1'), - }) - NameNs.anonymous = _CtorMeta("anonymous", (), { - '_ctor_name': 'anonymous', - '_type_name': 'Name', - '_tag': 0, - '__match_args__': (), - }) + NameNs.str = _CtorMeta( + "str", + (), + { + "_ctor_name": "str", + "_type_name": "Name", + "_tag": 1, + "__match_args__": ("_0", "_1"), + }, + ) + NameNs.anonymous = _CtorMeta( + "anonymous", + (), + { + "_ctor_name": "anonymous", + "_type_name": "Name", + "_tag": 0, + "__match_args__": (), + }, + ) match name: case NameNs.str(parent, leaf): diff --git a/tests/test_python_in_lean.py b/tests/test_python_in_lean.py index 1b8d5df..98d46db 100644 --- a/tests/test_python_in_lean.py +++ b/tests/test_python_in_lean.py @@ -5,9 +5,6 @@ (via `LeanPy.Python.init`), so we exercise the whole loader path. """ -import math -import sys - import pytest diff --git a/tests/test_sympy_demo.py b/tests/test_sympy_demo.py index cda70c4..03c7e66 100644 --- a/tests/test_sympy_demo.py +++ b/tests/test_sympy_demo.py @@ -16,8 +16,7 @@ def _have(mod: str) -> bool: @pytest.mark.skipif(not _have("sympy"), reason="sympy not installed") def test_sympy_factorial(example_lib): # sympy.factorial returns a sympy.Integer; str(.) yields the decimal form. - assert example_lib.pythonEvalStr("__import__('sympy').factorial(20)") == \ - "2432902008176640000" + assert example_lib.pythonEvalStr("__import__('sympy').factorial(20)") == "2432902008176640000" @pytest.mark.skipif(not _have("sympy"), reason="sympy not installed") diff --git a/tests/test_transport_unification.py b/tests/test_transport_unification.py index a926877..b72c3e8 100644 --- a/tests/test_transport_unification.py +++ b/tests/test_transport_unification.py @@ -4,6 +4,7 @@ ``LeanObjHandle`` type allow Lean objects (``Expr``, ``Name``, etc.) to pass through the ``Py`` bridge and back. """ + from __future__ import annotations import gc @@ -12,7 +13,6 @@ from lean_py.marshal import LeanObj - # --------------------------------------------------------------------------- # Fixtures # --------------------------------------------------------------------------- diff --git a/tests/test_z3_compat.py b/tests/test_z3_compat.py index 8a1994b..fdd9947 100644 --- a/tests/test_z3_compat.py +++ b/tests/test_z3_compat.py @@ -10,57 +10,79 @@ from lean_py.kernel import Kernel from lean_py.z3 import ( + RNE, + UGE, + UGT, + ULE, + ULT, Abs, AllChar, And, + ApplyResult, Array, + ArrayRef, ArraySort, - AShr, AsArray, - BV2Int, + AShr, BitVec, BitVecRef, + BitVecs, BitVecSort, BitVecVal, - BitVecs, Bool, BoolSort, BoolVal, + BV2Int, + BVAddNoOverflow, + BVMulNoOverflow, + CharIsDigit, + CharRef, + CharSort, + CharSortRef, + CharToBv, + CharToInt, + CharVal, Complement, Concat, Const, - Consts, Contains, Datatype, DeclareSort, Distinct, + Empty, + EmptySet, Exists, ExprRef, Extract, + Float64, ForAll, + FPNumRef, + FPVal, FreshBool, FreshConst, FreshInt, FreshReal, + FullSet, Function, Goal, - ApplyResult, If, Implies, - InRe, IndexOf, - Intersect, + InRe, Int, Int2BV, + Intersect, + Ints, IntSort, IntToStr, IntVal, - Ints, + IsMember, + IsSubset, K, - LShR, Lambda, Length, Loop, + LShR, Map, ModelRef, Nat, @@ -69,6 +91,7 @@ Not, Option, Or, + OrElse, Plus, PrefixOf, Product, @@ -78,42 +101,56 @@ Re, Real, RealSort, + Repeat, Replace, RotateLeft, RotateRight, SDiv, - SRem, Select, + SeqRef, + SeqSort, + SeqSortRef, + SetAdd, + SetComplement, + SetDifference, + SetIntersect, + SetSort, + SetUnion, SignExt, Solver, + SRem, Star, Store, StrConcat, - StrToInt, String, StringRef, + Strings, StringSort, StringSortRef, StringVal, - Strings, + StrToInt, SubString, SuffixOf, Sum, Tactic, Then, - OrElse, - Repeat, ToInt, ToReal, UDiv, - UGE, - UGT, - ULE, - ULT, - URem, Union, + Unit, + URem, Xor, ZeroExt, + fpAdd, + fpEQ, + fpIsNegative, + fpIsPositive, + fpLT, + fpMul, + fpNaN, + fpNeg, + fpPlusInfinity, is_add, is_and, is_array, @@ -142,49 +179,6 @@ simplify, unknown, unsat, - Float64, - FPVal, - FPNumRef, - FPRef, - fpAdd, - fpMul, - fpNeg, - fpLT, - fpEQ, - fpNaN, - fpPlusInfinity, - RNE, - RealVal, - Reals, - BVAddNoOverflow, - BVMulNoOverflow, - fpIsPositive, - fpIsNegative, - CharSort, - CharSortRef, - CharVal, - CharRef, - CharFromBv, - CharToBv, - CharToInt, - CharIsDigit, - SeqSort, - SeqSortRef, - SeqRef, - Empty, - Unit, - SetSort, - EmptySet, - FullSet, - SetAdd, - SetDel, - IsMember, - SetUnion, - SetIntersect, - SetComplement, - SetDifference, - IsSubset, - ArrayRef, ) from lean_py.z3._ast import ( BinOp, @@ -197,29 +191,26 @@ ExtractNode, ForAllNode, FpLitNode, + InductiveCtorNode, InReNode, - IntASTSort, IntLit, IteNode, LambdaNode, NatLit, - PropSort, ReStarNode, SelectNode, SignExtNode, StoreNode, StrConcatNode, StrContainsNode, - StrLenNode, - StringASTSort, StringLit, - ToRealNode, + StrLenNode, ToIntNode, + ToRealNode, UnOp, UnOpNode, Var, ZeroExtNode, - InductiveCtorNode, ) from lean_py.z3.solver import _try_prove @@ -229,10 +220,15 @@ def kernel(example_lib) -> Kernel: k = Kernel(example_lib) import subprocess from pathlib import Path - sp = subprocess.check_output( - ["lake", "env", "printenv", "LEAN_PATH"], - cwd=str(Path(__file__).parent / "lean"), - ).decode().strip() + + sp = ( + subprocess.check_output( + ["lake", "env", "printenv", "LEAN_PATH"], + cwd=str(Path(__file__).parent / "lean"), + ) + .decode() + .strip() + ) k.init_search(sp) k.load(["Init", "LeanPy.Z3"]) set_kernel(k) @@ -663,21 +659,36 @@ def test_constructor_application(self, kernel): p = Pair.mk(x, y) assert isinstance(p._ast, InductiveCtorNode) + def test_uninterpreted_sort_field(self, kernel): + """Datatype with a DeclareSort field should not fail (issue #9).""" + HeapRef = DeclareSort("HeapRef") + dt = Datatype("optional_HeapRef_") + dt.declare("missing") + dt.declare("present", ("valueat", HeapRef)) + result = dt.create() + assert hasattr(result, "missing") + assert hasattr(result, "present") + assert hasattr(result, "valueat") + class TestDatatypeStructural: """Test that inductive datatypes enable structural proofs.""" def test_enum_disjointness(self, kernel): - Color = Datatype('Color_s1') - Color.declare('red'); Color.declare('green'); Color.declare('blue') + Color = Datatype("Color_s1") + Color.declare("red") + Color.declare("green") + Color.declare("blue") Color = Color.create() assert _try_prove(Color.red != Color.green) def test_enum_exhaustiveness(self, kernel): - Color = Datatype('Color_s2') - Color.declare('red'); Color.declare('green'); Color.declare('blue') + Color = Datatype("Color_s2") + Color.declare("red") + Color.declare("green") + Color.declare("blue") Color = Color.create() - x = Const('x', Color) + x = Const("x", Color) g = Goal() g.add(Or(x == Color.red, x == Color.green, x == Color.blue)) t = Tactic("intro x; cases x <;> simp") @@ -685,34 +696,51 @@ def test_enum_exhaustiveness(self, kernel): assert len(r) == 0 def test_constructor_injectivity(self, kernel): - Pair = Datatype('IntPair_s3') - Pair.declare('mk_pair', ('fst', IntSort()), ('snd', IntSort())) + Pair = Datatype("IntPair_s3") + Pair.declare("mk_pair", ("fst", IntSort()), ("snd", IntSort())) Pair = Pair.create() - x, y = Ints('x y') - assert _try_prove(Implies(Pair.mk_pair(x, y) == Pair.mk_pair(IntVal(1), IntVal(2)), And(x == IntVal(1), y == IntVal(2)))) + x, y = Ints("x y") + assert _try_prove( + Implies( + Pair.mk_pair(x, y) == Pair.mk_pair(IntVal(1), IntVal(2)), + And(x == IntVal(1), y == IntVal(2)), + ) + ) def test_accessor_projection(self, kernel): - Pair = Datatype('IntPair_s4') - Pair.declare('mk', ('fst', IntSort()), ('snd', IntSort())) + Pair = Datatype("IntPair_s4") + Pair.declare("mk", ("fst", IntSort()), ("snd", IntSort())) Pair = Pair.create() assert _try_prove(Pair.fst(Pair.mk(IntVal(1), IntVal(2))) == IntVal(1)) def test_recursive_datatype(self, kernel): - Tree = Datatype('Tree_s5') - Tree.declare('leaf', ('val', IntSort())) - Tree.declare('node', ('left', Tree), ('right', Tree)) + Tree = Datatype("Tree_s5") + Tree.declare("leaf", ("val", IntSort())) + Tree.declare("node", ("left", Tree), ("right", Tree)) Tree = Tree.create() t1 = Tree.leaf(IntVal(1)) t2 = Tree.node(Tree.leaf(IntVal(1)), Tree.leaf(IntVal(2))) assert _try_prove(t1 != t2) def test_recognizer(self, kernel): - Color = Datatype('Color_s6') - Color.declare('red'); Color.declare('green'); Color.declare('blue') + Color = Datatype("Color_s6") + Color.declare("red") + Color.declare("green") + Color.declare("blue") Color = Color.create() assert _try_prove(Color.is_red(Color.red)) assert _try_prove(Not(Color.is_red(Color.green))) + def test_uninterp_sort_field_disjointness(self, kernel): + """Constructors of a datatype with DeclareSort fields are distinct (issue #9).""" + Ref = DeclareSort("Ref_s7") + Opt = Datatype("OptRef_s7") + Opt.declare("none_") + Opt.declare("some_", ("val", Ref)) + Opt = Opt.create() + x = Const("x", Ref) + assert _try_prove(Opt.none_ != Opt.some_(x)) + # ------------------------------------------------------------------ # Bug fixes @@ -723,7 +751,7 @@ class TestBugFixes: def test_pow_not_mul(self): """__pow__ should use POW, not MUL.""" x = Int("x") - p = x ** 2 + p = x**2 assert isinstance(p._ast, BinOpNode) and p._ast.op == BinOp.POW def test_bool_guard(self): @@ -764,7 +792,7 @@ def test_arith_rmod(self): def test_arith_rpow(self): x = Int("x") - r = 2 ** x + r = 2**x assert isinstance(r._ast, BinOpNode) and r._ast.op == BinOp.POW def test_arith_pos(self): @@ -1301,13 +1329,14 @@ def test_goal_as_expr(self): def test_apply_result_empty_proved(self): r = ApplyResult([]) assert len(r) == 0 - from lean_py.z3.core import BoolLit as BoolLitCls + assert r.as_expr()._ast == BoolLit(True) def test_tactic_solve_trivial(self, kernel): """Tactic('decide') can solve True.""" g = Goal() from lean_py.z3 import BoolVal + g.add(BoolVal(True)) t = Tactic("decide") result = t.apply(g) @@ -1359,9 +1388,9 @@ def test_string_concat(self): def test_length(self): s = String("s") - l = Length(s) - assert is_int(l) - assert isinstance(l._ast, StrLenNode) + length = Length(s) + assert is_int(length) + assert isinstance(length._ast, StrLenNode) def test_contains(self): s = String("s") @@ -1565,6 +1594,7 @@ def test_map_sort(self): a = Array("a", IntSort(), IntSort()) result = Map(f, a) from lean_py.z3 import ArraySortRef + assert isinstance(result._sort, ArraySortRef) @@ -1722,6 +1752,7 @@ class TestCoercionEdgeCases: def test_bv_negative_coercion(self): """BitVec + (-1) should produce two's complement.""" from lean_py.z3._ast import BvLit + bv = BitVec("x", 8) result = bv + (-1) # The -1 coerced to BvLit should be 255 (two's complement for 8-bit) @@ -1733,6 +1764,7 @@ def test_bv_negative_coercion(self): def test_bv_negative_coercion_16bit(self): """BitVec + (-1) on 16-bit should be 65535.""" from lean_py.z3._ast import BvLit + bv = BitVec("x", 16) result = bv + (-1) rhs = result._ast.rhs @@ -1745,6 +1777,7 @@ def test_real_float_coercion(self): result = x + 3.14 # The AST should NOT have IntLit(3) — it should be a rational from lean_py.z3._ast import BinOpNode, IntLit + assert isinstance(result._ast, BinOpNode) rhs = result._ast.rhs # rhs should NOT be IntLit(3) @@ -1754,7 +1787,8 @@ def test_real_float_half(self): """Real + 0.5 should be representable as 1/2.""" x = Real("x") result = x + 0.5 - from lean_py.z3._ast import BinOpNode, ToRealNode + from lean_py.z3._ast import BinOpNode + assert isinstance(result._ast, BinOpNode) rhs = result._ast.rhs # Should be a division of ToReal nodes (rational representation) @@ -1814,8 +1848,8 @@ def test_int_to_real_ground(self, kernel): # ------------------------------------------------------------------ -class TestBugFixes: - """Tests for specific bug fixes.""" +class TestBugFixesCoercion: + """Tests for specific bug fixes (coercion, overflow, FP).""" def test_inttostr_negative(self, kernel): """IntToStr(-5) should return empty string per SMT-LIB spec.""" @@ -1824,7 +1858,6 @@ def test_inttostr_negative(self, kernel): def test_bv_add_no_overflow_unsigned(self, kernel): """BVAddNoOverflow unsigned: 200 + 100 overflows 8-bit.""" - from lean_py.z3 import BVAddNoOverflow a = BitVecVal(200, 8) b = BitVecVal(100, 8) @@ -1834,7 +1867,6 @@ def test_bv_add_no_overflow_unsigned(self, kernel): def test_bv_mul_no_overflow_unsigned(self, kernel): """BVMulNoOverflow unsigned: 200 * 2 overflows 8-bit.""" - from lean_py.z3 import BVMulNoOverflow a = BitVecVal(200, 8) b = BitVecVal(2, 8) @@ -1844,14 +1876,12 @@ def test_bv_mul_no_overflow_unsigned(self, kernel): def test_fp_is_positive_zero(self, kernel): """fpIsPositive(+0.0) should be True.""" - from lean_py.z3 import fpIsPositive claim = fpIsPositive(FPVal(0.0, Float64())) assert _try_prove(claim) def test_fp_is_negative_neg_zero(self, kernel): """fpIsNegative(-0.0) should be True.""" - from lean_py.z3 import fpIsNegative claim = fpIsNegative(FPVal(-0.0, Float64())) assert _try_prove(claim) @@ -1867,28 +1897,24 @@ class TestChar: def test_char_sort_creation(self): """CharSort() creates the char sort.""" - from lean_py.z3 import CharSort, CharSortRef s = CharSort() assert isinstance(s, CharSortRef) def test_char_val_from_str(self): """CharVal creates a char literal from string.""" - from lean_py.z3 import CharVal, CharRef c = CharVal("A") assert isinstance(c, CharRef) def test_char_val_from_int(self): """CharVal creates a char literal from int.""" - from lean_py.z3 import CharVal, CharRef c = CharVal(65) assert isinstance(c, CharRef) def test_char_to_int(self): """CharToInt returns ArithRef.""" - from lean_py.z3 import CharVal, CharToInt from lean_py.z3.core import ArithRef @@ -1898,7 +1924,6 @@ def test_char_to_int(self): def test_char_to_bv(self): """CharToBv returns BitVecRef.""" - from lean_py.z3 import CharVal, CharToBv c = CharVal("A") bv = CharToBv(c) @@ -1906,7 +1931,6 @@ def test_char_to_bv(self): def test_char_is_digit(self): """CharIsDigit returns BoolRef.""" - from lean_py.z3 import CharVal, CharIsDigit from lean_py.z3.core import BoolRef c = CharVal("5") @@ -1915,14 +1939,12 @@ def test_char_is_digit(self): def test_char_to_int_semantic(self, kernel): """CharToInt(CharVal('A')) == 65.""" - from lean_py.z3 import CharVal, CharToInt claim = CharToInt(CharVal("A")) == IntVal(65) assert _try_prove(claim) def test_char_const(self): """Const with CharSort creates CharRef.""" - from lean_py.z3 import CharSort, CharRef c = Const("c", CharSort()) assert isinstance(c, CharRef) @@ -1938,35 +1960,32 @@ class TestSets: def test_set_sort_creation(self): """SetSort creates ArraySortRef.""" - from lean_py.z3 import SetSort, ArraySortRef + from lean_py.z3 import ArraySortRef s = SetSort(IntSort()) assert isinstance(s, ArraySortRef) def test_empty_set(self): """EmptySet creates an array expression.""" - from lean_py.z3 import EmptySet, ArrayRef s = EmptySet(IntSort()) assert isinstance(s, ArrayRef) def test_full_set(self): """FullSet creates an array expression.""" - from lean_py.z3 import FullSet, ArrayRef s = FullSet(IntSort()) assert isinstance(s, ArrayRef) def test_set_add(self): """SetAdd adds element to set.""" - from lean_py.z3 import SetAdd, EmptySet, ArrayRef s = SetAdd(EmptySet(IntSort()), IntVal(1)) assert isinstance(s, ArrayRef) def test_is_member(self): """IsMember tests membership.""" - from lean_py.z3 import IsMember, SetAdd, EmptySet, BoolRef + from lean_py.z3 import BoolRef s = SetAdd(EmptySet(IntSort()), IntVal(1)) m = IsMember(IntVal(1), s) @@ -1974,14 +1993,12 @@ def test_is_member(self): def test_is_member_semantic(self, kernel): """IsMember(1, SetAdd(EmptySet, 1)) is provable.""" - from lean_py.z3 import IsMember, SetAdd, EmptySet claim = IsMember(IntVal(1), SetAdd(EmptySet(IntSort()), IntVal(1))) assert _try_prove(claim) def test_set_union(self): """SetUnion creates an array expression.""" - from lean_py.z3 import SetUnion, EmptySet, SetAdd, ArrayRef a = SetAdd(EmptySet(IntSort()), IntVal(1)) b = SetAdd(EmptySet(IntSort()), IntVal(2)) @@ -1990,7 +2007,6 @@ def test_set_union(self): def test_set_intersect(self): """SetIntersect creates an array expression.""" - from lean_py.z3 import SetIntersect, EmptySet, SetAdd a = SetAdd(EmptySet(IntSort()), IntVal(1)) b = SetAdd(EmptySet(IntSort()), IntVal(1)) @@ -1999,14 +2015,12 @@ def test_set_intersect(self): def test_set_complement(self): """SetComplement creates an array expression.""" - from lean_py.z3 import SetComplement, EmptySet s = SetComplement(EmptySet(IntSort())) assert isinstance(s, ExprRef) def test_set_difference(self): """SetDifference creates an array expression.""" - from lean_py.z3 import SetDifference, EmptySet, SetAdd a = SetAdd(EmptySet(IntSort()), IntVal(1)) b = EmptySet(IntSort()) @@ -2015,7 +2029,7 @@ def test_set_difference(self): def test_is_subset(self): """IsSubset creates a BoolRef.""" - from lean_py.z3 import IsSubset, EmptySet, SetAdd, BoolRef + from lean_py.z3 import BoolRef a = EmptySet(IntSort()) b = SetAdd(EmptySet(IntSort()), IntVal(1)) @@ -2033,21 +2047,18 @@ class TestSequences: def test_seq_sort_creation(self): """SeqSort creates a SeqSortRef.""" - from lean_py.z3 import SeqSort, SeqSortRef s = SeqSort(IntSort()) assert isinstance(s, SeqSortRef) def test_seq_sort_char_is_string(self): """SeqSort(CharSort()) returns StringSort.""" - from lean_py.z3 import SeqSort, CharSort s = SeqSort(CharSort()) assert isinstance(s, StringSortRef) def test_empty_seq(self): """Empty(SeqSort) creates a SeqRef.""" - from lean_py.z3 import SeqSort, SeqRef, Empty s = SeqSort(IntSort()) e = Empty(s) @@ -2055,14 +2066,12 @@ def test_empty_seq(self): def test_unit_seq(self): """Unit creates a SeqRef from a non-string element.""" - from lean_py.z3 import Unit, SeqRef u = Unit(IntVal(42)) assert isinstance(u, SeqRef) def test_seq_concat(self): """Sequence concatenation via + operator.""" - from lean_py.z3 import SeqSort, SeqRef, Empty, Unit s1 = Unit(IntVal(1)) s2 = Unit(IntVal(2)) @@ -2073,16 +2082,15 @@ def test_seq_concat(self): def test_seq_length(self): """Length works on SeqRef.""" - from lean_py.z3 import Unit, SeqRef from lean_py.z3.core import ArithRef s = Unit(IntVal(42)) - l = Length(s) - assert isinstance(l, ArithRef) + length = Length(s) + assert isinstance(length, ArithRef) def test_seq_contains(self): """Contains works on SeqRef.""" - from lean_py.z3 import Unit, SeqRef, BoolRef + from lean_py.z3 import BoolRef s = Unit(IntVal(1)) t = Unit(IntVal(1)) @@ -2091,7 +2099,7 @@ def test_seq_contains(self): def test_seq_prefix_of(self): """PrefixOf works on SeqRef.""" - from lean_py.z3 import Unit, SeqRef, BoolRef + from lean_py.z3 import BoolRef s = Unit(IntVal(1)) t = Unit(IntVal(1)) @@ -2100,7 +2108,7 @@ def test_seq_prefix_of(self): def test_seq_suffix_of(self): """SuffixOf works on SeqRef.""" - from lean_py.z3 import Unit, SeqRef, BoolRef + from lean_py.z3 import BoolRef s = Unit(IntVal(1)) t = Unit(IntVal(1)) @@ -2109,7 +2117,6 @@ def test_seq_suffix_of(self): def test_seq_const(self): """Const with SeqSort creates SeqRef.""" - from lean_py.z3 import SeqSort, SeqRef s = Const("s", SeqSort(IntSort())) assert isinstance(s, SeqRef) diff --git a/tests/test_z3_ported.py b/tests/test_z3_ported.py index aeb3657..6c9517f 100644 --- a/tests/test_z3_ported.py +++ b/tests/test_z3_ported.py @@ -17,133 +17,395 @@ from lean_py.kernel import Kernel from lean_py.z3 import ( + FP, + RNA, + RNE, + RTN, + RTP, + RTZ, + UGE, + UGT, + ULE, + ULT, + # Arith functions + Abs, + AllChar, + # Operations + And, + AndThen, + ApplyResult, + ArithRef, + Array, + ArrayRef, + ArraySort, + ArraySortRef, + AsArray, + AShr, + AstMap, + AstRef, + AstVector, + At, + AtLeast, + # Pseudo-boolean + AtMost, + BitVec, + BitVecNumRef, + BitVecRef, + BitVecs, + BitVecSort, + BitVecVal, + Bool, + BoolRef, + Bools, # Sorts - BoolSort, IntSort, NatSort, RealSort, DeclareSort, - BitVecSort, ArraySort, StringSort, - SortRef, BoolSortRef, ArithSortRef, BitVecSortRef, ArraySortRef, - StringSortRef, ReSort, + BoolSort, + BoolSortRef, + BoolVal, + BoolVector, + BV2Int, + BVAddNoOverflow, + BVAddNoUnderflow, + BVMulNoOverflow, + BVMulNoUnderflow, + BvNand, + BvNor, + BVRedAnd, + BVRedOr, + BVSDivNoOverflow, + BVSubNoOverflow, + BVSubNoUnderflow, + BvXnor, + CharFromBv, + CharIsDigit, + CharSort, + CharToBv, + CharToInt, + CharVal, + Complement, + Concat, + Const, + Consts, + Contains, + # Stubs — Context / AstVector / AstMap + Context, + CreateDatatypes, + # Datatype + Datatype, + DeclareSort, + Diff, + DisjointSum, + Distinct, + Empty, + EmptySet, + EnumSort, + Exists, # Expressions - ExprRef, BoolRef, ArithRef, BitVecRef, ArrayRef, - QuantifierRef, StringRef, ReRef, - # Numeric references - IntNumRef, RatNumRef, BitVecNumRef, + ExprRef, + Extract, + FailIf, + FiniteDomainSize, + FiniteDomainSort, + FiniteDomainVal, + # Stubs — Fixedpoint / RecFunction + Fixedpoint, + Float16, + Float32, + Float64, + Float128, + # Quantifiers + ForAll, + FPNumRef, + FPRef, + FPRMRef, + FPs, + FPSort, + # Stubs — FP + FPSortRef, + FPVal, + FreshBool, + # Fresh + FreshConst, + FreshInt, + FreshReal, + FullSet, # Functions - FuncDeclRef, Function, + FuncDeclRef, + FuncEntry, + # Stubs — model introspection + FuncInterp, + Function, + # Tactic + Goal, + If, + Implies, + IndexOf, + InRe, # Variable constructors - Int, Ints, Nat, Real, Reals, Bool, Bools, - BitVec, BitVecs, Array, Const, Consts, - # Vector constructors - IntVector, BoolVector, RealVector, + Int, + Int2BV, + Intersect, + # Numeric references + IntNumRef, + Ints, + IntSort, + IntToStr, # Value constructors - IntVal, NatVal, RealVal, BoolVal, BitVecVal, StringVal, - # String constructors - String, Strings, - # Array operations - Select, Store, K, Map, AsArray, - # Datatype - Datatype, CreateDatatypes, EnumSort, TupleSort, - # Operations - And, Or, Not, Implies, Xor, If, Distinct, - # Quantifiers - ForAll, Exists, - # Substitute - substitute, - # BV functions - LShR, ULE, ULT, UGE, UGT, UDiv, URem, - Extract, Concat, ZeroExt, SignExt, BV2Int, Int2BV, - RotateLeft, RotateRight, SDiv, SRem, AShr, - # BV extras - RepeatBitVec, BVRedAnd, BVRedOr, - BvNand, BvNor, BvXnor, - BVAddNoOverflow, BVAddNoUnderflow, - BVSubNoOverflow, BVSubNoUnderflow, - BVMulNoOverflow, BVMulNoUnderflow, - BVSDivNoOverflow, - # Arith functions - Abs, ToReal, ToInt, Sum, Product, - IsInt, Sqrt, - # Rational - RatVal, Q, - # Pseudo-boolean - AtMost, AtLeast, PbEq, PbLe, PbGe, - # Fresh - FreshConst, FreshInt, FreshBool, FreshReal, + IntVal, + # Vector constructors + IntVector, + IsInt, + IsMember, + IsSubset, + K, # Lambda Lambda, + # Stubs — string/regex extras + LastIndexOf, # String functions - Length, Contains, PrefixOf, SuffixOf, Replace, - SubString, IndexOf, StrConcat, StrToInt, IntToStr, + Length, + Loop, + # BV functions + LShR, + Map, + ModelRef, + MultiPattern, + Nat, + NatSort, + NatVal, + Not, + Optimize, + Option, + Or, + OrElse, + ParAndThen, + ParOr, + ParThen, + PbEq, + PbGe, + PbLe, + Plus, + PrefixOf, + Probe, + ProbeAnd, + ProbeOr, + Product, + Q, + Range, + RatNumRef, + # Rational + RatVal, # Regex functions - Re, Star, Plus, Option, Union, Intersect, - Complement, Range, Loop, InRe, AllChar, - # Predicates - is_expr, is_true, is_false, is_int, is_real, - is_bool, is_bv, is_array, is_const, is_var, - is_quantifier, is_eq, is_distinct, is_and, is_or, - is_not, is_implies, is_add, is_mul, is_sub, is_div, - is_string, is_string_value, - is_arith, is_sort, is_app, is_func_decl, - is_int_value, is_rational_value, is_bv_value, - is_le, is_lt, is_ge, is_gt, is_mod, is_idiv, - # Solver - Solver, ModelRef, sat, unsat, unknown, - set_kernel, prove, solve, simplify, - set_param, set_option, - SolverFor, SimpleSolver, solve_using, - Optimize, parse_smt2_string, parse_smt2_file, - # Tactic - Goal, ApplyResult, Tactic, Then, OrElse, Repeat, - AndThen, With, TryFor, ParOr, ParThen, ParAndThen, - # Stubs — Context / AstVector / AstMap - Context, main_ctx, get_ctx, AstRef, AstVector, AstMap, - # Stubs — FP - FPSortRef, FPRef, FPNumRef, FPRMRef, - FPSort, Float16, Float32, Float64, Float128, - FP, FPs, FPVal, - fpNaN, fpPlusInfinity, fpMinusInfinity, fpPlusZero, fpMinusZero, - RoundNearestTiesToEven, RNE, RoundNearestTiesToAway, RNA, - RoundTowardPositive, RTP, RoundTowardNegative, RTN, RoundTowardZero, RTZ, - fpAdd, fpSub, fpMul, fpDiv, fpNeg, fpAbs, fpSqrt, fpFMA, fpRem, fpMin, fpMax, - fpLEQ, fpLT, fpGEQ, fpGT, fpEQ, - fpIsNaN, fpIsInf, fpIsZero, fpIsNormal, fpIsSubnormal, fpIsNegative, fpIsPositive, - fpToReal, fpToSBV, fpToUBV, fpToFP, fpBVToFP, fpFPToFP, fpRealToFP, - fpSignedToFP, fpUnsignedToFP, - # Stubs — Sets - SetSort, EmptySet, FullSet, IsMember, SetAdd, SetDel, - SetUnion, SetIntersect, SetComplement, SetDifference, IsSubset, SetHasSize, + Re, + Real, + Reals, + RealSort, + RealVal, + RealVector, + RecAddDefinition, + RecFunction, + Repeat, + # BV extras + RepeatBitVec, + Replace, + ReRef, + RotateLeft, + RotateRight, + RoundNearestTiesToAway, + RoundNearestTiesToEven, + RoundTowardNegative, + RoundTowardPositive, + RoundTowardZero, + SDiv, + # Array operations + Select, # Stubs — Sequences / Char / FiniteDomain - SeqSort, Empty, Full, Unit, - CharSort, CharVal, CharFromBv, CharToBv, CharToInt, CharIsDigit, - FiniteDomainSort, FiniteDomainVal, FiniteDomainSize, - # Stubs — Fixedpoint / RecFunction - Fixedpoint, RecFunction, RecAddDefinition, + SeqSort, + SetAdd, + SetComplement, + SetDel, + SetDifference, + SetHasSize, + SetIntersect, + # Stubs — Sets + SetSort, + SetUnion, + SignExt, + SimpleSolver, + # Solver + Solver, + SolverFor, + SortRef, + Sqrt, + SRem, + Star, + Statistics, + Store, + StrConcat, + StrFromCode, + # String constructors + String, + StringRef, + Strings, + StringSort, + StringSortRef, + StringVal, + StrToCode, + StrToInt, + SubString, + SuffixOf, + Sum, + Tactic, + Then, + ToInt, + ToReal, + TryFor, + TupleSort, + UDiv, + Union, + Unit, + # Stubs — Update / Probe / Statistics + Update, + URem, # Stubs — Var / MultiPattern / DisjointSum - Var, get_var_index, MultiPattern, DisjointSum, - # Stubs — predicates - is_ast, is_fp, is_fprm, is_fp_value, - is_seq, is_re, is_const_array, is_K, is_map, is_select, is_store, - is_to_real, is_to_int, is_is_int, is_pattern, - # Stubs — string/regex extras - LastIndexOf, StrToCode, StrFromCode, At, Diff, + Var, + With, + Xor, + ZeroExt, + disable_trace, + enable_trace, # Stubs — structural equality / utilities - eq, enable_trace, disable_trace, open_log, - get_version, get_version_string, get_full_version, - # Stubs — model introspection - FuncInterp, FuncEntry, - # Stubs — Update / Probe / Statistics - Update, Probe, ProbeAnd, ProbeOr, FailIf, Statistics, + eq, + fpAbs, + fpAdd, + fpBVToFP, + fpDiv, + fpEQ, + fpFMA, + fpFPToFP, + fpGEQ, + fpGT, + fpIsInf, + fpIsNaN, + fpIsNegative, + fpIsNormal, + fpIsPositive, + fpIsSubnormal, + fpIsZero, + fpLEQ, + fpLT, + fpMax, + fpMin, + fpMinusInfinity, + fpMinusZero, + fpMul, + fpNaN, + fpNeg, + fpPlusInfinity, + fpPlusZero, + fpRealToFP, + fpRem, + fpSignedToFP, + fpSqrt, + fpSub, + fpToFP, + fpToReal, + fpToSBV, + fpToUBV, + fpUnsignedToFP, + get_ctx, + get_full_version, + get_var_index, + get_version, + get_version_string, + is_add, + is_and, + is_app, + is_arith, + is_array, + # Stubs — predicates + is_ast, + is_bool, + is_bv, + is_bv_value, + is_const, + is_const_array, + is_distinct, + is_div, + is_eq, + # Predicates + is_expr, + is_false, + is_fp, + is_fp_value, + is_fprm, + is_func_decl, + is_ge, + is_gt, + is_idiv, + is_implies, + is_int, + is_int_value, + is_K, + is_le, + is_lt, + is_mod, + is_mul, + is_not, + is_or, + is_pattern, + is_quantifier, + is_rational_value, + is_re, + is_real, + is_select, + is_seq, + is_sort, + is_store, + is_string, + is_string_value, + is_sub, + is_to_int, + is_to_real, + is_true, + is_var, + main_ctx, + open_log, + parse_smt2_file, + parse_smt2_string, + prove, + sat, + set_kernel, + set_option, + set_param, + simplify, + solve, + solve_using, + # Substitute + substitute, + unknown, + unsat, ) from lean_py.z3._ast import ( - BinOp, BinOpNode, UnOp, UnOpNode, - BoolLit, IntLit, NatLit, BvLit, Var as AstVar, - ForAllNode, ExistsNode, DistinctNode, IteNode, - SelectNode, StoreNode, ConstArrayNode, LambdaNode, - ToRealNode, ToIntNode, ExtractNode, ZeroExtNode, SignExtNode, - StringLit, StrConcatNode, StrLenNode, StrContainsNode, - ReStarNode, InReNode, - PropSort, IntASTSort, StringASTSort, + BinOp, + BinOpNode, + BoolLit, + BvLit, + DistinctNode, + ExistsNode, + ForAllNode, + InReNode, + IntLit, + IteNode, + LambdaNode, + NatLit, + ReStarNode, + SelectNode, + StrConcatNode, + StrContainsNode, + StringLit, + ToRealNode, + UnOpNode, ) -from lean_py.z3.solver import _try_prove @pytest.fixture(scope="module") @@ -863,7 +1125,9 @@ def test_dog_cat_mouse_unsat_variant(self, kernel): """No solution with impossible extra constraint.""" dog, cat, mouse = Ints("dog cat mouse") constraints = [ - dog >= 1, cat >= 1, mouse >= 1, + dog >= 1, + cat >= 1, + mouse >= 1, dog + cat + mouse == 100, dog * 15 + cat + mouse / 4 == 100, # integer division mouse < 0, # impossible with mouse >= 1 @@ -892,7 +1156,10 @@ def test_2queens_unsat(self, kernel): """2 queens on 2x2 board: impossible.""" q0, q1 = Ints("q0 q1") constraints = [ - q0 >= 1, q0 <= 2, q1 >= 1, q1 <= 2, + q0 >= 1, + q0 <= 2, + q1 >= 1, + q1 <= 2, Distinct(q0, q1), q0 - q1 != IntVal(1), q0 - q1 != IntVal(-1), @@ -1129,8 +1396,8 @@ def test_string_concat_operator(self): def test_string_length(self): s = String("s") - l = Length(s) - assert is_int(l) + length = Length(s) + assert is_int(length) def test_contains(self): s = String("s") @@ -1481,7 +1748,7 @@ def test_arith_operators(self): assert isinstance((x * y)._ast, BinOpNode) assert isinstance((x / y)._ast, BinOpNode) assert isinstance((x % y)._ast, BinOpNode) - assert isinstance((x ** y)._ast, BinOpNode) + assert isinstance((x**y)._ast, BinOpNode) assert isinstance((-x)._ast, UnOpNode) assert (+x) is x @@ -1493,7 +1760,7 @@ def test_arith_reverse_operators(self): assert isinstance((2 * x)._ast, BinOpNode) assert isinstance((10 / x)._ast, BinOpNode) assert isinstance((10 % x)._ast, BinOpNode) - assert isinstance((2 ** x)._ast, BinOpNode) + assert isinstance((2**x)._ast, BinOpNode) def test_comparison_operators(self): x = Int("x") @@ -2838,7 +3105,6 @@ def test_var_name(self): def test_var_sort(self): x = Int("x") - y = Real("y") q = ForAll([x], x > 0) assert q.var_sort(0) == IntSort() @@ -2929,6 +3195,7 @@ def test_denominator_as_long(self): def test_as_fraction(self): from fractions import Fraction + r = RatVal(1, 3) f = r.as_fraction() assert f == Fraction(1, 3) @@ -3182,11 +3449,8 @@ def test_repr(self): class TestParseSmt2String: - def test_basic_assertions(self): - result = parse_smt2_string( - "(declare-const x Int) (assert (> x 0)) (assert (< x 10))" - ) + result = parse_smt2_string("(declare-const x Int) (assert (> x 0)) (assert (< x 10))") assert len(result) == 2 def test_with_decls(self): @@ -3207,28 +3471,22 @@ def test_with_sorts(self): def test_boolean_ops(self): result = parse_smt2_string( - "(declare-const p Bool) (declare-const q Bool)" - " (assert (and p (or q (not p))))" + "(declare-const p Bool) (declare-const q Bool) (assert (and p (or q (not p))))" ) assert len(result) == 1 def test_let_binding(self): - result = parse_smt2_string( - "(declare-const x Int) (assert (let ((y (+ x 1))) (> y 0)))" - ) + result = parse_smt2_string("(declare-const x Int) (assert (let ((y (+ x 1))) (> y 0)))") assert len(result) == 1 def test_bitvec(self): result = parse_smt2_string( - "(declare-const x (_ BitVec 8))" - " (assert (= (bvadd x #x01) #b00000010))" + "(declare-const x (_ BitVec 8)) (assert (= (bvadd x #x01) #b00000010))" ) assert len(result) == 1 def test_quantifier(self): - result = parse_smt2_string( - "(assert (forall ((x Int)) (>= (* x x) 0)))" - ) + result = parse_smt2_string("(assert (forall ((x Int)) (>= (* x x) 0)))") assert len(result) == 1 def test_empty(self): @@ -3237,38 +3495,29 @@ def test_empty(self): def test_comments(self): result = parse_smt2_string( - "; this is a comment\n" - "(declare-const x Int)\n" - "; another comment\n" - "(assert (> x 0))" + "; this is a comment\n(declare-const x Int)\n; another comment\n(assert (> x 0))" ) assert len(result) == 1 def test_declare_fun(self): result = parse_smt2_string( - "(declare-fun f (Int Int) Int)" - " (declare-const x Int)" - " (assert (> (f x x) 0))" + "(declare-fun f (Int Int) Int) (declare-const x Int) (assert (> (f x x) 0))" ) assert len(result) == 1 def test_ite(self): - result = parse_smt2_string( - "(declare-const x Int) (assert (= (ite (> x 0) x (- x)) x))" - ) + result = parse_smt2_string("(declare-const x Int) (assert (= (ite (> x 0) x (- x)) x))") assert len(result) == 1 def test_implies(self): result = parse_smt2_string( - "(declare-const p Bool) (declare-const q Bool)" - " (assert (=> p q))" + "(declare-const p Bool) (declare-const q Bool) (assert (=> p q))" ) assert len(result) == 1 def test_distinct(self): result = parse_smt2_string( - "(declare-const x Int) (declare-const y Int)" - " (assert (distinct x y))" + "(declare-const x Int) (declare-const y Int) (assert (distinct x y))" ) assert len(result) == 1 diff --git a/tests/test_z3_semantic.py b/tests/test_z3_semantic.py index 05f2088..58c5f20 100644 --- a/tests/test_z3_semantic.py +++ b/tests/test_z3_semantic.py @@ -8,54 +8,123 @@ from __future__ import annotations from pathlib import Path + import pytest from lean_py.kernel import Kernel from lean_py.z3 import ( - And, Or, Not, Implies, Xor, If, Distinct, - Bool, BoolVal, BoolSort, - Int, IntVal, IntSort, Ints, - Nat, NatVal, NatSort, - Real, RealVal, RealSort, Reals, ToReal, ToInt, - Q, RatVal, - BitVec, BitVecVal, BitVecSort, BitVecs, - Concat, Extract, ZeroExt, SignExt, - RotateLeft, RotateRight, LShR, AShr, - BV2Int, Int2BV, ULT, ULE, UGT, UGE, - SDiv, SRem, UDiv, URem, - Array, ArraySort, Select, Store, K, - String, StringVal, StringSort, Strings, - Length, Contains, PrefixOf, SuffixOf, - Replace, SubString, IndexOf, StrConcat, - StrToInt, IntToStr, - Re, Star, Plus, Option, Union, Intersect, - Range, Loop, InRe, - Float64, FPVal, FPSort, FPNumRef, FPRef, - fpAdd, fpSub, fpMul, fpDiv, fpNeg, fpAbs, - fpMin, fpMax, fpLT, fpLEQ, fpGT, fpGEQ, fpEQ, - fpIsNaN, fpIsZero, fpIsInf, - fpNaN, fpPlusInfinity, fpMinusInfinity, - fpPlusZero, fpMinusZero, RNE, - ForAll, Exists, Lambda, - Function, DeclareSort, Const, - Solver, sat, unsat, unknown, - Sum, Product, Abs, + UGT, + ULE, + ULT, + Abs, + And, + Array, + AShr, + BitVec, + BitVecs, + BitVecVal, + Bool, + BoolSort, + BoolVal, + BV2Int, + Concat, + Const, + Contains, + DeclareSort, + Distinct, + Exists, + Extract, + Float64, + ForAll, + FPVal, + Function, + If, + Implies, + IndexOf, + Int, + Int2BV, + Ints, + IntSort, + IntToStr, + IntVal, + K, + Lambda, + Length, + LShR, + Nat, + NatVal, + Not, + Or, + PrefixOf, + Product, + Q, + Reals, + RealVal, + Replace, + RotateLeft, + RotateRight, + SDiv, + Select, + SignExt, + Solver, + SRem, + Store, + StrConcat, + String, + Strings, + StringVal, + StrToInt, + SubString, + SuffixOf, + Sum, + ToReal, + UDiv, + URem, + Xor, + ZeroExt, + fpAbs, + fpAdd, + fpDiv, + fpEQ, + fpGEQ, + fpGT, + fpIsInf, + fpIsNaN, + fpIsZero, + fpLEQ, + fpLT, + fpMax, + fpMin, + fpMinusInfinity, + fpMinusZero, + fpMul, + fpNaN, + fpNeg, + fpPlusInfinity, + fpPlusZero, + fpSub, + sat, set_kernel, - Complement, + unsat, ) from lean_py.z3.solver import _try_prove -from lean_py.z3.tactic import Tactic, Goal +from lean_py.z3.tactic import Goal, Tactic @pytest.fixture(scope="module") def kernel(example_lib) -> Kernel: k = Kernel(example_lib) import subprocess - sp = subprocess.check_output( - ["lake", "env", "printenv", "LEAN_PATH"], - cwd=str(Path(__file__).parent / "lean"), - ).decode().strip() + + sp = ( + subprocess.check_output( + ["lake", "env", "printenv", "LEAN_PATH"], + cwd=str(Path(__file__).parent / "lean"), + ) + .decode() + .strip() + ) k.init_search(sp) k.load(["Init", "LeanPy.Z3"]) set_kernel(k) @@ -66,6 +135,7 @@ def kernel(example_lib) -> Kernel: # SECTION 1: BOOLEAN LOGIC — Truth tables, laws, tautologies # =================================================================== + class TestBoolTruthTables: """Exhaustive truth-table verification for basic connectives.""" @@ -220,6 +290,7 @@ def test_ite_false_branch(self, kernel): # SECTION 2: INTEGER ARITHMETIC # =================================================================== + class TestIntArithmeticGround: """Ground integer arithmetic proofs (concrete values).""" @@ -356,6 +427,7 @@ def test_nat_succ_pos(self, kernel): # SECTION 3: RATIONAL (REAL) ARITHMETIC # =================================================================== + class TestRationalGround: """Ground rational arithmetic proofs.""" @@ -420,6 +492,7 @@ def test_to_real_preserves_mul(self, kernel): # SECTION 4: BIT-VECTOR OPERATIONS # =================================================================== + class TestBVGroundArith: """Ground bit-vector arithmetic proofs.""" @@ -459,13 +532,19 @@ class TestBVBitwise: """Ground bitwise operation proofs.""" def test_and(self, kernel): - assert _try_prove(BitVecVal(0b11001100, 8) & BitVecVal(0b10101010, 8) == BitVecVal(0b10001000, 8)) + assert _try_prove( + BitVecVal(0b11001100, 8) & BitVecVal(0b10101010, 8) == BitVecVal(0b10001000, 8) + ) def test_or(self, kernel): - assert _try_prove(BitVecVal(0b11001100, 8) | BitVecVal(0b10101010, 8) == BitVecVal(0b11101110, 8)) + assert _try_prove( + BitVecVal(0b11001100, 8) | BitVecVal(0b10101010, 8) == BitVecVal(0b11101110, 8) + ) def test_xor(self, kernel): - assert _try_prove(BitVecVal(0b11001100, 8) ^ BitVecVal(0b10101010, 8) == BitVecVal(0b01100110, 8)) + assert _try_prove( + BitVecVal(0b11001100, 8) ^ BitVecVal(0b10101010, 8) == BitVecVal(0b01100110, 8) + ) def test_not(self, kernel): assert _try_prove(~BitVecVal(0b11001100, 8) == BitVecVal(0b00110011, 8)) @@ -583,6 +662,7 @@ def test_bv2int_unsigned(self, kernel): # SECTION 5: ARRAY THEORY # =================================================================== + class TestArraySemantics: """Array theory proofs — store/select axioms.""" @@ -615,8 +695,9 @@ def test_store_chain(self, kernel): a = K(IntSort(), IntVal(0)) a = Store(a, IntVal(0), IntVal(10)) a = Store(a, IntVal(1), IntVal(20)) - assert _try_prove(And(Select(a, IntVal(0)) == IntVal(10), - Select(a, IntVal(1)) == IntVal(20))) + assert _try_prove( + And(Select(a, IntVal(0)) == IntVal(10), Select(a, IntVal(1)) == IntVal(20)) + ) def test_constant_array_bool(self, kernel): """Constant True array: all elements are True.""" @@ -634,11 +715,14 @@ def test_store_preserves_other(self, kernel): # SECTION 6: STRING THEORY # =================================================================== + class TestStringGround: """Ground string proofs.""" def test_concat(self, kernel): - assert _try_prove(StrConcat(StringVal("hello"), StringVal(" world")) == StringVal("hello world")) + assert _try_prove( + StrConcat(StringVal("hello"), StringVal(" world")) == StringVal("hello world") + ) def test_length(self, kernel): assert _try_prove(Length(StringVal("hello")) == IntVal(5)) @@ -680,10 +764,15 @@ def test_contains_self(self, kernel): assert _try_prove(Contains(StringVal("abc"), StringVal("abc"))) def test_replace(self, kernel): - assert _try_prove(Replace(StringVal("hello world"), StringVal("world"), StringVal("lean")) == StringVal("hello lean")) + assert _try_prove( + Replace(StringVal("hello world"), StringVal("world"), StringVal("lean")) + == StringVal("hello lean") + ) def test_replace_no_match(self, kernel): - assert _try_prove(Replace(StringVal("abc"), StringVal("xyz"), StringVal("!")) == StringVal("abc")) + assert _try_prove( + Replace(StringVal("abc"), StringVal("xyz"), StringVal("!")) == StringVal("abc") + ) def test_indexof_found(self, kernel): assert _try_prove(IndexOf(StringVal("abcdef"), StringVal("cd"), IntVal(0)) == IntVal(2)) @@ -742,6 +831,7 @@ def test_length_nonneg(self, kernel): # SECTION 7: FLOATING-POINT PROOFS # =================================================================== + class TestFPGroundArith: """Ground floating-point arithmetic proofs.""" @@ -859,6 +949,7 @@ def test_normal_is_not_inf(self, kernel): # SECTION 8: QUANTIFIER PROOFS # =================================================================== + class TestForAllProofs: """Universal quantifier proofs.""" @@ -942,10 +1033,7 @@ def test_syllogism(self, kernel): Mortal = Function("Mortal", Person, BoolSort()) socrates = Const("socrates", Person) x = Const("x", Person) - premise = And( - ForAll([x], Implies(Human(x), Mortal(x))), - Human(socrates) - ) + premise = And(ForAll([x], Implies(Human(x), Mortal(x))), Human(socrates)) assert _try_prove(Implies(premise, Mortal(socrates))) @@ -953,6 +1041,7 @@ def test_syllogism(self, kernel): # SECTION 9: SOLVER SEMANTICS # =================================================================== + class TestSolverSemantics: """Solver behavioral correctness tests.""" @@ -985,7 +1074,6 @@ def test_two_equalities_unsat(self, kernel): assert s.check() == unsat def test_push_pop_restores(self, kernel): - x = Int("x") s = Solver() s.add(BoolVal(True)) s.push() @@ -1046,6 +1134,7 @@ def test_context_manager(self, kernel): # SECTION 10: NEGATIVE PROOFS (things that should NOT be provable) # =================================================================== + class TestNegativeProofs: """Claims that must NOT be provable.""" @@ -1113,6 +1202,7 @@ def test_nan_not_zero(self, kernel): # SECTION 11: IF-THEN-ELSE PROOFS # =================================================================== + class TestIfThenElse: """Conditional expression proofs.""" @@ -1144,6 +1234,7 @@ def test_ite_min(self, kernel): # SECTION 12: DISTINCT # =================================================================== + class TestDistinct: """Distinctness constraint proofs.""" @@ -1165,6 +1256,7 @@ def test_distinct_implies_neq(self, kernel): # SECTION 13: MIXED-SORT PROOFS # =================================================================== + class TestMixedSort: """Cross-sort interaction proofs.""" @@ -1188,6 +1280,7 @@ def test_bv_to_int_add(self, kernel): # SECTION 14: SUM / PRODUCT / ABS # =================================================================== + class TestSumProductAbs: """Aggregation function proofs.""" @@ -1221,6 +1314,7 @@ def test_triangle_inequality(self, kernel): # SECTION 15: LAMBDA APPLICATION # =================================================================== + class TestLambdaApplication: """Lambda expression semantics via arrays.""" @@ -1247,6 +1341,7 @@ def test_lambda_square(self, kernel): # SECTION 16: COMPLEX COMBINED PROOFS # =================================================================== + class TestComplexProofs: """Multi-step proofs combining multiple theories.""" @@ -1268,7 +1363,10 @@ def test_linear_system(self, kernel): def test_modular_identity(self, kernel): """(a + b) mod n = ((a mod n) + (b mod n)) mod n for n > 0""" # Ground instance: (7 + 8) mod 5 = ((7 mod 5) + (8 mod 5)) mod 5 - assert _try_prove(IntVal(15) % IntVal(5) == ((IntVal(7) % IntVal(5)) + (IntVal(8) % IntVal(5))) % IntVal(5)) + assert _try_prove( + IntVal(15) % IntVal(5) + == ((IntVal(7) % IntVal(5)) + (IntVal(8) % IntVal(5))) % IntVal(5) + ) def test_bv_add_sub_inverse(self, kernel): """(x + y) - y = x for bitvectors.""" @@ -1282,12 +1380,15 @@ def test_string_length_nonneg(self, kernel): def test_concat_contains_parts(self, kernel): """'hello' ++ 'world' contains 'hello' as prefix (ground).""" - assert _try_prove(PrefixOf(StringVal("hello"), StrConcat(StringVal("hello"), StringVal("world")))) + assert _try_prove( + PrefixOf(StringVal("hello"), StrConcat(StringVal("hello"), StringVal("world"))) + ) def test_fp_mul_comm_ground(self, kernel): """FP multiplication is commutative for ground values.""" - assert _try_prove(fpEQ(fpMul(RNE(), FPVal(2.0), FPVal(3.0)), - fpMul(RNE(), FPVal(3.0), FPVal(2.0)))) + assert _try_prove( + fpEQ(fpMul(RNE(), FPVal(2.0), FPVal(3.0)), fpMul(RNE(), FPVal(3.0), FPVal(2.0))) + ) def test_array_swap(self, kernel): """Swapping two elements and reading back.""" diff --git a/uv.lock b/uv.lock index 65d9526..42e4cf9 100644 --- a/uv.lock +++ b/uv.lock @@ -1,6 +1,10 @@ version = 1 revision = 3 requires-python = ">=3.12" +resolution-markers = [ + "python_full_version >= '3.15'", + "python_full_version < '3.15'", +] [[package]] name = "alabaster" @@ -11,6 +15,46 @@ wheels = [ { url = "https://files.pythonhosted.org/packages/7e/b3/6b4067be973ae96ba0d615946e314c5ae35f9f993eca561b356540bb0c2b/alabaster-1.0.0-py3-none-any.whl", hash = "sha256:fc6786402dc3fcb2de3cabd5fe455a2db534b371124f1f21de8731783dec828b", size = 13929, upload-time = "2024-07-26T18:15:02.05Z" }, ] +[[package]] +name = "ast-serialize" +version = "0.5.0" +source = { registry = "https://pypi.org/simple" } +sdist = { url = "https://files.pythonhosted.org/packages/81/9d/09e27731bd5864a9ce04e3244074e674bb8936bf62b45e0357248717adac/ast_serialize-0.5.0.tar.gz", hash = "sha256:5880091bfe6f4f986f22866375c2e884843e7a0b6343ae41aeea659613d879b6", size = 61157, upload-time = "2026-05-17T17:48:29.429Z" } +wheels = [ + { url = "https://files.pythonhosted.org/packages/c0/9a/13dde51ba9e15f8b97957ab7cb0120d0e381524d651c6bd630b9c359227f/ast_serialize-0.5.0-cp314-cp314t-macosx_10_12_x86_64.whl", hash = "sha256:8f5c14f169eb0972c0c21bada5358b23d6047c76583b005234f865b11f1fa00a", size = 1183520, upload-time = "2026-05-17T17:47:30.831Z" }, + { url = "https://files.pythonhosted.org/packages/37/de/5a7f0a9fe68944f536632a5af84676739c7d2582be42deb082634bf3a754/ast_serialize-0.5.0-cp314-cp314t-macosx_11_0_arm64.whl", hash = "sha256:7d1a2de9de5be04652f0ed60738356ef94f66db37924a9499fffe98dc491aa0b", size = 1175779, upload-time = "2026-05-17T17:47:32.551Z" }, + { url = "https://files.pythonhosted.org/packages/9c/81/0bb853e76e4f6e9a1855d569003c59e19ffac45f7079d91505d1bb212f92/ast_serialize-0.5.0-cp314-cp314t-manylinux_2_17_aarch64.manylinux2014_aarch64.whl", hash = "sha256:be5173fb66f9b49026d9d5a2ff0fc7c7009077107c0eb285b2d60fdf1fe10bd1", size = 1233750, upload-time = "2026-05-17T17:47:34.731Z" }, + { url = "https://files.pythonhosted.org/packages/e5/d3/4cf705beeccc08754d0bbda99aefff26110e209b9a07ac8a6b60eec48531/ast_serialize-0.5.0-cp314-cp314t-manylinux_2_17_armv7l.manylinux2014_armv7l.whl", hash = "sha256:f8015cd071ac1339924ee2b8098c93e00e155f30a16f40ec9816fcf84f4753f6", size = 1235942, upload-time = "2026-05-17T17:47:36.287Z" }, + { url = "https://files.pythonhosted.org/packages/26/c8/ee097e437ea27dd2b8b227865c875492b585650a5802a22d82b304c8201b/ast_serialize-0.5.0-cp314-cp314t-manylinux_2_17_ppc64le.manylinux2014_ppc64le.whl", hash = "sha256:5499e8797edff2a9186aa313ed382c6b422e798e9332d9953badcee6e69a88f2", size = 1442517, upload-time = "2026-05-17T17:47:38.17Z" }, + { url = "https://files.pythonhosted.org/packages/ff/bd/68063442838f1ba68ec72b5436430bc75b3bb17a1a3c3063f09b0c05ae2b/ast_serialize-0.5.0-cp314-cp314t-manylinux_2_17_s390x.manylinux2014_s390x.whl", hash = "sha256:6848f2a093fb5548751a9a09bff8fcd229e2bbeb0e3331f391b6ae6d26cd9903", size = 1254081, upload-time = "2026-05-17T17:47:39.826Z" }, + { url = "https://files.pythonhosted.org/packages/50/e2/1e520793bc6a4e4524a6ab022391e827825eaa0c3811828bfdc6852eca26/ast_serialize-0.5.0-cp314-cp314t-manylinux_2_17_x86_64.manylinux2014_x86_64.whl", hash = "sha256:832d4c998e0b091fd60a6d6bceee535483c4d490de9ba85003af835225719261", size = 1259910, upload-time = "2026-05-17T17:47:41.369Z" }, + { url = "https://files.pythonhosted.org/packages/4e/e1/49b60f467979979cfe6913b43948ff25bca971ad0591d181812f163a988e/ast_serialize-0.5.0-cp314-cp314t-manylinux_2_31_riscv64.whl", hash = "sha256:16db7c62ec0b8efe1d7afd283a388d8f74f2605d56032e5a37747d2de8dba027", size = 1250678, upload-time = "2026-05-17T17:47:43.702Z" }, + { url = "https://files.pythonhosted.org/packages/74/ba/66ab9555de6275677566f6574e5ef6c29cb185ea866f643bc06f8280a8ee/ast_serialize-0.5.0-cp314-cp314t-manylinux_2_5_i686.manylinux1_i686.whl", hash = "sha256:baf5eb061eb5bccade4128ad42da33787d72f6013809cd1b590376ece8b3c937", size = 1301603, upload-time = "2026-05-17T17:47:46.256Z" }, + { url = "https://files.pythonhosted.org/packages/66/42/6aca9b9abc710014b2be9059689e5dd1679339e78f567ffb4d255a9e2050/ast_serialize-0.5.0-cp314-cp314t-musllinux_1_2_aarch64.whl", hash = "sha256:104e4a35bd7c124173c41760ef9aaea17ddb3f86c65cb643671d59afbe3ee94c", size = 1410332, upload-time = "2026-05-17T17:47:47.899Z" }, + { url = "https://files.pythonhosted.org/packages/47/68/2f76594432a22581ecf878b5e75a9b8601c24b2241cf0bbeb1e21fcf370c/ast_serialize-0.5.0-cp314-cp314t-musllinux_1_2_armv7l.whl", hash = "sha256:36be371028fc1675acb38a331bde160dbab7ff907fdf00b67eb6911aa106951b", size = 1509979, upload-time = "2026-05-17T17:47:50.942Z" }, + { url = "https://files.pythonhosted.org/packages/40/ac/a93c9b58292653f6c595752f677a08e608f903b710594909e9231a389b3b/ast_serialize-0.5.0-cp314-cp314t-musllinux_1_2_i686.whl", hash = "sha256:061ee58bdb52341c8201a6df41182a977736bae3b7ded87ca7176ca25a8a47ab", size = 1505002, upload-time = "2026-05-17T17:47:54.093Z" }, + { url = "https://files.pythonhosted.org/packages/14/2e/b278f68c497ee2f1d1576cbbef8db5281cd4a5f2db040537592ac9c8862e/ast_serialize-0.5.0-cp314-cp314t-musllinux_1_2_x86_64.whl", hash = "sha256:b15219e9cdc9f53f6f4cb51c009203507228226148c05c5e8fe451c28b435eb3", size = 1456231, upload-time = "2026-05-17T17:47:56.311Z" }, + { url = "https://files.pythonhosted.org/packages/0b/43/419be1c566a4c504cd8fd60ce2f84e790f295495c0f327cfaeadf3d51012/ast_serialize-0.5.0-cp314-cp314t-win32.whl", hash = "sha256:842d1c004bb466c7df036f95fabef789570541922b10976b12f5592a69cf0b38", size = 1058668, upload-time = "2026-05-17T17:47:58.305Z" }, + { url = "https://files.pythonhosted.org/packages/03/6f/c9d4d549295ed05111aeb8853232d1afd9d0a179fddb01eeffbb3a4a6842/ast_serialize-0.5.0-cp314-cp314t-win_amd64.whl", hash = "sha256:b0c06d760909b095cc466356dfccd05a1c7233a6ca191c020dca2c6a6f16c24c", size = 1101075, upload-time = "2026-05-17T17:48:00.35Z" }, + { url = "https://files.pythonhosted.org/packages/d0/8e/d00c5ab30c58222e07d62956fca86c59d91b9ad32997e633c38b526623a3/ast_serialize-0.5.0-cp314-cp314t-win_arm64.whl", hash = "sha256:787baedb0262cc49e8ce37cc15c00ae818e46a165a3b36f5e21ed174998104cb", size = 1075347, upload-time = "2026-05-17T17:48:01.753Z" }, + { url = "https://files.pythonhosted.org/packages/e0/9e/dc2530acb3a60dc6e46d65abf27d1d9f86721694757906a148d90a6860de/ast_serialize-0.5.0-cp39-abi3-macosx_10_12_x86_64.whl", hash = "sha256:0668aa9459cfa8c9c49ddd2163ebcf43088ba045ef7492af6fe22e0098303101", size = 1191380, upload-time = "2026-05-17T17:48:03.738Z" }, + { url = "https://files.pythonhosted.org/packages/26/0a/bd3d18a582f273d6c843d16bb9e22e9e16365ff7991e92f18f798e9f1224/ast_serialize-0.5.0-cp39-abi3-macosx_11_0_arm64.whl", hash = "sha256:bf683d6363edf2b39eed6b6d4fe22d34b6203867a67e27134d9e2a2680c4bc4a", size = 1183879, upload-time = "2026-05-17T17:48:05.463Z" }, + { url = "https://files.pythonhosted.org/packages/40/ae/1f919100f8620887af58fcc381c61a1f218cdf89c6e155f87b213e61010a/ast_serialize-0.5.0-cp39-abi3-manylinux_2_17_aarch64.manylinux2014_aarch64.whl", hash = "sha256:9cc22cf0c9be65e71cf88fda130af60d61eb4a79370ad4cfe7900d48a4aa2211", size = 1244529, upload-time = "2026-05-17T17:48:07.008Z" }, + { url = "https://files.pythonhosted.org/packages/c6/ca/6376559dcce707cdbc1d0d9a13c8d3baaaa501e949ce0ebdc4230cd881aa/ast_serialize-0.5.0-cp39-abi3-manylinux_2_17_armv7l.manylinux2014_armv7l.whl", hash = "sha256:f66173891548c9f2726bf27957b41cabce12fa679dc6da505ddbde4d4b3b31cf", size = 1240560, upload-time = "2026-05-17T17:48:08.46Z" }, + { url = "https://files.pythonhosted.org/packages/35/b2/a620e206b5aeb7efbf2710336df57d457cffbb3991076bbcc1147ef9abd4/ast_serialize-0.5.0-cp39-abi3-manylinux_2_17_ppc64le.manylinux2014_ppc64le.whl", hash = "sha256:e42d729ef2be96a14efbad355093284739e3670ece3e534f82cc8832790911d9", size = 1451172, upload-time = "2026-05-17T17:48:09.922Z" }, + { url = "https://files.pythonhosted.org/packages/fa/e0/4ad5c04c24a40481b2935ce9a0ccdb6023dc8b667167d06ae530cc3512f2/ast_serialize-0.5.0-cp39-abi3-manylinux_2_17_s390x.manylinux2014_s390x.whl", hash = "sha256:b725026bafa801dbd7310eb13a75f0a2e370e7e51b2cb225f9d21fcfadf919ee", size = 1265072, upload-time = "2026-05-17T17:48:11.469Z" }, + { url = "https://files.pythonhosted.org/packages/b2/71/4d1d479aa56d0101c40e17720c3d6ac2af7269ea0487a80b18e7bfd1a5b7/ast_serialize-0.5.0-cp39-abi3-manylinux_2_17_x86_64.manylinux2014_x86_64.whl", hash = "sha256:b54f60c1d78767a53b67eaa663f0dfac3afe606aa07f1301572f588b73d64809", size = 1270488, upload-time = "2026-05-17T17:48:13.575Z" }, + { url = "https://files.pythonhosted.org/packages/6d/4f/0de1bbe06f6edef9fde4ed12ca8e7b3ec7e6e2bd4e672c5af487f7957665/ast_serialize-0.5.0-cp39-abi3-manylinux_2_31_riscv64.whl", hash = "sha256:27d51654fc240a1e87e742d353d98eb45b75f62f129086b3596ab53df2ac2a43", size = 1260702, upload-time = "2026-05-17T17:48:15.141Z" }, + { url = "https://files.pythonhosted.org/packages/75/61/e00872439cfdddcc3c1b6cdaa6e5d904ba8e26a18807c67c4e14409d0ca8/ast_serialize-0.5.0-cp39-abi3-manylinux_2_5_i686.manylinux1_i686.whl", hash = "sha256:2782c36237c46dd1674542f2109740ea5ea485a169bf1431939ada0434e17934", size = 1311182, upload-time = "2026-05-17T17:48:16.779Z" }, + { url = "https://files.pythonhosted.org/packages/76/8e/699a5b955f7926956c95e9e1d74132acad73c2fe7a426f94da89123c20aa/ast_serialize-0.5.0-cp39-abi3-musllinux_1_2_aarch64.whl", hash = "sha256:1943db345233cc7194a470f13afa9c59772c0b123dea0c9414c4d4ca54369759", size = 1421410, upload-time = "2026-05-17T17:48:18.527Z" }, + { url = "https://files.pythonhosted.org/packages/a9/ae/d5b7626874478997adc7a29ab28accf21e596fb590c944290401dfd0b29e/ast_serialize-0.5.0-cp39-abi3-musllinux_1_2_armv7l.whl", hash = "sha256:df1c00022cbbcb064bfaa505aa9c9295362443ce5dacb459d1331d3da353f887", size = 1516587, upload-time = "2026-05-17T17:48:20.133Z" }, + { url = "https://files.pythonhosted.org/packages/0c/ce/b59e02a82d9c4244d64cde502e0b00e83e38816abe19155ceb5437402c7f/ast_serialize-0.5.0-cp39-abi3-musllinux_1_2_i686.whl", hash = "sha256:cae65289fc456fde04af979a2be09302ef5d8ab92ef23e596d6746dc267ada27", size = 1515171, upload-time = "2026-05-17T17:48:21.921Z" }, + { url = "https://files.pythonhosted.org/packages/8b/38/d8d90042747d05aa08d4efcf1c99035a5f670a6bf4c214d31644392afbca/ast_serialize-0.5.0-cp39-abi3-musllinux_1_2_x86_64.whl", hash = "sha256:239a4c354e8d676e9d94631d1d4a64edc6b266f86ff3a5a80aedd344f342c01d", size = 1464668, upload-time = "2026-05-17T17:48:23.544Z" }, + { url = "https://files.pythonhosted.org/packages/dd/51/5b840c4df7334104cecffa28f23904fe81ca89ca223d2450e288de39fd3c/ast_serialize-0.5.0-cp39-abi3-win32.whl", hash = "sha256:143a4ef63285a075871908fda3672dc21864b83a8ec3ee12304aa3e4c5387b9a", size = 1068311, upload-time = "2026-05-17T17:48:25.027Z" }, + { url = "https://files.pythonhosted.org/packages/41/11/ca5672c7d491825bc4cd6702dea106a6b60d928707712ec257c7833ae476/ast_serialize-0.5.0-cp39-abi3-win_amd64.whl", hash = "sha256:cf25572c526add400f26a4750dc6ce0c3bb93fc1f75e7ae0cad4ce4f2cd5c590", size = 1108931, upload-time = "2026-05-17T17:48:26.591Z" }, + { url = "https://files.pythonhosted.org/packages/45/19/cc8bd127d28a43da249aa955cfd164cf8fd534e79e42cea96c4854d72fd0/ast_serialize-0.5.0-cp39-abi3-win_arm64.whl", hash = "sha256:92a31c9c20d25a076edaeec76b128a3535d74a24f340b9a8a7e96c9b86dc9642", size = 1081181, upload-time = "2026-05-17T17:48:28.122Z" }, +] + [[package]] name = "babel" version = "2.18.0" @@ -177,7 +221,9 @@ docs = [ [package.dev-dependencies] dev = [ + { name = "mypy" }, { name = "pytest" }, + { name = "ruff" }, ] [package.metadata] @@ -191,7 +237,71 @@ requires-dist = [ provides-extras = ["docs"] [package.metadata.requires-dev] -dev = [{ name = "pytest", specifier = ">=8.0" }] +dev = [ + { name = "mypy", specifier = ">=1.13" }, + { name = "pytest", specifier = ">=8.0" }, + { name = "ruff", specifier = ">=0.8" }, +] + +[[package]] +name = "librt" +version = "0.11.0" +source = { registry = "https://pypi.org/simple" } +sdist = { url = "https://files.pythonhosted.org/packages/40/08/9e7f6b5d2b5bed6ad055cdd5925f192bb403a51280f86b56554d9d0699a2/librt-0.11.0.tar.gz", hash = "sha256:075dc3ef4458a278e0195cbf6ac9d38808d9b906c5a6c7f7f79c3888276a3fb1", size = 200139, upload-time = "2026-05-10T18:17:25.138Z" } +wheels = [ + { url = "https://files.pythonhosted.org/packages/8b/d0/07c77e067f0838949b43bd89232c29d72efebb9d2801a9750184eb706b71/librt-0.11.0-cp312-cp312-macosx_10_13_x86_64.whl", hash = "sha256:b87504f1690a23b9a2cca841191a04f83895d4fc2dd04df91d82b1a04ca2ad46", size = 144147, upload-time = "2026-05-10T18:15:53.227Z" }, + { url = "https://files.pythonhosted.org/packages/7a/24/8493538fa4f62f982686398a5b8f68008138a75086abdea19ade64bf4255/librt-0.11.0-cp312-cp312-macosx_11_0_arm64.whl", hash = "sha256:40071fc5fe0ce8daa6de616702314a01e1250711682b0523d6ab8d4525910cb3", size = 143614, upload-time = "2026-05-10T18:15:54.657Z" }, + { url = "https://files.pythonhosted.org/packages/ff/1e/f8bad050810d9171f34a1648ed910e56814c2ba61639f2bd53c6377ae24b/librt-0.11.0-cp312-cp312-manylinux2014_aarch64.manylinux_2_17_aarch64.manylinux_2_28_aarch64.whl", hash = "sha256:137e79445c896a0ea7b265f52d23954e05b64222ee1af69e2cb34219067cbb67", size = 485538, upload-time = "2026-05-10T18:15:56.117Z" }, + { url = "https://files.pythonhosted.org/packages/c0/fe/3594ebfbaf03084ba4b120c9ba5c3183fd938a48725e9bbe6ff0a5159ad8/librt-0.11.0-cp312-cp312-manylinux2014_i686.manylinux_2_17_i686.manylinux_2_28_i686.whl", hash = "sha256:cca6644054e78746d8d4ef238681f9c34ff8b584fe6b988ecebb8db3b15e622a", size = 479623, upload-time = "2026-05-10T18:15:57.544Z" }, + { url = "https://files.pythonhosted.org/packages/b0/da/5d1876984b3746c85dbd219dbfcb73c85f54ee263fd32e5b2a632ec14571/librt-0.11.0-cp312-cp312-manylinux2014_x86_64.manylinux_2_17_x86_64.manylinux_2_28_x86_64.whl", hash = "sha256:d5b0eea49f5562861ee8d757a32ef7d559c1d35be2aaaa1ec28941d74c9ffc8a", size = 513082, upload-time = "2026-05-10T18:15:58.805Z" }, + { url = "https://files.pythonhosted.org/packages/19/6e/55bdf5d5ca00c3e18430690bf2c953d8d3ffd3c337418173d33dec985dc9/librt-0.11.0-cp312-cp312-manylinux_2_34_riscv64.manylinux_2_39_riscv64.whl", hash = "sha256:0d1029d7e1ae1a7e647ed6fb5df8c4ce2dffefb7a9f5fd1376a4554d96dac09f", size = 508105, upload-time = "2026-05-10T18:16:00.2Z" }, + { url = "https://files.pythonhosted.org/packages/07/10/f1f23a7c595ee90ece4d35c851e5d104b1311a887ed1b4ac4c35bbd13da8/librt-0.11.0-cp312-cp312-musllinux_1_2_aarch64.whl", hash = "sha256:bc3ce6b33c5828d9e80592011a5c584cb2ce86edbc4088405f70da47dc1d1b3b", size = 522268, upload-time = "2026-05-10T18:16:01.708Z" }, + { url = "https://files.pythonhosted.org/packages/b6/02/5720f5697a7f54b78b3aefbe20df3a48cedcff1276618c4aa481177942ed/librt-0.11.0-cp312-cp312-musllinux_1_2_i686.whl", hash = "sha256:936c5995f3514a42111f20099397d8177c79b4d7e70961e396c6f5a0a3566766", size = 527348, upload-time = "2026-05-10T18:16:03.496Z" }, + { url = "https://files.pythonhosted.org/packages/50/db/b4a47c6f91db4ff76348a0b3dd0cc65e090a078b765a810a62ff9434c3d3/librt-0.11.0-cp312-cp312-musllinux_1_2_riscv64.whl", hash = "sha256:9bc0ca6ad9381cbe8e4aa6e5726e4c80c78115a6e9723c599ed1d73e092bc49d", size = 516294, upload-time = "2026-05-10T18:16:05.173Z" }, + { url = "https://files.pythonhosted.org/packages/9e/58/9384b2f4eb1ed1d273d40948a7c5c4b2360213b402ef3be4641c06299f9c/librt-0.11.0-cp312-cp312-musllinux_1_2_x86_64.whl", hash = "sha256:070aa8c26c0a74774317a72df8851facc7f0f012a5b406557ac56992d92e1ec8", size = 553608, upload-time = "2026-05-10T18:16:06.839Z" }, + { url = "https://files.pythonhosted.org/packages/21/7b/5aa8848a7c6a9278c79375146da1812e695754ceec5f005e6043461a7315/librt-0.11.0-cp312-cp312-win32.whl", hash = "sha256:6bf14feb84b05ae945277395451998c89c54d0def4070eb5c08de544930b245a", size = 101879, upload-time = "2026-05-10T18:16:08.103Z" }, + { url = "https://files.pythonhosted.org/packages/37/33/8a745436944947575b584231750a41417de1a38cf6a2e9251d1065651c09/librt-0.11.0-cp312-cp312-win_amd64.whl", hash = "sha256:75672f0bc524ede266287d532d7923dbce94c7514ad07627bac3d0c6d92cc4d9", size = 119831, upload-time = "2026-05-10T18:16:09.174Z" }, + { url = "https://files.pythonhosted.org/packages/59/67/a6739ac96e28b7855808bdb0370e250606104a859750d209e5a0716fe7ab/librt-0.11.0-cp312-cp312-win_arm64.whl", hash = "sha256:2f10cf143e4a9bb0f4f5af568a00df94a2d69ef41c2579584454bb0fe5cc642c", size = 103470, upload-time = "2026-05-10T18:16:10.369Z" }, + { url = "https://files.pythonhosted.org/packages/82/61/e59168d4d0bf2bf90f4f0caf7a001bfc60254c3af4586013b04dc3ef517b/librt-0.11.0-cp313-cp313-macosx_10_13_x86_64.whl", hash = "sha256:78dc31f7fdfe9c9d0eb0e8f42d139db230e826415bbcabd9f0e9faaaee909894", size = 144119, upload-time = "2026-05-10T18:16:11.771Z" }, + { url = "https://files.pythonhosted.org/packages/61/fd/caa1d60b12f7dd79ccea23054e06eeaebe266a5f52c40a6b651069200ce5/librt-0.11.0-cp313-cp313-macosx_11_0_arm64.whl", hash = "sha256:fa475675db22290c3158e1d42326d0f5a65f04f44a0e68c3630a25b53560fb9c", size = 143565, upload-time = "2026-05-10T18:16:13.334Z" }, + { url = "https://files.pythonhosted.org/packages/b8/a9/dc744f5c2b4978d48db970be29f22716d3413d28b14ad99740817315cf2c/librt-0.11.0-cp313-cp313-manylinux2014_aarch64.manylinux_2_17_aarch64.manylinux_2_28_aarch64.whl", hash = "sha256:621db29691044bdeda22e789e482e1b0f3a985d90e3426c9c6d17606416205ea", size = 485395, upload-time = "2026-05-10T18:16:14.729Z" }, + { url = "https://files.pythonhosted.org/packages/8f/21/7f8e97a1e4dae952a5a95948f6f8507a173bc1e669f54340bba6ca1ca31b/librt-0.11.0-cp313-cp313-manylinux2014_i686.manylinux_2_17_i686.manylinux_2_28_i686.whl", hash = "sha256:a9010e2ed5b3a9e158c5fd966b3ab7e834bb3d3aacc8f66c91dd4b57a3799230", size = 479383, upload-time = "2026-05-10T18:16:16.321Z" }, + { url = "https://files.pythonhosted.org/packages/a6/6d/d8ee9c114bebf2c50e29ec2aa940826fccb62a645c3e4c18760987d0e16d/librt-0.11.0-cp313-cp313-manylinux2014_x86_64.manylinux_2_17_x86_64.manylinux_2_28_x86_64.whl", hash = "sha256:7c39513d8b7477a2e1ed8c43fc21c524e8d5a0f8d4e8b7b074dbdbe7820a08e2", size = 513010, upload-time = "2026-05-10T18:16:17.647Z" }, + { url = "https://files.pythonhosted.org/packages/f0/43/0b5708af2bd30a46400e72ba6bdaa8f066f15fb9a688527e34220e8d6c06/librt-0.11.0-cp313-cp313-manylinux_2_34_riscv64.manylinux_2_39_riscv64.whl", hash = "sha256:7aef3cf1d5af86e770ab04bfd993dfc4ae8b8c17f66fb77dd4a7d50de7bbb1a3", size = 508433, upload-time = "2026-05-10T18:16:19.309Z" }, + { url = "https://files.pythonhosted.org/packages/4a/50/356187247d09013490481033183b3532b58acf8028bcb34b2b56a375c9b2/librt-0.11.0-cp313-cp313-musllinux_1_2_aarch64.whl", hash = "sha256:557183ddc36babe46b27dd60facbd5adb4492181a5be887587d57cda6e092f21", size = 522595, upload-time = "2026-05-10T18:16:20.642Z" }, + { url = "https://files.pythonhosted.org/packages/40/e7/c6ac4240899c7f3248079d5a9900debe0dadb3fdeaf856684c987105ba47/librt-0.11.0-cp313-cp313-musllinux_1_2_i686.whl", hash = "sha256:83d3e1f72bd42f6c5c0b7daec530c3f829bd02db42c70b8ddf0c2d90a2459930", size = 527255, upload-time = "2026-05-10T18:16:22.352Z" }, + { url = "https://files.pythonhosted.org/packages/eb/b5/a81322dbeedeeaf9c1ee6f001734d28a09d8383ac9e6779bc24bbd0743c6/librt-0.11.0-cp313-cp313-musllinux_1_2_riscv64.whl", hash = "sha256:4ce1f21fbe589bc1afd7872dece84fb0e1144f794a288e58a10d2c54a55c43be", size = 516847, upload-time = "2026-05-10T18:16:23.627Z" }, + { url = "https://files.pythonhosted.org/packages/ae/66/6e6323787d592b55204a42595ff1102da5115601b53a7e9ddebc889a6da5/librt-0.11.0-cp313-cp313-musllinux_1_2_x86_64.whl", hash = "sha256:970b09f7044ea2b64c9da42fd3d335666518cfd1c6e8a182c95da73d0214b41e", size = 553920, upload-time = "2026-05-10T18:16:25.025Z" }, + { url = "https://files.pythonhosted.org/packages/9c/21/623f8ca230857102066d9ca8c6c1734995908c4d0d1bee7bb2ef0021cb33/librt-0.11.0-cp313-cp313-win32.whl", hash = "sha256:78fddc31cd4d3caa897ad5d31f856b1faadc9474021ad6cb182b9018793e254e", size = 101898, upload-time = "2026-05-10T18:16:26.649Z" }, + { url = "https://files.pythonhosted.org/packages/b3/1d/b4ebd44dd723f768469007515cb92251e0ae286c94c140f374801140fa74/librt-0.11.0-cp313-cp313-win_amd64.whl", hash = "sha256:8ca8aa88751a775870b764e93bad5135385f563cb8dcee399abf034ea4d3cb47", size = 119812, upload-time = "2026-05-10T18:16:27.859Z" }, + { url = "https://files.pythonhosted.org/packages/3b/e4/b2f4ca7965ca373b491cdb4bc25cdb30c1649ca81a8782056a83850292a9/librt-0.11.0-cp313-cp313-win_arm64.whl", hash = "sha256:96f044bb325fd9cf1a723015638c219e9143f0dfbc0ca54c565df2b7fc748b44", size = 103448, upload-time = "2026-05-10T18:16:29.066Z" }, + { url = "https://files.pythonhosted.org/packages/29/eb/dbce197da4e227779e56b5735f2decc3eb36e55a1cdbf1bd65d6639d76c1/librt-0.11.0-cp314-cp314-macosx_10_13_x86_64.whl", hash = "sha256:4a017a95e5837dc15a8c5661d60e05daa96b90908b1aa6b7acdf443cd25c8ebd", size = 143345, upload-time = "2026-05-10T18:16:30.674Z" }, + { url = "https://files.pythonhosted.org/packages/76/a3/254bebd0c11c8ba684018efb8006ff22e466abce445215cca6c778e7d9de/librt-0.11.0-cp314-cp314-macosx_11_0_arm64.whl", hash = "sha256:b1ecbd9819deccc39b7542bf4d2a740d8a620694d39989e58661d3763458f8d4", size = 143131, upload-time = "2026-05-10T18:16:32.037Z" }, + { url = "https://files.pythonhosted.org/packages/f1/3f/f77d6122d21ac7bf6ae8a7dfced1bd2a7ac545d3273ebdcaf8042f6d619f/librt-0.11.0-cp314-cp314-manylinux2014_aarch64.manylinux_2_17_aarch64.manylinux_2_28_aarch64.whl", hash = "sha256:7da327dacd7be8f8ec36547373550744a3cc0e536d54665cd83f8bcd961200e8", size = 477024, upload-time = "2026-05-10T18:16:33.493Z" }, + { url = "https://files.pythonhosted.org/packages/ac/0a/2c996dadebaa7d9bbbd43ef2d4f3e66b6da545f838a41694ef6172cebec8/librt-0.11.0-cp314-cp314-manylinux2014_i686.manylinux_2_17_i686.manylinux_2_28_i686.whl", hash = "sha256:0dc56b1f8d06e60db362cc3fdae206681817f86ce4725d34511473487f12a34b", size = 474221, upload-time = "2026-05-10T18:16:34.864Z" }, + { url = "https://files.pythonhosted.org/packages/0a/7e/f5d92af8486b8272c23b3e686b46ff72d89c8169585eb61eef01a2ac7147/librt-0.11.0-cp314-cp314-manylinux2014_x86_64.manylinux_2_17_x86_64.manylinux_2_28_x86_64.whl", hash = "sha256:05fb8fb2ab90e21c8d12ea240d744ad514da9baf381ebfa70d91d20d21713175", size = 505174, upload-time = "2026-05-10T18:16:36.705Z" }, + { url = "https://files.pythonhosted.org/packages/af/1a/cb0734fe86398eb33193ab753b7326255c74cac5eb09e76b9b16536e7adb/librt-0.11.0-cp314-cp314-manylinux_2_34_riscv64.manylinux_2_39_riscv64.whl", hash = "sha256:cae74872be221df4374d10fec61f93ed1513b9546ea84f2c0bf73ab3e9bd0b03", size = 497216, upload-time = "2026-05-10T18:16:38.418Z" }, + { url = "https://files.pythonhosted.org/packages/18/06/094820f91558b66e29943c0ec41c9914f460f48dd51fc503c3101e10842d/librt-0.11.0-cp314-cp314-musllinux_1_2_aarch64.whl", hash = "sha256:32bcc918c0148eb7e3d57385125bac7e5f9e4359d05f07448b09f6f778c2f31c", size = 513921, upload-time = "2026-05-10T18:16:39.848Z" }, + { url = "https://files.pythonhosted.org/packages/0b/c2/00de9018871a282f530cacb457d5ec0428f6ac7e6fedde9aff7468d9fb04/librt-0.11.0-cp314-cp314-musllinux_1_2_i686.whl", hash = "sha256:f9743fc99135d5f78d2454435615f6dec0473ca507c26ce9d92b10b562a280d3", size = 520850, upload-time = "2026-05-10T18:16:41.471Z" }, + { url = "https://files.pythonhosted.org/packages/51/9d/64631832348fd1834fb3a61b996434edddaaf25a31d03b0a76273159d2cf/librt-0.11.0-cp314-cp314-musllinux_1_2_riscv64.whl", hash = "sha256:5ba067f4aadae8fda802d91d2124c90c42195ff32d9161d3549e6d05cfe26f96", size = 504237, upload-time = "2026-05-10T18:16:43.15Z" }, + { url = "https://files.pythonhosted.org/packages/a5/ec/ae5525eb16edc827a044e7bb8777a455ff95d4bca9379e7e6bddd7383647/librt-0.11.0-cp314-cp314-musllinux_1_2_x86_64.whl", hash = "sha256:de3bf945454d032f9e390b85c4072e0a0570bf825421c8be0e71209fa65e1abe", size = 546261, upload-time = "2026-05-10T18:16:44.408Z" }, + { url = "https://files.pythonhosted.org/packages/5a/09/adce371f27ca039411da9659f7430fcc2ba6cd0c7b3e4467a0f091be7fa9/librt-0.11.0-cp314-cp314-win32.whl", hash = "sha256:d2277a05f6dcb9fd13db9566aac4fabd68c3ea1ea46ee5567d4eef8efa495a2f", size = 96965, upload-time = "2026-05-10T18:16:46.039Z" }, + { url = "https://files.pythonhosted.org/packages/d6/ee/8ac720d98548f173c7ce2e632a7ca94673f74cacd5c8162a84af5b35958a/librt-0.11.0-cp314-cp314-win_amd64.whl", hash = "sha256:ab73e8db5e3f564d812c1f5c3a175930a5f9bc96ccb5e3b22a34d7858b401cf7", size = 115151, upload-time = "2026-05-10T18:16:47.133Z" }, + { url = "https://files.pythonhosted.org/packages/94/20/c900cf14efeb09b6bef2b2dff20779f73464b97fd58d1c6bccc379588ae3/librt-0.11.0-cp314-cp314-win_arm64.whl", hash = "sha256:aea3caa317752e3a466fa8af45d91ee0ea8c7fdd96e42b0a8dd9b76a7931eba1", size = 98850, upload-time = "2026-05-10T18:16:48.597Z" }, + { url = "https://files.pythonhosted.org/packages/0c/71/944bfe4b64e12abffcd3c15e1cce07f72f3d55655083786285f4dedeb532/librt-0.11.0-cp314-cp314t-macosx_10_13_x86_64.whl", hash = "sha256:d1b36540d7aaf9b9101b3a6f376c8d8e9f7a9aec93ed05918f2c69d493ffef72", size = 151138, upload-time = "2026-05-10T18:16:49.839Z" }, + { url = "https://files.pythonhosted.org/packages/b6/10/99e64a5c86989357fda078c8143c533389585f6473b7439172dd8f3b3b2d/librt-0.11.0-cp314-cp314t-macosx_11_0_arm64.whl", hash = "sha256:efbb343ab2ce3540f4ecbe6315d677ed70f37cd9a72b1e58066c918ca83acbaa", size = 151976, upload-time = "2026-05-10T18:16:51.062Z" }, + { url = "https://files.pythonhosted.org/packages/21/31/5072ad880946d83e5ea4147d6d018c78eefce85b77819b19bdd0ee229435/librt-0.11.0-cp314-cp314t-manylinux2014_aarch64.manylinux_2_17_aarch64.manylinux_2_28_aarch64.whl", hash = "sha256:aa0dd688aab3f7914d3e6e5e3554978e0383312fb8e771d84be008a35b9ee548", size = 557927, upload-time = "2026-05-10T18:16:52.632Z" }, + { url = "https://files.pythonhosted.org/packages/5e/8d/70b5fb7cfbab60edbe7381614ab985da58e144fbf465c86d44c95f43cdca/librt-0.11.0-cp314-cp314t-manylinux2014_i686.manylinux_2_17_i686.manylinux_2_28_i686.whl", hash = "sha256:f5fb36b8c6c63fdcbb1d526d94c0d1331610d43f4118cc1beb4efef4f3faacb2", size = 539698, upload-time = "2026-05-10T18:16:53.934Z" }, + { url = "https://files.pythonhosted.org/packages/fa/a3/ba3495a0b3edbd24a4cae0d1d3c64f39a9fc45d06e812101289b50c1a619/librt-0.11.0-cp314-cp314t-manylinux2014_x86_64.manylinux_2_17_x86_64.manylinux_2_28_x86_64.whl", hash = "sha256:4a9a237d13addb93715b6fee74023d5ee3469b53fce527626c0e088aa585805f", size = 577162, upload-time = "2026-05-10T18:16:55.589Z" }, + { url = "https://files.pythonhosted.org/packages/f7/db/36e25fb81f99937ff1b96612a1dc9fd66f039cb9cc3aee12c01fac31aab9/librt-0.11.0-cp314-cp314t-manylinux_2_34_riscv64.manylinux_2_39_riscv64.whl", hash = "sha256:5ddd17bd87b2c56ddd60e546a7984a2e64c4e8eab92fb4cf3830a48ad5469d51", size = 566494, upload-time = "2026-05-10T18:16:56.975Z" }, + { url = "https://files.pythonhosted.org/packages/33/0d/3f622b47f0b013eeb9cf4cc07ae9bfe378d832a4eec998b2b209fe84244d/librt-0.11.0-cp314-cp314t-musllinux_1_2_aarch64.whl", hash = "sha256:bd43992b4473d42f12ff9e68326079f0696d9d4e6000e8f39a0238d482ba6ee2", size = 596858, upload-time = "2026-05-10T18:16:58.374Z" }, + { url = "https://files.pythonhosted.org/packages/a9/02/71b90bc93039c46a2000651f6ad60122b114c8f54c4ad306e0e96f5b75ad/librt-0.11.0-cp314-cp314t-musllinux_1_2_i686.whl", hash = "sha256:f8e3e8056dd674e279741485e2e512d6e9a751c7455809d0114e6ebf8d781085", size = 590318, upload-time = "2026-05-10T18:16:59.676Z" }, + { url = "https://files.pythonhosted.org/packages/04/04/418cb3f75621e2b761fb1ab0f017f4d70a1a72a6e7c74ee4f7e8d198c2f3/librt-0.11.0-cp314-cp314t-musllinux_1_2_riscv64.whl", hash = "sha256:c1f708d8ae9c56cf38a903c44297243d2ec83fd82b396b977e0144a3e76217e3", size = 575115, upload-time = "2026-05-10T18:17:01.007Z" }, + { url = "https://files.pythonhosted.org/packages/cc/2c/5a2183ac58dd911f26b5d7e7d7d8f1d87fcecdddd99d6c12169a258ff62c/librt-0.11.0-cp314-cp314t-musllinux_1_2_x86_64.whl", hash = "sha256:0add982e0e7b9fc14cf4b33789d5f13f66581889b88c2f58099f6ce8f92617bd", size = 617918, upload-time = "2026-05-10T18:17:02.682Z" }, + { url = "https://files.pythonhosted.org/packages/15/1f/dc6771a52592a4451be6effa200cbfc9cec61e4393d3033d81a9d307961d/librt-0.11.0-cp314-cp314t-win32.whl", hash = "sha256:2b481d846ac894c4e8403c5fd0e87c5d11d6499e404b474602508a224ff531c8", size = 103562, upload-time = "2026-05-10T18:17:03.99Z" }, + { url = "https://files.pythonhosted.org/packages/62/4a/7d1415567027286a75ba1093ec4aca11f073e0f559c530cf3e0a757ad55c/librt-0.11.0-cp314-cp314t-win_amd64.whl", hash = "sha256:28edb433edde181112a908c78907af28f964eabc15f4dd16c9d66c834302677c", size = 124327, upload-time = "2026-05-10T18:17:05.465Z" }, + { url = "https://files.pythonhosted.org/packages/ce/62/b40b382fa0c66fee1478073eb8db352a4a6beda4a1adccf1df911d8c289c/librt-0.11.0-cp314-cp314t-win_arm64.whl", hash = "sha256:dee008f20b542e3cd162ba338a7f9ec0f6d23d395f66fe8aeeec3c9d067ea253", size = 102572, upload-time = "2026-05-10T18:17:06.809Z" }, +] [[package]] name = "markdown-it-py" @@ -289,6 +399,59 @@ wheels = [ { url = "https://files.pythonhosted.org/packages/b3/38/89ba8ad64ae25be8de66a6d463314cf1eb366222074cfda9ee839c56a4b4/mdurl-0.1.2-py3-none-any.whl", hash = "sha256:84008a41e51615a49fc9966191ff91509e3c40b939176e643fd50a5c2196b8f8", size = 9979, upload-time = "2022-08-14T12:40:09.779Z" }, ] +[[package]] +name = "mypy" +version = "2.1.0" +source = { registry = "https://pypi.org/simple" } +dependencies = [ + { name = "ast-serialize" }, + { name = "librt", marker = "platform_python_implementation != 'PyPy'" }, + { name = "mypy-extensions" }, + { name = "pathspec" }, + { name = "typing-extensions" }, +] +sdist = { url = "https://files.pythonhosted.org/packages/82/15/cca9d88503549ed6fedeaa1d448cdddd542ee8a490232d732e278036fbf2/mypy-2.1.0.tar.gz", hash = "sha256:81e76ad12c2d804512e9b13240d1588316531bfba07558286078bfbce9613633", size = 3898359, upload-time = "2026-05-11T18:37:36.237Z" } +wheels = [ + { url = "https://files.pythonhosted.org/packages/95/b1/55861beb5c339b44f9a2ba92df9e2cb1eeb4ae1eee674cdf7772c797778b/mypy-2.1.0-cp312-cp312-macosx_10_13_x86_64.whl", hash = "sha256:244358bf1c0da7722230bce60683d52e8e9fd030554926f15b747a84efb5b3af", size = 14874381, upload-time = "2026-05-11T18:37:31.784Z" }, + { url = "https://files.pythonhosted.org/packages/0b/b3/b7f770114b7d0ac92d0f76e8d93c2780844a70488a90e91821927850da86/mypy-2.1.0-cp312-cp312-macosx_11_0_arm64.whl", hash = "sha256:4ec7c57657493c7a75534df2751c8ae2cda383c16ecc55d2106c54476b1b16f6", size = 13665501, upload-time = "2026-05-11T18:34:23.063Z" }, + { url = "https://files.pythonhosted.org/packages/b6/f3/8ae2037967e2126689a0c11d99e2b707134a565191e92c60ca2572aec60a/mypy-2.1.0-cp312-cp312-manylinux2014_aarch64.manylinux_2_17_aarch64.manylinux_2_28_aarch64.whl", hash = "sha256:d8161b6ff4392410023224f0969d17db93e1e154bc3e4ba62598e720723ae211", size = 14045750, upload-time = "2026-05-11T18:31:48.151Z" }, + { url = "https://files.pythonhosted.org/packages/a0/32/615eb5911859e43d054941b0d0a7d06cfa2870eba86529cf385b052b111c/mypy-2.1.0-cp312-cp312-manylinux2014_x86_64.manylinux_2_17_x86_64.manylinux_2_28_x86_64.whl", hash = "sha256:bf03e12003084a67395184d3eb8cbd6a489dc3655b5664b28c210a9e2403ab0b", size = 15061630, upload-time = "2026-05-11T18:37:06.898Z" }, + { url = "https://files.pythonhosted.org/packages/d4/03/4eafbfff8bfab1b87082741eae6e6a624028c984e6708b73bce2a8570c9d/mypy-2.1.0-cp312-cp312-musllinux_1_2_x86_64.whl", hash = "sha256:20509760fd791c51579d573153407d226385ec1f8bcce55d730b354f3336bc22", size = 15288831, upload-time = "2026-05-11T18:31:18.07Z" }, + { url = "https://files.pythonhosted.org/packages/99/ee/919661478e5891a3c96e549c036e467e64563ab85995b10c53c8358e16a3/mypy-2.1.0-cp312-cp312-win_amd64.whl", hash = "sha256:6753d0c1fdd6b1a23b9e4f283ce80b2153b724adcb2653b20b85a8a28ac6436b", size = 11135228, upload-time = "2026-05-11T18:34:31.23Z" }, + { url = "https://files.pythonhosted.org/packages/24/0a/6a12b9782ca0831a553192f351679f4548abc9d19a7cc93bb7feb02084c7/mypy-2.1.0-cp312-cp312-win_arm64.whl", hash = "sha256:98ebb6589bb3b6d0c6f0c459d53ca55b8091fbc13d277c4041c885392e8195e8", size = 10040684, upload-time = "2026-05-11T18:36:48.199Z" }, + { url = "https://files.pythonhosted.org/packages/6e/dd/c7191469c777f07689c032a8f7326e393ea34c92d6d76eb7ce5ba57ea66d/mypy-2.1.0-cp313-cp313-macosx_10_13_x86_64.whl", hash = "sha256:35aac3bb114e03888f535d5eb51b8bafbb3266586b599da1940f9b1be3ec5bd5", size = 14852174, upload-time = "2026-05-11T18:31:38.929Z" }, + { url = "https://files.pythonhosted.org/packages/55/8c/aed55408879043d72bb9135f4d0d19a02b886dd569631e113e3d2706cb8d/mypy-2.1.0-cp313-cp313-macosx_11_0_arm64.whl", hash = "sha256:8de55a8c861f2a49331f807be98d90caeceeef520bde13d43a160207f8af613e", size = 13651542, upload-time = "2026-05-11T18:36:04.636Z" }, + { url = "https://files.pythonhosted.org/packages/3a/8e/f371a824b1f1fa8ea6e3dbb8703d232977d572be2329554a3bc4d960302f/mypy-2.1.0-cp313-cp313-manylinux2014_aarch64.manylinux_2_17_aarch64.manylinux_2_28_aarch64.whl", hash = "sha256:5fdf2941a07434af755837d9880f7d7d25f1dacb1af9dcd4b9b66f2220a3024e", size = 14033929, upload-time = "2026-05-11T18:35:55.742Z" }, + { url = "https://files.pythonhosted.org/packages/94/21/f54be870d6dd53a82c674407e0f8eed7174b05ec78d42e5abd7b42e84fd5/mypy-2.1.0-cp313-cp313-manylinux2014_x86_64.manylinux_2_17_x86_64.manylinux_2_28_x86_64.whl", hash = "sha256:e195b817c13f02352a9c124301f9f30f078405444679b6753c1b96b6eed37285", size = 15039200, upload-time = "2026-05-11T18:33:10.281Z" }, + { url = "https://files.pythonhosted.org/packages/17/99/bf21748626a40ce59fd29a39386ab46afec88b7bd2f0fa6c3a97c995523f/mypy-2.1.0-cp313-cp313-musllinux_1_2_x86_64.whl", hash = "sha256:5431d42af987ebd92ba2f71d45c85ed41d8e6ca9f5fd209a69f68f707d2469e5", size = 15272690, upload-time = "2026-05-11T18:32:07.205Z" }, + { url = "https://files.pythonhosted.org/packages/d6/d7/9e90d2cf47100bea550ed2bc7b0d4de3a62181d84d5e37da0003e8462637/mypy-2.1.0-cp313-cp313-win_amd64.whl", hash = "sha256:767fe8c66dc3e01e19e1737d4c38ebefead16125e1b8e58ad421903b376f5c65", size = 11147435, upload-time = "2026-05-11T18:33:56.477Z" }, + { url = "https://files.pythonhosted.org/packages/ec/46/e5c449e858798e35ffc90946282a27c62a77be743fe17480e4977374eb91/mypy-2.1.0-cp313-cp313-win_arm64.whl", hash = "sha256:ecfe70d43775ab99562ab128ce49854a362044c9f894961f68f898c23cb7429d", size = 10035052, upload-time = "2026-05-11T18:32:30.049Z" }, + { url = "https://files.pythonhosted.org/packages/b0/ca/b279a672e874aedd5498ae25f722dacc8aa86bbffb939b3f97cbb1cf6686/mypy-2.1.0-cp314-cp314-macosx_10_15_x86_64.whl", hash = "sha256:7354c5a7f69d9345c3d6e69921d57088eea3ddeeb6b20d34c1b3855b02c36ec2", size = 14848422, upload-time = "2026-05-11T18:35:45.984Z" }, + { url = "https://files.pythonhosted.org/packages/27/e6/3efe56c631d959b9b4454e208b0ac4b7f4f58b404c89f8bec7b49efdfc21/mypy-2.1.0-cp314-cp314-macosx_11_0_arm64.whl", hash = "sha256:49890d4f76ac9e06ec117f9e09f3174da70a620a0c300953d8595c926e80947f", size = 13677374, upload-time = "2026-05-11T18:36:57.188Z" }, + { url = "https://files.pythonhosted.org/packages/84/7f/8107ea87a44fd1f1b59882442f033c9c3488c127201b1d1d15f1cbd6022e/mypy-2.1.0-cp314-cp314-manylinux2014_aarch64.manylinux_2_17_aarch64.manylinux_2_28_aarch64.whl", hash = "sha256:761be68e023ef5d94678772396a8af1220030f80837a3afd8d0aef3b419666f4", size = 14055743, upload-time = "2026-05-11T18:35:18.361Z" }, + { url = "https://files.pythonhosted.org/packages/51/4d/b6d34db183133b83761b9199a82d31557cdbb70a380d8c3b3438e11882a3/mypy-2.1.0-cp314-cp314-manylinux2014_x86_64.manylinux_2_17_x86_64.manylinux_2_28_x86_64.whl", hash = "sha256:c90345fc182dc363b891350457ec69c35140858538f38b4540845afcc32b1aef", size = 15020937, upload-time = "2026-05-11T18:34:59.618Z" }, + { url = "https://files.pythonhosted.org/packages/ff/d7/f08360c691d758acb02f45022c34d98b92892f4ea756644e1000d4b9f3d8/mypy-2.1.0-cp314-cp314-musllinux_1_2_x86_64.whl", hash = "sha256:b84802e7b5a6daf1f5e15bc9fcd7ddae77be13981ffab037f1c67bb84d67d135", size = 15253371, upload-time = "2026-05-11T18:36:41.081Z" }, + { url = "https://files.pythonhosted.org/packages/67/1b/09460a13719530a19bce27bd3bc8449e83569dd2ba7faf51c9c3c30c0b61/mypy-2.1.0-cp314-cp314-win_amd64.whl", hash = "sha256:022c771234936ceac541ebaf836fe9e2abeb3f5e09aff21588fe543ff006fe21", size = 11326429, upload-time = "2026-05-11T18:34:13.526Z" }, + { url = "https://files.pythonhosted.org/packages/40/62/75dbf0f82f7b6680340efc614af29dd0b3c17b8a4f1cd09b8bd2fd6bc814/mypy-2.1.0-cp314-cp314-win_arm64.whl", hash = "sha256:498207db725cec88829a6a5c2fc771205fd043719ef98bc49aba8fb9fc4e6d57", size = 10218799, upload-time = "2026-05-11T18:32:23.491Z" }, + { url = "https://files.pythonhosted.org/packages/b2/66/caca04ed7d972fb6eb6dd1ccd6df1de5c38fae8c5b3dc1c4e8e0d85ee6b9/mypy-2.1.0-cp314-cp314t-macosx_10_15_x86_64.whl", hash = "sha256:7d5e5cad0efeba72b93cd17490cc0d69c5ac9ca132994fe3fb0314808aeeb83e", size = 15923458, upload-time = "2026-05-11T18:35:28.64Z" }, + { url = "https://files.pythonhosted.org/packages/ed/52/2d90cbe49d014b13ed7ff337930c30bad35893fe38a1e4641e756bb62191/mypy-2.1.0-cp314-cp314t-macosx_11_0_arm64.whl", hash = "sha256:ff715050c127d724fd260a2e666e7747fdd83511c0c47d449d98238970aef780", size = 14757697, upload-time = "2026-05-11T18:36:14.208Z" }, + { url = "https://files.pythonhosted.org/packages/ac/37/d98f4a14e081b238992d0ed96b6d39c7cc0148c9699eb71eaa68629665ea/mypy-2.1.0-cp314-cp314t-manylinux2014_aarch64.manylinux_2_17_aarch64.manylinux_2_28_aarch64.whl", hash = "sha256:82208da9e09414d520e912d3e462d454854bed0810b71540bb016dcbca7308fd", size = 15405638, upload-time = "2026-05-11T18:33:48.249Z" }, + { url = "https://files.pythonhosted.org/packages/a3/c2/15c46613b24a84fad2aea1248bf9619b99c2767ae9071fe224c179a0b7d4/mypy-2.1.0-cp314-cp314t-manylinux2014_x86_64.manylinux_2_17_x86_64.manylinux_2_28_x86_64.whl", hash = "sha256:e79ebc1b904b84f0310dff7469655a9c36c7a68bddb37bdd42b67a332df61d08", size = 16215852, upload-time = "2026-05-11T18:32:50.296Z" }, + { url = "https://files.pythonhosted.org/packages/5c/90/9c16a57f482c76d25f6379762b56bbf65c711d8158cf271fb2802cfb0640/mypy-2.1.0-cp314-cp314t-musllinux_1_2_x86_64.whl", hash = "sha256:e583edc957cfb0deb142079162ae826f58449b116c1d442f2d91c69d9fced081", size = 16452695, upload-time = "2026-05-11T18:33:38.182Z" }, + { url = "https://files.pythonhosted.org/packages/0f/4c/215a4eeb63cacc5f17f516691ea7285d11e249802b942476bff15922a314/mypy-2.1.0-cp314-cp314t-win_amd64.whl", hash = "sha256:b33b6cd332695bba180d55e717a79d3038e479a2c49cc5eb3d53603409b9a5d7", size = 12866622, upload-time = "2026-05-11T18:34:39.945Z" }, + { url = "https://files.pythonhosted.org/packages/4b/50/1043e1db5f455ffe4c9ab22747cd8ca2bc492b1e4f4e21b130a44ee2b217/mypy-2.1.0-cp314-cp314t-win_arm64.whl", hash = "sha256:4f910fe825376a7b66ef7ca8c98e5a149e8cd64c19ae71d84047a74ee060d4e6", size = 10610798, upload-time = "2026-05-11T18:36:31.444Z" }, + { url = "https://files.pythonhosted.org/packages/0d/2a/13ca1f292f6db1b98ff495ef3467736b331621c5917cad984b7043e7348d/mypy-2.1.0-py3-none-any.whl", hash = "sha256:a663814603a5c563fb87a4f96fb473eeb30d1f5a4885afcf44f9db000a366289", size = 2693302, upload-time = "2026-05-11T18:31:29.246Z" }, +] + +[[package]] +name = "mypy-extensions" +version = "1.1.0" +source = { registry = "https://pypi.org/simple" } +sdist = { url = "https://files.pythonhosted.org/packages/a2/6e/371856a3fb9d31ca8dac321cda606860fa4548858c0cc45d9d1d4ca2628b/mypy_extensions-1.1.0.tar.gz", hash = "sha256:52e68efc3284861e772bbcd66823fde5ae21fd2fdb51c62a211403730b916558", size = 6343, upload-time = "2025-04-22T14:54:24.164Z" } +wheels = [ + { url = "https://files.pythonhosted.org/packages/79/7b/2c79738432f5c924bef5071f933bcc9efd0473bac3b4aa584a6f7c1c8df8/mypy_extensions-1.1.0-py3-none-any.whl", hash = "sha256:1be4cccdb0f2482337c4743e60421de3a356cd97508abadd57d47403e94f5505", size = 4963, upload-time = "2025-04-22T14:54:22.983Z" }, +] + [[package]] name = "myst-parser" version = "5.1.0" @@ -315,6 +478,15 @@ wheels = [ { url = "https://files.pythonhosted.org/packages/df/b2/87e62e8c3e2f4b32e5fe99e0b86d576da1312593b39f47d8ceef365e95ed/packaging-26.2-py3-none-any.whl", hash = "sha256:5fc45236b9446107ff2415ce77c807cee2862cb6fac22b8a73826d0693b0980e", size = 100195, upload-time = "2026-04-24T20:15:22.081Z" }, ] +[[package]] +name = "pathspec" +version = "1.1.1" +source = { registry = "https://pypi.org/simple" } +sdist = { url = "https://files.pythonhosted.org/packages/5a/82/42f767fc1c1143d6fd36efb827202a2d997a375e160a71eb2888a925aac1/pathspec-1.1.1.tar.gz", hash = "sha256:17db5ecd524104a120e173814c90367a96a98d07c45b2e10c2f3919fff91bf5a", size = 135180, upload-time = "2026-04-27T01:46:08.907Z" } +wheels = [ + { url = "https://files.pythonhosted.org/packages/f1/d9/7fb5aa316bc299258e68c73ba3bddbc499654a07f151cba08f6153988714/pathspec-1.1.1-py3-none-any.whl", hash = "sha256:a00ce642f577bf7f473932318056212bc4f8bfdf53128c78bbd5af0b9b20b189", size = 57328, upload-time = "2026-04-27T01:46:07.06Z" }, +] + [[package]] name = "pluggy" version = "1.6.0" @@ -428,6 +600,31 @@ wheels = [ { url = "https://files.pythonhosted.org/packages/04/54/6f679c435d28e0a568d8e8a7c0a93a09010818634c3c3907fc98d8983770/roman_numerals-4.1.0-py3-none-any.whl", hash = "sha256:647ba99caddc2cc1e55a51e4360689115551bf4476d90e8162cf8c345fe233c7", size = 7676, upload-time = "2025-12-17T18:25:33.098Z" }, ] +[[package]] +name = "ruff" +version = "0.15.14" +source = { registry = "https://pypi.org/simple" } +sdist = { url = "https://files.pythonhosted.org/packages/dc/8a/8bce2894573e9dae6ff4d77fe34ad727d79b9e6238ad288c5638990d90f6/ruff-0.15.14.tar.gz", hash = "sha256:48e866b165be4a9bdbf310f7d3c9a07edef2fe8cd63ffeb4e00bb590506ebf9f", size = 4700910, upload-time = "2026-05-21T14:34:55.177Z" } +wheels = [ + { url = "https://files.pythonhosted.org/packages/b9/c8/74a92c6ff9fcfb4f1f947126d3ebee8389276e161ecc85de5bda7cda51bd/ruff-0.15.14-py3-none-linux_armv6l.whl", hash = "sha256:8dd2db9416e487c8d4b01fa7056bb02c4d05969d4f8d17a08c229c2f4ff3c108", size = 10739177, upload-time = "2026-05-21T14:34:37.332Z" }, + { url = "https://files.pythonhosted.org/packages/45/91/254a35c20acc38a7223c9d2d594af12e794432464f2cdeb52af1dc4a892d/ruff-0.15.14-py3-none-macosx_10_12_x86_64.whl", hash = "sha256:be4ff55af755bd71a00ab3dc6bd7ffc467bd76e0df6881e286c2e3d23e8fb43b", size = 11144969, upload-time = "2026-05-21T14:34:43.978Z" }, + { url = "https://files.pythonhosted.org/packages/56/9e/d13e40f83b8d0a94430e6778ce1d94a43b38cf2efe63278bdd2b4c65abbf/ruff-0.15.14-py3-none-macosx_11_0_arm64.whl", hash = "sha256:48d5909d7d06276ce7dde6d32bfa4b0d4cb2651145cd8ee4b440722cbc77832f", size = 10478207, upload-time = "2026-05-21T14:34:48.378Z" }, + { url = "https://files.pythonhosted.org/packages/8d/f1/b15a7839fa4f332f8acec78e20564f26bb2d866e3d21710b877fd0263000/ruff-0.15.14-py3-none-manylinux_2_17_aarch64.manylinux2014_aarch64.whl", hash = "sha256:ca8cbfa94c4f90984a67561978602746d4cd27103568f745fa90eee3f0d4107d", size = 10818459, upload-time = "2026-05-21T14:34:22.318Z" }, + { url = "https://files.pythonhosted.org/packages/45/33/53d651177f84f94b400a0e27f8824eeada3dddc9d5ee8aeb048f4352a520/ruff-0.15.14-py3-none-manylinux_2_17_armv7l.manylinux2014_armv7l.whl", hash = "sha256:9a6bbc0333f1ab053423bcbf6226477d266ca7cec7738c4c8e3f55647803f3c4", size = 10541800, upload-time = "2026-05-21T14:34:20.209Z" }, + { url = "https://files.pythonhosted.org/packages/b8/a6/868f87e0bf9786ed24b5d0d0ad8676b8a94fd1912f42cddf9cfc7857818a/ruff-0.15.14-py3-none-manylinux_2_17_i686.manylinux2014_i686.whl", hash = "sha256:8a24a4f7605d7003a6674d4387651effd939dead3fddd0f36561eb77a9a2e542", size = 11342149, upload-time = "2026-05-21T14:34:46.365Z" }, + { url = "https://files.pythonhosted.org/packages/a7/8b/38cd5c19faffdcc05a408d2b78edccc69492ab9720eadb49ea15ef80d768/ruff-0.15.14-py3-none-manylinux_2_17_ppc64le.manylinux2014_ppc64le.whl", hash = "sha256:049b5326e53ed80978f2fc041a280603f69dd6b0c95464342a2bb4572d9d9e2f", size = 12212563, upload-time = "2026-05-21T14:34:28.579Z" }, + { url = "https://files.pythonhosted.org/packages/3e/4d/a3c5b874a556d5731e3e657aaf04311bb76f0a5c3ec220ed43051be6b64b/ruff-0.15.14-py3-none-manylinux_2_17_s390x.manylinux2014_s390x.whl", hash = "sha256:d4ed42e6696c8dfa5f06728e6441993901f548eb92d73bc472cb5a38d1395fbf", size = 11493299, upload-time = "2026-05-21T14:34:41.836Z" }, + { url = "https://files.pythonhosted.org/packages/1e/c0/56472c251d09858a53e51efbd485b09e1995d8731668b76d52e5dd6ee0f1/ruff-0.15.14-py3-none-manylinux_2_17_x86_64.manylinux2014_x86_64.whl", hash = "sha256:715c543cf450c4888251f91c52f1942a800541d9bddd7ac060aa4e6b77ae7cba", size = 11455931, upload-time = "2026-05-21T14:34:57.276Z" }, + { url = "https://files.pythonhosted.org/packages/2c/4a/e2e7b4d8dbf233d4eace59c75bc3435fa6d8bd3bae82d351d4e4300c0fd1/ruff-0.15.14-py3-none-manylinux_2_31_riscv64.whl", hash = "sha256:72ebab6013ec887d439d8b7593737a0a4ffb06d45d209d4e4bf2e92813082d3f", size = 11400794, upload-time = "2026-05-21T14:34:39.773Z" }, + { url = "https://files.pythonhosted.org/packages/97/c7/83c0539fe34c3e09136204d1e75d6052492364e0b3cb05e9465423f567d7/ruff-0.15.14-py3-none-musllinux_1_2_aarch64.whl", hash = "sha256:49072d36abdbe97a8dd7f480afe9c675699c0c495d4c84076e2c1203c4550581", size = 10804759, upload-time = "2026-05-21T14:34:31.045Z" }, + { url = "https://files.pythonhosted.org/packages/86/a6/18f2bfc095a2ab4a78745644e428205532ce6653a5d0fa8501572891534d/ruff-0.15.14-py3-none-musllinux_1_2_armv7l.whl", hash = "sha256:958522aee105068640c2c2ceae08f413ae44d922f52a1374ac13d6a96032fc93", size = 10539517, upload-time = "2026-05-21T14:34:53.064Z" }, + { url = "https://files.pythonhosted.org/packages/54/3a/5a8b3b69c654d4e4bf1d246ac5b49cbcdac6eaab6905925f8915f31e3b80/ruff-0.15.14-py3-none-musllinux_1_2_i686.whl", hash = "sha256:f3707da619a143a2e8830e2abab8224478d69ace2d28cb6c20543ae97c36bf61", size = 11065169, upload-time = "2026-05-21T14:34:24.484Z" }, + { url = "https://files.pythonhosted.org/packages/ed/c5/8864e4e7925b836ea354b31d57641ec03830564e281a8b6f061f8c3e0ec1/ruff-0.15.14-py3-none-musllinux_1_2_x86_64.whl", hash = "sha256:bb01d645694e3ec0102105d07ef2d53703970407d59c04e59d3ba0b7a1d53553", size = 11560214, upload-time = "2026-05-21T14:34:50.975Z" }, + { url = "https://files.pythonhosted.org/packages/36/38/012bf76752e1f89ed50b77b99532d90f3a3e287bc7918e1fc0948ac866ac/ruff-0.15.14-py3-none-win32.whl", hash = "sha256:6d0c1ad2a0ab718d39b6d8fd2217981ce4d625cd96a720095f798fb47d8b13e6", size = 10805548, upload-time = "2026-05-21T14:34:33.453Z" }, + { url = "https://files.pythonhosted.org/packages/d1/b7/4ea2c170f10ad760fff2a5250beb18897719dc8b52b53a24cddbb9dd3f19/ruff-0.15.14-py3-none-win_amd64.whl", hash = "sha256:802342981e056db3851a7836e5b070f8f15f67d4a685ae2a6160939d364b2902", size = 11939523, upload-time = "2026-05-21T14:34:18.077Z" }, + { url = "https://files.pythonhosted.org/packages/62/d5/bc97ff895ec35cf3925d4bd60f3b39d822f377a446906ec9bcc87405e59b/ruff-0.15.14-py3-none-win_arm64.whl", hash = "sha256:ff47b90a9ef6a40c9e2f3b479c1fb78531adf055b94c1eba0a7ba04b31951826", size = 11208607, upload-time = "2026-05-21T14:34:26.525Z" }, +] + [[package]] name = "snowballstemmer" version = "3.0.1" @@ -557,6 +754,15 @@ wheels = [ { url = "https://files.pythonhosted.org/packages/52/a7/d2782e4e3f77c8450f727ba74a8f12756d5ba823d81b941f1b04da9d033a/sphinxcontrib_serializinghtml-2.0.0-py3-none-any.whl", hash = "sha256:6e2cb0eef194e10c27ec0023bfeb25badbbb5868244cf5bc5bdc04e4464bf331", size = 92072, upload-time = "2024-07-29T01:10:08.203Z" }, ] +[[package]] +name = "typing-extensions" +version = "4.15.0" +source = { registry = "https://pypi.org/simple" } +sdist = { url = "https://files.pythonhosted.org/packages/72/94/1a15dd82efb362ac84269196e94cf00f187f7ed21c242792a923cdb1c61f/typing_extensions-4.15.0.tar.gz", hash = "sha256:0cea48d173cc12fa28ecabc3b837ea3cf6f38c6d1136f85cbaaf598984861466", size = 109391, upload-time = "2025-08-25T13:49:26.313Z" } +wheels = [ + { url = "https://files.pythonhosted.org/packages/18/67/36e9267722cc04a6b9f15c7f3441c2363321a3ea07da7ae0c0707beb2a9c/typing_extensions-4.15.0-py3-none-any.whl", hash = "sha256:f0fa19c6845758ab08074a0cfa8b7aecb71c999ca73d62883bc25cc018c4e548", size = 44614, upload-time = "2025-08-25T13:49:24.86Z" }, +] + [[package]] name = "urllib3" version = "2.6.3"