🍃 Dal.v
Environment
Require Import CoqOfOCaml.CoqOfOCaml.
Require Import CoqOfOCaml.Settings.
Require TezosOfOCaml.Environment.Structs.V0.Data_encoding.
Require TezosOfOCaml.Environment.Structs.V0.Result.
Parameter t : Set.
Module parameters.
Record record : Set := Build {
redundancy_factor : int;
page_size : int;
slot_size : int;
number_of_shards : int;
}.
Definition with_redundancy_factor redundancy_factor (r : record) :=
Build redundancy_factor r.(page_size) r.(slot_size) r.(number_of_shards).
Definition with_page_size page_size (r : record) :=
Build r.(redundancy_factor) page_size r.(slot_size) r.(number_of_shards).
Definition with_slot_size slot_size (r : record) :=
Build r.(redundancy_factor) r.(page_size) slot_size r.(number_of_shards).
Definition with_number_of_shards number_of_shards (r : record) :=
Build r.(redundancy_factor) r.(page_size) r.(slot_size) number_of_shards.
End parameters.
Definition parameters := parameters.record.
Parameter make : parameters → Pervasives.result t Variant.t.
Parameter commitment : Set.
Module Commitment.
Parameter encoding : Data_encoding.t commitment.
Parameter to_b58check : commitment → string.
Parameter of_b58check_opt : string → option commitment.
Parameter zero : commitment.
Parameter equal : commitment → commitment → bool.
Parameter pp : Format.formatter → commitment → unit.
End Commitment.
Parameter commitment_proof : Set.
Parameter commitment_proof_encoding : Data_encoding.t commitment_proof.
Parameter verify_commitment : t → commitment → commitment_proof → bool.
Module page.
Record record : Set := Build {
index : int;
content : bytes;
}.
Definition with_index index (r : record) :=
Build index r.(content).
Definition with_content content (r : record) :=
Build r.(index) content.
End page.
Definition page := page.record.
Parameter page_proof : Set.
Parameter page_proof_encoding : Data_encoding.t page_proof.
Parameter verify_page :
t → commitment → page → page_proof → Result.t bool Variant.t.
Require Import CoqOfOCaml.Settings.
Require TezosOfOCaml.Environment.Structs.V0.Data_encoding.
Require TezosOfOCaml.Environment.Structs.V0.Result.
Parameter t : Set.
Module parameters.
Record record : Set := Build {
redundancy_factor : int;
page_size : int;
slot_size : int;
number_of_shards : int;
}.
Definition with_redundancy_factor redundancy_factor (r : record) :=
Build redundancy_factor r.(page_size) r.(slot_size) r.(number_of_shards).
Definition with_page_size page_size (r : record) :=
Build r.(redundancy_factor) page_size r.(slot_size) r.(number_of_shards).
Definition with_slot_size slot_size (r : record) :=
Build r.(redundancy_factor) r.(page_size) slot_size r.(number_of_shards).
Definition with_number_of_shards number_of_shards (r : record) :=
Build r.(redundancy_factor) r.(page_size) r.(slot_size) number_of_shards.
End parameters.
Definition parameters := parameters.record.
Parameter make : parameters → Pervasives.result t Variant.t.
Parameter commitment : Set.
Module Commitment.
Parameter encoding : Data_encoding.t commitment.
Parameter to_b58check : commitment → string.
Parameter of_b58check_opt : string → option commitment.
Parameter zero : commitment.
Parameter equal : commitment → commitment → bool.
Parameter pp : Format.formatter → commitment → unit.
End Commitment.
Parameter commitment_proof : Set.
Parameter commitment_proof_encoding : Data_encoding.t commitment_proof.
Parameter verify_commitment : t → commitment → commitment_proof → bool.
Module page.
Record record : Set := Build {
index : int;
content : bytes;
}.
Definition with_index index (r : record) :=
Build index r.(content).
Definition with_content content (r : record) :=
Build r.(index) content.
End page.
Definition page := page.record.
Parameter page_proof : Set.
Parameter page_proof_encoding : Data_encoding.t page_proof.
Parameter verify_page :
t → commitment → page → page_proof → Result.t bool Variant.t.