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.t) ⇒
            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.t) ⇒
        Build_extensible "Unrevealed_manager_key" Contract_repr.t 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.t) ⇒
            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.t) ⇒
        Build_extensible "Previously_revealed_key" Contract_repr.t 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.t) ⇒
          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.t) ⇒
      Build_extensible "Missing_manager_contract" Contract_repr.t 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_with_local_context.init_value).

Definition is_manager_key_revealed
  (c_value : Raw_context.t) (manager : Signature.public_key_hash) : M? bool :=
  let contract := Contract_repr.Implicit manager in
  let? function_parameter :=
    Storage.Contract.Manager.(Storage_sigs.Indexed_data_storage_with_local_context.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 check_public_key
  (public_key : Signature.public_key)
  (expected_hash : Signature.public_key_hash) : M? unit :=
  let provided_hash :=
    Signature.Public_key.(S.SIGNATURE_PUBLIC_KEY.hash_value) public_key in
  Error_monad.error_unless
    (Signature.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.equal) provided_hash
      expected_hash)
    (Build_extensible "Inconsistent_hash" Inconsistent_hash
      {| Inconsistent_hash.public_key := public_key;
        Inconsistent_hash.expected_hash := expected_hash;
        Inconsistent_hash.provided_hash := provided_hash; |}).

Definition reveal_manager_key (op_staroptstar : option bool)
  : Raw_context.t Signature.public_key_hash Signature.public_key
  M? Raw_context.t :=
  let check_consistency :=
    match op_staroptstar with
    | Some op_starsthstarop_starsthstar
    | Nonetrue
    end in
  fun (c_value : Raw_context.t) ⇒
    fun (manager : Signature.public_key_hash) ⇒
      fun (public_key : Signature.public_key) ⇒
        let contract := Contract_repr.Implicit manager in
        let? function_parameter :=
          Storage.Contract.Manager.(Storage_sigs.Indexed_data_storage_with_local_context.get)
            c_value contract in
        match function_parameter with
        | Manager_repr.Public_key _
          Error_monad.tzfail
            (Build_extensible "Previously_revealed_key" Contract_repr.t contract)
        | Manager_repr.Hash expected_hash
          let? '_ :=
            Error_monad.error_unless
              (Signature.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.equal)
                manager expected_hash)
              (Build_extensible "Inconsistent_hash" Inconsistent_hash
                {| Inconsistent_hash.public_key := public_key;
                  Inconsistent_hash.expected_hash := expected_hash;
                  Inconsistent_hash.provided_hash := manager; |}) in
          let? '_ :=
            Error_monad.when_ check_consistency
              (fun (function_parameter : unit) ⇒
                let '_ := function_parameter in
                check_public_key public_key expected_hash) in
          let pk := Manager_repr.Public_key public_key in
          Storage.Contract.Manager.(Storage_sigs.Indexed_data_storage_with_local_context.update)
            c_value contract pk
        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 pkh in
  let? function_parameter :=
    Storage.Contract.Manager.(Storage_sigs.Indexed_data_storage_with_local_context.find)
      ctxt contract in
  match function_parameter with
  | None
    match error_value with
    | None
      Error_monad.tzfail
        (Build_extensible "Missing_manager_contract" Contract_repr.t contract)
    | Some error_valueError_monad.tzfail error_value
    end
  | Some (Manager_repr.Hash _) ⇒
    match error_value with
    | None
      Error_monad.tzfail
        (Build_extensible "Unrevealed_manager_key" Contract_repr.t contract)
    | Some error_valueError_monad.tzfail 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_with_local_context.remove_existing).