Skip to section
Foundationsfor rotation-free search
Section 51 of 5298% of course
Contents
Chapter 8 Section 8.5 75 min

Part VI · The implementation

Verification across representations

Use reference models, invariants, and end-to-end checks together.

Don't bet everything on one big end-to-end test

A "hello world" demo that passes is dangerous. It can hide edge cases like weird block dimensions, random pipeline stalls, negative residue wrapping, partial blocks, or precision loss on close scores. Worse, if an end-to-end test fails, you have no idea which of the hundred transformations broke it. You need a ladder of smaller, trusted tests.

1index identity

symbolic proofs and exhaustive checks on small arrays

2Python polynomial model

checking basic dot products against actual target coefficients

3Rust encoding/encryption

round-trip encryption tests and cross-language vector matching

4RTL module tests

throwing random stalls, phases, limbs, and lane configurations at the hardware

5system test

checking decrypted scores and ensuring the top-k rankings match reality

Test the rules, not just the examples

  • Ensure every supported D divides cleanly into N and generates N/D valid targets.
  • Verify every single (j, i) coordinate pair lands exactly at Dj + D − 1.
  • Prove that no stray cross-term can ever pollute that specific target index.
  • Prove that no wrapped t + N source can accidentally reach the target.
  • Verify the hardware emits the exact same mathematical result no matter how many backpressure stalls you throw at it.
  • Confirm Python, Rust, and Verilog all serialize the bytes in the exact same order.

Worked example

Differential testing

Generate a bunch of random, small integer vectors. Then, run them through three different engines: a normal Python dot product, a pure polynomial product, and the fully encrypted FHE hardware path. If they disagree, you can instantly see which layer broke the math.

for D in supported_dimensions:
    for query, corpus in generated_cases(D):
        packed = polynomial_scores(query, corpus, D)
        direct = [sum(a*b for a, b in zip(query, row))
                  for row in corpus]
        assert extract_targets(packed, D, len(corpus)) == direct

        decoded = encrypted_scores(query, corpus, D)
        assert max_abs_error(decoded, direct) <= ERROR_LIMIT

Let the symptom tell you where to look

symptomfirst boundary to inspectlikely class
all scores are way too big (scaled by ~Δ)decode divisor metadatascale-depth mismatch (forgot to divide by Δ²)
scores are right, but assigned to wrong corpus IDsproduct/local/global mappingserialization or padding index bug
test passes normally, but fails if RTL stallsvalid, phase, row, stash enablestemporal alignment (wires didn't freeze together)
one residue limb has garbage datamodulus selection and limb orderRNS mismatch
scores are slightly off, top-k ranking is jumping aroundscore-margin distributionapplication precision (Δ is too small)
Why should we check 'accepted transaction numbers' instead of just counting clock cycles in tests?

Because backpressure is allowed to insert random idle cycles. The rule isn't 'input cycle 5 produces output cycle 15'. The rule is 'the 5th accepted input produces the 5th valid output'. Your tests have to respect the valid/ready handshake.

Check your understanding

Why do we inject random m_ready stalls into the hardware tests?

Section summary

  • Layered testing helps you isolate exactly where a bug lives.
  • Invariant testing proves your math works for entire classes of configurations.
  • Randomly pausing the hardware proves your control logic is solid.
  • Checking the top-k rankings proves the application actually works for the user.

Repository layer · second pass

Why do we need tests at several representations?

No single end-to-end test localizes defects. Use a plain dot-product oracle, exact integer packing identity, negacyclic polynomial reference, NTT equivalence, encrypted approximate trials, RTL unit tests, randomized handshake scoreboards, and cross-language fixtures. Each catches a different class of mistake.

Verification evidence should be reproducible: parameters, seeds, fixture versions, tolerances, simulator commands, and benchmark hardware. Classify failures by the first layer that diverges.

Reasoning chain

  1. 1

    Build the simplest trustworthy oracle.

  2. 2

    Test layout exactly before encryption.

  3. 3

    Test optimized arithmetic against the oracle.

  4. 4

    Add approximation tolerances only at the CKKS layer.

  5. 5

    Stress transport independently.

  6. 6

    Run full-path tests last.

Worked trace

A diagnostic matrix

  1. Dot oracle passes.
  2. Packed integer identity passes.
  3. NTT product passes.
  4. RTL fails only under ready stalls.

Result. The evidence points to protocol state, not mathematics or modular arithmetic.

Executable lens · Python

Make the hidden state visible

tests = {
 "semantic":"dot oracle",
 "layout":"integer identity",
 "ring":"negacyclic reference",
 "transform":"NTT equivalence",
 "transport":"random stalls",
}

Retype this example, predict each intermediate value, and then change one input that touches a boundary.

Misconception clinic

Tempting mistakes

  • Using the production implementation as its own oracle.
  • Applying floating tolerance to exact index or integer tests.

Retrieval and transfer

Close the book first

  1. Build a layer-by-failure matrix.
  2. Specify seeds and fixture serialization.
  3. Design mutation tests for each invariant.