Refresh Issues

   oldest_age (in intervals)   ledger state   device requirement
   -------------------------   ------------   ------------------
        0 .. 3                 due            met
        4 .. 7                 urgent         met
        8                      overdue        AT the bound
        9 and beyond           overdue        MISSED

   so: overdue begins at 8 and a MISS begins at 9.

   a controller reporting "overdue events: 412, deadline misses: 0"
   is a controller using its allowance -- which is what the allowance
   is for. That is a PERFORMANCE observation, not a correctness one.

   a controller reporting "overdue: 412, misses: 3" has three
   correctness events and 409 performance events, and the two need
   completely different investigations.

// SIMULATION-ONLY. Shows why aggregate refresh telemetry cannot see a
// scope mismatch, by modelling per-bank service against a device-level
// ledger. It does NOT rebuild 15.2's scope-aware ledger -- it consumes
// the idea and demonstrates the blind spot.
//
// WHAT IT DOES NOT MODEL: the device, charge, or the command encoding.
// WHAT IT WOULD MISS: any starvation that is uniform across banks,
//   which an aggregate counter WOULD see -- this model is only
//   sensitive to the distribution.
class scope_mismatch_demo #(parameter int BANKS = 16);
  int  bank_age[BANKS];      // per-bank intervals since service
  int  device_pending;       // the aggregate ledger §11 publishes
  int  device_misses;

  function void new_interval();
    device_pending++;
    foreach (bank_age[b]) bank_age[b]++;
  endfunction

  // A device-wide command serves every bank and retires one aggregate
  // obligation. Both views agree.
  function void refresh_all_banks();
    if (device_pending > 0) device_pending--;
    foreach (bank_age[b]) bank_age[b] = 0;
  endfunction

  // A per-bank command serves ONE bank -- and a controller keeping a
  // single device-level counter retires the same one obligation it
  // would have retired for a device-wide command. That is the bug.
  function void refresh_one_bank(int b);
    if (device_pending > 0) device_pending--;
    if (b >= 0 && b < BANKS) bank_age[b] = 0;
  endfunction

  function int worst_bank_age();
    int w = 0;
    foreach (bank_age[b]) if (bank_age[b] > w) w = bank_age[b];
    return w;
  endfunction

  // The whole point: the aggregate view is clean and the distribution
  // is not. A test asserts these DISAGREE under a scope mismatch.
  function bit aggregate_looks_healthy(int allowance);
    return device_pending <= allowance;
  endfunction

  function bit distribution_is_starved(int deadline);
    return worst_bank_age() >= deadline;
  endfunction
endclass

   bucket the failing accesses by their position in the refresh window

   (B) drain / restart          (A) retention
   ------------------           --------------
   |#                 |         |                #|
   |#                 |         |               ##|
   |##                |         |             ####|
   +------------------+         +-----------------+
    ^ first access               age ->     ^ oldest
      after drain falls                       cells

   B clusters at the START of the window, immediately after traffic
   resumes, and does not care how old the obligation was.
   A clusters at the END, and gets worse as oldest_age grows.

   the same top-level symptom -- "corruption correlated with refresh"
   -- produces opposite distributions, and one histogram separates
   them.

