Data Corruption

   expected  0x33   0011 0011
   observed  0xB3   1011 0011
   XOR       0x80   1000 0000     one bit, position 7

   the VALUE tells you almost nothing. The XOR says: exactly one bit
   flipped, and it was bit 7. Accumulate that over a thousand errors
   and you have a distribution over bit positions -- which is a
   different and far more useful object than a thousand values.

   the interpretability requirement, stated plainly

   baseline : 40 errors in 8 hours
   after a change : 0 errors in 20 minutes

   this proves NOTHING. 20 minutes at the baseline rate expects
   40 * (20/480) = 1.67 errors, and observing zero of an expected 1.67
   is unremarkable.

   to claim a 10x improvement you must run long enough that the
   baseline would have produced enough errors for zero to be
   surprising -- which for 40-per-8-hours is many hours, not minutes.

   this is why "establish the rate first" is not pedantry. It sets
   the duration every later experiment must run for.

   accumulate over failing addresses:
     OR  of all failing addresses
     AND of all failing addresses

   a bit set in AND  -> that bit was 1 in EVERY failure
   a bit clear in OR -> that bit was 0 in EVERY failure
   either way the bit is CORRELATED with failure.

   bits that are 1 in OR and 0 in AND varied across failures, so
   they are uncorrelated.

   ILLUSTRATIVE, over 812 failing addresses:
     OR  = 0x3FFF_FE00
     AND = 0x0000_0200

   bit 9  : set in AND  -> always 1  -> CORRELATED
   bits 0-8 : clear in OR -> always 0 -> CORRELATED
   bits 10+ : varied              -> uncorrelated

   reading that through 8.6's map: the low nine bits being always
   zero means every failure was at a 512-byte-aligned address, and
   bit 9 always set narrows it further. That is a statement about a
   FIELD, and the map says which field.

   why mis-correction breaks a bit-position histogram

   underlying fault : bits 3 and 11 are wrong
   correction sees  : a syndrome consistent with a single fault
   it "repairs"     : bit 22

   what the interface returns : bits 3, 11 AND 22 are wrong

   the observed XOR now has THREE bits, one of which was never
   faulty, and a bit-position histogram accumulated across many such
   events reports positions the hardware never failed at.

   so the honest statement is not "bit 22 fails" but "the observed
   pattern is a function of the fault pattern AND the correction
   applied to it, and the mapping is not invertible from the
   interface".

