Training Failures

   bit[k]  =  classifier( observe( device( apply(setting k) ) ) )
              ^^^^^^^^^^  ^^^^^^^  ^^^^^^  ^^^^^
              judgement   capture  physics  control

   THE THREE-READBACK TEST, in order of cost

   1. does the APPLIED setting change across the sweep?
         no  -> control defect (A). The sweep never happened.
         yes -> continue.

   2. does the CAPTURED data change across the sweep?
         no  -> observation defect (B). The classifier is judging a
                constant, so every bit of the bitmap is the same bit.
         yes -> continue.

   3. did every PREREQUISITE step commit?
         no  -> ordering / prerequisite defect (C). The step under
                investigation may be blameless.
         yes -> margin hypothesis (D) is now the surviving one, and
                §18 is where it goes.

   note the order: each test is cheaper than the next and each one
   invalidates the evidence the later tests depend on. Running them
   out of order wastes the lab time you spent on the expensive one.

   sweep step = 1 tap.  window observed = 1 tap (index 4 passes).

   what the bitmap constrains:
     the good region overlaps tap 4's decision point,
     and does NOT overlap tap 3's or tap 5's.

   what it does NOT constrain:
     the width of the good region. It may be
        slightly wider than one step and badly aligned, or
        far narrower than one step and centred on tap 4.

   so the SAME bitmap is produced by a comfortable window that the
   sweep grid samples badly and by a window on the edge of failing.
   Refining the step size distinguishes them; nothing else here does.

