🐆 Tx_rollup_l2_context_sig.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_qty.

Definition Ticket_indexable :=
  Indexable.Make
    {|
      Indexable.VALUE.encoding := Alpha_context.Ticket_hash.encoding;
      Indexable.VALUE.compare := Alpha_context.Ticket_hash.compare;
      Indexable.VALUE.pp := Alpha_context.Ticket_hash.pp
    |}.

An integer used to identified a layer-2 address. See {!Tx_rollup_l2_address.index}.

Definition address_index : Set := Tx_rollup_l2_address.Indexable.index.

An integer used to identified a layer-1 ticket deposited in a transaction rollup.

Definition ticket_index : Set := Ticket_indexable.(Indexable.INDEXABLE.index).

The metadata associated to a layer-2 address.

The counter is an counter-measure against replay attack. Each operation is signed with an integer (its counter). The counter is incremented when the operation is applied. This prevents the operation to be applied once again, since its integer will not be in sync with the counter of the account. The choice of [int64] for the type of the counter theoretically prevents the rollup to an integer overflow. However, it can only happen if a single account makes more than [1.8446744e+19] operations. If an account sends 1000 operations per seconds, it would take them more than 5845420 centuries to achieve that.

The [public_key] allows to authenticate the owner of the address, by verifying BLS signatures.

Module metadata.
  Record record : Set := Build {
    counter : int64;
    public_key : Bls.Public_key.(S.SIGNATURE_PUBLIC_KEY.t);
  }.
  Definition with_counter counter (r : record) :=
    Build counter r.(public_key).
  Definition with_public_key public_key (r : record) :=
    Build r.(counter) public_key.
End metadata.
Definition metadata := metadata.record.

Init function; without side-effects in Coq

Definition init_module : unit :=
  let '_ :=
    Error_monad.register_error_kind Error_monad.Temporary
      "tx_rollup_unknown_address_index" "Unknown address index"
      "Tried to increment the counter of an unknown address index" None
      (Data_encoding.obj1
        (Data_encoding.req None None "index"
          Tx_rollup_l2_address.Indexable.index_encoding))
      (fun (function_parameter : Error_monad._error) ⇒
        match function_parameter with
        | Build_extensible tag _ payload ⇒
          if String.eqb tag "Unknown_address_index" then
            let x_value := cast address_index payload in
            Some x_value
          else None
        end)
      (fun (x_value : Tx_rollup_l2_address.Indexable.index) ⇒
        Build_extensible "Unknown_address_index"
          Tx_rollup_l2_address.Indexable.index x_value) in
  let '_ :=
    Error_monad.register_error_kind Error_monad.Temporary
      "tx_rollup_balance_too_low" "Balance too low"
      "Tried to spend a ticket index from an index without the required balance"
      None Data_encoding.empty
      (fun (function_parameter : Error_monad._error) ⇒
        match function_parameter with
        | Build_extensible tag _ payload ⇒
          if String.eqb tag "Balance_too_low" then
            Some tt
          else None
        end)
      (fun (function_parameter : unit) ⇒
        let '_ := function_parameter in
        Build_extensible "Balance_too_low" unit tt) in
  let '_ :=
    Error_monad.register_error_kind Error_monad.Temporary
      "tx_rollup_balance_overflow" "Balance overflow"
      "Tried to credit a ticket index to an index to a new balance greater than the integer 32 limit"
      None Data_encoding.empty
      (fun (function_parameter : Error_monad._error) ⇒
        match function_parameter with
        | Build_extensible tag _ payload ⇒
          if String.eqb tag "Balance_overflow" then
            Some tt
          else None
        end)
      (fun (function_parameter : unit) ⇒
        let '_ := function_parameter in
        Build_extensible "Balance_overflow" unit tt) in
  let '_ :=
    Error_monad.register_error_kind Error_monad.Permanent
      "tx_rollup_invalid_quantity" "Invalid quantity"
      "Tried to credit a ticket index to an index with a quantity non-strictly positive"
      None Data_encoding.empty
      (fun (function_parameter : Error_monad._error) ⇒
        match function_parameter with
        | Build_extensible tag _ payload ⇒
          if String.eqb tag "Invalid_quantity" then
            Some tt
          else None
        end)
      (fun (function_parameter : unit) ⇒
        let '_ := function_parameter in
        Build_extensible "Invalid_quantity" unit tt) in
  let '_ :=
    Error_monad.register_error_kind Error_monad.Branch
      "tx_rollup_metadata_already_initialized" "Metadata already initiliazed"
      "Tried to initialize a metadata for an index which was already initiliazed"
      None
      (Data_encoding.obj1
        (Data_encoding.req None None "index"
          Tx_rollup_l2_address.Indexable.index_encoding))
      (fun (function_parameter : Error_monad._error) ⇒
        match function_parameter with
        | Build_extensible tag _ payload ⇒
          if String.eqb tag "Metadata_already_initialized" then
            let x_value := cast address_index payload in
            Some x_value
          else None
        end)
      (fun (x_value : Tx_rollup_l2_address.Indexable.index) ⇒
        Build_extensible "Metadata_already_initialized"
          Tx_rollup_l2_address.Indexable.index x_value) in
  let '_ :=
    Error_monad.register_error_kind Error_monad.Branch
      "tx_rollup_too_many_l2_addresses" "Too many l2 addresses"
      "The number of l2 addresses has reached the integer 32 limit" None
      Data_encoding.empty
      (fun (function_parameter : Error_monad._error) ⇒
        match function_parameter with
        | Build_extensible tag _ payload ⇒
          if String.eqb tag "Too_many_l2_addresses" then
            Some tt
          else None
        end)
      (fun (function_parameter : unit) ⇒
        let '_ := function_parameter in
        Build_extensible "Too_many_l2_addresses" unit tt) in
  let '_ :=
    Error_monad.register_error_kind Error_monad.Branch
      "tx_rollup_too_many_l2_tickets" "Too many l2 tickets"
      "The number of l2 tickets has reached the integer 32 limit" None
      Data_encoding.empty
      (fun (function_parameter : Error_monad._error) ⇒
        match function_parameter with
        | Build_extensible tag _ payload ⇒
          if String.eqb tag "Too_many_l2_tickets" then
            Some tt
          else None
        end)
      (fun (function_parameter : unit) ⇒
        let '_ := function_parameter in
        Build_extensible "Too_many_l2_tickets" unit tt) in
  Error_monad.register_error_kind Error_monad.Branch
    "tx_rollup_counter_overflow" "Counter overflow"
    "Tried to increment the counter of an address and reached the integer 64 limit"
    None Data_encoding.empty
    (fun (function_parameter : Error_monad._error) ⇒
      match function_parameter with
      | Build_extensible tag _ payload ⇒
        if String.eqb tag "Counter_overflow" then
          Some tt
        else None
      end)
    (fun (function_parameter : unit) ⇒
      let '_ := function_parameter in
      Build_extensible "Counter_overflow" unit tt).

