From d9cff29451106764aa3486ad676445b3bf615c38 Mon Sep 17 00:00:00 2001 From: dbanks12 Date: Wed, 24 Dec 2025 19:44:11 +0000 Subject: [PATCH] chore: claude-generated sha audit --- barretenberg/cpp/pil/vm2/sha256_mem.pil | 33 +++++++++++++++++++++++-- 1 file changed, 31 insertions(+), 2 deletions(-) diff --git a/barretenberg/cpp/pil/vm2/sha256_mem.pil b/barretenberg/cpp/pil/vm2/sha256_mem.pil index 255715e80a03..ec77092cd227 100644 --- a/barretenberg/cpp/pil/vm2/sha256_mem.pil +++ b/barretenberg/cpp/pil/vm2/sha256_mem.pil @@ -113,9 +113,38 @@ namespace sha256; pol commit latch; latch * (1 - latch) = 0; - #[LATCH_HAS_SEL_ON] // sel = 1 when latch = 1, sel = 0 at first row because of shift relations + #[LATCH_HAS_SEL_ON] latch * (1 - sel) = 0; - // This is now guaranteed to be mututally exclusive because of the above condition and since sel = 0 at row = 0 (since it has shifts) + + // LATCH_CONDITION is the sum of latch and first_row. We need to ensure these are mutually + // exclusive (i.e., LATCH_CONDITION is always 0 or 1, never 2) for start to remain boolean. + // + // Proof that latch = 0 when first_row = 1 (i.e., on row 0): + // + // For latch_0 = 1, the zero-check constraint (sha256.pil) requires rounds_remaining_0 = 0. + // Also, LATCH_HAS_SEL_ON requires sel_0 = 1. + // + // From START_AFTER_LAST on the last row (N-1): sel_0 * (start_0 - LATCH_CONDITION_{N-1}) = 0 + // Since sel_0 = 1: start_0 = LATCH_CONDITION_{N-1} + // + // Case A: LATCH_CONDITION_{N-1} = 1 (last row has latch = 1) + // - start_0 = 1 + // - Round initialization constraint: start * (rounds_remaining - 64) = 0 + // - This forces rounds_remaining_0 = 64 + // - CONTRADICTION: rounds_remaining_0 cannot be both 0 (for latch=1) and 64 (for start=1) + // - This case is impossible - constraints are unsatisfiable. + // + // Case B: LATCH_CONDITION_{N-1} = 0 (last row has latch = 0, boundary-spanning computation) + // - start_0 = 0 + // - LATCH_CONDITION_0 = latch_0 + first_row_0 = 1 + 1 = 2 + // - perform_round_0 = (1 - LATCH_CONDITION_0) * SEL_NO_ERR = (1 - 2) * 1 = -1 + // - sel_compute_w and other selectors derived from perform_round become non-boolean (-1) + // - Lookups using these selectors contribute -1 to the grand product + // - Destination selectors are boolean (0 or 1), so lookups CANNOT balance + // - This case fails lookup constraints - no valid proof can be generated. + // + // Therefore, latch = 1 on row 0 is impossible in any valid trace, and LATCH_CONDITION + // is guaranteed to be 0 or 1. pol LATCH_CONDITION = latch + precomputed.first_row; #[START_AFTER_LAST]