From Stdlib Require Import List NArith ZArith Lia.
Import ListNotations.
Require Import skylabs.auto.cpp.proof.
Require Import skylabs.lang.cpp.cpp.
Require Import monad.asts.storage_page_cpp.
Require Import monad.proofs.exec_specs.
Require Import monad.proofs.libspecs.byte_string_specs.
Require Import monad.proofs.libspecs.evmc_specs.
Require Import monad.proofs.libspecs.rlp_specs.
Require Import monad.proofs.libspecs.stdlib_specs.
Require Import monad.proofs.libspecs.u256_specs.
Require monad.proofs.libspecs.blake3.model.
Require Import monad.proofs.execproofs.mip8.blake3model.
Require Import monad.proofs.execproofs.mip8.blake3specs.
Require Import monad.proofs.execproofs.mip8.commitment.
Require Import monad.proofs.execproofs.mip8.commitment_balanced.
Require Import monad.proofs.execproofs.mip8.storage_page_encoding.
Import cQp_compat.
#[local] Open Scope N_scope.
The storage-page proof layer uses N for bytes32 words because
bytes32R is already phrased that way. The commitment model itself works
over optional concrete slot_word values. These definitions are the
page-local bridge between those two views.
Definition page_slot_value_model (word : N) : option slot_word :=
if N.eq_dec word 0 then None else Some (bytes32_of_N word).
Fixpoint page_slots_model (page : list N) : slot_values :=
match page with
| [] ⇒ []
| slot :: rest ⇒ page_slot_value_model slot :: page_slots_model rest
end.
Section with_Sigma.
Context `{Sigma : cpp_logic} {CU : genv} {hh : HasOwn mpredI fracR}.
Definition bytes32_ty : type := "evmc::bytes32"%cpp_type.
Definition storage_page_ty : type := "monad::storage_page_t"%cpp_type.
Definition byte_string_view_ty : type :=
Tnamed
(Ninst
(Nscoped (Nglobal (Nid "std")) (Nid "basic_string_view"))
[Atype Tuchar;
Atype
(Tnamed
(Ninst
(Nscoped (Nglobal (Nid "evmc")) (Nid "byte_traits"))
[Atype Tuchar]))]).
Definition result_storage_page_ty : type :=
Tnamed
(Ninst
(Nscoped
(Nscoped (Nglobal (Nid "boost")) (Nid "outcome_v2"))
(Nid "basic_result"))
[Atype storage_page_ty;
Atype
(Tnamed
(Ninst
(Nscoped (Nglobal (Nid "system_error2"))
(Nid "errored_status_code"))
[Atype
(Tnamed
(Ninst
(Nscoped
(Nscoped (Nglobal (Nid "system_error2"))
(Nid "detail"))
(Nid "erased"))
[Atype "long"%cpp_type]))]));
Atype
(Tnamed
(Ninst
(Nscoped
(Nscoped
(Nscoped
(Nscoped (Nglobal (Nid "boost"))
(Nid "outcome_v2"))
(Nid "experimental"))
(Nid "policy"))
(Nid "status_code_throw"))
[Atype storage_page_ty;
Atype
(Tnamed
(Ninst
(Nscoped (Nglobal (Nid "system_error2"))
(Nid "errored_status_code"))
[Atype
(Tnamed
(Ninst
(Nscoped
(Nscoped
(Nglobal (Nid "system_error2"))
(Nid "detail"))
(Nid "erased"))
[Atype "long"%cpp_type]))]));
Atype "void"%cpp_type]))]).
Definition storage_page_is_empty_lambda_name : name :=
"monad::storage_page_t::is_empty() const::@0"%cpp_name.
Definition compute_page_key_name : name :=
Nscoped (Nglobal (Nid "monad"))
(Nfunction function_qualifiers.N "compute_page_key"
[Tref (Qconst bytes32_ty)]).
Definition compute_slot_offset_name : name :=
Nscoped (Nglobal (Nid "monad"))
(Nfunction function_qualifiers.N "compute_slot_offset"
[Tref (Qconst bytes32_ty)]).
Definition compute_slot_key_name : name :=
Nscoped (Nglobal (Nid "monad"))
(Nfunction function_qualifiers.N "compute_slot_key"
[Tref (Qconst bytes32_ty); Tuchar]).
Definition page_commit_name : name :=
Nscoped (Nglobal (Nid "monad"))
(Nfunction function_qualifiers.N "page_commit"
[Tref (Qconst storage_page_ty)]).
Definition page_commit_balanced_name : name :=
Nscoped (Nglobal (Nid "monad"))
(Nfunction function_qualifiers.N "page_commit_balanced"
[Tref (Qconst storage_page_ty)]).
Definition encode_storage_page_name : name :=
Nscoped (Nglobal (Nid "monad"))
(Nfunction function_qualifiers.N "encode_storage_page"
[Tref (Qconst storage_page_ty)]).
Definition decode_storage_page_name : name :=
Nscoped (Nglobal (Nid "monad"))
(Nfunction function_qualifiers.N "decode_storage_page"
[byte_string_view_ty]).
Definition storage_page_slots : offset :=
_field "monad::storage_page_t::slots".
Definition scratch_array_ty : type :=
Tarray bytes32_ty 64%N.
Definition scratch_arg_ty : type :=
Tdecay_type scratch_array_ty (Tptr bytes32_ty).
Definition merge_index_array_ty : type :=
Tarray Tuchar 32%N.
Definition merge_index_arg_ty : type :=
Tptr Tuchar.
Definition merge_const_index_array_ty : type :=
Tarray (Qconst Tuchar) 32%N.
Definition merge_const_index_arg_ty : type :=
Tptr (Qconst Tuchar).
Definition merge_block_row_ty : type :=
Tarray Tuchar 64%N.
Definition merge_blocks_array_ty : type :=
Tarray merge_block_row_ty 32%N.
Definition merge_blocks_arg_ty : type :=
Tptr merge_block_row_ty.
Definition merge_input_ptr_ty : type :=
Tptr Tuchar.
Definition merge_inputs_array_ty : type :=
Tarray merge_input_ptr_ty 32%N.
Definition merge_inputs_arg_ty : type :=
Tptr merge_input_ptr_ty.
Definition merge_const_inputs_arg_ty : type :=
Tptr (Qconst merge_input_ptr_ty).
Definition merge_output_array_ty : type :=
Tarray bytes32_ty 32%N.
Definition merge_output_arg_ty : type :=
Tptr bytes32_ty.
Definition merge_const_output_array_ty : type :=
Tarray (Qconst bytes32_ty) 32%N.
Definition merge_const_output_arg_ty : type :=
Tptr (Qconst bytes32_ty).
Definition init_leaf_scratch_name : name :=
Nscoped (Nscoped (Nglobal (Nid "monad")) Nanonymous)
(Nfunction function_qualifiers.N "init_leaf_scratch"
[Tref (Qconst storage_page_ty); Qconst Tulong; scratch_arg_ty]).
Definition merge_scratch_level_name : name :=
Nscoped (Nscoped (Nglobal (Nid "monad")) Nanonymous)
(Nfunction function_qualifiers.N "merge_scratch_level"
[Qconst Tuchar; Tulong; scratch_arg_ty]).
Definition init_balanced_leaf_scratch_name : name :=
Nscoped (Nscoped (Nglobal (Nid "monad")) Nanonymous)
(Nfunction function_qualifiers.N "init_balanced_leaf_scratch"
[Tref (Qconst storage_page_ty); Qconst Tulong; scratch_arg_ty]).
Definition merge_balanced_range_name : name :=
Nscoped (Nscoped (Nglobal (Nid "monad")) Nanonymous)
(Nfunction function_qualifiers.N "merge_balanced_range"
[scratch_arg_ty; Qconst Tulong; Qconst Tulong]).
Definition compute_nonempty_subtree_root_name : name :=
Nscoped (Nscoped (Nglobal (Nid "monad")) Nanonymous)
(Nfunction function_qualifiers.N "compute_nonempty_subtree_root"
[Tref (Qconst storage_page_ty); Qconst Tulong]).
Definition storage_SLOTS_name : name :=
Nscoped (Nscoped (Nglobal (Nid "monad")) (Nid "storage_page_t"))
(Nid "SLOTS").
Definition storage_SLOT_SIZE_name : name :=
Nscoped (Nscoped (Nglobal (Nid "monad")) (Nid "storage_page_t"))
(Nid "SLOT_SIZE").
Definition storage_NUM_PAIRS_name : name :=
Nscoped (Nscoped (Nglobal (Nid "monad")) Nanonymous)
(Nid "NUM_PAIRS").
Definition StoragePageR (q : Qp) (page : list N) : Rep :=
storage_page_slots
|-> arrayR bytes32_ty (bytes32R q) page
** structR "monad::storage_page_t" q
** [| length page = page_slot_count |].
Definition storage_page_update_slot
(offset : nat) (value : N) (page : list N) : list N :=
firstn offset page ++ value :: skipn (S offset) page.
Transparent bytes32R evmc_bytes32_wordR.
#[global] Instance StoragePageR_cfrac :
CFracSplittable_1 StoragePageR.
Definition ScratchR (q : Qp) (scratch : list N) : Rep :=
arrayR bytes32_ty (bytes32R q) scratch
** [| length scratch = page_pair_count |].
Definition DecodeStoragePageResultR
(_q : Qp) (_result : option (list N)) : Rep := validR.
Definition page_index_model (key : N) : N :=
N.shiftr key 7.
Definition slot_offset_model (key : N) : N :=
N.land key 127.
Definition slot_key_model (page_key slot_offset : N) : N :=
N.lor
(N.modulo (N.shiftl page_key 7) (2 ^ 256))
(N.land slot_offset 127).
Lemma slot_offset_low_byte key :
N.land (N.land key 255) 127 = slot_offset_model key.
Lemma slot_offset_mask_small offset :
(0 ≤ offset < 128)%Z →
N.land (Z.to_N offset) 127 = Z.to_N offset.
Fixpoint slot_bitmap_from (index : nat) (page : list N) : N :=
match page with
| [] ⇒ 0
| slot :: rest ⇒
(if N.eq_dec slot 0 then 0 else 2 ^ N.of_nat index)
+ slot_bitmap_from (S index) rest
end.
Definition slot_bitmap_word (page : list N) : N :=
slot_bitmap_from 0 page.
Definition pair_slot_mask (pair_index : nat) : N :=
3 × 2 ^ (2 × N.of_nat pair_index).
Definition pair_bit_mask (pair_index : nat) : N :=
2 ^ N.of_nat pair_index.
Fixpoint pair_bitmap_prefix (fuel : nat) (slot_bitmap : N) : N :=
match fuel with
| O ⇒ 0
| S fuel' ⇒
let prefix := pair_bitmap_prefix fuel' slot_bitmap in
if N.eqb (N.land slot_bitmap (pair_slot_mask fuel')) 0
then prefix
else N.lor prefix (pair_bit_mask fuel')
end.
Fixpoint pair_bitmap_from
(fuel : nat) (slot_bitmap pair_index : N) : N :=
match fuel with
| O ⇒ 0
| S fuel' ⇒
let lo := 2 ^ (2 × pair_index) in
let hi := 2 ^ (2 × pair_index + 1) in
(if N.eqb (N.land slot_bitmap (N.lor lo hi)) 0
then 0
else 2 ^ pair_index)
+ pair_bitmap_from fuel' slot_bitmap (N.succ pair_index)
end.
Definition pair_bitmap_word (slot_bitmap : N) : N :=
pair_bitmap_prefix page_pair_count slot_bitmap.
Lemma pair_bitmap_prefix_64_pair_bitmap_word slot_bitmap :
pair_bitmap_prefix 64 slot_bitmap = pair_bitmap_word slot_bitmap.
Opaque pair_bitmap_word.
Definition storage_page_empty (page : list N) : bool :=
forallb (N.eqb 0) page.
Definition bitmap_word_bit (bm : N) (index : nat) : bool :=
negb (N.eqb (N.land bm (2 ^ N.of_nat index)) 0).
Definition page_pair_leaf_model
(page : list N) (pair_index : nat) : pair_leaf :=
(bytes32_of_N (nth (2 × pair_index) page 0),
bytes32_of_N (nth (2 × pair_index + 1) page 0)).
Definition init_leaf_scratch_model
(page : list N) (pair_bitmap : N) (old_scratch : list N) : list N :=
map
(fun pair_index ⇒
if bitmap_word_bit pair_bitmap pair_index
then
bytes32_to_N
(H64 leaf_mode (page_pair_leaf_model page pair_index))
else nth pair_index old_scratch 0)
(seq 0 page_pair_count).
Definition bitmap_clear_lowbit (word : N) : N :=
N.land word (word - 1).
Fixpoint bitmap_indices_from (fuel : nat) (word : N) : list nat :=
match fuel with
| O ⇒ []
| S fuel' ⇒
if N.eqb word 0
then []
else
let idx := N.to_nat (countr_zero64 word) in
idx :: bitmap_indices_from fuel' (bitmap_clear_lowbit word)
end.
Definition bitmap_indices (word : N) : list nat :=
bitmap_indices_from page_pair_count word.
Definition balanced_leaf_hashes
(page : list N) (pair_bitmap : N) : list N :=
blake3_hash_many_outputs
leaf_mode (map (page_pair_leaf_model page) (bitmap_indices pair_bitmap)).
Definition init_balanced_leaf_scratch_model
(page : list N) (pair_bitmap : N) (old_scratch : list N) : list N :=
balanced_leaf_hashes page pair_bitmap ++
drop (length (bitmap_indices pair_bitmap)) old_scratch.
Definition merge_pair_hash (lhs rhs : N) : N :=
bytes32_to_N
(H64 merge_mode (bytes32_of_N lhs, bytes32_of_N rhs)).
Definition merge_balanced_range_step
(scratch : list N) (begin mid : nat) : list N :=
match scratch !! begin, scratch !! mid with
| Some lhs, Some rhs ⇒
<[ begin := merge_pair_hash lhs rhs ]> scratch
| _, _ ⇒ scratch
end.
Fixpoint merge_balanced_range_model_fuel
(fuel : nat) (scratch : list N) (begin end_ : nat) : list N :=
match fuel with
| O ⇒ scratch
| S fuel' ⇒
let count := Nat.sub end_ begin in
if Nat.leb count 1
then scratch
else
let mid := Nat.add begin (Nat.div2 count) in
let scratch_l :=
merge_balanced_range_model_fuel fuel' scratch begin mid in
let scratch_r :=
merge_balanced_range_model_fuel fuel' scratch_l mid end_ in
merge_balanced_range_step scratch_r begin mid
end.
Definition merge_balanced_range_model
(scratch : list N) (begin end_ : nat) : list N :=
merge_balanced_range_model_fuel (Nat.sub end_ begin) scratch begin end_.
Fixpoint balanced_tree_from_digests_fuel
(fuel : nat) (digests : list digest) : option digest :=
match fuel with
| O ⇒
match digests with
| [digest] ⇒ Some digest
| _ ⇒ None
end
| S fuel' ⇒
match digests with
| [] ⇒ None
| [digest] ⇒ Some digest
| _ ⇒
let split := Nat.div2 (length digests) in
match
balanced_tree_from_digests_fuel fuel' (firstn split digests),
balanced_tree_from_digests_fuel fuel' (skipn split digests)
with
| Some lhs, Some rhs ⇒ Some (H64 merge_mode (lhs, rhs))
| _, _ ⇒ None
end
end
end.
Definition balanced_tree_from_digests (digests : list digest) :
option digest :=
balanced_tree_from_digests_fuel (length digests) digests.
Definition page_subtree_root_model (page : list N) : digest :=
match value_tree_from_slots (page_slots_model page) with
| Some tree ⇒ eval_tree tree
| None ⇒ bytes32_of_N 0
end.
Definition balanced_page_subtree_root_model (page : list N) : digest :=
match balanced_located_tree_from_slots (page_slots_model page) with
| Some tree ⇒ eval_located_tree tree
| None ⇒ bytes32_of_N 0
end.
Definition live_nodes_bitmap_word (nodes : list live_node) : N :=
fold_left
(fun bm node ⇒ N.lor bm (2 ^ N.of_nat node.(live_index)))
nodes 0.
Fixpoint live_nodes_well_formed_from
(lower : nat) (nodes : list live_node) : Prop :=
match nodes with
| [] ⇒ True
| node :: rest ⇒
(lower ≤ node.(live_index) < page_pair_count)%nat ∧
live_nodes_well_formed_from (S node.(live_index)) rest
end.
Definition live_nodes_well_formed (nodes : list live_node) : Prop :=
live_nodes_well_formed_from 0 nodes.
Lemma live_nodes_well_formed_from_weaken lower lower' nodes :
(lower' ≤ lower)%nat →
live_nodes_well_formed_from lower nodes →
live_nodes_well_formed_from lower' nodes.
Lemma merge_level_preserves_well_formed_from bit lower nodes :
live_nodes_well_formed_from lower nodes →
live_nodes_well_formed_from lower (merge_level bit nodes).
Lemma merge_level_preserves_well_formed bit nodes :
live_nodes_well_formed nodes →
live_nodes_well_formed (merge_level bit nodes).
Definition scratch_represents_live_nodes
(scratch : list N) (nodes : list live_node) : Prop :=
length scratch = page_pair_count ∧
∀ node,
In node nodes →
nth node.(live_index) scratch 0 =
bytes32_to_N (eval_tree node.(live_tree)).
Record merge_job : Type := {
merge_left : live_node;
merge_right : live_node;
}.
Definition merge_job_node (job : merge_job) : live_node :=
{|
live_index := job.(merge_left).(live_index);
live_tree :=
TreeNode
job.(merge_left).(live_tree)
job.(merge_right).(live_tree);
|}.
Definition merge_job_input (job : merge_job) : bytes64 :=
(eval_tree job.(merge_left).(live_tree),
eval_tree job.(merge_right).(live_tree)).
Definition merge_job_output (job : merge_job) : N :=
bytes32_to_N (H64 merge_mode (merge_job_input job)).
Definition merge_job_left_index (job : merge_job) : nat :=
job.(merge_left).(live_index).
Definition merge_job_right_index (job : merge_job) : nat :=
job.(merge_right).(live_index).
Record merge_scan_state : Type := {
scan_pending : option live_node;
scan_jobs : list merge_job;
}.
Definition initial_merge_scan_state : merge_scan_state :=
{| scan_pending := None; scan_jobs := [] |}.
Definition scan_one_node
(bit : nat) (state : merge_scan_state) (node : live_node)
: merge_scan_state :=
match state.(scan_pending) with
| None ⇒
{|
scan_pending := Some node;
scan_jobs := state.(scan_jobs);
|}
| Some previous ⇒
if sibling_candidate bit previous.(live_index) node.(live_index)
then
{|
scan_pending := None;
scan_jobs :=
state.(scan_jobs) ++
[{| merge_left := previous; merge_right := node |}];
|}
else
{|
scan_pending := Some node;
scan_jobs := state.(scan_jobs);
|}
end.
Fixpoint scan_nodes_from
(bit : nat) (state : merge_scan_state) (nodes : list live_node)
: merge_scan_state :=
match nodes with
| [] ⇒ state
| node :: rest ⇒
scan_nodes_from bit (scan_one_node bit state node) rest
end.
Definition scan_nodes (bit : nat) (nodes : list live_node)
: merge_scan_state :=
scan_nodes_from bit initial_merge_scan_state nodes.
Definition merge_jobs (bit : nat) (nodes : list live_node)
: list merge_job :=
(scan_nodes bit nodes).(scan_jobs).
Local Open Scope nat_scope.
Definition merge_scan_pending_count
(state : merge_scan_state) : nat :=
match state.(scan_pending) with
| Some _ ⇒ 1
| None ⇒ 0
end.
Lemma scan_one_node_jobs_bound bit state node :
2 × length (scan_one_node bit state node).(scan_jobs) +
merge_scan_pending_count (scan_one_node bit state node) ≤
2 × length state.(scan_jobs) +
merge_scan_pending_count state + 1.
Lemma scan_nodes_from_jobs_bound bit nodes state :
2 × length (scan_nodes_from bit state nodes).(scan_jobs) +
merge_scan_pending_count (scan_nodes_from bit state nodes) ≤
2 × length state.(scan_jobs) +
merge_scan_pending_count state + length nodes.
Lemma merge_jobs_two_for_one bit nodes :
2 × length (merge_jobs bit nodes) ≤ length nodes.
Lemma live_nodes_well_formed_from_length lower nodes :
live_nodes_well_formed_from lower nodes →
(lower ≤ page_pair_count)%nat →
(length nodes + lower ≤ page_pair_count)%nat.
Lemma live_nodes_well_formed_length nodes :
live_nodes_well_formed nodes →
(length nodes ≤ page_pair_count)%nat.
Lemma merge_jobs_length_le_32 bit nodes :
live_nodes_well_formed nodes →
(length (merge_jobs bit nodes) ≤ 32)%nat.
Local Close Scope nat_scope.
Definition apply_merge_job_to_scratch
(scratch : list N) (job : merge_job) : list N :=
<[ job.(merge_left).(live_index) := merge_job_output job ]> scratch.
Definition apply_merge_job_to_bitmap (bm : N) (job : merge_job) : N :=
N.clearbit bm (N.of_nat job.(merge_right).(live_index)).
Fixpoint apply_merge_jobs_to_scratch
(scratch : list N) (jobs : list merge_job) : list N :=
match jobs with
| [] ⇒ scratch
| job :: rest ⇒
apply_merge_jobs_to_scratch
(apply_merge_job_to_scratch scratch job) rest
end.
Fixpoint apply_merge_jobs_to_bitmap (bm : N) (jobs : list merge_job) : N :=
match jobs with
| [] ⇒ bm
| job :: rest ⇒
apply_merge_jobs_to_bitmap
(apply_merge_job_to_bitmap bm job) rest
end.
Definition merge_hash_outputs
(jobs : list merge_job) (old_outputs : list N) : list N :=
blake3_hash_many_outputs merge_mode (map merge_job_input jobs) ++
skipn (length jobs) old_outputs.
Inductive merge_block_row : Type :=
| MergeBlockUninit
| MergeBlockLeft : digest → merge_block_row
| MergeBlockFull : bytes64 → merge_block_row.
Definition merge_block_rowR (row : merge_block_row) : Rep :=
match row with
| MergeBlockUninit ⇒
arrayLR Tuchar 0 64
(fun _ : unit ⇒ anyR Tuchar 1$m)
(replicateN 64 ())
| MergeBlockLeft lhs ⇒
arrayLR Tuchar 0 32
(fun byte : val ⇒ primR Tuchar 1$m byte)
(blake3specs.bytes32_byte_values lhs)
** arrayLR Tuchar 32 64
(fun _ : unit ⇒ uninitR Tuchar 1$m)
(replicateN 32 ())
| MergeBlockFull block ⇒
blake3specs.Blake3BlockR 1 block
end.
Definition merge_block_rows (jobs : list merge_job)
: list merge_block_row :=
map (fun job ⇒ MergeBlockFull (merge_job_input job)) jobs ++
replicateN
(Z.to_N (32 - Z.of_nat (length jobs))) MergeBlockUninit.
Definition merge_index_arrayR (indexes : list nat) : Rep :=
as_Rep
(fun base ⇒
match indexes with
| [] ⇒
base |-> arrayLR Tuchar 0 32
(fun _ : unit ⇒ anyR Tuchar 1$m)
(replicateN 32 ())
| _ :: _ ⇒
base |-> arrayLR Tuchar 0 (Z.of_nat (length indexes))
(fun index : nat ⇒ ucharR 1$m (Z.of_nat index)) indexes
** base |-> arrayLR Tuchar (Z.of_nat (length indexes)) 32
(fun _ : unit ⇒ anyR Tuchar 1$m)
(replicateN
(Z.to_N (32 - Z.of_nat (length indexes))) ())
end
).
Definition merge_inputs_arrayR
(blocksp : ptr) (jobs : list merge_job) : Rep :=
as_Rep
(fun base ⇒
match jobs with
| [] ⇒
base |-> arrayLR merge_input_ptr_ty 0 32
(fun _ : unit ⇒ anyR merge_input_ptr_ty 1$m)
(replicateN 32 ())
| _ :: _ ⇒
base |-> arrayLR merge_input_ptr_ty
0 (Z.of_nat (length jobs))
(fun job_index : nat ⇒
primR merge_input_ptr_ty 1$m
(Vptr (blocksp .[ merge_block_row_ty ! Z.of_nat job_index ])))
(seq 0 (length jobs))
** base |-> arrayLR merge_input_ptr_ty
(Z.of_nat (length jobs)) 32
(fun _ : unit ⇒ anyR merge_input_ptr_ty 1$m)
(replicateN
(Z.to_N (32 - Z.of_nat (length jobs))) ())
end
).
Definition merge_plan_arraysR
(leftsp rightsp blocksp inputsp : ptr) (jobs : list merge_job)
: mpred :=
type_ptr merge_index_array_ty leftsp
** type_ptr merge_index_array_ty rightsp
** type_ptr merge_blocks_array_ty blocksp
** type_ptr merge_inputs_array_ty inputsp
** leftsp |-> merge_index_arrayR (map merge_job_left_index jobs)
** rightsp |-> merge_index_arrayR (map merge_job_right_index jobs)
** blocksp |-> arrayLR merge_block_row_ty 0 32
merge_block_rowR (merge_block_rows jobs)
** inputsp |-> merge_inputs_arrayR blocksp jobs.
Definition merge_plan_arrays_cleanupR
(leftsp rightsp blocksp inputsp : ptr) (jobs : list merge_job)
: mpred :=
type_ptr merge_index_array_ty leftsp
** type_ptr merge_index_array_ty rightsp
** type_ptr merge_blocks_array_ty blocksp
** type_ptr merge_inputs_array_ty inputsp
** leftsp |-> arrayLR Tuchar 0 32
(fun _ : unit ⇒ anyR Tuchar 1$m)
(replicateN 32 ())
** rightsp |-> arrayLR Tuchar 0 32
(fun _ : unit ⇒ anyR Tuchar 1$m)
(replicateN 32 ())
** blocksp |-> arrayLR merge_block_row_ty 0 32
(fun _ : unit ⇒
arrayLR Tuchar 0 64
(fun _ : unit ⇒ anyR Tuchar 1$m)
(replicateN 64 ()))
(replicateN 32 ())
** inputsp |-> arrayLR merge_input_ptr_ty 0 32
(fun _ : unit ⇒ anyR merge_input_ptr_ty 1$m)
(replicateN 32 ()).
Lemma storage_page_empty_page_slots page :
storage_page_empty page = true →
page_slots_model page = repeat None (length page).
Lemma bitmap_to_N_repeat_false bits :
bitmap_to_N (repeat false bits) = 0.
Lemma bitmap_to_bytes16_repeat_false_page_slot_count :
bitmap_to_bytes16 (repeat false page_slot_count) =
bytes16_of_N 0.
Lemma page_commit_root_empty page :
length page = page_slot_count →
storage_page_empty page = true →
bytes32_to_N (root (page_slots_model page)) = blake3_seal_model 0 None.
Lemma page_slots_model_length page :
length (page_slots_model page) = length page.
Lemma normalize_page_slots_model page :
length page = page_slot_count →
normalize_slots (page_slots_model page) = page_slots_model page.
Lemma slot_bitmap_from_page_slots_model index page :
slot_bitmap_from index page =
(2 ^ N.of_nat index ×
bitmap_to_N (map slot_present (page_slots_model page)))%N.
Lemma slot_bitmap_word_page_slots_model page :
slot_bitmap_word page =
bitmap_to_N (map slot_present (page_slots_model page)).
Lemma slot_bitmap_word_lt_128 page :
length page = page_slot_count →
(slot_bitmap_word page < pow2N 128)%N.
Lemma page_slot_bitmap_bytes page :
length page = page_slot_count →
bytes16_of_N (slot_bitmap_word page) =
bitmap_to_bytes16 (slot_bitmap (page_slots_model page)).
Lemma slots_from_bitmap_values_nil bm slots :
slots_from_bitmap_values bm [] = Some slots →
slots = repeat None (length bm).
Lemma page_slots_model_all_none_empty page :
page_slots_model page = repeat None (length page) →
storage_page_empty page = true.
Lemma value_tree_from_page_slots_nonempty page :
length page = page_slot_count →
storage_page_empty page = false →
∃ tree, value_tree_from_slots (page_slots_model page) = Some tree.
Lemma page_commit_root_nonempty page :
length page = page_slot_count →
storage_page_empty page = false →
bytes32_to_N (root (page_slots_model page)) =
blake3_seal_model
(slot_bitmap_word page)
(Some (page_subtree_root_model page)).
Lemma page_commit_root_nonempty_digest page :
length page = page_slot_count →
storage_page_empty page = false →
root (page_slots_model page) =
seal_nonempty
(bytes16_of_N (slot_bitmap_word page))
(page_subtree_root_model page).
Lemma balanced_located_tree_from_page_slots_nonempty page :
length page = page_slot_count →
storage_page_empty page = false →
∃ tree,
balanced_located_tree_from_slots (page_slots_model page) = Some tree.
Lemma page_commit_balanced_root_empty page :
length page = page_slot_count →
storage_page_empty page = true →
bytes32_to_N (balanced_root (page_slots_model page)) =
blake3_seal_model 0 None.
Lemma page_commit_balanced_root_nonempty page :
length page = page_slot_count →
storage_page_empty page = false →
bytes32_to_N (balanced_root (page_slots_model page)) =
blake3_seal_model
(slot_bitmap_word page)
(Some (balanced_page_subtree_root_model page)).
Lemma page_commit_balanced_root_nonempty_digest page :
length page = page_slot_count →
storage_page_empty page = false →
balanced_root (page_slots_model page) =
seal_nonempty
(bytes16_of_N (slot_bitmap_word page))
(balanced_page_subtree_root_model page).
if N.eq_dec word 0 then None else Some (bytes32_of_N word).
Fixpoint page_slots_model (page : list N) : slot_values :=
match page with
| [] ⇒ []
| slot :: rest ⇒ page_slot_value_model slot :: page_slots_model rest
end.
Section with_Sigma.
Context `{Sigma : cpp_logic} {CU : genv} {hh : HasOwn mpredI fracR}.
Definition bytes32_ty : type := "evmc::bytes32"%cpp_type.
Definition storage_page_ty : type := "monad::storage_page_t"%cpp_type.
Definition byte_string_view_ty : type :=
Tnamed
(Ninst
(Nscoped (Nglobal (Nid "std")) (Nid "basic_string_view"))
[Atype Tuchar;
Atype
(Tnamed
(Ninst
(Nscoped (Nglobal (Nid "evmc")) (Nid "byte_traits"))
[Atype Tuchar]))]).
Definition result_storage_page_ty : type :=
Tnamed
(Ninst
(Nscoped
(Nscoped (Nglobal (Nid "boost")) (Nid "outcome_v2"))
(Nid "basic_result"))
[Atype storage_page_ty;
Atype
(Tnamed
(Ninst
(Nscoped (Nglobal (Nid "system_error2"))
(Nid "errored_status_code"))
[Atype
(Tnamed
(Ninst
(Nscoped
(Nscoped (Nglobal (Nid "system_error2"))
(Nid "detail"))
(Nid "erased"))
[Atype "long"%cpp_type]))]));
Atype
(Tnamed
(Ninst
(Nscoped
(Nscoped
(Nscoped
(Nscoped (Nglobal (Nid "boost"))
(Nid "outcome_v2"))
(Nid "experimental"))
(Nid "policy"))
(Nid "status_code_throw"))
[Atype storage_page_ty;
Atype
(Tnamed
(Ninst
(Nscoped (Nglobal (Nid "system_error2"))
(Nid "errored_status_code"))
[Atype
(Tnamed
(Ninst
(Nscoped
(Nscoped
(Nglobal (Nid "system_error2"))
(Nid "detail"))
(Nid "erased"))
[Atype "long"%cpp_type]))]));
Atype "void"%cpp_type]))]).
Definition storage_page_is_empty_lambda_name : name :=
"monad::storage_page_t::is_empty() const::@0"%cpp_name.
Definition compute_page_key_name : name :=
Nscoped (Nglobal (Nid "monad"))
(Nfunction function_qualifiers.N "compute_page_key"
[Tref (Qconst bytes32_ty)]).
Definition compute_slot_offset_name : name :=
Nscoped (Nglobal (Nid "monad"))
(Nfunction function_qualifiers.N "compute_slot_offset"
[Tref (Qconst bytes32_ty)]).
Definition compute_slot_key_name : name :=
Nscoped (Nglobal (Nid "monad"))
(Nfunction function_qualifiers.N "compute_slot_key"
[Tref (Qconst bytes32_ty); Tuchar]).
Definition page_commit_name : name :=
Nscoped (Nglobal (Nid "monad"))
(Nfunction function_qualifiers.N "page_commit"
[Tref (Qconst storage_page_ty)]).
Definition page_commit_balanced_name : name :=
Nscoped (Nglobal (Nid "monad"))
(Nfunction function_qualifiers.N "page_commit_balanced"
[Tref (Qconst storage_page_ty)]).
Definition encode_storage_page_name : name :=
Nscoped (Nglobal (Nid "monad"))
(Nfunction function_qualifiers.N "encode_storage_page"
[Tref (Qconst storage_page_ty)]).
Definition decode_storage_page_name : name :=
Nscoped (Nglobal (Nid "monad"))
(Nfunction function_qualifiers.N "decode_storage_page"
[byte_string_view_ty]).
Definition storage_page_slots : offset :=
_field "monad::storage_page_t::slots".
Definition scratch_array_ty : type :=
Tarray bytes32_ty 64%N.
Definition scratch_arg_ty : type :=
Tdecay_type scratch_array_ty (Tptr bytes32_ty).
Definition merge_index_array_ty : type :=
Tarray Tuchar 32%N.
Definition merge_index_arg_ty : type :=
Tptr Tuchar.
Definition merge_const_index_array_ty : type :=
Tarray (Qconst Tuchar) 32%N.
Definition merge_const_index_arg_ty : type :=
Tptr (Qconst Tuchar).
Definition merge_block_row_ty : type :=
Tarray Tuchar 64%N.
Definition merge_blocks_array_ty : type :=
Tarray merge_block_row_ty 32%N.
Definition merge_blocks_arg_ty : type :=
Tptr merge_block_row_ty.
Definition merge_input_ptr_ty : type :=
Tptr Tuchar.
Definition merge_inputs_array_ty : type :=
Tarray merge_input_ptr_ty 32%N.
Definition merge_inputs_arg_ty : type :=
Tptr merge_input_ptr_ty.
Definition merge_const_inputs_arg_ty : type :=
Tptr (Qconst merge_input_ptr_ty).
Definition merge_output_array_ty : type :=
Tarray bytes32_ty 32%N.
Definition merge_output_arg_ty : type :=
Tptr bytes32_ty.
Definition merge_const_output_array_ty : type :=
Tarray (Qconst bytes32_ty) 32%N.
Definition merge_const_output_arg_ty : type :=
Tptr (Qconst bytes32_ty).
Definition init_leaf_scratch_name : name :=
Nscoped (Nscoped (Nglobal (Nid "monad")) Nanonymous)
(Nfunction function_qualifiers.N "init_leaf_scratch"
[Tref (Qconst storage_page_ty); Qconst Tulong; scratch_arg_ty]).
Definition merge_scratch_level_name : name :=
Nscoped (Nscoped (Nglobal (Nid "monad")) Nanonymous)
(Nfunction function_qualifiers.N "merge_scratch_level"
[Qconst Tuchar; Tulong; scratch_arg_ty]).
Definition init_balanced_leaf_scratch_name : name :=
Nscoped (Nscoped (Nglobal (Nid "monad")) Nanonymous)
(Nfunction function_qualifiers.N "init_balanced_leaf_scratch"
[Tref (Qconst storage_page_ty); Qconst Tulong; scratch_arg_ty]).
Definition merge_balanced_range_name : name :=
Nscoped (Nscoped (Nglobal (Nid "monad")) Nanonymous)
(Nfunction function_qualifiers.N "merge_balanced_range"
[scratch_arg_ty; Qconst Tulong; Qconst Tulong]).
Definition compute_nonempty_subtree_root_name : name :=
Nscoped (Nscoped (Nglobal (Nid "monad")) Nanonymous)
(Nfunction function_qualifiers.N "compute_nonempty_subtree_root"
[Tref (Qconst storage_page_ty); Qconst Tulong]).
Definition storage_SLOTS_name : name :=
Nscoped (Nscoped (Nglobal (Nid "monad")) (Nid "storage_page_t"))
(Nid "SLOTS").
Definition storage_SLOT_SIZE_name : name :=
Nscoped (Nscoped (Nglobal (Nid "monad")) (Nid "storage_page_t"))
(Nid "SLOT_SIZE").
Definition storage_NUM_PAIRS_name : name :=
Nscoped (Nscoped (Nglobal (Nid "monad")) Nanonymous)
(Nid "NUM_PAIRS").
Definition StoragePageR (q : Qp) (page : list N) : Rep :=
storage_page_slots
|-> arrayR bytes32_ty (bytes32R q) page
** structR "monad::storage_page_t" q
** [| length page = page_slot_count |].
Definition storage_page_update_slot
(offset : nat) (value : N) (page : list N) : list N :=
firstn offset page ++ value :: skipn (S offset) page.
Transparent bytes32R evmc_bytes32_wordR.
#[global] Instance StoragePageR_cfrac :
CFracSplittable_1 StoragePageR.
Definition ScratchR (q : Qp) (scratch : list N) : Rep :=
arrayR bytes32_ty (bytes32R q) scratch
** [| length scratch = page_pair_count |].
Definition DecodeStoragePageResultR
(_q : Qp) (_result : option (list N)) : Rep := validR.
Definition page_index_model (key : N) : N :=
N.shiftr key 7.
Definition slot_offset_model (key : N) : N :=
N.land key 127.
Definition slot_key_model (page_key slot_offset : N) : N :=
N.lor
(N.modulo (N.shiftl page_key 7) (2 ^ 256))
(N.land slot_offset 127).
Lemma slot_offset_low_byte key :
N.land (N.land key 255) 127 = slot_offset_model key.
Lemma slot_offset_mask_small offset :
(0 ≤ offset < 128)%Z →
N.land (Z.to_N offset) 127 = Z.to_N offset.
Fixpoint slot_bitmap_from (index : nat) (page : list N) : N :=
match page with
| [] ⇒ 0
| slot :: rest ⇒
(if N.eq_dec slot 0 then 0 else 2 ^ N.of_nat index)
+ slot_bitmap_from (S index) rest
end.
Definition slot_bitmap_word (page : list N) : N :=
slot_bitmap_from 0 page.
Definition pair_slot_mask (pair_index : nat) : N :=
3 × 2 ^ (2 × N.of_nat pair_index).
Definition pair_bit_mask (pair_index : nat) : N :=
2 ^ N.of_nat pair_index.
Fixpoint pair_bitmap_prefix (fuel : nat) (slot_bitmap : N) : N :=
match fuel with
| O ⇒ 0
| S fuel' ⇒
let prefix := pair_bitmap_prefix fuel' slot_bitmap in
if N.eqb (N.land slot_bitmap (pair_slot_mask fuel')) 0
then prefix
else N.lor prefix (pair_bit_mask fuel')
end.
Fixpoint pair_bitmap_from
(fuel : nat) (slot_bitmap pair_index : N) : N :=
match fuel with
| O ⇒ 0
| S fuel' ⇒
let lo := 2 ^ (2 × pair_index) in
let hi := 2 ^ (2 × pair_index + 1) in
(if N.eqb (N.land slot_bitmap (N.lor lo hi)) 0
then 0
else 2 ^ pair_index)
+ pair_bitmap_from fuel' slot_bitmap (N.succ pair_index)
end.
Definition pair_bitmap_word (slot_bitmap : N) : N :=
pair_bitmap_prefix page_pair_count slot_bitmap.
Lemma pair_bitmap_prefix_64_pair_bitmap_word slot_bitmap :
pair_bitmap_prefix 64 slot_bitmap = pair_bitmap_word slot_bitmap.
Opaque pair_bitmap_word.
Definition storage_page_empty (page : list N) : bool :=
forallb (N.eqb 0) page.
Definition bitmap_word_bit (bm : N) (index : nat) : bool :=
negb (N.eqb (N.land bm (2 ^ N.of_nat index)) 0).
Definition page_pair_leaf_model
(page : list N) (pair_index : nat) : pair_leaf :=
(bytes32_of_N (nth (2 × pair_index) page 0),
bytes32_of_N (nth (2 × pair_index + 1) page 0)).
Definition init_leaf_scratch_model
(page : list N) (pair_bitmap : N) (old_scratch : list N) : list N :=
map
(fun pair_index ⇒
if bitmap_word_bit pair_bitmap pair_index
then
bytes32_to_N
(H64 leaf_mode (page_pair_leaf_model page pair_index))
else nth pair_index old_scratch 0)
(seq 0 page_pair_count).
Definition bitmap_clear_lowbit (word : N) : N :=
N.land word (word - 1).
Fixpoint bitmap_indices_from (fuel : nat) (word : N) : list nat :=
match fuel with
| O ⇒ []
| S fuel' ⇒
if N.eqb word 0
then []
else
let idx := N.to_nat (countr_zero64 word) in
idx :: bitmap_indices_from fuel' (bitmap_clear_lowbit word)
end.
Definition bitmap_indices (word : N) : list nat :=
bitmap_indices_from page_pair_count word.
Definition balanced_leaf_hashes
(page : list N) (pair_bitmap : N) : list N :=
blake3_hash_many_outputs
leaf_mode (map (page_pair_leaf_model page) (bitmap_indices pair_bitmap)).
Definition init_balanced_leaf_scratch_model
(page : list N) (pair_bitmap : N) (old_scratch : list N) : list N :=
balanced_leaf_hashes page pair_bitmap ++
drop (length (bitmap_indices pair_bitmap)) old_scratch.
Definition merge_pair_hash (lhs rhs : N) : N :=
bytes32_to_N
(H64 merge_mode (bytes32_of_N lhs, bytes32_of_N rhs)).
Definition merge_balanced_range_step
(scratch : list N) (begin mid : nat) : list N :=
match scratch !! begin, scratch !! mid with
| Some lhs, Some rhs ⇒
<[ begin := merge_pair_hash lhs rhs ]> scratch
| _, _ ⇒ scratch
end.
Fixpoint merge_balanced_range_model_fuel
(fuel : nat) (scratch : list N) (begin end_ : nat) : list N :=
match fuel with
| O ⇒ scratch
| S fuel' ⇒
let count := Nat.sub end_ begin in
if Nat.leb count 1
then scratch
else
let mid := Nat.add begin (Nat.div2 count) in
let scratch_l :=
merge_balanced_range_model_fuel fuel' scratch begin mid in
let scratch_r :=
merge_balanced_range_model_fuel fuel' scratch_l mid end_ in
merge_balanced_range_step scratch_r begin mid
end.
Definition merge_balanced_range_model
(scratch : list N) (begin end_ : nat) : list N :=
merge_balanced_range_model_fuel (Nat.sub end_ begin) scratch begin end_.
Fixpoint balanced_tree_from_digests_fuel
(fuel : nat) (digests : list digest) : option digest :=
match fuel with
| O ⇒
match digests with
| [digest] ⇒ Some digest
| _ ⇒ None
end
| S fuel' ⇒
match digests with
| [] ⇒ None
| [digest] ⇒ Some digest
| _ ⇒
let split := Nat.div2 (length digests) in
match
balanced_tree_from_digests_fuel fuel' (firstn split digests),
balanced_tree_from_digests_fuel fuel' (skipn split digests)
with
| Some lhs, Some rhs ⇒ Some (H64 merge_mode (lhs, rhs))
| _, _ ⇒ None
end
end
end.
Definition balanced_tree_from_digests (digests : list digest) :
option digest :=
balanced_tree_from_digests_fuel (length digests) digests.
Definition page_subtree_root_model (page : list N) : digest :=
match value_tree_from_slots (page_slots_model page) with
| Some tree ⇒ eval_tree tree
| None ⇒ bytes32_of_N 0
end.
Definition balanced_page_subtree_root_model (page : list N) : digest :=
match balanced_located_tree_from_slots (page_slots_model page) with
| Some tree ⇒ eval_located_tree tree
| None ⇒ bytes32_of_N 0
end.
Definition live_nodes_bitmap_word (nodes : list live_node) : N :=
fold_left
(fun bm node ⇒ N.lor bm (2 ^ N.of_nat node.(live_index)))
nodes 0.
Fixpoint live_nodes_well_formed_from
(lower : nat) (nodes : list live_node) : Prop :=
match nodes with
| [] ⇒ True
| node :: rest ⇒
(lower ≤ node.(live_index) < page_pair_count)%nat ∧
live_nodes_well_formed_from (S node.(live_index)) rest
end.
Definition live_nodes_well_formed (nodes : list live_node) : Prop :=
live_nodes_well_formed_from 0 nodes.
Lemma live_nodes_well_formed_from_weaken lower lower' nodes :
(lower' ≤ lower)%nat →
live_nodes_well_formed_from lower nodes →
live_nodes_well_formed_from lower' nodes.
Lemma merge_level_preserves_well_formed_from bit lower nodes :
live_nodes_well_formed_from lower nodes →
live_nodes_well_formed_from lower (merge_level bit nodes).
Lemma merge_level_preserves_well_formed bit nodes :
live_nodes_well_formed nodes →
live_nodes_well_formed (merge_level bit nodes).
Definition scratch_represents_live_nodes
(scratch : list N) (nodes : list live_node) : Prop :=
length scratch = page_pair_count ∧
∀ node,
In node nodes →
nth node.(live_index) scratch 0 =
bytes32_to_N (eval_tree node.(live_tree)).
Record merge_job : Type := {
merge_left : live_node;
merge_right : live_node;
}.
Definition merge_job_node (job : merge_job) : live_node :=
{|
live_index := job.(merge_left).(live_index);
live_tree :=
TreeNode
job.(merge_left).(live_tree)
job.(merge_right).(live_tree);
|}.
Definition merge_job_input (job : merge_job) : bytes64 :=
(eval_tree job.(merge_left).(live_tree),
eval_tree job.(merge_right).(live_tree)).
Definition merge_job_output (job : merge_job) : N :=
bytes32_to_N (H64 merge_mode (merge_job_input job)).
Definition merge_job_left_index (job : merge_job) : nat :=
job.(merge_left).(live_index).
Definition merge_job_right_index (job : merge_job) : nat :=
job.(merge_right).(live_index).
Record merge_scan_state : Type := {
scan_pending : option live_node;
scan_jobs : list merge_job;
}.
Definition initial_merge_scan_state : merge_scan_state :=
{| scan_pending := None; scan_jobs := [] |}.
Definition scan_one_node
(bit : nat) (state : merge_scan_state) (node : live_node)
: merge_scan_state :=
match state.(scan_pending) with
| None ⇒
{|
scan_pending := Some node;
scan_jobs := state.(scan_jobs);
|}
| Some previous ⇒
if sibling_candidate bit previous.(live_index) node.(live_index)
then
{|
scan_pending := None;
scan_jobs :=
state.(scan_jobs) ++
[{| merge_left := previous; merge_right := node |}];
|}
else
{|
scan_pending := Some node;
scan_jobs := state.(scan_jobs);
|}
end.
Fixpoint scan_nodes_from
(bit : nat) (state : merge_scan_state) (nodes : list live_node)
: merge_scan_state :=
match nodes with
| [] ⇒ state
| node :: rest ⇒
scan_nodes_from bit (scan_one_node bit state node) rest
end.
Definition scan_nodes (bit : nat) (nodes : list live_node)
: merge_scan_state :=
scan_nodes_from bit initial_merge_scan_state nodes.
Definition merge_jobs (bit : nat) (nodes : list live_node)
: list merge_job :=
(scan_nodes bit nodes).(scan_jobs).
Local Open Scope nat_scope.
Definition merge_scan_pending_count
(state : merge_scan_state) : nat :=
match state.(scan_pending) with
| Some _ ⇒ 1
| None ⇒ 0
end.
Lemma scan_one_node_jobs_bound bit state node :
2 × length (scan_one_node bit state node).(scan_jobs) +
merge_scan_pending_count (scan_one_node bit state node) ≤
2 × length state.(scan_jobs) +
merge_scan_pending_count state + 1.
Lemma scan_nodes_from_jobs_bound bit nodes state :
2 × length (scan_nodes_from bit state nodes).(scan_jobs) +
merge_scan_pending_count (scan_nodes_from bit state nodes) ≤
2 × length state.(scan_jobs) +
merge_scan_pending_count state + length nodes.
Lemma merge_jobs_two_for_one bit nodes :
2 × length (merge_jobs bit nodes) ≤ length nodes.
Lemma live_nodes_well_formed_from_length lower nodes :
live_nodes_well_formed_from lower nodes →
(lower ≤ page_pair_count)%nat →
(length nodes + lower ≤ page_pair_count)%nat.
Lemma live_nodes_well_formed_length nodes :
live_nodes_well_formed nodes →
(length nodes ≤ page_pair_count)%nat.
Lemma merge_jobs_length_le_32 bit nodes :
live_nodes_well_formed nodes →
(length (merge_jobs bit nodes) ≤ 32)%nat.
Local Close Scope nat_scope.
Definition apply_merge_job_to_scratch
(scratch : list N) (job : merge_job) : list N :=
<[ job.(merge_left).(live_index) := merge_job_output job ]> scratch.
Definition apply_merge_job_to_bitmap (bm : N) (job : merge_job) : N :=
N.clearbit bm (N.of_nat job.(merge_right).(live_index)).
Fixpoint apply_merge_jobs_to_scratch
(scratch : list N) (jobs : list merge_job) : list N :=
match jobs with
| [] ⇒ scratch
| job :: rest ⇒
apply_merge_jobs_to_scratch
(apply_merge_job_to_scratch scratch job) rest
end.
Fixpoint apply_merge_jobs_to_bitmap (bm : N) (jobs : list merge_job) : N :=
match jobs with
| [] ⇒ bm
| job :: rest ⇒
apply_merge_jobs_to_bitmap
(apply_merge_job_to_bitmap bm job) rest
end.
Definition merge_hash_outputs
(jobs : list merge_job) (old_outputs : list N) : list N :=
blake3_hash_many_outputs merge_mode (map merge_job_input jobs) ++
skipn (length jobs) old_outputs.
Inductive merge_block_row : Type :=
| MergeBlockUninit
| MergeBlockLeft : digest → merge_block_row
| MergeBlockFull : bytes64 → merge_block_row.
Definition merge_block_rowR (row : merge_block_row) : Rep :=
match row with
| MergeBlockUninit ⇒
arrayLR Tuchar 0 64
(fun _ : unit ⇒ anyR Tuchar 1$m)
(replicateN 64 ())
| MergeBlockLeft lhs ⇒
arrayLR Tuchar 0 32
(fun byte : val ⇒ primR Tuchar 1$m byte)
(blake3specs.bytes32_byte_values lhs)
** arrayLR Tuchar 32 64
(fun _ : unit ⇒ uninitR Tuchar 1$m)
(replicateN 32 ())
| MergeBlockFull block ⇒
blake3specs.Blake3BlockR 1 block
end.
Definition merge_block_rows (jobs : list merge_job)
: list merge_block_row :=
map (fun job ⇒ MergeBlockFull (merge_job_input job)) jobs ++
replicateN
(Z.to_N (32 - Z.of_nat (length jobs))) MergeBlockUninit.
Definition merge_index_arrayR (indexes : list nat) : Rep :=
as_Rep
(fun base ⇒
match indexes with
| [] ⇒
base |-> arrayLR Tuchar 0 32
(fun _ : unit ⇒ anyR Tuchar 1$m)
(replicateN 32 ())
| _ :: _ ⇒
base |-> arrayLR Tuchar 0 (Z.of_nat (length indexes))
(fun index : nat ⇒ ucharR 1$m (Z.of_nat index)) indexes
** base |-> arrayLR Tuchar (Z.of_nat (length indexes)) 32
(fun _ : unit ⇒ anyR Tuchar 1$m)
(replicateN
(Z.to_N (32 - Z.of_nat (length indexes))) ())
end
).
Definition merge_inputs_arrayR
(blocksp : ptr) (jobs : list merge_job) : Rep :=
as_Rep
(fun base ⇒
match jobs with
| [] ⇒
base |-> arrayLR merge_input_ptr_ty 0 32
(fun _ : unit ⇒ anyR merge_input_ptr_ty 1$m)
(replicateN 32 ())
| _ :: _ ⇒
base |-> arrayLR merge_input_ptr_ty
0 (Z.of_nat (length jobs))
(fun job_index : nat ⇒
primR merge_input_ptr_ty 1$m
(Vptr (blocksp .[ merge_block_row_ty ! Z.of_nat job_index ])))
(seq 0 (length jobs))
** base |-> arrayLR merge_input_ptr_ty
(Z.of_nat (length jobs)) 32
(fun _ : unit ⇒ anyR merge_input_ptr_ty 1$m)
(replicateN
(Z.to_N (32 - Z.of_nat (length jobs))) ())
end
).
Definition merge_plan_arraysR
(leftsp rightsp blocksp inputsp : ptr) (jobs : list merge_job)
: mpred :=
type_ptr merge_index_array_ty leftsp
** type_ptr merge_index_array_ty rightsp
** type_ptr merge_blocks_array_ty blocksp
** type_ptr merge_inputs_array_ty inputsp
** leftsp |-> merge_index_arrayR (map merge_job_left_index jobs)
** rightsp |-> merge_index_arrayR (map merge_job_right_index jobs)
** blocksp |-> arrayLR merge_block_row_ty 0 32
merge_block_rowR (merge_block_rows jobs)
** inputsp |-> merge_inputs_arrayR blocksp jobs.
Definition merge_plan_arrays_cleanupR
(leftsp rightsp blocksp inputsp : ptr) (jobs : list merge_job)
: mpred :=
type_ptr merge_index_array_ty leftsp
** type_ptr merge_index_array_ty rightsp
** type_ptr merge_blocks_array_ty blocksp
** type_ptr merge_inputs_array_ty inputsp
** leftsp |-> arrayLR Tuchar 0 32
(fun _ : unit ⇒ anyR Tuchar 1$m)
(replicateN 32 ())
** rightsp |-> arrayLR Tuchar 0 32
(fun _ : unit ⇒ anyR Tuchar 1$m)
(replicateN 32 ())
** blocksp |-> arrayLR merge_block_row_ty 0 32
(fun _ : unit ⇒
arrayLR Tuchar 0 64
(fun _ : unit ⇒ anyR Tuchar 1$m)
(replicateN 64 ()))
(replicateN 32 ())
** inputsp |-> arrayLR merge_input_ptr_ty 0 32
(fun _ : unit ⇒ anyR merge_input_ptr_ty 1$m)
(replicateN 32 ()).
Lemma storage_page_empty_page_slots page :
storage_page_empty page = true →
page_slots_model page = repeat None (length page).
Lemma bitmap_to_N_repeat_false bits :
bitmap_to_N (repeat false bits) = 0.
Lemma bitmap_to_bytes16_repeat_false_page_slot_count :
bitmap_to_bytes16 (repeat false page_slot_count) =
bytes16_of_N 0.
Lemma page_commit_root_empty page :
length page = page_slot_count →
storage_page_empty page = true →
bytes32_to_N (root (page_slots_model page)) = blake3_seal_model 0 None.
Lemma page_slots_model_length page :
length (page_slots_model page) = length page.
Lemma normalize_page_slots_model page :
length page = page_slot_count →
normalize_slots (page_slots_model page) = page_slots_model page.
Lemma slot_bitmap_from_page_slots_model index page :
slot_bitmap_from index page =
(2 ^ N.of_nat index ×
bitmap_to_N (map slot_present (page_slots_model page)))%N.
Lemma slot_bitmap_word_page_slots_model page :
slot_bitmap_word page =
bitmap_to_N (map slot_present (page_slots_model page)).
Lemma slot_bitmap_word_lt_128 page :
length page = page_slot_count →
(slot_bitmap_word page < pow2N 128)%N.
Lemma page_slot_bitmap_bytes page :
length page = page_slot_count →
bytes16_of_N (slot_bitmap_word page) =
bitmap_to_bytes16 (slot_bitmap (page_slots_model page)).
Lemma slots_from_bitmap_values_nil bm slots :
slots_from_bitmap_values bm [] = Some slots →
slots = repeat None (length bm).
Lemma page_slots_model_all_none_empty page :
page_slots_model page = repeat None (length page) →
storage_page_empty page = true.
Lemma value_tree_from_page_slots_nonempty page :
length page = page_slot_count →
storage_page_empty page = false →
∃ tree, value_tree_from_slots (page_slots_model page) = Some tree.
Lemma page_commit_root_nonempty page :
length page = page_slot_count →
storage_page_empty page = false →
bytes32_to_N (root (page_slots_model page)) =
blake3_seal_model
(slot_bitmap_word page)
(Some (page_subtree_root_model page)).
Lemma page_commit_root_nonempty_digest page :
length page = page_slot_count →
storage_page_empty page = false →
root (page_slots_model page) =
seal_nonempty
(bytes16_of_N (slot_bitmap_word page))
(page_subtree_root_model page).
Lemma balanced_located_tree_from_page_slots_nonempty page :
length page = page_slot_count →
storage_page_empty page = false →
∃ tree,
balanced_located_tree_from_slots (page_slots_model page) = Some tree.
Lemma page_commit_balanced_root_empty page :
length page = page_slot_count →
storage_page_empty page = true →
bytes32_to_N (balanced_root (page_slots_model page)) =
blake3_seal_model 0 None.
Lemma page_commit_balanced_root_nonempty page :
length page = page_slot_count →
storage_page_empty page = false →
bytes32_to_N (balanced_root (page_slots_model page)) =
blake3_seal_model
(slot_bitmap_word page)
(Some (balanced_page_subtree_root_model page)).
Lemma page_commit_balanced_root_nonempty_digest page :
length page = page_slot_count →
storage_page_empty page = false →
balanced_root (page_slots_model page) =
seal_nonempty
(bytes16_of_N (slot_bitmap_word page))
(balanced_page_subtree_root_model page).
For background on the style of the C++ specifications below, see
this video.
cpp.spec "monad::page_commit(const monad::storage_page_t&)"
from storage_page_cpp.module as page_commit_spec
with (
\arg{pagep : ptr} "page" (Vref pagep)
\prepost{qslots}
_global storage_SLOTS_name
|-> primR "unsigned long" qslots (Vn 128)
\prepost{qslot_size}
_global storage_SLOT_SIZE_name
|-> primR "unsigned long" qslot_size (Vn 32)
\prepost{qnum_pairs}
_global storage_NUM_PAIRS_name
|-> primR "unsigned long" qnum_pairs (Vn 64)
\prepost{qleafiv}
_global blake3specs.storage_get_leaf_iv_static_iv_name
|-> blake3specs.Blake3ConstKeyWordsR
qleafiv blake3model.mip8_leaf_iv_words
\prepost{qiv}
_global "IV" |-> blake3specs.Blake3ConstKeyWordsR
qiv model.blake3_iv_words
\prepost{q page} pagep |-> StoragePageR q page
\post{retp : ptr} [Vptr retp]
retp |-> bytes32R 1 (bytes32_to_N (root (page_slots_model page)))
).
cpp.spec "monad::encode_storage_page(const monad::storage_page_t&)"
from storage_page_cpp.module as encode_storage_page_spec
with (
\arg{pagep : ptr} "page" (Vref pagep)
\prepost{q page} pagep |-> StoragePageR q page
\post{retp : ptr} [Vptr retp]
retp |-> ByteStringR 1 (encode_storage_page_model page)
).
cpp.spec "monad::decode_storage_page(std::basic_string_view<unsigned char, evmc::byte_traits<unsigned char>>)"
from storage_page_cpp.module as decode_storage_page_spec
with (
\arg{encp : ptr} "enc" (Vptr encp)
\prepost{q bytes} encp |-> ByteStringViewR q bytes
\post{retp : ptr} [Vptr retp]
retp |-> DecodeStoragePageResultR 1
(decode_storage_page_model bytes)
).
from storage_page_cpp.module as page_commit_spec
with (
\arg{pagep : ptr} "page" (Vref pagep)
\prepost{qslots}
_global storage_SLOTS_name
|-> primR "unsigned long" qslots (Vn 128)
\prepost{qslot_size}
_global storage_SLOT_SIZE_name
|-> primR "unsigned long" qslot_size (Vn 32)
\prepost{qnum_pairs}
_global storage_NUM_PAIRS_name
|-> primR "unsigned long" qnum_pairs (Vn 64)
\prepost{qleafiv}
_global blake3specs.storage_get_leaf_iv_static_iv_name
|-> blake3specs.Blake3ConstKeyWordsR
qleafiv blake3model.mip8_leaf_iv_words
\prepost{qiv}
_global "IV" |-> blake3specs.Blake3ConstKeyWordsR
qiv model.blake3_iv_words
\prepost{q page} pagep |-> StoragePageR q page
\post{retp : ptr} [Vptr retp]
retp |-> bytes32R 1 (bytes32_to_N (root (page_slots_model page)))
).
cpp.spec "monad::encode_storage_page(const monad::storage_page_t&)"
from storage_page_cpp.module as encode_storage_page_spec
with (
\arg{pagep : ptr} "page" (Vref pagep)
\prepost{q page} pagep |-> StoragePageR q page
\post{retp : ptr} [Vptr retp]
retp |-> ByteStringR 1 (encode_storage_page_model page)
).
cpp.spec "monad::decode_storage_page(std::basic_string_view<unsigned char, evmc::byte_traits<unsigned char>>)"
from storage_page_cpp.module as decode_storage_page_spec
with (
\arg{encp : ptr} "enc" (Vptr encp)
\prepost{q bytes} encp |-> ByteStringViewR q bytes
\post{retp : ptr} [Vptr retp]
retp |-> DecodeStoragePageResultR 1
(decode_storage_page_model bytes)
).
The two specs above are tied together by the pure model theorem
decode_encode_storage_page_model.
Concretely, if page has exactly the 128 storage slots expected by
MIP-8 and is already canonical as a list of bytes32 words, then encoding
it with encode_storage_page_model and immediately decoding those bytes
with decode_storage_page_model returns Some page. The canonicality
side condition rules out differences that are only artifacts of the
model's bytes32 normalization. The more general theorem
decode_encode_storage_page_model_normalized states the same roundtrip
for arbitrary 128-slot pages, but returns the normalized page.
Thus, once the C++ encoder is proved against encode_storage_page_spec
and the C++ decoder is proved against decode_storage_page_spec, their
composition inherits this pure model roundtrip property.
This page has been generated by coqdoc