(*****************************************************************************)
(*                                                                           *)
(* Open Source License                                                       *)
(* Copyright (c) 2021 Nomadic Labs <contact@nomadic-labs.com>                *)
(*                                                                           *)
(* Permission is hereby granted, free of charge, to any person obtaining a   *)
(* copy of this software and associated documentation files (the "Software"),*)
(* to deal in the Software without restriction, including without limitation *)
(* the rights to use, copy, modify, merge, publish, distribute, sublicense,  *)
(* and/or sell copies of the Software, and to permit persons to whom the     *)
(* Software is furnished to do so, subject to the following conditions:      *)
(*                                                                           *)
(* The above copyright notice and this permission notice shall be included   *)
(* in all copies or substantial portions of the Software.                    *)
(*                                                                           *)
(* THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR*)
(* IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,  *)
(* FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL   *)
(* THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER*)
(* LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING   *)
(* FROM, OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER       *)
(* DEALINGS IN THE SOFTWARE.                                                 *)
(*                                                                           *)
(*****************************************************************************)

(** This module provides a temporary toy rollup to be used as a demo. *)

(*
   FIXME/DAL: https://gitlab.com/tezos/tezos/-/issues/3995
   Use EOL/SOL once merged to import Dal pages.
*)

(**

   This rollup is a stack machine equipped with addition.

   It processes postfix arithmetic expressions written as sequence of
   (space separated) [int] and [+] using the following rules:

   - a number [x] is interpreted as pushing [x] on the stack ;

   - a variable [a] is interpreted as storing the topmost element of the
     stack in the storage under the name "a" ;

   - a variable [out] is interpreted as adding a message to the outbox
     containing a single transaction batch with the topmost element of the
     stack as payload, the zero contract as destination, and a default
     entrypoint ;

   - a symbol [+] pops two integers [x] and [y] and pushes [x + y] on
     the stack ;

   - an input [hash:<HASH>] is interpreted as a directive to request the DAC
     data whose hash is <HASH> ;

   - an input [dal:<LVL>:<SID>:<PID>] is interpreted as a directive to request
     the DAL page whose index is <PID> belonging to slot index <SID> confirmed
     at level <LVL> (i.e published at level LVL - endorsement_lag) ;

   If a message is not syntactically correct or does not evaluate
   correctly, the machine stops its evaluation and waits for the next
   message.

   The machine has a boot sector which is a mere string used a prefix
   for each message.

   The module implements the {!Sc_rollup_PVM_sig.S}Î interface to be
   used in the smart contract rollup infrastructure.

   The machine exposes extra operations to be used in the rollup node.

*)
module type S = sig
  include Sc_rollup_PVM_sig.S

  (** [name] is "arith". *)
  val name : string

  (** [parse_boot_sector s] builds a boot sector from its human
      writable description. *)
  val parse_boot_sector : string -> string option

  (** [pp_boot_sector fmt s] prints a human readable representation of
     a boot sector. *)
  val pp_boot_sector : Format.formatter -> string -> unit

  (** [pp state] returns a pretty-printer valid for [state]. *)
  val pp : state -> (Format.formatter -> unit -> unit) Lwt.t

  (** [get_tick state] returns the current tick of [state]. *)
  val get_tick : state -> Sc_rollup_tick_repr.t Lwt.t

  (** The machine has five possible statuses: *)
  type status =
    | Halted
    | Waiting_for_input_message
    | Waiting_for_reveal
    | Waiting_for_metadata
    | Parsing
    | Evaluating

  (** [get_status state] returns the machine status in [state]. *)
  val get_status : state -> status Lwt.t

  (** [get_outbox state] returns the outbox in [state]. *)
  val get_outbox : state -> Sc_rollup_PVM_sig.output list Lwt.t

  (** The machine has only three instructions. *)
  type instruction =
    | IPush : int -> instruction
    | IAdd : instruction
    | IStore : string -> instruction

  (** [equal_instruction i1 i2] is [true] iff [i1] equals [i2]. *)
  val equal_instruction : instruction -> instruction -> bool

  (** [pp_instruction fmt i] shows a human readable representation of [i]. *)
  val pp_instruction : Format.formatter -> instruction -> unit

  (** [get_parsing_result state] is [Some true] if the current
      message is syntactically correct, [Some false] when it
      contains a syntax error, and [None] when the machine is
      not in parsing state. *)
  val get_parsing_result : state -> bool option Lwt.t

  (** [get_code state] returns the current code obtained by parsing
      the current input message. *)
  val get_code : state -> instruction list Lwt.t

  (** [get_stack state] returns the current stack. *)
  val get_stack : state -> int list Lwt.t

  (** [get_var state x] returns the current value of variable [x].
      Returns [None] if [x] does not exist. *)
  val get_var : state -> string -> int option Lwt.t

  (** [get_evaluation_result state] returns [Some true] if the current
      message evaluation succeeds, [Some false] if it failed, and
      [None] if the evaluation has not been done yet. *)
  val get_evaluation_result : state -> bool option Lwt.t

  (** [get_is_stuck state] returns [Some err] if some internal error
      made the machine fail during the last evaluation step. [None]
      if no internal error occurred. When a machine is stuck, it
      reboots, waiting for the next message to process. *)
  val get_is_stuck : state -> string option Lwt.t
end

module Protocol_implementation :
  S
    with type context = Context.t
     and type state = Context.tree
     and type proof = Context.Proof.tree Context.Proof.t

(** This is the state hash of reference that both the prover of the
    node and the verifier of the protocol {!Protocol_implementation}
    have to agree on (if they do, it means they are using the same
    tree structure). *)
val reference_initial_state_hash : Sc_rollup_repr.State_hash.t

module type P = sig
  module Tree : Context.TREE with type key = string list and type value = bytes

  type tree = Tree.tree

  val hash_tree : tree -> Sc_rollup_repr.State_hash.t

  type proof

  val proof_encoding : proof Data_encoding.t

  val proof_before : proof -> Sc_rollup_repr.State_hash.t

  val proof_after : proof -> Sc_rollup_repr.State_hash.t

  val verify_proof :
    proof -> (tree -> (tree * 'a) Lwt.t) -> (tree * 'a) option Lwt.t

  val produce_proof :
    Tree.t -> tree -> (tree -> (tree * 'a) Lwt.t) -> (proof * 'a) option Lwt.t
end

module Make (Context : P) :
  S
    with type context = Context.Tree.t
     and type state = Context.tree
     and type proof = Context.proof