👥 Delegate_consensus_key.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.Constants_storage.
Require TezosOfOCaml.Proto_alpha.Contract_repr.
Require TezosOfOCaml.Proto_alpha.Cycle_repr.
Require TezosOfOCaml.Proto_alpha.Level_repr.
Require TezosOfOCaml.Proto_alpha.Raw_context.
Require TezosOfOCaml.Proto_alpha.Storage.
Require TezosOfOCaml.Proto_alpha.Storage_sigs.

Init function; without side-effects in Coq

Definition init_module : unit :=
  let '_ :=
    Error_monad.register_error_kind Error_monad.Permanent
      "delegate.consensus_key.invalid_noop"
      "Invalid key for consensus key update"
      "Tried to update the consensus key with the active key"
      (Some
        (fun (ppf : Format.formatter) ⇒
          fun (cycle : Cycle_repr.cycle) ⇒
            Format.fprintf ppf
              (CamlinternalFormatBasics.Format
                (CamlinternalFormatBasics.String_literal
                  "Invalid key while updating a consensus key (already active since "
                  (CamlinternalFormatBasics.Alpha
                    (CamlinternalFormatBasics.String_literal ")."
                      CamlinternalFormatBasics.End_of_format)))
                "Invalid key while updating a consensus key (already active since %a).")
              Cycle_repr.pp cycle))
      (Data_encoding.obj1
        (Data_encoding.req None None "cycle" Cycle_repr.encoding))
      (fun (function_parameter : Error_monad._error) ⇒
        match function_parameter with
        | Build_extensible tag _ payload ⇒
          if String.eqb tag "Invalid_consensus_key_update_noop" then
            let c_value := cast Cycle_repr.t payload in
            Some c_value
          else None
        end)
      (fun (c_value : Cycle_repr.cycle) ⇒
        Build_extensible "Invalid_consensus_key_update_noop" Cycle_repr.cycle
          c_value) in
  Error_monad.register_error_kind Error_monad.Permanent
    "delegate.consensus_key.active" "Active consensus key"
    "The delegate consensus key is already used by another delegate"
    (Some
      (fun (ppf : Format.formatter) ⇒
        fun (function_parameter : unit) ⇒
          let '_ := function_parameter in
          Format.fprintf ppf
            (CamlinternalFormatBasics.Format
              (CamlinternalFormatBasics.String_literal
                "The delegate consensus key is already used by another delegate"
                CamlinternalFormatBasics.End_of_format)
              "The delegate consensus key is already used by another delegate")))
    Data_encoding.empty
    (fun (function_parameter : Error_monad._error) ⇒
      match function_parameter with
      | Build_extensible tag _ payload ⇒
        if String.eqb tag "Invalid_consensus_key_update_active" then
          Some tt
        else None
      end)
    (fun (function_parameter : unit) ⇒
      let '_ := function_parameter in
      Build_extensible "Invalid_consensus_key_update_active" unit tt).

Definition pk : Set := Raw_context.consensus_pk.

Module t.
  Record record : Set := Build {
    delegate : Signature.public_key_hash;
    consensus_pkh : Signature.public_key_hash;
  }.
  Definition with_delegate delegate (r : record) :=
    Build delegate r.(consensus_pkh).
  Definition with_consensus_pkh consensus_pkh (r : record) :=
    Build r.(delegate) consensus_pkh.
End t.
Definition t := t.record.

Definition pkh (function_parameter : pk) : t :=
  let '{|
    Raw_context.consensus_pk.delegate := delegate;
      Raw_context.consensus_pk.consensus_pk := _;
      Raw_context.consensus_pk.consensus_pkh := consensus_pkh
      |} := function_parameter in
  {| t.delegate := delegate; t.consensus_pkh := consensus_pkh; |}.

Definition zero : t :=
  {| t.delegate := Signature.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.zero);
    t.consensus_pkh :=
      Signature.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.zero); |}.

