"CRC Provides Security"

R(m) = m(x) · x³² mod G(x)      over GF(2)
G(x) = x³² + x²⁶ + x²³ + x²² + x¹⁶ + x¹² + x¹¹ + x¹⁰ + x⁸ + x⁷ + x⁵ + x⁴ + x² + x + 1

addition in GF(2) is XOR, and polynomial multiplication distributes over it:
  (a ⊕ b) · x³² = (a · x³²) ⊕ (b · x³²)

the remainder of a sum is the sum of the remainders:
  ((a ⊕ b) · x³²) mod G = ((a · x³²) mod G) ⊕ ((b · x³²) mod G)

therefore:
  R(a ⊕ b) = R(a) ⊕ R(b)

FCS(m ⊕ d) = FCS(m) ⊕ R₀(d)

// ---------------------------------------------------------------------
// crcsec_pkg -- the constants an integrity argument needs, with the
// polynomial taken from Chapter 6.2 Section 4 and every derived figure
// computed here rather than written as a literal.
//
// Units: Chapter 23.3 Section 2's bitcell equivalent for STATE, and
// gate equivalents for LOGIC. Section 19 explains why this chapter
// needs both and the previous eight needed one.
//   1 BCE = 0.35 GE = one bit of usable on-die SRAM
//   1 flip-flop = 7 GE = 20 BCE
//   Chapter 19.7 Section 19's MAC receive datapath = 283 320 BCE
// ---------------------------------------------------------------------
package crcsec_pkg;

  localparam int unsigned DATAPATH_BCE = 283_320;
  localparam int unsigned BCE_PER_FLOP = 20;
  localparam int unsigned GE_PER_FLOP  = 7;
  localparam int unsigned GE_PER_XOR   = 3;      // 2-input XOR, rounded up

  // ---- the generator, Chapter 6.2 Section 4 ---------------------------
  // x^32 implicit; the stored value is the low 32 terms.
  localparam logic [31:0] CRC32_POLY = 32'h04C1_1DB7;
  localparam int unsigned CRC_WIDTH  = 32;

  // ---- Chapter 6.1's guarantees, with their bounds --------------------
  localparam int unsigned BURST_BOUND_BITS   = 32;
  localparam int unsigned WEIGHT3_ANY_LENGTH = 3;
  localparam int unsigned WEIGHT4_MAX_OCTETS = 375;

  // ---- MACsec, 802.1AE -------------------------------------------------
  localparam int unsigned SECTAG_NO_SCI   = 8;
  localparam int unsigned SECTAG_WITH_SCI = 16;
  localparam int unsigned ICV_OCTETS      = 16;
  localparam int unsigned AES_BLOCK_BITS  = 128;
  localparam int unsigned AES_ROUNDS      = 10;   // AES-128

  // ---- a gate model for the two mechanisms ----------------------------
  // Derived, not quoted: an S-box optimised for a pipelined datapath,
  // MixColumns as four column circuits, AddRoundKey as 128 XORs.
  localparam int unsigned SBOX_GE      = 400;
  localparam int unsigned MIXCOL_GE    = 800;     // 4 columns x 200
  localparam int unsigned GHASH_GE     = 17_000;  // Karatsuba + reduction
  // Chapter 19.4 Section 6's 512-bit engine, re-read: 19 461 XOR terms
  // across both cores and about 70 flops of state.
  localparam int unsigned CRC_XOR_TERMS = 19_461;
  localparam int unsigned CRC_FLOPS     = 70;

  typedef enum logic [1:0] {
    THREAT_NOISE     = 2'd0,   // Chapter 6.1's channel
    THREAT_FAULT     = 2'd1,   // a broken device, no intent
    THREAT_CHOSEN    = 2'd2    // a difference pattern somebody selected
  } threat_e;

  // ---- the polynomial division, one bit, no conventions ---------------
  function automatic logic [31:0] crc_step(logic [31:0] state, logic bit_in);
    logic fb;
    fb = state[31] ^ bit_in;
    return fb ? ((state << 1) ^ CRC32_POLY) : (state << 1);
  endfunction

  // R0(d): the pure remainder of a difference pattern, zero init, no
  // complement. Section 4 shows this IS the compensating delta.
  function automatic logic [31:0] r0(logic [1023:0] d, int unsigned nbits);
    logic [31:0] s;
    s = '0;
    for (int i = 0; i < nbits; i++) s = crc_step(s, d[i]);
    return s;
  endfunction

  // ---- derived gate counts ---------------------------------------------
  function automatic int unsigned aes_round_ge();
    return (16 * SBOX_GE) + MIXCOL_GE + (AES_BLOCK_BITS * GE_PER_XOR);
  endfunction

  function automatic int unsigned aes_pipeline_ge();
    return (AES_ROUNDS * aes_round_ge())
         + (AES_ROUNDS * AES_BLOCK_BITS * GE_PER_FLOP);
  endfunction

  function automatic int unsigned gcm_pipeline_ge();
    return aes_pipeline_ge() + GHASH_GE;
  endfunction

  function automatic int unsigned crc_engine_ge();
    return (CRC_XOR_TERMS * GE_PER_XOR) + (CRC_FLOPS * GE_PER_FLOP);
  endfunction

  function automatic int unsigned datapaths_milli(int unsigned bce);
    return (bce * 1000) / DATAPATH_BCE;
  endfunction