// ---------------------------------------------------------------------
// train_diag_ledger -- CLASSIFICATION: synthesisable, BINDABLE.
//
// WHAT IT DOES: records one training step's pass bitmap plus the derived
// quantities §2's signature table needs, and latches the FIRST failure
// reason so a later cascading failure cannot overwrite the earliest
// reliable evidence.
//
// WHY IT EXISTS: §2. Eleven signatures are distinguishable only if the
// run's shape is preserved. A single pass/fail flag collapses all
// eleven into one bit, and a retry destroys even that.
//
// WHY A COUNT AND NOT A BIT PER SETTING (§7): an unstable bitmap is a
// real signature, and a one-bit-per-setting record cannot represent
// "passed 4 of 8 attempts". REPEATS>1 makes instability visible.
//
// WHY settings_tried IS PUBLISHED (§9): a timeout's bitmap is PARTIAL.
// Ten zeros after three attempts is not an all-zero signature, and
// §3's four hypotheses do not apply to it.
//
// WHAT IT CANNOT TELL YOU: which of §1's four layers failed. It records
// the classifier's verdict, not its correctness.
//
// SYNTHESIS: counters and a shift register. No DUT handle, no
// hierarchical reference; it sees the sequencer's interface only.
// ---------------------------------------------------------------------
module train_diag_ledger #(
  parameter int TAPS      = 16,   // settings in the sweep range
  parameter int LANES     = 8,
  parameter int REPEATS   = 1     // attempts per setting -- §7
)(
  input  logic                       clk,
  input  logic                       rst_n,

  // ---- sequencer interface (observed, never driven)
  input  logic                       step_start,
  input  logic                       step_done,
  input  logic                       setting_applied, // one pulse per attempt
  input  logic [$clog2(TAPS)-1:0]    setting_idx,
  input  logic                       verdict_valid,
  input  logic                       verdict_pass,
  input  logic [$clog2(LANES)-1:0]   lane_idx,
  input  logic                       committed,
  input  logic [$clog2(TAPS)-1:0]    committed_idx,
  input  logic                       timeout,
  input  logic                       prereq_committed, // §3 hypothesis C
  input  logic                       clear,            // explicit, §16

  // ---- published evidence
  output logic [TAPS-1:0]            bitmap,
  output logic [$clog2(TAPS+1)-1:0]  n_pass,
  output logic [$clog2(TAPS+1)-1:0]  settings_tried,
  output logic [$clog2(TAPS)-1:0]    first_pass,
  output logic [$clog2(TAPS)-1:0]    last_pass,
  output logic [$clog2(TAPS+1)-1:0]  windows,
  output logic                       fragmented,
  output logic                       have_pass,
  output logic [2:0]                 fail_reason,
  output logic                       fail_latched
);
  // TAPS and LANES of 1 would make $clog2 zero and every index vector
  // illegal as [-1:0]. A power-of-two test alone accepts 1, so the
  // bound is explicit. REPEATS of 0 would make the ledger record
  // nothing while reporting success.
  initial begin
    if (TAPS < 2)    $fatal(1, "train_diag_ledger: TAPS must be >= 2 (got %0d)", TAPS);
    if (LANES < 2)   $fatal(1, "train_diag_ledger: LANES must be >= 2 (got %0d)", LANES);
    if (REPEATS < 1) $fatal(1, "train_diag_ledger: REPEATS must be >= 1");
  end

  // §12's three failure states, encoded. NONE is not a failure.
  localparam logic [2:0] FR_NONE     = 3'd0;
  localparam logic [2:0] FR_NO_PASS  = 3'd1;
  localparam logic [2:0] FR_FRAGMENT = 3'd2;
  localparam logic [2:0] FR_TIMEOUT  = 3'd3;
  localparam logic [2:0] FR_PREREQ   = 3'd4;
  localparam logic [2:0] FR_STALE    = 3'd5;

  logic prev_pass;        // was the previous CLASSIFIED setting a pass?
  logic seen_any;         // has any setting been classified yet?

  always_ff @(posedge clk) begin
    if (!rst_n || clear) begin
      bitmap         <= '0;
      n_pass         <= '0;
      settings_tried <= '0;
      first_pass     <= '0;
      last_pass      <= '0;
      windows        <= '0;
      fragmented     <= 1'b0;
      have_pass      <= 1'b0;
      fail_reason    <= FR_NONE;
      fail_latched   <= 1'b0;
      prev_pass      <= 1'b0;
      seen_any       <= 1'b0;
    end else begin
      // A new step clears the per-step evidence but NOT the latched
      // failure reason -- §16. The first failure of a boot wins.
      if (step_start) begin
        bitmap         <= '0;
        n_pass         <= '0;
        settings_tried <= '0;
        windows        <= '0;
        fragmented     <= 1'b0;
        have_pass      <= 1'b0;
        prev_pass      <= 1'b0;
        seen_any       <= 1'b0;
      end

      // §9: count attempts separately from verdicts. A sweep that
      // stopped early has settings_tried < TAPS, and its zeros are
      // untried settings rather than failing ones.
      if (setting_applied && settings_tried != TAPS)
        settings_tried <= settings_tried + 1'b1;

      if (verdict_valid) begin
        seen_any <= 1'b1;
        if (verdict_pass) begin
          bitmap[setting_idx] <= 1'b1;
          if (n_pass != TAPS) n_pass <= n_pass + 1'b1;
          last_pass <= setting_idx;
          if (!have_pass) begin
            have_pass  <= 1'b1;
            first_pass <= setting_idx;
          end
          // A window OPENS on a pass whose predecessor was a fail, or
          // on the very first classified setting. Counting openings
          // rather than edges is what makes `windows` a window count
          // and not an edge count.
          if (!seen_any || !prev_pass) begin
            if (windows != TAPS) windows <= windows + 1'b1;
            // §6: two or more windows is the fragmented signature, and
            // it is sticky -- a later contiguous run must not clear it.
            if (windows >= 1) fragmented <= 1'b1;
          end
        end
        prev_pass <= verdict_pass;
      end

      // ---- FIRST failure wins, and only an explicit clear releases it.
      // §16 proves this; the ordering below is the priority, and PREREQ
      // is checked before the bitmap shapes because §3 hypothesis C
      // means the bitmap may be describing a blameless step.
      if (!fail_latched) begin
        if (step_done && !prereq_committed) begin
          fail_reason  <= FR_PREREQ;
          fail_latched <= 1'b1;
        end else if (timeout) begin
          fail_reason  <= FR_TIMEOUT;
          fail_latched <= 1'b1;
        end else if (step_done && !have_pass) begin
          fail_reason  <= FR_NO_PASS;
          fail_latched <= 1'b1;
        end else if (step_done && fragmented && committed) begin
          // Committing FROM a fragmented bitmap is a finding even
          // though the step reported success -- §13's midpoint trap.
          fail_reason  <= FR_FRAGMENT;
          fail_latched <= 1'b1;
        end
      end
    end
  end

  // Window width around the committed setting, computed combinationally
  // so it is readable the cycle after a commit. §5: a one-wide window
  // and the centre of a wide window both report success, and this is
  // the number that separates them.
  logic [$clog2(TAPS+1)-1:0] commit_window_w;
  always_comb begin
    commit_window_w = '0;
    if (committed) begin
      for (int i = 0; i < TAPS; i++)
        if (bitmap[i]) begin
          // count only the contiguous run containing committed_idx
          if (i == int'(committed_idx)) commit_window_w = commit_window_w + 1'b1;
          else if (i < int'(committed_idx)) begin
            automatic bit gap = 1'b0;
            for (int k = i; k < int'(committed_idx); k++) if (!bitmap[k]) gap = 1'b1;
            if (!gap) commit_window_w = commit_window_w + 1'b1;
          end else begin
            automatic bit gap2 = 1'b0;
            for (int k = int'(committed_idx); k < i; k++) if (!bitmap[k]) gap2 = 1'b1;
            if (!gap2) commit_window_w = commit_window_w + 1'b1;
          end
        end
    end
  end
endmodule

// ---------------------------------------------------------------------
// train_signature_classifier -- SIMULATION-ONLY.
//
// Maps §14's evidence to §11's ORDERED domain list. It deliberately
// returns several hypotheses and a next experiment, never one cause:
// §1 establishes that a bitmap is a projection of four independent
// layers onto one bit per setting, so a signature cannot identify a
// layer.
//
// WHAT IT DOES NOT MODEL: the device, the channel, any electrical
// quantity, or the classifier whose verdicts it is reading.
//
// WHAT IT WOULD MISS: two different faults with the same signature.
// That is not a bug in this class; it is the projection.
// ---------------------------------------------------------------------
typedef enum {
  SIG_OK, SIG_NO_PASS, SIG_ALL_PASS, SIG_SINGLE, SIG_NARROW,
  SIG_FRAGMENTED, SIG_TIMEOUT_PARTIAL, SIG_UNSTABLE, SIG_EDGE_PICK
} train_sig_e;

// §11's six domains, in the cheapest-first order that table establishes.
typedef enum {
  DOM_CONTROL, DOM_OBSERVATION, DOM_CONFIG, DOM_ORDERING,
  DOM_STALE, DOM_PHYSICAL
} train_domain_e;

class train_evidence;
  int taps;
  int n_pass;
  int settings_tried;
  int first_pass;
  int last_pass;
  int windows;
  bit fragmented;
  bit have_pass;
  bit timed_out;
  bit prereq_committed;
  bit committed;
  int committed_idx;
  int commit_window_w;
  int repeats;            // §7
  int min_repeat_passes;  // lowest pass count over repeats at any setting
  int max_repeat_passes;
endclass


class train_signature_classifier;

  // §9: a partial bitmap is not a margin result. Checked FIRST, because
  // every shape below assumes the sweep completed.
  function train_sig_e signature(train_evidence e);
    if (e.timed_out || e.settings_tried < e.taps) return SIG_TIMEOUT_PARTIAL;
    // §7: instability outranks shape, because an unstable bitmap has no
    // stable shape to classify.
    if (e.repeats > 1 && e.min_repeat_passes != e.max_repeat_passes)
      return SIG_UNSTABLE;
    if (!e.have_pass)             return SIG_NO_PASS;
    if (e.n_pass == e.taps)       return SIG_ALL_PASS;
    if (e.fragmented)             return SIG_FRAGMENTED;
    if (e.n_pass == 1)            return SIG_SINGLE;
    if (e.n_pass <= 3)            return SIG_NARROW;
    // §11 signature 10: a commit within one of the outermost settings
    // of its own window is an edge pick.
    if (e.committed && e.commit_window_w >= 3 &&
        (e.committed_idx == e.first_pass || e.committed_idx == e.last_pass))
      return SIG_EDGE_PICK;
    return SIG_OK;
  endfunction

  // The ordered domain list. §11: cheapest-first, and each domain
  // invalidates the evidence for the ones after it.
  function void hypotheses(train_evidence e, ref train_domain_e out[$]);
    train_sig_e s = signature(e);
    out.delete();
    // Ordering is checked before anything else whenever the prerequisite
    // is known not to have committed -- §3 hypothesis C, the module's
    // second law.
    if (!e.prereq_committed) out.push_back(DOM_ORDERING);
    case (s)
      SIG_NO_PASS: begin
        out.push_back(DOM_CONTROL);
        out.push_back(DOM_OBSERVATION);
        out.push_back(DOM_CONFIG);
        out.push_back(DOM_PHYSICAL);   // last: §11's argument
      end
      SIG_ALL_PASS: begin
        // §4: this signature is about the INSTRUMENT, so no physical
        // hypothesis is offered at all. A non-discriminating classifier
        // makes every margin statement unavailable.
        out.push_back(DOM_OBSERVATION);
        out.push_back(DOM_CONFIG);
      end
      SIG_SINGLE, SIG_NARROW: begin
        out.push_back(DOM_CONFIG);     // §5: step size first
        out.push_back(DOM_PHYSICAL);
      end
      SIG_FRAGMENTED: begin
        out.push_back(DOM_CONFIG);     // §6: aliasing / sweep origin
        out.push_back(DOM_OBSERVATION);
        out.push_back(DOM_PHYSICAL);
      end
      SIG_TIMEOUT_PARTIAL: begin
        out.push_back(DOM_CONTROL);
        out.push_back(DOM_CONFIG);
      end
      SIG_UNSTABLE: begin
        out.push_back(DOM_CONFIG);
        out.push_back(DOM_STALE);
        out.push_back(DOM_PHYSICAL);
      end
      SIG_EDGE_PICK: out.push_back(DOM_CONFIG);
      default: ;                        // SIG_OK offers no hypothesis
    endcase
  endfunction

  // The discriminating experiment §11 requires: a named action WITH the
  // two outcomes that separate the leading hypotheses. An action with
  // no predicted outcomes is random tweaking.
  function string next_experiment(train_evidence e);
    case (signature(e))
      SIG_NO_PASS:
        return "read back the applied setting across the sweep; unchanged => control defect, changing => continue to captured data";
      SIG_ALL_PASS:
        return "apply a setting known to be bad; still passes => classifier proven non-discriminating, fails => widen the sweep range";
      SIG_SINGLE, SIG_NARROW:
        return "halve the step and re-sweep the neighbourhood; window grows proportionally => sampling artefact, stays one fine step => real at this granularity";
      SIG_FRAGMENTED:
        return "rotate the sweep start point; windows join => aliasing across a cyclic range, stay disjoint => two genuine regions";
      SIG_TIMEOUT_PARTIAL:
        return "raise the budget and re-run; completes => budget or liveness, stops at the same index => sweep stuck at that index";
      SIG_UNSTABLE:
        return "repeat each setting N times and count; a 50/50 setting => classifier threshold, first repeat differs only => uncontrolled prior state";
      SIG_EDGE_PICK:
        return "re-run the chooser on the recorded bitmap; picks the same edge => chooser defect, picks the centre => bitmap changed between runs";
      default:
        return "no signature: do not change settings";
    endcase
  endfunction

  // §1's boundary, enforced in code. No method here returns a physical
  // cause, and this one exists so a caller cannot ask for one.
  function string physical_verdict(train_evidence e);
    return "unavailable: a pass bitmap is a digital sample of a classifier's decision, not a measurement of eye height or width (§1, §18)";
  endfunction

  // §11's last row: the physical hypothesis is admissible only when the
  // five cheaper domains have been excluded BY EXPERIMENT, which is a
  // fact about the investigation and cannot be derived from a bitmap.
  function bit physical_hypothesis_admissible(
      bit control_excluded, bit observation_excluded,
      bit config_excluded, bit ordering_excluded, bit stale_excluded);
    return control_excluded && observation_excluded && config_excluded
        && ordering_excluded && stale_excluded;
  endfunction
endclass

// Bound to §14's ledger. Every property is guarded by `disable iff`, and
// every antecedent is published as a cover below -- 27.2 measured this
// curriculum at 78.53% implications, so a silent pass is otherwise
// indistinguishable from a property that never armed.
module train_diag_ledger_sva #(
  parameter int TAPS = 16
)(
  input logic clk, rst_n,
  input logic step_start, step_done, setting_applied, verdict_valid,
  input logic verdict_pass, committed, timeout, prereq_committed, clear,
  input logic [TAPS-1:0]           bitmap,
  input logic [$clog2(TAPS+1)-1:0] n_pass, settings_tried, windows,
  input logic                      fragmented, have_pass, fail_latched,
  input logic [2:0]                fail_reason
);
  // ---- P1. FIRST FAILURE WINS. Once latched, the reason is stable
  // until an explicit clear. This is the module's third and fourth laws
  // in one property: a later cascading failure must not overwrite the
  // earliest reliable evidence.
  property p_first_failure_sticky;
    @(posedge clk) disable iff (!rst_n)
      (fail_latched && !clear) |=> (fail_reason == $past(fail_reason));
  endproperty
  assert property (p_first_failure_sticky)
    else $error("ledger: latched failure reason changed without a clear");

  // ---- P2. FORBIDDEN. A new step must not release the latch. Only
  // `clear` does. Without this, a retry erases the evidence.
  property p_step_start_does_not_clear_latch;
    @(posedge clk) disable iff (!rst_n)
      (step_start && fail_latched && !clear) |=> fail_latched;
  endproperty
  assert property (p_step_start_does_not_clear_latch)
    else $error("ledger: step_start released the failure latch");

  // ---- P3. Clear actually clears. A latch with no release is a
  // one-shot register that silently stops recording after boot.
  property p_clear_releases;
    @(posedge clk) disable iff (!rst_n)
      clear |=> (!fail_latched && fail_reason == 3'd0);
  endproperty
  assert property (p_clear_releases)
    else $error("ledger: clear did not release the latch");

  // ---- P4. n_pass counts verdicts, not attempts. §9: collapsing the
  // two makes a partial bitmap look like a margin result.
  property p_npass_only_on_pass;
    @(posedge clk) disable iff (!rst_n)
      (verdict_valid && !verdict_pass) |=> (n_pass == $past(n_pass));
  endproperty
  assert property (p_npass_only_on_pass)
    else $error("ledger: n_pass advanced on a failing verdict");

  // ---- P5. settings_tried counts attempts, not verdicts.
  property p_tried_on_apply;
    @(posedge clk) disable iff (!rst_n)
      (setting_applied && settings_tried != TAPS)
        |=> (settings_tried == $past(settings_tried) + 1);
  endproperty
  assert property (p_tried_on_apply)
    else $error("ledger: settings_tried did not advance on an attempt");

  // ---- P6. FORBIDDEN. n_pass never exceeds settings_tried. A bitmap
  // reporting more passes than attempts is arithmetically impossible
  // and indicates the two are being driven from one event.
  property p_pass_le_tried;
    @(posedge clk) disable iff (!rst_n)
      (n_pass <= settings_tried);
  endproperty
  assert property (p_pass_le_tried)
    else $error("ledger: n_pass %0d exceeds settings_tried %0d", n_pass, settings_tried);

  // ---- P7. INVARIANT. n_pass never exceeds the sweep width. The
  // counter is sized for TAPS+1 values precisely so this cannot wrap
  // silently -- COUNT versus INDEX.
  property p_npass_bounded;
    @(posedge clk) disable iff (!rst_n)
      (n_pass <= TAPS);
  endproperty
  assert property (p_npass_bounded)
    else $error("ledger: n_pass exceeded TAPS");

  // ---- P8. have_pass is sticky within a step. §14: first_pass must
  // keep the FIRST index, so the flag that guards it cannot drop.
  property p_have_pass_sticky;
    @(posedge clk) disable iff (!rst_n)
      (have_pass && !step_start && !clear) |=> have_pass;
  endproperty
  assert property (p_have_pass_sticky)
    else $error("ledger: have_pass dropped mid-step");

  // ---- P9. FORBIDDEN. fragmented is sticky: a later contiguous run
  // must not clear it. §6 -- a run that committed from a fragmented
  // bitmap has to stay distinguishable afterwards.
  property p_fragmented_sticky;
    @(posedge clk) disable iff (!rst_n)
      (fragmented && !step_start && !clear) |=> fragmented;
  endproperty
  assert property (p_fragmented_sticky)
    else $error("ledger: fragmented dropped without a new step");

  // ---- P10. fragmented implies at least two windows, and conversely.
  // The two must agree or `fragmented` is decoration.
  property p_fragmented_matches_windows;
    @(posedge clk) disable iff (!rst_n)
      fragmented |-> (windows >= 2);
  endproperty
  assert property (p_fragmented_matches_windows)
    else $error("ledger: fragmented asserted with windows=%0d", windows);

  // ---- P11. FORBIDDEN. A prerequisite failure outranks every bitmap
  // shape. §3 hypothesis C: the bitmap may describe a blameless step,
  // so the reason must be PREREQ and not NO_PASS.
  property p_prereq_outranks_shape;
    @(posedge clk) disable iff (!rst_n)
      (step_done && !prereq_committed && !$past(fail_latched))
        |=> (fail_reason == 3'd4);
  endproperty
  assert property (p_prereq_outranks_shape)
    else $error("ledger: prerequisite failure did not outrank the bitmap shape");

  // ---- P12. FORBIDDEN. Committing from a fragmented bitmap is
  // recorded as a finding even though the step reported success --
  // §13's midpoint trap, which otherwise reports a clean commit.
  property p_fragment_commit_recorded;
    @(posedge clk) disable iff (!rst_n)
      (step_done && fragmented && committed && !$past(fail_latched))
        |=> fail_latched;
  endproperty
  assert property (p_fragment_commit_recorded)
    else $error("ledger: a commit from a fragmented bitmap was not recorded");

  // ---- 27.2 §7: publish every antecedent. Without these the twelve
  // properties above are indistinguishable from a bound checker whose
  // sequencer was never connected.
  cover property (@(posedge clk) disable iff (!rst_n) step_start);
  cover property (@(posedge clk) disable iff (!rst_n) step_done);
  cover property (@(posedge clk) disable iff (!rst_n) setting_applied);
  cover property (@(posedge clk) disable iff (!rst_n) verdict_valid && verdict_pass);
  cover property (@(posedge clk) disable iff (!rst_n) verdict_valid && !verdict_pass);
  cover property (@(posedge clk) disable iff (!rst_n) committed);
  cover property (@(posedge clk) disable iff (!rst_n) timeout);
  cover property (@(posedge clk) disable iff (!rst_n) clear);
  cover property (@(posedge clk) disable iff (!rst_n) fail_latched);
  cover property (@(posedge clk) disable iff (!rst_n) fragmented);
  // The signature-specific covers: each is one of §2's rows, and an
  // empty bin means that signature was never exercised.
  cover property (@(posedge clk) disable iff (!rst_n) step_done && !have_pass);
  cover property (@(posedge clk) disable iff (!rst_n) step_done && (n_pass == TAPS));
  cover property (@(posedge clk) disable iff (!rst_n) step_done && (n_pass == 1));
  cover property (@(posedge clk) disable iff (!rst_n) step_done && fragmented && committed);
  cover property (@(posedge clk) disable iff (!rst_n) step_done && !prereq_committed);
endmodule

// ---------------------------------------------------------------------
// bitmap_reference -- SIMULATION-ONLY independent reference for §14.
//
// WHY A DIFFERENT ALGORITHM: the ledger derives windows and
// fragmentation in ONE streaming pass, incrementally, as verdicts
// arrive. This model rescans the FINISHED bitmap for contiguous runs.
// Two different algorithms agreeing is evidence; the same algorithm
// written twice is a restatement -- 27.4 §15's argument.
//
// WHAT IT DOES NOT MODEL: the sequencer, classifier, or device.
//
// WHAT IT WOULD MISS: an error both implementations make identically.
// They share the bitmap, so a corrupted bitmap agrees with itself.
// ---------------------------------------------------------------------
class bitmap_reference #(parameter int TAPS = 16);

  // Contiguous runs of set bits, rescanned from the finished bitmap.
  function int windows(logic [TAPS-1:0] bm);
    int n = 0;
    bit prev = 1'b0;
    for (int i = 0; i < TAPS; i++) begin
      if (bm[i] && !prev) n++;
      prev = bm[i];
    end
    return n;
  endfunction

  function bit fragmented(logic [TAPS-1:0] bm);
    return windows(bm) >= 2;
  endfunction

  function int n_pass(logic [TAPS-1:0] bm);
    int n = 0;
    for (int i = 0; i < TAPS; i++) if (bm[i]) n++;
    return n;
  endfunction

  // Returns -1 when the bitmap is empty, so "no pass" is a distinct
  // answer rather than index 0 -- the same three-valued discipline
  // 27.3 §6 and 27.4 §2 arrived at, here for an index.
  function int first_pass(logic [TAPS-1:0] bm);
    for (int i = 0; i < TAPS; i++) if (bm[i]) return i;
    return -1;
  endfunction

  function int last_pass(logic [TAPS-1:0] bm);
    for (int i = TAPS - 1; i >= 0; i--) if (bm[i]) return i;
    return -1;
  endfunction

  // §5: the width of the contiguous run CONTAINING idx -- not the span
  // between the outermost passes, which §13 shows can straddle a gap.
  function int commit_window(logic [TAPS-1:0] bm, int idx);
    int lo, hi;
    if (idx < 0 || idx >= TAPS || !bm[idx]) return 0;
    lo = idx; while (lo > 0        && bm[lo-1]) lo--;
    hi = idx; while (hi < TAPS - 1 && bm[hi+1]) hi++;
    return hi - lo + 1;
  endfunction

  // §13's trap, computed so a test can assert it is NOT what the
  // chooser used: the midpoint of the outermost-pass span.
  function int span_midpoint(logic [TAPS-1:0] bm);
    int f = first_pass(bm), l = last_pass(bm);
    if (f < 0) return -1;
    return (f + l) / 2;
  endfunction

  function bit span_midpoint_is_failing(logic [TAPS-1:0] bm);
    int mid = span_midpoint(bm);
    if (mid < 0) return 1'b0;
    return !bm[mid];
  endfunction
endclass

  A BOUND LEDGER THAT PROVED NOTHING

  stimulus : the ledger is bound, reset is released, and the training
             sequencer is never started
  p_first_failure_sticky            PASS
  p_step_start_does_not_clear_latch PASS
  p_clear_releases                  PASS
  p_npass_only_on_pass              PASS
  p_tried_on_apply                  PASS
  p_pass_le_tried                   PASS
  p_npass_bounded                   PASS
  p_have_pass_sticky                PASS
  p_fragmented_sticky               PASS
  p_fragmented_matches_windows      PASS
  p_prereq_outranks_shape           PASS
  p_fragment_commit_recorded        PASS
  ------------------------------------------------
  cover step_start                  0 hits
  cover verdict_valid && pass       0 hits
  cover verdict_valid && !pass      0 hits
  cover fail_latched                0 hits
  cover fragmented                  0 hits
  ... all 15 covers                 0 hits

  ten of the twelve properties are implications, so with no sweep they
  never arm. The two INVARIANTS -- p_pass_le_tried and
  p_npass_bounded -- also pass, correctly: zero never exceeds zero.

  diagnosis : this is 27.2's vacuity argument in a debug block. The
    covers are the only thing separating a working ledger from an
    unconnected one, and a boot log showing "training diagnostics:
    no failures recorded" is produced by BOTH.

  the fix : read the covers, not the asserts. A ledger whose
    step_start cover is empty recorded nothing because nothing ran --
    which is a different finding from a clean training pass, and the
    module's first law says the difference matters.