🍲 Dal_services.v

Translated OCaml

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.Alpha_context.
Require TezosOfOCaml.Proto_alpha.Raw_context.

Definition assert_dal_feature_enabled (ctxt : Alpha_context.context)
  : M? unit :=
  let '{|
    Alpha_context.Constants.Parametric.t.dal := {|
      Alpha_context.Constants.Parametric.dal.feature_enable := feature_enable
        |}
      |} := Alpha_context.Constants.parametric_value ctxt in
  Error_monad.error_unless (Compare.Bool.(Compare.S.op_eq) feature_enable true)
    (Build_extensible "Dal_feature_disabled" unit tt).

Definition shards
  (ctxt : Alpha_context.context) (level : Alpha_context.Raw_level.t)
  : M?
    (list
      (Signature.public_key_hash ×
        (Alpha_context.Dal.Attestation.shard_index × int))) :=
  let? '_ := assert_dal_feature_enabled ctxt in
  let? level := Alpha_context.Level.from_raw ctxt level in
  let pkh_from_tenderbake_slot (slot : Alpha_context.Slot.t)
    : M? (Alpha_context.context × Signature.public_key_hash) :=
    let? '(ctxt, consensus_key) :=
      Alpha_context.Stake_distribution.slot_owner ctxt level slot in
    return? (ctxt, consensus_key.(Raw_context.consensus_pk.delegate)) in
  let? committee_value :=
    Alpha_context.Dal.Attestation.compute_committee ctxt
      pkh_from_tenderbake_slot in
  return?
    (Signature.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.Map).(S.INDEXES_MAP.bindings)
      committee_value.(Raw_context.dal_committee.pkh_to_shards)).