// ---------------------------------------------------------------------
// refresh_telemetry -- CLASSIFICATION: synthesisable, BINDABLE.
//
// WHAT IT DOES: keeps §3's four quantities, separates OVERDUE events
// from DEADLINE MISSES (§3 -- they route to different
// investigations), and buckets data errors by position in the refresh
// window so §9's two opposite distributions are distinguishable.
//
// WHY OVERDUE AND MISS ARE SEPARATE COUNTERS: 15.3 owns a postponement
// allowance, and USING it is not a fault. A design reporting one
// combined "refresh error" count forces every performance excursion to
// be investigated as a correctness bug.
//
// WHY THE MISS FLAG IS STICKY (§4): a miss is a historical fact about
// the device, not a current condition. A flag that cleared when
// service resumed would make a system missing every window look
// identical to one that never missed.
//
// WHY THE HISTOGRAM (§9): retention clusters errors at the END of the
// window and grows with age; a drain/restart bug clusters them at the
// START and does not care about age. One histogram separates the two
// hypotheses that a "correlated with refresh" symptom cannot.
//
// WHAT IT CANNOT TELL YOU: whether charge was lost. Every field is
// controller bookkeeping. 15.4 owns retention as a SPECIFICATION and
// nothing here measures a physical quantity.
//
// SYNTHESIS: counters, one small histogram array, no DUT handle.
// ---------------------------------------------------------------------
module refresh_telemetry #(
  parameter int MAX_PENDING  = 16,   // postponement allowance, ILLUSTRATIVE
  parameter int DEADLINE_AGE = 9,    // ages beyond this are MISSES -- §3
  parameter int BUCKETS      = 8,    // window-position histogram -- §9
  parameter int AGE_W        = 12
)(
  input  logic                        clk,
  input  logic                        rst_n,

  // ---- refresh manager interface (observed only)
  input  logic                        accrue,     // an obligation accrues
  input  logic                        ref_issued, // a refresh retires one
  input  logic                        drain,      // 17.3's drain window
  input  logic                        temp_band_changed, // §11

  // ---- data-path error strobe (§9's histogram input)
  input  logic                        err_valid,

  input  logic                        clear,

  // ---- published evidence
  output logic [$clog2(MAX_PENDING+1)-1:0] pending,
  output logic [AGE_W-1:0]                 oldest_age,
  output logic [AGE_W-1:0]                 max_delay,
  output logic [15:0]                      overdue_events,
  output logic [15:0]                      deadline_misses,
  output logic                             miss_sticky,
  output logic                             accruing_seen,
  output logic [15:0]                      drains,
  output logic [15:0]                      drains_without_issue,
  output logic [15:0]                      band_changes,
  output logic [15:0]                      err_bucket [BUCKETS]
);
  // $clog2(1) is 0, which makes the pending vector illegal as [-1:0].
  initial begin
    if (MAX_PENDING  < 2) $fatal(1, "refresh_telemetry: MAX_PENDING must be >= 2 (got %0d)", MAX_PENDING);
    if (BUCKETS      < 2) $fatal(1, "refresh_telemetry: BUCKETS must be >= 2");
    if (AGE_W        < 4) $fatal(1, "refresh_telemetry: AGE_W must be >= 4");
    // A deadline at or below the allowance would make every use of the
    // allowance a miss, collapsing §3's distinction the block exists
    // to preserve.
    if (DEADLINE_AGE < 2) $fatal(1, "refresh_telemetry: DEADLINE_AGE must be >= 2");
  end

  localparam logic [AGE_W-1:0] AGE_MAX = {AGE_W{1'b1}};

  logic                      drain_q;
  logic                      in_window;      // since drain fell
  logic [AGE_W-1:0]          since_drain;
  logic                      issued_this_drain;

  always_ff @(posedge clk) begin
    if (!rst_n || clear) begin
      pending              <= '0;
      oldest_age           <= '0;
      max_delay            <= '0;
      overdue_events       <= '0;
      deadline_misses      <= '0;
      miss_sticky          <= 1'b0;
      accruing_seen        <= 1'b0;
      drains               <= '0;
      drains_without_issue <= '0;
      band_changes         <= '0;
      drain_q              <= 1'b0;
      in_window            <= 1'b0;
      since_drain          <= '0;
      issued_this_drain    <= 1'b0;
      for (int b = 0; b < BUCKETS; b++) err_bucket[b] <= '0;
    end else begin
      drain_q <= drain;

      // §2 row five: a ledger that never accrues looks identical to a
      // healthy one at zero. Publishing "have we EVER seen an accrual"
      // makes a dead accrual path a one-bit check.
      if (accrue) accruing_seen <= 1'b1;

      // ---- pending, saturating at the allowance rather than wrapping
      if (accrue && !ref_issued && pending != MAX_PENDING[$clog2(MAX_PENDING+1)-1:0])
        pending <= pending + 1'b1;
      else if (ref_issued && !accrue && pending != '0)
        pending <= pending - 1'b1;

      // ---- oldest age. Ages while anything is pending; resets only
      // when the LAST pending obligation retires, because the age is
      // the oldest one's, not the most recent one's.
      if (ref_issued && pending <= 1) oldest_age <= '0;
      else if (pending != '0 && oldest_age != AGE_MAX)
        oldest_age <= oldest_age + 1'b1;

      if (oldest_age > max_delay) max_delay <= oldest_age;

      // ---- §3's two DIFFERENT counters. Overdue is a ledger state;
      // a miss is a device statement. Counting them together would
      // make 412 performance events and 3 correctness events into one
      // meaningless number.
      if (pending == MAX_PENDING[$clog2(MAX_PENDING+1)-1:0]
          && overdue_events != 16'hFFFF)
        overdue_events <= overdue_events + 1'b1;

      if (oldest_age >= DEADLINE_AGE[AGE_W-1:0]) begin
        if (deadline_misses != 16'hFFFF) deadline_misses <= deadline_misses + 1'b1;
        // §4: sticky. Issuing a refresh afterwards does not undo it.
        miss_sticky <= 1'b1;
      end

      // ---- §6 row five: a drain that runs without issuing pays the
      // whole cost and retires nothing.
      if (drain && !drain_q) begin
        if (drains != 16'hFFFF) drains <= drains + 1'b1;
        issued_this_drain <= 1'b0;
      end
      if (drain && ref_issued) issued_this_drain <= 1'b1;
      if (!drain && drain_q) begin
        if (!issued_this_drain && drains_without_issue != 16'hFFFF)
          drains_without_issue <= drains_without_issue + 1'b1;
        // window position restarts when traffic resumes
        in_window   <= 1'b1;
        since_drain <= '0;
      end

      if (in_window && since_drain != AGE_MAX) since_drain <= since_drain + 1'b1;

      // ---- §9's histogram: bucket errors by position since traffic
      // resumed. Bucket 0 is the first access after drain fell.
      if (err_valid && in_window) begin
        automatic int b = (since_drain >= BUCKETS) ? BUCKETS - 1 : int'(since_drain);
        if (err_bucket[b] != 16'hFFFF) err_bucket[b] <= err_bucket[b] + 1'b1;
      end

      if (temp_band_changed && band_changes != 16'hFFFF)
        band_changes <= band_changes + 1'b1;
    end
  end
endmodule

// ---------------------------------------------------------------------
// refresh_correlation_ranker -- SIMULATION-ONLY.
//
// Ranks §9's four hypotheses from §12's telemetry. It returns a LIST
// and an experiment, never a cause -- and it refuses to return a
// retention verdict at all, because nothing digital measures charge.
//
// WHAT IT DOES NOT MODEL: charge, temperature physics, the device.
//
// WHAT IT WOULD MISS: a mechanism whose window-position distribution
// matches another's. The histogram separates START-clustered from
// END-clustered; it does not separate all four hypotheses.
// ---------------------------------------------------------------------
typedef enum {
  HYP_RETENTION, HYP_DRAIN_RESTART, HYP_TIMING, HYP_THERMAL
} refresh_hyp_e;

class refresh_snapshot;
  int pending;
  int oldest_age;
  int max_delay;
  int overdue_events;
  int deadline_misses;
  bit miss_sticky;
  bit accruing_seen;
  int drains;
  int drains_without_issue;
  int band_changes;
  int err_bucket[];        // §9's histogram
  bit timing_snapshot_valid;   // from 28.2's snapshot
  bit temperature_controlled;  // was the run thermally held?
endclass


class refresh_correlation_ranker;

  // §9: START-clustered means the first buckets dominate; END-clustered
  // means the last do. Returns -1 when the histogram is empty, so "no
  // errors" is distinct from "uniformly spread".
  function int peak_bucket(refresh_snapshot s);
    int best = -1, bestv = 0;
    foreach (s.err_bucket[i])
      if (s.err_bucket[i] > bestv) begin bestv = s.err_bucket[i]; best = i; end
    return best;
  endfunction

  function int total_errors(refresh_snapshot s);
    int n = 0;
    foreach (s.err_bucket[i]) n += s.err_bucket[i];
    return n;
  endfunction

  // §2 row five, checked FIRST: a ledger that never accrued makes every
  // other refresh number meaningless, so no hypothesis is ranked until
  // it is excluded.
  function bit telemetry_trustworthy(refresh_snapshot s);
    return s.accruing_seen;
  endfunction

  function void rank(refresh_snapshot s, ref refresh_hyp_e out[$]);
    int pk = peak_bucket(s);
    int n  = s.err_bucket.size();
    out.delete();
    if (!telemetry_trustworthy(s)) return;   // §2: nothing is rankable

    // §6 row five and §7: a manager that drains without issuing is a
    // control defect, and its errors are restart errors.
    if (s.drains_without_issue > 0) out.push_back(HYP_DRAIN_RESTART);

    // §9: START-clustered -> drain/restart. Checked before retention
    // because it is cheaper to test and is the commonly missed one.
    if (pk >= 0 && pk < (n / 4)) out.push_back(HYP_DRAIN_RESTART);

    // 28.2's snapshot is non-empty: a refresh-adjacent timing rule
    // fired, and that is a digital fact rather than an inference.
    if (s.timing_snapshot_valid) out.push_back(HYP_TIMING);

    // §11: a band change with misses points at the rate not following
    // the condition.
    if (s.band_changes > 0 && !s.temperature_controlled)
      out.push_back(HYP_THERMAL);

    // §9 hypothesis A is offered ONLY when the obligation was actually
    // missed AND the errors cluster at the END of the window. Without
    // a miss, the device was served within its requirement and a
    // retention story has no supporting evidence.
    if (s.deadline_misses > 0 && pk >= (3 * n / 4))
      out.push_back(HYP_RETENTION);
  endfunction

  // §10's confound, made a method so a caller cannot forget it. Errors
  // per DRAIN EVENT removes the exposure-rate confound that errors per
  // second does not.
  function real errors_per_window(refresh_snapshot s);
    if (s.drains == 0) return -1.0;          // not "zero errors"
    return real'(total_errors(s)) / real'(s.drains);
  endfunction

  function string next_experiment(refresh_snapshot s);
    int pk = peak_bucket(s);
    int n  = s.err_bucket.size();
    if (!telemetry_trustworthy(s))
      return "the ledger never accrued: stop issuing refresh and confirm it climbs before anything else is investigated";
    if (s.drains_without_issue > 0)
      return "drains without an issue are non-zero: the manager pays for refresh and retires nothing -- read 17.3's issue path before any retention work";
    if (pk >= 0 && pk < (n / 4))
      return "errors cluster at the first accesses after drain: compare errors per drain event across two refresh rates; unchanged per-window => restart bug, not retention";
    if (s.deadline_misses == 0)
      return "no deadline was missed: the obligation was met, so a retention story has no supporting evidence -- bucket the errors and check the drain interval";
    if (pk >= (3 * n / 4))
      return "errors cluster at the end of the window with misses present: hold temperature and bandwidth constant, then compare errors per window across refresh rates";
    return "no distinguishing distribution: collect more windows before changing any configuration";
  endfunction

  // §9's boundary, enforced in code rather than in a comment.
  function string retention_verdict(refresh_snapshot s);
    return "unavailable: retention is a specified physical property (15.4). No controller telemetry measures charge, and a correlation with refresh position is consistent with at least four mechanisms (§9)";
  endfunction
endclass

// Bound to §12's telemetry. Every property carries `disable iff`, and
// every antecedent is covered below -- 27.2 measured this curriculum
// at 78.53% implications, so a silent pass is otherwise
// indistinguishable from an unbound block.
module refresh_telemetry_sva #(
  parameter int MAX_PENDING = 16,
  parameter int DEADLINE_AGE = 9,
  parameter int AGE_W = 12
)(
  input logic clk, rst_n, clear,
  input logic accrue, ref_issued, drain, err_valid, temp_band_changed,
  input logic [$clog2(MAX_PENDING+1)-1:0] pending,
  input logic [AGE_W-1:0] oldest_age, max_delay,
  input logic [15:0] overdue_events, deadline_misses, drains, drains_without_issue,
  input logic miss_sticky, accruing_seen
);
  // ---- P1. FORBIDDEN. A miss flag never clears without an explicit
  // clear. §4: a miss is a historical fact, and a flag that cleared on
  // service would make a system missing every window look clean.
  property p_miss_sticky;
    @(posedge clk) disable iff (!rst_n)
      (miss_sticky && !clear) |=> miss_sticky;
  endproperty
  assert property (p_miss_sticky)
    else $error("telemetry: miss_sticky cleared without a clear");

  // ---- P2. FORBIDDEN. Issuing a refresh does not clear the miss.
  // This is P1's specific and most tempting violation.
  property p_issue_does_not_clear_miss;
    @(posedge clk) disable iff (!rst_n)
      (miss_sticky && ref_issued && !clear) |=> miss_sticky;
  endproperty
  assert property (p_issue_does_not_clear_miss)
    else $error("telemetry: a refresh issue cleared the miss flag");

  // ---- P3. A miss is recorded whenever the oldest age reaches the
  // deadline. Without this the flag could be sticky and never set.
  property p_miss_recorded;
    @(posedge clk) disable iff (!rst_n)
      (oldest_age >= DEADLINE_AGE) |=> miss_sticky;
  endproperty
  assert property (p_miss_recorded)
    else $error("telemetry: deadline age reached without recording a miss");

  // ---- P4. FORBIDDEN. Overdue and miss are DIFFERENT counters. An
  // overdue event must not increment the miss count. §3: 412
  // performance events and 3 correctness events must stay separable.
  property p_overdue_is_not_a_miss;
    @(posedge clk) disable iff (!rst_n)
      (pending == MAX_PENDING && oldest_age < DEADLINE_AGE)
        |=> (deadline_misses == $past(deadline_misses));
  endproperty
  assert property (p_overdue_is_not_a_miss)
    else $error("telemetry: an overdue event incremented the miss count");

  // ---- P5. INVARIANT. pending never exceeds the allowance. The
  // counter is sized for MAX_PENDING+1 values -- COUNT versus INDEX --
  // precisely so this cannot wrap silently.
  property p_pending_bounded;
    @(posedge clk) disable iff (!rst_n)
      (pending <= MAX_PENDING);
  endproperty
  assert property (p_pending_bounded)
    else $error("telemetry: pending %0d exceeded the allowance", pending);

  // ---- P6. max_delay is monotone within a run. A high-water mark
  // that fell would erase the worst case it exists to remember.
  property p_max_delay_monotone;
    @(posedge clk) disable iff (!rst_n)
      (!clear) |=> (max_delay >= $past(max_delay));
  endproperty
  assert property (p_max_delay_monotone)
    else $error("telemetry: max_delay decreased");

  // ---- P7. max_delay bounds the current age at all times.
  property p_max_delay_bounds_age;
    @(posedge clk) disable iff (!rst_n)
      (max_delay >= oldest_age) || (oldest_age == 0);
  endproperty
  assert property (p_max_delay_bounds_age)
    else $error("telemetry: oldest_age %0d exceeds max_delay %0d", oldest_age, max_delay);

  // ---- P8. FORBIDDEN. The age never advances with nothing pending.
  // An age that ticked on an empty ledger would manufacture misses.
  property p_no_age_without_pending;
    @(posedge clk) disable iff (!rst_n)
      (pending == '0) |=> (oldest_age <= $past(oldest_age));
  endproperty
  assert property (p_no_age_without_pending)
    else $error("telemetry: oldest_age advanced with nothing pending");

  // ---- P9. accruing_seen is sticky. §2 row five: it is the one bit
  // that separates a healthy ledger at zero from a dead one.
  property p_accruing_seen_sticky;
    @(posedge clk) disable iff (!rst_n)
      (accruing_seen && !clear) |=> accruing_seen;
  endproperty
  assert property (p_accruing_seen_sticky)
    else $error("telemetry: accruing_seen dropped");

  // ---- P10. An accrual sets it. Together with P9 this makes the bit
  // a faithful "has the ledger ever moved".
  property p_accrue_sets_seen;
    @(posedge clk) disable iff (!rst_n)
      accrue |=> accruing_seen;
  endproperty
  assert property (p_accrue_sets_seen)
    else $error("telemetry: an accrual did not set accruing_seen");

  // ---- P11. A drain that ends without an issue is counted. §6 row
  // five: the manager paid the whole cost and retired nothing.
  property p_drain_without_issue_counted;
    @(posedge clk) disable iff (!rst_n)
      ($fell(drain) && !$past(ref_issued) && drains_without_issue != 16'hFFFF)
        |-> (drains_without_issue >= $past(drains_without_issue));
  endproperty
  assert property (p_drain_without_issue_counted)
    else $error("telemetry: a drain without an issue was not counted");

  // ---- P12. INVARIANT. Counters saturate rather than wrap. A wrapped
  // miss count reading 2 after 65,538 misses would understate a
  // systemic failure catastrophically.
  property p_misses_saturate;
    @(posedge clk) disable iff (!rst_n)
      (deadline_misses == 16'hFFFF) |=> (deadline_misses == 16'hFFFF);
  endproperty
  assert property (p_misses_saturate)
    else $error("telemetry: deadline_misses wrapped past saturation");

  // ---- 27.2 §7: publish every antecedent.
  cover property (@(posedge clk) disable iff (!rst_n) accrue);
  cover property (@(posedge clk) disable iff (!rst_n) ref_issued);
  cover property (@(posedge clk) disable iff (!rst_n) drain);
  cover property (@(posedge clk) disable iff (!rst_n) $fell(drain));
  cover property (@(posedge clk) disable iff (!rst_n) err_valid);
  cover property (@(posedge clk) disable iff (!rst_n) clear);
  cover property (@(posedge clk) disable iff (!rst_n) temp_band_changed);
  cover property (@(posedge clk) disable iff (!rst_n) pending == MAX_PENDING);
  cover property (@(posedge clk) disable iff (!rst_n) miss_sticky);
  // P3's antecedent, published explicitly: without this cover, a run
  // that never reached the deadline age is indistinguishable from one
  // where P3 armed and held -- which is 27.2 §2's vacuity argument
  // applied to this property specifically.
  cover property (@(posedge clk) disable iff (!rst_n)
                  oldest_age >= DEADLINE_AGE);
  cover property (@(posedge clk) disable iff (!rst_n) !accruing_seen);
  cover property (@(posedge clk) disable iff (!rst_n) drains_without_issue != 16'd0);
  cover property (@(posedge clk) disable iff (!rst_n) overdue_events != 16'd0 && deadline_misses == 16'd0);
  cover property (@(posedge clk) disable iff (!rst_n) err_valid && drain);
endmodule

// SIMULATION-ONLY. Independent reference: it replays the accrual and
// issue stream into a QUEUE of obligation timestamps and derives the
// age by inspecting the queue head, rather than maintaining an
// incremental age register. A different algorithm, so agreement is
// evidence -- 27.4 §15's argument.
class refresh_reference;
  int obligations[$];      // accrual cycle of each pending obligation
  int now;
  int max_delay_seen;
  int misses;
  int overdue;

  function void tick();
    now++;
    if (obligations.size() > 0) begin
      int age = now - obligations[0];
      if (age > max_delay_seen) max_delay_seen = age;
    end
  endfunction

  function void accrue();
    obligations.push_back(now);
  endfunction

  // A refresh retires the OLDEST obligation, which is what makes the
  // queue head the right place to read the age from.
  function void issue();
    if (obligations.size() > 0) void'(obligations.pop_front());
  endfunction

  function int oldest_age();
    if (obligations.size() == 0) return 0;
    return now - obligations[0];
  endfunction

  // §3: two different classifications from one age.
  function void classify(int allowance, int deadline);
    int a = oldest_age();
    if (obligations.size() >= allowance) overdue++;
    if (a >= deadline) misses++;
  endfunction

  function int pending(); return obligations.size(); endfunction
endclass

  TWO PASSING REFRESH REPORTS

  (A) the ledger never accrued
        accrue tied low; traffic running; no refresh ever issued
        pending                     0
        oldest_age                  0
        max_delay                   0
        overdue_events              0
        deadline_misses             0
        miss_sticky                 0
        accruing_seen               0     <-- the only non-clean field
        ------------------------------------------------
        all 12 properties           PASS
        cover accrue                0 hits
        cover ref_issued            0 hits
        cover pending == MAX        0 hits

        every refresh number is perfect and no refresh ever happened.
        A report reading "refresh: 0 misses, 0 overdue" is produced by
        this run AND by a flawless one, and the ONE field that
        separates them is a sticky bit nobody usually publishes.

        §13's ranker returns an EMPTY hypothesis list here, which is
        the correct behaviour: with untrustworthy telemetry, nothing
        about the device is rankable.

  (B) the obligation was met and data was still corrupted
        stimulus : full traffic, refresh healthy, errors observed
        deadline_misses             0
        overdue_events              91
        max_delay                   6      (deadline 9)
        drains                      4,118
        drains_without_issue        0
        err_bucket[0]               2,204  <-- first access after drain
        err_bucket[1..6]            0
        err_bucket[7]               3
        ------------------------------------------------
        all 12 properties           PASS
        all 13 covers               HIT

        the refresh obligation was met with three intervals of margin
        and 2,207 data errors occurred. 99.9% of them are at the FIRST
        access after traffic resumed.

        §9's histogram says drain/restart, not retention -- and the
        retention story, which is what "corruption correlated with
        refresh" usually becomes, is not merely unsupported here: the
        obligation was never missed, so it has no evidence at all.

    diagnosis : (A) is the vacuity case with a refresh face. (B) is
      §9's trap: the correlation is real, the mechanism is a traffic
      restart, and raising the refresh rate -- §10 -- would have made
      it WORSE while appearing to change something.

    the fix : (A) publish accruing_seen and read it first. (B) bucket
      the errors by window position before proposing any mechanism,
      and compare errors PER WINDOW across rates rather than per
      second.