Skip to main content

🥖 Baking.v

Translated OCaml

See proofs, See simulations, Gitlab , OCaml

File generated by coq-of-ocaml
Init function; without side-effects in Coq
Definition init_module1 : unit :=
  Error_monad.register_error_kind Error_monad.Permanent
    "baking.insufficient_endorsing_power" "Insufficient endorsing power"
    "The endorsing power is insufficient to satisfy the consensus threshold."
    (Some
      (fun (ppf : Format.formatter) ⇒
        fun (function_parameter : int × int) ⇒
          let '(endorsing_power, consensus_threshold) := function_parameter in
          Format.fprintf ppf
            (CamlinternalFormatBasics.Format
              (CamlinternalFormatBasics.String_literal "The endorsing power ("
                (CamlinternalFormatBasics.Int CamlinternalFormatBasics.Int_d
                  CamlinternalFormatBasics.No_padding
                  CamlinternalFormatBasics.No_precision
                  (CamlinternalFormatBasics.String_literal
                    ") is insufficient to satisfy the consensus threshold ("
                    (CamlinternalFormatBasics.Int CamlinternalFormatBasics.Int_d
                      CamlinternalFormatBasics.No_padding
                      CamlinternalFormatBasics.No_precision
                      (CamlinternalFormatBasics.String_literal ")."
                        CamlinternalFormatBasics.End_of_format)))))
              "The endorsing power (%d) is insufficient to satisfy the consensus threshold (%d).")
            endorsing_power consensus_threshold))
    (Data_encoding.obj2
      (Data_encoding.req None None "endorsing_power" Data_encoding.int31)
      (Data_encoding.req None None "consensus_threshold" Data_encoding.int31))
    (fun (function_parameter : Error_monad._error) ⇒
      match function_parameter with
      | Build_extensible tag _ payload
        if String.eqb tag "Insufficient_endorsing_power" then
          let '{|
            Insufficient_endorsing_power.endorsing_power := endorsing_power;
              Insufficient_endorsing_power.consensus_threshold :=
                consensus_threshold
              |} := cast Insufficient_endorsing_power payload in
          Some (endorsing_power, consensus_threshold)
        else None
      end)
    (fun (function_parameter : int × int) ⇒
      let '(endorsing_power, consensus_threshold) := function_parameter in
      Build_extensible "Insufficient_endorsing_power"
        Insufficient_endorsing_power
        {| Insufficient_endorsing_power.endorsing_power := endorsing_power;
          Insufficient_endorsing_power.consensus_threshold :=
            consensus_threshold; |}).

Definition bonus_baking_reward
  (ctxt : Alpha_context.context) (endorsing_power : int)
  : M? Alpha_context.Tez.tez :=
  let consensus_threshold := Alpha_context.Constants.consensus_threshold ctxt in
  let baking_reward_bonus_per_slot :=
    Alpha_context.Constants.baking_reward_bonus_per_slot ctxt in
  let extra_endorsing_power := endorsing_power -i consensus_threshold in
  let? '_ :=
    Error_monad.error_when (extra_endorsing_power <i 0)
      (Build_extensible "Insufficient_endorsing_power"
        Insufficient_endorsing_power
        {| Insufficient_endorsing_power.endorsing_power := endorsing_power;
          Insufficient_endorsing_power.consensus_threshold :=
            consensus_threshold; |}) in
  Alpha_context.Tez.op_starquestion baking_reward_bonus_per_slot
    (Int64.of_int extra_endorsing_power).

#[bypass_check(guard)]
Definition baking_rights
  (c_value : Alpha_context.context) (level : Alpha_context.Level.t)
  : M? (Misc.lazy_list_t Alpha_context.Consensus_key.t) :=
  let fix f_value
    (c_value : Alpha_context.context) (round : Alpha_context.Round.t)
    {struct round} : M? (Misc.lazy_list_t Alpha_context.Consensus_key.t) :=
    let? '(c_value, _slot, consensus_pk) :=
      Alpha_context.Stake_distribution.baking_rights_owner c_value level round
      in
    return?
      (Misc.LCons (Alpha_context.Consensus_key.pkh consensus_pk)
        (fun (function_parameter : unit) ⇒
          let '_ := function_parameter in
          f_value c_value (Alpha_context.Round.succ round))) in
  f_value c_value Alpha_context.Round.zero.

