Skip to main content

✒️ Contract_manager_storage.v

Translated OCaml

See proofs, Gitlab , OCaml

File generated by coq-of-ocaml
Init function; without side-effects in Coq
Definition init_module : unit :=
  let '_ :=
    Error_monad.register_error_kind Error_monad.Branch "contract.unrevealed_key"
      "Manager operation precedes key revelation"
      "One tried to apply a manager operation without revealing the manager public key"
      (Some
        (fun (ppf : Format.formatter) ⇒
          fun (s_value : Contract_repr.contract) ⇒
            Format.fprintf ppf
              (CamlinternalFormatBasics.Format
                (CamlinternalFormatBasics.String_literal
                  "Unrevealed manager key for contract "
                  (CamlinternalFormatBasics.Alpha
                    (CamlinternalFormatBasics.Char_literal "." % char
                      CamlinternalFormatBasics.End_of_format)))
                "Unrevealed manager key for contract %a.") Contract_repr.pp
              s_value))
      (Data_encoding.obj1
        (Data_encoding.req None None "contract" Contract_repr.encoding))
      (fun (function_parameter : Error_monad._error) ⇒
        match function_parameter with
        | Build_extensible tag _ payload
          if String.eqb tag "Unrevealed_manager_key" then
            let s_value := cast Contract_repr.t payload in
            Some s_value
          else None
        end)
      (fun (s_value : Contract_repr.contract) ⇒
        Build_extensible "Unrevealed_manager_key" Contract_repr.contract s_value)
    in
  let '_ :=
    Error_monad.register_error_kind Error_monad.Permanent
      "contract.manager.inconsistent_hash" "Inconsistent public key hash"
      "A revealed manager public key is inconsistent with the announced hash"
      (Some
        (fun (ppf : Format.formatter) ⇒
          fun (function_parameter :
            Signature.public_key × Signature.public_key_hash ×
              Signature.public_key_hash) ⇒
            let '(k_value, eh, ph) := function_parameter in
            Format.fprintf ppf
              (CamlinternalFormatBasics.Format
                (CamlinternalFormatBasics.String_literal
                  "The hash of the manager public key "
                  (CamlinternalFormatBasics.String
                    CamlinternalFormatBasics.No_padding
                    (CamlinternalFormatBasics.String_literal " is not "
                      (CamlinternalFormatBasics.Alpha
                        (CamlinternalFormatBasics.String_literal
                          " as announced but "
                          (CamlinternalFormatBasics.Alpha
                            CamlinternalFormatBasics.End_of_format))))))
                "The hash of the manager public key %s is not %a as announced but %a")
              (Signature.Public_key.(S.SIGNATURE_PUBLIC_KEY.to_b58check) k_value)
              Signature.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.pp) ph
              Signature.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.pp) eh))
      (Data_encoding.obj3
        (Data_encoding.req None None "public_key"
          Signature.Public_key.(S.SIGNATURE_PUBLIC_KEY.encoding))
        (Data_encoding.req None None "expected_hash"
          Signature.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.encoding))
        (Data_encoding.req None None "provided_hash"
          Signature.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.encoding)))
      (fun (function_parameter : Error_monad._error) ⇒
        match function_parameter with
        | Build_extensible tag _ payload
          if String.eqb tag "Inconsistent_hash" then
            let '{|
              Inconsistent_hash.public_key := public_key;
                Inconsistent_hash.expected_hash := expected_hash;
                Inconsistent_hash.provided_hash := provided_hash
                |} := cast Inconsistent_hash payload in
            Some (public_key, expected_hash, provided_hash)
          else None
        end)
      (fun (function_parameter :
        Signature.public_key × Signature.public_key_hash ×
          Signature.public_key_hash) ⇒
        let '(public_key, expected_hash, provided_hash) := function_parameter in
        Build_extensible "Inconsistent_hash" Inconsistent_hash
          {| Inconsistent_hash.public_key := public_key;
            Inconsistent_hash.expected_hash := expected_hash;
            Inconsistent_hash.provided_hash := provided_hash; |}) in
  let '_ :=
    Error_monad.register_error_kind Error_monad.Branch
      "contract.previously_revealed_key" "Manager operation already revealed"
      "One tried to reveal twice a manager public key"
      (Some
        (fun (ppf : Format.formatter) ⇒
          fun (s_value : Contract_repr.contract) ⇒
            Format.fprintf ppf
              (CamlinternalFormatBasics.Format
                (CamlinternalFormatBasics.String_literal
                  "Previously revealed manager key for contract "
                  (CamlinternalFormatBasics.Alpha
                    (CamlinternalFormatBasics.Char_literal "." % char
                      CamlinternalFormatBasics.End_of_format)))
                "Previously revealed manager key for contract %a.")
              Contract_repr.pp s_value))
      (Data_encoding.obj1
        (Data_encoding.req None None "contract" Contract_repr.encoding))
      (fun (function_parameter : Error_monad._error) ⇒
        match function_parameter with
        | Build_extensible tag _ payload
          if String.eqb tag "Previously_revealed_key" then
            let s_value := cast Contract_repr.t payload in
            Some s_value
          else None
        end)
      (fun (s_value : Contract_repr.contract) ⇒
        Build_extensible "Previously_revealed_key" Contract_repr.contract
          s_value) in
  Error_monad.register_error_kind Error_monad.Branch
    "contract.missing_manager_contract" "Missing manager contract"
    "The manager contract is missing from the storage"
    (Some
      (fun (ppf : Format.formatter) ⇒
        fun (s_value : Contract_repr.contract) ⇒
          Format.fprintf ppf
            (CamlinternalFormatBasics.Format
              (CamlinternalFormatBasics.String_literal "The contract "
                (CamlinternalFormatBasics.Alpha
                  (CamlinternalFormatBasics.String_literal
                    " is missing from the storage."
                    CamlinternalFormatBasics.End_of_format)))
              "The contract %a is missing from the storage.") Contract_repr.pp
            s_value))
    (Data_encoding.obj1
      (Data_encoding.req None None "contract" Contract_repr.encoding))
    (fun (function_parameter : Error_monad._error) ⇒
      match function_parameter with
      | Build_extensible tag _ payload
        if String.eqb tag "Missing_manager_contract" then
          let s_value := cast Contract_repr.t payload in
          Some s_value
        else None
      end)
    (fun (s_value : Contract_repr.contract) ⇒
      Build_extensible "Missing_manager_contract" Contract_repr.contract s_value).

Definition init_value
  : Raw_context.t Contract_repr.t Manager_repr.manager_key
  M? Raw_context.t :=
  Storage.Contract.Manager.(Storage_sigs.Indexed_data_storage.init_value).

Definition is_manager_key_revealed
  (c_value : Raw_context.t) (manager : Signature.public_key_hash) : M? bool :=
  let contract := Contract_repr.implicit_contract manager in
  let? function_parameter :=
    Storage.Contract.Manager.(Storage_sigs.Indexed_data_storage.find) c_value
      contract in
  match function_parameter with
  | NoneError_monad.return_false
  | Some (Manager_repr.Hash _) ⇒ Error_monad.return_false
  | Some (Manager_repr.Public_key _) ⇒ Error_monad.return_true
  end.

Definition reveal_manager_key
  (c_value : Raw_context.t) (manager : Signature.public_key_hash)
  (public_key : Signature.public_key) : M? Raw_context.t :=
  let contract := Contract_repr.implicit_contract manager in
  let? function_parameter :=
    Storage.Contract.Manager.(Storage_sigs.Indexed_data_storage.get) c_value
      contract in
  match function_parameter with
  | Manager_repr.Public_key _
    Error_monad.fail
      (Build_extensible "Previously_revealed_key" Contract_repr.contract
        contract)
  | Manager_repr.Hash v_value
    let actual_hash :=
      Signature.Public_key.(S.SIGNATURE_PUBLIC_KEY.hash_value) public_key in
    if
      Signature.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.equal) actual_hash
        v_value
    then
      let v_value := Manager_repr.Public_key public_key in
      Storage.Contract.Manager.(Storage_sigs.Indexed_data_storage.update)
        c_value contract v_value
    else
      Error_monad.fail
        (Build_extensible "Inconsistent_hash" Inconsistent_hash
          {| Inconsistent_hash.public_key := public_key;
            Inconsistent_hash.expected_hash := v_value;
            Inconsistent_hash.provided_hash := actual_hash; |})
  end.

Definition get_manager_key
  (error_value : option Error_monad._error) (ctxt : Raw_context.t)
  (pkh : Signature.public_key_hash) : M? Signature.public_key :=
  let contract := Contract_repr.implicit_contract pkh in
  let? function_parameter :=
    Storage.Contract.Manager.(Storage_sigs.Indexed_data_storage.find) ctxt
      contract in
  match function_parameter with
  | None
    match error_value with
    | None
      Error_monad.fail
        (Build_extensible "Missing_manager_contract" Contract_repr.contract
          contract)
    | Some error_valueError_monad.fail error_value
    end
  | Some (Manager_repr.Hash _) ⇒
    match error_value with
    | None
      Error_monad.fail
        (Build_extensible "Unrevealed_manager_key" Contract_repr.contract
          contract)
    | Some error_valueError_monad.fail error_value
    end
  | Some (Manager_repr.Public_key pk) ⇒ return? pk
  end.

Definition remove_existing
  : Raw_context.t Contract_repr.t M? Raw_context.t :=
  Storage.Contract.Manager.(Storage_sigs.Indexed_data_storage.remove_existing).