🖼️ Raw_context.v

Translated OCaml

See proofs, See simulations, Gitlab , OCaml

File generated by coq-of-ocaml

Init function; without side-effects in Coq

Init function; without side-effects in Coq

Definition init_module2 : unit :=
  let '_ :=
    Error_monad.register_error_kind Error_monad.Permanent
      "too_many_internal_operations" "Too many internal operations"
      "A transaction exceeded the hard limit of internal operations it can emit"
      None Data_encoding.empty
      (fun (function_parameter : Error_monad._error) ⇒
        match function_parameter with
        | Build_extensible tag _ payload ⇒
          if String.eqb tag "Too_many_internal_operations" then
            Some tt
          else None
        end)
      (fun (function_parameter : unit) ⇒
        let '_ := function_parameter in
        Build_extensible "Too_many_internal_operations" unit tt) in
  let '_ :=
    Error_monad.register_error_kind Error_monad.Temporary
      "gas_exhausted.operation" "Gas quota exceeded for the operation"
      "A script or one of its callee took more time than the operation said it would"
      None Data_encoding.empty
      (fun (function_parameter : Error_monad._error) ⇒
        match function_parameter with
        | Build_extensible tag _ payload ⇒
          if String.eqb tag "Operation_quota_exceeded" then
            Some tt
          else None
        end)
      (fun (function_parameter : unit) ⇒
        let '_ := function_parameter in
        Build_extensible "Operation_quota_exceeded" unit tt) in
  let '_ :=
    Error_monad.register_error_kind Error_monad.Temporary "gas_exhausted.block"
      "Gas quota exceeded for the block"
      "The sum of gas consumed by all the operations in the block exceeds the hard gas limit per block"
      None Data_encoding.empty
      (fun (function_parameter : Error_monad._error) ⇒
        match function_parameter with
        | Build_extensible tag _ payload ⇒
          if String.eqb tag "Block_quota_exceeded" then
            Some tt
          else None
        end)
      (fun (function_parameter : unit) ⇒
        let '_ := function_parameter in
        Build_extensible "Block_quota_exceeded" unit tt) in
  let '_ :=
    Error_monad.register_error_kind Error_monad.Permanent
      "delegate.stake_distribution_not_set" "Stake distribution not set"
      "The stake distribution for the current cycle is not set."
      (Some
        (fun (ppf : Format.formatter) ⇒
          fun (function_parameter : unit) ⇒
            let '_ := function_parameter in
            Format.fprintf ppf
              (CamlinternalFormatBasics.Format
                (CamlinternalFormatBasics.String_literal
                  "The stake distribution for the current cycle is not set."
                  CamlinternalFormatBasics.End_of_format)
                "The stake distribution for the current cycle is not set.")))
      Data_encoding.empty
      (fun (function_parameter : Error_monad._error) ⇒
        match function_parameter with
        | Build_extensible tag _ payload ⇒
          if String.eqb tag "Stake_distribution_not_set" then
            Some tt
          else None
        end)
      (fun (function_parameter : unit) ⇒
        let '_ := function_parameter in
        Build_extensible "Stake_distribution_not_set" unit tt) in
  Error_monad.register_error_kind Error_monad.Permanent "sampler_already_set"
    "Sampler already set"
    "Internal error: Raw_context.set_sampler_for_cycle was called twice for a given cycle"
    (Some
      (fun (ppf : Format.formatter) ⇒
        fun (c_value : Cycle_repr.cycle) ⇒
          Format.fprintf ppf
            (CamlinternalFormatBasics.Format
              (CamlinternalFormatBasics.String_literal
                "Internal error: sampler already set for cycle "
                (CamlinternalFormatBasics.Alpha
                  (CamlinternalFormatBasics.Char_literal "." % char
                    CamlinternalFormatBasics.End_of_format)))
              "Internal error: sampler already set for cycle %a.") Cycle_repr.pp
            c_value))
    (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 "Sampler_already_set" then
          let c_value := cast Cycle_repr.t payload in
          Some c_value
        else None
      end)
    (fun (c_value : Cycle_repr.cycle) ⇒
      Build_extensible "Sampler_already_set" Cycle_repr.cycle c_value).

Definition fresh_internal_nonce (ctxt : t) : M ? (t × int) :=
  if (internal_nonce ctxt ) ≥i 65535 then
    Error_monad.error_value
      (Build_extensible "Too_many_internal_operations" unit tt)
  else
    return ?
      ((update_internal_nonce ctxt ((internal_nonce ctxt ) +i 1)),
        (internal_nonce ctxt)).

Definition reset_internal_nonce (ctxt : t) : t :=
  let ctxt := update_internal_nonce ctxt 0 in
  update_internal_nonces_used ctxt Int_set.(_Set.S.empty).

Definition record_internal_nonce (ctxt : t) (k_value : Compare.Int.t) : t :=
  update_internal_nonces_used ctxt
    (Int_set.(_Set.S.add) k_value (internal_nonces_used ctxt)).

Definition internal_nonce_already_recorded (ctxt : t) (k_value : Compare.Int.t)
  : bool := Int_set.(_Set.S.mem) k_value (internal_nonces_used ctxt).

Definition get_collected_fees (ctxt : t) : Tez_repr.t := fees ctxt.

Definition credit_collected_fees_only_call_from_token
  (ctxt : t) (fees' : Tez_repr.t) : M ? t :=
  let previous := get_collected_fees ctxt in
  let ? fees := Tez_repr.op_plusquestion previous fees' in
  return ? (update_fees ctxt fees ).

Definition spend_collected_fees_only_call_from_token
  (ctxt : t) (fees' : Tez_repr.t) : M ? t :=
  let previous := get_collected_fees ctxt in
  let ? fees := Tez_repr.op_minusquestion previous fees' in
  return ? (update_fees ctxt fees ).

Init function; without side-effects in Coq

Definition init_module3 : unit :=
  Error_monad.register_error_kind Error_monad.Permanent
    "undefined_operation_nonce" "Ill timed access to the origination nonce"
    "An origination was attempted out of the scope of a manager operation" None
    Data_encoding.empty
    (fun (function_parameter : Error_monad._error) ⇒
      match function_parameter with
      | Build_extensible tag _ payload ⇒
        if String.eqb tag "Undefined_operation_nonce" then
          Some tt
        else None
      end)
    (fun (function_parameter : unit) ⇒
      let '_ := function_parameter in
      Build_extensible "Undefined_operation_nonce" unit tt).

Definition init_origination_nonce (ctxt : t) (operation_hash : Operation_hash.t)
  : t :=
  let origination_nonce := Some (Origination_nonce.initial operation_hash) in
  update_origination_nonce ctxt origination_nonce.

Definition increment_origination_nonce (ctxt : t)
  : M ? (t × Origination_nonce.t ) :=
  match origination_nonce ctxt with
  | None ⇒
    Error_monad.error_value
      (Build_extensible "Undefined_operation_nonce" unit tt)
  | Some cur_origination_nonce ⇒
    let origination_nonce := Some (Origination_nonce.incr cur_origination_nonce)
      in
    let ctxt := update_origination_nonce ctxt origination_nonce in
    return ? (ctxt, cur_origination_nonce)
  end.

Definition get_origination_nonce (ctxt : t) : M ? Origination_nonce.t :=
  match origination_nonce ctxt with
  | None ⇒
    Error_monad.error_value
      (Build_extensible "Undefined_operation_nonce" unit tt)
  | Some origination_nonce ⇒ return ? origination_nonce
  end.

Definition unset_origination_nonce (ctxt : t) : t :=
  update_origination_nonce ctxt None.

Definition gas_level (ctxt : t) : Gas_limit_repr.t :=
  if unlimited_operation_gas ctxt then
    Gas_limit_repr.Unaccounted
  else
    Gas_limit_repr.Limited
      {| Gas_limit_repr.t.Limited.remaining := remaining_operation_gas ctxt; |}.

Definition block_gas_level : t → Gas_limit_repr.Arith.fp :=
  remaining_block_gas.

Definition consume_gas_limit_in_block
  (ctxt : t) (gas_limit : Gas_limit_repr.Arith.t) : M ? t :=
  let ? '_ :=
    Gas_limit_repr.check_gas_limit
      (constants ctxt).(Constants_parametric_repr.t.hard_gas_limit_per_operation)
      gas_limit in
  let block_gas := block_gas_level ctxt in
  let limit := Gas_limit_repr.Arith.fp_value gas_limit in
  if Gas_limit_repr.Arith.op_gt limit block_gas then
    Error_monad.error_value (Build_extensible "Block_quota_exceeded" unit tt)
  else
    let level := Gas_limit_repr.Arith.sub (block_gas_level ctxt) limit in
    let ctxt := update_remaining_block_gas ctxt level in
    Pervasives.Ok ctxt.

Definition set_gas_limit (ctxt : t) (remaining : Gas_limit_repr.Arith.t) : t :=
  let remaining_operation_gas := Gas_limit_repr.Arith.fp_value remaining in
  let ctxt := update_unlimited_operation_gas ctxt false in
  t.with_remaining_operation_gas remaining_operation_gas ctxt.

Definition set_gas_unlimited (ctxt : t) : t :=
  update_unlimited_operation_gas ctxt true.

Definition consume_gas (ctxt : t) (cost : Gas_limit_repr.cost) : M ? t :=
  match Gas_limit_repr.raw_consume (remaining_operation_gas ctxt) cost with
  | Some gas_counter ⇒
    Pervasives.Ok (update_remaining_operation_gas ctxt gas_counter)
  | None ⇒
    if unlimited_operation_gas ctxt then
      return ? ctxt
    else
      Error_monad.error_value
        (Build_extensible "Operation_quota_exceeded" unit tt)
  end.

Definition check_enough_gas (ctxt : t) (cost : Gas_limit_repr.cost) : M ? unit :=
  let ? function_parameter := consume_gas ctxt cost in
  let '_ := function_parameter in
  Result.return_unit.

Definition gas_consumed (since : t) (until : t) : Gas_limit_repr.Arith.t :=
  match ((gas_level since), (gas_level until)) with
  |
    (Gas_limit_repr.Limited {| Gas_limit_repr.t.Limited.remaining := before |},
      Gas_limit_repr.Limited {| Gas_limit_repr.t.Limited.remaining := after |})
    ⇒ Gas_limit_repr.Arith.sub before after
  | (_, _) ⇒ Gas_limit_repr.Arith.zero
  end.

Inductive missing_key_kind : Set :=
| Get : missing_key_kind
| _Set : missing_key_kind
| Del : missing_key_kind
| Copy : missing_key_kind.

Inductive storage_error : Set :=
| Incompatible_protocol_version : string → storage_error
| Missing_key : list string → missing_key_kind → storage_error
| Existing_key : list string → storage_error
| Corrupted_data : list string → storage_error.

Definition storage_error_encoding : Data_encoding.encoding storage_error :=
  Data_encoding.union None
    [
      Data_encoding.case_value "Incompatible_protocol_version" None
        (Data_encoding.Tag 0)
        (Data_encoding.obj1
          (Data_encoding.req None None "incompatible_protocol_version"
            Data_encoding.string_value))
        (fun (function_parameter : storage_error) ⇒
          match function_parameter with
          | Incompatible_protocol_version arg ⇒ Some arg
          | _ ⇒ None
          end) (fun (arg : string) ⇒ Incompatible_protocol_version arg);
      Data_encoding.case_value "Missing_key" None (Data_encoding.Tag 1)
        (Data_encoding.obj2
          (Data_encoding.req None None "missing_key"
            (Data_encoding.list_value None Data_encoding.string_value))
          (Data_encoding.req None None "function"
            (Data_encoding.string_enum
              [
                ("get", Get);
                ("set", _Set);
                ("del", Del);
                ("copy", Copy)
              ])))
        (fun (function_parameter : storage_error) ⇒
          match function_parameter with
          | Missing_key key_value f_value ⇒ Some (key_value, f_value)
          | _ ⇒ None
          end)
        (fun (function_parameter : list string × missing_key_kind) ⇒
          let '(key_value, f_value) := function_parameter in
          Missing_key key_value f_value);
      Data_encoding.case_value "Existing_key" None (Data_encoding.Tag 2)
        (Data_encoding.obj1
          (Data_encoding.req None None "existing_key"
            (Data_encoding.list_value None Data_encoding.string_value)))
        (fun (function_parameter : storage_error) ⇒
          match function_parameter with
          | Existing_key key_value ⇒ Some key_value
          | _ ⇒ None
          end) (fun (key_value : list string) ⇒ Existing_key key_value);
      Data_encoding.case_value "Corrupted_data" None (Data_encoding.Tag 3)
        (Data_encoding.obj1
          (Data_encoding.req None None "corrupted_data"
            (Data_encoding.list_value None Data_encoding.string_value)))
        (fun (function_parameter : storage_error) ⇒
          match function_parameter with
          | Corrupted_data key_value ⇒ Some key_value
          | _ ⇒ None
          end) (fun (key_value : list string) ⇒ Corrupted_data key_value)
    ].

Definition pp_storage_error
  (ppf : Format.formatter) (function_parameter : storage_error) : unit :=
  match function_parameter with
  | Incompatible_protocol_version version ⇒
    Format.fprintf ppf
      (CamlinternalFormatBasics.Format
        (CamlinternalFormatBasics.String_literal
          "Found a context with an unexpected version '"
          (CamlinternalFormatBasics.String CamlinternalFormatBasics.No_padding
            (CamlinternalFormatBasics.String_literal "'."
              CamlinternalFormatBasics.End_of_format)))
        "Found a context with an unexpected version '%s'.") version
  | Missing_key key_value Get ⇒
    Format.fprintf ppf
      (CamlinternalFormatBasics.Format
        (CamlinternalFormatBasics.String_literal "Missing key '"
          (CamlinternalFormatBasics.String CamlinternalFormatBasics.No_padding
            (CamlinternalFormatBasics.String_literal "'."
              CamlinternalFormatBasics.End_of_format))) "Missing key '%s'.")
      (String.concat "/" key_value)
  | Missing_key key_value _Set ⇒
    Format.fprintf ppf
      (CamlinternalFormatBasics.Format
        (CamlinternalFormatBasics.String_literal "Cannot set undefined key '"
          (CamlinternalFormatBasics.String CamlinternalFormatBasics.No_padding
            (CamlinternalFormatBasics.String_literal "'."
              CamlinternalFormatBasics.End_of_format)))
        "Cannot set undefined key '%s'.") (String.concat "/" key_value)
  | Missing_key key_value Del ⇒
    Format.fprintf ppf
      (CamlinternalFormatBasics.Format
        (CamlinternalFormatBasics.String_literal "Cannot delete undefined key '"
          (CamlinternalFormatBasics.String CamlinternalFormatBasics.No_padding
            (CamlinternalFormatBasics.String_literal "'."
              CamlinternalFormatBasics.End_of_format)))
        "Cannot delete undefined key '%s'.") (String.concat "/" key_value)
  | Missing_key key_value Copy ⇒
    Format.fprintf ppf
      (CamlinternalFormatBasics.Format
        (CamlinternalFormatBasics.String_literal "Cannot copy undefined key '"
          (CamlinternalFormatBasics.String CamlinternalFormatBasics.No_padding
            (CamlinternalFormatBasics.String_literal "'."
              CamlinternalFormatBasics.End_of_format)))
        "Cannot copy undefined key '%s'.") (String.concat "/" key_value)
  | Existing_key key_value ⇒
    Format.fprintf ppf
      (CamlinternalFormatBasics.Format
        (CamlinternalFormatBasics.String_literal
          "Cannot initialize defined key '"
          (CamlinternalFormatBasics.String CamlinternalFormatBasics.No_padding
            (CamlinternalFormatBasics.String_literal "'."
              CamlinternalFormatBasics.End_of_format)))
        "Cannot initialize defined key '%s'.") (String.concat "/" key_value)
  | Corrupted_data key_value ⇒
    Format.fprintf ppf
      (CamlinternalFormatBasics.Format
        (CamlinternalFormatBasics.String_literal "Failed to parse the data at '"
          (CamlinternalFormatBasics.String CamlinternalFormatBasics.No_padding
            (CamlinternalFormatBasics.String_literal "'."
              CamlinternalFormatBasics.End_of_format)))
        "Failed to parse the data at '%s'.") (String.concat "/" key_value)
  end.

Init function; without side-effects in Coq

Definition init_module4 : unit :=
  Error_monad.register_error_kind Error_monad.Permanent "context.storage_error"
    "Storage error (fatal internal error)"
    "An error that should never happen unless something has been deleted or corrupted in the database."
    (Some
      (fun (ppf : Format.formatter) ⇒
        fun (err : storage_error) ⇒
          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.String_literal "Storage error:"
                  (CamlinternalFormatBasics.Formatting_lit
                    (CamlinternalFormatBasics.Break "@ " 1 0)
                    (CamlinternalFormatBasics.Alpha
                      (CamlinternalFormatBasics.Formatting_lit
                        CamlinternalFormatBasics.Close_box
                        CamlinternalFormatBasics.End_of_format)))))
              "@[<v 2>Storage error:@ %a@]") pp_storage_error err))
    storage_error_encoding
    (fun (function_parameter : Error_monad._error) ⇒
      match function_parameter with
      | Build_extensible tag _ payload ⇒
        if String.eqb tag "Storage_error" then
          let err := cast storage_error payload in
          Some err
        else None
      end)
    (fun (err : storage_error) ⇒
      Build_extensible "Storage_error" storage_error err).

