Skip to main content

🦏 Sc_rollup_wasm.v

Translated OCaml

See proofs, 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_wasm_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 "WASM_invalid_claim_about_outbox" then
            Some tt
          else None
        end)
      (fun (function_parameter : unit) ⇒
        let '_ := function_parameter in
        Build_extensible "WASM_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_wasm_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 "WASM_output_proof_production_failed" then
            Some tt
          else None
        end)
      (fun (function_parameter : unit) ⇒
        let '_ := function_parameter in
        Build_extensible "WASM_output_proof_production_failed" unit tt) in
  let msg := "Proof production failed" in
  Error_monad.register_error_kind Error_monad.Permanent
    "sc_rollup_wasm_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 "WASM_proof_production_failed" then
          Some tt
        else None
      end)
    (fun (function_parameter : unit) ⇒
      let '_ := function_parameter in
      Build_extensible "WASM_proof_production_failed" unit tt).

Module V2_0_0.
  Definition reference_initial_state_hash : Sc_rollup_repr.State_hash.t :=
    Sc_rollup_repr.State_hash.of_b58check_exn
      "scs11pDQTn37TBnWgQAiCPdMAcQPiXARjg9ZZVmLx26sZwxeSxovE5".

  Module PS := Sc_rollup_PVM_sig.

  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);
      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 : 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 : state 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] gets the total tick counter for the given PVM state.
      get_tick : state Sc_rollup_tick_repr.t;
      
PVM status
      status := status;
      