// ---------------------------------------------------------------------
// corruption_evidence -- CLASSIFICATION: synthesisable, BINDABLE.
//
// TWO mechanisms, deliberately separate:
//   FIRST-ERROR CAPTURE  latches and refuses to update. The thousandth
//     error is a consequence of the state the first one left, so the
//     first is the evidence (Module 28's second law).
//   STRUCTURE ACCUMULATION never latches. A single error carries
//     almost nothing; the DISTRIBUTION over many carries §5's and
//     §6's answers.
// A single block doing both loses one of them.
//
// WHY THE XOR AND NOT THE VALUE (§1): "33 vs B3" is two numbers; the
// XOR 0x80 is one bit in position 7, which is a fact about hardware.
// OR over XORs = every position that ever failed. AND over XORs =
// every position that failed EVERY time. Those two separate a stuck
// bit from scattered flips, which no list of values does.
//
// WHY ADDRESS OR/AND (§6): a bit set in AND was 1 in every failure; a
// bit clear in OR was 0 in every failure. Either way it is CORRELATED,
// and 8.6's map says which field it selects.
//
// WHAT IT CANNOT TELL YOU: the FAULT structure when correction is
// active. §12 -- mis-correction can make bits appear wrong that never
// failed, so a bit-position conclusion is a statement about fault
// composed with correction.
//
// SYNTHESIS: capture registers, a small histogram, four accumulators.
// ---------------------------------------------------------------------
module corruption_evidence #(
  parameter int DATA_W  = 64,
  parameter int ADDR_W  = 34,
  parameter int LANES   = 8,
  parameter int BEATS   = 16,   // max burst beats -- 12.1 owns the contract
  parameter int BANKS   = 16
)(
  input  logic                      clk,
  input  logic                      rst_n,

  // ---- mismatch report (from Module 27's scoreboard)
  input  logic                      err_valid,
  input  logic [ADDR_W-1:0]         err_addr,
  input  logic [DATA_W-1:0]         err_expected,
  input  logic [DATA_W-1:0]         err_observed,
  input  logic [$clog2(BEATS)-1:0]  err_beat,
  input  logic [$clog2(BANKS)-1:0]  err_bank,
  input  logic                      err_is_read,
  input  logic                      ecc_correction_active, // §12

  input  logic                      clear,

  // ---- FIRST-ERROR CAPTURE (latched, first wins)
  output logic                      first_valid,
  output logic [ADDR_W-1:0]         first_addr,
  output logic [DATA_W-1:0]         first_xor,
  output logic [$clog2(BEATS)-1:0]  first_beat,
  output logic [$clog2(BANKS)-1:0]  first_bank,
  output logic [LANES-1:0]          first_lane_bm,
  output logic                      first_is_read,
  output logic                      first_ecc_active,

  // ---- STRUCTURE ACCUMULATION (never latched)
  output logic [DATA_W-1:0]         xor_or,
  output logic [DATA_W-1:0]         xor_and,
  output logic [LANES-1:0]          lane_or,
  output logic [LANES-1:0]          lane_and,
  output logic [ADDR_W-1:0]         addr_or,
  output logic [ADDR_W-1:0]         addr_and,
  output logic [BANKS-1:0]          bank_bm,
  output logic [15:0]               beat_hist [BEATS],
  output logic [31:0]               err_count,
  output logic [31:0]               err_reads,
  output logic [31:0]               err_writes,
  output logic [31:0]               err_with_ecc_active,
  output logic [$clog2(DATA_W+1)-1:0] first_popcount
);
  // $clog2(1) is 0, making every index vector illegal as [-1:0]. A
  // power-of-two test alone accepts 1, so the bounds are explicit.
  initial begin
    if (LANES  < 2) $fatal(1, "corruption_evidence: LANES must be >= 2 (got %0d)", LANES);
    if (BEATS  < 2) $fatal(1, "corruption_evidence: BEATS must be >= 2");
    if (BANKS  < 2) $fatal(1, "corruption_evidence: BANKS must be >= 2");
    if (DATA_W < LANES || (DATA_W % LANES) != 0)
      $fatal(1, "corruption_evidence: DATA_W %0d must be a multiple of LANES %0d", DATA_W, LANES);
    if (ADDR_W < 2) $fatal(1, "corruption_evidence: ADDR_W must be >= 2");
  end

  localparam int LANE_W = DATA_W / LANES;

  logic [DATA_W-1:0] xr;
  logic [LANES-1:0]  lane_bm;

  // Which lanes does this error touch? A lane is LANE_W contiguous
  // bits -- 6.9 owns the bus organisation.
  always_comb begin
    xr = err_expected ^ err_observed;
    for (int l = 0; l < LANES; l++)
      lane_bm[l] = |xr[l*LANE_W +: LANE_W];
  end

  always_ff @(posedge clk) begin
    if (!rst_n || clear) begin
      first_valid         <= 1'b0;
      first_addr          <= '0;
      first_xor           <= '0;
      first_beat          <= '0;
      first_bank          <= '0;
      first_lane_bm       <= '0;
      first_is_read       <= 1'b0;
      first_ecc_active    <= 1'b0;
      first_popcount      <= '0;
      // OR accumulators start at zero; AND accumulators must start at
      // ALL ONES or the first AND would clear everything.
      xor_or              <= '0;
      xor_and             <= {DATA_W{1'b1}};
      lane_or             <= '0;
      lane_and            <= {LANES{1'b1}};
      addr_or             <= '0;
      addr_and            <= {ADDR_W{1'b1}};
      bank_bm             <= '0;
      err_count           <= '0;
      err_reads           <= '0;
      err_writes          <= '0;
      err_with_ecc_active <= '0;
      for (int b = 0; b < BEATS; b++) beat_hist[b] <= '0;
    end else if (err_valid) begin
      // ---- FIRST WINS. Nothing but `clear` replaces this.
      if (!first_valid) begin
        first_valid      <= 1'b1;
        first_addr       <= err_addr;
        first_xor        <= xr;
        first_beat       <= err_beat;
        first_bank       <= err_bank;
        first_lane_bm    <= lane_bm;
        first_is_read    <= err_is_read;
        // §12: whether correction was active is part of the evidence,
        // because it determines whether a bit-position conclusion is
        // available at all.
        first_ecc_active <= ecc_correction_active;
        first_popcount   <= $countones(xr);
      end

      // ---- ACCUMULATE, always. §1: the distribution is the finding.
      xor_or   <= xor_or   | xr;
      xor_and  <= xor_and  & xr;
      lane_or  <= lane_or  | lane_bm;
      lane_and <= lane_and & lane_bm;
      addr_or  <= addr_or  | err_addr;
      addr_and <= addr_and & err_addr;
      bank_bm  <= bank_bm  | (1'b1 << err_bank);

      // §5: the beat histogram. Saturating -- a wrapped bin reading 3
      // after 65,539 errors would invert the distribution's shape,
      // which is the one thing this array exists to show.
      if (beat_hist[err_beat] != 16'hFFFF)
        beat_hist[err_beat] <= beat_hist[err_beat] + 1'b1;

      if (err_count != 32'hFFFF_FFFF) err_count <= err_count + 1'b1;
      if (err_is_read) begin
        if (err_reads  != 32'hFFFF_FFFF) err_reads  <= err_reads  + 1'b1;
      end else begin
        if (err_writes != 32'hFFFF_FFFF) err_writes <= err_writes + 1'b1;
      end
      if (ecc_correction_active && err_with_ecc_active != 32'hFFFF_FFFF)
        err_with_ecc_active <= err_with_ecc_active + 1'b1;
    end
  end
endmodule

// ---------------------------------------------------------------------
// corruption_classifier -- SIMULATION-ONLY.
//
// Maps §13's accumulated structure to §9's ranked hypotheses and the
// next discriminating experiment. Returns a LIST, never a cause.
//
// WHY IT WITHHOLDS BIT CONCLUSIONS UNDER CORRECTION (§12): 25.4's
// visibility problem means mis-correction can make bits appear wrong
// that never failed. A bit-position verdict is then a statement about
// fault composed with correction, and the composition is not
// invertible from the interface.
//
// WHAT IT WOULD MISS: two mechanisms with one observed structure --
// the normal case per §1, not an edge case.
// ---------------------------------------------------------------------
typedef enum {
  SIG_NONE, SIG_STUCK_BIT, SIG_LANE_LOCAL, SIG_FIRST_BEAT, SIG_LAST_BEAT,
  SIG_MID_BEAT, SIG_ADDR_CORRELATED, SIG_BANK_LOCAL, SIG_SCATTERED
} corr_sig_e;

class corruption_snapshot;
  int data_w, lanes, beats, addr_w;
  longint xor_or, xor_and;
  int     lane_or, lane_and;
  longint addr_or, addr_and;
  int     bank_bm;
  int     beat_hist[];
  int     err_count, err_reads, err_writes, err_with_ecc_active;
  bit     ecc_was_active;
endclass


class corruption_classifier;

  function int popcount(longint v, int width);
    int n = 0;
    for (int i = 0; i < width; i++) if (v[i]) n++;
    return n;
  endfunction

  function int peak_beat(corruption_snapshot s);
    int best = -1, bestv = 0;
    foreach (s.beat_hist[i])
      if (s.beat_hist[i] > bestv) begin bestv = s.beat_hist[i]; best = i; end
    return best;
  endfunction

  // §6: a bit is correlated when it was 1 in every failure (set in
  // AND) or 0 in every failure (clear in OR). Returns a mask.
  function longint correlated_addr_bits(corruption_snapshot s);
    longint m = 0;
    for (int i = 0; i < s.addr_w; i++)
      if (s.addr_and[i] || !s.addr_or[i]) m[i] = 1'b1;
    return m;
  endfunction

  // §12: available only when correction was NOT active.
  function bit bit_conclusion_available(corruption_snapshot s);
    return !s.ecc_was_active;
  endfunction

  function corr_sig_e signature(corruption_snapshot s);
    int pk;
    if (s.err_count == 0) return SIG_NONE;

    // A stuck bit is the strongest and cheapest conclusion -- and it
    // is WITHHELD under correction, because §12 says the observed bit
    // positions may include bits that never failed.
    if (bit_conclusion_available(s)
        && popcount(s.xor_and, s.data_w) == 1
        && popcount(s.xor_or,  s.data_w) == 1) return SIG_STUCK_BIT;

    // Lane structure survives correction: a lane correlates with paths
    // OUTSIDE the protected word.
    if (popcount(s.lane_and, s.lanes) >= 1
        && popcount(s.lane_or, s.lanes) == popcount(s.lane_and, s.lanes))
      return SIG_LANE_LOCAL;

    pk = peak_beat(s);
    if (pk == 0)                    return SIG_FIRST_BEAT;
    if (pk == s.beats - 1)          return SIG_LAST_BEAT;
    if (pk > 0)                     return SIG_MID_BEAT;

    if (popcount(correlated_addr_bits(s), s.addr_w) > 0)
      return SIG_ADDR_CORRELATED;
    if (popcount(s.bank_bm, 32) == 1) return SIG_BANK_LOCAL;
    return SIG_SCATTERED;
  endfunction

  function void rank(corruption_snapshot s, ref corr_sig_e out[$]);
    out.delete();
    if (s.err_count == 0) return;
    out.push_back(signature(s));
    // Direction is an independent axis (§4) and always worth reporting
    // alongside, because it eliminates whole families rather than
    // naming one.
    if (s.err_reads > 0 && s.err_writes == 0) out.push_back(SIG_LANE_LOCAL);
  endfunction

  function string next_experiment(corruption_snapshot s);
    case (signature(s))
      SIG_STUCK_BIT:
        return "swap the lane mapping; the failing bit should move with the lane if the fault is in the lane path, and stay put if it is downstream of the remap";
      SIG_LANE_LOCAL:
        return "swap the device; if the failing lane stays the same, the cause is board or package rather than device";
      SIG_FIRST_BEAT, SIG_LAST_BEAT:
        return "change the burst length (12.1); a burst-relative mechanism moves the failing beat index, a fixed-position datapath fault does not";
      SIG_MID_BEAT:
        return "vary the starting column (12.2); if the failing beat index follows the starting column the mechanism is burst-relative";
      SIG_ADDR_CORRELATED:
        return "change the mapping policy (18.1); a bit that stops correlating under a different policy implicates the field that bit selected, not the bit";
      SIG_BANK_LOCAL:
        return "redistribute traffic across banks; if the failures follow the bank index the cause is per-bank, if they follow the address the map is implicated";
      SIG_SCATTERED:
        return "establish the error rate per ACCESS at two frequencies before changing anything (§7); scattered errors need a rate, not a sample";
      default:
        return "no errors accumulated: the reproducer is not exercising the failure";
    endcase
  endfunction

  // §12's boundary, enforced rather than commented.
  function string bit_position_verdict(corruption_snapshot s);
    if (!bit_conclusion_available(s))
      return "unavailable: on-die correction was active, so the observed bit positions are a function of the fault pattern AND the correction applied to it (25.4's visibility problem, §12)";
    if (popcount(s.xor_and, s.data_w) == 1)
      return "one bit failed in every observed error -- a stuck-path hypothesis, testable by remapping lanes";
    return "no single bit failed in every error: the structure is not per-bit";
  endfunction

  // §3's interpretability requirement, as a computation nobody can
  // skip. Returns the hours a follow-up run must last for ZERO errors
  // to be surprising at the baseline rate.
  function real hours_needed_for_zero_to_mean_something(
      real baseline_errors, real baseline_hours, real want_expected);
    if (baseline_errors <= 0.0 || baseline_hours <= 0.0) return -1.0;
    return want_expected * baseline_hours / baseline_errors;
  endfunction
endclass

// Bound to §13's evidence block. 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 corruption_evidence_sva #(
  parameter int DATA_W = 64, parameter int LANES = 8,
  parameter int BEATS  = 16, parameter int ADDR_W = 34
)(
  input logic clk, rst_n, clear,
  input logic err_valid, err_is_read, ecc_correction_active,
  input logic [DATA_W-1:0] err_expected, err_observed, first_xor, xor_or, xor_and,
  input logic [ADDR_W-1:0] addr_or, addr_and,
  input logic [LANES-1:0]  lane_or, lane_and, first_lane_bm,
  input logic first_valid, first_ecc_active,
  input logic [31:0] err_count, err_reads, err_writes, err_with_ecc_active
);
  // ---- P1. FIRST WINS. The captured evidence never changes without
  // an explicit clear. Module 28's second law: the thousandth error is
  // a consequence of the state the first one left.
  property p_first_error_sticky;
    @(posedge clk) disable iff (!rst_n)
      (first_valid && !clear) |=> (first_xor == $past(first_xor)
                                && first_lane_bm == $past(first_lane_bm));
  endproperty
  assert property (p_first_error_sticky)
    else $error("evidence: a later error overwrote the first");

  // ---- P2. FORBIDDEN. A later error must not clear first_valid.
  property p_first_valid_sticky;
    @(posedge clk) disable iff (!rst_n)
      (first_valid && !clear) |=> first_valid;
  endproperty
  assert property (p_first_valid_sticky)
    else $error("evidence: first_valid dropped without a clear");

  // ---- P3. The capture is the FIRST error's XOR, not a later one's.
  property p_capture_is_first_xor;
    @(posedge clk) disable iff (!rst_n)
      (err_valid && !first_valid)
        |=> (first_xor == $past(err_expected ^ err_observed));
  endproperty
  assert property (p_capture_is_first_xor)
    else $error("evidence: captured XOR is not the first error's");

  // ---- P4. FORBIDDEN. A mismatch is never reported with equal
  // expected and observed. That combination means the scoreboard and
  // this block disagree about what an error is.
  property p_error_has_a_difference;
    @(posedge clk) disable iff (!rst_n)
      err_valid |-> (err_expected != err_observed);
  endproperty
  assert property (p_error_has_a_difference)
    else $error("evidence: an error was reported with no difference");

  // ---- P5. INVARIANT. The OR accumulator is monotone: a bit position
  // once seen failing stays recorded. §1 depends on accumulation.
  property p_xor_or_monotone;
    @(posedge clk) disable iff (!rst_n)
      (!clear) |=> ((xor_or & $past(xor_or)) == $past(xor_or));
  endproperty
  assert property (p_xor_or_monotone)
    else $error("evidence: xor_or lost a bit");

  // ---- P6. INVARIANT. The AND accumulator is anti-monotone: it only
  // ever loses bits. Together with P5 this makes the pair meaningful.
  property p_xor_and_antimonotone;
    @(posedge clk) disable iff (!rst_n)
      (!clear) |=> ((xor_and & $past(xor_and)) == xor_and);
  endproperty
  assert property (p_xor_and_antimonotone)
    else $error("evidence: xor_and gained a bit");

  // ---- P7. FORBIDDEN. AND is always a subset of OR. A bit that
  // failed every time must be a bit that failed at least once, and a
  // violation here means the accumulators were initialised wrongly --
  // the specific failure §13 warns about for AND starting at zero.
  property p_and_subset_of_or;
    @(posedge clk) disable iff (!rst_n)
      (err_count != 32'd0) |-> ((xor_and & xor_or) == xor_and);
  endproperty
  assert property (p_and_subset_of_or)
    else $error("evidence: xor_and is not a subset of xor_or");

  // ---- P8. Same relationship for lanes and addresses.
  property p_lane_and_subset;
    @(posedge clk) disable iff (!rst_n)
      (err_count != 32'd0) |-> ((lane_and & lane_or) == lane_and);
  endproperty
  assert property (p_lane_and_subset)
    else $error("evidence: lane_and is not a subset of lane_or");

  property p_addr_and_subset;
    @(posedge clk) disable iff (!rst_n)
      (err_count != 32'd0) |-> ((addr_and & addr_or) == addr_and);
  endproperty
  assert property (p_addr_and_subset)
    else $error("evidence: addr_and is not a subset of addr_or");

  // ---- P9. PARTITION. Reads plus writes account for every error. §4
  // is an axis, and an error belonging to neither direction means the
  // axis was never populated.
  property p_direction_partition;
    @(posedge clk) disable iff (!rst_n)
      (err_reads + err_writes == err_count);
  endproperty
  assert property (p_direction_partition)
    else $error("evidence: %0d reads + %0d writes != %0d errors",
                err_reads, err_writes, err_count);

  // ---- P10. FORBIDDEN. The ECC-active error count never exceeds the
  // total. §12 depends on that count being trustworthy.
  property p_ecc_count_bounded;
    @(posedge clk) disable iff (!rst_n)
      (err_with_ecc_active <= err_count);
  endproperty
  assert property (p_ecc_count_bounded)
    else $error("evidence: ECC-active errors exceed total errors");

  // ---- P11. The first error's ECC flag matches the condition at
  // capture. §12: whether a bit conclusion is available at all depends
  // on this, so it must be captured WITH the error, not read later.
  property p_first_ecc_captured;
    @(posedge clk) disable iff (!rst_n)
      (err_valid && !first_valid)
        |=> (first_ecc_active == $past(ecc_correction_active));
  endproperty
  assert property (p_first_ecc_captured)
    else $error("evidence: the first error's ECC context was not captured");

  // ---- P12. FORBIDDEN. err_count advances only on an error.
  property p_count_only_on_error;
    @(posedge clk) disable iff (!rst_n)
      (!err_valid) |=> (err_count == $past(err_count));
  endproperty
  assert property (p_count_only_on_error)
    else $error("evidence: err_count advanced with no error");

  // ---- 27.2 §7: publish every antecedent.
  cover property (@(posedge clk) disable iff (!rst_n) err_valid);
  cover property (@(posedge clk) disable iff (!rst_n) err_valid && err_is_read);
  cover property (@(posedge clk) disable iff (!rst_n) err_valid && !err_is_read);
  cover property (@(posedge clk) disable iff (!rst_n) err_valid && !first_valid);
  cover property (@(posedge clk) disable iff (!rst_n) err_valid &&  first_valid);
  cover property (@(posedge clk) disable iff (!rst_n) err_valid && ecc_correction_active);
  cover property (@(posedge clk) disable iff (!rst_n) clear);
  cover property (@(posedge clk) disable iff (!rst_n) first_valid);
  cover property (@(posedge clk) disable iff (!rst_n) $countones(xor_and) == 1);
  cover property (@(posedge clk) disable iff (!rst_n) $countones(xor_or)  == 1);
  cover property (@(posedge clk) disable iff (!rst_n) $countones(xor_or)  >  4);
  cover property (@(posedge clk) disable iff (!rst_n) $countones(lane_and) == 1);
  cover property (@(posedge clk) disable iff (!rst_n) err_reads != 32'd0 && err_writes == 32'd0);
  cover property (@(posedge clk) disable iff (!rst_n) err_count > 32'd1000);
endmodule

// SIMULATION-ONLY. Independent reference: it stores every error in a
// QUEUE and computes the structure by rescanning, rather than
// accumulating incrementally. A different algorithm, so agreement is
// evidence -- 27.4 §15's argument.
class evidence_reference;
  typedef struct { longint addr; longint xr; int beat; int bank; bit rd; } err_t;
  err_t log[$];

  function void record(longint addr, longint xr, int beat, int bank, bit rd);
    err_t e; e.addr = addr; e.xr = xr; e.beat = beat; e.bank = bank; e.rd = rd;
    log.push_back(e);
  endfunction

  function longint xor_or();
    longint v = 0;
    foreach (log[i]) v |= log[i].xr;
    return v;
  endfunction

  // Rescanning AND: start from the FIRST entry rather than all-ones,
  // which is the natural formulation when the data is already held --
  // and it is the check that catches §13's all-ones initialisation
  // being wrong.
  function longint xor_and();
    longint v;
    if (log.size() == 0) return 0;
    v = log[0].xr;
    foreach (log[i]) v &= log[i].xr;
    return v;
  endfunction

  function longint addr_or();
    longint v = 0;
    foreach (log[i]) v |= log[i].addr;
    return v;
  endfunction

  function longint addr_and();
    longint v;
    if (log.size() == 0) return 0;
    v = log[0].addr;
    foreach (log[i]) v &= log[i].addr;
    return v;
  endfunction

  function int beat_count(int b);
    int n = 0;
    foreach (log[i]) if (log[i].beat == b) n++;
    return n;
  endfunction

  function int reads();
    int n = 0;
    foreach (log[i]) if (log[i].rd) n++;
    return n;
  endfunction

  // §1's first error, by construction rather than by latching.
  function longint first_xor();
    if (log.size() == 0) return 0;
    return log[0].xr;
  endfunction

  function int errors(); return log.size(); endfunction
endclass

  TWO PASSING CORRUPTION INVESTIGATIONS

  (A) the evidence block was never connected
        all 12 properties            PASS
        err_count                    0
        first_valid                  0
        xor_or                       0x0000000000000000
        xor_and                      0xFFFFFFFFFFFFFFFF   <-- initial
        ------------------------------------------------
        cover err_valid              0 hits
        ... all 14 covers            0 hits

        ten of twelve properties are implications and never armed. The
        two INVARIANTS -- direction partition and ECC bound -- pass
        because 0 + 0 == 0 and 0 <= 0.

        and note xor_and reads ALL ONES, which an unwary report would
        render as "every bit failed every time". It is the
        initialisation value, and the only field that says so is
        err_count.

  (B) a confident, self-consistent, wrong conclusion
        stimulus : 4,212 errors on a device with on-die correction
                   ENABLED; nobody recorded that
        err_count                    4,212
        err_with_ecc_active          4,212
        xor_and                      0x0000000000400000   (bit 22)
        xor_or                       0x0000000000400000   (bit 22)
        lane_or                      0x04                 (lane 2)
        beat_hist                    uniform
        ------------------------------------------------
        all 12 properties            PASS
        all 14 covers                HIT

        the structure is perfect: ONE bit, every time, one lane,
        uniform across beats. SIG_STUCK_BIT. The obvious conclusion is
        a stuck path at bit 22, and a week of board and package work
        follows.

        §12 says the conclusion is unavailable. With correction
        active, the observed bit positions are a function of the fault
        pattern AND the correction applied -- and mis-correction can
        make a bit appear wrong that never failed. The underlying
        fault may be at entirely different positions.

        the classifier's bit_position_verdict() returns a REFUSAL
        here, and err_with_ecc_active == err_count is the field that
        triggers it.

    diagnosis : (A) is the vacuity case, with an extra trap: an
      all-ones AND accumulator reads like a catastrophic finding and
      is an initialisation value. (B) is §12 -- the investigation was
      not wrong about the structure, it was wrong about what the
      structure was of.

    the fix : (A) read err_count before any accumulator. (B) record
      which correction layers are active WITH the evidence, and if the
      mechanism can be disabled for a debug run, do that first -- it
      is the highest-value experiment in this chapter.