Module ordered_slots.
  Record record : Set := Build {
    delegate : Signature.public_key_hash;
    consensus_key : Signature.public_key_hash;
    slots : list Alpha_context.Slot.t;
  }.
  Definition with_delegate delegate (r : record) :=
    Build delegate r.(consensus_key) r.(slots).
  Definition with_consensus_key consensus_key (r : record) :=
    Build r.(delegate) consensus_key r.(slots).
  Definition with_slots slots (r : record) :=
    Build r.(delegate) r.(consensus_key) slots.
End ordered_slots.
Definition ordered_slots := ordered_slots.record.

Definition endorsing_rights
  (ctxt : Alpha_context.t) (level : Alpha_context.Level.t)
  : M?
    (Alpha_context.context ×
      Signature.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.Map).(S.INDEXES_MAP.t)
        ordered_slots) :=
  let consensus_committee_size :=
    Alpha_context.Constants.consensus_committee_size ctxt in
  let? slots := Alpha_context.Slot.Range.create 0 consensus_committee_size in
  Alpha_context.Slot.Range.rev_fold_es
    (fun (function_parameter :
      Alpha_context.context ×
        Signature.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.Map).(S.INDEXES_MAP.t)
          ordered_slots) ⇒
      let '(ctxt, map) := function_parameter in
      fun (slot : Alpha_context.Slot.slot) ⇒
        let? '(ctxt, consensus_pk) :=
          Alpha_context.Stake_distribution.slot_owner ctxt level slot in
        let map :=
          Signature.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.Map).(S.INDEXES_MAP.update)
            consensus_pk.(Raw_context.consensus_pk.delegate)
            (fun (function_parameter : option ordered_slots) ⇒
              match function_parameter with
              | None
                Some
                  {|
                    ordered_slots.delegate :=
                      consensus_pk.(Raw_context.consensus_pk.delegate);
                    ordered_slots.consensus_key :=
                      consensus_pk.(Raw_context.consensus_pk.consensus_pkh);
                    ordered_slots.slots := [ slot ]; |}
              | Some slots
                Some
                  (ordered_slots.with_slots
                    (cons slot slots.(ordered_slots.slots)) slots)
              end) map in
        return? (ctxt, map))
    (ctxt,
      Signature.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.Map).(S.INDEXES_MAP.empty))
    slots.

Definition endorsing_rights_by_first_slot
  (ctxt : Alpha_context.context) (level : Alpha_context.Level.t)
  : M?
    (Alpha_context.context ×
      Alpha_context.Slot.Map.(Map.S.t) (Alpha_context.Consensus_key.pk × int)) :=
  let? slots :=
    Alpha_context.Slot.Range.create 0
      (Alpha_context.Constants.consensus_committee_size ctxt) in
  let? '(ctxt, (_, slots_map)) :=
    Alpha_context.Slot.Range.fold_es
      (fun (function_parameter :
        Alpha_context.context ×
          (Signature.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.Map).(S.INDEXES_MAP.t)
            Alpha_context.Slot.slot ×
            Alpha_context.Slot.Map.(Map.S.t)
              (Alpha_context.Consensus_key.pk × int))) ⇒
        let '(ctxt, (delegates_map, slots_map)) := function_parameter in
        fun (slot : Alpha_context.Slot.slot) ⇒
          let? '(ctxt, consensus_pk) :=
            Alpha_context.Stake_distribution.slot_owner ctxt level slot in
          let '(initial_slot, delegates_map) :=
            match
              Signature.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.Map).(S.INDEXES_MAP.find)
                consensus_pk.(Raw_context.consensus_pk.delegate) delegates_map
              with
            | None
              (slot,
                (Signature.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.Map).(S.INDEXES_MAP.add)
                  consensus_pk.(Raw_context.consensus_pk.delegate) slot
                  delegates_map))
            | Some initial_slot(initial_slot, delegates_map)
            end in
          let slots_map :=
            Alpha_context.Slot.Map.(Map.S.update) initial_slot
              (fun (function_parameter :
                option (Alpha_context.Consensus_key.pk × int)) ⇒
                match function_parameter with
                | NoneSome (consensus_pk, 1)
                | Some (consensus_pk, count)
                  Some (consensus_pk, (count +i 1))
                end) slots_map in
          return? (ctxt, (delegates_map, slots_map)))
      (ctxt,
        (Signature.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.Map).(S.INDEXES_MAP.empty),
          Alpha_context.Slot.Map.(Map.S.empty))) slots in
  return? (ctxt, slots_map).