🍲 Dal_apply.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.Alpha_context.
Require TezosOfOCaml.Proto_alpha.Dal_slot_repr.
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 only_if_dal_feature_enabled {A : Set}
  (ctxt : Alpha_context.context) (default : Alpha_context.context → A)
  (f_value : Alpha_context.context → A) : A :=
  let '{|
    Alpha_context.Constants.Parametric.t.dal := {|
      Alpha_context.Constants.Parametric.dal.feature_enable := feature_enable
        |}
      |} := Alpha_context.Constants.parametric_value ctxt in
  if feature_enable then
    f_value ctxt
  else
    default ctxt.

Definition slot_of_int_e (n_value : int) : M? Alpha_context.Dal.Slot_index.t :=
  match Alpha_context.Dal.Slot_index.of_int n_value with
  | None ⇒
    Error_monad.Result_syntax.tzfail
      (Build_extensible "Dal_slot_index_above_hard_limit" unit tt)
  | Some slot_index ⇒ return? slot_index
  end.

Definition validate_attestation
  (ctxt : Alpha_context.context) (op : Alpha_context.Dal.Attestation.operation)
  : M? unit :=
  let? '_ := assert_dal_feature_enabled ctxt in
  let '{|
    Alpha_context.Dal.Attestation.operation.attestor := _;
      Alpha_context.Dal.Attestation.operation.attestation := attestation;
      Alpha_context.Dal.Attestation.operation.level := given
      |} := op in
  let? max_index :=
    slot_of_int_e
      ((Alpha_context.Constants.parametric_value ctxt).(Alpha_context.Constants.Parametric.t.dal).(Alpha_context.Constants.Parametric.dal.number_of_slots)
      -i 1) in
  let maximum_size :=
    Alpha_context.Dal.Attestation.expected_size_in_bits max_index in
  let size_value :=
    Alpha_context.Dal.Attestation.occupied_size_in_bits attestation in
  let? '_ :=
    Error_monad.error_unless (size_value ≤i maximum_size)
      (Build_extensible "Dal_attestation_size_limit_exceeded"
        Alpha_context.Dal_errors.Dal_attestation_size_limit_exceeded
        {|
          Alpha_context.Dal_errors.Dal_attestation_size_limit_exceeded.maximum_size
            := maximum_size;
          Alpha_context.Dal_errors.Dal_attestation_size_limit_exceeded.got :=
            size_value; |}) in
  let current :=
    (Alpha_context.Level.current ctxt).(Alpha_context.Level.t.level) in
  let delta_levels := Alpha_context.Raw_level.diff_value current given in
  let? '_ :=
    Error_monad.error_when (delta_levels >i32 0)
      (Build_extensible "Dal_operation_for_old_level"
        Alpha_context.Dal_errors.Dal_operation_for_old_level
        {|
          Alpha_context.Dal_errors.Dal_operation_for_old_level.current :=
            current;
          Alpha_context.Dal_errors.Dal_operation_for_old_level.given := given;
          |}) in
  Error_monad.error_when (delta_levels <i32 0)
    (Build_extensible "Dal_operation_for_future_level"
      Alpha_context.Dal_errors.Dal_operation_for_future_level
      {|
        Alpha_context.Dal_errors.Dal_operation_for_future_level.current :=
          current;
        Alpha_context.Dal_errors.Dal_operation_for_future_level.given := given;
        |}).

Definition apply_attestation
  (ctxt : Alpha_context.context) (op : Alpha_context.Dal.Attestation.operation)
  : M? Alpha_context.context :=
  let? '_ := assert_dal_feature_enabled ctxt in
  let '{|
    Alpha_context.Dal.Attestation.operation.attestor := attestor;
      Alpha_context.Dal.Attestation.operation.attestation := attestation;
      Alpha_context.Dal.Attestation.operation.level := _
      |} := op in
  match Alpha_context.Dal.Attestation.shards_of_attestor ctxt attestor with
  | None ⇒
    let level := Alpha_context.Level.current ctxt in
    Error_monad.error_value
      (Build_extensible "Dal_data_availibility_attestor_not_in_committee"
        Alpha_context.Dal_errors.Dal_data_availibility_attestor_not_in_committee
        {|
          Alpha_context.Dal_errors.Dal_data_availibility_attestor_not_in_committee.attestor
            := attestor;
          Alpha_context.Dal_errors.Dal_data_availibility_attestor_not_in_committee.level
            := level; |})
  | Some shards ⇒
    Pervasives.Ok
      (Alpha_context.Dal.Attestation.record_available_shards ctxt attestation
        shards)
  end.

