Skip to content

tests: congestion β(t) region/bound invariant property tests#455

Merged
adamkrellenstein merged 1 commit into
feat/congestion-pricingfrom
test/congestion-properties
Jun 3, 2026
Merged

tests: congestion β(t) region/bound invariant property tests#455
adamkrellenstein merged 1 commit into
feat/congestion-pricingfrom
test/congestion-properties

Conversation

@adamkrellenstein

@adamkrellenstein adamkrellenstein commented Jun 3, 2026

Copy link
Copy Markdown
Contributor

Stacked on #445. Adds property tests for the β(t) congestion recurrence.

Tests

  • congestion_beta_invariants_over_random_walk — 60-step random walk of utilizations across all three regions, asserting: region 1 decays (β'≤β); region 3 grows (β'≥max(β,1)≥1); region 2 bounded by the smoothstep ceiling (β'≤max(β,1)); β never negative; fee_multiplier == φ_base·β throughout.
  • congestion_smoothstep_continuous_at_band_edges — S(1)=1 at u_high (joins region 3's floor), S(0)=0 at u_low (joins region 1's decay floor).

Design decision

The random-walk test asserts structural invariants via comparisons (≤/≥) rather than re-deriving exact β' values. Region-2's x = (u−u_low)/(u_high−u_low) is not always a terminating decimal, so exact re-derivation would couple the test to fixed-point rounding; the existing point tests already pin exact interior values (1.2 → 1.44 → 1.368, midpoint 0.5). The Python test_congestion.py remains the value oracle.

Test-only; no contract change.


Note

Low Risk
Test-only additions to contract tests; no production, auth, or fee logic changes.

Overview
Adds two in-process contract tests for the congestion β(t) recurrence in congestion.rs, complementing existing point-value checks.

congestion_beta_invariants_over_random_walk runs 60 deterministic utilization steps (0–100% in bps) and asserts structural properties via inequalities: low-util decay (β′ ≤ β), high-util growth (β′ ≥ 1 and ≥ prior β), mid-band smoothstep ceiling (β′ ≤ max(β, 1)), non-negative β, and fee_multiplier == φ_base · β each step—without pinning exact β′ in region 2 where fixed-point rounding would be brittle.

congestion_smoothstep_continuous_at_band_edges checks continuity at u_low / u_high: S(1)=1 at the upper band (β→1 from zero) and S(0)=0 at the lower band with the region-1 decay floor (β→0.95 from β=1).

No runtime or contract logic changes; Python remains the value oracle for exact numbers.

Reviewed by Cursor Bugbot for commit 21dd2bc. Bugbot is set up for automated code reviews on this repo. Configure here.

Add seeded random-walk + band-edge property tests for the congestion β(t)
recurrence:

- congestion_beta_invariants_over_random_walk: over utilizations spanning all
  three regions — region 1 decays (β'≤β); region 3 grows (β'≥max(β,1)≥1);
  region 2 is bounded by the smoothstep ceiling (β'≤max(β,1)); β never negative;
  fee multiplier always == φ_base·β.
- congestion_smoothstep_continuous_at_band_edges: S(1)=1 at u_high (joins
  region 3's floor), S(0)=0 at u_low (joins region 1's decay floor).

Design decision: the random-walk test asserts STRUCTURAL invariants via
comparisons (≤/≥), not re-derived exact β' values — robust to fixed-point
rounding (region-2 x=(u−u_low)/(u_high−u_low) is not always a terminating
decimal). Exact interior values stay covered by the existing point tests.
Test-only.
@adamkrellenstein
adamkrellenstein merged commit dfd632b into feat/congestion-pricing Jun 3, 2026
8 checks passed
@adamkrellenstein
adamkrellenstein deleted the test/congestion-properties branch June 3, 2026 13:16
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant