Valida C Compiler Toolchain

Update: May 5, 2024

We are excited to announce the alpha release of the Valida C Compiler Toolchain, designed to compile C programs to run on the Valida zk-VM. This package includes:

• Valida C Compiler: This compiler converts C programs to Valida-compatible code.

• Valida zk-VM: A virtual machine for executing and verifying Valida programs.

---

What You Can Do:

With this package, you can:

1. Compile C Programs: Convert your C code into Valida-compatible programs using the included C to Valida compiler.

2. Run and Verify Programs: Execute your programs on the Valida zk-VM and create succinct proofs of execution.

3. Test and Debug: Explore the capabilities and limitations of both the compiler and the VM in this alpha release.

---

Usage Instructions:

To compile, for example, the cat.c example, from within the decompressed release package directory:

./clang -c -target delendum ./examples/cat.c
./ld.lld --script=./valida.ld cat.o -o cat
./valida run cat log

Once running, the cat example will wait for input. After you are done providing input, press ctrl+D. The program should echo back what you wrote, writing its output to log.

Compiling and running the other examples follows the same procedure, substituting $NAME for the name of the example:

./clang -c -target delendum ./examples/${NAME}.c
./ld.lld --script=./valida.ld ${NAME}.o -o ${NAME}
./valida run ${NAME} log

There are three other examples not mentioned yet: reverse, checksum, and sha256. reverse will reverse the bytes of the input provided on the console and print out the reversed input. checksum will add up the bytes of the input and print out the least significant byte of the result. sha256 will compute the SHA-256 hash of the first 256 bytes of input and print out the resulting hash. Each of them will write their output to log or whichever file you specify on the command line.

---

Writing Your Own Programs:

To create your own programs in C:

• No libc Support: Use built-in functions __builtin_delendum_read_advice() (for getc(stdin)) and __builtin_delendum_write(x) (for putc(x, stdout)).

• Mind the Limitations: The compiler's current limitations necessitate workarounds, particularly for I/O, structures, and other unsupported features.

---

Benchmarks:

Here are some reports on benchmarks that we have run comparing the proving performance of Valida to RISC Zero, Jolt and SP1:

• May 2024: recursive and iterative Fibonacci, SHA-256

These benchmarks indicate that Valida is an industry leading competitor in terms of speed and efficiency of generating succinct knowledge proofs.

---

Important Caveats:

This software is in its alpha stage and has several limitations:

Compiler Limitations:

• No Floating Point: The compiler does not support floating-point operations.

• No 64-bit Integers: Types like long long and unsigned long long are unsupported.

• No libc Support: You must rely on built-in functions for I/O operations.

• Limited Inline Support: String and array literals cannot be used inline in function bodies.

• Struct Issues: Local variables of struct types may not always work properly.

• Varargs: The compiler does not support variable arguments.

zk-VM Limitations:

• Incomplete Proving System: Some constraints are still missing or incorrect, allowing some false statements to be proven, and preventing some true statements from being proven, pending resolution of these issues, which are actively being worked on.

• Arithmetic Overflows: The VM cannot handle executions involving arithmetic overflows. Support for arithmetic overflows is planned.

• No Zero Knowledge Proofs: The VM does not yet produce zero-knowledge proofs. Support for the zero knowledge property is planned.

---

Source repositories

Here are the source repositories used to generate the contents of this release bundle:

• The Valida C compiler: https://github.com/lita-xyz/llvm-valida/

• The Valida zk-VM: https://github.com/valida-xyz/valida

• Valida's fork of Plonky3: https://github.com/valida-xyz/Plonky3

• The provided example programs: https://github.com/lita-xyz/valida-c-examples/

---

Conclusion:

The Valida C Compiler Toolchain offers exciting possibilities for compiling and running C programs on the Valida zk-VM. While this alpha release has limitations, it provides a solid foundation for future developments. We encourage you to test the toolchain, provide feedback, and contribute to its evolution.

For more information or support, visit our website or contact our team directly.