Are you interested in learning how to make blockchain-based systems that guarantee privacy and scalability capable of complex tasks, such as machine learning? The programming language Leo simplifies the programming of ZKP-based programs but only supports integer-type-based numbers by default. This article analyzes the design of fixed-point numbers in zkSNARKS using Leo, which allows for computing using fractions for a wide range of applications. Learn how to represent fractional numbers and consider the trade-offs between the range of values that can be stored and the accuracy of the numbers represented. The knowledge is valuable for anyone building complex programs in zkSNARKs.
Introduction
Blockchain-based systems are emerging across many parts of our lives in industries such as DeFi or gaming. However, many contemporary blockchains need more privacy and scalability, limiting the range of use cases. Zero-knowledge proofs and blockchains enabled by zero-knowledge proofs, such as Provable, promise to provide better scalability and privacy guarantees and enable novel blockchain applications. This includes novel DeFi applications, more complex web3 games, or artificial intelligence-based programs. Many of these applications require representing various numbers, including fractional numbers. Provable comes with a programming language Leo that massively simplifies the programming of zero-knowledge-based programs. However, it only supports integer-type-based numbers. In this article, we analyze the design of fixed-point numbers in zkSNARKS using Leo, which allows us also to compute using fractions for a wide range of applications.
A simple implementation of fixed-point numbers
When implementing a fixed-point number notation, we can use the integer type provided by the Leo language for the variable. Additionally, we internally specify a scaling factor that defines the digits reserved for the integer part to the left of the decimal point of the value and also defines the fractional part to the right of the decimal point of the value. Suppose we want to represent the value 1.55 as a fixed point number with two digits of precision after the decimal point. To do so, we can introduce a variable i and assign 155, which is the value 1.55 multiplied by a scaling factor of 100:We can now perform math with this variable. For example, to add 0.45, we add 45 (.45*100) in the program code, which results in a variable value of 200. When interpreting the output of a program, we need to divide the value by the scaling factor of 100 to obtain the desired decimal-point notation - the addition result is 2 in the decimal-point notation.Similarly, we can also perform multiplications. When multiplying by 2.50 in decimal notation, we multiply by 250 in the fixed-point notation and then divide the result by the scaling factor of 100.
let i: u32 = 155;For example, 2*2.5=5 in decimal-point notation refers to 200*250/100=500 in fixed-point notation. Again, when interpreting the result outside of the fixed-point notation, we need to divide the fixed-point number 500 by the scaling factor 100 to obtain the expected result of 5.For divisions, we proceed similarly to multiplications but multiply by the scaling factor instead of dividing.For example, 4.5/0.5 = 9 in decimal-point notation refers to 100*450/50 = 900 in fixed-point notation. Divided by the scaling factor, we obtain the expected result of 9.
Generalization and things to consider
The above examples show that the scaling factor defines the number of fractional part digits. We used a scaling factor of 10n for n fractional digits. Generally, a higher scaling factor allows for more precision; however, we need to keep in mind the valid value range for the type.In the above example of using u32, the general range is between 0 and 232-1=4,294,967,295. Due to the binary nature of the types, a common notion is to use scaling factors S of powers of two. When using a scaling factor of 25=32, 5 bits are used for the fractional part, and only 27 bits remain for the integer part. Thus, the maximum number for the integer part is 227-1=134,217,727, and the resolution of the fractional part is 1/25=1/32. The fractional part can add a 31/32 to the maximum integer number, so the maximum representable value lies between 0 and 227-1+31/32=134,217,727.969.At the same time, the maximum representation error is computed as (1/S)/2, so in this example, it is (1/25)/2=1/64=0.015625. Thus, a more extensive scaling factor enables us to have more accurate fractional number representations but reduces the size of the integer part and, thus, the representable value range.As we can see, there is a trade-off between the range of values we can store and the accuracy of the numbers we represent.Especially when multiplying or dividing, we may run into an overflow. For example, assume we have a scaling factor of 25=32, and we want to multiply 216=65536 times 26=64. The code below attempts this.
function main() -> u32 {
let s: u32 = 32;
let a: u32 = 65536 * s;
let b: u32 = 64 * s;
let result: u32 = a * b / s;
return result;
}For the fixed point notation, we have to multiply both numbers by the scaling factor and multiply 221 with 211 before dividing with the scaling factor of 25. By just looking at the instructions, we would thus expect a code output of 227.However, when we look at the output, we get the following:The temporary result of c * d is 232, which is just out of the range of the u32 type. Thus, we got a number overflow and got the wrong result.So what can we do about this? We could use the u64 type instead of the u32 type for all types (variables and output), which can store numbers up to 264-1. This way, we get the expected result of 227:Remember that we need to divide again by the scaling factor to interpret the fixed-point number result in normal terms: 227 / 25 = 222, which is the result of the above-mentioned calculation of 216 times 26.However, by using u64, the circuit size grew from 96 to 192 constraints, effectively doubling in size. This can lead to higher proving costs, especially in complex applications. Thus, an alternative would be to reduce the scaling factor and thereby potentially reduce the number representation accuracy.When using 24 as a scaling factor instead of 25 with only u32 types, we get the following output:This output is 226. Again, divide it by the scaling factor of 24, and we get the expected and correct output of 222.The code generally also works for negative numbers. However, we need to use signed integer types. Take into account that the sign needs an additional bit, so for i32, the range of the integer part computes as +- 231-1, which translates to a range between -2147483648 to 2147483647.
Example code
Addition of two numbers, a and b, in the fixed-point format:Multiplication of two numbers, a and b, in the fixed-point format:Division of two numbers, a and b, in the fixed-point format:You can find the entire Leo project code on this GitHub page.