Skip to main content

🦏 Sc_rollup_arith.v

Translated OCaml

Gitlab , OCaml

File generated by coq-of-ocaml
Init function; without side-effects in Coq
Definition init_module : unit :=
  let msg := "Invalid claim about outbox" in
  let '_ :=
    Error_monad.register_error_kind Error_monad.Permanent
      "sc_rollup_arith_invalid_claim_about_outbox" msg msg
      (Some
        (fun (fmt : Format.formatter) ⇒
          fun (function_parameter : unit) ⇒
            let '_ := function_parameter in
            Format.pp_print_string fmt msg)) Data_encoding.unit_value
      (fun (function_parameter : Error_monad._error) ⇒
        match function_parameter with
        | Build_extensible tag _ payload
          if String.eqb tag "Arith_invalid_claim_about_outbox" then
            Some tt
          else None
        end)
      (fun (function_parameter : unit) ⇒
        let '_ := function_parameter in
        Build_extensible "Arith_invalid_claim_about_outbox" unit tt) in
  let msg := "Output proof production failed" in
  let '_ :=
    Error_monad.register_error_kind Error_monad.Permanent
      "sc_rollup_arith_output_proof_production_failed" msg msg
      (Some
        (fun (fmt : Format.formatter) ⇒
          fun (function_parameter : unit) ⇒
            let '_ := function_parameter in
            Format.fprintf fmt
              (CamlinternalFormatBasics.Format
                (CamlinternalFormatBasics.String
                  CamlinternalFormatBasics.No_padding
                  CamlinternalFormatBasics.End_of_format) "%s") msg))
      Data_encoding.unit_value
      (fun (function_parameter : Error_monad._error) ⇒
        match function_parameter with
        | Build_extensible tag _ payload
          if String.eqb tag "Arith_output_proof_production_failed" then
            Some tt
          else None
        end)
      (fun (function_parameter : unit) ⇒
        let '_ := function_parameter in
        Build_extensible "Arith_output_proof_production_failed" unit tt) in
  let msg := "Proof production failed" in
  Error_monad.register_error_kind Error_monad.Permanent
    "sc_rollup_arith_proof_production_failed" msg msg
    (Some
      (fun (fmt : Format.formatter) ⇒
        fun (function_parameter : unit) ⇒
          let '_ := function_parameter in
          Format.fprintf fmt
            (CamlinternalFormatBasics.Format
              (CamlinternalFormatBasics.String
                CamlinternalFormatBasics.No_padding
                CamlinternalFormatBasics.End_of_format) "%s") msg))
    Data_encoding.unit_value
    (fun (function_parameter : Error_monad._error) ⇒
      match function_parameter with
      | Build_extensible tag _ payload
        if String.eqb tag "Arith_proof_production_failed" then
          Some tt
        else None
      end)
    (fun (function_parameter : unit) ⇒
      let '_ := function_parameter in
      Build_extensible "Arith_proof_production_failed" unit tt).

Module P.
  Record signature {Tree_t Tree_tree proof : Set} : Set := {
    Tree :
      Context.TREE (t := Tree_t) (tree := Tree_tree) (key := list string)
        (value := bytes);
    tree := Tree.(Context.TREE.tree);
    hash_tree : tree Sc_rollup_repr.State_hash.t;
    proof := proof;
    proof_encoding : Data_encoding.t proof;
    proof_before : proof Sc_rollup_repr.State_hash.t;
    proof_after : proof Sc_rollup_repr.State_hash.t;
    verify_proof :
       {a : Set}, proof (tree tree × a) option (tree × a);
    produce_proof :
       {a : Set},
      Tree.(Context.TREE.t) tree (tree tree × a) option (proof × a);
  }.
End P.
Definition P := @P.signature.
Arguments P {_ _ _}.

Module S.
  Record signature {state context proof output_proof status instruction : Set}
    : Set := {
    state := state;
    pp : state (Format.formatter unit unit);
    context := context;
    hash := Sc_rollup_repr.State_hash.t;
    proof := proof;
    proof_encoding : Data_encoding.t proof;
    proof_start_state : proof hash;
    proof_stop_state : proof hash;
    state_hash : state hash;
    initial_state : context state;
    install_boot_sector : state string state;
    is_input_state : state Sc_rollup_PVM_sig.input_request;
    set_input : Sc_rollup_PVM_sig.input state state;
    eval : state state;
    verify_proof :
      option Sc_rollup_PVM_sig.input proof
      M? Sc_rollup_PVM_sig.input_request;
    produce_proof :
      context option Sc_rollup_PVM_sig.input state M? proof;
    verify_origination_proof : proof string bool;
    produce_origination_proof : context string M? proof;
    output_proof := output_proof;
    output_proof_encoding : Data_encoding.t output_proof;
    output_of_output_proof : output_proof Sc_rollup_PVM_sig.output;
    state_of_output_proof : output_proof hash;
    verify_output_proof : output_proof bool;
    produce_output_proof :
      context state Sc_rollup_PVM_sig.output
      Pervasives.result output_proof Error_monad._error;
    (* Internal_for_tests_insert_failure : state -> state; *)
    name : string;
    parse_boot_sector : string option string;
    pp_boot_sector : Format.formatter string unit;
    get_tick : state Sc_rollup_tick_repr.t;
    status := status;
    get_status : state status;
    get_outbox : state list Sc_rollup_PVM_sig.output;
    instruction := instruction;
    equal_instruction : instruction instruction bool;
    pp_instruction : Format.formatter instruction unit;
    get_parsing_result : state option bool;
    get_code : state list instruction;
    get_stack : state list int;
    get_var : state string option int;
    get_evaluation_result : state option bool;
    get_is_stuck : state option string;
  }.
End S.
Definition S := @S.signature.
Arguments S {_ _ _ _ _ _}.

