Verifying sympy.geometry

This chapter walks through the bundled sympy_geometry.deppy sidecar — a complete, runnable verification of properties of sympy.geometry's Point / Segment / Triangle / Polygon / Circle classes, without modifying a single line of SymPy's source code.

python -m deppy.pipeline.run_verify sympy_geometry.deppy --out sympy_geometry.lean

What's in the sidecar

The sympy_geometry.deppy file lays out the trust chain: foundations (generic mathematical facts) → sidecar axioms (claims about sympy.geometry's behaviour) → verify blocks (kernel-checked properties of named methods) → proofs (compositions citing the foundations and axioms).

A taste of the file

Foundations come first — admitted on user authority, but several get checked by Z3:

# sympy_geometry.deppy — foundations (excerpt)
foundation Real_sqrt_nonneg: "sqrt(x) >= 0 when x >= 0"
foundation Real_sqrt_sq_nonneg: "sqrt(x)**2 == x when x >= 0"
foundation Real_sub_sq_swap: "(a - b)**2 == (b - a)**2"
foundation Real_add_comm: "a + b == b + a"
foundation Real_avg_minus_endpoints: "2*a - (a + b) == a - b"

Next, the spec block for sympy.geometry.point.Point lists axioms about its distance and collinearity behaviour:

# sympy_geometry.deppy — Point spec (excerpt)
spec sympy.geometry.point.Point:
  guarantee: "Euclidean distance is a metric on R²; collinearity is the vanishing cross product"
  pure: true
  axiom dist_nonneg: "Point.distance(p, q) >= 0"
  axiom dist_zero_iff_equal: "(Point.distance(p, q) == 0) == (p == q)"
  axiom dist_symmetric: "Point.distance(p, q) == Point.distance(q, p)"
  axiom dist_pythagoras: "Point.distance(p, q)**2 == (p.x - q.x)**2 + (p.y - q.y)**2"
  axiom collinear_iff_zero_cross: "is_collinear(A, B, C) == ((B.x-A.x)*(C.y-A.y) == (C.x-A.x)*(B.y-A.y))"

Verify blocks pin properties to specific live methods so the kernel can run them:

# sympy_geometry.deppy — verify blocks (excerpt)
verify dist_nonneg_code:
  function: sympy.geometry.point.Point.distance
  property: "Point.distance(p, q) >= 0"
  via: foundation Real_sqrt_nonneg
  fibration: isinstance Point
  cubical: true

verify circle_radius_eq_code:
  function: sympy.geometry.ellipse.Circle.radius
  property: "Circle(c, r).radius == r"
  via: foundation Real_add_comm
  # NB: this claim is *false* under placeholder semantics —
  # Z3 counterexample search rejects it; the certificate
  # omits the theorem and reports it in the audit summary.

The last verify block exercises PSDL, the Python-syntax tactic language whose body becomes a deppy ProofTerm tree (kernel-verified) plus a Lean tactic (best-effort documentation):

# sympy_geometry.deppy — PSDL block
verify dist_nonneg_psdl:
  function: sympy.geometry.point.Point.distance
  property: "Point.distance(p, q) >= 0"
  via: foundation Real_sqrt_nonneg
  binders: p: Point, q: Point
  psdl_proof: |
    if isinstance(other, Point):
        # body returns sqrt(sum_zip_sub_sq(self, other))
        inline(Point.distance, sqrt(sum_zip_sub_sq(self, other)))
        apply(Real_sqrt_nonneg)
        assert sum_zip_sub_sq(self, other) >= 0, "z3"
    else:
        raise NotImplementedError  # exception fibre — vacuous

What the pipeline does

python -m deppy.pipeline.run_verify sympy_geometry.deppy runs every step in order; each step is real (no metadata stubs) and recorded in the JSON sidecar emitted alongside the .lean file:

Highlight: the PSDL block

verify dist_nonneg_psdl is the only verify block with a psdl_proof: body. PSDL — the Python-Semantic Deppy Language — lets you write the proof in literal Python with a small library of cubical-flavoured primitives. See Part 5: PSDL for the full reference.

Each PSDL line maps to a deppy ProofTerm subclass and a Lean tactic line:

The deppy kernel verifies the resulting ProofTerm tree independently of Lean — so when Lean's elaborator can't follow a PSDL idiom (isinstance other Point isn't a Lean predicate), the deppy verdict still holds and the Lean side falls back to a synthesised unfold + first | rfl | omega | … closer.

Highlight: a real false claim caught at run-time

verify circle_radius_eq_code claims Circle(c, r).radius == r. Mathematically true for a real Circle, but under deppy's placeholder mechanization (Circle_radius : Int → Int → Int defined as constantly 0), the claim becomes 0 = r — false for r ≠ 0. The per-verify counterexample search catches it:

verify circle_radius_eq_code — REJECTED
  property: Circle(c, r).radius == r
  Z3 found a counterexample showing this claim is
  false under the placeholder semantics:
    after placeholder substitution ``0 == r``: With r=1: 0 == r → False
    (real counterexample — claim is provably false)
  No theorem emitted; the block is reported in the audit
  summary as ``rejected``.

The kernel's structural ProofTerm tree (Unfold(Circle_radius, AxiomInvocation(Real_add_comm))) type-checks — that's the kernel rubber-stamping the shape. The Z3 search is the second gate that demands the shape actually entail the claim under some interpretation. When placeholder semantics expose a contradiction, the certificate refuses to admit the theorem and records the rejection. This is the system catching itself.

Architecture diagram

sympy_geometry.deppy          run_verify pipeline
┌──────────────────┐          ┌──────────────────────────────┐
│ foundation R…    │          │ 1. Foundation Z3 discharge   │
│ spec Point:      │          │ 2. Counterexample search      │
│   axiom dist…    │──parse──▶│ 3. Mechanize to Lean Props   │
│ verify NAME:     │          │ 4. Body translate (live src) │
│   psdl_proof: |  │          │ 5. ProofKernel.verify        │
│ proof T: by:…    │          │ 6. Per-verify counterexample │
└──────────────────┘          │ 7. Lean certificate emit     │
                              │ 8. lean round-trip           │
                              │ 9. JSON sidecar emit         │
                              │10. certify_or_die            │
                              └──────────────────────────────┘
                                        │
                                        ▼
                        ┌────────────────────────────────┐
                        │ 11/11 verify blocks      ✓    │
                        │ 38/38 axioms mechanized   ✓    │
                        │ 6/14 foundations Z3       ✓    │
                        │ Lean round-trip OK        ✓    │
                        │ ✓ CERTIFIED                    │
                        └────────────────────────────────┘

Full Output

Running the verification produces:

$ python -m deppy.pipeline.run_verify sympy_geometry.deppy --out sympy_geometry.lean

  ...
  Foundations:
    foundations / Z3-attempted / verified:  14 / 10 / 7
  Counterexample search:
    foundations attempted / counterexamples: 3 / 0
  Subsystem invocations (B1–B16 audit batch):
    invoked / successful:                   45 / 44
  ProofTerm subclasses (C1–C7 audit batch):
    constructed / kernel-accepted:          38 / 27
  ``verify`` blocks (.deppy → kernel.verify):
    accepted by ProofKernel.verify:         11 / 11
  Specs (informational):                    5
  Proofs total:                             45
    derived (real proof bodies):            20
    cited  (renaming of trusted axioms):    25
    sorry  (unrecognised by-clause):        0
  ────────────────────────────────────────────────────────────
  deppy.lean.lean_runner round-trip:        OK
  ────────────────────────────────────────────────────────────
  ✓ CERTIFIED — top-level certify_or_die: PASS
  ════════════════════════════════════════════════════════════
  Certificate at: sympy_geometry.lean
  JSON sidecar:   sympy_geometry.json

Exercises