🍃 Dal.v

Environment

Gitlab

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 parameters_encoding : Data_encoding.t parameters.

Parameter make : parameters → Pervasives.result t Variant.t.

Parameter parameters_value : t → parameters.

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.

Definition page : Set := bytes.

Parameter page_proof : Set.

Parameter page_proof_encoding : Data_encoding.t page_proof.

Parameter pages_per_slot : parameters → int.

Parameter verify_page :
  t → commitment → int → page → page_proof → Result.t bool Variant.t.