Pure model of MIP-8 storage-page encoding
This file contains the executable Coq model for
encode_storage_page and decode_storage_page from
storage_page.cpp. It is deliberately separate from
storage_page_specs.v: the C++ separation-logic specs should import these
definitions, but the format itself is just a pure byte-level contract.
The format is a page-local run-length encoding over the 128 storage slots:
The main theorem at the end is the canonical roundtrip property:
decoding the canonical encoder output recovers the page after applying the
same 32-byte normalization that the encoder performs. The corollary
decode_encode_storage_page_model gives raw page equality when every slot is
already canonical for that normalization.
- zero runs are represented by a small count byte;
- the byte 0 means "the rest of the 128-slot page is zero";
- nonzero runs are represented by 128 + run - 1 followed by compact RLP encodings of the run's bytes32 slots.
From Stdlib Require Import Bool List NArith ZArith Lia.
Import ListNotations.
Require Import monad.proofs.execproofs.mip8.commitment.
Compact bytes32 encoding drops leading zero bytes before applying the RLP
short-string encoding used in MIP 8. Bytes are represented as Z because
the generated C++ AST uses integer values for unsigned-char operations.
Definition word_byte (shift word : N) : Z :=
Z.of_N (N.land (N.shiftr word shift) 255).
Fixpoint be_bytes (len : nat) (word : N) : list Z :=
match len with
| O ⇒ []
| S len' ⇒
word_byte (8 × N.of_nat len') word :: be_bytes len' word
end.
Fixpoint drop_leading_zeroes (bytes : list Z) : list Z :=
match bytes with
| 0%Z :: rest ⇒ drop_leading_zeroes rest
| _ ⇒ bytes
end.
Definition compact_bytes32_payload (word : N) : list Z :=
drop_leading_zeroes (be_bytes 32 word).
Definition rlp_encode_short_string (payload : list Z) : list Z :=
match payload with
| [byte] ⇒
if (0 <=? byte)%Z && (byte <=? 127)%Z
then [byte]
else [(128 + Z.of_nat (length payload))%Z; byte]
| _ ⇒ (128 + Z.of_nat (length payload))%Z :: payload
end.
Definition encode_slot_model (slot : N) : list Z :=
rlp_encode_short_string (compact_bytes32_payload slot).
Fixpoint count_zero_prefix (limit : nat) (page : list N) : nat :=
match limit, page with
| O, _ ⇒ O
| S limit', slot :: rest ⇒
if N.eq_dec slot 0
then S (count_zero_prefix limit' rest)
else O
| _, [] ⇒ O
end.
Fixpoint count_nonzero_prefix (limit : nat) (page : list N) : nat :=
match limit, page with
| O, _ ⇒ O
| S limit', slot :: rest ⇒
if N.eq_dec slot 0
then O
else S (count_nonzero_prefix limit' rest)
| _, [] ⇒ O
end.
Fixpoint encode_storage_page_fuel
(fuel : nat) (page : list N) : list Z :=
match fuel, page with
| O, _ ⇒ []
| _, [] ⇒ []
| S fuel', slot :: _ ⇒
if N.eq_dec slot 0
then
let zeros := count_zero_prefix (S fuel') page in
if Nat.eqb zeros (length page)
then [0%Z]
else Z.of_nat zeros :: encode_storage_page_fuel fuel' (skipn zeros page)
else
let run := count_nonzero_prefix page_slot_count page in
(128 + Z.of_nat (run - 1))%Z
:: concat (map encode_slot_model (firstn run page))
++ encode_storage_page_fuel fuel' (skipn run page)
end.
Definition encode_storage_page_model (page : list N) : list Z :=
encode_storage_page_fuel (length page) page.
Fixpoint word_of_be_bytes_from (acc : N) (bytes : list Z) : N :=
match bytes with
| [] ⇒ acc
| byte :: rest ⇒
word_of_be_bytes_from (256 × acc + Z.to_N byte) rest
end.
Definition word_of_compact_payload (payload : list Z) : N :=
word_of_be_bytes_from 0 payload.
Z.of_N (N.land (N.shiftr word shift) 255).
Fixpoint be_bytes (len : nat) (word : N) : list Z :=
match len with
| O ⇒ []
| S len' ⇒
word_byte (8 × N.of_nat len') word :: be_bytes len' word
end.
Fixpoint drop_leading_zeroes (bytes : list Z) : list Z :=
match bytes with
| 0%Z :: rest ⇒ drop_leading_zeroes rest
| _ ⇒ bytes
end.
Definition compact_bytes32_payload (word : N) : list Z :=
drop_leading_zeroes (be_bytes 32 word).
Definition rlp_encode_short_string (payload : list Z) : list Z :=
match payload with
| [byte] ⇒
if (0 <=? byte)%Z && (byte <=? 127)%Z
then [byte]
else [(128 + Z.of_nat (length payload))%Z; byte]
| _ ⇒ (128 + Z.of_nat (length payload))%Z :: payload
end.
Definition encode_slot_model (slot : N) : list Z :=
rlp_encode_short_string (compact_bytes32_payload slot).
Fixpoint count_zero_prefix (limit : nat) (page : list N) : nat :=
match limit, page with
| O, _ ⇒ O
| S limit', slot :: rest ⇒
if N.eq_dec slot 0
then S (count_zero_prefix limit' rest)
else O
| _, [] ⇒ O
end.
Fixpoint count_nonzero_prefix (limit : nat) (page : list N) : nat :=
match limit, page with
| O, _ ⇒ O
| S limit', slot :: rest ⇒
if N.eq_dec slot 0
then O
else S (count_nonzero_prefix limit' rest)
| _, [] ⇒ O
end.
Fixpoint encode_storage_page_fuel
(fuel : nat) (page : list N) : list Z :=
match fuel, page with
| O, _ ⇒ []
| _, [] ⇒ []
| S fuel', slot :: _ ⇒
if N.eq_dec slot 0
then
let zeros := count_zero_prefix (S fuel') page in
if Nat.eqb zeros (length page)
then [0%Z]
else Z.of_nat zeros :: encode_storage_page_fuel fuel' (skipn zeros page)
else
let run := count_nonzero_prefix page_slot_count page in
(128 + Z.of_nat (run - 1))%Z
:: concat (map encode_slot_model (firstn run page))
++ encode_storage_page_fuel fuel' (skipn run page)
end.
Definition encode_storage_page_model (page : list N) : list Z :=
encode_storage_page_fuel (length page) page.
Fixpoint word_of_be_bytes_from (acc : N) (bytes : list Z) : N :=
match bytes with
| [] ⇒ acc
| byte :: rest ⇒
word_of_be_bytes_from (256 × acc + Z.to_N byte) rest
end.
Definition word_of_compact_payload (payload : list Z) : N :=
word_of_be_bytes_from 0 payload.
normalize_slot_model is the value-level effect of storing only the compact
32-byte encoding and reading it back. For ordinary bytes32 values this is
the identity; keeping it explicit makes the page roundtrip theorem true
without silently assuming every N is already below 2^256.
Definition normalize_slot_model (slot : N) : N :=
word_of_compact_payload (compact_bytes32_payload slot).
Definition normalize_storage_page_model (page : list N) : list N :=
map normalize_slot_model page.
Fixpoint rlp_decode_short_string
(encoded : list Z) : option (list Z × list Z) :=
match encoded with
| [] ⇒ None
| header :: rest ⇒
if (header <=? 127)%Z
then Some ([header], rest)
else if (128 <=? header)%Z && (header <=? 183)%Z
then
let len := Z.to_nat (header - 128)%Z in
if Nat.leb len (length rest)
then Some (firstn len rest, skipn len rest)
else None
else None
end.
Fixpoint decode_slot_run
(count : nat) (encoded : list Z) : option (list N × list Z) :=
match count with
| O ⇒ Some ([], encoded)
| S count' ⇒
match rlp_decode_short_string encoded with
| None ⇒ None
| Some (payload, after_slot) ⇒
match decode_slot_run count' after_slot with
| None ⇒ None
| Some (slots, rest) ⇒
Some (word_of_compact_payload payload :: slots, rest)
end
end
end.
Fixpoint decode_storage_page_fuel
(fuel slots_left : nat) (encoded : list Z) : option (list N) :=
match fuel with
| O ⇒ None
| S fuel' ⇒
if Nat.eqb slots_left O
then Some []
else
match encoded with
| [] ⇒ None
| header :: rest ⇒
if (header =? 0)%Z
then Some (repeat 0%N slots_left)
else if (header <? 128)%Z
then
let zeros := Z.to_nat header in
if Nat.leb zeros slots_left
then
match decode_storage_page_fuel
fuel' (slots_left - zeros) rest with
| None ⇒ None
| Some suffix ⇒ Some (repeat 0%N zeros ++ suffix)
end
else None
else
let run := S (Z.to_nat (header - 128)%Z) in
if Nat.leb run slots_left
then
match decode_slot_run run rest with
| None ⇒ None
| Some (slots, after_run) ⇒
match decode_storage_page_fuel
fuel' (slots_left - run) after_run with
| None ⇒ None
| Some suffix ⇒ Some (slots ++ suffix)
end
end
else None
end
end.
Definition decode_storage_page_model (bytes : list Z) : option (list N) :=
decode_storage_page_fuel
(S page_slot_count) page_slot_count bytes.
Lemma normalize_slot_model_zero :
normalize_slot_model 0 = 0%N.
Lemma be_bytes_length len word :
length (be_bytes len word) = len.
Lemma drop_leading_zeroes_length_le bytes :
length (drop_leading_zeroes bytes) ≤ length bytes.
Lemma compact_bytes32_payload_length word :
length (compact_bytes32_payload word) ≤ 32.
Lemma word_byte_range shift word :
(0 ≤ word_byte shift word ≤ 255)%Z.
Lemma be_bytes_range len word :
Forall (fun byte ⇒ (0 ≤ byte ≤ 255)%Z) (be_bytes len word).
Lemma drop_leading_zeroes_Forall (P : Z → Prop) bytes :
Forall P bytes →
Forall P (drop_leading_zeroes bytes).
Lemma compact_bytes32_payload_range word :
Forall (fun byte ⇒ (0 ≤ byte ≤ 255)%Z) (compact_bytes32_payload word).
Lemma rlp_decode_short_string_encode_app payload rest :
length payload ≤ 32 →
Forall (fun byte ⇒ (0 ≤ byte ≤ 255)%Z) payload →
rlp_decode_short_string (rlp_encode_short_string payload ++ rest) =
Some (payload, rest).
Lemma rlp_decode_encode_slot_app slot rest :
rlp_decode_short_string (encode_slot_model slot ++ rest) =
Some (compact_bytes32_payload slot, rest).
Lemma decode_slot_run_encode_app slots rest :
decode_slot_run (length slots)
(concat (map encode_slot_model slots) ++ rest) =
Some (normalize_storage_page_model slots, rest).
Lemma count_zero_prefix_le limit page :
count_zero_prefix limit page ≤ length page.
Lemma count_nonzero_prefix_le limit page :
count_nonzero_prefix limit page ≤ length page.
Lemma count_zero_prefix_pos limit rest :
count_zero_prefix (S limit) (0%N :: rest) > 0.
Lemma count_nonzero_prefix_pos limit slot rest :
slot ≠ 0%N →
count_nonzero_prefix (S limit) (slot :: rest) > 0.
Lemma count_zero_prefix_all_zero limit page :
count_zero_prefix limit page = length page →
normalize_storage_page_model page = repeat 0%N (length page).
Lemma normalize_storage_page_model_app lhs rhs :
normalize_storage_page_model (lhs ++ rhs) =
normalize_storage_page_model lhs ++ normalize_storage_page_model rhs.
Lemma normalize_storage_page_model_firstn_skipn n page :
normalize_storage_page_model page =
normalize_storage_page_model (firstn n page) ++
normalize_storage_page_model (skipn n page).
Lemma count_zero_prefix_firstn_normalized limit page :
normalize_storage_page_model
(firstn (count_zero_prefix limit page) page) =
repeat 0%N (count_zero_prefix limit page).
Lemma normalize_storage_page_model_zero_prefix_split limit page :
normalize_storage_page_model page =
repeat 0%N (count_zero_prefix limit page) ++
normalize_storage_page_model (skipn (count_zero_prefix limit page) page).
Lemma decode_encode_storage_page_fuel_normalized fuel page :
length page ≤ fuel →
length page ≤ page_slot_count →
decode_storage_page_fuel (S fuel) (length page)
(encode_storage_page_fuel fuel page) =
Some (normalize_storage_page_model page).
Theorem decode_encode_storage_page_model_normalized page :
length page = page_slot_count →
decode_storage_page_model (encode_storage_page_model page) =
Some (normalize_storage_page_model page).
Definition canonical_storage_page (page : list N) : Prop :=
normalize_storage_page_model page = page.
Corollary decode_encode_storage_page_model page :
length page = page_slot_count →
canonical_storage_page page →
decode_storage_page_model (encode_storage_page_model page) = Some page.
word_of_compact_payload (compact_bytes32_payload slot).
Definition normalize_storage_page_model (page : list N) : list N :=
map normalize_slot_model page.
Fixpoint rlp_decode_short_string
(encoded : list Z) : option (list Z × list Z) :=
match encoded with
| [] ⇒ None
| header :: rest ⇒
if (header <=? 127)%Z
then Some ([header], rest)
else if (128 <=? header)%Z && (header <=? 183)%Z
then
let len := Z.to_nat (header - 128)%Z in
if Nat.leb len (length rest)
then Some (firstn len rest, skipn len rest)
else None
else None
end.
Fixpoint decode_slot_run
(count : nat) (encoded : list Z) : option (list N × list Z) :=
match count with
| O ⇒ Some ([], encoded)
| S count' ⇒
match rlp_decode_short_string encoded with
| None ⇒ None
| Some (payload, after_slot) ⇒
match decode_slot_run count' after_slot with
| None ⇒ None
| Some (slots, rest) ⇒
Some (word_of_compact_payload payload :: slots, rest)
end
end
end.
Fixpoint decode_storage_page_fuel
(fuel slots_left : nat) (encoded : list Z) : option (list N) :=
match fuel with
| O ⇒ None
| S fuel' ⇒
if Nat.eqb slots_left O
then Some []
else
match encoded with
| [] ⇒ None
| header :: rest ⇒
if (header =? 0)%Z
then Some (repeat 0%N slots_left)
else if (header <? 128)%Z
then
let zeros := Z.to_nat header in
if Nat.leb zeros slots_left
then
match decode_storage_page_fuel
fuel' (slots_left - zeros) rest with
| None ⇒ None
| Some suffix ⇒ Some (repeat 0%N zeros ++ suffix)
end
else None
else
let run := S (Z.to_nat (header - 128)%Z) in
if Nat.leb run slots_left
then
match decode_slot_run run rest with
| None ⇒ None
| Some (slots, after_run) ⇒
match decode_storage_page_fuel
fuel' (slots_left - run) after_run with
| None ⇒ None
| Some suffix ⇒ Some (slots ++ suffix)
end
end
else None
end
end.
Definition decode_storage_page_model (bytes : list Z) : option (list N) :=
decode_storage_page_fuel
(S page_slot_count) page_slot_count bytes.
Lemma normalize_slot_model_zero :
normalize_slot_model 0 = 0%N.
Lemma be_bytes_length len word :
length (be_bytes len word) = len.
Lemma drop_leading_zeroes_length_le bytes :
length (drop_leading_zeroes bytes) ≤ length bytes.
Lemma compact_bytes32_payload_length word :
length (compact_bytes32_payload word) ≤ 32.
Lemma word_byte_range shift word :
(0 ≤ word_byte shift word ≤ 255)%Z.
Lemma be_bytes_range len word :
Forall (fun byte ⇒ (0 ≤ byte ≤ 255)%Z) (be_bytes len word).
Lemma drop_leading_zeroes_Forall (P : Z → Prop) bytes :
Forall P bytes →
Forall P (drop_leading_zeroes bytes).
Lemma compact_bytes32_payload_range word :
Forall (fun byte ⇒ (0 ≤ byte ≤ 255)%Z) (compact_bytes32_payload word).
Lemma rlp_decode_short_string_encode_app payload rest :
length payload ≤ 32 →
Forall (fun byte ⇒ (0 ≤ byte ≤ 255)%Z) payload →
rlp_decode_short_string (rlp_encode_short_string payload ++ rest) =
Some (payload, rest).
Lemma rlp_decode_encode_slot_app slot rest :
rlp_decode_short_string (encode_slot_model slot ++ rest) =
Some (compact_bytes32_payload slot, rest).
Lemma decode_slot_run_encode_app slots rest :
decode_slot_run (length slots)
(concat (map encode_slot_model slots) ++ rest) =
Some (normalize_storage_page_model slots, rest).
Lemma count_zero_prefix_le limit page :
count_zero_prefix limit page ≤ length page.
Lemma count_nonzero_prefix_le limit page :
count_nonzero_prefix limit page ≤ length page.
Lemma count_zero_prefix_pos limit rest :
count_zero_prefix (S limit) (0%N :: rest) > 0.
Lemma count_nonzero_prefix_pos limit slot rest :
slot ≠ 0%N →
count_nonzero_prefix (S limit) (slot :: rest) > 0.
Lemma count_zero_prefix_all_zero limit page :
count_zero_prefix limit page = length page →
normalize_storage_page_model page = repeat 0%N (length page).
Lemma normalize_storage_page_model_app lhs rhs :
normalize_storage_page_model (lhs ++ rhs) =
normalize_storage_page_model lhs ++ normalize_storage_page_model rhs.
Lemma normalize_storage_page_model_firstn_skipn n page :
normalize_storage_page_model page =
normalize_storage_page_model (firstn n page) ++
normalize_storage_page_model (skipn n page).
Lemma count_zero_prefix_firstn_normalized limit page :
normalize_storage_page_model
(firstn (count_zero_prefix limit page) page) =
repeat 0%N (count_zero_prefix limit page).
Lemma normalize_storage_page_model_zero_prefix_split limit page :
normalize_storage_page_model page =
repeat 0%N (count_zero_prefix limit page) ++
normalize_storage_page_model (skipn (count_zero_prefix limit page) page).
Lemma decode_encode_storage_page_fuel_normalized fuel page :
length page ≤ fuel →
length page ≤ page_slot_count →
decode_storage_page_fuel (S fuel) (length page)
(encode_storage_page_fuel fuel page) =
Some (normalize_storage_page_model page).
Theorem decode_encode_storage_page_model_normalized page :
length page = page_slot_count →
decode_storage_page_model (encode_storage_page_model page) =
Some (normalize_storage_page_model page).
Definition canonical_storage_page (page : list N) : Prop :=
normalize_storage_page_model page = page.
Corollary decode_encode_storage_page_model page :
length page = page_slot_count →
canonical_storage_page page →
decode_storage_page_model (encode_storage_page_model page) = Some page.
This page has been generated by coqdoc