Module Make.
  Class FArgs {Context_Tree_t Context_Tree_tree Context_proof : Set} := {
    Context :
      P (Tree_t := Context_Tree_t) (Tree_tree := Context_Tree_tree)
        (proof := Context_proof);
  }.
  Arguments Build_FArgs {_ _ _}.

  Definition Tree `{FArgs} := Context.(P.Tree).

  Definition context `{FArgs} : Set := Context.(P.Tree).(Context.TREE.t).

  Definition hash `{FArgs} : Set := Sc_rollup_repr.State_hash.t.

  Definition proof `{FArgs} : Set := Context.(P.proof).

  Definition proof_encoding `{FArgs} : Data_encoding.t proof :=
    Context.(P.proof_encoding).

  Definition proof_start_state `{FArgs} (proof_value : proof)
    : Sc_rollup_repr.State_hash.t := Context.(P.proof_before) proof_value.

  Definition proof_stop_state `{FArgs} (proof_value : proof)
    : Sc_rollup_repr.State_hash.t := Context.(P.proof_after) proof_value.

  Definition name `{FArgs} : string := "arith".

  Definition parse_boot_sector `{FArgs} {A : Set} (s_value : A) : option A :=
    Some s_value.

  Definition pp_boot_sector `{FArgs} (fmt : Format.formatter) (s_value : string)
    : unit :=
    Format.fprintf fmt
      (CamlinternalFormatBasics.Format
        (CamlinternalFormatBasics.String CamlinternalFormatBasics.No_padding
          CamlinternalFormatBasics.End_of_format) "%s") s_value.

  Definition tree `{FArgs} : Set := Context.(P.Tree).(Context.TREE.tree).

  Inductive status `{FArgs} : Set :=
  | Halted : status
  | Waiting_for_input_message : status
  | Waiting_for_reveal : status
  | Parsing : status
  | Evaluating : status.

  Inductive instruction `{FArgs} : Set :=
  | IPush : int instruction
  | IAdd : instruction
  | IStore : string instruction.

  Definition equal_instruction `{FArgs} (i1 : instruction) (i2 : instruction)
    : bool :=
    match (i1, i2) with
    | (IPush x_value, IPush y_value)x_value =i y_value
    | (IAdd, IAdd)true
    | (IStore x_value, IStore y_value)
      Compare.String.(Compare.S.op_eq) x_value y_value
    | (_, _)false
    end.

  Definition pp_instruction `{FArgs}
    (fmt : Format.formatter) (function_parameter : instruction) : unit :=
    match function_parameter with
    | IPush x_value
      Format.fprintf fmt
        (CamlinternalFormatBasics.Format
          (CamlinternalFormatBasics.String_literal "push("
            (CamlinternalFormatBasics.Int CamlinternalFormatBasics.Int_d
              CamlinternalFormatBasics.No_padding
              CamlinternalFormatBasics.No_precision
              (CamlinternalFormatBasics.Char_literal ")" % char
                CamlinternalFormatBasics.End_of_format))) "push(%d)") x_value
    | IAdd
      Format.fprintf fmt
        (CamlinternalFormatBasics.Format
          (CamlinternalFormatBasics.String_literal "add"
            CamlinternalFormatBasics.End_of_format) "add")
    | IStore x_value
      Format.fprintf fmt
        (CamlinternalFormatBasics.Format
          (CamlinternalFormatBasics.String_literal "store("
            (CamlinternalFormatBasics.String CamlinternalFormatBasics.No_padding
              (CamlinternalFormatBasics.Char_literal ")" % char
                CamlinternalFormatBasics.End_of_format))) "store(%s)") x_value
    end.

  Module State.
    Definition state `{FArgs} : Set := tree.

    Module Monad.
      Definition t `{FArgs} (a : Set) : Set := state state × option a.

      Definition _return `{FArgs} {A B : Set} (x_value : A) (state_value : B)
        : B × option A := (state_value, (Some x_value)).

      Definition bind `{FArgs} {A B C D : Set}
        (m_value : A B × option C) (f_value : C B B × option D)
        (state_value : A) : B × option D :=
        let '(state_value, res) := m_value state_value in
        match res with
        | None(state_value, None)
        | Some resf_value res state_value
        end.

      Module Syntax.
        Definition op_letstar `{FArgs} {A B C D : Set}
          : (A B × option C) (C B B × option D) A B × option D :=
          bind.
      End Syntax.

      Definition run `{FArgs} {A B : Set} (m_value : A B) (state_value : A)
        : B := m_value state_value.

      Definition internal_error_key `{FArgs} : list string :=
        [ "internal_error" ].

      Definition internal_error `{FArgs} {A : Set}
        (msg : string) (tree_value : Context.(P.Tree).(Context.TREE.tree))
        : Context.(P.Tree).(Context.TREE.tree) × option A :=
        let tree_value :=
          Tree.(Context.TREE.add) tree_value internal_error_key
            (Bytes.of_string msg) in
        (tree_value, None).

      Definition is_stuck `{FArgs}
        (tree_value : Context.(P.Tree).(Context.TREE.tree))
        : Context.(P.Tree).(Context.TREE.tree) × option (option string) :=
        let v_value := Tree.(Context.TREE.find) tree_value internal_error_key in
        (tree_value, (Some (Option.map Bytes.to_string v_value))).

      Definition remove `{FArgs}
        (key_value : Tree.(Context.TREE.key))
        (tree_value : Context.(P.Tree).(Context.TREE.tree))
        : Context.(P.Tree).(Context.TREE.tree) × option unit :=
        let tree_value := Tree.(Context.TREE.remove) tree_value key_value in
        (tree_value, (Some tt)).

      Definition decode `{FArgs} {A : Set}
        (encoding : Data_encoding.encoding A) (bytes_value : bytes)
        (state_value : Context.(P.Tree).(Context.TREE.tree))
        : Context.(P.Tree).(Context.TREE.tree) × option A :=
        match Data_encoding.Binary.of_bytes_opt encoding bytes_value with
        | Noneinternal_error "Error during decoding" state_value
        | Some v_value(state_value, (Some v_value))
        end.

      Definition find_value `{FArgs} {A : Set}
        (key_value : Tree.(Context.TREE.key))
        (encoding : Data_encoding.encoding A)
        (state_value : Context.(P.Tree).(Context.TREE.tree))
        : Context.(P.Tree).(Context.TREE.tree) × option (option A) :=
        let obytes := Tree.(Context.TREE.find) state_value key_value in
        match obytes with
        | None(state_value, (Some None))
        | Some bytes_value
          let '(state_value, value_value) :=
            decode encoding bytes_value state_value in
          (state_value, (Some value_value))
        end.

      Definition children `{FArgs} {A : Set}
        (key_value : Tree.(Context.TREE.key))
        (encoding : Data_encoding.encoding A)
        (state_value : Context.(P.Tree).(Context.TREE.tree))
        : Context.(P.Tree).(Context.TREE.tree) × option (list (string × A)) :=
        let children :=
          Tree.(Context.TREE.list_value) state_value None None key_value in
        let fix aux {B : Set}
          (function_parameter : list (B × Context.(P.Tree).(Context.TREE.tree)))
          : Context.(P.Tree).(Context.TREE.tree) × option (list (B × A)) :=
          match function_parameter with
          | [](state_value, (Some nil))
          | cons (key_value, tree_value) children
            let obytes := Tree.(Context.TREE.to_value) tree_value in
            match obytes with
            | Noneinternal_error "Invalid children" state_value
            | Some bytes_value
              let '(state_value, v_value) :=
                decode encoding bytes_value state_value in
              match v_value with
              | None(state_value, None)
              | Some v_value
                let '(state_value, l_value) := aux children in
                match l_value with
                | None(state_value, None)
                | Some l_value
                  (state_value, (Some (cons (key_value, v_value) l_value)))
                end
              end
            end
          end in
        aux children.

      Definition get_value `{FArgs} {A : Set}
        (default : A) (key_value : Tree.(Context.TREE.key))
        (encoding : Data_encoding.encoding A)
        : Context.(P.Tree).(Context.TREE.tree)
        Context.(P.Tree).(Context.TREE.tree) × option A :=
        Syntax.op_letstar (find_value key_value encoding)
          (fun ov
            match ov with
            | None_return default
            | Some x_value_return x_value
            end).

      Definition set_value `{FArgs} {A : Set}
        (key_value : Tree.(Context.TREE.key))
        (encoding : Data_encoding.encoding A) (value_value : A)
        (tree_value : Context.(P.Tree).(Context.TREE.tree))
        : Context.(P.Tree).(Context.TREE.tree) × option unit :=
        (fun (function_parameter : option bytes) ⇒
          match function_parameter with
          | Noneinternal_error "Internal_Error during encoding" tree_value
          | Some bytes_value
            let tree_value :=
              Tree.(Context.TREE.add) tree_value key_value bytes_value in
            (tree_value, (Some tt))
          end) (Data_encoding.Binary.to_bytes_opt None encoding value_value).
    End Monad.

    Module P_MakeVar.
      Record signature `{FArgs} {t : Set} : Set := {
        t := t;
        name : string;
        initial : t;
        pp : Format.formatter t unit;
        encoding : Data_encoding.t t;
      }.
    End P_MakeVar.
    Definition P_MakeVar := @P_MakeVar.signature.
    Arguments P_MakeVar {_ _ _ _ _}.

    Module S_MakeVar.
      Record signature `{FArgs} {t : Set} : Set := {
        t := t;
        create : Monad.t unit;
        get : Monad.t t;
        set : t Monad.t unit;
        pp : Monad.t (Format.formatter unit unit);
      }.
    End S_MakeVar.
    Definition S_MakeVar := @S_MakeVar.signature.
    Arguments S_MakeVar {_ _ _ _ _}.

    Module Make_var.
      Class FArgs `{FArgs} {P_t : Set} := {
        P : P_MakeVar (t := P_t);
      }.
      Arguments Build_FArgs {_ _ _ _ _}.

      Definition key_value `{FArgs} : list string := [ P.(P_MakeVar.name) ].

      Definition create `{FArgs} : Monad.t unit :=
        Monad.set_value key_value P.(P_MakeVar.encoding) P.(P_MakeVar.initial).

      Definition get `{FArgs} : Monad.t P.(P_MakeVar.t) :=
        Monad.Syntax.op_letstar
          (Monad.find_value key_value P.(P_MakeVar.encoding))
          (fun v_value
            match v_value with
            | NoneMonad._return P.(P_MakeVar.initial)
            | Some v_valueMonad._return v_value
            end).

      Definition set `{FArgs} : P.(P_MakeVar.t) Monad.t unit :=
        Monad.set_value key_value P.(P_MakeVar.encoding).

      Definition pp `{FArgs} : Monad.t (Format.formatter unit unit) :=
        Monad.Syntax.op_letstar get
          (fun v_value
            Monad._return
              (fun (fmt : Format.formatter) ⇒
                fun (function_parameter : unit) ⇒
                  let '_ := function_parameter in
                  Format.fprintf fmt
                    (CamlinternalFormatBasics.Format
                      (CamlinternalFormatBasics.Formatting_gen
                        (CamlinternalFormatBasics.Open_box
                          (CamlinternalFormatBasics.Format
                            CamlinternalFormatBasics.End_of_format ""))
                        (CamlinternalFormatBasics.String
                          CamlinternalFormatBasics.No_padding
                          (CamlinternalFormatBasics.String_literal " : "
                            (CamlinternalFormatBasics.Alpha
                              (CamlinternalFormatBasics.Formatting_lit
                                CamlinternalFormatBasics.Close_box
                                CamlinternalFormatBasics.End_of_format)))))
                      "@[%s : %a@]") P.(P_MakeVar.name) P.(P_MakeVar.pp) v_value)).

      (* Make_var *)
      Definition functor `{FArgs} :=
        {|
          S_MakeVar.create := create;
          S_MakeVar.get := get;
          S_MakeVar.set := set;
          S_MakeVar.pp := pp
        |}.
    End Make_var.
    Definition Make_var `{FArgs} {P_t : Set} (P : P_MakeVar (t := P_t))
      : S_MakeVar (t := P.(P_MakeVar.t)) :=
      let '_ := Make_var.Build_FArgs P in
      Make_var.functor.

    Module P_MakeDict.
      Record signature `{FArgs} {t : Set} : Set := {
        t := t;
        name : string;
        pp : Format.formatter t unit;
        encoding : Data_encoding.t t;
      }.
    End P_MakeDict.
    Definition P_MakeDict := @P_MakeDict.signature.
    Arguments P_MakeDict {_ _ _ _ _}.

    Module MakeDict_sig.
      Record signature `{FArgs} {t : Set} : Set := {
        t := t;
        get : string Monad.t (option t);
        set : string t Monad.t unit;
        entries : Monad.t (list (string × t));
        mapped_to : string t state bool;
        pp : Monad.t (Format.formatter unit unit);
      }.
    End MakeDict_sig.
    Definition MakeDict_sig := @MakeDict_sig.signature.
    Arguments MakeDict_sig {_ _ _ _ _}.

    Module Make_dict.
      Class FArgs `{FArgs} {P_t : Set} := {
        P : P_MakeDict (t := P_t);
      }.
      Arguments Build_FArgs {_ _ _ _ _}.

      Definition key_value `{FArgs} (k_value : string) : list string :=
        [ P.(P_MakeDict.name); k_value ].

      Definition get `{FArgs} (k_value : string)
        : Monad.t (option P.(P_MakeDict.t)) :=
        Monad.find_value (key_value k_value) P.(P_MakeDict.encoding).

      Definition set `{FArgs} (k_value : string) (v_value : P.(P_MakeDict.t))
        : Monad.t unit :=
        Monad.set_value (key_value k_value) P.(P_MakeDict.encoding) v_value.

      Definition entries `{FArgs}
        : Monad.t (list (string × P.(P_MakeDict.t))) :=
        Monad.children [ P.(P_MakeDict.name) ] P.(P_MakeDict.encoding).

      Definition mapped_to `{FArgs}
        (k_value : string) (v_value : P.(P_MakeDict.t)) (state_value : state)
        : bool :=
        let '(state', _) := Monad.run (set k_value v_value) state_value in
        let t_value :=
          Tree.(Context.TREE.find_tree) state_value (key_value k_value) in
        let t' := Tree.(Context.TREE.find_tree) state' (key_value k_value) in
        Option.equal Tree.(Context.TREE.equal) t_value t'.

      Definition pp `{FArgs} : Monad.t (Format.formatter unit unit) :=
        Monad.Syntax.op_letstar entries
          (fun l_value
            let pp_elem
              (fmt : Format.formatter)
              (function_parameter : string × P.(P_MakeDict.t)) : unit :=
              let '(key_value, value_value) := function_parameter in
              Format.fprintf fmt
                (CamlinternalFormatBasics.Format
                  (CamlinternalFormatBasics.Formatting_gen
                    (CamlinternalFormatBasics.Open_box
                      (CamlinternalFormatBasics.Format
                        CamlinternalFormatBasics.End_of_format ""))
                    (CamlinternalFormatBasics.String
                      CamlinternalFormatBasics.No_padding
                      (CamlinternalFormatBasics.String_literal " : "
                        (CamlinternalFormatBasics.Alpha
                          (CamlinternalFormatBasics.Formatting_lit
                            CamlinternalFormatBasics.Close_box
                            CamlinternalFormatBasics.End_of_format)))))
                  "@[%s : %a@]") key_value P.(P_MakeDict.pp) value_value in
            Monad._return
              (fun (fmt : Format.formatter) ⇒
                fun (function_parameter : unit) ⇒
                  let '_ := function_parameter in
                  Format.pp_print_list None pp_elem fmt l_value)).

      (* Make_dict *)
      Definition functor `{FArgs} :=
        {|
          MakeDict_sig.get := get;
          MakeDict_sig.set := set;
          MakeDict_sig.entries := entries;
          MakeDict_sig.mapped_to := mapped_to;
          MakeDict_sig.pp := pp
        |}.
    End Make_dict.
    Definition Make_dict `{FArgs} {P_t : Set} (P : P_MakeDict (t := P_t))
      : MakeDict_sig (t := P.(P_MakeDict.t)) :=
      let '_ := Make_dict.Build_FArgs P in
      Make_dict.functor.

    Module P_deque.
      Record signature `{FArgs} {t : Set} : Set := {
        t := t;
        name : string;
        encoding : Data_encoding.t t;
      }.
    End P_deque.
    Definition P_deque := @P_deque.signature.
    Arguments P_deque {_ _ _ _ _}.

    Module MakeDeque_sig.
      Record signature `{FArgs} {t : Set} : Set := {
        t := t;
        top : Monad.t (option t);
        push : t Monad.t unit;
        pop : Monad.t (option t);
        inject : t Monad.t unit;
        to_list : Monad.t (list t);
        clear : Monad.t unit;
      }.
    End MakeDeque_sig.
    Definition MakeDeque_sig := @MakeDeque_sig.signature.
    Arguments MakeDeque_sig {_ _ _ _ _}.

    Module Make_deque.
      Class FArgs `{FArgs} {P_t : Set} := {
        P : P_deque (t := P_t);
      }.
      Arguments Build_FArgs {_ _ _ _ _}.

      Definition head_key `{FArgs} : list string :=
        [ P.(P_deque.name); "head" ].

      Definition end_key `{FArgs} : list string := [ P.(P_deque.name); "end" ].

      Definition get_head `{FArgs} : Monad.t Z.t :=
        Monad.get_value Z.zero head_key Data_encoding.z_value.

      Definition set_head `{FArgs} : Z.t Monad.t unit :=
        Monad.set_value head_key Data_encoding.z_value.

      Definition get_end `{FArgs} : Monad.t Z.t :=
        Monad.get_value (Z.of_int 0) end_key Data_encoding.z_value.

      Definition set_end `{FArgs} : Z.t Monad.t unit :=
        Monad.set_value end_key Data_encoding.z_value.

      Definition idx_key `{FArgs} (idx : Z.t) : list string :=
        [ P.(P_deque.name); Z.to_string idx ].

      Definition top `{FArgs} : Monad.t (option P.(P_deque.t)) :=
        Monad.Syntax.op_letstar get_head
          (fun head_idx
            Monad.Syntax.op_letstar get_end
              (fun end_idx
                Monad.Syntax.op_letstar
                  (Monad.find_value (idx_key head_idx) P.(P_deque.encoding))
                  (fun v_value
                    if Z.leq end_idx head_idx then
                      Monad._return None
                    else
                      match v_value with
                      | None
                        (* ❌ Assert instruction is not handled. *)
                        assert (Monad.t (option P.(P_deque.t))) false
                      | Some x_valueMonad._return (Some x_value)
                      end))).

      Definition push `{FArgs} (x_value : P.(P_deque.t)) : Monad.t unit :=
        Monad.Syntax.op_letstar get_head
          (fun head_idx
            let head_idx' := Z.pred head_idx in
            Monad.Syntax.op_letstar (set_head head_idx')
              (fun function_parameter
                let '_ := function_parameter in
                Monad.set_value (idx_key head_idx') P.(P_deque.encoding) x_value)).

      Definition pop `{FArgs} : Monad.t (option P.(P_deque.t)) :=
        Monad.Syntax.op_letstar get_head
          (fun head_idx
            Monad.Syntax.op_letstar get_end
              (fun end_idx
                if Z.leq end_idx head_idx then
                  Monad._return None
                else
                  Monad.Syntax.op_letstar
                    (Monad.find_value (idx_key head_idx) P.(P_deque.encoding))
                    (fun v_value
                      match v_value with
                      | None
                        (* ❌ Assert instruction is not handled. *)
                        assert (Monad.t (option P.(P_deque.t))) false
                      | Some x_value
                        Monad.Syntax.op_letstar
                          (Monad.remove (idx_key head_idx))
                          (fun function_parameter
                            let '_ := function_parameter in
                            let head_idx := Z.succ head_idx in
                            Monad.Syntax.op_letstar (set_head head_idx)
                              (fun function_parameter
                                let '_ := function_parameter in
                                Monad._return (Some x_value)))
                      end))).

      Definition inject `{FArgs} (x_value : P.(P_deque.t)) : Monad.t unit :=
        Monad.Syntax.op_letstar get_end
          (fun end_idx
            let end_idx' := Z.succ end_idx in
            Monad.Syntax.op_letstar (set_end end_idx')
              (fun function_parameter
                let '_ := function_parameter in
                Monad.set_value (idx_key end_idx) P.(P_deque.encoding) x_value)).

      #[bypass_check(guard)]
      Definition to_list `{FArgs} : Monad.t (list P.(P_deque.t)) :=
        Monad.Syntax.op_letstar get_head
          (fun head_idx
            Monad.Syntax.op_letstar get_end
              (fun end_idx
                let fix aux (l_value : list P.(P_deque.t)) (idx : Z.t)
                  {struct idx} : Monad.t (list P.(P_deque.t)) :=
                  if Z.lt idx head_idx then
                    Monad._return l_value
                  else
                    Monad.Syntax.op_letstar
                      (Monad.find_value (idx_key idx) P.(P_deque.encoding))
                      (fun v_value
                        match v_value with
                        | None
                          (* ❌ Assert instruction is not handled. *)
                          assert (Monad.t (list P.(P_deque.t))) false
                        | Some v_value
                          aux (cons v_value l_value) (Z.pred idx)
                        end) in
                aux nil (Z.pred end_idx))).

      Definition clear `{FArgs} : Monad.t unit :=
        Monad.remove [ P.(P_deque.name) ].

      (* Make_deque *)
      Definition functor `{FArgs} :=
        {|
          MakeDeque_sig.top := top;
          MakeDeque_sig.push := push;
          MakeDeque_sig.pop := pop;
          MakeDeque_sig.inject := inject;
          MakeDeque_sig.to_list := to_list;
          MakeDeque_sig.clear := clear
        |}.
    End Make_deque.
    Definition Make_deque `{FArgs} {P_t : Set} (P : P_deque (t := P_t))
      : MakeDeque_sig (t := P.(P_deque.t)) :=
      let '_ := Make_deque.Build_FArgs P in
      Make_deque.functor.

    Definition Current_tick `{FArgs} :=
      Make_var
        (let t : Set := Sc_rollup_tick_repr.t in
        let name := "tick" in
        let initial := Sc_rollup_tick_repr.initial in
        let pp := Sc_rollup_tick_repr.pp in
        let encoding := Sc_rollup_tick_repr.encoding in
        {|
          P_MakeVar.name := name;
          P_MakeVar.initial := initial;
          P_MakeVar.pp := pp;
          P_MakeVar.encoding := encoding
        |}).

    Definition Vars `{FArgs} :=
      Make_dict
        (let t : Set := int in
        let name := "vars" in
        let encoding := Data_encoding.int31 in
        let pp (fmt : Format.formatter) (x_value : int) : unit :=
          Format.fprintf fmt
            (CamlinternalFormatBasics.Format
              (CamlinternalFormatBasics.Int CamlinternalFormatBasics.Int_d
                CamlinternalFormatBasics.No_padding
                CamlinternalFormatBasics.No_precision
                CamlinternalFormatBasics.End_of_format) "%d") x_value in
        {|
          P_MakeDict.name := name;
          P_MakeDict.pp := pp;
          P_MakeDict.encoding := encoding
        |}).

    Definition Stack `{FArgs} :=
      Make_deque
        (let t : Set := int in
        let name := "stack" in
        let encoding := Data_encoding.int31 in
        {|
          P_deque.name := name;
          P_deque.encoding := encoding
        |}).

    Definition Code `{FArgs} :=
      Make_deque
        (let t : Set := instruction in
        let name := "code" in
        let encoding :=
          Data_encoding.union None
            [
              Data_encoding.case_value "push" None (Data_encoding.Tag 0)
                Data_encoding.int31
                (fun (function_parameter : instruction) ⇒
                  match function_parameter with
                  | IPush x_valueSome x_value
                  | _None
                  end)
                (fun (x_value : int) ⇒ IPush x_value);
              Data_encoding.case_value "add" None (Data_encoding.Tag 1)
                Data_encoding.unit_value
                (fun (function_parameter : instruction) ⇒
                  match function_parameter with
                  | IAddSome tt
                  | _None
                  end)
                (fun (function_parameter : unit) ⇒
                  let '_ := function_parameter in
                  IAdd);
              Data_encoding.case_value "store" None (Data_encoding.Tag 2)
                Data_encoding.string_value
                (fun (function_parameter : instruction) ⇒
                  match function_parameter with
                  | IStore x_valueSome x_value
                  | _None
                  end)
                (fun (x_value : string) ⇒ IStore x_value)
            ] in
        {|
          P_deque.name := name;
          P_deque.encoding := encoding
        |}).

    Definition Boot_sector `{FArgs} :=
      Make_var
        (let t : Set := string in
        let name := "boot_sector" in
        let initial := "" in
        let encoding := Data_encoding.string_value in
        let pp (fmt : Format.formatter) (s_value : string) : unit :=
          Format.fprintf fmt
            (CamlinternalFormatBasics.Format
              (CamlinternalFormatBasics.String
                CamlinternalFormatBasics.No_padding
                CamlinternalFormatBasics.End_of_format) "%s") s_value in
        {|
          P_MakeVar.name := name;
          P_MakeVar.initial := initial;
          P_MakeVar.pp := pp;
          P_MakeVar.encoding := encoding
        |}).

    Definition Status `{FArgs} :=
      Make_var
        (let t : Set := status in
        let initial := Halted in
        let encoding :=
          Data_encoding.string_enum
            [
              ("Halted", Halted);
              ("Waiting_for_input_message", Waiting_for_input_message);
              ("Waiting_for_reveal", Waiting_for_reveal);
              ("Parsing", Parsing);
              ("Evaluating", Evaluating)
            ] in
        let name := "status" in
        let string_of_status (function_parameter : status) : string :=
          match function_parameter with
          | Halted ⇒ "Halted"
          | Waiting_for_input_message ⇒ "Waiting for input message"
          | Waiting_for_reveal ⇒ "Waiting for reveal"
          | Parsing ⇒ "Parsing"
          | Evaluating ⇒ "Evaluating"
          end in
        let pp (fmt : Format.formatter) (status : status) : unit :=
          Format.fprintf fmt
            (CamlinternalFormatBasics.Format
              (CamlinternalFormatBasics.String
                CamlinternalFormatBasics.No_padding
                CamlinternalFormatBasics.End_of_format) "%s")
            (string_of_status status) in
        {|
          P_MakeVar.name := name;
          P_MakeVar.initial := initial;
          P_MakeVar.pp := pp;
          P_MakeVar.encoding := encoding
        |}).

    Definition Required_reveal `{FArgs} :=
      Make_var
        (let t : Set := option Sc_rollup_PVM_sig.Input_hash.(S.HASH.t) in
        let initial {A : Set} : option A :=
          None in
        let encoding :=
          Data_encoding.option_value PS.Input_hash.(S.HASH.encoding) in
        let name := "required_pre_image_hash" in
        let pp
          (fmt : Format.formatter)
          (v_value : option Sc_rollup_PVM_sig.Input_hash.(S.HASH.t)) : unit :=
          match v_value with
          | None
            Format.fprintf fmt
              (CamlinternalFormatBasics.Format
                (CamlinternalFormatBasics.String_literal "<none>"
                  CamlinternalFormatBasics.End_of_format) "<none>")
          | Some h_valuePS.Input_hash.(S.HASH.pp) fmt h_value
          end in
        {|
          P_MakeVar.name := name;
          P_MakeVar.initial := initial;
          P_MakeVar.pp := pp;
          P_MakeVar.encoding := encoding
        |}).

    Definition Current_level `{FArgs} :=
      Make_var
        (let t : Set := Raw_level_repr.t in
        let initial := Raw_level_repr.root_value in
        let encoding := Raw_level_repr.encoding in
        let name := "current_level" in
        let pp := Raw_level_repr.pp in
        {|
          P_MakeVar.name := name;
          P_MakeVar.initial := initial;
          P_MakeVar.pp := pp;
          P_MakeVar.encoding := encoding
        |}).

    Definition Message_counter `{FArgs} :=
      Make_var
        (let t : Set := option Z.t in
        let initial {A : Set} : option A :=
          None in
        let encoding := Data_encoding.option_value Data_encoding.n_value in
        let name := "message_counter" in
        let pp (fmt : Format.formatter) (function_parameter : option Z.t)
          : unit :=
          match function_parameter with
          | None
            Format.fprintf fmt
              (CamlinternalFormatBasics.Format
                (CamlinternalFormatBasics.String_literal "None"
                  CamlinternalFormatBasics.End_of_format) "None")
          | Some c_value
            Format.fprintf fmt
              (CamlinternalFormatBasics.Format
                (CamlinternalFormatBasics.String_literal "Some "
                  (CamlinternalFormatBasics.Alpha
                    CamlinternalFormatBasics.End_of_format)) "Some %a")
              Z.pp_print c_value
          end in
        {|
          P_MakeVar.name := name;
          P_MakeVar.initial := initial;
          P_MakeVar.pp := pp;
          P_MakeVar.encoding := encoding
        |}).

    Definition Next_message `{FArgs} :=
      Make_var
        (let t : Set := option string in
        let initial {A : Set} : option A :=
          None in
        let encoding := Data_encoding.option_value Data_encoding.string_value in
        let name := "next_message" in
        let pp (fmt : Format.formatter) (function_parameter : option string)
          : unit :=
          match function_parameter with
          | None
            Format.fprintf fmt
              (CamlinternalFormatBasics.Format
                (CamlinternalFormatBasics.String_literal "None"
                  CamlinternalFormatBasics.End_of_format) "None")
          | Some s_value
            Format.fprintf fmt
              (CamlinternalFormatBasics.Format
                (CamlinternalFormatBasics.String_literal "Some "
                  (CamlinternalFormatBasics.String
                    CamlinternalFormatBasics.No_padding
                    CamlinternalFormatBasics.End_of_format)) "Some %s") s_value
          end in
        {|
          P_MakeVar.name := name;
          P_MakeVar.initial := initial;
          P_MakeVar.pp := pp;
          P_MakeVar.encoding := encoding
        |}).

    Inductive parser_state `{FArgs} : Set :=
    | ParseInt : parser_state
    | ParseVar : parser_state
    | SkipLayout : parser_state.

    Definition Lexer_state `{FArgs} :=
      Make_var
        (let t : Set := int × int in
        let name := "lexer_buffer" in
        let initial := ((-1), (-1)) in
        let encoding :=
          Data_encoding.tup2 Data_encoding.int31 Data_encoding.int31 in
        let pp (fmt : Format.formatter) (function_parameter : int × int)
          : unit :=
          let '(start, len) := function_parameter in
          Format.fprintf fmt
            (CamlinternalFormatBasics.Format
              (CamlinternalFormatBasics.String_literal "lexer.(start = "
                (CamlinternalFormatBasics.Int CamlinternalFormatBasics.Int_d
                  CamlinternalFormatBasics.No_padding
                  CamlinternalFormatBasics.No_precision
                  (CamlinternalFormatBasics.String_literal ", len = "
                    (CamlinternalFormatBasics.Int CamlinternalFormatBasics.Int_d
                      CamlinternalFormatBasics.No_padding
                      CamlinternalFormatBasics.No_precision
                      (CamlinternalFormatBasics.Char_literal ")" % char
                        CamlinternalFormatBasics.End_of_format)))))
              "lexer.(start = %d, len = %d)") start len in
        {|
          P_MakeVar.name := name;
          P_MakeVar.initial := initial;
          P_MakeVar.pp := pp;
          P_MakeVar.encoding := encoding
        |}).

    Definition Parser_state `{FArgs} :=
      Make_var
        (let t : Set := parser_state in
        let name := "parser_state" in
        let initial := SkipLayout in
        let encoding :=
          Data_encoding.string_enum
            [
              ("ParseInt", ParseInt);
              ("ParseVar", ParseVar);
              ("SkipLayout", SkipLayout)
            ] in
        let pp (fmt : Format.formatter) (function_parameter : parser_state)
          : unit :=
          match function_parameter with
          | ParseInt
            Format.fprintf fmt
              (CamlinternalFormatBasics.Format
                (CamlinternalFormatBasics.String_literal "Parsing int"
                  CamlinternalFormatBasics.End_of_format) "Parsing int")
          | ParseVar
            Format.fprintf fmt
              (CamlinternalFormatBasics.Format
                (CamlinternalFormatBasics.String_literal "Parsing var"
                  CamlinternalFormatBasics.End_of_format) "Parsing var")
          | SkipLayout
            Format.fprintf fmt
              (CamlinternalFormatBasics.Format
                (CamlinternalFormatBasics.String_literal "Skipping layout"
                  CamlinternalFormatBasics.End_of_format) "Skipping layout")
          end in
        {|
          P_MakeVar.name := name;
          P_MakeVar.initial := initial;
          P_MakeVar.pp := pp;
          P_MakeVar.encoding := encoding
        |}).

    Definition Parsing_result `{FArgs} :=
      Make_var
        (let t : Set := option bool in
        let name := "parsing_result" in
        let initial {A : Set} : option A :=
          None in
        let encoding := Data_encoding.option_value Data_encoding.bool_value in
        let pp (fmt : Format.formatter) (function_parameter : option bool)
          : unit :=
          match function_parameter with
          | None
            Format.fprintf fmt
              (CamlinternalFormatBasics.Format
                (CamlinternalFormatBasics.String_literal "n/a"
                  CamlinternalFormatBasics.End_of_format) "n/a")
          | Some true
            Format.fprintf fmt
              (CamlinternalFormatBasics.Format
                (CamlinternalFormatBasics.String_literal "parsing succeeds"
                  CamlinternalFormatBasics.End_of_format) "parsing succeeds")
          | Some false
            Format.fprintf fmt
              (CamlinternalFormatBasics.Format
                (CamlinternalFormatBasics.String_literal "parsing fails"
                  CamlinternalFormatBasics.End_of_format) "parsing fails")
          end in
        {|
          P_MakeVar.name := name;
          P_MakeVar.initial := initial;
          P_MakeVar.pp := pp;
          P_MakeVar.encoding := encoding
        |}).

    Definition Evaluation_result `{FArgs} :=
      Make_var
        (let t : Set := option bool in
        let name := "evaluation_result" in
        let initial {A : Set} : option A :=
          None in
        let encoding := Data_encoding.option_value Data_encoding.bool_value in
        let pp (fmt : Format.formatter) (function_parameter : option bool)
          : unit :=
          match function_parameter with
          | None
            Format.fprintf fmt
              (CamlinternalFormatBasics.Format
                (CamlinternalFormatBasics.String_literal "n/a"
                  CamlinternalFormatBasics.End_of_format) "n/a")
          | Some true
            Format.fprintf fmt
              (CamlinternalFormatBasics.Format
                (CamlinternalFormatBasics.String_literal "evaluation succeeds"
                  CamlinternalFormatBasics.End_of_format) "evaluation succeeds")
          | Some false
            Format.fprintf fmt
              (CamlinternalFormatBasics.Format
                (CamlinternalFormatBasics.String_literal "evaluation fails"
                  CamlinternalFormatBasics.End_of_format) "evaluation fails")
          end in
        {|
          P_MakeVar.name := name;
          P_MakeVar.initial := initial;
          P_MakeVar.pp := pp;
          P_MakeVar.encoding := encoding
        |}).

    Definition Output_counter `{FArgs} :=
      Make_var
        (let t : Set := Z.t in
        let initial := Z.zero in
        let name := "output_counter" in
        let encoding := Data_encoding.n_value in
        let pp := Z.pp_print in
        {|
          P_MakeVar.name := name;
          P_MakeVar.initial := initial;
          P_MakeVar.pp := pp;
          P_MakeVar.encoding := encoding
        |}).

    Definition Output `{FArgs} :=
      Make_dict
        (let t : Set := Sc_rollup_PVM_sig.output in
        let name := "output" in
        let encoding := Sc_rollup_PVM_sig.output_encoding in
        let pp := Sc_rollup_PVM_sig.pp_output in
        {|
          P_MakeDict.name := name;
          P_MakeDict.pp := pp;
          P_MakeDict.encoding := encoding
        |}).

    Definition pp `{FArgs} : Monad.t (Format.formatter unit unit) :=
      Monad.Syntax.op_letstar Status.(S_MakeVar.pp)
        (fun status_pp
          Monad.Syntax.op_letstar Message_counter.(S_MakeVar.pp)
            (fun message_counter_pp
              Monad.Syntax.op_letstar Next_message.(S_MakeVar.pp)
                (fun next_message_pp
                  Monad.Syntax.op_letstar Parsing_result.(S_MakeVar.pp)
                    (fun parsing_result_pp
                      Monad.Syntax.op_letstar Parser_state.(S_MakeVar.pp)
                        (fun parser_state_pp
                          Monad.Syntax.op_letstar Lexer_state.(S_MakeVar.pp)
                            (fun lexer_state_pp
                              Monad.Syntax.op_letstar
                                Evaluation_result.(S_MakeVar.pp)
                                (fun evaluation_result_pp
                                  Monad.Syntax.op_letstar Vars.(MakeDict_sig.pp)
                                    (fun vars_pp
                                      Monad.Syntax.op_letstar
                                        Output.(MakeDict_sig.pp)
                                        (fun output_pp
                                          Monad.Syntax.op_letstar
                                            Stack.(MakeDeque_sig.to_list)
                                            (fun stack_value
                                              Monad.Syntax.op_letstar
                                                Current_tick.(S_MakeVar.pp)
                                                (fun current_tick_pp
                                                  Monad._return
                                                    (fun (fmt :
                                                      Format.formatter) ⇒
                                                      fun (function_parameter :
                                                        unit) ⇒
                                                        let '_ :=
                                                          function_parameter in
                                                        Format.fprintf fmt
                                                          (CamlinternalFormatBasics.Format
                                                            (CamlinternalFormatBasics.Formatting_gen
                                                              (CamlinternalFormatBasics.Open_box
                                                                (CamlinternalFormatBasics.Format
                                                                  (CamlinternalFormatBasics.String_literal
                                                                    "<v 0 >"
                                                                    CamlinternalFormatBasics.End_of_format)
                                                                  "<v 0 >"))
                                                              (CamlinternalFormatBasics.Formatting_lit
                                                                (CamlinternalFormatBasics.Break
                                                                  "@;" 1 0)
                                                                (CamlinternalFormatBasics.Alpha
                                                                  (CamlinternalFormatBasics.Formatting_lit
                                                                    (CamlinternalFormatBasics.Break
                                                                      "@;" 1 0)
                                                                    (CamlinternalFormatBasics.Alpha
                                                                      (CamlinternalFormatBasics.Formatting_lit
                                                                        (CamlinternalFormatBasics.Break
                                                                          "@;" 1
                                                                          0)
                                                                        (CamlinternalFormatBasics.Alpha
                                                                          (CamlinternalFormatBasics.Formatting_lit
                                                                            (CamlinternalFormatBasics.Break
                                                                              "@;"
                                                                              1
                                                                              0)
                                                                            (CamlinternalFormatBasics.Alpha
                                                                              (CamlinternalFormatBasics.Formatting_lit
                                                                                (CamlinternalFormatBasics.Break
                                                                                  "@;"
                                                                                  1
                                                                                  0)
                                                                                (CamlinternalFormatBasics.Alpha
                                                                                  (CamlinternalFormatBasics.Formatting_lit
                                                                                    (CamlinternalFormatBasics.Break
                                                                                      "@;"
                                                                                      1
                                                                                      0)
                                                                                    (CamlinternalFormatBasics.Alpha
                                                                                      (CamlinternalFormatBasics.Formatting_lit
                                                                                        (CamlinternalFormatBasics.Break
                                                                                          "@;"
                                                                                          1
                                                                                          0)
                                                                                        (CamlinternalFormatBasics.Alpha
                                                                                          (CamlinternalFormatBasics.Formatting_lit
                                                                                            (CamlinternalFormatBasics.Break
                                                                                              "@;"
                                                                                              1
                                                                                              0)
                                                                                            (CamlinternalFormatBasics.String_literal
                                                                                              "tick : "
                                                                                              (CamlinternalFormatBasics.Alpha
                                                                                                (CamlinternalFormatBasics.Formatting_lit
                                                                                                  (CamlinternalFormatBasics.Break
                                                                                                    "@;"
                                                                                                    1
                                                                                                    0)
                                                                                                  (CamlinternalFormatBasics.String_literal
                                                                                                    "vars : "
                                                                                                    (CamlinternalFormatBasics.Alpha
                                                                                                      (CamlinternalFormatBasics.Formatting_lit
                                                                                                        (CamlinternalFormatBasics.Break
                                                                                                          "@;"
                                                                                                          1
                                                                                                          0)
                                                                                                        (CamlinternalFormatBasics.String_literal
                                                                                                          "output :"
                                                                                                          (CamlinternalFormatBasics.Alpha
                                                                                                            (CamlinternalFormatBasics.Formatting_lit
                                                                                                              (CamlinternalFormatBasics.Break
                                                                                                                "@;"
                                                                                                                1
                                                                                                                0)
                                                                                                              (CamlinternalFormatBasics.String_literal
                                                                                                                "stack : "
                                                                                                                (CamlinternalFormatBasics.Alpha
                                                                                                                  (CamlinternalFormatBasics.Formatting_lit
                                                                                                                    (CamlinternalFormatBasics.Break
                                                                                                                      "@;"
                                                                                                                      1
                                                                                                                      0)
                                                                                                                    (CamlinternalFormatBasics.Formatting_lit
                                                                                                                      CamlinternalFormatBasics.Close_box
                                                                                                                      CamlinternalFormatBasics.End_of_format)))))))))))))))))))))))))))))
                                                            "@[<v 0 >@;%a@;%a@;%a@;%a@;%a@;%a@;%a@;tick : %a@;vars : %a@;output :%a@;stack : %a@;@]")
                                                          status_pp tt
                                                          message_counter_pp tt
                                                          next_message_pp tt
                                                          parsing_result_pp tt
                                                          parser_state_pp tt
                                                          lexer_state_pp tt
                                                          evaluation_result_pp
                                                          tt current_tick_pp tt
                                                          vars_pp tt output_pp
                                                          tt
                                                          (Format.pp_print_list
                                                            None
                                                            Format.pp_print_int)
                                                          stack_value)))))))))))).
  End State.

  Definition state `{FArgs} : Set := State.state.

  Definition initial_state `{FArgs} (ctxt : Context.(P.Tree).(Context.TREE.t))
    : State.state :=
    let state_value := Tree.(Context.TREE.empty) ctxt in
    let m_value :=
      State.Monad.Syntax.op_letstar (State.Status.(State.S_MakeVar.set) Halted)
        (fun function_parameter
          let '_ := function_parameter in
          State.Monad._return tt) in
    let '(state_value, _) := State.Monad.run m_value state_value in
    state_value.

  Definition install_boot_sector `{FArgs}
    (state_value : State.state) (boot_sector : string) : State.state :=
    let m_value :=
      State.Monad.Syntax.op_letstar
        (State.Boot_sector.(State.S_MakeVar.set) boot_sector)
        (fun function_parameter
          let '_ := function_parameter in
          State.Monad._return tt) in
    let '(state_value, _) := State.Monad.run m_value state_value in
    state_value.

  Definition state_hash `{FArgs}
    (state_value : Context.(P.Tree).(Context.TREE.tree))
    : Sc_rollup_repr.State_hash.t :=
    let context_hash := Tree.(Context.TREE.hash_value) state_value in
    match Sc_rollup_repr.State_hash.context_hash_to_state_hash context_hash with
    | Pervasives.Ok sthsth
    | Pervasives.Error _
      (* ❌ Assert instruction is not handled. *)
      assert Sc_rollup_repr.State_hash.t false
    end.

  Definition pp `{FArgs} (state_value : State.state)
    : Format.formatter unit unit :=
    let '(_, pp) := State.Monad.run State.pp state_value in
    match pp with
    | None
      fun (fmt : Format.formatter) ⇒
        fun (function_parameter : unit) ⇒
          let '_ := function_parameter in
          Format.fprintf fmt
            (CamlinternalFormatBasics.Format
              (CamlinternalFormatBasics.String_literal "<opaque>"
                CamlinternalFormatBasics.End_of_format) "<opaque>")
    | Some pp
      let state_hash := state_hash state_value in
      fun (fmt : Format.formatter) ⇒
        fun (function_parameter : unit) ⇒
          let '_ := function_parameter in
          Format.fprintf fmt
            (CamlinternalFormatBasics.Format
              (CamlinternalFormatBasics.Formatting_gen
                (CamlinternalFormatBasics.Open_box
                  (CamlinternalFormatBasics.Format
                    CamlinternalFormatBasics.End_of_format ""))
                (CamlinternalFormatBasics.Alpha
                  (CamlinternalFormatBasics.String_literal ": "
                    (CamlinternalFormatBasics.Alpha
                      (CamlinternalFormatBasics.Formatting_lit
                        CamlinternalFormatBasics.Close_box
                        CamlinternalFormatBasics.End_of_format))))) "@[%a: %a@]")
            Sc_rollup_repr.State_hash.pp state_hash pp tt
    end.

  Definition boot `{FArgs} : State.Monad.t unit :=
    State.Monad.Syntax.op_letstar State.Status.(State.S_MakeVar.create)
      (fun function_parameter
        let '_ := function_parameter in
        State.Monad.Syntax.op_letstar
          State.Next_message.(State.S_MakeVar.create)
          (fun function_parameter
            let '_ := function_parameter in
            State.Monad.Syntax.op_letstar
              (State.Status.(State.S_MakeVar.set) Waiting_for_input_message)
              (fun function_parameter
                let '_ := function_parameter in
                State.Monad._return tt))).

  Definition result_of `{FArgs} {A : Set}
    (default : A) (m_value : State.Monad.t A) (state_value : State.state) : A :=
    let '(_, v_value) := State.Monad.run m_value state_value in
    match v_value with
    | Nonedefault
    | Some v_valuev_value
    end.

  Definition state_of `{FArgs} {A : Set}
    (m_value : State.Monad.t A) (state_value : State.state) : State.state :=
    let '(s_value, _) := State.Monad.run m_value state_value in
    s_value.

  Definition get_tick `{FArgs} : State.state Sc_rollup_tick_repr.t :=
    result_of Sc_rollup_tick_repr.initial
      State.Current_tick.(State.S_MakeVar.get).

  Definition is_input_state_monadic `{FArgs} : State.Monad.t PS.input_request :=
    State.Monad.Syntax.op_letstar State.Status.(State.S_MakeVar.get)
      (fun status
        match status with
        | Waiting_for_input_message
          State.Monad.Syntax.op_letstar
            State.Current_level.(State.S_MakeVar.get)
            (fun level
              State.Monad.Syntax.op_letstar
                State.Message_counter.(State.S_MakeVar.get)
                (fun counter
                  match counter with
                  | Some n_value
                    State.Monad._return
                      (Sc_rollup_PVM_sig.First_after level n_value)
                  | NoneState.Monad._return Sc_rollup_PVM_sig.Initial
                  end))
        | Waiting_for_reveal
          State.Monad.Syntax.op_letstar
            State.Required_reveal.(State.S_MakeVar.get)
            (fun h_value
              match h_value with
              | None
                State.Monad.internal_error
                  "Internal error: Reveal invariant broken"
              | Some h_value
                State.Monad._return
                  (Sc_rollup_PVM_sig.Needs_reveal
                    (Sc_rollup_PVM_sig.Reveal_raw_data h_value))
              end)
        | _State.Monad._return Sc_rollup_PVM_sig.No_input_required
        end).

  Definition is_input_state `{FArgs} : State.state PS.input_request :=
    result_of Sc_rollup_PVM_sig.No_input_required is_input_state_monadic.

  Definition get_status `{FArgs} : State.state status :=
    result_of Waiting_for_input_message State.Status.(State.S_MakeVar.get).

  Definition get_outbox `{FArgs} (state_value : State.state)
    : list Sc_rollup_PVM_sig.output :=
    let entries :=
      result_of nil State.Output.(State.MakeDict_sig.entries) state_value in
    List.map Pervasives.snd entries.

  Definition get_code `{FArgs} : State.state list instruction :=
    result_of nil State.Code.(State.MakeDeque_sig.to_list).

  Definition get_parsing_result `{FArgs} : State.state option bool :=
    result_of None State.Parsing_result.(State.S_MakeVar.get).

  Definition get_stack `{FArgs} : State.state list int :=
    result_of nil State.Stack.(State.MakeDeque_sig.to_list).

  Definition get_var `{FArgs} (state_value : State.state) (k_value : string)
    : option int :=
    result_of None (State.Vars.(State.MakeDict_sig.get) k_value) state_value.

  Definition get_evaluation_result `{FArgs} : State.state option bool :=
    result_of None State.Evaluation_result.(State.S_MakeVar.get).

  Definition get_is_stuck `{FArgs} : State.state option string :=
    result_of None State.Monad.is_stuck.

  Definition start_parsing `{FArgs} : State.Monad.t unit :=
    State.Monad.Syntax.op_letstar (State.Status.(State.S_MakeVar.set) Parsing)
      (fun function_parameter
        let '_ := function_parameter in
        State.Monad.Syntax.op_letstar
          (State.Parsing_result.(State.S_MakeVar.set) None)
          (fun function_parameter
            let '_ := function_parameter in
            State.Monad.Syntax.op_letstar
              (State.Parser_state.(State.S_MakeVar.set) State.SkipLayout)
              (fun function_parameter
                let '_ := function_parameter in
                State.Monad.Syntax.op_letstar
                  (State.Lexer_state.(State.S_MakeVar.set) (0, 0))
                  (fun function_parameter
                    let '_ := function_parameter in
                    State.Monad.Syntax.op_letstar
                      State.Code.(State.MakeDeque_sig.clear)
                      (fun function_parameter
                        let '_ := function_parameter in
                        State.Monad._return tt))))).

  Definition set_inbox_message_monadic `{FArgs}
    (function_parameter : PS.inbox_message) : State.Monad.t unit :=
    let '{|
      Sc_rollup_PVM_sig.inbox_message.inbox_level := inbox_level;
        Sc_rollup_PVM_sig.inbox_message.message_counter := message_counter;
        Sc_rollup_PVM_sig.inbox_message.payload := payload
        |} := function_parameter in
    let payload :=
      match Sc_rollup_inbox_message_repr.deserialize payload with
      | Pervasives.Error _None
      | Pervasives.Ok (Sc_rollup_inbox_message_repr.External payload) ⇒
        Some payload
      |
        Pervasives.Ok
          (Sc_rollup_inbox_message_repr.Internal {|
            Sc_rollup_inbox_message_repr.internal_inbox_message.payload := payload
              |}) ⇒
        match Micheline.root_value payload with
        | Micheline.String _ payloadSome payload
        | _None
        end
      end in
    match payload with
    | Some payload
      State.Monad.Syntax.op_letstar State.Boot_sector.(State.S_MakeVar.get)
        (fun boot_sector
          let msg := Pervasives.op_caret boot_sector payload in
          State.Monad.Syntax.op_letstar
            (State.Current_level.(State.S_MakeVar.set) inbox_level)
            (fun function_parameter
              let '_ := function_parameter in
              State.Monad.Syntax.op_letstar
                (State.Message_counter.(State.S_MakeVar.set)
                  (Some message_counter))
                (fun function_parameter
                  let '_ := function_parameter in
                  State.Monad.Syntax.op_letstar
                    (State.Next_message.(State.S_MakeVar.set) (Some msg))
                    (fun function_parameter
                      let '_ := function_parameter in
                      State.Monad.Syntax.op_letstar start_parsing
                        (fun function_parameter
                          let '_ := function_parameter in
                          State.Monad._return tt)))))
    | None
      State.Monad.Syntax.op_letstar
        (State.Current_level.(State.S_MakeVar.set) inbox_level)
        (fun function_parameter
          let '_ := function_parameter in
          State.Monad.Syntax.op_letstar
            (State.Message_counter.(State.S_MakeVar.set) (Some message_counter))
            (fun function_parameter
              let '_ := function_parameter in
              State.Monad.Syntax.op_letstar
                (State.Status.(State.S_MakeVar.set) Waiting_for_input_message)
                (fun function_parameter
                  let '_ := function_parameter in
                  State.Monad._return tt)))
    end.

  Definition reveal_monadic `{FArgs} (function_parameter : PS.reveal_data)
    : State.Monad.t unit :=
    let 'Sc_rollup_PVM_sig.Raw_data data := function_parameter in
    State.Monad.Syntax.op_letstar
      (State.Next_message.(State.S_MakeVar.set) (Some data))
      (fun function_parameter
        let '_ := function_parameter in
        State.Monad.Syntax.op_letstar start_parsing
          (fun function_parameter
            let '_ := function_parameter in
            State.Monad._return tt)).

  Definition ticked `{FArgs} {A : Set} (m_value : State.Monad.t A)
    : State.Monad.t A :=
    State.Monad.Syntax.op_letstar State.Current_tick.(State.S_MakeVar.get)
      (fun tick
        State.Monad.Syntax.op_letstar
          (State.Current_tick.(State.S_MakeVar.set)
            (Sc_rollup_tick_repr.next tick))
          (fun function_parameter
            let '_ := function_parameter in
            m_value)).

  Definition set_input_monadic `{FArgs} (input : PS.input)
    : State.Monad.t unit :=
    match input with
    | Sc_rollup_PVM_sig.Inbox_message m_value
      set_inbox_message_monadic m_value
    | Sc_rollup_PVM_sig.Reveal s_valuereveal_monadic s_value
    end.

  Definition set_input `{FArgs} (input : PS.input)
    : State.state State.state := state_of (ticked (set_input_monadic input)).

  Definition next_char `{FArgs} : State.Monad.t unit :=
    State.Monad.Syntax.op_letstar State.Lexer_state.(State.S_MakeVar.get)
      (fun function_parameter
        let '(start, len) := function_parameter in
        State.Lexer_state.(State.S_MakeVar.set) (start, (len +i 1))).

  Definition no_message_to_lex `{FArgs} {A : Set} (function_parameter : unit)
    : State.Monad.t A :=
    let '_ := function_parameter in
    State.Monad.internal_error "lexer: There is no input message to lex".

  Definition current_char `{FArgs} : State.Monad.t (option ascii) :=
    State.Monad.Syntax.op_letstar State.Lexer_state.(State.S_MakeVar.get)
      (fun function_parameter
        let '(start, len) := function_parameter in
        State.Monad.Syntax.op_letstar State.Next_message.(State.S_MakeVar.get)
          (fun msg
            match msg with
            | Noneno_message_to_lex tt
            | Some s_value
              if (start +i len) <i (String.length s_value) then
                State.Monad._return (Some (String.get s_value (start +i len)))
              else
                State.Monad._return None
            end)).

  Definition lexeme `{FArgs} : State.Monad.t string :=
    State.Monad.Syntax.op_letstar State.Lexer_state.(State.S_MakeVar.get)
      (fun function_parameter
        let '(start, len) := function_parameter in
        State.Monad.Syntax.op_letstar State.Next_message.(State.S_MakeVar.get)
          (fun msg
            match msg with
            | Noneno_message_to_lex tt
            | Some s_value
              State.Monad.Syntax.op_letstar
                (State.Lexer_state.(State.S_MakeVar.set) ((start +i len), 0))
                (fun function_parameter
                  let '_ := function_parameter in
                  State.Monad._return (String.sub s_value start len))
            end)).

  Definition push_int_literal `{FArgs} : State.Monad.t unit :=
    State.Monad.Syntax.op_letstar lexeme
      (fun s_value
        match Pervasives.int_of_string_opt s_value with
        | Some x_value
          State.Code.(State.MakeDeque_sig.inject) (IPush x_value)
        | None
          (* ❌ Assert instruction is not handled. *)
          assert (State.Monad.t unit) false
        end).

  Definition push_var `{FArgs} : State.Monad.t unit :=
    State.Monad.Syntax.op_letstar lexeme
      (fun s_valueState.Code.(State.MakeDeque_sig.inject) (IStore s_value)).

  Definition start_evaluating `{FArgs} : State.Monad.t unit :=
    State.Monad.Syntax.op_letstar
      (State.Status.(State.S_MakeVar.set) Evaluating)
      (fun function_parameter
        let '_ := function_parameter in
        State.Monad.Syntax.op_letstar
          (State.Evaluation_result.(State.S_MakeVar.set) None)
          (fun function_parameter
            let '_ := function_parameter in
            State.Monad._return tt)).

  Definition stop_parsing `{FArgs} (outcome : bool) : State.Monad.t unit :=
    State.Monad.Syntax.op_letstar
      (State.Parsing_result.(State.S_MakeVar.set) (Some outcome))
      (fun function_parameter
        let '_ := function_parameter in
        start_evaluating).

  Definition stop_evaluating `{FArgs} (outcome : bool) : State.Monad.t unit :=
    State.Monad.Syntax.op_letstar
      (State.Evaluation_result.(State.S_MakeVar.set) (Some outcome))
      (fun function_parameter
        let '_ := function_parameter in
        State.Status.(State.S_MakeVar.set) Waiting_for_input_message).

  Definition parse `{FArgs} : State.Monad.t unit :=
    let produce_add :=
      State.Monad.Syntax.op_letstar lexeme
        (fun function_parameter
          let '_ := function_parameter in
          State.Monad.Syntax.op_letstar next_char
            (fun function_parameter
              let '_ := function_parameter in
              State.Monad.Syntax.op_letstar
                (State.Code.(State.MakeDeque_sig.inject) IAdd)
                (fun function_parameter
                  let '_ := function_parameter in
                  State.Monad._return tt))) in
    let produce_int :=
      State.Monad.Syntax.op_letstar push_int_literal
        (fun function_parameter
          let '_ := function_parameter in
          State.Monad.Syntax.op_letstar
            (State.Parser_state.(State.S_MakeVar.set) State.SkipLayout)
            (fun function_parameter
              let '_ := function_parameter in
              State.Monad._return tt)) in
    let produce_var :=
      State.Monad.Syntax.op_letstar push_var
        (fun function_parameter
          let '_ := function_parameter in
          State.Monad.Syntax.op_letstar
            (State.Parser_state.(State.S_MakeVar.set) State.SkipLayout)
            (fun function_parameter
              let '_ := function_parameter in
              State.Monad._return tt)) in
    let is_digit (d_value : ascii) : bool :=
      (Compare.Char.(Compare.S.op_gteq) d_value "0" % char) &&
      (Compare.Char.(Compare.S.op_lteq) d_value "9" % char) in
    let is_letter (d_value : ascii) : bool :=
      ((Compare.Char.(Compare.S.op_gteq) d_value "a" % char) &&
      (Compare.Char.(Compare.S.op_lteq) d_value "z" % char)) ||
      ((Compare.Char.(Compare.S.op_gteq) d_value "A" % char) &&
      (Compare.Char.(Compare.S.op_lteq) d_value "Z" % char)) in
    let is_identifier_char (d_value : ascii) : bool :=
      (is_letter d_value) ||
      ((is_digit d_value) ||
      ((Compare.Char.(Compare.S.op_eq) d_value ":" % char) ||
      (Compare.Char.(Compare.S.op_eq) d_value "%" % char))) in
    State.Monad.Syntax.op_letstar State.Parser_state.(State.S_MakeVar.get)
      (fun parser_state
        match parser_state with
        | State.ParseInt
          State.Monad.Syntax.op_letstar current_char
            (fun char_value
              match
                (char_value,
                  match char_value with
                  | Some d_valueis_digit d_value
                  | _false
                  end) with
              | (Some d_value, true)next_char
              | (Some "+" % char, _)
                State.Monad.Syntax.op_letstar produce_int
                  (fun function_parameter
                    let '_ := function_parameter in
                    State.Monad.Syntax.op_letstar produce_add
                      (fun function_parameter
                        let '_ := function_parameter in
                        State.Monad._return tt))
              | (Some (" " % char | "010" % char), _)
                State.Monad.Syntax.op_letstar produce_int
                  (fun function_parameter
                    let '_ := function_parameter in
                    State.Monad.Syntax.op_letstar next_char
                      (fun function_parameter
                        let '_ := function_parameter in
                        State.Monad._return tt))
              | (None, _)
                State.Monad.Syntax.op_letstar push_int_literal
                  (fun function_parameter
                    let '_ := function_parameter in
                    stop_parsing true)
              | (_, _)stop_parsing false
              end)
        | State.ParseVar
          State.Monad.Syntax.op_letstar current_char
            (fun char_value
              match
                (char_value,
                  match char_value with
                  | Some d_valueis_identifier_char d_value
                  | _false
                  end) with
              | (Some d_value, true)next_char
              | (Some "+" % char, _)
                State.Monad.Syntax.op_letstar produce_var
                  (fun function_parameter
                    let '_ := function_parameter in
                    State.Monad.Syntax.op_letstar produce_add
                      (fun function_parameter
                        let '_ := function_parameter in
                        State.Monad._return tt))
              | (Some (" " % char | "010" % char), _)
                State.Monad.Syntax.op_letstar produce_var
                  (fun function_parameter
                    let '_ := function_parameter in
                    State.Monad.Syntax.op_letstar next_char
                      (fun function_parameter
                        let '_ := function_parameter in
                        State.Monad._return tt))
              | (None, _)
                State.Monad.Syntax.op_letstar push_var
                  (fun function_parameter
                    let '_ := function_parameter in
                    stop_parsing true)
              | (_, _)stop_parsing false
              end)
        | State.SkipLayout
          State.Monad.Syntax.op_letstar current_char
            (fun char_value
              match
                (char_value,
                  match char_value with
                  | Some d_valueis_digit d_value
                  | _false
                  end,
                  match char_value with
                  | Some d_valueis_letter d_value
                  | _false
                  end) with
              | (Some (" " % char | "010" % char), _, _)next_char
              | (Some "+" % char, _, _)produce_add
              | (Some d_value, true, _)
                State.Monad.Syntax.op_letstar lexeme
                  (fun function_parameter
                    let '_ := function_parameter in
                    State.Monad.Syntax.op_letstar next_char
                      (fun function_parameter
                        let '_ := function_parameter in
                        State.Monad.Syntax.op_letstar
                          (State.Parser_state.(State.S_MakeVar.set)
                            State.ParseInt)
                          (fun function_parameter
                            let '_ := function_parameter in
                            State.Monad._return tt)))
              | (Some d_value, _, true)
                State.Monad.Syntax.op_letstar lexeme
                  (fun function_parameter
                    let '_ := function_parameter in
                    State.Monad.Syntax.op_letstar next_char
                      (fun function_parameter
                        let '_ := function_parameter in
                        State.Monad.Syntax.op_letstar
                          (State.Parser_state.(State.S_MakeVar.set)
                            State.ParseVar)
                          (fun function_parameter
                            let '_ := function_parameter in
                            State.Monad._return tt)))
              | (None, _, _)stop_parsing true
              | (_, _, _)stop_parsing false
              end)
        end).

  Definition output `{FArgs}
    (function_parameter : Contract_hash.t × Entrypoint_repr.t)
    : int State.Monad.t unit :=
    let '(destination, entrypoint) := function_parameter in
    fun (v_value : int) ⇒
      State.Monad.Syntax.op_letstar State.Output_counter.(State.S_MakeVar.get)
        (fun counter
          State.Monad.Syntax.op_letstar
            (State.Output_counter.(State.S_MakeVar.set) (Z.succ counter))
            (fun function_parameter
              let '_ := function_parameter in
              let unparsed_parameters :=
                Micheline.strip_locations (Micheline.Int tt (Z.of_int v_value))
                in
              let transaction :=
                {|
                  Sc_rollup_outbox_message_repr.transaction.unparsed_parameters
                    := unparsed_parameters;
                  Sc_rollup_outbox_message_repr.transaction.destination :=
                    destination;
                  Sc_rollup_outbox_message_repr.transaction.entrypoint :=
                    entrypoint; |} in
              let message :=
                Sc_rollup_outbox_message_repr.Atomic_transaction_batch
                  {|
                    Sc_rollup_outbox_message_repr.t.Atomic_transaction_batch.transactions
                      := [ transaction ]; |} in
              State.Monad.Syntax.op_letstar
                State.Current_level.(State.S_MakeVar.get)
                (fun outbox_level
                  let output :=
                    {| Sc_rollup_PVM_sig.output.outbox_level := outbox_level;
                      Sc_rollup_PVM_sig.output.message_index := counter;
                      Sc_rollup_PVM_sig.output.message := message; |} in
                  State.Output.(State.MakeDict_sig.set) (Z.to_string counter)
                    output))).

  Definition identifies_target_contract `{FArgs} (x_value : string)
    : option (Contract_hash.t × Entrypoint_repr.t) :=
    match String.split_on_char "%" % char x_value with
    | cons destination entrypoint
      match Contract_hash.of_b58check_opt destination with
      | None
        if Compare.String.(Compare.S.op_eq) x_value "out" then
          return× (Contract_hash.zero, Entrypoint_repr.default)
        else
          Error_monad.Option_syntax.fail
      | Some destination
        let× entrypoint :=
          match entrypoint with
          | []return× Entrypoint_repr.default
          | _
            let× entrypoint :=
              Non_empty_string.of_string (String.concat "" entrypoint) in
            let× entrypoint := Entrypoint_repr.of_annot_lax_opt entrypoint in
            return× entrypoint
          end in
        return× (destination, entrypoint)
      end
    | []Error_monad.Option_syntax.fail
    end.

  Definition evaluate `{FArgs} : State.Monad.t unit :=
    State.Monad.Syntax.op_letstar State.Code.(State.MakeDeque_sig.pop)
      (fun i_value
        match i_value with
        | Nonestop_evaluating true
        | Some (IPush x_value) ⇒ State.Stack.(State.MakeDeque_sig.push) x_value
        | Some (IStore x_value) ⇒
          let len := String.length x_value in
          if
            (len >i 5) &&
            (Compare.String.(Compare.S.op_eq) (String.sub x_value 0 5) "hash:")
          then
            let hash_value := String.sub x_value 5 (len -i 5) in
            match PS.Input_hash.(S.HASH.of_b58check_opt) hash_value with
            | Nonestop_evaluating false
            | Some hash_value
              State.Monad.Syntax.op_letstar
                (State.Required_reveal.(State.S_MakeVar.set) (Some hash_value))
                (fun function_parameter
                  let '_ := function_parameter in
                  State.Monad.Syntax.op_letstar
                    (State.Status.(State.S_MakeVar.set) Waiting_for_reveal)
                    (fun function_parameter
                      let '_ := function_parameter in
                      State.Monad._return tt))
            end
          else
            State.Monad.Syntax.op_letstar State.Stack.(State.MakeDeque_sig.top)
              (fun v_value
                match v_value with
                | Nonestop_evaluating false
                | Some v_value
                  match identifies_target_contract x_value with
                  | Some contract_entrypoint
                    output contract_entrypoint v_value
                  | NoneState.Vars.(State.MakeDict_sig.set) x_value v_value
                  end
                end)
        | Some IAdd
          State.Monad.Syntax.op_letstar State.Stack.(State.MakeDeque_sig.pop)
            (fun v_value
              match v_value with
              | Nonestop_evaluating false
              | Some x_value
                State.Monad.Syntax.op_letstar
                  State.Stack.(State.MakeDeque_sig.pop)
                  (fun v_value
                    match v_value with
                    | Nonestop_evaluating false
                    | Some y_value
                      State.Stack.(State.MakeDeque_sig.push)
                        (x_value +i y_value)
                    end)
              end)
        end).

  Definition reboot `{FArgs} : State.Monad.t unit :=
    State.Monad.Syntax.op_letstar
      (State.Status.(State.S_MakeVar.set) Waiting_for_input_message)
      (fun function_parameter
        let '_ := function_parameter in
        State.Monad.Syntax.op_letstar State.Stack.(State.MakeDeque_sig.clear)
          (fun function_parameter
            let '_ := function_parameter in
            State.Monad.Syntax.op_letstar State.Code.(State.MakeDeque_sig.clear)
              (fun function_parameter
                let '_ := function_parameter in
                State.Monad._return tt))).

  Definition eval_step `{FArgs} : State.Monad.t unit :=
    State.Monad.Syntax.op_letstar State.Monad.is_stuck
      (fun x_value
        match x_value with
        | Some _reboot
        | None
          State.Monad.Syntax.op_letstar State.Status.(State.S_MakeVar.get)
            (fun status
              match status with
              | Haltedboot
              | (Waiting_for_input_message | Waiting_for_reveal) ⇒
                State.Monad.Syntax.op_letstar
                  State.Next_message.(State.S_MakeVar.get)
                  (fun msg
                    match msg with
                    | None
                      State.Monad.internal_error
                        "An input state was not provided an input."
                    | Some _start_parsing
                    end)
              | Parsingparse
              | Evaluatingevaluate
              end)
        end).

  Definition eval `{FArgs} (state_value : State.state) : State.state :=
    state_of (ticked eval_step) state_value.

  Definition step_transition `{FArgs}
    (input_given : option PS.input) (state_value : State.state)
    : State.state × PS.input_request :=
    let request := is_input_state state_value in
    let state_value :=
      match request with
      | Sc_rollup_PVM_sig.No_input_requiredeval state_value
      | (Sc_rollup_PVM_sig.Initial | Sc_rollup_PVM_sig.First_after _ _) ⇒
        match input_given with
        | Some ((Sc_rollup_PVM_sig.Inbox_message _) as input_given) ⇒
          set_input input_given state_value
        | (None | Some (Sc_rollup_PVM_sig.Reveal _)) ⇒
          state_of
            ((State.Monad.internal_error (A := unit))
              "Invalid set_input: expecting inbox message, got a reveal.")
            state_value
        end
      | Sc_rollup_PVM_sig.Needs_reveal _hash
        match input_given with
        | Some ((Sc_rollup_PVM_sig.Reveal _) as input_given) ⇒
          set_input input_given state_value
        | (None | Some (Sc_rollup_PVM_sig.Inbox_message _)) ⇒
          state_of
            ((State.Monad.internal_error (A := unit))
              "Invalid set_input: expecting a reveal, got an inbox message.")
            state_value
        end
      end in
    (state_value, request).

  Definition verify_proof `{FArgs}
    (input_given : option PS.input) (proof_value : Context.(P.proof))
    : M? PS.input_request :=
    let result_value :=
      Context.(P.verify_proof) proof_value (step_transition input_given) in
    match result_value with
    | None
      Error_monad.Lwt_tzresult_syntax.fail
        (Build_extensible "Arith_proof_verification_failed" unit tt)
    | Some (_state, request)return? request
    end.

  Definition produce_proof `{FArgs}
    (context_value : Context.(P.Tree).(Context.TREE.t))
    (input_given : option PS.input)
    (state_value : Context.(P.Tree).(Context.TREE.tree)) : M? proof :=
    let result_value :=
      Context.(P.produce_proof) context_value state_value
        (step_transition input_given) in
    match result_value with
    | Some (tree_proof, _requested)return? tree_proof
    | None
      Error_monad.Lwt_tzresult_syntax.fail
        (Build_extensible "Arith_proof_production_failed" unit tt)
    end.

  Definition verify_origination_proof `{FArgs}
    (proof_value : proof) (boot_sector : string) : bool :=
    let before := Context.(P.proof_before) proof_value in
    if
      Sc_rollup_repr.State_hash.op_ltgt before reference_initial_state_hash
    then
      false
    else
      let result_value :=
        Context.(P.verify_proof) proof_value
          (fun (state_value : Context.(P.Tree).(Context.TREE.tree)) ⇒
            let state_value := install_boot_sector state_value boot_sector in
            (state_value, tt)) in
      match result_value with
      | Nonefalse
      | Some (_, _)true
      end.

  Definition produce_origination_proof `{FArgs}
    (context_value : Context.(P.Tree).(Context.TREE.t)) (boot_sector : string)
    : M? proof :=
    let state_value := initial_state context_value in
    let result_value :=
      Context.(P.produce_proof) context_value state_value
        (fun (state_value : Context.(P.Tree).(Context.TREE.tree)) ⇒
          let state_value := install_boot_sector state_value boot_sector in
          (state_value, tt)) in
    match result_value with
    | Some (proof_value, _)return? proof_value
    | None
      Error_monad.Lwt_tzresult_syntax.fail
        (Build_extensible "Arith_proof_production_failed" unit tt)
    end.

  Module output_proof.
    Record record `{FArgs} : Set := Build {
      output_proof : Context.(P.proof);
      output_proof_state : hash;
      output_proof_output : PS.output;
    }.
    Definition with_output_proof `{FArgs} output_proof (r : record) :=
      Build _ _ _ _ output_proof r.(output_proof_state) r.(output_proof_output).
    Definition with_output_proof_state `{FArgs} output_proof_state
      (r : record) :=
      Build _ _ _ _ r.(output_proof) output_proof_state r.(output_proof_output).
    Definition with_output_proof_output `{FArgs} output_proof_output
      (r : record) :=
      Build _ _ _ _ r.(output_proof) r.(output_proof_state) output_proof_output.
  End output_proof.
  Definition output_proof `{FArgs} := output_proof.record.

  Definition output_proof_encoding `{FArgs}
    : Data_encoding.encoding output_proof :=
    Data_encoding.conv
      (fun (function_parameter : output_proof) ⇒
        let '{|
          output_proof.output_proof := output_proof;
            output_proof.output_proof_state := output_proof_state;
            output_proof.output_proof_output := output_proof_output
            |} := function_parameter in
        (output_proof, output_proof_state, output_proof_output))
      (fun (function_parameter : Context.(P.proof) × hash × PS.output) ⇒
        let '(output_proof, output_proof_state, output_proof_output) :=
          function_parameter in
        {| output_proof.output_proof := output_proof;
          output_proof.output_proof_state := output_proof_state;
          output_proof.output_proof_output := output_proof_output; |}) None
      (Data_encoding.obj3
        (Data_encoding.req None None "output_proof" Context.(P.proof_encoding))
        (Data_encoding.req None None "output_proof_state"
          Sc_rollup_repr.State_hash.encoding)
        (Data_encoding.req None None "output_proof_output" PS.output_encoding)).

  Definition output_of_output_proof `{FArgs} (s_value : output_proof)
    : PS.output := s_value.(output_proof.output_proof_output).

  Definition state_of_output_proof `{FArgs} (s_value : output_proof) : hash :=
    s_value.(output_proof.output_proof_state).

  Definition output_key `{FArgs} (output : PS.output) : string :=
    Z.to_string output.(Sc_rollup_PVM_sig.output.message_index).

  Definition has_output `{FArgs} (output : PS.output) (tree_value : State.state)
    : State.state × bool :=
    let equal :=
      State.Output.(State.MakeDict_sig.mapped_to) (output_key output) output
        tree_value in
    (tree_value, equal).

  Definition verify_output_proof `{FArgs} (p_value : output_proof) : bool :=
    let transition := has_output p_value.(output_proof.output_proof_output) in
    let result_value :=
      Context.(P.verify_proof) p_value.(output_proof.output_proof) transition in
    match result_value with
    | Nonefalse
    | Some _true
    end.

  Definition produce_output_proof `{FArgs}
    (context_value : Context.(P.Tree).(Context.TREE.t))
    (state_value : Context.(P.Tree).(Context.TREE.tree))
    (output_proof_output : PS.output)
    : Pervasives.result output_proof Error_monad._error :=
    let output_proof_state := state_hash state_value in
    let result_value :=
      Context.(P.produce_proof) context_value state_value
        (has_output output_proof_output) in
    match result_value with
    | Some (output_proof, true)
      return?
        {| output_proof.output_proof := output_proof;
          output_proof.output_proof_state := output_proof_state;
          output_proof.output_proof_output := output_proof_output; |}
    | Some (_, false)
      Error_monad.Lwt_result_syntax.fail
        (Build_extensible "Arith_invalid_claim_about_outbox" unit tt)
    | None
      Error_monad.Lwt_result_syntax.fail
        (Build_extensible "Arith_output_proof_production_failed" unit tt)
    end.

  (* Make *)
  Definition functor `{FArgs} :=
    {|
      S.pp := pp;
      S.proof_encoding := proof_encoding;
      S.proof_start_state := proof_start_state;
      S.proof_stop_state := proof_stop_state;
      S.state_hash := state_hash;
      S.initial_state := initial_state;
      S.install_boot_sector := install_boot_sector;
      S.is_input_state := is_input_state;
      S.set_input := set_input;
      S.eval := eval;
      S.verify_proof := verify_proof;
      S.produce_proof := produce_proof;
      S.verify_origination_proof := verify_origination_proof;
      S.produce_origination_proof := produce_origination_proof;
      S.output_proof_encoding := output_proof_encoding;
      S.output_of_output_proof := output_of_output_proof;
      S.state_of_output_proof := state_of_output_proof;
      S.verify_output_proof := verify_output_proof;
      S.produce_output_proof := produce_output_proof;
      S.name := name;
      S.parse_boot_sector := parse_boot_sector;
      S.pp_boot_sector := pp_boot_sector;
      S.get_tick := get_tick;
      S.get_status := get_status;
      S.get_outbox := get_outbox;
      S.equal_instruction := equal_instruction;
      S.pp_instruction := pp_instruction;
      S.get_parsing_result := get_parsing_result;
      S.get_code := get_code;
      S.get_stack := get_stack;
      S.get_var := get_var;
      S.get_evaluation_result := get_evaluation_result;
      S.get_is_stuck := get_is_stuck
    |}.