Definition pp (ppf : Format.formatter) (function_parameter : t) : unit :=
  let '{| t.delegate := delegate; t.consensus_pkh := consensus_pkh |} :=
    function_parameter in
  let '_ :=
    Format.fprintf ppf
      (CamlinternalFormatBasics.Format
        (CamlinternalFormatBasics.Formatting_gen
          (CamlinternalFormatBasics.Open_box
            (CamlinternalFormatBasics.Format
              (CamlinternalFormatBasics.String_literal "<v 2>"
                CamlinternalFormatBasics.End_of_format) "<v 2>"))
          (CamlinternalFormatBasics.Alpha CamlinternalFormatBasics.End_of_format))
        "@[<v 2>%a") Signature.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.pp)
      delegate in
  let '_ :=
    if
      Pervasives.not
        (Signature.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.equal)
          delegate consensus_pkh)
    then
      Format.fprintf ppf
        (CamlinternalFormatBasics.Format
          (CamlinternalFormatBasics.Formatting_lit
            (CamlinternalFormatBasics.Break "@," 0 0)
            (CamlinternalFormatBasics.String_literal "Active key: "
              (CamlinternalFormatBasics.Alpha
                CamlinternalFormatBasics.End_of_format))) "@,Active key: %a")
        Signature.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.pp) consensus_pkh
    else
      tt in
  Format.fprintf ppf
    (CamlinternalFormatBasics.Format
      (CamlinternalFormatBasics.Formatting_lit
        CamlinternalFormatBasics.Close_box
        CamlinternalFormatBasics.End_of_format) "@]").

Definition check_unused (ctxt : Raw_context.t) (pkh : Signature.public_key_hash)
  : M? unit :=
  let is_active :=
    Storage.Consensus_keys.(Storage_sigs.Data_set_storage.mem) ctxt pkh in
  Error_monad.fail_when is_active
    (Build_extensible "Invalid_consensus_key_update_active" unit tt).

Definition set_unused
  : Raw_context.t → Signature.public_key_hash → Raw_context.t :=
  Storage.Consensus_keys.(Storage_sigs.Data_set_storage.remove).

Definition set_used
  : Raw_context.t → Signature.public_key_hash → Raw_context.t :=
  Storage.Consensus_keys.(Storage_sigs.Data_set_storage.add).

Definition init_value
  (ctxt : Raw_context.t) (delegate : Signature.public_key_hash)
  (pk : Signature.public_key) : M? Raw_context.t :=
  let pkh := Signature.Public_key.(S.SIGNATURE_PUBLIC_KEY.hash_value) pk in
  let? '_ := check_unused ctxt pkh in
  let ctxt := set_used ctxt pkh in
  Storage.Contract.Consensus_key.(Storage_sigs.Indexed_data_storage.init_value)
    ctxt (Contract_repr.Implicit delegate) pk.

Definition active_pubkey
  (ctxt : Raw_context.t) (delegate : Signature.public_key_hash) : M? pk :=
  let? pk :=
    Storage.Contract.Consensus_key.(Storage_sigs.Indexed_data_storage.get) ctxt
      (Contract_repr.Implicit delegate) in
  let pkh := Signature.Public_key.(S.SIGNATURE_PUBLIC_KEY.hash_value) pk in
  return?
    {| Raw_context.consensus_pk.delegate := delegate;
      Raw_context.consensus_pk.consensus_pk := pk;
      Raw_context.consensus_pk.consensus_pkh := pkh; |}.

Definition active_key
  (ctxt : Raw_context.t) (delegate : Signature.public_key_hash) : M? t :=
  let? pk := active_pubkey ctxt delegate in
  return? (pkh pk).

Definition raw_pending_updates
  (ctxt : Raw_context.t) (delegate : Signature.public_key_hash)
  : M? (list (Cycle_repr.t × Signature.public_key)) :=
  Storage.Contract.Pending_consensus_keys.(Storage_sigs.Indexed_data_storage.bindings)
    (ctxt, (Contract_repr.Implicit delegate)).

Definition pending_updates
  (ctxt : Raw_context.t) (delegate : Signature.public_key_hash)
  : M? (list (Cycle_repr.t × Signature.public_key_hash)) :=
  let? updates := raw_pending_updates ctxt delegate in
  let updates :=
    List.sort
      (fun (function_parameter : Cycle_repr.t × Signature.public_key) ⇒
        let '(c1, _) := function_parameter in
        fun (function_parameter : Cycle_repr.t × Signature.public_key) ⇒
          let '(c2, _) := function_parameter in
          Cycle_repr.compare c1 c2) updates in
  return?
    (List.map
      (fun (function_parameter : Cycle_repr.t × Signature.public_key) ⇒
        let '(c_value, pk) := function_parameter in
        (c_value, (Signature.Public_key.(S.SIGNATURE_PUBLIC_KEY.hash_value) pk)))
      updates).

