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

    Fields

    No fields configured for issues without a type.

    Projects

    Status
    No status

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions