🐆 Tx_rollup_services.v

Proofs

See code, Gitlab , OCaml

Require Import CoqOfOCaml.CoqOfOCaml.
Require Import CoqOfOCaml.Settings.

Require Import TezosOfOCaml.Environment.V8.

Require TezosOfOCaml.Environment.V8.Proofs.Data_encoding.
Require TezosOfOCaml.Environment.V8.Proofs.RPC_service.

Require TezosOfOCaml.Proto_alpha.Tx_rollup_services.

Require TezosOfOCaml.Proto_alpha.Proofs.Raw_level_repr.
Require TezosOfOCaml.Proto_alpha.Proofs.Tez_repr.
Require TezosOfOCaml.Proto_alpha.Proofs.Tx_rollup_state_repr.

Module S.
  Lemma state_value_is_valid :
    RPC_service.Valid.t (fun _ ⇒ True) (fun _ ⇒ True)
      Tx_rollup_state_repr.Valid.t
      Tx_rollup_services.S.state_value.
  Proof.
    RPC_service.rpc_auto;
    intros [] []; repeat split; trivial.
  Qed.
End S.