Architecture and verification
One mathematical reference.
Any backend.
For backend implementors and technical evaluators: Poulpy defines scheme operations through a shared mathematical vocabulary. Backends can change how an operation runs while preserving exactly what it computes.
Explore the architecture ↓Layouts, key switching, and data lifecycle →01 / A shared vocabulary
Schemes built from precise operations.
Backend-agnostic crates define FHE operations and their mathematical building blocks. Your application chooses which APIs to use and a backend to execute them. Backends provide hardware-specific arithmetic and storage behind the same contracts.
Read the layer ownership rule →Backend-agnostic code
Scheme
poulpy-ckks
Approximate numerical computation.
Scheme
poulpy-bin-fhe
Boolean and integer computation.
Cryptographic primitives
poulpy-core
GLWE, encryption, key switching, and external products.
Mathematical primitives
poulpy-hal
Polynomial operations, layouts, and contracts.
Application
Choose your API level and backend.
Module<B>Backends
Hardware-specific execution and storage.
- poulpy-cpu-refPortable reference
- poulpy-cpu-avxAVX2 / FMA
- poulpy-cpu-avx512AVX-512 / IFMA
- poulpy-cpu-armARM NEON
- GPU backendIn active development
02 / A canonical definition
Follow an operation all the way down.
Every operation above the HAL has a reference composition: a sequence of calls to APIs in its own layer or the layers below. Unless the backend overrides the operation, dispatch follows that composition. Expanding these calls recursively reaches a sequence of HAL operations.
For a fixed operation, parameters, and inputs, that fully expanded reference gives a canonical mathematical expression. It provides a common definition for each scheme operation, suitable for mathematical standardization and comparison across implementations.
Canonical means the expression chosen by the reference composition. An optimized backend may use a different algorithm or an equivalent expression; the reference fixes the result it must reproduce.
Scheme operation → reference composition → HAL operations
Worked example / CKKS multiplication
CKKS tensoring, expanded to the HAL.
Take ckks_mul_into: multiply two ciphertexts, form their tensor product, then relinearize it. The graph follows the actual default dispatch through poulpy-ckks and poulpy-core to the mathematical operations in poulpy-hal. OEP means open extension point: a backend implementation can replace the operation at that boundary.
All default compositions
The reference stays the definition.
With no override, each API dispatches to its default implementation. Recursively expanding the arithmetic calls reaches HAL contracts. Together with the specified parameters, rounding, and metadata rules, this is the reference mathematical representation of the operation.
CKKS multiplication OEP
Replace the whole multiplication.
Implement CKKSMulImpl::ckks_mul_into_impl directly, bypassing ckks_mul_into_default. A backend can combine tensoring and relinearization, keep intermediates on a device, and choose its own execution plan. It must preserve the CKKS result bytes, metadata, and operation contract.
Core tensor-product OEP
Specialize the tensor product.
Implement GLWETensoringImpl::glwe_tensor_apply directly, bypassing glwe_tensor_apply_default. Preparation, convolution, inverse transforms, normalization, and tensor assembly can be implemented together. The enclosing CKKS composition and the reference relinearization can still be reused.
Core relinearization OEP
Specialize the key-switching stage.
Implement GLWETensoringImpl::glwe_tensor_relinearize directly, bypassing glwe_tensor_relinearize_default. Fuse its transforms, gadget product, accumulation, and normalization while preserving the reference tensoring stage. The internal gadget-product helper is not a separate OEP on this dsize = 1 path.
HAL pairwise-convolution operation
Work at the smallest contract.
Implement cnv_pairwise_apply_dft for the target hardware while retaining every higher-level reference composition. SIMD instructions, parallel scheduling, and internal fusion are backend choices within that HAL operation’s contract.
Every fusion boundary preserves the same reference result, down to the output bytes.
03 / Freedom within a contract
Implement the HAL. Unlock the stack.
A new backend implements the HAL contracts and connects the higher layers to their reference compositions. That opens the stack without rewriting scheme logic.
Reference execution
- Reference composition
Expand calls through the scheme and core APIs.
- HAL operation sequence
Reach the shared mathematical primitives.
- Portable reference backend
Execute the baseline arithmetic in poulpy-cpu-ref.
Custom execution
- Backend override at an OEP
The backend implements the OEP directly, bypassing its default composition.
- Fused or specialized kernel
Combine work and choose intermediate layouts suited to the hardware.
- Defined output boundary
Expose the result in the representation required by the contract.
Reference output bytesb₀ b₁ … bₙ
Custom output bytesb₀ b₁ … bₙ
04 / Standardization and formal verification
A mathematical specification for every scheme.
Poulpy’s reference compositions provide a way to standardize primitives and schemes in one mathematical vocabulary: HAL operations. For a fixed configuration, expanding an operation through those compositions gives it a canonical expression, including normalization and rounding. That definition can be shared, analyzed, and used as the basis for scheme standardization and formal verification independently of any backend.
Define the HAL vocabulary
Give each mathematical operation precise inputs, outputs, and preconditions. Make coefficient arithmetic, transforms, normalization, and rounding explicit.
Specify cryptographic primitives
Express core operations, such as GLWE key switching and tensoring, as reference compositions that resolve to HAL calls. Each primitive gets a well-defined mathematical expression.
Standardize scheme operations
Build CKKS and Binary FHE operations from those primitives. Their reference compositions define a common scheme specification that every backend can implement and researchers can reason about.
Verify implementations against that definition.
Parity tests compare computation outputs that the reference backend can interpret, typically from operations taking and returning ScalarZnx, VecZnx, or MatZnx. Transform-domain computations are checked through DFT → OP → IDFT → Normalize, returning to a reference-readable coefficient layout before comparing bytes. These tests exercise sampled inputs; formal proofs would establish scheme correctness and backend equivalence for all inputs covered by their assumptions. Read the core parity suite ↗
Custom layouts require backend-owned tests. A backend that defines custom layouts is responsible for testing their invariants, conversions, and kernels. Internal storage may differ across backends; parity is checked after conversion to a common, reference-readable representation. The comparison depends on the actual layout, not just the Rust type name.
Explore the design and code.
Layer ownership
Where semantics and extension points belong.
Choose a backend
Portable and accelerated implementations.
HAL/OEP design issue #234
The architecture goals and remaining cleanup.
Core parity suite
Read the byte-for-byte comparison contract in the code.
Codebase overview
How API, OEP, default, and delegate modules connect.
Architecture post
The accompanying discussion on LinkedIn.