🐆 Tx_rollup_l2_context.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.
Require TezosOfOCaml.Proto_alpha.Alpha_context.
Require TezosOfOCaml.Proto_alpha.Indexable.
Require TezosOfOCaml.Proto_alpha.Tx_rollup_l2_address.
Require TezosOfOCaml.Proto_alpha.Tx_rollup_l2_context_sig.
Require TezosOfOCaml.Proto_alpha.Tx_rollup_l2_qty.
Require TezosOfOCaml.Proto_alpha.Tx_rollup_l2_storage_sig.

Definition metadata_encoding
  : Data_encoding.encoding Tx_rollup_l2_context_sig.metadata :=
  Data_encoding.conv
    (fun (function_parameter : Tx_rollup_l2_context_sig.metadata) ⇒
      let '{|
        Tx_rollup_l2_context_sig.metadata.counter := counter;
          Tx_rollup_l2_context_sig.metadata.public_key := public_key
          |} := function_parameter in
      (counter, public_key))
    (fun (function_parameter :
      int64 × Bls.Public_key.(S.SIGNATURE_PUBLIC_KEY.t)) ⇒
      let '(counter, public_key) := function_parameter in
      {| Tx_rollup_l2_context_sig.metadata.counter := counter;
        Tx_rollup_l2_context_sig.metadata.public_key := public_key; |}) None
    (Data_encoding.obj2
      (Data_encoding.req None None "counter" Data_encoding.int64_value)
      (Data_encoding.req None None "public_key"
        Bls.Public_key.(S.SIGNATURE_PUBLIC_KEY.encoding))).

A value of type ['a key] identifies a value of type ['a] in an underlying, untyped storage.

This GADT is used to enforce type-safety of the abstraction of the transactions rollup context. For this abstraction to work, it is necessary to ensure that the serialization of values ['a key] and ['b key] cannot collide. To that end, we use [Data_encoding] (see {!packed_key_encoding}).

Inductive key : Set :=
| Address_metadata : Tx_rollup_l2_context_sig.address_index → key
| Address_count : key
| Address_index : Tx_rollup_l2_address.t → key
| Ticket_count : key
| Ticket_index : Alpha_context.Ticket_hash.t → key
| Ticket_ledger :
  Tx_rollup_l2_context_sig.ticket_index →
  Tx_rollup_l2_context_sig.address_index → key.

A monomorphic version of {!Key}, used for serialization purposes.

Inductive packed_key : Set :=
| Key : key → packed_key.

The encoding used to serialize keys to be used with an untyped storage.

