From 8df42086acac6fbd4ffdb2cfeb54a0aa59b3d406 Mon Sep 17 00:00:00 2001 From: Lydia Garms Date: Wed, 24 Jun 2026 15:27:49 +0100 Subject: [PATCH 1/4] fix(circuits): underflow constraints --- circuits/common/splitCommitments.zok | 1 + .../zokrates/raw/BoilerplateGenerator.ts | 25 ++- .../circuit/zokrates/toCircuit.ts | 184 ++++++++++++++++-- 3 files changed, 178 insertions(+), 32 deletions(-) diff --git a/circuits/common/splitCommitments.zok b/circuits/common/splitCommitments.zok index e9c105811..a25b23fba 100644 --- a/circuits/common/splitCommitments.zok +++ b/circuits/common/splitCommitments.zok @@ -92,6 +92,7 @@ def main( // prepare secret state 'newCommitments' for commitments field newCommitment_0_value_field = value; + assert(oldCommitment_0_value >= value); field newCommitment_1_value_field = oldCommitment_0_value - value; // preimage check - newCommitment_commitment diff --git a/src/boilerplate/circuit/zokrates/raw/BoilerplateGenerator.ts b/src/boilerplate/circuit/zokrates/raw/BoilerplateGenerator.ts index f02273508..dec1eeb84 100644 --- a/src/boilerplate/circuit/zokrates/raw/BoilerplateGenerator.ts +++ b/src/boilerplate/circuit/zokrates/raw/BoilerplateGenerator.ts @@ -335,29 +335,20 @@ class BoilerplateGenerator { ]; }, - postStatements({ name: x, isWhole, isNullified, newCommitmentValue, structProperties, structPropertiesTypes, typeName }): string[] { + postStatements({ name: x, isWhole, isNullified, structProperties, structPropertiesTypes, typeName }): string[] { // if (!isWhole && !newCommitmentValue) throw new Error('PATH'); let y = isWhole ? x : x.slice(0, -2); const lines: string[] = []; if (!isWhole && isNullified) { // decrement - const i = parseInt(x.slice(-1), 10); - const x0 = x.slice(0, -1) + `${i-2}`; - const x1 = x.slice(0, -1) + `${i-1}`; if (!structProperties) { lines.push( - `assert(${y} >0); - // TODO: assert no under/overflows - - field ${x}_newCommitment_value_field = ${y};` + `field ${x}_newCommitment_value_field = ${y};` ); } else { // TODO types for each structProperty lines.push( - `${structProperties.map(p => newCommitmentValue[p] === '0' ? '' : `assert(${y}.${p} > 0);`).join('\n')} - // TODO: assert no under/overflows - - ${typeName} ${x}_newCommitment_value = ${typeName} { ${structProperties.map(p => ` ${p}: ${y}.${p}`)} };` + `${typeName} ${x}_newCommitment_value = ${typeName} { ${structProperties.map(p => ` ${p}: ${y}.${p}`)} };` ); } } else { @@ -551,9 +542,15 @@ class BoilerplateGenerator { statements({ name: x, subtrahend, newCommitmentValue, structProperties, memberName}): string[] { if (subtrahend.decrementType === '-='){ if (structProperties) { - return [`${x}.${memberName} = ${x}.${memberName} - (${newCommitmentValue});`] + return [ + `assert(${x}.${memberName} >= (${newCommitmentValue})); + ${x}.${memberName} = ${x}.${memberName} - (${newCommitmentValue});`, + ]; } - return [`${x} = ${x} - (${newCommitmentValue});`]; + return [ + `assert(${x} >= (${newCommitmentValue})); + ${x} = ${x} - (${newCommitmentValue});`, + ]; } else if (subtrahend.decrementType === '='){ if (structProperties) { return [`${x}.${memberName} = ${newCommitmentValue};`] diff --git a/src/codeGenerators/circuit/zokrates/toCircuit.ts b/src/codeGenerators/circuit/zokrates/toCircuit.ts index f84c36a46..3df0266b6 100644 --- a/src/codeGenerators/circuit/zokrates/toCircuit.ts +++ b/src/codeGenerators/circuit/zokrates/toCircuit.ts @@ -16,6 +16,92 @@ const keepOneTrailingSemicolon = (code: string) => { return code.endsWith('}') ? code : code.replace(/;+$/, '') + ';'; }; +// Traverses a node to check for any guards that are necessary to prevent underflows +const underflowGuardConditions = ( + node: any, + codeGeneratorState: any, + seen = new Set(), +): string[] => { + if (!node) return []; + if (Array.isArray(node)) return node.flatMap(child => underflowGuardConditions(child, codeGeneratorState, seen)); + if (typeof node !== 'object') return []; + if (seen.has(node)) return []; + seen.add(node); + + switch (node.nodeType) { + // If the node is a binary operation with operator "-", we return a guard to prevent underflows, analogously to solidity, + // otherwise we traverse the child nodes + case 'BinaryOperation': { + const subExpressionConditions = [ + ...underflowGuardConditions(node.leftExpression, codeGeneratorState, seen), + ...underflowGuardConditions(node.rightExpression, codeGeneratorState, seen), + ]; + if (node.operator !== '-') return subExpressionConditions; + return [ + ...subExpressionConditions, + `${codeGenerator(node.leftExpression, codeGeneratorState)} >= ${codeGenerator(node.rightExpression, codeGeneratorState)}`, + ]; + } + + // We only need to prevent underflows in if statements if the branch of the if statement is taken + case 'Conditional': { + const condition = removeTrailingSemicolon(codeGenerator(node.condition, codeGeneratorState)); + return [ + ...underflowGuardConditions(node.condition, codeGeneratorState, seen), + ...underflowGuardConditions(node.trueExpression, codeGeneratorState, seen).map(guard => `!(${condition}) || (${guard})`), + ...underflowGuardConditions(node.falseExpression, codeGeneratorState, seen).map(guard => `(${condition}) || (${guard})`), + ]; + } + + case 'UnaryOperation': { + const subExpressionConditions = underflowGuardConditions( + node.subExpression, + codeGeneratorState, + seen, + ); + if (node.operator !== '--') return subExpressionConditions; + return [ + ...subExpressionConditions, + `${codeGenerator(node.subExpression, codeGeneratorState)} >= 1`, + ]; + } + + default: + return Object.values(node).flatMap(child => underflowGuardConditions(child, codeGeneratorState, seen)); + } +}; + +const underflowGuardAssertions = (node: any, codeGeneratorState: any) => { + return underflowGuardConditions(node, codeGeneratorState) + .map(guard => ` assert(${guard});`) + .join('\n'); +}; + +// Adds a guard to the statement to prevent underflows +const withUnderflowGuardAssertions = (node: any, statement: string, codeGeneratorState: any) => { + const guards = underflowGuardAssertions(node, codeGeneratorState); + return guards ? `${guards}\n${statement}` : statement; +}; + +const assignmentStatement = (node: any, codeGeneratorState: any) => + `${codeGenerator(node.leftHandSide, codeGeneratorState)} ${node.operator} ${codeGenerator(node.rightHandSide, codeGeneratorState)};`; + +// Return an underflow guard that only is enforced if a condition is satisfied +const conditionalUnderflowGuardAssertions = ( + node: any, + condition: string, + activeWhenTrue: boolean, + codeGeneratorState: any, +) => { + return underflowGuardConditions(node, codeGeneratorState) + .map(guard => + activeWhenTrue + ? `\n assert(!(${condition}) || (${guard}));` + : `\n assert((${condition}) || (${guard}));`, + ) + .join(''); +}; + function poseidonLibraryChooser(fileObj: string) { if (!fileObj.includes('poseidon')) return fileObj; let poseidonFieldCount = 0; @@ -241,12 +327,12 @@ codeGeneratorState.wrapperFunctions.set(functionName, wrapperFunction); if(node.initialValue?.nodeType === 'InternalFunctionCall'){ if(!declarations) return ; if(node.initialValue?.expression?.nodeType === 'BinaryOperation') - return `${declarations} = ${codeGenerator(node.initialValue.expression, codeGeneratorState)};`; - return `${declarations} = ${node.initialValue.name};`; + return withUnderflowGuardAssertions(node.initialValue, `${declarations} = ${codeGenerator(node.initialValue.expression, codeGeneratorState)};`, codeGeneratorState); + return withUnderflowGuardAssertions(node.initialValue, `${declarations} = ${node.initialValue.name};`, codeGeneratorState); } const initialValue = codeGenerator(node.initialValue, codeGeneratorState); - return `${declarations} = ${initialValue};`; + return withUnderflowGuardAssertions(node.initialValue, `${declarations} = ${initialValue};`, codeGeneratorState); } case 'ElementaryTypeName': @@ -262,6 +348,21 @@ codeGeneratorState.wrapperFunctions.set(functionName, wrapperFunction); case 'ExpressionStatement': { if (node.isVarDec) { + if (node.expression?.nodeType === 'Assignment') { + const declarationType = + node.expression?.leftHandSide?.typeName === 'bool' + ? 'bool' + : 'field'; + return withUnderflowGuardAssertions( + node.expression, + ` + ${declarationType} mut ${assignmentStatement( + node.expression, + codeGeneratorState, + )}`, + codeGeneratorState, + ); + } if (node.expression?.leftHandSide?.typeName === 'bool'){ return ` bool mut ${codeGenerator(node.expression, codeGeneratorState)}`; @@ -295,13 +396,21 @@ codeGeneratorState.wrapperFunctions.set(functionName, wrapperFunction); return ` ` ; case 'Assignment': - return `${codeGenerator(node.leftHandSide, codeGeneratorState)} ${node.operator} ${codeGenerator(node.rightHandSide, codeGeneratorState)};`; + return withUnderflowGuardAssertions( + node, + assignmentStatement(node, codeGeneratorState), + codeGeneratorState, + ); case 'UnaryOperation': if (node.subExpression?.typeName?.name === 'bool' && node.operator === '!'){ return `${node.operator}${node.subExpression.name};`; } - return `${codeGenerator(node.initialValue, codeGeneratorState)} = ${codeGenerator(node.subExpression, codeGeneratorState)} ${node.operator[0]} 1;`; + return withUnderflowGuardAssertions( + node, + `${codeGenerator(node.initialValue, codeGeneratorState)} = ${codeGenerator(node.subExpression, codeGeneratorState)} ${node.operator[0]} 1;`, + codeGeneratorState, + ); case 'BinaryOperation': if (node.operator === '/') { @@ -361,6 +470,8 @@ codeGeneratorState.wrapperFunctions.set(functionName, wrapperFunction); node.condition.rightExpression.name = node.condition.rightExpression.name.replace('_temp',''); if(node.condition.leftExpression.nodeType == 'Identifier') node.condition.leftExpression.name = node.condition.leftExpression.name.replace('_temp',''); + const conditionUnderflowGuards = underflowGuardAssertions(node.condition, codeGeneratorState); + if (conditionUnderflowGuards) initialStatements += `\n${conditionUnderflowGuards}`; initialStatements+= ` assert(!(${codeGenerator(node.condition, codeGeneratorState)}));`; return initialStatements; @@ -374,11 +485,17 @@ codeGeneratorState.wrapperFunctions.set(functionName, wrapperFunction); ${varDec} ${codeGenerator(elt, codeGeneratorState)}_temp = ${codeGenerator(elt, codeGeneratorState)};`; } }); + const condition = removeTrailingSemicolon(codeGenerator(node.condition, codeGeneratorState)); + // Check for underflow in the condition of the if statement + const conditionUnderflowGuards = underflowGuardAssertions(node.condition, codeGeneratorState); + if (conditionUnderflowGuards) initialStatements += `\n${conditionUnderflowGuards}`; for (let i =0; i= c + return guardNode + ? withUnderflowGuardAssertions(guardNode, Circuitbp.generateBoilerplate(node), codeGeneratorState) + : Circuitbp.generateBoilerplate(node); } // And if we haven't recognized the node, we'll throw an error. From 62d98ca270f9e77e251194da080ae8a6b7b64267 Mon Sep 17 00:00:00 2001 From: Lydia Garms Date: Thu, 2 Jul 2026 14:32:55 +0100 Subject: [PATCH 2/4] chore(tests): add test contract for underflows --- test/contracts/action-tests/Underflows.zol | 140 +++++++++++++++++++++ 1 file changed, 140 insertions(+) create mode 100644 test/contracts/action-tests/Underflows.zol diff --git a/test/contracts/action-tests/Underflows.zol b/test/contracts/action-tests/Underflows.zol new file mode 100644 index 000000000..ce895723c --- /dev/null +++ b/test/contracts/action-tests/Underflows.zol @@ -0,0 +1,140 @@ +// SPDX-License-Identifier: CC0 + +pragma solidity ^0.8.0; + +contract MyContract { + + secret uint256 private a; + secret mapping(address => uint256) private balances; + uint256 public publicCounter; + + function assign(secret uint256 value) public { + a = value; + } + + function compoundSub(secret uint256 amount) public { + a -= amount; + } + + function assignmentSub(secret uint256 amount) public { + a = a - amount; + } + + function localDeclarationSub(secret uint256 amount) public { + secret uint256 remaining = a - amount; + a = remaining; + } + + function requireSub(secret uint256 amount, secret uint256 minimum) public { + require(a - amount >= minimum, "a - amount too low"); + a = a - amount; + } + + function unknownMappingDecSub(secret uint256 value, secret uint256 amount) public { + unknown balances[msg.sender] -= value - amount; + } + + function unknownMappingAddNestedSub(secret uint256 value, secret uint256 amount, secret uint256 fee) public { + unknown balances[msg.sender] += value - (amount - fee); + } + + function unknownMappingNestedSub(secret uint256 value, secret uint256 amount, secret uint256 fee) public { + unknown balances[msg.sender] -= value - (amount - fee); + } + + function publicUnaryIncrementThenSecret(secret uint256 value) public { + publicCounter++; + known a += value + publicCounter; + } + + function publicUnaryDecrementThenSecret(secret uint256 value) public { + publicCounter--; + known a += value + publicCounter; + } + + // The following two functions do not compile because of a bug where threshold is not a circuit parameter + //function publicUnaryDecrementTrueBranchThenSecret(secret uint256 value, uint256 threshold) public { + // if (threshold > 0) { + // publicCounter--; + // } + // known a += value + publicCounter; + //} + + //function publicUnaryDecrementFalseBranchThenSecret(secret uint256 value, uint256 threshold) public { + // if (threshold > 0) { + // publicCounter++; + // } else { + // publicCounter--; + // } + // known a += value + publicCounter; + //} + + // The following four functions do not compile because of a bug where start is not a circuit parameter + //function localUnaryIncrementThenSecret(secret uint256 value, uint256 start) public { + // uint256 counter = start; + // counter++; + // known a += value + counter; + //} + + //function localUnaryDecrementThenSecret(secret uint256 value, uint256 start) public { + // uint256 counter = start; + // counter--; + // known a += value + counter; + //} + + //function localUnaryDecrementTrueBranchThenSecret(secret uint256 value, uint256 start, uint256 threshold) public { + // uint256 counter = start; + // if (threshold > 0) { + // counter--; + // } + // known a += value + counter; + //} + + //function localUnaryDecrementFalseBranchThenSecret(secret uint256 value, uint256 start, uint256 threshold) public { + // uint256 counter = start; + // if (threshold > 0) { + // counter++; + // } else { + // counter--; + // } + // known a += value + counter; + //} + + function addThenSub(secret uint256 amount1, secret uint256 amount) public { + a = a + amount1 - amount; + } + + function subThenAdd(secret uint256 amount, secret uint256 amount1) public { + a = a - amount + amount1; + } + + function parenthesizedSub(secret uint256 amount1, secret uint256 amount) public { + a = a + (amount1 - amount); + } + + function parenthesizedSub2(secret uint256 amount1, secret uint256 amount) public { + a = a - (amount1 - amount); + } + + function branchSub(secret uint256 threshold, secret uint256 amount) public { + if (a > threshold) { + a -= amount; + } + } + + // Does not compile because of a bug where start is not a circuit parameter + //function loopInitSub(secret uint256 value, uint256 start, uint256 amount) public { + // for (uint256 index = start - amount; index < 5; index++) { + // known a += value; + // } + //} + + // Does not compile because of a bug where a_temp is not defined + //function revertIfSub(secret uint256 amount, secret uint256 minimum) public { + // if (a - amount < minimum) { + // revert(); + // } + // known a += 1; + //} + +} From dfc706718cf57eb02ec2035fda1faccd71d78f2a Mon Sep 17 00:00:00 2001 From: Lydia Garms Date: Mon, 13 Jul 2026 16:56:43 +0100 Subject: [PATCH 3/4] fix(circuits): underflows for conditions with ||/ && --- .../circuit/zokrates/toCircuit.ts | 23 +++++++++++++++---- test/contracts/action-tests/Underflows.zol | 5 ++++ 2 files changed, 24 insertions(+), 4 deletions(-) diff --git a/src/codeGenerators/circuit/zokrates/toCircuit.ts b/src/codeGenerators/circuit/zokrates/toCircuit.ts index 3df0266b6..0a7b70673 100644 --- a/src/codeGenerators/circuit/zokrates/toCircuit.ts +++ b/src/codeGenerators/circuit/zokrates/toCircuit.ts @@ -32,10 +32,25 @@ const underflowGuardConditions = ( // If the node is a binary operation with operator "-", we return a guard to prevent underflows, analogously to solidity, // otherwise we traverse the child nodes case 'BinaryOperation': { - const subExpressionConditions = [ - ...underflowGuardConditions(node.leftExpression, codeGeneratorState, seen), - ...underflowGuardConditions(node.rightExpression, codeGeneratorState, seen), - ]; + const leftExpressionConditions = underflowGuardConditions(node.leftExpression, codeGeneratorState, seen); + const rightExpressionConditions = underflowGuardConditions(node.rightExpression, codeGeneratorState, seen); + + if (node.operator === '&&') { + const leftExpression = removeTrailingSemicolon(codeGenerator(node.leftExpression, codeGeneratorState)); + return [ + ...leftExpressionConditions, + ...rightExpressionConditions.map(guard => `!(${leftExpression}) || (${guard})`), + ]; + } + if (node.operator === '||') { + const leftExpression = removeTrailingSemicolon(codeGenerator(node.leftExpression, codeGeneratorState)); + return [ + ...leftExpressionConditions, + ...rightExpressionConditions.map(guard => `(${leftExpression}) || (${guard})`), + ]; + } + + const subExpressionConditions = [...leftExpressionConditions, ...rightExpressionConditions]; if (node.operator !== '-') return subExpressionConditions; return [ ...subExpressionConditions, diff --git a/test/contracts/action-tests/Underflows.zol b/test/contracts/action-tests/Underflows.zol index ce895723c..951bf874f 100644 --- a/test/contracts/action-tests/Underflows.zol +++ b/test/contracts/action-tests/Underflows.zol @@ -30,6 +30,11 @@ contract MyContract { a = a - amount; } + function requireShortCircuitOr(secret uint256 amount, bool skip) public { + require(skip || a - amount >= 0, "skip or no underflow"); + a = a; + } + function unknownMappingDecSub(secret uint256 value, secret uint256 amount) public { unknown balances[msg.sender] -= value - amount; } From d011d87b717f9910add21f973e4329ac18b76a57 Mon Sep 17 00:00:00 2001 From: Lydia Garms Date: Tue, 14 Jul 2026 15:02:02 +0100 Subject: [PATCH 4/4] fix(checks): add an unsupported errors for internal function calls with parameters that are expressions --- doc/STATUS.md | 4 +- .../visitors/checks/internalCallVisitor.ts | 60 +++++++++++++------ 2 files changed, 44 insertions(+), 20 deletions(-) diff --git a/doc/STATUS.md b/doc/STATUS.md index 40e267251..a4506a2a4 100644 --- a/doc/STATUS.md +++ b/doc/STATUS.md @@ -19,7 +19,7 @@ Do note that `LoanSimple.zol` don't currently compile - we are actively working - Any combination of: - Any number of functions: - - Standalone functions can be compiled, along with internal function calls as long as secrecy is preserved (e.g. don't pass a secret parameter to a public function). + - Standalone functions can be compiled, along with internal function calls as long as secrecy is preserved (e.g. don't pass a secret parameter to a public function). Internal function calls currently only support arguments passed as identifiers, or as direct member accesses on struct values. - External function calls are supported, as long as secret states aren't involved. - Constructors are supported, but be aware that the output shield contract will contain a constructor combining the `.zol` constructor and some extra functionality. - Functions can have any number of secret or public parameters of the types below. @@ -62,6 +62,8 @@ Here we summarise the as of yet unsupported Solidity syntax. - These create a very complex commitment structure. This includes structs with properties of type `mapping`, dynamic or fixed-size `array` (e.g., `uint256[]`, `address[3]`), or other structs. We may work on this in future if there is high demand for this feature. - **Arrays of structs:** - Consider using mappings to structs, which are supported. +- **Internal calls with computed or special-expression arguments:** + - Internal function call arguments must currently be identifiers, such as `add(value)`, or direct member accesses on struct values, such as `add(value.amount)`. Expressions such as `add(a + b)`, `add(msg.sender)`, casts, and array or mapping index accesses are not supported. These patterns throw a `TODOError`: `TODO: zappify doesn't yet support this feature: Unsupported argument N in internal function call 'name'. Only identifiers and struct member accesses are currently supported.` - **While statements:** - These are unsupported in zero-knowledge proof circuits because they cannot handle dynamic loops. - **Assembly:** diff --git a/src/transformers/visitors/checks/internalCallVisitor.ts b/src/transformers/visitors/checks/internalCallVisitor.ts index 7140687be..95333ac1a 100644 --- a/src/transformers/visitors/checks/internalCallVisitor.ts +++ b/src/transformers/visitors/checks/internalCallVisitor.ts @@ -1,37 +1,59 @@ /* eslint-disable no-param-reassign, no-shadow, no-continue */ -import { TODOError, ZKPError } from '../../../error/errors.js'; +import { TODOError } from '../../../error/errors.js'; import NodePath from '../../../traverse/NodePath.js'; /** * @desc: * Throws an error if secret states are passed to an external function call. -*/ + */ export default { FunctionCall: { enter(path: NodePath) { const { node, scope } = path; const args = node.arguments; - let isSecretArray : string[]; - for (const arg of args) { - if (arg.nodeType !== 'Identifier' && !arg.expression?.typeDescriptions.typeIdentifier.includes('_struct')) continue; - isSecretArray = args.map(arg => scope.getReferencedBinding(arg)?.isSecret); - } + if ( + path.isInternalFunctionCall() && + node.expression.nodeType === 'Identifier' + ) { + for (const [index, arg] of args.entries()) { + if ( + arg.nodeType !== 'Identifier' && + !arg.expression?.typeDescriptions?.typeIdentifier?.includes( + '_struct', + ) + ) { + // If we support expressions, e.g. `a - amount`, we will need to ensure there are + // constraints in the circuits to prevent underflows/ overflows + throw new TODOError( + `Unsupported argument ${index + 1} in internal function call '${ + node.expression.name + }'. Only identifiers and struct member accesses are currently supported.`, + node, + ); + } + } - if(path.isInternalFunctionCall() && node.expression.nodeType === 'Identifier') { - const functionReferencedPath = scope.getReferencedPath(node.expression); - const params = functionReferencedPath.node.parameters.parameters; - params.forEach((param, index) => { - if(param.isSecret){ - if(isSecretArray[index] !== param.isSecret) - throw new Error('Make sure that passed parameters have same decorators'); - } - }); - const thisFunctionIndicator = path.scope.indicators; - thisFunctionIndicator.internalFunctionInteractsWithSecret ??= functionReferencedPath.scope.indicators.interactsWithSecret; - thisFunctionIndicator.internalFunctionModifiesSecretState ??= functionReferencedPath.scope.modifiesSecretState(); + const isSecretArray = args.map( + arg => scope.getReferencedBinding(arg)?.isSecret, + ); + const functionReferencedPath = scope.getReferencedPath(node.expression); + const params = functionReferencedPath.node.parameters.parameters; + params.forEach((param, index) => { + if (param.isSecret) { + if (isSecretArray[index] !== param.isSecret) + throw new Error( + 'Make sure that passed parameters have same decorators', + ); + } + }); + const thisFunctionIndicator = path.scope.indicators; + thisFunctionIndicator.internalFunctionInteractsWithSecret ??= + functionReferencedPath.scope.indicators.interactsWithSecret; + thisFunctionIndicator.internalFunctionModifiesSecretState ??= + functionReferencedPath.scope.modifiesSecretState(); } }, },