🍲 Dal_attestation_repr.v

Translated OCaml

See proofs, Gitlab , OCaml

File generated by coq-of-ocaml

Require Import CoqOfOCaml.CoqOfOCaml.
Require Import CoqOfOCaml.Settings.

Require Import TezosOfOCaml.Environment.V8.
Require TezosOfOCaml.Proto_alpha.Bitset.
Require TezosOfOCaml.Proto_alpha.Dal_slot_repr.
Require TezosOfOCaml.Proto_alpha.Misc.
Require TezosOfOCaml.Proto_alpha.Raw_level_repr.

Definition t : Set := Bitset.t.

Definition attested_slots : Set := t.

Module operation.
  Record record : Set := Build {
    attestor : Signature.public_key_hash;
    attestation : t;
    level : Raw_level_repr.t;
  }.
  Definition with_attestor attestor (r : record) :=
    Build attestor r.(attestation) r.(level).
  Definition with_attestation attestation (r : record) :=
    Build r.(attestor) attestation r.(level).
  Definition with_level level (r : record) :=
    Build r.(attestor) r.(attestation) level.
End operation.
Definition operation := operation.record.

Definition encoding : Data_encoding.t Bitset.t := Bitset.encoding.

Definition empty : Bitset.t := Bitset.empty.

Definition is_attested
  (t_value : Bitset.t) (index_value : Dal_slot_repr.Index.t) : bool :=
  match Bitset.mem t_value (Dal_slot_repr.Index.to_int index_value) with
  | Pervasives.Ok b_value ⇒ b_value
  | Pervasives.Error _ ⇒ false
  end.

Definition commit (t_value : Bitset.t) (index_value : Dal_slot_repr.Index.t)
  : Bitset.t :=
  match Bitset.add t_value (Dal_slot_repr.Index.to_int index_value) with
  | Pervasives.Ok t_value ⇒ t_value
  | Pervasives.Error _ ⇒ t_value
  end.

Definition occupied_size_in_bits : Bitset.t → int :=
  Bitset.occupied_size_in_bits.

Definition expected_size_in_bits (max_index : Dal_slot_repr.Index.t) : int :=
  match Bitset.add Bitset.empty (Dal_slot_repr.Index.to_int max_index) with
  | Pervasives.Error _ ⇒ 0
  | Pervasives.Ok t_value ⇒ Bitset.occupied_size_in_bits t_value
  end.

Definition shard_index : Set := int.

Definition Shard_map :=
  Map.Make
    (let t : Set := shard_index in
    let compare := Compare.Int.compare in
    {|
      Compare.COMPARABLE.compare := compare
    |}).

Module Accountability.
  Definition t : Set := list Bitset.t.

  Definition init_value (length : int) : list Bitset.t :=
    let l_value :=
      List.init_value
        "Dal_attestation_repr.Accountability.init: length cannot be negative"
        length
        (fun (function_parameter : int) ⇒
          let '_ := function_parameter in
          Bitset.empty) in
    match l_value with
    | Pervasives.Error msg ⇒ Pervasives.invalid_arg msg
    | Pervasives.Ok l_value ⇒ l_value
    end.

  Definition record_slot_shard_availability
    (bitset : Bitset.t) (shards : list int) : Bitset.t :=
    List.fold_left
      (fun (bitset : Bitset.t) ⇒
        fun (shard : int) ⇒
          (fun x_1 ⇒ Result.value_value x_1 bitset) (Bitset.add bitset shard))
      bitset shards.

  Definition record_shards_availability
    (shard_bitset_per_slot : list Bitset.t) (slots : Bitset.t)
    (shards : list int) : list Bitset.t :=
    List.mapi
      (fun (slot : int) ⇒
        fun (bitset : Bitset.t) ⇒
          match Bitset.mem slots slot with
          | Pervasives.Error _ ⇒ bitset
          | Pervasives.Ok slot_available ⇒
            if slot_available then
              record_slot_shard_availability bitset shards
            else
              bitset
          end) shard_bitset_per_slot.

  Definition is_slot_available
    (shard_bitset_per_slot : list Bitset.t) (threshold : int)
    (number_of_shards : int) (index_value : Dal_slot_repr.Index.t) : bool :=
    match
      List.nth shard_bitset_per_slot (Dal_slot_repr.Index.to_int index_value)
      with
    | None ⇒ false
    | Some bitset ⇒
      let acc_value := Pervasives.ref_value 0 in
      let '_ :=
        List.iter
          (fun (x_value : int) ⇒
            match Bitset.mem bitset x_value with
            | (Pervasives.Error _ | Pervasives.Ok false) ⇒ tt
            | Pervasives.Ok true ⇒ Pervasives.incr acc_value
            end) (Misc.op_minusminusgt 0 (number_of_shards -i 1)) in
      (Pervasives.op_exclamation acc_value) ≥i
      ((threshold ×i number_of_shards) /i 100)
    end.
End Accountability.