Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Added segment arena cairo1 runner validation. #1721

Merged
merged 4 commits into from
Apr 24, 2024

Conversation

orizi
Copy link
Contributor

@orizi orizi commented Apr 17, 2024

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 orizi force-pushed the feat/segment-arena-cairo1-validation branch 2 times, most recently from 8aefb47 to 116e7cf Compare April 17, 2024 10:44
Copy link
Contributor

@fmoletta fmoletta left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

The cairo programs returning non-squashed dicts are mainly used to test output serialization, and correspond to issues raised by users of the crate. I would prefer to keep them like this to ensure that the same issues don't pop up in the future.
(Relevant issue)

@orizi
Copy link
Contributor Author

orizi commented Apr 17, 2024

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
Copy link
Contributor Author

orizi commented Apr 17, 2024

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.

@@ -356,97 +362,112 @@ fn create_entry_code(
// The builtins in the formatting expected by the runner.
let (builtins, builtin_offset) =
get_function_builtins(&signature.param_types, copy_to_output_builtin);
let mut ctx = casm! {};
let mut ctx = CasmBuilder::default();
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

@orizi Can you add some documentation here?
Specially in the casm_extend! cases?

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

do note this is exactly the same code as before - only where the code may somewhat be understandable by variable name.

add some additional doc.

cairo1-run/src/cairo_run.rs Show resolved Hide resolved
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Since this Dict return programs are still running without proof_mode, can we made some test for the old version of the cairo program that runs OK without proof_mode and fails when proof_mode?

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

it shouldn't work at any version - it is a legal cairo function - but not a sensible run.
even when not running in proof mode i would not expect to be able to run unprovable programs, unless these are actually a test.

Ok((ctx, builtins))
let result = ctx.build(["FUNCTION"]);
let [call_inst] = result.branches[0].1.as_slice() else {
panic!("Expected a single relocation");
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Can we avoid the panics here? If it is to much work just create an issue and we will handle it

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

this cannot ever actually panic - given that the builder code is correct (it will either always crash if we've written bad code here) or never crash (if the code here is fine - which it is)

@orizi orizi force-pushed the feat/segment-arena-cairo1-validation branch from 672d638 to 9699235 Compare April 17, 2024 21:45
@orizi orizi force-pushed the feat/segment-arena-cairo1-validation branch from 9699235 to a79d32f Compare April 18, 2024 15:27
@orizi orizi force-pushed the feat/segment-arena-cairo1-validation branch from d4c96d2 to dfe52bc Compare April 18, 2024 17:14
Copy link
Collaborator

@pefontana pefontana left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Great @orizi !
Thanks for the work!
We just tested proving some dict programs with these changes + the gas related ones + Stone Prover and work OK

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

4 participants