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.
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-reductionadversarial-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_propertytest module plus a small deterministic expression generator).In: randomly generated
Exprs — bounded depth (≤ 6), variables from a fixed pool (n,m,k), constructorsConst/Var/Add/Mul/Pow(const)/Sqrt/Logplus linear2^xforms; 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)
ewithgrowth(e) = Terms(...), render the growth back to anExprgand checkeval(e, s) ≤ C · eval(g, s)fors ∈ {2^8, 2^10, 2^12}(all variables set jointly), withCderived 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.growth(render(growth(e))) == growth(e).(a, b)of generated terms wheredominates(b, a)holds, asserteval(b, s₂)/eval(a, s₂) ≥ eval(b, s₁)/eval(a, s₁)fors₂ ≫ s₁(the ratio does not shrink), and it exceeds 1 at the larger size.Unknown(count them; assert they are a minority so the generator actually exercises the domain).Verification
cargo test growth_propertypasses 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. anAddthat 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.