Definition packed_key_encoding : Data_encoding.t packed_key :=
  Data_encoding.union (Some (Variant.Build "Uint8" unit tt))
    [
      Data_encoding.case_value "Address_metadata" None (Data_encoding.Tag 0)
        Tx_rollup_l2_address.Indexable.index_encoding
        (fun (function_parameter : packed_key) ⇒
          match function_parameter with
          | Key (Address_metadata idx) ⇒ Some idx
          | _ ⇒ None
          end)
        (fun (idx : Tx_rollup_l2_address.Indexable.index) ⇒
          Key (Address_metadata idx));
      Data_encoding.case_value "Address_count" None (Data_encoding.Tag 1)
        Data_encoding.empty
        (fun (function_parameter : packed_key) ⇒
          match function_parameter with
          | Key Address_count ⇒ Some tt
          | _ ⇒ None
          end)
        (fun (function_parameter : unit) ⇒
          let '_ := function_parameter in
          Key Address_count);
      Data_encoding.case_value "Address_index" None (Data_encoding.Tag 2)
        Tx_rollup_l2_address.encoding
        (fun (function_parameter : packed_key) ⇒
          match function_parameter with
          | Key (Address_index addr) ⇒ Some addr
          | _ ⇒ None
          end)
        (fun (addr : Tx_rollup_l2_address.t) ⇒ Key (Address_index addr));
      Data_encoding.case_value "Ticket_count" None (Data_encoding.Tag 3)
        Data_encoding.empty
        (fun (function_parameter : packed_key) ⇒
          match function_parameter with
          | Key Ticket_count ⇒ Some tt
          | _ ⇒ None
          end)
        (fun (function_parameter : unit) ⇒
          let '_ := function_parameter in
          Key Ticket_count);
      Data_encoding.case_value "Ticket_index" None (Data_encoding.Tag 4)
        Alpha_context.Ticket_hash.encoding
        (fun (function_parameter : packed_key) ⇒
          match function_parameter with
          | Key (Ticket_index ticket) ⇒ Some ticket
          | _ ⇒ None
          end)
        (fun (ticket : Alpha_context.Ticket_hash.t) ⇒
          Key (Ticket_index ticket));
      Data_encoding.case_value "Ticket_ledger" None (Data_encoding.Tag 5)
        (Data_encoding.tup2
          Tx_rollup_l2_context_sig.Ticket_indexable.(Indexable.INDEXABLE.index_encoding)
          Tx_rollup_l2_address.Indexable.index_encoding)
        (fun (function_parameter : packed_key) ⇒
          match function_parameter with
          | Key (Ticket_ledger ticket address) ⇒ Some (ticket, address)
          | _ ⇒ None
          end)
        (fun (function_parameter :
          Tx_rollup_l2_context_sig.Ticket_indexable.(Indexable.INDEXABLE.index)
            × Tx_rollup_l2_address.Indexable.index) ⇒
          let '(ticket, address) := function_parameter in
          Key (Ticket_ledger ticket address))
    ].

[value_encoding key] returns the encoding to be used to serialize and deserialize values associated to a [key] from and to the underlying storage.

Definition value_encoding {a : Set} (function_parameter : key)
  : Data_encoding.t a :=
  match function_parameter with
  | Address_metadata _ ⇒ cast (Data_encoding.t a) metadata_encoding
  | Address_count ⇒ cast (Data_encoding.t a) Data_encoding.int32_value
  | Address_index _ ⇒
    cast (Data_encoding.t a) Tx_rollup_l2_address.Indexable.index_encoding
  | Ticket_count ⇒ cast (Data_encoding.t a) Data_encoding.int32_value
  | Ticket_index _ ⇒
    cast (Data_encoding.t a)
    Tx_rollup_l2_context_sig.Ticket_indexable.(Indexable.INDEXABLE.index_encoding)
  | Ticket_ledger _ _ ⇒ cast (Data_encoding.t a) Tx_rollup_l2_qty.encoding
  end.

Init function; without side-effects in Coq

Definition init_module1 : unit :=
  let '_ :=
    Error_monad.register_error_kind Error_monad.Permanent
      "tx_rollup_key_cannot_be_serialized" "Key cannot be serialized"
      "Tried to serialize an invalid key." None Data_encoding.empty
      (fun (function_parameter : Error_monad._error) ⇒
        match function_parameter with
        | Build_extensible tag _ payload ⇒
          if String.eqb tag "Key_cannot_be_serialized" then
            Some tt
          else None
        end)
      (fun (function_parameter : unit) ⇒
        let '_ := function_parameter in
        Build_extensible "Key_cannot_be_serialized" unit tt) in
  let '_ :=
    Error_monad.register_error_kind Error_monad.Permanent
      "tx_rollup_value_cannot_be_serialized" "Value cannot be serialized"
      "Tried to serialize an invalid value." None Data_encoding.empty
      (fun (function_parameter : Error_monad._error) ⇒
        match function_parameter with
        | Build_extensible tag _ payload ⇒
          if String.eqb tag "Value_cannot_be_serialized" then
            Some tt
          else None
        end)
      (fun (function_parameter : unit) ⇒
        let '_ := function_parameter in
        Build_extensible "Value_cannot_be_serialized" unit tt) in
  Error_monad.register_error_kind Error_monad.Permanent
    "tx_rollup_value_cannot_be_deserialized" "Value cannot be deserialized"
    "A value has been serialized in the Tx_rollup store, but cannot be deserialized."
    None Data_encoding.empty
    (fun (function_parameter : Error_monad._error) ⇒
      match function_parameter with
      | Build_extensible tag _ payload ⇒
        if String.eqb tag "Value_cannot_be_deserialized" then
          Some tt
        else None
      end)
    (fun (function_parameter : unit) ⇒
      let '_ := function_parameter in
      Build_extensible "Value_cannot_be_deserialized" unit tt).

Module Make.
  Class FArgs {S_t : Set} {S_m : Set → Set} := {
    S : Tx_rollup_l2_storage_sig.STORAGE (t := S_t) (m := S_m);
  }.
  Arguments Build_FArgs {_ _}.

  Definition t `{FArgs} : Set := S.(Tx_rollup_l2_storage_sig.STORAGE.t).

  Definition m `{FArgs} (a : Set) : Set :=
    S.(Tx_rollup_l2_storage_sig.STORAGE.m) a.

  Module Syntax.

Inclusion of the module [S.Syntax]

    Definition op_letplus `{FArgs} {a b : Set} :=
      S.(Tx_rollup_l2_storage_sig.STORAGE.Syntax).(Tx_rollup_l2_storage_sig.SYNTAX.op_letplus) (a := a) (b := b).

    Definition op_letstar `{FArgs} {a b : Set} :=
      S.(Tx_rollup_l2_storage_sig.STORAGE.Syntax).(Tx_rollup_l2_storage_sig.SYNTAX.op_letstar) (a := a) (b := b).

    Definition fail `{FArgs} {a : Set} :=
      S.(Tx_rollup_l2_storage_sig.STORAGE.Syntax).(Tx_rollup_l2_storage_sig.SYNTAX.fail) (a := a).

    Definition catch `{FArgs} {a b : Set} :=
      S.(Tx_rollup_l2_storage_sig.STORAGE.Syntax).(Tx_rollup_l2_storage_sig.SYNTAX.catch) (a := a) (b := b).

    Definition _return `{FArgs} {a : Set} :=
      S.(Tx_rollup_l2_storage_sig.STORAGE.Syntax).(Tx_rollup_l2_storage_sig.SYNTAX._return) (a := a).

    Definition list_fold_left_m `{FArgs} {a b : Set} :=
      S.(Tx_rollup_l2_storage_sig.STORAGE.Syntax).(Tx_rollup_l2_storage_sig.SYNTAX.list_fold_left_m) (a := a)
        (b := b).

    Definition op_letstarquestion `{FArgs} {A B : Set}
      (res : Result.t A Error_monad._error)
      (f_value : A → S.(Tx_rollup_l2_storage_sig.STORAGE.m) B)
      : S.(Tx_rollup_l2_storage_sig.STORAGE.m) B :=
      match res with
      | Pervasives.Ok v_value ⇒ f_value v_value
      | Pervasives.Error error_value ⇒ fail error_value
      end.

    Definition fail_unless `{FArgs}
      (cond : bool) (error_value : Error_monad._error)
      : S.(Tx_rollup_l2_storage_sig.STORAGE.m) unit :=
      if cond then
        S.(Tx_rollup_l2_storage_sig.STORAGE.Syntax).(Tx_rollup_l2_storage_sig.SYNTAX._return)
          tt
      else
        S.(Tx_rollup_l2_storage_sig.STORAGE.Syntax).(Tx_rollup_l2_storage_sig.SYNTAX.fail)
          error_value.

    Definition fail_when `{FArgs}
      (cond : bool) (error_value : Error_monad._error)
      : S.(Tx_rollup_l2_storage_sig.STORAGE.m) unit :=
      if cond then
        S.(Tx_rollup_l2_storage_sig.STORAGE.Syntax).(Tx_rollup_l2_storage_sig.SYNTAX.fail)
          error_value
      else
        S.(Tx_rollup_l2_storage_sig.STORAGE.Syntax).(Tx_rollup_l2_storage_sig.SYNTAX._return)
          tt.

    (* Syntax *)
    Definition module `{FArgs} :=
      {|
        Tx_rollup_l2_context_sig.SYNTAX.op_letplus _ _ := op_letplus (H := H);
        Tx_rollup_l2_context_sig.SYNTAX.op_letstar _ _ := op_letstar;
        Tx_rollup_l2_context_sig.SYNTAX.op_letstarquestion _ _ :=
          op_letstarquestion;
        Tx_rollup_l2_context_sig.SYNTAX.fail _ := fail;
        Tx_rollup_l2_context_sig.SYNTAX.catch _ _ := catch;
        Tx_rollup_l2_context_sig.SYNTAX._return _ := _return;
        Tx_rollup_l2_context_sig.SYNTAX.list_fold_left_m _ _ := list_fold_left_m;
        Tx_rollup_l2_context_sig.SYNTAX.fail_unless := fail_unless;
        Tx_rollup_l2_context_sig.SYNTAX.fail_when := fail_when
      |}.
  End Syntax.
  Definition Syntax `{FArgs}
    : Tx_rollup_l2_context_sig.SYNTAX (m := fun (a : Set) ⇒ m a) :=
    Syntax.module.

  Definition bls_verify `{FArgs}
    (accounts : list (Bls.Public_key.(S.SIGNATURE_PUBLIC_KEY.t) × bytes))
    (aggregated_signature : Tx_rollup_l2_context_sig.signature) : m bool :=
    let msgs {A : Set}
      : list (Bls.Public_key.(S.SIGNATURE_PUBLIC_KEY.t) × option A × bytes) :=
      List.map
        (fun (function_parameter :
          Bls.Public_key.(S.SIGNATURE_PUBLIC_KEY.t) × bytes) ⇒
          let '(pk, msg) := function_parameter in
          (pk, None, msg)) accounts in
    Syntax.(Tx_rollup_l2_context_sig.SYNTAX._return)
      (Bls.aggregate_check msgs aggregated_signature).

  Definition unwrap_or `{FArgs} {a : Set}
    (opt : option a) (err : Error_monad._error)
    : S.(Tx_rollup_l2_storage_sig.STORAGE.m) a :=
    match opt with
    | Some x_value ⇒
      S.(Tx_rollup_l2_storage_sig.STORAGE.Syntax).(Tx_rollup_l2_storage_sig.SYNTAX._return)
        x_value
    | None ⇒
      S.(Tx_rollup_l2_storage_sig.STORAGE.Syntax).(Tx_rollup_l2_storage_sig.SYNTAX.fail)
        err
    end.

  Definition serialize_key `{FArgs} (key_value : key) : m bytes :=
    unwrap_or
      (Data_encoding.Binary.to_bytes_opt None packed_key_encoding
        (Key key_value)) (Build_extensible "Key_cannot_be_serialized" unit tt).

  Definition serialize_value `{FArgs} {a : Set}
    (encoding : Data_encoding.t a) (value_value : a) : m bytes :=
    unwrap_or (Data_encoding.Binary.to_bytes_opt None encoding value_value)
      (Build_extensible "Value_cannot_be_serialized" unit tt).

  Definition deserialize_value `{FArgs} {a : Set}
    (encoding : Data_encoding.t a) (value_value : bytes) : m a :=
    unwrap_or (Data_encoding.Binary.of_bytes_opt encoding value_value)
      (Build_extensible "Value_cannot_be_deserialized" unit tt).

[get ctxt key] is a type-safe [get] function.

  Definition get `{FArgs} {a : Set} (ctxt : t) (key_value : key)
    : m (option a) :=
    let value_encoding := value_encoding key_value in
    Syntax.(Tx_rollup_l2_context_sig.SYNTAX.op_letstar)
      (serialize_key key_value)
      (fun key_value ⇒
        Syntax.(Tx_rollup_l2_context_sig.SYNTAX.op_letstar)
          (S.(Tx_rollup_l2_storage_sig.STORAGE.get) ctxt key_value)
          (fun value_value ⇒
            match value_value with
            | Some value_value ⇒
              Syntax.(Tx_rollup_l2_context_sig.SYNTAX.op_letstar)
                (deserialize_value value_encoding value_value)
                (fun value_value ⇒
                  Syntax.(Tx_rollup_l2_context_sig.SYNTAX._return)
                    (Some value_value))
            | None ⇒ Syntax.(Tx_rollup_l2_context_sig.SYNTAX._return) None
            end)).

[set ctxt key value] is a type-safe [set] function.

  Definition set `{FArgs} {a : Set}
    (ctxt : t) (key_value : key) (value_value : a) : m t :=
    let value_encoding := value_encoding key_value in
    Syntax.(Tx_rollup_l2_context_sig.SYNTAX.op_letstar)
      (serialize_key key_value)
      (fun key_value ⇒
        Syntax.(Tx_rollup_l2_context_sig.SYNTAX.op_letstar)
          (serialize_value value_encoding value_value)
          (fun value_value ⇒
            S.(Tx_rollup_l2_storage_sig.STORAGE.set) ctxt key_value value_value)).

  Definition remove `{FArgs} (ctxt : t) (key_value : key) : m t :=
    Syntax.(Tx_rollup_l2_context_sig.SYNTAX.op_letstar)
      (serialize_key key_value)
      (fun key_value ⇒
        S.(Tx_rollup_l2_storage_sig.STORAGE.remove) ctxt key_value).

  Module Address_metadata.
    Definition get `{FArgs}
      (ctxt : t) (idx : Tx_rollup_l2_context_sig.address_index)
      : m (option Tx_rollup_l2_context_sig.metadata) :=
      get ctxt (Address_metadata idx).

    Definition incr_counter `{FArgs}
      (ctxt : t) (idx : Tx_rollup_l2_context_sig.address_index) : m t :=
      Syntax.(Tx_rollup_l2_context_sig.SYNTAX.op_letstar) (get ctxt idx)
        (fun metadata ⇒
          match metadata with
          | Some meta ⇒
            let new_counter :=
              Int64.succ meta.(Tx_rollup_l2_context_sig.metadata.counter) in
            Syntax.(Tx_rollup_l2_context_sig.SYNTAX.op_letstar)
              (Syntax.(Tx_rollup_l2_context_sig.SYNTAX.fail_unless)
                (new_counter ≥i64
                meta.(Tx_rollup_l2_context_sig.metadata.counter))
                (Build_extensible "Counter_overflow" unit tt))
              (fun function_parameter ⇒
                let '_ := function_parameter in
                set ctxt (Address_metadata idx)
                  (Tx_rollup_l2_context_sig.metadata.with_counter new_counter
                    meta))
          | None ⇒
            Syntax.(Tx_rollup_l2_context_sig.SYNTAX.fail)
              (Build_extensible "Unknown_address_index"
                Tx_rollup_l2_context_sig.address_index idx)
          end).

    Definition init_with_public_key `{FArgs}
      (ctxt : t) (idx : Tx_rollup_l2_context_sig.address_index)
      (public_key : Bls.Public_key.(S.SIGNATURE_PUBLIC_KEY.t)) : m t :=
      Syntax.(Tx_rollup_l2_context_sig.SYNTAX.op_letstar) (get ctxt idx)
        (fun metadata ⇒
          match metadata with
          | None ⇒
            set ctxt (Address_metadata idx)
              {| Tx_rollup_l2_context_sig.metadata.counter := 0;
                Tx_rollup_l2_context_sig.metadata.public_key := public_key; |}
          | Some _ ⇒
            Syntax.(Tx_rollup_l2_context_sig.SYNTAX.fail)
              (Build_extensible "Metadata_already_initialized"
                Tx_rollup_l2_context_sig.address_index idx)
          end).

    (* Address_metadata *)
    Definition module `{FArgs} :=
      {|
        Tx_rollup_l2_context_sig.ADDRESS_METADATA.get := get;
        Tx_rollup_l2_context_sig.ADDRESS_METADATA.incr_counter := incr_counter;
        Tx_rollup_l2_context_sig.ADDRESS_METADATA.init_with_public_key :=
          init_with_public_key
      |}.
  End Address_metadata.
  Definition Address_metadata `{FArgs} := Address_metadata.module.

  Module Address_index.
    Definition count `{FArgs} (ctxt : t) : m int32 :=
      Syntax.(Tx_rollup_l2_context_sig.SYNTAX.op_letplus)
        (get ctxt Address_count) (fun count ⇒ Option.value_value count 0).

    Definition init_counter `{FArgs} (ctxt : t) : m t :=
      set ctxt Address_count 0.

    Definition associate_index `{FArgs}
      (ctxt : t) (addr : Tx_rollup_l2_address.t)
      : m (t × Indexable.index Tx_rollup_l2_address.address) :=
      Syntax.(Tx_rollup_l2_context_sig.SYNTAX.op_letstar) (count ctxt)
        (fun i_value ⇒
          let new_count := Int32.succ i_value in
          Syntax.(Tx_rollup_l2_context_sig.SYNTAX.op_letstar)
            (Syntax.(Tx_rollup_l2_context_sig.SYNTAX.fail_unless)
              (new_count ≥i32 i_value)
              (Build_extensible "Too_many_l2_addresses" unit tt))
            (fun function_parameter ⇒
              let '_ := function_parameter in
              let idx := Indexable.index_exn i_value in
              Syntax.(Tx_rollup_l2_context_sig.SYNTAX.op_letstar)
                (set ctxt (Address_index addr) idx)
                (fun ctxt ⇒
                  Syntax.(Tx_rollup_l2_context_sig.SYNTAX.op_letplus)
                    (set ctxt Address_count new_count) (fun ctxt ⇒ (ctxt, idx))))).

    Definition get `{FArgs} (ctxt : t) (addr : Tx_rollup_l2_address.t)
      : m (option Tx_rollup_l2_context_sig.address_index) :=
      get ctxt (Address_index addr).

    Definition get_or_associate_index `{FArgs}
      (ctxt : t) (addr : Tx_rollup_l2_address.t)
      : m
        (t × Tx_rollup_l2_context_sig.created_existed ×
          Tx_rollup_l2_context_sig.address_index) :=
      Syntax.(Tx_rollup_l2_context_sig.SYNTAX.op_letstar) (get ctxt addr)
        (fun index_opt ⇒
          match index_opt with
          | Some idx ⇒
            Syntax.(Tx_rollup_l2_context_sig.SYNTAX._return)
              (ctxt, Tx_rollup_l2_context_sig.Existed, idx)
          | None ⇒
            Syntax.(Tx_rollup_l2_context_sig.SYNTAX.op_letplus)
              (associate_index ctxt addr)
              (fun function_parameter ⇒
                let '(ctxt, idx) := function_parameter in
                (ctxt, Tx_rollup_l2_context_sig.Created, idx))
          end).

    (* Address_index *)
    Definition module `{FArgs} :=
      {|
        Tx_rollup_l2_context_sig.INDEX.init_counter := init_counter;
        Tx_rollup_l2_context_sig.INDEX.get := get;
        Tx_rollup_l2_context_sig.INDEX.get_or_associate_index :=
          get_or_associate_index;
        Tx_rollup_l2_context_sig.INDEX.count := count
      |}.
  End Address_index.
  Definition Address_index `{FArgs}
    : Tx_rollup_l2_context_sig.INDEX (t := t) (m := fun (a : Set) ⇒ m a)
      (hash := Tx_rollup_l2_address.t)
      (index := Tx_rollup_l2_context_sig.address_index) := Address_index.module.

  Module Ticket_index.
    Definition count `{FArgs} (ctxt : t) : m int32 :=
      Syntax.(Tx_rollup_l2_context_sig.SYNTAX.op_letplus)
        (get ctxt Ticket_count) (fun count ⇒ Option.value_value count 0).

    Definition init_counter `{FArgs} (ctxt : t) : m t :=
      set ctxt Ticket_count 0.

    Definition associate_index `{FArgs}
      (ctxt : t) (ticket : Alpha_context.Ticket_hash.t)
      : m (t × Indexable.index Alpha_context.Ticket_hash.t) :=
      Syntax.(Tx_rollup_l2_context_sig.SYNTAX.op_letstar) (count ctxt)
        (fun i_value ⇒
          let new_count := Int32.succ i_value in
          Syntax.(Tx_rollup_l2_context_sig.SYNTAX.op_letstar)
            (Syntax.(Tx_rollup_l2_context_sig.SYNTAX.fail_unless)
              (new_count ≥i32 i_value)
              (Build_extensible "Too_many_l2_tickets" unit tt))
            (fun function_parameter ⇒
              let '_ := function_parameter in
              let idx := Indexable.index_exn i_value in
              Syntax.(Tx_rollup_l2_context_sig.SYNTAX.op_letstar)
                (set ctxt (Ticket_index ticket) idx)
                (fun ctxt ⇒
                  Syntax.(Tx_rollup_l2_context_sig.SYNTAX.op_letplus)
                    (set ctxt Ticket_count new_count) (fun ctxt ⇒ (ctxt, idx))))).

    Definition get `{FArgs} (ctxt : t) (ticket : Alpha_context.Ticket_hash.t)
      : m (option Tx_rollup_l2_context_sig.ticket_index) :=
      get ctxt (Ticket_index ticket).

    Definition get_or_associate_index `{FArgs}
      (ctxt : t) (ticket : Alpha_context.Ticket_hash.t)
      : m
        (t × Tx_rollup_l2_context_sig.created_existed ×
          Tx_rollup_l2_context_sig.ticket_index) :=
      Syntax.(Tx_rollup_l2_context_sig.SYNTAX.op_letstar) (get ctxt ticket)
        (fun index_opt ⇒
          match index_opt with
          | Some idx ⇒
            Syntax.(Tx_rollup_l2_context_sig.SYNTAX._return)
              (ctxt, Tx_rollup_l2_context_sig.Existed, idx)
          | None ⇒
            Syntax.(Tx_rollup_l2_context_sig.SYNTAX.op_letplus)
              (associate_index ctxt ticket)
              (fun function_parameter ⇒
                let '(ctxt, idx) := function_parameter in
                (ctxt, Tx_rollup_l2_context_sig.Created, idx))
          end).

    (* Ticket_index *)
    Definition module `{FArgs} :=
      {|
        Tx_rollup_l2_context_sig.INDEX.init_counter := init_counter;
        Tx_rollup_l2_context_sig.INDEX.get := get;
        Tx_rollup_l2_context_sig.INDEX.get_or_associate_index :=
          get_or_associate_index;
        Tx_rollup_l2_context_sig.INDEX.count := count
      |}.
  End Ticket_index.
  Definition Ticket_index `{FArgs}
    : Tx_rollup_l2_context_sig.INDEX (t := t) (m := fun (a : Set) ⇒ m a)
      (hash := Alpha_context.Ticket_hash.t)
      (index := Tx_rollup_l2_context_sig.ticket_index) := Ticket_index.module.

  Module Ticket_ledger.
    Definition get_opt `{FArgs}
      (ctxt : t) (tidx : Tx_rollup_l2_context_sig.ticket_index)
      (aidx : Tx_rollup_l2_context_sig.address_index)
      : m (option Tx_rollup_l2_qty.t) := get ctxt (Ticket_ledger tidx aidx).

    Definition get `{FArgs}
      (ctxt : t) (tidx : Tx_rollup_l2_context_sig.ticket_index)
      (aidx : Tx_rollup_l2_context_sig.address_index) : m Tx_rollup_l2_qty.t :=
      Syntax.(Tx_rollup_l2_context_sig.SYNTAX.op_letplus)
        (get_opt ctxt tidx aidx)
        (fun res ⇒ Option.value_value res Tx_rollup_l2_qty.zero).

    Definition set `{FArgs}
      (ctxt : t) (tidx : Tx_rollup_l2_context_sig.ticket_index)
      (aidx : Tx_rollup_l2_context_sig.address_index)
      : Tx_rollup_l2_qty.t → m t := set ctxt (Ticket_ledger tidx aidx).

    Definition remove `{FArgs}
      (ctxt : t) (tidx : Tx_rollup_l2_context_sig.ticket_index)
      (aidx : Tx_rollup_l2_context_sig.address_index) : m t :=
      remove ctxt (Ticket_ledger tidx aidx).

    Definition spend `{FArgs}
      (ctxt : t) (tidx : Tx_rollup_l2_context_sig.ticket_index)
      (aidx : Tx_rollup_l2_context_sig.address_index) (qty : Tx_rollup_l2_qty.t)
      : m t :=
      Syntax.(Tx_rollup_l2_context_sig.SYNTAX.op_letstar) (get ctxt tidx aidx)
        (fun src_balance ⇒
          match
            ((Tx_rollup_l2_qty.sub src_balance qty),
              match Tx_rollup_l2_qty.sub src_balance qty with
              | Some remainder ⇒
                Tx_rollup_l2_qty.op_gt remainder Tx_rollup_l2_qty.zero
              | _ ⇒ false
              end) with
          | (None, _) ⇒
            Syntax.(Tx_rollup_l2_context_sig.SYNTAX.fail)
              (Build_extensible "Balance_too_low" unit tt)
          | (Some remainder, true) ⇒ set ctxt tidx aidx remainder
          | (Some _, _) ⇒ remove ctxt tidx aidx
          end).

    Definition credit `{FArgs}
      (ctxt : t) (tidx : Tx_rollup_l2_context_sig.ticket_index)
      (aidx : Tx_rollup_l2_context_sig.address_index) (qty : Tx_rollup_l2_qty.t)
      : m t :=
      Syntax.(Tx_rollup_l2_context_sig.SYNTAX.op_letstar) (get ctxt tidx aidx)
        (fun balance ⇒
          match Tx_rollup_l2_qty.add balance qty with
          | None ⇒
            Syntax.(Tx_rollup_l2_context_sig.SYNTAX.fail)
              (Build_extensible "Balance_overflow" unit tt)
          | Some new_balance ⇒ set ctxt tidx aidx new_balance
          end).

    (* Ticket_ledger *)
    Definition module `{FArgs} :=
      {|
        Tx_rollup_l2_context_sig.TICKET_LEDGER.get := get;
        Tx_rollup_l2_context_sig.TICKET_LEDGER.credit := credit;
        Tx_rollup_l2_context_sig.TICKET_LEDGER.spend := spend
      |}.
  End Ticket_ledger.
  Definition Ticket_ledger `{FArgs}
    : Tx_rollup_l2_context_sig.TICKET_LEDGER (t := t)
      (m := fun (a : Set) ⇒ m a) := Ticket_ledger.module.

  (* Make *)
  Definition functor `{FArgs} :=
    {|
      Tx_rollup_l2_context_sig.CONTEXT.Syntax := Syntax;
      Tx_rollup_l2_context_sig.CONTEXT.bls_verify := bls_verify;
      Tx_rollup_l2_context_sig.CONTEXT.Address_metadata := Address_metadata;
      Tx_rollup_l2_context_sig.CONTEXT.Address_index := Address_index;
      Tx_rollup_l2_context_sig.CONTEXT.Ticket_index := Ticket_index;
      Tx_rollup_l2_context_sig.CONTEXT.Ticket_ledger := Ticket_ledger
    |}.
End Make.
Definition Make {S_t : Set} {S_m : Set → Set}
  (S : Tx_rollup_l2_storage_sig.STORAGE (t := S_t) (m := S_m))
  : Tx_rollup_l2_context_sig.CONTEXT
    (t := S.(Tx_rollup_l2_storage_sig.STORAGE.t))
    (m := fun (a : Set) ⇒ S.(Tx_rollup_l2_storage_sig.STORAGE.m) a) :=
  let '_ := Make.Build_FArgs S in
  Make.functor.