feat(sol): sign gadget (#860)

stuarttimwhite · web-flow · commit e088a2774b93 · 2025-06-04T22:01:50.000Z
Please be sure to look over the pull request guidelines here: https://github.com/spaceandtimelabs/sxt-proof-of-sql/blob/main/CONTRIBUTING.md#submit-pr. # Please go through the following checklist - [ ] The PR title and commit messages adhere to guidelines here: https://github.com/spaceandtimelabs/sxt-proof-of-sql/blob/main/CONTRIBUTING.md. In particular `!` is used if and only if at least one breaking change has been introduced. - [ ] I have run the ci check script with `source scripts/run_ci_checks.sh`. - [ ] I have run the clean commit check script with `source scripts/check_commits.sh`, and the commit history is certified to follow clean commit guidelines as described here: https://github.com/spaceandtimelabs/sxt-proof-of-sql/blob/main/COMMIT_GUIDELINES.md - [ ] The latest changes from `main` have been incorporated to this PR by simple rebase if possible, if not, then conflicts are resolved appropriately. # Rationale for this change We need sign_expr for group by # What changes are included in this PR? New sign_expr in solidity. # Are these changes tested? Yes
diff --git a/solidity/src/base/Constants.sol b/solidity/src/base/Constants.sol
@@ -6,6 +6,8 @@ pragma solidity ^0.8.28;
 uint256 constant MODULUS = 0x30644e72_e131a029_b85045b6_8181585d_2833e848_79b97091_43e1f593_f0000001;
 /// @dev The largest mask that can be applied to a 256-bit number in order to enforce that it is less than the modulus.
 uint256 constant MODULUS_MASK = 0x1FFFFFFF_FFFFFFFF_FFFFFFFF_FFFFFFFF_FFFFFFFF_FFFFFFFF_FFFFFFFF_FFFFFFFF;
+/// @dev A mask that can be applied to a bit distributions vary mask to see if it is valid, given the modulus.
+uint256 constant MODULUS_INVALID_VARY_MASK = 0x60000000_00000000_00000000_00000000_00000000_00000000_00000000_00000000;
 /// @dev MODULUS + 1. Needs to be explicit for Yul usage.
 uint256 constant MODULUS_PLUS_ONE = 0x30644e72_e131a029_b85045b6_8181585d_2833e848_79b97091_43e1f593_f0000002;
 /// @dev MODULUS - 1. Needs to be explicit for Yul usage.
@@ -174,7 +176,7 @@ uint256 constant VK_TAU_HY_REAL = 0x2bad9a374aec49d329ec66e8f530f68509313450580c
 uint256 constant VK_TAU_HY_IMAG = 0x219edfceee1723de674f5b2f6fdb69d9e32dd53b15844956a630d3c7cdaa6ed9;
 
 /// @dev Size of the verification builder in bytes.
-uint256 constant VERIFICATION_BUILDER_SIZE = 0x20 * 14;
+uint256 constant VERIFICATION_BUILDER_SIZE = 0x20 * 15;
 /// @dev Offset of the pointer to the challenge queue in the verification builder.
 uint256 constant BUILDER_CHALLENGES_OFFSET = 0x20 * 0;
 /// @dev Offset of the pointer to the first round MLEs in the verification builder.
@@ -203,6 +205,8 @@ uint256 constant BUILDER_FIRST_ROUND_COMMITMENTS_OFFSET = 0x20 * 11;
 uint256 constant BUILDER_FINAL_ROUND_COMMITMENTS_OFFSET = 0x20 * 12;
 /// @dev Offset of the singleton chi evaluation in the verification builder.
 uint256 constant BUILDER_SINGLETON_CHI_EVALUATION_OFFSET = 0x20 * 13;
+/// @dev Offset of the pointer to the final round bit distributions in the verification builder.
+uint256 constant BUILDER_FINAL_ROUND_BIT_DISTRIBUTIONS_OFFSET = 0x20 * 14;
 
 /// @dev The initial transcript state. This is the hash of the empty string.
 uint256 constant INITIAL_TRANSCRIPT_STATE = 0x7c26f909f37b2c61df0bb3b19f76296469cb4d07b582a215c4e2b1f7a05527c3;
diff --git a/solidity/src/base/Errors.sol b/solidity/src/base/Errors.sol
@@ -55,6 +55,10 @@ uint32 constant ERR_UNSUPPORTED_PROOF_PLAN_VARIANT = 0xe5503cfa;
 uint32 constant ERR_UNSUPPORTED_DATA_TYPE_VARIANT = 0xbd12560e;
 /// @dev Error code for when the evaluation length is too large.
 uint32 constant ERR_EVALUATION_LENGTH_TOO_LARGE = 0xb65e7142;
+/// @dev Error code for when a bit decomposition is invalid.
+uint32 constant ERR_BIT_DECOMPOSITION_INVALID = 0xda443b2b;
+/// @dev Error code for when bits that shouldn't vary do vary.
+uint32 constant ERR_INVALID_VARYING_BITS = 0x76d56a3d;
 
 library Errors {
     /// @notice Error thrown when the inputs to the ECADD precompile are invalid.
@@ -110,6 +114,10 @@ library Errors {
     error UnsupportedDataTypeVariant();
     /// @notice Error thrown when the evaluation length is too large.
     error EvaluationLengthTooLarge();
+    /// @notice Error thrown when a bit decomposition is invalid.
+    error BitDecompositionInvalid();
+    /// @notice Error thrown when bits that shouldn't vary do vary.
+    error InvalidVaryingBits();
 
     function __err(uint32 __code) internal pure {
         assembly {
diff --git a/solidity/src/base/Queue.pre.sol b/solidity/src/base/Queue.pre.sol
@@ -42,4 +42,47 @@ library Queue {
             __value := dequeue(__queue)
         }
     }
+
+    /// @notice Dequeues two uint256 values from the front of the queue
+    /// @custom:as-yul-wrapper
+    /// #### Wrapped Yul Function
+    /// ##### Signature
+    /// ```yul
+    /// function dequeue_uint512(queue_ptr) -> upper, lower
+    /// ```
+    /// ##### Parameters
+    /// * `queue_ptr` - pointer to the array in memory. In Solidity memory layout,
+    ///   this points to where the array length is stored, followed by the array elements
+    /// ##### Return Values
+    /// * `upper` - the first word from the dequeued value from the front of the queue
+    /// * `lower` - the second word from the dequeued value from the front of the queue
+    /// @dev Removes and returns the first element from the queue.
+    /// Reverts with Errors.EmptyQueue if the queue is empty.
+    /// @param __queuePtr Single-element array containing the queue array
+    /// @return __upper The first word from the dequeued value from the front of the queue
+    /// @return __lower The second word from the dequeued value from the front of the queue
+    function __dequeueUint512(uint256[][1] memory __queuePtr)
+        internal
+        pure
+        returns (uint256 __upper, uint256 __lower)
+    {
+        assembly {
+            // IMPORT-YUL Errors.sol
+            function err(code) {
+                revert(0, 0)
+            }
+            function dequeue_uint512(queue_ptr) -> upper, lower {
+                let queue := mload(queue_ptr)
+                let length := mload(queue)
+                if iszero(length) { err(ERR_EMPTY_QUEUE) }
+                queue := add(queue, WORD_SIZE)
+                upper := mload(queue)
+                queue := add(queue, WORD_SIZE)
+                lower := mload(queue)
+                mstore(queue, sub(length, 1))
+                mstore(queue_ptr, queue)
+            }
+            __upper, __lower := dequeue_uint512(__queuePtr)
+        }
+    }
 }
diff --git a/solidity/src/builder/VerificationBuilder.pre.sol b/solidity/src/builder/VerificationBuilder.pre.sol
@@ -778,12 +778,50 @@ library VerificationBuilder {
                 revert(0, 0)
             }
             function builder_set_bit_distributions(builder_ptr, values_ptr) {
-                if mload(values_ptr) { err(ERR_UNSUPPORTED_PROOF) }
+                mstore(add(builder_ptr, BUILDER_FINAL_ROUND_BIT_DISTRIBUTIONS_OFFSET), values_ptr)
             }
             builder_set_bit_distributions(__builder, __values)
         }
     }
 
+    /// @notice Consumes a final round bit distribution from the verification builder
+    /// @custom:as-yul-wrapper
+    /// #### Wrapped Yul Function
+    /// ##### Signature
+    /// ```yul
+    /// builder_consume_bit_distribution(builder_ptr) -> vary_mask, leading_bit_mask
+    /// ```
+    /// ##### Parameters
+    /// * `builder_ptr` - memory pointer to the builder struct region
+    /// ##### Return Values
+    /// * `vary_mask` - the vary mask of the bit distribution
+    /// * `leading_bit_mask` - the leading bit mask of the bit distribution
+    /// @dev Dequeues and returns a final round bit distribution. Reverts with Errors.EmptyQueue if no values remain
+    /// @param __builder The builder struct
+    /// @return __varyMask the vary mask of the consumed bit distribution
+    /// @return __leadingBitMask the leading bit mask of the consumed bit distribution
+    function __consumeBitDistribution(Builder memory __builder)
+        internal
+        pure
+        returns (uint256 __varyMask, uint256 __leadingBitMask)
+    {
+        assembly {
+            // IMPORT-YUL ../base/Errors.sol
+            function err(code) {
+                revert(0, 0)
+            }
+            // IMPORT-YUL ../base/Queue.pre.sol
+            function dequeue_uint512(queue_ptr) -> upper, lower {
+                revert(0, 0)
+            }
+            function builder_consume_bit_distribution(builder_ptr) -> vary_mask, leading_bit_mask {
+                let values_ptr := add(builder_ptr, BUILDER_FINAL_ROUND_BIT_DISTRIBUTIONS_OFFSET)
+                vary_mask, leading_bit_mask := dequeue_uint512(values_ptr)
+            }
+            __varyMask, __leadingBitMask := builder_consume_bit_distribution(__builder)
+        }
+    }
+
     /// @notice Gets the chi column evaluations array from the verification builder
     /// @custom:as-yul-wrapper
     /// #### Wrapped Yul Function
diff --git a/solidity/src/proof_gadgets/SignExpr.pre.sol b/solidity/src/proof_gadgets/SignExpr.pre.sol
@@ -0,0 +1,165 @@
+// SPDX-License-Identifier: UNLICENSED
+// This is licensed under the Cryptographic Open Software License 1.0
+pragma solidity ^0.8.28;
+
+import "../base/Constants.sol";
+import "../base/Errors.sol";
+import {VerificationBuilder} from "../builder/VerificationBuilder.pre.sol";
+
+/// @title SignExpr
+/// @dev Library for handling the sign of an evaluation
+library SignExpr {
+    /// @notice Evaluates a sign expression by finding the sign of an expression evaluation
+    /// @custom:as-yul-wrapper
+    /// #### Wrapped Yul Function
+    /// ##### Signature
+    /// ```yul
+    /// sign_expr_evaluate(expr_eval, builder_ptr, chi_eval) -> eval
+    /// ```
+    /// ##### Parameters
+    /// * `expr_eval` - the expression evaluation
+    /// * `builder_ptr` - memory pointer to the verification builder
+    /// * `chi_eval` - the chi value for evaluation
+    /// ##### Return Values
+    /// * `eval` - the evaluation result from the builder's final round MLE (or bit distribution)
+    /// @notice Evaluates the sign of an expression
+    /// ##### Proof Plan Encoding
+    /// The sign expression is encoded as follows:
+    /// The expression
+    /// @param __exprEval The expression evaluation
+    /// @param __builder The verification builder
+    /// @param __chiEval The chi value for evaluation
+    /// @return __builderOut The verification builder result
+    /// @return __eval The evaluated result
+    function __signExprEvaluate( // solhint-disable-line gas-calldata-parameters
+    uint256 __exprEval, VerificationBuilder.Builder memory __builder, uint256 __chiEval)
+        internal
+        pure
+        returns (VerificationBuilder.Builder memory __builderOut, uint256 __eval)
+    {
+        assembly {
+            // IMPORT-YUL ../base/Errors.sol
+            function err(code) {
+                revert(0, 0)
+            }
+            // IMPORT-YUL ../base/Queue.pre.sol
+            function dequeue(queue_ptr) -> value {
+                revert(0, 0)
+            }
+            // IMPORT-YUL ../base/Queue.pre.sol
+            function dequeue_uint512(queue_ptr) -> value {
+                revert(0, 0)
+            }
+            // IMPORT-YUL ../base/MathUtil.sol
+            function addmod_bn254(lhs, rhs) -> sum {
+                revert(0, 0)
+            }
+            // IMPORT-YUL ../base/MathUtil.sol
+            function submod_bn254(lhs, rhs) -> difference {
+                revert(0, 0)
+            }
+            // IMPORT-YUL ../base/MathUtil.sol
+            function mulmod_bn254(lhs, rhs) -> product {
+                revert(0, 0)
+            }
+            // IMPORT-YUL ../base/SwitchUtil.pre.sol
+            function case_const(lhs, rhs) {
+                revert(0, 0)
+            }
+            // IMPORT-YUL ../builder/VerificationBuilder.pre.sol
+            function builder_consume_final_round_mle(builder_ptr) -> value {
+                revert(0, 0)
+            }
+            // IMPORT-YUL ../base/Array.pre.sol
+            function get_array_element(arr_ptr, index) -> value {
+                revert(0, 0)
+            }
+            // IMPORT-YUL ../builder/VerificationBuilder.pre.sol
+            function builder_consume_bit_distribution(builder_ptr) -> vary_mask, leading_bit_mask {
+                revert(0, 0)
+            }
+            // IMPORT-YUL ../builder/VerificationBuilder.pre.sol
+            function builder_produce_identity_constraint(builder_ptr, evaluation, degree) {
+                revert(0, 0)
+            }
+            // IMPORT-YUL ../base/DataType.pre.sol
+            function read_entry(result_ptr, data_type_variant) -> result_ptr_out, entry {
+                revert(0, 0)
+            }
+            // IMPORT-YUL ../base/DataType.pre.sol
+            function read_binary(result_ptr) -> result_ptr_out, entry {
+                revert(0, 0)
+            }
+            // IMPORT-YUL ../base/DataType.pre.sol
+            function read_data_type(ptr) -> ptr_out, data_type {
+                revert(0, 0)
+            }
+
+            function sign_expr_evaluate(expr_eval, builder_ptr, chi_eval) -> result_eval {
+                let vary_mask
+                let leading_bit_mask
+                vary_mask, leading_bit_mask := builder_consume_bit_distribution(builder_ptr)
+
+                // Other than the lead bit, no bit should vary past some max bit position, depending on the field
+                if and(vary_mask, MODULUS_INVALID_VARY_MASK) { err(ERR_INVALID_VARYING_BITS) }
+
+                // The lead bit of the leading_bit_mask dictates the sign, if it's constant sign.
+                // So this will be the value if sign is constant. Otherwise, it will be overwritten
+                let sign_eval := mulmod_bn254(shr(255, leading_bit_mask), chi_eval)
+
+                // For future computations, leading_bit_mask should have a 1 in the lead bit
+                leading_bit_mask := or(leading_bit_mask, shl(255, 1))
+
+                // leading_bit_inverse_mask identifies columns that match the inverse of the lead bit column
+                // So !vary_mask ^ leading_bit_mask, with a lead bit of zero.
+                let leading_bit_inverse_mask := shr(1, shl(1, xor(not(vary_mask), leading_bit_mask)))
+
+                // sum_eval should ultimately add up to the original column of data
+                // It will effectively be a recomposition of the bit decomposition
+                let sum_eval := 0
+
+                for { let i := 0 } vary_mask {
+                    i := add(i, 1)
+                    vary_mask := shr(1, vary_mask)
+                } {
+                    if and(vary_mask, 1) {
+                        // For any varying bits...
+                        let bit_eval := builder_consume_final_round_mle(builder_ptr)
+
+                        // Verify that every eval is a bit
+                        // bit_eval - bit_eval * bit_eval = 0
+                        builder_produce_identity_constraint(
+                            builder_ptr, submod_bn254(bit_eval, mulmod_bn254(bit_eval, bit_eval)), 2
+                        )
+
+                        switch i
+                        // If the lead bit varies, that we get the sign from the mles.
+                        case 255 { sign_eval := bit_eval }
+                        // For varying non lead bits,
+                        // we add bit_eval * 2ⁱ to the sum in order to recompose the original value of the column
+                        default { sum_eval := addmod_bn254(sum_eval, mulmod_bn254(bit_eval, shl(i, 1))) }
+                    }
+                }
+
+                result_eval := submod_bn254(chi_eval, sign_eval)
+
+                // For constant and lead bits...
+                // sum += sign_eval * leading_bit_mask + (sign_eval - chi_eval) * leading_bit_inverse_mask - chi_eval * (1 << 255)
+                sum_eval :=
+                    submod_bn254(
+                        addmod_bn254(
+                            addmod_bn254(sum_eval, mulmod_bn254(sign_eval, leading_bit_mask)),
+                            mulmod_bn254(result_eval, leading_bit_inverse_mask)
+                        ),
+                        mulmod_bn254(chi_eval, shl(255, 1))
+                    )
+
+                // Verify the bit recomposition matches the original column evaluation
+                if sub(sum_eval, expr_eval) { err(ERR_BIT_DECOMPOSITION_INVALID) }
+            }
+
+            __eval := sign_expr_evaluate(__exprEval, __builder, __chiEval)
+        }
+        __builderOut = __builder;
+    }
+}
diff --git a/solidity/test/base/Constants.t.sol b/solidity/test/base/Constants.t.sol
@@ -21,6 +21,11 @@ contract ConstantsTest is Test {
         assert(mask == 0);
     }
 
+    function testModulusMaskAndModulusInvalidVaryMaskAgree() public pure {
+        assert(MODULUS_MASK & MODULUS_INVALID_VARY_MASK == 0);
+        assert(MODULUS_MASK | MODULUS_INVALID_VARY_MASK == (1 << 255) - 1);
+    }
+
     function testModulusPlusAndMinusOneAreCorrect() public pure {
         assert(MODULUS_PLUS_ONE == MODULUS + 1);
         assert(MODULUS_MINUS_ONE == MODULUS - 1);
@@ -85,7 +90,7 @@ contract ConstantsTest is Test {
     }
 
     function testVerificationBuilderOffsetsAreValid() public pure {
-        uint256[14] memory offsets = [
+        uint256[15] memory offsets = [
             BUILDER_CHALLENGES_OFFSET,
             BUILDER_FIRST_ROUND_MLES_OFFSET,
             BUILDER_FINAL_ROUND_MLES_OFFSET,
@@ -99,7 +104,8 @@ contract ConstantsTest is Test {
             BUILDER_TABLE_CHI_EVALUATIONS_OFFSET,
             BUILDER_FIRST_ROUND_COMMITMENTS_OFFSET,
             BUILDER_FINAL_ROUND_COMMITMENTS_OFFSET,
-            BUILDER_SINGLETON_CHI_EVALUATION_OFFSET
+            BUILDER_SINGLETON_CHI_EVALUATION_OFFSET,
+            BUILDER_FINAL_ROUND_BIT_DISTRIBUTIONS_OFFSET
         ];
         uint256 offsetsLength = offsets.length;
         assert(VERIFICATION_BUILDER_SIZE == offsetsLength * WORD_SIZE);
diff --git a/solidity/test/base/Queue.t.pre.sol b/solidity/test/base/Queue.t.pre.sol
@@ -27,6 +27,19 @@ contract ErrorsTest is Test {
         Queue.__dequeue(queue);
     }
 
+    /// forge-config: default.allow_internal_expect_revert = true
+    function testDequeueUint512() public pure {
+        uint256[][1] memory queue = [new uint256[](2)];
+        queue[0][0] = 1001;
+        queue[0][1] = 1002;
+        (uint256 upper, uint256 lower) = Queue.__dequeueUint512(queue);
+        assert(upper == 1001);
+        assert(lower == 1002);
+        // This is a little hacky. Even though we lost two elements, the length only drops by one,
+        // because the dequeue function is interpreting it as a 512 array
+        assert(queue[0].length == 1);
+    }
+
     /// forge-config: default.allow_internal_expect_revert = true
     function testFuzzDequeue(uint256[][1] memory queue) public {
         uint256 length = queue[0].length;
diff --git a/solidity/test/builder/VerificationBuilder.t.pre.sol b/solidity/test/builder/VerificationBuilder.t.pre.sol
diff --git a/solidity/test/proof_gadgets/SignExpr.t.pre.sol b/solidity/test/proof_gadgets/SignExpr.t.pre.sol
