TritonVM / tasm-lib

A collection of functions written in Triton VM assembly (tasm)
Apache License 2.0
11 stars 2 forks source link

merge “safe” and “unsafe” lists #81

Closed jan-ferdinand closed 6 months ago

jan-ferdinand commented 7 months ago

The primary purpose of this PR is to unify the two list types “safe” and “unsafe”. Even though both list types existed, only “unsafe” lists were used in practice. To make these lists safe, each memory allocation request results in enough memory being assigned to the caller to make out-of-bounds access impossible in practice.[^safe]

There are two additional major changes:

  1. The dynamic memory allocator no longer accepts an argument. Its signature is now || -> address.
  2. A new memory convention.

The new memory convention is as follows[^mem]:

[^mem]: The convention is now also part of the documentation. It can be found in src/memory.rs. [^safe]: It is always possible to access arbitrary memory locations if one chooses to do so; Triton VM has no understanding of anything resembling memory allocation. [^static]: The current implementation does not enforce this explicitly. Instead, it is assumed that calling the dynamic allocator often enough to accidentally access the memory page for static allocations is impossible.

aszepieniec commented 7 months ago

:+1:

Sword-Smith commented 6 months ago

One open question: Do we want to verify that the memory offsets are of type u32? E.g. in the Get snippet, we have:

            // BEFORE: _ *list index
            // AFTER:  _ elem{{N - 1}}, elem{{N - 2}}, ..., elem{{0}}
            {entrypoint}:
                push 1
                add
                {&mul_with_size}
                // stack: _ *list (N * (index + 1))

               // <--- Here, we could insert `split swap 1 pop 1` or something like that to actually achieve memory safety.

                add
                // stack: _ (*list + N * index + 1)

                {&self.data_type.read_value_from_memory_pop_pointer()}
                // stack: _ elem{{N - 1}}, elem{{N - 2}}, ..., elem{{0}}

                return
jan-ferdinand commented 6 months ago

Do we want to verify that the memory offsets are of type u32?

Good idea. :+1: Do think split swap 1 pop 1 or split swap 1 push 0 eq assert?

Sword-Smith commented 6 months ago

Do we want to verify that the memory offsets are of type u32?

Good idea. 👍 Do think split swap 1 pop 1 or split swap 1 push 0 eq assert?

We can go with the 2nd option, the one containing an assert instruction. Then we can always hand-optimize later when needed.