💎 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.Environment.V8.

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 :=
  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; |}) None
    (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.