@@ -569,8 +569,27 @@ impl AggregationState {
569569 }
570570
571571 fn insert ( & mut self , timestamp : u64 , metric : Metric ) -> bool {
572+ // The context map is hard-capped at `context_limit` and no path grows it past the cap. This is the one
573+ // non-advisory runtime memory bound, so we assert it as an invariant under Antithesis. The numeric form hands
574+ // the search the margin to the limit as a gradient.
575+ #[ cfg( feature = "antithesis" ) ]
576+ antithesis_sdk:: assert_always_less_than_or_equal_to!(
577+ self . contexts. len( ) ,
578+ self . context_limit,
579+ "aggregate context map within context_limit" ,
580+ & serde_json:: json!( { "len" : self . contexts. len( ) , "limit" : self . context_limit } )
581+ ) ;
582+
572583 // If we haven't seen this context yet, and it would put us over the limit to insert it, then return early.
573584 if !self . contexts . contains_key ( metric. context ( ) ) && self . contexts . len ( ) >= self . context_limit {
585+ // Anti-vacuity anchor: prove a run actually reaches the cap, else the invariant above passes trivially.
586+ #[ cfg( feature = "antithesis" ) ]
587+ antithesis_sdk:: assert_sometimes!(
588+ true ,
589+ "aggregate context limit breached" ,
590+ & serde_json:: json!( { "limit" : self . context_limit } )
591+ ) ;
592+
574593 self . context_limit_breached = true ;
575594 return false ;
576595 }
@@ -632,11 +651,45 @@ impl AggregationState {
632651 if self . last_flush != 0 {
633652 let start = align_to_bucket_start ( self . last_flush , bucket_width_secs) ;
634653
654+ // Clock-skew guards. Bucketing reads the wall clock while the flush cadence is monotonic, so a wall-clock
655+ // jump is not bounded by the flush interval. A backward jump empties the zero-value range (a silent counter
656+ // gap); a forward jump makes the loop below run once per bucket across the whole jumped span — O(jump) work
657+ // and allocation. Assert before the loop so a flood fails fast rather than after the damage is done.
658+ #[ cfg( feature = "antithesis" ) ]
659+ {
660+ // Generous versus the normal cadence (default 15s flush over a 10s bucket yields 1-2 buckets); a bound
661+ // this large trips only on a multi-hour wall-clock jump, never on a slow-but-sane flush.
662+ const MAX_ZERO_VALUE_BUCKETS_PER_FLUSH : u64 = 10_000 ;
663+ antithesis_sdk:: assert_always!(
664+ current_time >= self . last_flush,
665+ "aggregate flush wall-clock did not move backward" ,
666+ & serde_json:: json!( { "current_time" : current_time, "last_flush" : self . last_flush } )
667+ ) ;
668+ antithesis_sdk:: assert_always_less_than_or_equal_to!(
669+ current_time. saturating_sub( self . last_flush) / bucket_width_secs. get( ) ,
670+ MAX_ZERO_VALUE_BUCKETS_PER_FLUSH ,
671+ "aggregate zero-value bucket span bounded across a flush" ,
672+ & serde_json:: json!( {
673+ "current_time" : current_time,
674+ "last_flush" : self . last_flush,
675+ "bucket_width_secs" : bucket_width_secs. get( )
676+ } )
677+ ) ;
678+ }
679+
635680 for bucket_start in ( start..current_time) . step_by ( bucket_width_secs. get ( ) as usize ) {
636681 if is_bucket_closed ( current_time, bucket_start, bucket_width_secs, flush_open_buckets) {
637682 zero_value_buckets. push ( ( bucket_start, MetricValues :: counter ( ( bucket_start, 0.0 ) ) ) ) ;
638683 }
639684 }
685+
686+ // Anti-vacuity anchor: prove the idle-counter zero-value path actually runs in some timeline.
687+ #[ cfg( feature = "antithesis" ) ]
688+ antithesis_sdk:: assert_sometimes!(
689+ !zero_value_buckets. is_empty( ) ,
690+ "aggregate flush generated zero-value counter buckets" ,
691+ & serde_json:: json!( { "count" : zero_value_buckets. len( ) } )
692+ ) ;
640693 }
641694
642695 // Iterate over each context we're tracking, and flush any values that are in buckets which are now closed.
0 commit comments