lambdaclass / cairo-vm

cairo-vm is a Rust implementation of the Cairo VM. Cairo (CPU Algebraic Intermediate Representation) is a programming language for writing provable programs, where one party can prove to another that a certain computation was executed correctly without the need for this party to re-execute the same program.

https://lambdaclass.github.io/cairo-vm

Apache License 2.0

485 stars 133 forks source link

Added segment arena cairo1 runner validation. #1721

Closed orizi closed 2 months ago

orizi commented 2 months ago

Added Cairo1 run minibootloader for segment arena validation.

Description

Using the cairo1 repo casm builder for easier CASM writing for writing the validation. Added finalization of dicts in cairo1 hint processor. Used both to add the validation in the runner. Updated the tests - as some of the tests returned a Dictionary from main - which isn't sound for proving code (as no squash occured).

Checklist

[V] This change requires new documentation.
- [V] CHANGELOG has been updated.

orizi commented 2 months ago

The serialization of such dictionaries should not be supported - it is never a valid run. If you want these as tests - the tests should make sure you fail.

orizi commented 2 months ago

Specifically - the related issue should have the same effect for checking on SquashedDict - i simply add that a regular Dict should never be returned - as it didn't pass a squash - and therefore not provable.