Definition validate_publish_slot_header
  (ctxt : Alpha_context.context)
  (function_parameter : Alpha_context.Dal.Slot.Header.t) : M? unit :=
  let '{|
    Alpha_context.Dal.Slot.Header.t.id := {|
      Dal_slot_repr.Header.id.published_level := published_level;
        Dal_slot_repr.Header.id.index := index_value
        |}
      |} := function_parameter in
  let? '_ := assert_dal_feature_enabled ctxt in
  let '{|
    Alpha_context.Constants.Parametric.t.dal := {|
      Alpha_context.Constants.Parametric.dal.number_of_slots := number_of_slots
        |}
      |} := Alpha_context.Constants.parametric_value ctxt in
  let? number_of_slots := slot_of_int_e (number_of_slots -i 1) in
  let? '_ :=
    Error_monad.error_unless
      (((Alpha_context.Dal.Slot_index.compare index_value number_of_slots) ≤i 0)
      &&
      ((Alpha_context.Dal.Slot_index.compare index_value
        Alpha_context.Dal.Slot_index.zero) ≥i 0))
      (Build_extensible "Dal_publish_slot_header_invalid_index"
        Alpha_context.Dal_errors.Dal_publish_slot_header_invalid_index
        {|
          Alpha_context.Dal_errors.Dal_publish_slot_header_invalid_index.given
            := index_value;
          Alpha_context.Dal_errors.Dal_publish_slot_header_invalid_index.maximum
            := number_of_slots; |}) in
  let current_level :=
    (Alpha_context.Level.current ctxt).(Alpha_context.Level.t.level) in
  let? '_ :=
    Error_monad.error_when
      (Alpha_context.Raw_level.op_lt current_level published_level)
      (Build_extensible "Dal_publish_slot_header_future_level"
        Alpha_context.Dal_errors.Dal_publish_slot_header_future_level
        {|
          Alpha_context.Dal_errors.Dal_publish_slot_header_future_level.provided
            := published_level;
          Alpha_context.Dal_errors.Dal_publish_slot_header_future_level.expected
            := current_level; |}) in
  Error_monad.error_when
    (Alpha_context.Raw_level.op_gt current_level published_level)
    (Build_extensible "Dal_publish_slot_header_past_level"
      Alpha_context.Dal_errors.Dal_publish_slot_header_past_level
      {|
        Alpha_context.Dal_errors.Dal_publish_slot_header_past_level.provided :=
          published_level;
        Alpha_context.Dal_errors.Dal_publish_slot_header_past_level.expected :=
          current_level; |}).

Definition apply_publish_slot_header
  (ctxt : Alpha_context.context) (slot_header : Alpha_context.Dal.Slot.Header.t)
  : M? Alpha_context.context :=
  let? '_ := assert_dal_feature_enabled ctxt in
  let? '(ctxt, updated) :=
    Alpha_context.Dal.Slot.register_slot_header ctxt slot_header in
  if updated then
    return? ctxt
  else
    Error_monad.error_value
      (Build_extensible "Dal_publish_slot_header_duplicate"
        Alpha_context.Dal_errors.Dal_publish_slot_header_duplicate
        {|
          Alpha_context.Dal_errors.Dal_publish_slot_header_duplicate.slot_header
            := slot_header; |}).

Definition finalisation (ctxt : Alpha_context.context)
  : M? (Alpha_context.context × option Alpha_context.Dal.Attestation.t) :=
  only_if_dal_feature_enabled ctxt
    (fun (ctxt : Alpha_context.context) ⇒ return? (ctxt, None))
    (fun (ctxt : Alpha_context.context) ⇒
      let ctxt := Alpha_context.Dal.Slot.finalize_current_slot_headers ctxt in
      let? '(ctxt, attestation) :=
        Alpha_context.Dal.Slot.finalize_pending_slot_headers ctxt in
      return? (ctxt, (Some attestation))).

Definition initialisation
  (ctxt : Alpha_context.context) (level : Alpha_context.Level.t)
  : M? Alpha_context.context :=
  only_if_dal_feature_enabled ctxt
    (fun (ctxt : Alpha_context.context) ⇒ return? ctxt)
    (fun (ctxt : Alpha_context.context) ⇒
      let pkh_from_tenderbake_slot (slot : Alpha_context.Slot.t)
        : M? (Alpha_context.context × Signature.public_key_hash) :=
        let? '(ctxt, consensus_pk1) :=
          Alpha_context.Stake_distribution.slot_owner ctxt level slot in
        return? (ctxt, consensus_pk1.(Raw_context.consensus_pk.delegate)) in
      let? committee_value :=
        Alpha_context.Dal.Attestation.compute_committee ctxt
          pkh_from_tenderbake_slot in
      return?
        (Alpha_context.Dal.Attestation.init_committee ctxt committee_value)).