Skip to main content

🍲 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.V7.
Require TezosOfOCaml.Proto_alpha.Alpha_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.Tzresult_syntax.fail
      (Build_extensible "Dal_slot_index_above_hard_limit" unit tt)
  | Some slot_indexreturn? slot_index
  end.

Definition validate_data_availability
  (ctxt : Alpha_context.context)
  (data_availability : Alpha_context.Dal.Endorsement.t) : M? unit :=
  let? '_ := assert_dal_feature_enabled ctxt 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.Endorsement.expected_size_in_bits max_index in
  let size_value :=
    Alpha_context.Dal.Endorsement.occupied_size_in_bits data_availability in
  Error_monad.error_unless (size_value i maximum_size)
    (Build_extensible "Dal_endorsement_size_limit_exceeded"
      Alpha_context.Dal_errors.Dal_endorsement_size_limit_exceeded
      {|
        Alpha_context.Dal_errors.Dal_endorsement_size_limit_exceeded.maximum_size
          := maximum_size;
        Alpha_context.Dal_errors.Dal_endorsement_size_limit_exceeded.got :=
          size_value; |}).

Definition apply_data_availability
  (ctxt : Alpha_context.context)
  (data_availability : Alpha_context.Dal.Endorsement.t)
  (endorser : Alpha_context.public_key_hash) : M? Alpha_context.context :=
  let? '_ := assert_dal_feature_enabled ctxt in
  let shards := Alpha_context.Dal.Endorsement.shards ctxt endorser in
  return?
    (Alpha_context.Dal.Endorsement.record_available_shards ctxt
      data_availability shards).

Definition validate_publish_slot_header
  (ctxt : Alpha_context.context) (function_parameter : Alpha_context.Dal.Slot.t)
  : M? unit :=
  let '{|
    Alpha_context.Dal.Slot.t.id := {|
      Alpha_context.Dal.Slot.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
  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; |}).

Definition apply_publish_slot_header
  (ctxt : Alpha_context.context) (slot : Alpha_context.Dal.Slot.t)
  : M? Alpha_context.context :=
  let? '_ := assert_dal_feature_enabled ctxt in
  let? '(ctxt, updated) := Alpha_context.Dal.Slot.register_slot ctxt slot 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 :=
            slot; |}).

Definition dal_finalisation (ctxt : Alpha_context.context)
  : M? (Alpha_context.context × option Alpha_context.Dal.Endorsement.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_slots ctxt in
      let? '(ctxt, slot_availability) :=
        Alpha_context.Dal.Slot.finalize_pending_slots ctxt in
      return? (ctxt, (Some slot_availability))).