[get_status state] gives you the current execution status for the PVM.
      get_status : state status;
      get_outbox : Raw_level_repr.t state list Sc_rollup_PVM_sig.output;
    }.
  End S.
  Definition S := @S.signature.
  Arguments S {_ _ _ _ _}.

  Module Make.
    Class FArgs {Context_Tree_t Context_Tree_tree Context_proof : Set} := {
      Make_backend :
         {Tree_t Tree_tree : Set},
         (Tree :
          Context.TREE (t := Tree_t) (tree := Tree_tree) (key := list string)
            (value := bytes)), Wasm_2_0_0.S (tree := Tree.(Context.TREE.tree));
      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 := "wasm_2_0_0".

    Definition parse_boot_sector `{FArgs} (s_value : string) : option string :=
      Hex.to_string (Hex.Hex 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 :=
    | Computing : status
    | Waiting_for_input_message : status
    | Waiting_for_reveal : Sc_rollup_PVM_sig.reveal status.

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

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

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

        Definition bind `{FArgs} {A B C D : Set}
          (m_value : A B × C) (f_value : C B D) (state_value : A)
          : D :=
          let '(state_value, res) := m_value state_value in
          f_value res state_value.

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

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

        Definition get `{FArgs} {A : Set} (s_value : A) : A × A :=
          (s_value, s_value).

        Definition set `{FArgs} {A B : Set}
          (s_value : A) (function_parameter : B) : A × unit :=
          let '_ := function_parameter in
          (s_value, tt).

        Definition lift `{FArgs} {A B : Set} (m_value : A) (s_value : B)
          : B × A := id (fun (r_value : A) ⇒ (s_value, r_value)) m_value.
      End Monad.
    End State.

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

    Definition WASM_machine `{FArgs} := Make_backend Tree.

    Definition pp `{FArgs} {A : Set} (_state : A)
      : Format.formatter unit unit :=
      fun (fmt : Format.formatter) ⇒
        fun (function_parameter : unit) ⇒
          let '_ := function_parameter in
          Format.pp_print_string fmt "<wasm-state>".

    Definition initial_state `{FArgs}
      (empty : Context.(P.Tree).(Context.TREE.tree))
      : Context.(P.Tree).(Context.TREE.tree) :=
      let state_value :=
        Tree.(Context.TREE.add) empty [ "wasm-version" ]
          (Bytes.of_string "2.0.0") in
      state_value.

    Definition install_boot_sector `{FArgs}
      (state_value : Context.(P.Tree).(Context.TREE.tree))
      (boot_sector : string) : Context.(P.Tree).(Context.TREE.tree) :=
      WASM_machine.(Wasm_2_0_0.S.install_boot_sector) boot_sector 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 result_of `{FArgs} {A : Set}
      (m_value : State.Monad.t A) (state_value : State.state) : A :=
      let '(_, v_value) := State.Monad.run m_value state_value in
      v_value.

    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_aux `{FArgs} : State.Monad.t Sc_rollup_tick_repr.t :=
      State.Monad.Syntax.op_letstar State.Monad.get
        (fun s_value
          State.Monad.Syntax.op_letstar
            (State.Monad.lift (WASM_machine.(Wasm_2_0_0.S.get_info) s_value))
            (fun info_value
              State.Monad._return
                (Sc_rollup_tick_repr.of_z
                  info_value.(Wasm_2_0_0.info.current_tick)))).

    Definition get_tick `{FArgs} : State.state Sc_rollup_tick_repr.t :=
      result_of get_tick_aux.

    Definition get_status_aux `{FArgs} : State.Monad.t status :=
      State.Monad.Syntax.op_letstar State.Monad.get
        (fun s_value
          State.Monad.Syntax.op_letstar
            (State.Monad.lift (WASM_machine.(Wasm_2_0_0.S.get_info) s_value))
            (fun info_value
              State.Monad._return
                match info_value.(Wasm_2_0_0.info.input_request) with
                | Wasm_2_0_0.No_input_requiredComputing
                | Wasm_2_0_0.Input_requiredWaiting_for_input_message
                |
                  Wasm_2_0_0.Reveal_required
                    (Wasm_2_0_0.Reveal_raw_data hash_value) ⇒
                  match
                    Data_encoding.Binary.of_string_opt
                      Sc_rollup_PVM_sig.Reveal_hash.encoding
                      (Wasm_2_0_0.reveal_hash_to_string hash_value) with
                  | Some hash_value
                    Waiting_for_reveal
                      (Sc_rollup_PVM_sig.Reveal_raw_data hash_value)
                  | None
                    Waiting_for_reveal
                      (Sc_rollup_PVM_sig.Reveal_raw_data
                        Sc_rollup_PVM_sig.Reveal_hash.zero)
                  end
                | Wasm_2_0_0.Reveal_required Wasm_2_0_0.Reveal_metadata
                  Waiting_for_reveal Sc_rollup_PVM_sig.Reveal_metadata
                end)).

    Definition get_last_message_read `{FArgs}
      : State.Monad.t (option (M? Raw_level_repr.raw_level × Z.t)) :=
      State.Monad.Syntax.op_letstar State.Monad.get
        (fun s_value
          State.Monad.Syntax.op_letstar
            (State.Monad.lift (WASM_machine.(Wasm_2_0_0.S.get_info) s_value))
            (fun info_value
              State.Monad._return
                match info_value.(Wasm_2_0_0.info.last_input_read) with
                |
                  Some {|
                    Wasm_2_0_0.input.inbox_level := inbox_level;
                      Wasm_2_0_0.input.message_counter := message_counter
                      |} ⇒
                  let inbox_level :=
                    Raw_level_repr.of_int32_non_negative inbox_level in
                  Some (inbox_level, message_counter)
                | _None
                end)).

    Definition is_input_state_aux `{FArgs} : State.Monad.t PS.input_request :=
      State.Monad.Syntax.op_letstar get_status_aux
        (fun status
          match status with
          | Waiting_for_input_message
            State.Monad.Syntax.op_letstar get_last_message_read
              (fun last_read
                match last_read with
                | Some (level, n_value)
                  match level with
                  | Pervasives.Ok lvl
                    State.Monad._return
                      (Sc_rollup_PVM_sig.First_after lvl n_value)
                  | Pervasives.Error _
                    (* ❌ Assert instruction is not handled. *)
                    assert (State.Monad.t PS.input_request) false
                  end
                | NoneState.Monad._return Sc_rollup_PVM_sig.Initial
                end)
          | ComputingState.Monad._return Sc_rollup_PVM_sig.No_input_required
          | Waiting_for_reveal reveal
            State.Monad._return (Sc_rollup_PVM_sig.Needs_reveal reveal)
          end).

    Definition is_input_state `{FArgs} : State.state PS.input_request :=
      result_of is_input_state_aux.

    Definition get_status `{FArgs} : State.state status :=
      result_of get_status_aux.

    #[bypass_check(guard)]
    Definition get_outbox `{FArgs}
      (outbox_level : Raw_level_repr.raw_level)
      (state_value : Context.(P.Tree).(Context.TREE.tree)) : list PS.output :=
      let outbox_level_int32 :=
        Internal_errors.ignore_errors
          (Raw_level_repr.to_int32_non_negative outbox_level) in
      let fix aux (outbox : list PS.output) (message_index : Z.t)
        {struct message_index} : list PS.output :=
        let output :=
          {| Wasm_2_0_0.output.outbox_level := outbox_level_int32;
            Wasm_2_0_0.output.message_index := message_index; |} in
        let res := WASM_machine.(Wasm_2_0_0.S.get_output) output state_value in
        match res with
        | NoneList.rev outbox
        | Some msg
          let serialized := Sc_rollup_outbox_message_repr.unsafe_of_string msg
            in
          match Sc_rollup_outbox_message_repr.deserialize serialized with
          | Pervasives.Error _aux outbox (Z.succ message_index)
          | Pervasives.Ok message
            let output :=
              {| Sc_rollup_PVM_sig.output.outbox_level := outbox_level;
                Sc_rollup_PVM_sig.output.message_index := message_index;
                Sc_rollup_PVM_sig.output.message := message; |} in
            aux (cons output outbox) (Z.succ message_index)
          end
        end in
      aux nil Z.zero.

    Definition set_input_state `{FArgs} (input : PS.input)
      : State.Monad.t unit :=
      match input with
      | Sc_rollup_PVM_sig.Inbox_message input
        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
            |} := input in
        State.Monad.Syntax.op_letstar State.Monad.get
          (fun s_value
            let inbox_level :=
              match Raw_level_repr.to_int32_non_negative inbox_level with
              | Pervasives.Ok lvllvl
              | Pervasives.Error _
                (* ❌ Assert instruction is not handled. *)
                assert Bounded.Non_negative_int32.(Bounded.S.t) false
              end in
            State.Monad.Syntax.op_letstar
              (State.Monad.lift
                (WASM_machine.(Wasm_2_0_0.S.set_input_step)
                  {| Wasm_2_0_0.input.inbox_level := inbox_level;
                    Wasm_2_0_0.input.message_counter := message_counter; |}
                  payload s_value)) (fun s_valueState.Monad.set s_value))
      | Sc_rollup_PVM_sig.Reveal (Sc_rollup_PVM_sig.Raw_data data) ⇒
        State.Monad.Syntax.op_letstar State.Monad.get
          (fun s_value
            State.Monad.Syntax.op_letstar
              (State.Monad.lift
                (WASM_machine.(Wasm_2_0_0.S.reveal_step) (Bytes.of_string data)
                  s_value)) (fun s_valueState.Monad.set s_value))
      | Sc_rollup_PVM_sig.Reveal (Sc_rollup_PVM_sig.Metadata metadata) ⇒
        let metadata_bytes :=
          Data_encoding.Binary.to_bytes_exn None
            Sc_rollup_metadata_repr.encoding metadata in
        State.Monad.Syntax.op_letstar State.Monad.get
          (fun s_value
            State.Monad.Syntax.op_letstar
              (State.Monad.lift
                (WASM_machine.(Wasm_2_0_0.S.reveal_step) metadata_bytes s_value))
              (fun s_valueState.Monad.set s_value))
      | Sc_rollup_PVM_sig.Reveal (Sc_rollup_PVM_sig.Dal_page _content_opt) ⇒
        (* ❌ Assert instruction is not handled. *)
        assert (State.Monad.t unit) false
      end.

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

    Definition eval_step `{FArgs} : State.Monad.t unit :=
      State.Monad.Syntax.op_letstar State.Monad.get
        (fun s_value
          State.Monad.Syntax.op_letstar
            (State.Monad.lift (WASM_machine.(Wasm_2_0_0.S.compute_step) s_value))
            (fun s_valueState.Monad.set s_value)).

    Definition eval `{FArgs} (state_value : State.state) : State.state :=
      state_of 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
        | _
          match input_given with
          | Some inputset_input input state_value
          | Nonestate_value
          end
        end in
      (state_value, request).

    Definition verify_proof `{FArgs}
      (input_given : option PS.input) (proof_value : 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_result_syntax.tzfail
          (Build_extensible "WASM_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_result_syntax.tzfail
          (Build_extensible "WASM_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 (Tree.(Context.TREE.empty) 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 (tree_proof, _)return? tree_proof
      | None
        Error_monad.Lwt_result_syntax.tzfail
          (Build_extensible "WASM_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 has_output `{FArgs} (function_parameter : PS.output)
      : State.Monad.t bool :=
      let '{|
        Sc_rollup_PVM_sig.output.outbox_level := outbox_level;
          Sc_rollup_PVM_sig.output.message_index := message_index;
          Sc_rollup_PVM_sig.output.message := message
          |} := function_parameter in
      State.Monad.Syntax.op_letstar State.Monad.get
        (fun s_value
          let lvl :=
            match Raw_level_repr.to_int32_non_negative outbox_level with
            | Pervasives.Ok lvllvl
            | Pervasives.Error _
              (* ❌ Assert instruction is not handled. *)
              assert Bounded.Non_negative_int32.(Bounded.S.t) false
            end in
          State.Monad.Syntax.op_letstar
            (State.Monad.lift
              (WASM_machine.(Wasm_2_0_0.S.get_output)
                {| Wasm_2_0_0.output.outbox_level := lvl;
                  Wasm_2_0_0.output.message_index := message_index; |} s_value))
            (fun result_value
              let message_encoded :=
                Data_encoding.Binary.to_string_exn None
                  Sc_rollup_outbox_message_repr.encoding message in
              State.Monad._return
                match result_value with
                | Some result_value
                  Compare.String.(Compare.S.op_eq) result_value message_encoded
                | Nonefalse
                end)).

    Definition verify_output_proof `{FArgs} (p_value : output_proof) : bool :=
      let transition :=
        State.Monad.run (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
          (State.Monad.run (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 "WASM_invalid_claim_about_outbox" unit tt)
      | None
        Error_monad.Lwt_result_syntax.fail
          (Build_extensible "WASM_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
      |}.
  End Make.
  Definition Make {Context_Tree_t Context_Tree_tree Context_proof : Set}
    (Make_backend :
       {Tree_t Tree_tree : Set},
       (Tree :
        Context.TREE (t := Tree_t) (tree := Tree_tree) (key := list string)
          (value := bytes)), Wasm_2_0_0.S (tree := Tree.(Context.TREE.tree)))
    (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 := _) :=
    let '_ := Make.Build_FArgs (@Make_backend) Context in
    Make.functor.

  Definition Protocol_implementation :=
    Make (@Wasm_2_0_0.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 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 sthsth
        | 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 sthsth
        | 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.proof_encoding := proof_encoding;
        P.proof_before := proof_before;
        P.proof_after := proof_after;
        P.verify_proof _ := verify_proof;
        P.produce_proof _ := produce_proof
      |}).
End V2_0_0.