Inductive created_existed : Set :=
| Created : created_existed
| Existed : created_existed.

The necessary monadic operators the storage monad is required to provide.

Module SYNTAX.
  Record signature {m : Set → Set} : Set := {
    m := m;
    op_letplus : ∀ {a b : Set}, m a → (a → b) → m b;
    op_letstar : ∀ {a b : Set}, m a → (a → m b) → m b;
    

[let*?] is for binding the value from Result-only expressions into the storage monad.

    op_letstarquestion :
      ∀ {a b : Set},
      Pervasives.result a Error_monad._error → (a → m b) → m b;
    

[fail err] shortcuts the current computation by raising an error.

Said error can be handled with the [catch] combinator.

    fail : ∀ {a : Set}, Error_monad._error → m a;
    

[catch p k h] tries to executes the monadic computation [p]. If [p] terminates without an error, then its result is passed to the continuation [k]. On the contrary, if an error [err] is raised, it is passed to the error handler [h].

    catch :
      ∀ {a b : Set},
      m a → (a → m b) → (Error_monad._error → m b) → m b;
    

[return x] is the simplest computation inside the monad [m] which simply computes [x] and nothing else.

    _return : ∀ {a : Set}, a → m a;
    

[list_fold_left_m f] is a monadic version of [List.fold_left f], wherein [f] is not a pure computation, but a computation in the monad [m].

    list_fold_left_m :
      ∀ {a b : Set}, (a → b → m a) → a → list b → m a;
    

[fail_unless cond err] raises [err] iff [cond] is [false].

    fail_unless : bool → Error_monad._error → m unit;
    

[fail_when cond err] raises [err] iff [cond] is [true].

    fail_when : bool → Error_monad._error → m unit;
  }.
End SYNTAX.
Definition SYNTAX := @SYNTAX.signature.
Arguments SYNTAX {_}.

Module ADDRESS_METADATA.
  Record signature {t : Set} {m : Set → Set} : Set := {
    t := t;
    m := m;
    

[get ctxt idx] returns the current metadata associated to the address indexed by [idx].

    get : t → address_index → m (option metadata);
    

[incr_counter ctxt idx] increments the counter of the address indexed by [idx].

This function can fail with [Counter_overflow] iff the counter has reached the [Int64.max_int] limit.

This function can fail with [Unknown_address_index] if [idx] has not been associated with a layer-2 address already.

    incr_counter : t → address_index → m t;
    

[init_with_public_key ctxt idx pk] initializes the metadata associated to the address indexed by [idx].

This can fails with [Metadata_already_initialized] if this function has already been called with [idx].

    init_with_public_key :
      t → address_index → Bls.Public_key.(S.SIGNATURE_PUBLIC_KEY.t) → m t;
  }.
End ADDRESS_METADATA.
Definition ADDRESS_METADATA := @ADDRESS_METADATA.signature.
Arguments ADDRESS_METADATA {_ _}.

