Fixed-point arithmetic in the zkSNARK-based programming language LEO

Author: @zk_tutorials

Introduction

Blockchain-based systems are entering many parts of our lives, in industries such as DeFi or gaming. Many contemporary blockchains, however, lack privacy and scalability, limiting the range of use cases. Zero-knowledge proofs and blockchains enabled by zero-knowledge proofs, such as Aleo, promise to provide better scalability and privacy guarantees and enable novel blockchain applications. This includes novel DeFi applications, more complex web3 games, or even artificial intelligence-based programs. Many of these applications require representing a wide range of numbers, including fractional numbers. Aleo 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 to also 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:

let i: u32 = 155;

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 a decimal notation, we multiply by 250 in the fixed-point notation and then divide the result by the scaling factor 100. 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 similar 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

As shown in the above examples, the scaling factor defines the number of fractional part digits. We used a scaling factor of 10^n 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 2³²-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 2⁵=32, for example, 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 2²⁷-1=134,217,727 and the resolution of the fractional part is 1/2⁵=1/32. The fractional part can add a 31/32 to the maximum integer number, so the maximum representable value lies between 0 and 2²⁷-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/2⁵)/2=1/64=0.015625. Thus, a larger 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 that we can store, and the accuracy of numbers we represent.

Especially when multiplying or dividing, we may run into an overflow. For example, assume we have a scaling factor of 2⁵=32, and we want to multiply 2¹⁶=65536 times 2⁶=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 actually multiply 2²¹ with 2¹¹, before dividing with the scaling factor of 2⁵. By just looking at the instructions, we would thus expect a code output of 2²⁷.

However, when we look at the output, we get:

[registers]
r0: u32 = 0;

The temporary result of c * d is 2³², which is just out of the range of the u32 type. Thus, we actually got a number overflow, and get 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 2⁶⁴-1. This way, we get the expected result of 2²⁷:

[registers]
r0: u64 = 134217728;

Remember that we need to divide again by the scaling factor to interpret the fixed-point number result in normal terms: 2²⁷ / 2⁵ = 2²² which is the result of the above mentioned calculation of 2¹⁶ times 2⁶.

However, by using u64, the circuit size grew from 96 to 192 constraints, effectively doubling in size. This can lead to higher proving cost, especially in complex applications. Thus, an alternative would be to reduce the scaling factor, and thereby potentially reduce the number representation accuracy.

When using 2⁴ as a scaling factor instead of 2⁵ with only u32 types, we get the following output:

[registers]
r0: u32 = 67108864;

This output is 2²⁶. Again, divide it by the scaling factor of 2⁴, and we get the expected and correct output of 2²².

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 +- 2³¹-1 which translates to a range between -2147483648 to 2147483647.

Example code

Addition of two numbers a and b in fixed-point format:

function add(a: u32, b: u32) -> u32 {
let result: u32 = a + b;
return result;
}

Multiplication of two numbers a and b in fixed-point format:

function multiply(a: u32, b: u32, s: u32) -> u32 {
let result: u32 = a * b / s;
return result;
}

Division of two numbers a and b in fixed-point format:

function divide(a: u32, b: u32, s: u32) -> u32 {
let result: u32 = s * a / b;
return result;
}

You can find the entire Leo project code here.