A proof is really just an executable contract
Every single step of our proof leaned on a specific assumption. If our software accidentally accepts data outside those assumptions, our beautiful theorem no longer actually describes our program! The safest way to write this code is to make every assumption explicit, validate it as early as possible near the boundary where it might fail, and carry enough metadata to double-check it later.
N == 4096N % D == 0q.Length <= Dv.Length == Dtarget < NValidate as close to the boundary as possible
The client needs to check the query length before it ever starts encoding. Our ingest pipeline must check corpus dimensions before packing them. The hardware configuration has to verify D before it accepts a job. Our extraction code has to derive its score taps using that exact same D. By repeating these cheap validations at every trust boundary, we make data corruption way easier to track down.
This isn't just needless code duplication. Every boundary is protecting you against a totally different kind of failure: a caller screwing up, storage getting corrupted, a mismatched deployment config, or the caller interpreting the response wrong. A validation check that successfully ran months ago during corpus ingestion doesn't prove that today's hardware job is actually using the same D.
Worked example
A dangerous near miss
Imagine your ingest pipeline packs everything using D=256, but your extraction code assumes D=128. Both of those numbers cleanly divide 4096, so a generic N % D == 0 check will pass! This is why the exact agreement invariant has to travel alongside the artifact, or be securely authenticated as metadata.
Worked example
Length ≤ D isn't the whole story for queries
If you have a three-element query for D=4, you might pad it with a zero at coefficient 3, which keeps it safely inside our support bound. But what if a buggy serializer places those exact same three values at coefficients 0, 1, and 4? The length is still three, but the support bound is completely violated. You must validate the physical support after layout, not just the length of the source array.
A layout bug looks very different from an approximation error
A layout mismatch almost always radically moves or mixes up massive contributions, which creates a huge structural error that sticks around even if you use exact integers. On the other hand, CKKS approximation introduces tiny, normal numerical deviations around a structurally correct result. Always test your integer layout reference first! Then, measure encoding and encryption error completely separately. If you don't, you might spend weeks trying to fix "normal FHE noise" that is actually a severe indexing bug.
Check your understanding
Which invariant comes directly from our block-isolation proof?
Validation check
Why is it not enough to just check N % D == 0 at both ingest and extraction?
Section summary
- Turn your mathematical proof assumptions into executable code guards.
- Agreement on D is a much stronger requirement than independent validity of D.
- Validate aggressively at encoding, ingest, hardware configuration, and extraction.
Repository layer · second pass
How do proofs become executable guardrails?
Every proof premise should have an owner and a check. D divides N; each vector has length D; query coefficients outside 0…D−1 are zero; block j uses the exact reversed mapping; extraction uses Dj+D−1. If code can violate a premise silently, the proof no longer applies to the program.
Check invariants at representation boundaries, not only deep inside arithmetic. Fail before encrypting an invalid layout, because ciphertext hides the evidence and makes diagnosis expensive.
Reasoning chain
- 1
Underline every assumption in the proof.
- 2
Map it to the producing component.
- 3
Choose compile-time, construction-time, or runtime enforcement.
- 4
Add an adversarial negative test.
- 5
Reuse one parameter object for packing and extraction.
Worked trace
Prevent producer-consumer drift
- Encoder uses D=512.
- Extractor accidentally uses D=768.
- Both indices are individually in range.
- Shared immutable parameters make the mismatch unrepresentable.
Result. Type and construction design can enforce what comments merely request.
Executable lens · Python
Make the hidden state visible
def validate(n, d, vectors):
if d <= 0 or n % d: raise ValueError("D must divide N")
if len(vectors) > n // d: raise ValueError("batch too large")
if any(len(v) != d for v in vectors): raise ValueError("wrong dimension")Retype this example, predict each intermediate value, and then change one input that touches a boundary.
Misconception clinic
Tempting mistakes
- Testing outputs but never invalid inputs.
- Duplicating target formulas across languages without cross-checks.
Retrieval and transfer
Close the book first
- Create a proof-to-assertion table.
- Classify each invariant by owner.
- Design a serialized parameter manifest shared by Python, Rust, and RTL tests.