Tracing the Ghost in the Machine: Debugging the Pre-Compiled Constraint Evaluator's Correctness Bug

In the midst of implementing Phase 5 of the cuzk proving engine optimization — the Pre-Compiled Constraint Evaluator (PCE) — the assistant encountered a critical failure. The initial benchmark run had revealed two alarming problems: a correctness bug causing approximately 53% of constraint evaluations to produce wrong results, and a performance regression where the supposedly faster PCE path was actually slower than the old synthesis path. Message [msg 1427] captures a pivotal moment in the debugging process: the assistant reading the ProvingAssignment::enforce() method from the bellperson source to understand how the existing (correct) code path computes the a, b, and c vectors that form the core of a Groth16 proof.

The Message in Context

To understand why this message was written, we must step back to the broader narrative. The PCE is a sophisticated optimization that exploits a structural property of Filecoin's PoRep (Proof of Replication) circuit: the R1CS constraint matrices (A, B, C) are identical for every proof of a given sector size. Only the witness vector changes. The old pipeline re-synthesized the full circuit for every proof, constructing and evaluating ~390 million LinearCombination objects per partition — an enormous waste of CPU cycles and memory bandwidth. The PCE instead separates witness generation (which computes the actual SHA-256 and Poseidon intermediate values) from constraint evaluation (which computes a = A·w, b = B·w, c = C·w via sparse matrix-vector multiplication). The constraint matrices are extracted once and reused forever.

The assistant had just run the first end-to-end benchmark of this new pipeline. The results were sobering. The old path completed synthesis in 50.4 seconds. The new PCE path took 61.1 seconds — 21% slower. Worse, when the assistant added a --validate flag to compare the a, b, and c vectors produced by both paths, the output showed massive mismatches: 53% of a entries, 50% of b entries, and 46% of c entries differed between the two paths, starting at index 1 (the second constraint). The PCE was not just slow — it was wrong.

Message [msg 1427] is the assistant's next logical step in diagnosing this failure. Having already read the PCE's own source files (eval.rs, recording_cs.rs, csr.rs) in [msg 1425] and the bellperson prover module in [msg 1426], the assistant now drills deeper into the specific method that computes a/b/c in the old path: ProvingAssignment::enforce().

The Reasoning and Motivation

The assistant's thinking is methodical and reveals a clear debugging strategy. The core question is: why do 53% of constraint evaluations produce different results between the old path and the PCE path? Both paths take the same circuit and the same witness values. The old path builds LinearCombination objects during enforce() and evaluates them against the witness. The PCE path records the constraint structure once into CSR matrices, then performs sparse matrix-vector multiplication. If the CSR matrices correctly capture the constraint structure, the results should match bit-for-bit.

The fact that mismatches start at index 1 (not index 0) is a critical clue that the assistant explicitly notes in [msg 1424]: "The fact that mismatches start at index 1 (not 0) suggests an off-by-one or variable mapping issue." This observation shapes the entire debugging approach. The assistant suspects a variable indexing problem — that the PCE is mapping variable indices to matrix columns differently than the old path does.

To verify this hypothesis, the assistant needs to understand exactly how the old path indexes variables during enforce(). The ProvingAssignment::enforce() method is the canonical reference implementation. It receives three closures a, b, and c that produce LinearCombination objects. Each LinearCombination contains terms that reference variables by their Index (either Index::Input(i) or Index::Aux(i)). The method evaluates each term by looking up the corresponding value in input_assignment[i] or aux_assignment[i], multiplies by the coefficient, and accumulates into the output vectors self.a, self.b, self.c.

The PCE path, by contrast, records these same variable references during a one-time extraction pass, but encodes them into a unified column index: col = index for input variables and col = num_inputs + index for aux variables. At evaluation time, the witness vector is constructed as [input_assignment | aux_assignment] and the MatVec does witness[col]. If the column indices are consistent, this should produce identical results.

The Hidden Bug: Interleaved Allocation and Enforcement

The message itself is brief — a single file read operation — but it represents the critical transition from hypothesis to investigation. The assistant is about to discover the root cause of the correctness bug, which will be identified in [msg 1432] and confirmed in [msg 1433].

The bug is subtle and elegant in its treachery. In RecordingCS::enforce(), the assistant had naively computed the unified column index as self.num_inputs + *index for aux variables. But self.num_inputs is not a constant — it grows as alloc_input() calls are processed. And crucially, the PoRep circuit interleaves alloc_input() calls with enforce() calls during synthesis. Early enforce() calls see a smaller num_inputs than later ones. The result is that aux variable indices recorded early in synthesis point to different absolute positions in the unified witness vector than the same aux variables would if recorded later. The column indices are inconsistent across the matrix.

At evaluation time, the witness vector is constructed with the final num_inputs as the boundary between input and aux regions. Every aux column index recorded before the last alloc_input() is shifted — it points into the input region instead of the aux region, producing garbage results for any constraint that references aux variables.

