[WIP – ignore until reviewed by @ChrisRackauckas] Property suite: isautonomous, issmooth, hasrandomness, hasmutation, ispure, isinferable#67
Draft
ChrisRackauckas-Claude wants to merge 4 commits into
Conversation
…ypes Implements the islinear/isquadratic proofs requested in SciML#1, using the tracer-type abstract-interpretation approach of the referenced Sparsity Programming paper, applied to polynomial degree instead of sparsity. `islinear(f, x...; wrt = 1)` and `isquadratic(f, x...; wrt = 1)` attempt to PROVE that `f` is a polynomial of degree <= 1 (affine) or <= 2 in the tracked arguments, holding the others fixed. `true` is a certificate under real arithmetic; `false` only means "not proven" -- the safe polarity for choosing an LP/QP path. Deciding this for arbitrary programs is impossible (Rice's theorem), so the design gives one-sided reliability: - The tracked arguments are seeded with `PolyDegree` tracer numbers and `f` is executed on them: `+`/`-` take the max degree, `*` adds, division by a constant and integer powers scale, and any non-polynomial operation on a non-constant poisons the result. Conservative by construction: the bound does not model cancellation (`x^2 - x^2 + x` is not certified). - Every predicate or conversion that would need the traced VALUE (comparisons, `isnan`, rounding, conversion) throws, aborting the trace -- this catches value-dependent branching dynamically even inside Base broadcast machinery, where `hasbranching`'s library-leaf policy is blind (`max.(u, 0)` is correctly rejected). - `hasbranching` is additionally required, proving statically that the traced path is the only path. The two guards cover each other's blind spots; a branch on an UNTRACKED argument also withholds the certificate (conservative, documented). The `wrt` selection gives the semantics SciML needs: an ODE right-hand side `(u, p, t) -> p[1]*u[1]` is certified linear in `u` for fixed `p`, while tracking everything (`wrt = :`) correctly refuses. Generic matrix code certifies: `u -> A*u` proves linear through the generic matmul. In-place right-hand sides work through a closure, shown in the tests. Tests include a ground-truth cross-validation: every issued linear certificate must have exactly vanishing second finite differences over exact Rational{BigInt} arithmetic at random points -- soundness is checked against real arithmetic, not against the tracer's own rules. The source is split by concern: `src/hasbranching.jl` holds the branch analysis, `src/polydegree.jl` the degree tracer and certificates, and the module file only exports and includes. Suites 70/70 on 1.10.11 and 72/72 on 1.12.6 and 1.13.0-rc1 (the tracer is pure dispatch, fully functional on lts); QA 18/18 (constructor disambiguators added for Base's cross-family Number constructors); docs build clean; Runic and typos clean. Additive on the 1.0.0 release: 1.0.0 -> 1.1.0. Co-Authored-By: Chris Rackauckas <accounts@chrisrackauckas.com>
…spure,
isinferable; document the certification interface
Extends the certification families along both engines, and documents the
package-wide contract as a docs page (design.md): one-sided certificates
(`is*`: true is a proof; `has*`: false is the certificate), every internal
give-up resolves to the conservative answer, dual guards (static IR scan and
dynamic tracer types cover each other's blind spots), and independent
mathematical validation in the tests.
- `isautonomous(f, x...; wrt = length(x))`: certified independence from the
trailing (time) argument via the degree tracer -- degree 0 in `t` plus the
`hasbranching` path proof. `t * 0` is conservatively not certified (no
cancellation modeling), branches on `t` block the certificate.
- `issmooth(f, x...; wrt = :)`: a new smoothness probe certifies that `f` is
a composition of real-analytic primitives on its domain interior; `abs`,
`sign`, rounding, `mod`, two-argument `atan`, `hypot`, `max`/`min`, and all
value-dependent comparisons abort the trace -- including through broadcast
machinery, where the static scan is leaf-blind.
- `hasrandomness(f, x...)`: a sibling of the `hasbranching` walk with the
callee policy inverted for the Random standard library -- any statically
reachable `rand`-family call reports true, however deeply nested. This is
the property that makes compiled ReverseDiff tapes silently wrong.
- `hasmutation(f, x...; arg = :)`: per-argument non-mutation certificates via
write-recording probe arrays with raw-memory access blocked, aliasing
detected one structural level deep, non-isbits element types rejected, and
the `hasbranching` path proof. Answers e.g. whether `u` is written by an
in-place `f!(du, u, p, t)` (`arg = 2`), with `du` (`arg = 1`) correctly
reported as written.
- `ispure` / `isinferable`: thin certificates over the compiler's effects
analysis and inferred return type, the former behind a functional
capability probe in the style of the constant-refutation gate.
Also: non-numeric arguments (parameter placeholders like `nothing`) now pass
through tracer seeding untouched, so `wrt = :` works on standard SciML
signatures, and `islinear`'s docstring notes the equivalence with a constant
Jacobian.
Tests grow to 102 (1.10.11) / 104 (1.12.6, 1.13.0-rc1) assertions, including
witness oracles: certified-unmutated arguments are verified exactly unchanged
by real calls, and known-impure/nonsmooth/random corpora are asserted
never-certified. QA 18/18 (effects internals allow-listed with justification);
docs build clean with the new design page; Runic and typos clean. Additive on
the islinear PR: 1.1.0 -> 1.2.0.
Co-Authored-By: Chris Rackauckas <accounts@chrisrackauckas.com>
…racle fuzzers added
Adversarial probing of the new certificates found five real defects, each
demonstrated with a runtime witness before fixing and locked in as a
regression test:
1. Text rendering was a value channel: `string(t)` on a tracer completed
with a fixed type-printed string, laundering the traced value into
untraced data with no visible branch --
`(u, p, t) -> u .+ Float64(codeunit(string(t), 1))` earned a false
`isautonomous` certificate while provably depending on `t` at runtime,
and the equivalent construction fooled `issmooth` (a runtime staircase).
`show` on both tracers now aborts the trace, closing the channel like
comparisons, rounding, and conversion before it.
2. `hasrandomness` missed function VALUES in argument position: `rand.()`
and `map(x -> x + rand(), u)` pass `rand`/a closure into Base machinery
with no visible call. `rand`/`randn` are moreover Base-owned functions
that the Random stdlib merely extends, so ownership rules cannot see
them: the fix matches the family by name, walks the methods of
user-defined singleton functions and closures, and treats closures with
captured state (no inspectable instance) as conservatively random.
3. `hasmutation`'s alias guard missed NamedTuples and struct fields:
`p = (cache = u,)` let `f` mutate the probed argument through `p` while
the probe watched a copy -- a false non-mutation certificate with the
mutation demonstrated on the caller's array. `_children` now traverses
NamedTuples and struct fields.
4. The same guard compared by `===` only, so a memory-sharing
`view(u, :)` argument aliased the probed array while comparing unequal
(also demonstrated). Arrays are now compared with `Base.mightalias`
(shared dataids); aliasing detection has no public equivalent, so the
access is allow-listed with justification.
5. A legitimate `nothing` argument (the ubiquitous parameter placeholder)
was mistaken for the internal cannot-probe sentinel, conservatively
poisoning e.g. `f!(du, u, nothing, t)`: the sentinel is now a dedicated
type.
Also added from the battery: Ref- and interpolation-smuggled `t`, `zero(t)`
correctly autonomous, float powers smooth, `sign` not, `fill!`/`copyto!`/
`view`-write/write-then-restore all flagged, `empty!` conservative, and two
seeded fuzzers with runtime witness oracles -- certified autonomy implies
exact output agreement across different `t`, and a certified-unmutated
argument is verified bit-identical after a real call.
Suites: 173/173 on 1.10.11, 175/175 on 1.12.6 and 1.13.0-rc1; the full
hardening battery passes on all three channels; QA 18/18; docs, Runic, and
typos clean.
Co-Authored-By: Chris Rackauckas <accounts@chrisrackauckas.com>
Contributor
Author
|
Hardening round for the property suite (commit 50e35d6). Adversarial probing with implementation knowledge found five real defects, each demonstrated with a runtime witness before fixing, each now a regression test:
Also added: Ref/interpolation-smuggled Suites: 173/173 (lts) · 175/175 (1.12.6) · 175/175 (1.13-rc1); battery green on all channels; QA 18/18; docs/Runic/typos clean. Familiar pattern worth noting for review: defects 1 and 5 are new instances of the two classes from the |
…perty fuzzer
Continued adversarial probing of the property suite:
- `isautonomous(() -> 1.0)` threw an uncaught ArgumentError: the default
`wrt = length(x)` is out of range for a zero-argument function. Such a
function is vacuously autonomous; certified as `true`.
- The `hash` value channel is blocked only incidentally today (Base's
`hash(::Real)` fallback reaches `decompose`, which has no tracer method
and aborts the trace): regression tests lock the conservative answer for
`hash`- and `Dict`-keyed constructions so a Base fallback change cannot
silently reopen the channel.
- `objectid` is confirmed as an unclosable value channel (it is not
overloadable) and is now documented as a known boundary on the design
page, as in every tracer-based system.
- Randomness smuggled through kwarg defaults (`g = rand`), varargs
(`fs[1]()` with `rand` passed in), and higher-order arguments
(`grideval(u, x -> x + randn())`) is verified detected; the clean
higher-order variant is verified not flagged.
- A task spawned inside `f` that mutates an argument after `f` returns is
verified conservatively flagged.
- Purity of a global-reading closure is verified not certified; `error`-only
functions and unusual argument containers (empty arrays, adjoints, ranges)
return Bools rather than throwing.
The suite gains a cross-property fuzzer: 30 randomly composed in-place
right-hand sides with independently toggled t-usage, kinks, randomness,
argument writes, and nonlinearity, where every certificate is checked against
a runtime witness -- certified-unmutated arguments are bit-identical after a
real call, certified non-randomness survives reseeding, certified autonomy
gives exact agreement across different `t`, and constructed kinks and
nonlinearities are never certified smooth or linear. (The offline battery runs
the same fuzzer at 80 cases across all three channels.)
Suites: 272/272 on 1.10.11, 274/274 on 1.12.6 and 1.13.0-rc1; QA 18/18; docs,
Runic, and typos clean.
Co-Authored-By: Chris Rackauckas <accounts@chrisrackauckas.com>
Contributor
Author
|
Hardening round 2 (commit 813e076): further value-channel, smuggling, and edge probing plus a cross-property fuzzer. Fixed (demonstrated first): Locked/documented:
Verified robust (no change needed): randomness smuggled through kwarg defaults ( Cross-property fuzzer now in the suite (30 cases; offline battery ran 80 × 3 channels): randomly composed in-place RHS with independently toggled t-usage, kinks, randomness, writes, and nonlinearity — every certificate checked against a runtime witness (bit-identity after real calls, reseeding invariance, exact two- Suites 272/272 (lts) · 274/274 (1.12.6) · 274/274 (1.13-rc1); QA 18/18; docs/Runic/typos clean. Cumulative for the property suite: 7 demonstrated defects found → fixed → regression-tested across both hardening rounds, plus two documented boundaries ( |
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
2 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
The certification interface, now documented
New docs page (
design.md) states the package-wide contract as interface: one-sided certificates (is*:trueis a proof,falseis "not proven";has*:falseis the certificate,trueis "observed or not ruled out"), every internal give-up resolves conservatively, dual guards (static IR scan × dynamic tracer types, each covering the other's blind spots), and independent mathematical validation in the tests.checkdocsenforces the API listing.New properties
isautonomous(f, x...; wrt=length(x))t(degree 0 + path proof);t*0conservatively not certified; branches ontblockissmooth(f, x...; wrt=:)abs/sign/rounding/mod/atan(y,x)/hypot/max/minabort — including through broadcast, where the static scan is leaf-blindhasrandomness(f, x...)false⇒ no statically reachablerand-family call, however nested — the property that makes compiled ReverseDiff tapes silently wronghasmutation(f, x...; arg=:)hasmutation(f!, du, u, p, t; arg=2)answers "isuwritten?" —ducorrectly flagged, sneakyu-writes caught, aliasing detected one structural level deep, raw-memory access blocked, non-isbitseltypes rejectedispure(f, x...)/isinferable(f, x...)ispurebehind a functional capability probe (same pattern as the constant-refutation gate)Also: non-numeric arguments (e.g.
p = nothing) pass through tracer seeding, sowrt = :works on standard SciML signatures;islineardocstring notes the constant-Jacobian equivalence.Validation
Tests grow to 102/104/104 (lts / 1.12.6 / 1.13-rc1) with witness oracles: certified-unmutated arguments verified exactly unchanged by real calls; known-impure/nonsmooth/random corpora asserted never-certified. QA 18/18 (effects internals allow-listed with justification), docs build clean with the new page, Runic and typos clean.