End Make.
Definition Make {Context_Tree_t Context_Tree_tree Context_proof : Set}
  (Context :
    P (Tree_t := Context_Tree_t) (Tree_tree := Context_Tree_tree)
      (proof := Context_proof))
  : S (state := Context.(P.Tree).(Context.TREE.tree))
    (context := Context.(P.Tree).(Context.TREE.t)) (proof := Context.(P.proof))
    (output_proof := _) (status := _) (instruction := _) :=
  let '_ := Make.Build_FArgs Context in
  Make.functor.

Definition Protocol_implementation :=
  Make
    (let Tree :=
      let mem := Context.Tree.(Context.TREE.mem) in
      let mem_tree := Context.Tree.(Context.TREE.mem_tree) in
      let find := Context.Tree.(Context.TREE.find) in
      let find_tree := Context.Tree.(Context.TREE.find_tree) in
      let list_value := Context.Tree.(Context.TREE.list_value) in
      let length := Context.Tree.(Context.TREE.length) in
      let add := Context.Tree.(Context.TREE.add) in
      let add_tree := Context.Tree.(Context.TREE.add_tree) in
      let remove := Context.Tree.(Context.TREE.remove) in
      let fold {a : Set} := Context.Tree.(Context.TREE.fold) in
      let config_value := Context.Tree.(Context.TREE.config_value) in
      let empty := Context.Tree.(Context.TREE.empty) in
      let is_empty := Context.Tree.(Context.TREE.is_empty) in
      let kind_value := Context.Tree.(Context.TREE.kind_value) in
      let to_value := Context.Tree.(Context.TREE.to_value) in
      let of_value := Context.Tree.(Context.TREE.of_value) in
      let hash_value := Context.Tree.(Context.TREE.hash_value) in
      let equal := Context.Tree.(Context.TREE.equal) in
      let clear := Context.Tree.(Context.TREE.clear) in
      let tree : Set := Context.tree in
      let t : Set := Context.t in
      let key : Set := list string in
      let value : Set := bytes in
      {|
        Context.TREE.mem := mem;
        Context.TREE.mem_tree := mem_tree;
        Context.TREE.find := find;
        Context.TREE.find_tree := find_tree;
        Context.TREE.list_value := list_value;
        Context.TREE.length := length;
        Context.TREE.add := add;
        Context.TREE.add_tree := add_tree;
        Context.TREE.remove := remove;
        Context.TREE.fold _ := fold;
        Context.TREE.config_value := config_value;
        Context.TREE.empty := empty;
        Context.TREE.is_empty := is_empty;
        Context.TREE.kind_value := kind_value;
        Context.TREE.to_value := to_value;
        Context.TREE.of_value := of_value;
        Context.TREE.hash_value := hash_value;
        Context.TREE.equal := equal;
        Context.TREE.clear := clear
      |} in
    let tree : Set := Context.tree in
    let hash_tree (t_value : Context.tree) : Sc_rollup_repr.State_hash.t :=
      match
        Sc_rollup_repr.State_hash.context_hash_to_state_hash
          (Tree.(Context.TREE.hash_value) t_value) with
      | Pervasives.Ok sthsth
      | Pervasives.Error _
        (* ❌ Assert instruction is not handled. *)
        assert Sc_rollup_repr.State_hash.t false
      end in
    let proof : Set := Context.Proof.t Context.Proof.tree in
    let verify_proof {A : Set}
      (p_value : Context.Proof.t Context.Proof.tree)
      (f_value : Context.tree Context.tree × A)
      : option (Context.tree × A) :=
      id Result.to_option (Context.verify_tree_proof p_value f_value) in
    let produce_proof {A B C D : Set} (_context : A) (_state : B) (_f : C)
      : option D :=
      None in
    let kinded_hash_to_state_hash (function_parameter : Context.Proof.kinded_hash)
      : M? Sc_rollup_repr.State_hash.t :=
      match function_parameter with
      | (Context.Proof.KValue hash_value | Context.Proof.KNode hash_value) ⇒
        Sc_rollup_repr.State_hash.context_hash_to_state_hash hash_value
      end in
    let proof_before {A : Set} (proof_value : Context.Proof.t A)
      : Sc_rollup_repr.State_hash.t :=
      match kinded_hash_to_state_hash proof_value.(Context.Proof.t.before) with
      | Pervasives.Ok prfprf
      | Pervasives.Error _
        (* ❌ Assert instruction is not handled. *)
        assert Sc_rollup_repr.State_hash.t false
      end in
    let proof_after {A : Set} (proof_value : Context.Proof.t A)
      : Sc_rollup_repr.State_hash.t :=
      match kinded_hash_to_state_hash proof_value.(Context.Proof.t.after) with
      | Pervasives.Ok prfprf
      | Pervasives.Error _
        (* ❌ Assert instruction is not handled. *)
        assert Sc_rollup_repr.State_hash.t false
      end in
    let proof_encoding :=
      Context.Proof_encoding.V2.Tree32.(Context.PROOF_ENCODING.tree_proof_encoding)
      in
    {|
      P.Tree := Tree;
      P.hash_tree := hash_tree;
      P.proof_encoding := proof_encoding;
      P.proof_before := proof_before;
      P.proof_after := proof_after;
      P.verify_proof _ := verify_proof;
      P.produce_proof _ := produce_proof
    |}).