🍲 Dal_attestation_repr.v
Translated 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.
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.