Definition storage_error_value {A : Set} (err : storage_error) : M ? A :=
  Error_monad.error_value (Build_extensible "Storage_error" storage_error err).

Definition version_key : list string := [ "version" ].

Definition version_value : string := "alpha_current".

Definition version : string := "v1".

Definition cycle_eras_key : list string := [ version; "cycle_eras" ].

Definition constants_key : list string := [ version; "constants" ].

Definition protocol_param_key : list string := [ "protocol_parameters" ].

Definition get_cycle_eras (ctxt : Context.t) : M ? Level_repr.cycle_eras :=
  let function_parameter := Context.find ctxt cycle_eras_key in
  match function_parameter with
  | None ⇒ storage_error_value (Missing_key cycle_eras_key Get)
  | Some bytes_value ⇒
    match
      Data_encoding.Binary.of_bytes_opt Level_repr.cycle_eras_encoding
        bytes_value with
    | None ⇒ storage_error_value (Corrupted_data cycle_eras_key)
    | Some cycle_eras ⇒ return ? cycle_eras
    end
  end.

Definition set_cycle_eras {A : Set}
  (ctxt : Context.t) (cycle_eras : Level_repr.cycle_eras)
  : Pervasives.result Context.t A :=
  let bytes_value :=
    Data_encoding.Binary.to_bytes_exn None Level_repr.cycle_eras_encoding
      cycle_eras in
  Error_monad.op_gtpipeeq (Context.add ctxt cycle_eras_key bytes_value)
    Error_monad.ok.

Init function; without side-effects in Coq

Inclusion of the module [Context.Tree]

Init function; without side-effects in Coq

Explicit module to present this file as a record in Coq and reduce the size of the generated Coq code.