Add proof that segment 0 starts at address 0

[franck44]

The way the segments are built implies that, if segment 0 exists, then its start address is zero.
And this is where we should start execution of the byte code.

To do

Add proof that this is always the case (provided there is a segment 0).
This can be used to remove some tests in the Driver.