Skip to main content

💎 Origination_nonce.v

Translated OCaml

See proofs, Gitlab , OCaml

File generated by coq-of-ocaml
Require Import CoqOfOCaml.CoqOfOCaml.
Require Import CoqOfOCaml.Settings.

Require Import TezosOfOCaml.Proto_alpha.Environment.

Module t.
  Record record : Set := Build {
    operation_hash : Operation_hash.t;
    origination_index : int32;
  }.
  Definition with_operation_hash operation_hash (r : record) :=
    Build operation_hash r.(origination_index).
  Definition with_origination_index origination_index (r : record) :=
    Build r.(operation_hash) origination_index.
End t.
Definition t := t.record.

Definition encoding : Data_encoding.encoding t :=
  (let arg :=
    Data_encoding.conv
      (fun (function_parameter : t) ⇒
        let '{|
          t.operation_hash := operation_hash;
            t.origination_index := origination_index
            |} := function_parameter in
        (operation_hash, origination_index))
      (fun (function_parameter : Operation_hash.t × int32) ⇒
        let '(operation_hash, origination_index) := function_parameter in
        {| t.operation_hash := operation_hash;
          t.origination_index := origination_index; |}) in
  fun (eta : Data_encoding.encoding (Operation_hash.t × int32)) ⇒ arg None eta)
    (Data_encoding.obj2
      (Data_encoding.req None None "operation" Operation_hash.encoding)
      (Data_encoding.dft None None "index" Data_encoding.int32_value 0)).

Definition initial (operation_hash : Operation_hash.t) : t :=
  {| t.operation_hash := operation_hash; t.origination_index := 0; |}.

Definition incr (nonce_value : t) : t :=
  let origination_index := Int32.succ nonce_value.(t.origination_index) in
  t.with_origination_index origination_index nonce_value.