Skip to content

Add randomized property tests cross-validating the growth domain against numeric evaluation #1077

Description

@isPANN

Background

The growth domain (#1075, src/growth.rs) computes asymptotic (Big-O) normal forms of symbolic overhead expressions. Its trustworthiness rests on hand-written "transfer functions" (how add/mul/pow/log map into the domain) and a symbolic dominance order. Unit tests cover named cases; this issue adds the randomized layer that cross-validates the whole domain against the ground truth we already have — numeric evaluation of expressions (Expr::eval) — in the spirit of the repo's /verify-reduction adversarial-checking culture (≥ 5000 randomized checks).

Full design (shared overview for this batch): docs/design/symbolic-growth-domain.md, Quality requirements.

Objective

Add a property-test harness that generates random expressions and verifies the growth domain's three core contracts: upper-bound soundness, idempotence, and dominance soundness.

Interface (Input → Output)

Test-only code (a growth_property test module plus a small deterministic expression generator).
In: randomly generated Exprs — bounded depth (≤ 6), variables from a fixed pool (n, m, k), constructors Const/Var/Add/Mul/Pow(const)/Sqrt/Log plus linear 2^x forms; seeded RNG (fixed seed in CI, no wall-clock/entropy — repo tests must be deterministic).
Out: assertions; each contract exercised ≥ 5000 times.

Technical recommendations (non-binding)

  • Upper bound: for each generated e with growth(e) = Terms(...), render the growth back to an Expr g and check eval(e, s) ≤ C · eval(g, s) for s ∈ {2^8, 2^10, 2^12} (all variables set jointly), with C derived from the observed ratio at a small anchor size (e.g. s = 2^6) times a fixed slack — the exact derivation is the implementer's choice; what matters is that the bound is checked at sizes larger than the anchor.
  • Idempotence: growth(render(growth(e))) == growth(e).
  • Dominance soundness: for pairs (a, b) of generated terms where dominates(b, a) holds, assert eval(b, s₂)/eval(a, s₂) ≥ eval(b, s₁)/eval(a, s₁) for s₂ ≫ s₁ (the ratio does not shrink), and it exceeds 1 at the larger size.
  • Skip generated expressions that map to Unknown (count them; assert they are a minority so the generator actually exercises the domain).

Verification

cargo test growth_property passes in < 5 s (repo test-time policy), reporting ≥ 5000 checks per contract — which proves the transfer functions are sound over a far larger input space than the hand-written cases.

Negative control (harness has teeth): include one #[test] that runs the same upper-bound harness against a deliberately broken transfer function (e.g. an Add that keeps only the first operand's terms — an under-approximation) and asserts the harness detects a violation (the test passes because the harness fails the broken variant). If the harness cannot catch this seeded bug, the test fails — proving the property tests are capable of failing.

Dependencies

Depends on #1075. Milestone: Symbolic Growth Domain & Pareto Search.

Metadata

Metadata

Assignees

No one assigned

    Labels

    No labels
    No labels

    Type

    No type

    Projects

    Status
    No status

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions