Always use a normal segment for first SegmentArena segment

[notlesh]

(Note that this is basically a clone of Moonsong-Labs#45. We'd love to get this accepted upstream if possible.)

Problem: Starknet OS expects SegmentArena segments to all be temporary except the first segment, which must be normal. This is so that relocation rules for all segments can chain back into the first.

Solution: Use temporary segments only if it's not the first.

Description

The Starknet OS verifies the continuity of the segments in SegmentArenas here, which requires relocation rules to be properly set up.

The requirements for this to work are that each src_ptr is a temporary segment and each dest_ptr is a non-temporary segment (or a temporary segment with an existing rule mapping it to a non-temporary segment).

cairo-vm uses a number of hints to accomplish this, and these are injected by the sierra-to-casm compiler. However, it relies on one additional hint which is not injected anywhere in the case of SNOS.

This hint seems to ensure the same condition needed in SNOS: that the initial segment is a normal segment and that all other segments are temporary segments with relocation rules pointing back to the initial one. However, it creates the normal segment inside this last hint rather than when the SegmentArena is initialized.

SNOS handles this by simply allocating the initial segment as a normal one as explained here. This seems to alleviate the need to later recreate the segment in relocate_all_segments(), allowing the implementation to work in SNOS without the hint mentioned above.

Checklist

• Linked to Github Issue
• Unit tests added
• Integration tests added.
• This change requires new documentation.
  • Documentation has been added/updated.
  • CHANGELOG has been updated.

[pefontana]

Hi @notlesh
Thanks for the contribution!
There is just a minor error in the CI in the make check-fmt check
Also, would it be possible to add a small program or a little test for this fix?

[notlesh]

Hi @notlesh Thanks for the contribution! There is just a minor error in the CI in the make check-fmt check Also, would it be possible to add a small program or a little test for this fix?

I've wanted to produce a better way to test this, but it's complicated because the failure occurs in a different repo.

One idea for a test case is to show that the dictionaries do not have a temporary segment as their first segment prior to the RelocateAllDictionaries cheatcode being called -- this is fundamentally what was broken and what is fixed here.

This should act as a regression test (reproducing the problem and demonstrating that it's fixed) but it doesn't reproduce the exact error. Let me know what you think and if you want more details or want to know how you can reproduce the exact error yourself.

[pefontana]

This should act as a regression test (reproducing the problem and demonstrating that it's fixed) but it doesn't reproduce the exact error. Let me know what you think and if you want more details or want to know how you can reproduce the exact error yourself.

What do you mean by it doesn't reproduce the exact error? Can we add some Cairo program that plays with dictionaries triggering the error? O maybe just add some unit tests

Also, there are merge conflicts that need to let me approve the CI run, can you solve them?

[notlesh]

What do you mean by it doesn't reproduce the exact error? Can we add some Cairo program that plays with dictionaries triggering the error? O maybe just add some unit tests

Also, there are merge conflicts that need to let me approve the CI run, can you solve them?

Sorry for the long delay, I'd like to push this forward soon (resolve conflicts and add a test). In the meantime, I was wondering if you could point me to an example of the sort of test you have in mind, as I'm unsure of where to start with this.

[gabrielbosio]

Let me know what you think and if you want more details or want to know how you can reproduce the exact error yourself.

Hi, @notlesh! To test this, I think it would be helpful to know what's the code that's being problematic to see why is this scenario difficult to reproduce, because I'm not sure if there's a Cairo program that can be used for testing because the hint that calls new_default_dict already enforces the temporary segments to be all of the segments except the first one.
Once we have the code we can think of something smaller like a unit test.

[notlesh]

Let me know what you think and if you want more details or want to know how you can reproduce the exact error yourself.

Hi, @notlesh! To test this, I think it would be helpful to know what's the code that's being problematic to see why is this scenario difficult to reproduce, because I'm not sure if there's a Cairo program that can be used for testing because the hint that calls new_default_dict already enforces the temporary segments to be all of the segments except the first one. Once we have the code we can think of something smaller like a unit test.

Hey, @gabrielbosio , thanks for taking a look.

The code that is failing is the first link mentioned in the description, specifically the hint that calls memory.add_relocation_rule():

// Helper function for validate_segment_arena.
func _verify_continuity(infos: SegmentInfo*, n_segments_minus_one: felt) {
    if (n_segments_minus_one == 0) {
        // If there is only one segment left, there is no need to check anything.
        return ();
    }

    // Enforce an empty cell between two consecutive segments so that the start of a segment
    // is strictly bigger than the end of the previous segment.
    // This is required for proving the soundness of this construction, in the case where a segment
    // has length zero.

    // Note: the following code was copied from relocate_segment() for efficiency reasons.
    let src_ptr = infos[1].start;
    let dest_ptr = infos[0].end + 1;
    %{ memory.add_relocation_rule(src_ptr=ids.src_ptr, dest_ptr=ids.dest_ptr) %} // <--- FAILS HERE
    assert src_ptr = dest_ptr;

    return _verify_continuity(infos=&infos[1], n_segments_minus_one=n_segments_minus_one - 1);
}

This fails because src_ptr must be a temporary segment. cairo-vm currently does this, basically:

• Allocate everything as a temporary segment during execution
• At the end, in a hint injected by the Sierra-CASM compiler (IIRC), this is fixed by creating a single normal segment before processing all of the other segments

The current code works so long as this hint is called, but that's not possible in Cairo0 code -- which the OS is written in, hence the reason it doesn't work for SNOS.

This PR fixes this by ensuring that the required normal segment is allocated up front instead of fixed later on, which I think works for all cases.

Let me know if this is any clearer than it was, I know the problem is pretty detailed. I'd also be happy to jump on a call and walk through it with you. Thanks again!

[gabrielbosio]

This PR fixes this by ensuring that the required normal segment is allocated up front instead of fixed later on, which I think works for all cases.

To make sure that this works for all cases, I'm thinking of adding at least two tests:

• Check that this works for Cairo 0. This could be achieved by calling the validate_segment_arena without failing.

• Check that this works for Cairo 1. This could be achieved with a Cairo program that uses the alloc_felt_252_dict hint. For example, this program uses it:

  use dict::{felt252_dict_entry_finalize, Felt252DictTrait};
  
  fn main() -> (felt252, felt252) {
      let mut dict = felt252_dict_new::<felt252>();
      dict.insert(1, 64);
      let val = dict.get(1);
      dict.insert(1, 75);
      let val2 = dict.get(1);
      dict.squash();
      return (val, val2);
  }
  

  And then run this program and check the segments the hint creates are the same than
  main. I've run this program in both main and this branch and they produced the same segments. The segments created by the hint were the ones that had index >= 6 so I think you can compare those instead of the entire memory.

[gabrielbosio]

Also, there's an error from clippy