🥖 Baking.v
Translated OCaml
See proofs, See simulations, 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.
Module Insufficient_endorsing_power.
Record record : Set := Build {
endorsing_power : int;
consensus_threshold : int;
}.
Definition with_endorsing_power endorsing_power (r : record) :=
Build endorsing_power r.(consensus_threshold).
Definition with_consensus_threshold consensus_threshold (r : record) :=
Build r.(endorsing_power) consensus_threshold.
End Insufficient_endorsing_power.
Definition Insufficient_endorsing_power := Insufficient_endorsing_power.record.
Require Import CoqOfOCaml.Settings.
Require Import TezosOfOCaml.Environment.V8.
Require TezosOfOCaml.Proto_alpha.Alpha_context.
Require TezosOfOCaml.Proto_alpha.Raw_context.
Module Insufficient_endorsing_power.
Record record : Set := Build {
endorsing_power : int;
consensus_threshold : int;
}.
Definition with_endorsing_power endorsing_power (r : record) :=
Build endorsing_power r.(consensus_threshold).
Definition with_consensus_threshold consensus_threshold (r : record) :=
Build r.(endorsing_power) consensus_threshold.
End Insufficient_endorsing_power.
Definition Insufficient_endorsing_power := Insufficient_endorsing_power.record.
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).
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
| None ⇒ Some (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).
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).
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
| None ⇒ Some (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).