scikit-verify 0.4.4

scikit-verify 0.4.4

• Fix: np.percentile and np.quantile silently ignored the method
  kwarg and returned the linear-method result. lower, higher,
  nearest and midpoint are now lifted exactly; the remaining
  Hyndman-Fan methods and stray kwargs refuse with a stated reason.
• No other changes.

scikit-verify 0.4.3

scikit-verify 0.4.3

• np.piecewise maps to sympy.Piecewise as a dialect entry. numpy's
  last-condition-wins precedence is honored by building the chain
  forward, callable pieces are traced through, extra args pass
  through, and the trailing funclist entry is the otherwise clause.
  A concrete boolean mask still refuses, since there is no symbolic
  condition to recover.
• No other changes.

scikit-verify 0.4.2

scikit-verify 0.4.2

Test and documentation release; no breaking API changes.

• Raise test coverage 82% -> 96% (1519 tests, 1 skipped) via genuine
  tests across the dialect API, every ufunc, refusal branches, numpy
  map bodies, pair operators, explore.py, testing, contracts, coercion,
  and checks. Genuinely-unreachable defensive branches carry an honest
  '# pragma: no cover' with a stated reason.
• feat: array endpoints supported in space generators (linspace/
  logspace/geomspace) (#47); no public API change.
• docs: API reference for the property rung (@specifies.property).
• readme: self-contained, meaningful explore() example.

v0.4.0

One trace follows one path; this release proves the rest.

Highlights

• explore() and covers(): each traced branch condition is negated and handed to Z3, which produces an input for the other side or proves none exists. Coverage is claimed only when the solver proves the OR of path conditions covers the domain.
• @specifies checks every branch by default. A spec right on the tested branch and wrong on another now fails, with the guilty branch printed. A green test cannot hide an unchecked branch.
• @specifies.property: check a fact (entries sum to one, a null space holds) on every branch, with the failing input returned; inequalities checked by entailment.
• assume= simplification makes derivation-domain specs like the spline penalty closed forms checkable (#48, @be-student).
• FFT family joins the dialect: the DFT is a closed form at any n, so fft/ifft/rfft emit Sums; Parseval and linearity become provable, complex formulas are first class.
• Soundness: coverage completeness is a proven theorem, not bookkeeping; three CI oracles (ground-truth fuzzing, sympy-vs-Z3 differential, empirical coverage audit).
• z3-solver is now required (a plain pip wheel).
• New DESIGN.md (#40, @AAYUSHRAJPUT846) and branch_coverage_check.ipynb.

Measured: 274 of 293 public numpy functions that trace get full branch coverage proven.

pip install scikit-verify

v0.3.0

The testing release: the spec from the paper, checked as a test.

• skverify.testing lands: @specifies turns a formula into a pytest test, check_formula returns the Verdict behind it
• Verdicts are four-tier, never a bare boolean -- exact, float-constant, sampled, differs/undecided/incomplete -- each carrying the shape it was decided at, and a counterexample when it fails
• Guard-aware sampling: sampled points respect the traced branch conditions, so the sampled tier is honest about what it actually checked
• Real scipy specs across five modules in the suite, including the known refusals (pearsonr, iqr) pinned at the incomplete tier
• np.prod reductions, and 2D np.gradient with repeated axes rejected the way numpy rejects them
• 7x faster traces on loop-heavy code
• Sphinx docs on Read the Docs; numpydoc docstrings across the public API
• skverify-hypothesis is gone -- one testing story. The skverify_hypothesis module that shipped in 0.2.0 is no longer in the wheel.

v0.2.0

The demo release: the tracer handles the code real demos are made of.

• In-place operations land: -=, out=, views with write-back; every Pair owns its buffer
• Chained matmuls over scatter-built matrices (C.T @ R @ C traces to closed forms)
• Sparse diagonal matrices trace: diags_array as structured allocation, .diagonal/.tocsc on traced values
• Fold symbols never leak: certificates reference only defined terms, enforced at harvest
• Contracts for the everywhere-atoms: svd, qr, cholesky, lstsq, pinv, fft checked against their defining equations per call
• Random draws seal as sympy.stats variables; E and Var of results in closed form
• skverify.latex renders code-ish names and matrices cleanly
• Two executed demos: a 20-page scipy spline derivation checked symbolically, and sklearn 1.9's BayesianRidge fix read from certificates