[WIP – ignore until reviewed by @ChrisRackauckas] Property suite: isautonomous, issmooth, hasrandomness, hasmutation, ispure, isinferable

Project.toml

@@ -1,6 +1,6 @@
 name = "FunctionProperties"
 uuid = "f62d2435-5019-4c03-9749-2d4c77af0cbc"
-version = "1.0.0"
+version = "1.2.0"
 authors = ["SciML"]
 
 [deps]

docs/make.jl

@@ -5,6 +5,7 @@ cp("./docs/Project.toml", "./docs/src/assets/Project.toml", force = true)
 
 pages = [
     "Home" => "index.md",
+    "design.md",
     "api.md",
 ]
 

docs/src/api.md

@@ -2,5 +2,13 @@
 
 ```@docs
 hasbranching
+islinear
+isquadratic
+isautonomous
+issmooth
+hasrandomness
+hasmutation
+ispure
+isinferable
 is_leaf
 ```

docs/src/assets/Project.toml

@@ -0,0 +1,7 @@
+[deps]
+Documenter = "e30172f5-a6a5-5a46-863b-614d45cd2de4"
+FunctionProperties = "f62d2435-5019-4c03-9749-2d4c77af0cbc"
+
+[compat]
+Documenter = "1"
+FunctionProperties = "1"

docs/src/design.md

@@ -0,0 +1,60 @@
+# The certification interface
+
+Every query in this package answers a question about an arbitrary Julia function, and by
+Rice's theorem no such semantic question is decidable in general. The package therefore
+commits to a single, uniform contract, chosen so that a wrong answer can never be the unsafe
+one:
+
+## One-sided certificates
+
+For the `is*` family (`islinear`, `isquadratic`, `isautonomous`, `issmooth`, `ispure`,
+`isinferable`), **`true` is a proof** of the property along every execution path, and `false`
+only means *not proven* — the function may still have the property (for example
+`x^2 - x^2 + x` is linear but is not certified, because the degree bound does not model
+cancellation). Dispatch on `true`; treat `false` as "use the general path."
+
+For the `has*` family (`hasbranching`, `hasrandomness`, `hasmutation`), the polarity flips so
+that the same rule holds: **`false` is the certificate** (proven absent), and `true` means the
+property was observed *or could not be ruled out*.
+
+**Every internal "give up" — an unanalyzable call, an exhausted recursion budget, a foreign
+number type, an aborted trace — resolves to the conservative answer**, never to the
+certificate.
+
+## Dual guards
+
+Two complementary engines back the certificates, because each covers the other's blind spot:
+
+  - a **static scan of the type-inferred IR** (the `hasbranching` machinery), which sees every
+    execution path but deliberately treats `Base`/standard-library internals as opaque leaves;
+  - **dynamic tracer types** (`islinear`'s degree tracer, `issmooth`'s smoothness probe,
+    `hasmutation`'s write probe), which follow values through any generic code — including
+    library internals such as broadcasting, where the static scan is leaf-blind — but only
+    along the path actually taken. Every operation on a tracer that would need the traced
+    *value* (a comparison, `isnan`, rounding, conversion) throws, so a computation that the
+    tracer cannot faithfully follow aborts toward the conservative answer instead of producing
+    an unsound certificate.
+
+A tracer-based certificate is only issued when `hasbranching` additionally proves the traced
+path is the *only* path.
+
+## Independent validation
+
+The test suite checks certificates against mathematics, not against the implementation's own
+rules: linear certificates are cross-validated with exactly vanishing finite differences over
+`Rational{BigInt}` arithmetic at random points, and non-mutation certificates against exact
+before/after comparison of real calls. Each property is exercised by adversarial cases
+(recursion towers, wrapper indirection, cancellation, aliasing, exotic number types), and
+contributions of new properties are expected to bring an independent refutation oracle and an
+adversarial battery of their own.
+
+## Known boundaries
+
+The certificates share the documented visibility limits of the static scan: calls hidden
+behind dynamic dispatch (untyped `Function` fields) are invisible to it, `Base` internals are
+leaves for branch detection (tracers compensate where they run), and floating-point rounding
+is not modeled — polynomial and smoothness certificates are statements about the program's
+real-arithmetic semantics. One value channel cannot be closed by the tracers: `objectid` is not
+overloadable, so a program that feeds `objectid` of a traced value into its output can obtain a
+certificate that does not survive at runtime — as in every tracer-based system. Reflection of
+that kind is outside the certified program class.

p8_12.log

@@ -0,0 +1,8 @@
+ERROR: SystemError: opening file "/home/crackauc/sandbox/tmp_20260629_155622_81813/clones/FunctionProperties.jl/patho8.jl": No such file or directory
+Stacktrace:
+ [1] include(mod::Module, _path::String)
+   @ Base ./Base.jl:306
+ [2] exec_options(opts::Base.JLOptions)
+   @ Base ./client.jl:317
+ [3] _start()
+   @ Base ./client.jl:550