Module INDEX.
  Record signature {t : Set} {m : Set → Set} {hash index : Set} : Set := {
    t := t;
    m := m;
    hash := hash;
    index := index;
    

[init_counter ctxt] writes the default counter (i.e. [0L]) in the context.

    init_counter : t → m t;
    

[get ctxt hash] returns the index associated to [hash], if any.

    get : t → hash → m (option index);
    

[get_or_associate_index ctxt hash] associates a fresh [index] to [hash], and returns it. If the [hash] has already been associated to an index, it returns it. It also returns the information on whether the index was created or already existed.

This function can fail with [Too_many_l2_tickets] iff there is no fresh index available.

    get_or_associate_index : t → hash → m (t × created_existed × index);
    

[count ctxt] returns the number of tickets that have been involved in the transaction rollup.

    count : t → m int32;
  }.
End INDEX.
Definition INDEX := @INDEX.signature.
Arguments INDEX {_ _ _ _}.

Module TICKET_LEDGER.
  Record signature {t : Set} {m : Set → Set} : Set := {
    t := t;
    m := m;
    

[get ctxt tidx aidx] returns the quantity of tickets ([tidx]) [aidx] owns.

{b Note:} It is the responsibility of the caller to verify that [aidx] and [tidx] have been associated to an address and a ticket respectively. The function will return zero when the address has no such ticket.

    get : t → ticket_index → address_index → m Tx_rollup_l2_qty.t;
    

[credit ctxt tidx aidx qty] updates the ledger to increase the number of tickets indexed by [tidx] the address [aidx] owns by [qty] units.

This function can fail with [Balance_overflow] if adding [qty] to the current balance of [aidx] causes an integer overflow.

This function can fail with [Invalid_quantity] if [qty] is not strictly positive.

{b Note:} It is the responsibility of the caller to verify that [aidx] and [tidx] have been associated to an address and a ticket respectively.

    credit : t → ticket_index → address_index → Tx_rollup_l2_qty.t → m t;
    

[spend ctxt tidx aidx qty] updates the ledger to decrease the number of tickets indexed by [tidx] the address [aidx] owns by [qty] units.

This function can fail with [Balance_too_low] if [aidx] does not own at least [qty] ticket.

{b Note:} It is the responsibility of the caller to verify that [aidx] and [tidx] have been associated to an address and a ticket respectively.

    spend : t → ticket_index → address_index → Tx_rollup_l2_qty.t → m t;
  }.
End TICKET_LEDGER.
Definition TICKET_LEDGER := @TICKET_LEDGER.signature.
Arguments TICKET_LEDGER {_ _}.

This module type describes the API of the [Tx_rollup] context, which is used to implement the semantics of the L2 operations.

Module CONTEXT.
  Record signature {t : Set} {m : Set → Set} : Set := {
    

The state of the [Tx_rollup] context.

The context provides a type-safe, functional API to interact with the state of a transaction rollup. The functions of this module, manipulating and creating values of type [t] are called “context operations” afterwards.

    t := t;
    

The monad used by the context.

{b Note:} It is likely to be the monad of the underlying storage. In the case of the proof verifier, as it is expected to be run into the L1, the monad will also be used to perform gas accounting. This is why all the functions of this module type needs to be inside the monad [m].

    m := m;
    Syntax : SYNTAX (m := fun (a : Set) ⇒ m a);
    

[bls_aggregate_verify] allows to verify the aggregated signature of a batch.

    bls_verify :
      list (Bls.Public_key.(S.SIGNATURE_PUBLIC_KEY.t) × bytes) → Bls.t →
      m bool;
    

The metadata associated to an address.

    Address_metadata : ADDRESS_METADATA (t := t) (m := fun (a : Set) ⇒ m a);
    

Mapping between {!Tx_rollup_l2_address.address} and {!address_index}.

Addresses are supposed to be associated to a {!address_index} in order to reduce the batches' size submitted from the layer1 to the layer2. Therefore, the first time an address is used in a layer2 operation, we associate it to a address_index that should be use in future layer2 operations.

    Address_index :
      INDEX (t := t) (m := fun (a : Set) ⇒ m a)
        (hash := Tx_rollup_l2_address.t) (index := address_index);
    

Mapping between {!Ticket_hash.t} and {!ticket_index}.

Ticket hashes are supposed to be associated to a {!ticket_index} in order to reduce the batches' size submitted from the layer1 to the layer2. Therefore, the first time a ticket hash is used in a layer2 operation, we associate it to a ticket_index that should be use in future layer2 operations.

    Ticket_index :
      INDEX (t := t) (m := fun (a : Set) ⇒ m a)
        (hash := Alpha_context.Ticket_hash.t) (index := ticket_index);
    

The ledger of the layer 2 where are registered the amount of a given ticket a L2 [account] has in its possession.

    Ticket_ledger : TICKET_LEDGER (t := t) (m := fun (a : Set) ⇒ m a);
  }.
End CONTEXT.
Definition CONTEXT := @CONTEXT.signature.
Arguments CONTEXT {_ _}.

Definition signature : Set := Bls.t.