endpackage

// ---------------------------------------------------------------------
// crc_difference_model -- Section 2's linearity, measured.
//
// It computes the check value of a frame, of a difference pattern, and
// of their exclusive-or, and asserts that the third equals the first
// two combined. The output that matters is linearity_holds, which is
// always high and is the chapter's entire subject.
// ---------------------------------------------------------------------
module crc_difference_model
  import crcsec_pkg::*;
(
  input  logic          clk,
  input  logic          rst_n,

  input  logic          eval,
  input  logic [1023:0] frame_bits,
  input  logic [1023:0] diff_bits,
  input  logic [15:0]   nbits,

  output logic [31:0]   r_frame,
  output logic [31:0]   r_diff,
  output logic [31:0]   r_combined,
  output logic [31:0]   r_expected,
  output logic          linearity_holds,
  output logic          diff_is_nonzero,
  output logic [15:0]   diff_weight,
  output logic [15:0]   diff_span_bits,
  output logic          within_burst_bound,
  output logic [31:0]   c_evaluations
);
  logic [1023:0] combined;
  int unsigned   lo, hi;

  always_comb begin
    combined = frame_bits ^ diff_bits;

    r_frame    = r0(frame_bits, int'(nbits));
    r_diff     = r0(diff_bits,  int'(nbits));
    r_combined = r0(combined,   int'(nbits));

    // Section 2's identity, evaluated rather than asserted in prose.
    r_expected      = r_frame ^ r_diff;
    linearity_holds = (r_combined == r_expected);

    diff_is_nonzero = (diff_bits != '0);

    diff_weight = '0;
    for (int i = 0; i < 1024; i++)
      if (diff_bits[i]) diff_weight = diff_weight + 16'd1;

    // The span between the first and last set bit -- Chapter 6.1's
    // burst length, which is what the 32-bit bound is about.
    lo = 1024; hi = 0;
    for (int i = 0; i < 1024; i++) begin
      if (diff_bits[i]) begin
        if (i < lo) lo = i;
        if (i > hi) hi = i;
      end
    end
    diff_span_bits = diff_is_nonzero ? 16'(hi - lo + 1) : 16'd0;

    within_burst_bound = diff_is_nonzero
                      && (diff_span_bits <= 16'(BURST_BOUND_BITS));
  end

  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n)    c_evaluations <= '0;
    else if (eval) c_evaluations <= c_evaluations + 32'd1;
  end
endmodule

a frame m has check value FCS(m), and the receiver verifies it
somebody changes the payload:  m becomes m ⊕ d
by Section 2's identity:        FCS(m ⊕ d) = FCS(m) ⊕ R₀(d)
so the altered frame's check value is computable from d alone

// ---------------------------------------------------------------------
// compensating_delta -- Section 4's construction as a model, so a
// verification environment can demonstrate that a chosen difference
// leaves the check satisfied.
//
// It is an ELABORATION and TESTBENCH model. Its purpose is to make the
// design's integrity claim falsifiable: a design asserting that a
// passing FCS implies an unaltered frame can be shown wrong here, at
// no cost and on no real network.
//
// The output that matters is check_still_passes, which is hard-wired
// high for any nonzero difference. That constant IS the myth's refutation.
// ---------------------------------------------------------------------
module compensating_delta
  import crcsec_pkg::*;
(
  input  logic          clk,
  input  logic          rst_n,

  input  logic          eval,
  input  logic [31:0]   fcs_original,
  input  logic [1023:0] diff_bits,
  input  logic [15:0]   nbits,
  input  logic  [1:0]   threat,          // threat_e

  output logic [31:0]   delta,
  output logic [31:0]   fcs_compensated,
  output logic          check_still_passes,
  output logic          requires_a_secret,
  output logic          inputs_are_all_public,
  output logic [15:0]   bits_of_secret_available,
  output logic [31:0]   detection_prob_recip,   // 1 in N, for noise
  output logic [31:0]   c_compensations
);
  always_comb begin
    // Section 4 line 3: the compensating value is R0 of the difference.
    delta           = r0(diff_bits, int'(nbits));
    fcs_compensated = fcs_original ^ delta;

    // For a CHOSEN difference, the compensated frame verifies. For a
    // difference the channel produced, nobody computed the delta and
    // the check does its job.
    check_still_passes = (threat == 2'(THREAT_CHOSEN)) && (diff_bits != '0);

    // THE structural facts.
    requires_a_secret        = 1'b0;   // the CRC needs none
    inputs_are_all_public    = 1'b1;   // polynomial, frame, FCS
    bits_of_secret_available = 16'd0;

    // Chapter 6.1 Section 6: the residual for a pattern outside the
    // deterministic classes. Meaningful for noise, meaningless for a
    // chosen difference, and reported as such.
    detection_prob_recip = (threat == 2'(THREAT_CHOSEN))
                         ? 32'd1              // 1 in 1 -- it passes
                         : 32'hFFFF_FFFF;     // 1 in 4 294 967 295+
  end

  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n)    c_compensations <= '0;
    else if (eval) c_compensations <= c_compensations + 32'd1;
  end
endmodule

// ---------------------------------------------------------------------
// guarantee_model -- Chapter 6.1's four clauses as a classifier, so a
// difference pattern can be placed against them before its outcome is
// examined.
//
// The output that matters is guarantee_applies. When it is low the
// frame is in the residual class, and the residual is meaningful only
// if the difference was not chosen -- which is the input this module
// cannot compute and Section 9's model supplies.
// ---------------------------------------------------------------------
module guarantee_model
  import crcsec_pkg::*;
(
  input  logic        clk,
  input  logic        rst_n,

  input  logic        eval,
  input  logic [15:0] diff_span_bits,
  input  logic [15:0] diff_weight,
  input  logic [15:0] frame_octets,
  input  logic  [1:0] threat,

  output logic        in_burst_class,
  output logic        in_weight3_class,
  output logic        in_weight4_class,
  output logic        guarantee_applies,
  output logic        residual_class,
  output logic [31:0] residual_recip,
  output logic        residual_is_meaningful,
  output logic        provenance_observable,
  output logic [31:0] c_guaranteed,
  output logic [31:0] c_residual
);
  always_comb begin
    // Chapter 6.1 Section 5, clause by clause.
    in_burst_class   = (diff_span_bits != 16'd0)
                    && (diff_span_bits <= 16'(BURST_BOUND_BITS));

    in_weight3_class = (diff_weight != 16'd0)
                    && (diff_weight <= 16'(WEIGHT3_ANY_LENGTH));

    in_weight4_class = (diff_weight == 16'd4)
                    && (frame_octets <= 16'(WEIGHT4_MAX_OCTETS));

    guarantee_applies = in_burst_class || in_weight3_class || in_weight4_class;
    residual_class    = (diff_span_bits != 16'd0) && !guarantee_applies;

    // 2^-32, expressed as one in N.
    residual_recip = 32'hFFFF_FFFF;

    // THE qualification. The residual describes an ARBITRARY remainder.
    // A chosen difference does not have one.
    residual_is_meaningful = residual_class && (threat != 2'(THREAT_CHOSEN));

    // And the fact that makes the qualification unenforceable in
    // hardware: nothing in the frame says where the difference came from.
    provenance_observable = 1'b0;
  end

  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin
      c_guaranteed <= '0; c_residual <= '0;
    end else if (eval) begin
      if (guarantee_applies) c_guaranteed <= c_guaranteed + 32'd1;
      if (residual_class)    c_residual   <= c_residual + 32'd1;
    end
  end
endmodule

2⁻³² ÷ 2⁻¹²⁸ = 2⁹⁶ = 7.92 × 10²⁸

// ---------------------------------------------------------------------
// adversary_model -- what a mechanism's guarantee evaluates to when the
// difference pattern is chosen rather than sampled.
//
// It is a MODEL used to reason about a design's claims. It computes no
// frames and drives no interface; its outputs are a classification of
// what each mechanism promises under each threat.
//
// The output that matters is guarantee_survives, which is zero for
// every public mechanism and one for a keyed one -- and the field that
// decides it is key_bits.
// ---------------------------------------------------------------------
module adversary_model
  import crcsec_pkg::*;
(
  input  logic        clk,
  input  logic        rst_n,

  input  logic        eval,
  input  logic  [1:0] threat,
  input  logic [15:0] check_width_bits,
  input  logic [15:0] key_bits,
  input  logic        check_inputs_public,
  input  logic [15:0] stacked_public_checks,

  output logic        guarantee_survives,
  output logic [15:0] effective_security_bits,
  output logic [15:0] compensation_steps,
  output logic        widening_helps,
  output logic        stacking_helps,
  output logic        only_a_key_helps,
  output logic [31:0] c_chosen,
  output logic [31:0] c_noise
);
  always_comb begin
    // A mechanism resists a chosen difference only if something about
    // it is withheld. Width is not withheld; a key is.
    guarantee_survives = (threat != 2'(THREAT_CHOSEN)) || (key_bits != 16'd0);

    effective_security_bits = (threat == 2'(THREAT_CHOSEN))
                            ? key_bits          // zero for a CRC
                            : check_width_bits; // 32, against noise

    // Section 5's production note, as arithmetic: n public checks cost
    // n compensations, which is linear and therefore not a defence.
    compensation_steps = check_inputs_public ? stacked_public_checks : 16'hFFFF;

    // The three answers a design review needs.
    widening_helps = (threat != 2'(THREAT_CHOSEN));
    stacking_helps = 1'b0;
    only_a_key_helps = (threat == 2'(THREAT_CHOSEN));
  end

  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin
      c_chosen <= '0; c_noise <= '0;
    end else if (eval) begin
      if (threat == 2'(THREAT_CHOSEN)) c_chosen <= c_chosen + 32'd1;
      else                             c_noise  <= c_noise + 32'd1;
    end
  end
endmodule

19 461 XOR × 3 GE + 70 flops × 7 GE = 58 873 GE

// ---------------------------------------------------------------------
// macsec_overhead_model -- what protection costs on the wire and in
// state, derived from the SecTAG and ICV sizes rather than quoted.
//
// The output that matters is wire_cost_ppm, because it is the number
// that decides whether a deployment can afford protection on its
// traffic mix -- and it is Chapter 8.3's hyperbola with a bigger
// constant, so the answer depends entirely on the frame size.
// ---------------------------------------------------------------------
module macsec_overhead_model
  import crcsec_pkg::*;
(
  input  logic        clk,
  input  logic        rst_n,

  input  logic [15:0] payload_octets,
  input  logic        include_sci,
  input  logic [15:0] associations,
  input  logic [15:0] ports,
  input  logic [15:0] rate_gbps,

  output logic [15:0] sectag_octets,
  output logic [15:0] overhead_octets,
  output logic [31:0] wire_unprotected,
  output logic [31:0] wire_protected,
  output logic [31:0] wire_cost_ppm,
  output logic [31:0] eff_unprotected_ppm,
  output logic [31:0] eff_protected_ppm,
  output logic [31:0] sa_state_bce,
  output logic [31:0] sa_state_dp_milli,
  output logic [15:0] pipelines_needed,
  output logic [31:0] gcm_ge,
  output logic [31:0] crc_ge,
  output logic [15:0] gate_ratio_x100
);
  logic [31:0] blocks_per_s_m;   // millions of 128-bit blocks per second

  always_comb begin
    sectag_octets   = include_sci ? 16'(SECTAG_WITH_SCI)
                                  : 16'(SECTAG_NO_SCI);
    overhead_octets = sectag_octets + 16'(ICV_OCTETS);

    // Chapter 24.3 Section 1's 38 fixed octets, plus the protection.
    wire_unprotected = 32'(payload_octets) + 32'd38;
    wire_protected   = wire_unprotected + 32'(overhead_octets);

    wire_cost_ppm = (wire_unprotected == 0) ? 32'd0
                  : ((32'(overhead_octets) * 1_000_000) / wire_unprotected);

    eff_unprotected_ppm = (wire_unprotected == 0) ? 32'd0
                        : ((32'(payload_octets) * 1_000_000) / wire_unprotected);
    eff_protected_ppm   = (wire_protected == 0) ? 32'd0
                        : ((32'(payload_octets) * 1_000_000) / wire_protected);

    // State: the one quantity BCE prices without argument.
    sa_state_bce      = 32'd288 * 32'(associations) * 32'(ports);
    sa_state_dp_milli = 32'(datapaths_milli(sa_state_bce));

    // Throughput: 128-bit blocks per second against a 1 GHz core.
    blocks_per_s_m   = (32'(rate_gbps) * 1000) / 32'(AES_BLOCK_BITS);
    pipelines_needed = 16'((blocks_per_s_m + 999) / 1000);

    gcm_ge = 32'(pipelines_needed) * 32'(gcm_pipeline_ge());
    crc_ge = 32'(crc_engine_ge());

    gate_ratio_x100 = (crc_ge == 0) ? 16'd0
                    : 16'((gcm_ge * 32'd100) / crc_ge);
  end
endmodule

octet 0            6            12       14                    end−16   end−4
      +------------+------------+--------+----------------------+--------+----+
      | destination| source     | 0x88E5 |  SecTAG + protected  |  ICV   |FCS |
      +------------+------------+--------+----------------------+--------+----+
                                 ^ MACsec EtherType             ^ 16 octets

// ---------------------------------------------------------------------
// protected_parser -- Chapter 25.1's parse window meeting a MACsec
// boundary, and the two different reasons a parse stops.
//
// The output that matters is the pair stopped_by_budget and
// stopped_by_protection. A design that reports them through one bit has
// conflated a limit it could raise with a guarantee it bought.
// ---------------------------------------------------------------------
module protected_parser
  import crcsec_pkg::*;
#(
  parameter int unsigned WINDOW_OCTETS = 64,
  parameter int unsigned MAX_TAGS      = 2
)(
  input  logic        clk,
  input  logic        rst_n,

  input  logic        frame_start,
  input  logic        octet_valid,
  input  logic [15:0] octet_index,
  input  logic [15:0] type_at_cursor,
  input  logic        type_valid,
  input  logic        have_key,

  output logic [15:0] cursor,
  output logic [15:0] tags_seen,
  output logic        is_vlan,
  output logic        is_macsec,
  output logic        reached_payload_type,
  output logic        stopped_by_budget,
  output logic        stopped_by_protection,
  output logic        classification_available,
  output logic [15:0] visible_fields_mask,
  output logic [31:0] c_protected_frames,
  output logic [31:0] c_budget_stops
);
  localparam logic [15:0] ET_VLAN   = 16'h8100;
  localparam logic [15:0] ET_SVLAN  = 16'h88A8;
  localparam logic [15:0] ET_MACSEC = 16'h88E5;

  always_comb begin
    is_vlan   = type_valid && ((type_at_cursor == ET_VLAN) ||
                               (type_at_cursor == ET_SVLAN));
    is_macsec = type_valid && (type_at_cursor == ET_MACSEC);

    // Two stops, two meanings.
    stopped_by_budget     = (cursor >= 16'(WINDOW_OCTETS))
                         || (tags_seen > 16'(MAX_TAGS));
    stopped_by_protection = is_macsec && !have_key;

    reached_payload_type = type_valid && !is_vlan && !is_macsec
                        && !stopped_by_budget;

    // What a device without the key can still classify on: the two
    // addresses and the outer EtherType. Chapter 25.1 Section 12's
    // fallback fields, and on a protected link they are all there is.
    visible_fields_mask = stopped_by_protection ? 16'h0007   // DA, SA, type
                                                : 16'h00FF;

    classification_available = reached_payload_type;
  end

  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n) begin
      cursor <= 16'd12; tags_seen <= '0;
      c_protected_frames <= '0; c_budget_stops <= '0;
    end else begin
      if (frame_start) begin
        cursor <= 16'd12; tags_seen <= '0;
      end else if (octet_valid && type_valid) begin
        if (is_vlan) begin
          cursor    <= cursor + 16'd4;
          tags_seen <= tags_seen + 16'd1;
        end else if (is_macsec) begin
          cursor <= cursor + 16'd8;
          c_protected_frames <= c_protected_frames + 32'd1;
        end
      end
      if (stopped_by_budget) c_budget_stops <= c_budget_stops + 32'd1;
    end
  end
endmodule

// ---------------------------------------------------------------------
// integrity_telemetry -- the counters that keep a protection claim
// honest, with the two failure kinds kept apart.
//
// Design rule: a check and a protection are different mechanisms, so
// every counter here names which one it is about. A design that merges
// them produces a number nobody can act on.
// ---------------------------------------------------------------------
module integrity_telemetry
  import crcsec_pkg::*;
(
  input  logic        clk,
  input  logic        rst_n,
  input  logic        clear,

  input  logic        frame_valid,
  input  logic        fcs_failed,
  input  logic        icv_failed,
  input  logic        protection_enabled,
  input  logic        key_present,
  input  logic        replay_detected,
  input  logic        pn_gap_detected,
  input  logic [15:0] pn_gap_size,
  input  logic        stopped_by_protection_i,
  input  logic        stopped_by_budget_i,

  output logic [47:0] c_frames,
  output logic [47:0] c_fcs_failures,
  output logic [47:0] c_icv_failures,
  output logic [47:0] c_replays,
  output logic [47:0] c_pn_gaps,
  output logic [47:0] c_pn_frames_lost,
  output logic [47:0] c_protection_stops,
  output logic [47:0] c_budget_stops_o,
  output logic [31:0] fcs_fail_ppm,
  output logic [31:0] icv_fail_ppm,
  output logic        counters_are_separated,
  output logic        claim_is_supported,
  output logic        integrity_alarm
);
  always_ff @(posedge clk or negedge rst_n) begin
    if (!rst_n || clear) begin
      c_frames <= '0; c_fcs_failures <= '0; c_icv_failures <= '0;
      c_replays <= '0; c_pn_gaps <= '0; c_pn_frames_lost <= '0;
      c_protection_stops <= '0; c_budget_stops_o <= '0;
    end else if (frame_valid) begin
      c_frames <= c_frames + 48'd1;

      // Section 8's triage, honoured: a frame the wire corrupted is
      // counted as a wire error and never reaches the ICV counter.
      if (fcs_failed)                 c_fcs_failures <= c_fcs_failures + 48'd1;
      else if (icv_failed)            c_icv_failures <= c_icv_failures + 48'd1;

      if (replay_detected)            c_replays <= c_replays + 48'd1;
      if (pn_gap_detected) begin
        c_pn_gaps        <= c_pn_gaps + 48'd1;
        // Section 13's production note: the packet number is in the
        // clear, so a gap is an attributable loss count.
        c_pn_frames_lost <= c_pn_frames_lost + 48'(pn_gap_size);
      end
      if (stopped_by_protection_i)
        c_protection_stops <= c_protection_stops + 48'd1;
      if (stopped_by_budget_i)
        c_budget_stops_o   <= c_budget_stops_o + 48'd1;
    end
  end

  always_comb begin
    fcs_fail_ppm = (c_frames == 0) ? 32'd0
                 : 32'((c_fcs_failures * 48'd1_000_000) / c_frames);
    icv_fail_ppm = (c_frames == 0) ? 32'd0
                 : 32'((c_icv_failures * 48'd1_000_000) / c_frames);

    // The structural claims this module makes about itself.
    counters_are_separated = 1'b1;

    // A protection claim is supported only if protection is on AND a
    // key is present. Either alone is a claim about a configuration.
    claim_is_supported = protection_enabled && key_present;

    // And the alarm fires on the counter that means something.
    integrity_alarm = claim_is_supported
                   && ((c_icv_failures != 48'd0) || (c_replays != 48'd0));
  end
endmodule

// ---------------------------------------------------------------------
// integrity_conformance -- the checks that hold an integrity claim to
// what the mechanism actually provides.
//
// Note what is absent: there is no check that frames are unaltered.
// Section 7 established that provenance is unobservable, so no monitor
// can write it, and Section 20's rejected property is the attempt.
// ---------------------------------------------------------------------
module integrity_conformance
  import crcsec_pkg::*;
(
  input  logic        clk,
  input  logic        rst_n,

  input  logic        claims_integrity,
  input  logic [15:0] key_bits_i,
  input  logic        fcs_checked_first,
  input  logic        icv_checked,
  input  logic        counters_merged,
  input  logic [15:0] stacked_public_checks_i,
  input  logic        offered_as_security,
  input  logic        protection_stop_distinct,
  input  logic [15:0] replay_window,
  input  logic [15:0] fabric_skew_frames,

  output logic        v_claim_without_key,
  output logic        v_icv_before_fcs,
  output logic        v_counters_merged,
  output logic        v_public_check_as_security,
  output logic        v_stop_bits_merged,
  output logic        v_replay_window_short,
  output logic  [5:0] violations,
  output logic        conformant
);
  always_comb begin
    // 1. Section 9: only a key changes the answer.
    v_claim_without_key = claims_integrity && (key_bits_i == 16'd0);

    // 2. Section 8's callout: the cheap check filters for the
    //    expensive one, so its order is load-bearing.
    v_icv_before_fcs = icv_checked && !fcs_checked_first;

    // 3. Prohibition 4 -- an unactionable alarm.
    v_counters_merged = counters_merged;

    // 4. Prohibitions 1 to 3 -- a public check offered as protection,
    //    however many of them there are.
    v_public_check_as_security = offered_as_security && (key_bits_i == 16'd0)
                              && (stacked_public_checks_i >= 16'd1);

    // 5. Section 13 -- two stops, two meanings.
    v_stop_bits_merged = !protection_stop_distinct;

    // 6. A window below the fabric's reordering depth counts benign
    //    reordering as an attack.
    v_replay_window_short = (replay_window < fabric_skew_frames);

    violations = { v_replay_window_short, v_stop_bits_merged,
                   v_public_check_as_security, v_counters_merged,
                   v_icv_before_fcs, v_claim_without_key };
    conformant = (violations == 6'b000000);
  end
endmodule

// A1. The identity, on every frame and every difference.
p_ln_linearity: assert property (@(posedge clk) disable iff (!rst_n)
  eval |-> (r_combined == (r_frame ^ r_diff)));

// A2. And the model reports it.
p_ln_holds: assert property (@(posedge clk) disable iff (!rst_n)
  eval |-> linearity_holds);

// A3. A zero difference changes nothing.
p_ln_zero_diff: assert property (@(posedge clk) disable iff (!rst_n)
  (diff_bits == '0) |-> (r_combined == r_frame));

// A4. The difference's check value does not depend on the frame.
p_ln_diff_independent: assert property (@(posedge clk) disable iff (!rst_n)
  (diff_bits == $past(diff_bits)) |-> (r_diff == $past(r_diff)));

// A5. Weight is the count of set bits and nothing else.
p_ln_weight: assert property (@(posedge clk) disable iff (!rst_n)
  (diff_bits == '0) |-> (diff_weight == 16'd0));

// A6. Span is zero only for a zero difference.
p_ln_span_zero: assert property (@(posedge clk) disable iff (!rst_n)
  (diff_span_bits == 16'd0) |-> !diff_is_nonzero);

// A7. Span is at least the weight.
p_ln_span_ge_weight: assert property (@(posedge clk) disable iff (!rst_n)
  diff_is_nonzero |-> (diff_span_bits >= diff_weight));

// A8. A difference inside 32 bits is inside the burst class.
p_ln_burst_class: assert property (@(posedge clk) disable iff (!rst_n)
  (diff_is_nonzero && (diff_span_bits <= 16'd32)) |-> within_burst_bound);

// A9. Every evaluation is counted.
p_ln_counted: assert property (@(posedge clk) disable iff (!rst_n)
  eval |=> (c_evaluations == $past(c_evaluations) + 32'd1));

// B1. The delta is the difference's pure remainder.
p_cp_delta: assert property (@(posedge clk) disable iff (!rst_n)
  eval |-> (delta == r0(diff_bits, int'(nbits))));

// B2. And the compensated value is one XOR away.
p_cp_xor: assert property (@(posedge clk) disable iff (!rst_n)
  (fcs_compensated == (fcs_original ^ delta)));

// B3. A chosen nonzero difference leaves the check satisfied.
p_cp_passes: assert property (@(posedge clk) disable iff (!rst_n)
  ((threat == 2'(THREAT_CHOSEN)) && (diff_bits != '0)) |-> check_still_passes);

// B4. And a channel difference does not.
p_cp_noise_fails: assert property (@(posedge clk) disable iff (!rst_n)
  (threat != 2'(THREAT_CHOSEN)) |-> !check_still_passes);

// B5. The mechanism needs no secret and has none.
p_cp_no_secret: assert property (@(posedge clk) disable iff (!rst_n)
  (!requires_a_secret && (bits_of_secret_available == 16'd0)));

// B6. Every input is public.
p_cp_public: assert property (@(posedge clk) disable iff (!rst_n)
  inputs_are_all_public);

// B7. The reported probability is 1 for a chosen difference.
p_cp_certainty: assert property (@(posedge clk) disable iff (!rst_n)
  (threat == 2'(THREAT_CHOSEN)) |-> (detection_prob_recip == 32'd1));

// B8. And 2^32-ish otherwise.
p_cp_residual: assert property (@(posedge clk) disable iff (!rst_n)
  (threat != 2'(THREAT_CHOSEN)) |-> (detection_prob_recip == 32'hFFFF_FFFF));

// C1. Chapter 6.1's burst clause.
p_gu_burst: assert property (@(posedge clk) disable iff (!rst_n)
  ((diff_span_bits != 16'd0) && (diff_span_bits <= 16'd32)) |-> in_burst_class);

// C2. The weight-3 clause holds at any length.
p_gu_weight3: assert property (@(posedge clk) disable iff (!rst_n)
  ((diff_weight != 16'd0) && (diff_weight <= 16'd3)) |-> in_weight3_class);

// C3. The weight-4 clause is length-bounded.
p_gu_weight4: assert property (@(posedge clk) disable iff (!rst_n)
  ((diff_weight == 16'd4) && (frame_octets > 16'd375)) |-> !in_weight4_class);

// C4. Guaranteed and residual partition the nonzero differences.
p_gu_partition: assert property (@(posedge clk) disable iff (!rst_n)
  (diff_span_bits != 16'd0) |-> (guarantee_applies ^ residual_class));

// C5. The residual applies only to an unchosen difference.
p_gu_residual_qualified: assert property (@(posedge clk) disable iff (!rst_n)
  (threat == 2'(THREAT_CHOSEN)) |-> !residual_is_meaningful);

// C6. Provenance is never observable.
p_gu_provenance: assert property (@(posedge clk) disable iff (!rst_n)
  (provenance_observable == 1'b0));

// C7. The residual reciprocal is the width's bound.
p_gu_recip: assert property (@(posedge clk) disable iff (!rst_n)
  (residual_recip == 32'hFFFF_FFFF));

// C8. Guaranteed differences are counted.
p_gu_counted: assert property (@(posedge clk) disable iff (!rst_n)
  (eval && guarantee_applies) |=> (c_guaranteed == $past(c_guaranteed) + 32'd1));

// C9. A zero difference is in no class.
p_gu_zero: assert property (@(posedge clk) disable iff (!rst_n)
  (diff_span_bits == 16'd0) |-> (!guarantee_applies && !residual_class));

// D1. Only a key makes a guarantee survive a chosen difference.
p_ad_key_required: assert property (@(posedge clk) disable iff (!rst_n)
  ((threat == 2'(THREAT_CHOSEN)) && (key_bits == 16'd0)) |-> !guarantee_survives);

// D2. And with a key it does.
p_ad_key_suffices: assert property (@(posedge clk) disable iff (!rst_n)
  (key_bits != 16'd0) |-> guarantee_survives);

// D3. Effective security under a chosen difference is the key length.
p_ad_effective: assert property (@(posedge clk) disable iff (!rst_n)
  (threat == 2'(THREAT_CHOSEN)) |-> (effective_security_bits == key_bits));

// D4. Widening the check does not help against a chosen difference.
p_ad_widening: assert property (@(posedge clk) disable iff (!rst_n)
  (threat == 2'(THREAT_CHOSEN)) |-> !widening_helps);

// D5. Stacking public checks never helps.
p_ad_stacking: assert property (@(posedge clk) disable iff (!rst_n)
  (stacking_helps == 1'b0));

// D6. And the work to defeat n of them is n.
p_ad_linear_work: assert property (@(posedge clk) disable iff (!rst_n)
  check_inputs_public |-> (compensation_steps == stacked_public_checks));

// D7. Only a key is named as the remedy.
p_ad_only_key: assert property (@(posedge clk) disable iff (!rst_n)
  (threat == 2'(THREAT_CHOSEN)) |-> only_a_key_helps);

// D8. Chosen and noise evaluations are counted apart.
p_ad_counted_apart: assert property (@(posedge clk) disable iff (!rst_n)
  (eval && (threat == 2'(THREAT_CHOSEN))) |=>
    ((c_chosen == $past(c_chosen) + 32'd1) && (c_noise == $past(c_noise))));

// E1. The SecTAG size follows the SCI flag.
p_ms_sectag: assert property (@(posedge clk) disable iff (!rst_n)
  include_sci |-> (sectag_octets == 16'(SECTAG_WITH_SCI)));

// E2. Overhead is the SecTAG plus the ICV.
p_ms_overhead: assert property (@(posedge clk) disable iff (!rst_n)
  (overhead_octets == sectag_octets + 16'(ICV_OCTETS)));

// E3. Protection always costs wire.
p_ms_costs_wire: assert property (@(posedge clk) disable iff (!rst_n)
  (wire_protected > wire_unprotected));

// E4. And the cost falls as the frame grows -- Chapter 8.3's hyperbola.
p_ms_hyperbola: assert property (@(posedge clk) disable iff (!rst_n)
  (payload_octets > $past(payload_octets)) |->
    (wire_cost_ppm <= $past(wire_cost_ppm)));

// E5. Efficiency falls under protection.
p_ms_eff_falls: assert property (@(posedge clk) disable iff (!rst_n)
  (eff_protected_ppm < eff_unprotected_ppm));

// E6. The pipeline count rounds up.
p_ms_pipelines: assert property (@(posedge clk) disable iff (!rst_n)
  (rate_gbps != 0) |-> (pipelines_needed >= 16'd1));

// E7. Two stops, and they are distinguishable.
p_pp_two_stops: assert property (@(posedge clk) disable iff (!rst_n)
  stopped_by_protection |-> !classification_available);

// E8. Without a key only three fields are visible.
p_pp_visible: assert property (@(posedge clk) disable iff (!rst_n)
  stopped_by_protection |-> (visible_fields_mask == 16'h0007));

// E9. A MACsec frame with a key parses on.
p_pp_with_key: assert property (@(posedge clk) disable iff (!rst_n)
  (is_macsec && have_key) |-> !stopped_by_protection);

// F1. The two failure kinds are mutually exclusive by construction.
p_tl_exclusive: assert property (@(posedge clk) disable iff (!rst_n)
  (frame_valid && fcs_failed) |=> (c_icv_failures == $past(c_icv_failures)));

// F2. The counters are separated and the module says so.
p_tl_separated: assert property (@(posedge clk) disable iff (!rst_n)
  counters_are_separated);

// F3. A protection claim needs enablement AND a key.
p_tl_claim: assert property (@(posedge clk) disable iff (!rst_n)
  claim_is_supported |-> (protection_enabled && key_present));

// F4. The alarm fires only on a supported claim.
p_tl_alarm: assert property (@(posedge clk) disable iff (!rst_n)
  integrity_alarm |-> claim_is_supported);

// F5. A packet-number gap accumulates the lost count.
p_tl_pn_gap: assert property (@(posedge clk) disable iff (!rst_n)
  (frame_valid && pn_gap_detected) |=>
    (c_pn_frames_lost == $past(c_pn_frames_lost) + 48'($past(pn_gap_size))));

// F6. An integrity claim with no key is a violation.
p_cf_no_key: assert property (@(posedge clk) disable iff (!rst_n)
  (claims_integrity && (key_bits_i == 16'd0)) |-> v_claim_without_key);

// F7. The FCS must be checked before the ICV.
p_cf_order: assert property (@(posedge clk) disable iff (!rst_n)
  icv_checked |-> fcs_checked_first);

// F8. Conformance is the disjunction of its six checks.
p_cf_vector: assert property (@(posedge clk) disable iff (!rst_n)
  conformant |-> (violations == 6'b000000));

c_ln_burst32:    cover property (@(posedge clk) diff_span_bits == 16'd32);
c_ln_burst33:    cover property (@(posedge clk) diff_span_bits == 16'd33);
c_ln_weight4:    cover property (@(posedge clk) diff_weight == 16'd4);
c_gu_residual:   cover property (@(posedge clk) residual_class);
c_gu_not_mean:   cover property (@(posedge clk) residual_class && !residual_is_meaningful);
c_cp_chosen:     cover property (@(posedge clk) check_still_passes);
c_ad_no_key:     cover property (@(posedge clk) effective_security_bits == 16'd0);
c_ad_stacked:    cover property (@(posedge clk) stacked_public_checks >= 16'd3);
c_ms_min_frame:  cover property (@(posedge clk) payload_octets <= 16'd46);
c_ms_jumbo:      cover property (@(posedge clk) payload_octets >= 16'd9000);
c_pp_protected:  cover property (@(posedge clk) stopped_by_protection);
c_pp_tag_macsec: cover property (@(posedge clk) is_vlan && is_macsec);
c_tl_icv_fail:   cover property (@(posedge clk) icv_failed && !fcs_failed);
c_cf_merged:     cover property (@(posedge clk) v_counters_merged);