This explains the 53% mismatch rate: roughly half of all constraints reference aux variables, and those constraints that were recorded before the final alloc_input() use wrong column indices. The fact that constraint 0 (the first constraint) is correct makes sense — it's the "one" constraint that only references the input variable "one", which is allocated first and never interleaved.

Assumptions and Their Consequences

The assistant made a critical assumption when designing RecordingCS: that num_inputs would be fully determined before any enforce() calls. This assumption is natural — in many circuit frameworks, input allocation happens in a fixed phase before constraint enforcement. But the bellperson/bellpepper framework does not enforce this ordering. The Circuit::synthesize() method receives a ConstraintSystem reference and can call alloc_input(), alloc(), and enforce() in any interleaving. The PoRep circuit, being a complex composition of SHA-256, Poseidon, and labeling gadgets, freely interleaves these calls.

The assistant's assumption was not documented or tested — it was an implicit design choice made during the initial PCE implementation. The bug only manifested when running the actual PoRep circuit, not during unit tests with toy circuits. This highlights a broader lesson about optimization work on complex systems: assumptions about the structure of input data must be validated against real-world usage patterns, not just synthetic test cases.

The assistant also assumed that the CSR MatVec approach would be straightforwardly correct if the column indices were consistent. This assumption proved correct — once the indexing bug was fixed (using a tagged encoding scheme with bit 31 as an input/aux flag and deferred remapping in into_precompiled()), all 10 circuits × 130M constraints validated bit-for-bit correct.

Input and Output Knowledge

To fully understand this message, the reader needs several pieces of input knowledge: the architecture of the Groth16 proving system (particularly how a, b, c vectors are computed from R1CS constraints and witness assignments); the bellperson/bellpepper circuit framework (the ConstraintSystem trait, alloc_input(), alloc(), enforce() methods, and the Index enum distinguishing Input from Aux variables); the CSR sparse matrix format and how it maps to R1CS matrix-vector multiplication; and the structure of the PoRep circuit (SHA-256 and Poseidon gadgets, their interleaved allocation patterns).

The output knowledge created by this message is more about process than content. The file read itself reveals only a few lines of Rust code — the constructor and with_capacity method of ProvingAssignment. But the act of reading this file, in context, produces a crucial understanding: the assistant is now positioned to trace the exact mapping from LinearCombination terms to output vector entries, and to compare this against the PCE's column indexing scheme. This comparison will reveal the bug within a few more messages.

The Thinking Process

The assistant's reasoning, visible across the sequence of messages from [msg 1424] to [msg 1434], follows a classic scientific debugging methodology:

Observe: Run the benchmark, collect data. Two problems found (correctness + performance).
Prioritize: The user's comment "Synth is irrelevant no?" in [msg 1430] correctly focuses attention on correctness over performance.
Formulate hypothesis: Mismatches starting at index 1 suggest an off-by-one or variable mapping issue.
Gather evidence: Read the PCE source files to understand the new path's data flow.
Compare with reference: Read the old path's ProvingAssignment::enforce() to understand the correct behavior.
Identify discrepancy: The num_inputs offset is not constant during recording.
Fix and verify: Implement tagged encoding with deferred remapping, re-run validation. Message [msg 1427] is step 5 in this sequence. It is the moment when the assistant transitions from understanding the new path (which it wrote) to understanding the old path (which it must match). The message is brief because the assistant is in information-gathering mode — reading code, not writing it. But it is the linchpin of the entire debugging effort. Without this comparison, the assistant would be guessing at the bug rather than systematically tracing the data flow. The message also reveals something about the assistant's working style: it reads source files directly rather than relying on documentation or memory. The file paths are absolute, pointing to a local curio workspace. The assistant is deeply embedded in the codebase, navigating it with the confidence of someone who has read these files many times before. The [read] tool invocation is the assistant's primary mechanism for gathering information — it reads the exact lines it needs, focusing on the enforce() method's implementation details.

Conclusion

Message [msg 1427] is a deceptively simple moment in a complex debugging session. On its surface, it is just a file read — a few lines of Rust code displayed in a terminal. But in the narrative of the PCE implementation, it represents the critical pivot from building to debugging, from assumption to verification. The assistant's methodical approach — observe, hypothesize, gather evidence, compare, identify — is a model of disciplined software engineering. The bug it helps uncover — an inconsistency caused by assuming a fixed ordering of operations that the framework does not guarantee — is a classic systems pitfall. And the fix — deferred remapping with tagged encoding — is an elegant solution that preserves the PCE's performance characteristics while ensuring correctness.

The message stands as a testament to the importance of reading the reference implementation when debugging a rewrite. No amount of staring at the new code would have revealed the num_inputs inconsistency; only by tracing the old path's exact behavior could the assistant identify where the new path diverged. It is a lesson in humility for anyone undertaking optimization work: the old code may be slow, but it is (presumably) correct, and understanding its correctness is the first step to building something faster that is also correct.