Definition raw_active_pubkey_for_cycle
  (ctxt : Raw_context.t) (delegate : Signature.public_key_hash)
  (cycle : Cycle_repr.t) : M? (Cycle_repr.t × Signature.public_key) :=
  let? pendings := raw_pending_updates ctxt delegate in
  let? active := active_pubkey ctxt delegate in
  let current_level := Raw_context.current_level ctxt in
  let active_for_cycle :=
    List.fold_left
      (fun (function_parameter : Cycle_repr.t × Signature.public_key) ⇒
        let '(c1, active) := function_parameter in
        fun (function_parameter : Cycle_repr.t × Signature.public_key) ⇒
          let '(c2, pk) := function_parameter in
          if (Cycle_repr.op_lt c1 c2) && (Cycle_repr.op_lteq c2 cycle) then
            (c2, pk)
          else
            (c1, active))
      (current_level.(Level_repr.t.cycle),
        active.(Raw_context.consensus_pk.consensus_pk)) pendings in
  return? active_for_cycle.

Definition active_pubkey_for_cycle
  (ctxt : Raw_context.t) (delegate : Signature.public_key_hash)
  (cycle : Cycle_repr.t) : M? pk :=
  let? '(_, consensus_pk) := raw_active_pubkey_for_cycle ctxt delegate cycle in
  return?
    {| Raw_context.consensus_pk.delegate := delegate;
      Raw_context.consensus_pk.consensus_pk := consensus_pk;
      Raw_context.consensus_pk.consensus_pkh :=
        Signature.Public_key.(S.SIGNATURE_PUBLIC_KEY.hash_value) consensus_pk;
      |}.

Definition register_update
  (ctxt : Raw_context.t) (delegate : Signature.public_key_hash)
  (pk : Signature.public_key) : M? Raw_context.t :=
  let? update_cycle :=
    let current_level := Raw_context.current_level ctxt in
    let preserved_cycles := Constants_storage.preserved_cycles ctxt in
    Cycle_repr.add current_level.(Level_repr.t.cycle) (preserved_cycles +i 1) in
  let? '_ :=
    let? '(first_active_cycle, active_pubkey) :=
      raw_active_pubkey_for_cycle ctxt delegate update_cycle in
    Error_monad.fail_when
      (Signature.Public_key.(S.SIGNATURE_PUBLIC_KEY.op_eq) pk active_pubkey)
      (Build_extensible "Invalid_consensus_key_update_noop" Cycle_repr.t
        first_active_cycle) in
  let pkh := Signature.Public_key.(S.SIGNATURE_PUBLIC_KEY.hash_value) pk in
  let? '_ := check_unused ctxt pkh in
  let ctxt := set_used ctxt pkh in
  let? '{| Raw_context.consensus_pk.consensus_pkh := old_pkh |} :=
    active_pubkey_for_cycle ctxt delegate update_cycle in
  let ctxt := set_unused ctxt old_pkh in
  let ctxt :=
    Storage.Contract.Pending_consensus_keys.(Storage_sigs.Indexed_data_storage.add)
      (ctxt, (Contract_repr.Implicit delegate)) update_cycle pk in
  return? ctxt.

Definition activate (ctxt : Raw_context.t) (new_cycle : Cycle_repr.t)
  : M? Raw_context.t :=
  Storage.Delegates.(Storage_sigs.Data_set_storage.fold) ctxt
    (Variant.Build "Undefined" unit tt) ctxt
    (fun (delegate : Signature.public_key_hash) ⇒
      fun (ctxt : Raw_context.t) ⇒
        let delegate := Contract_repr.Implicit delegate in
        let? update :=
          Storage.Contract.Pending_consensus_keys.(Storage_sigs.Indexed_data_storage.find)
            (ctxt, delegate) new_cycle in
        match update with
        | None ⇒ return? ctxt
        | Some pk ⇒
          let ctxt :=
            Storage.Contract.Consensus_key.(Storage_sigs.Indexed_data_storage.add)
              ctxt delegate pk in
          let ctxt :=
            Storage.Contract.Pending_consensus_keys.(Storage_sigs.Indexed_data_storage.remove)
              (ctxt, delegate) new_cycle in
          return? ctxt
        end).