🐆 Tx_rollup_services.v
Proofs
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.
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.